PMW formal

README.md

@@ -1,3 +1,5 @@
+This is a fork of the clutch project in which I will do my M1 internship work.
+
 # Clutch Project
 
 This repository contains the formal development of a number of higher-order probabilistic separation logics for proving properties of higher-order probabilistic programs.

src/diffpriv/private_multiplicative_weights/README.md

@@ -0,0 +1,105 @@
+# Private Multiplicative Weights
+
+In this folder you will find an OCaml implementation of:
+- Numeric Sparse Vector technique
+- Private Multiplicative Weights
+
+The programs [`main_nsvt.ml`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/numeric_sparse_vector/main_nsvt.ml)
+and [`main_pmw.ml`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/numeric_sparse_vector/main_pmw.ml)
+are tests calling the two methods.
+
+## nSVT
+
+The numeric sparse vector technique is an algorithm which given:
+- A privacy parameter (`num`, `den`)
+- A threshold (`t`)
+- The maximum number of numeric answers (`n`)
+
+Outputs a function which given a database (`db`) and a query (`qi`) outputs:
+- `None`, if the value returned by the query on the db is under `t` or if it has
+        already answered more than `n` numeric values.
+- `Some (v)` with `v`$\in \mathbb(Z)$ otherwise.
+
+The `nSVT_stream` is a client which given a stream of queries (represented by a 
+function which computes the next query adaptively to the answers) returns the 
+list of the answers while preserving the $\varepsilon$-DP.
+
+## PMW
+
+The private multiplicative weights is a mechanism which given a database and 
+some privacy and accuracy parameters returns a function which one can call 
+with an adaptive stream of queries and get each time a numeric answer.
+
+This algorithm is working. There is just a point to raise.
+The implementation is derived from C.Dwork book on differential privacy (!!!cite better),
+in which the threshold is computed in order to match an accuracy statement.
+Since we are working on small databases, the threshold often get really high. 
+Then very few updates are made and the execution is not interesting.
+Then we can lower manually the threshold to get an interesting output.
+Even if it does change something about the accuracy statement, it do
+not change anything for the privacy one. 
+That is why we are making this choice. Then the threshold will need 
+to be modified depending on the database under study.
+
+For the [`main_pmw.ml`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/numeric_sparse_vector/main_pmw.ml)
+example, we consider the database that are randomly generated  [`rd_data.csv`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/numeric_sparse_vector/data/rd_data.csv)
+.
+Or the databases from ... (!!!push and cite the database.)
+
+In order to manage the databases, inputs, outputs and histograms we uses 
+functions defined in 
+[`utils.ml`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/numeric_sparse_vector/utils.ml).
+
+When calling:
+```bash
+ocaml main_pmw.ml
+```
+
+The output is, the initial database and the approached (sanitized) database as 
+well as the list (of the distances between the real answer and the returned 
+answer to the stream of queries) *see what to put in the final version*.
+
+You can add the three optional following arguments:
+- `--file [file]` in order to specify the database to use
+- `--list` use the list implementation.
+- `--gif` in order to save the databases in a folder and then to be able to 
+    build a graphical representation of the evolution of the sanitized database
+    during the update process.
+
+For the `--list` option, instead of using the hastable implementation, it uses
+lists. It is the translation of what is written in rocq into ocaml.
+It then uses a natural (int) distribution / it is not normalized.
+
+## DATA
+
+To get the data, you can go to [`data/`](https://github.com/Pbi0/clutch/tree/pMW_formal/src/diffpriv/private_multiplicative_weights/data).
+
+## GIF
+
+If you want to have a gif illustration of the distribution evolution during
+the pmw, you can add the argument `--gif` when calling
+[`main_pmw.ml`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/numeric_sparse_vector/main_pmw.ml)
+and then can go to [`gif/`](https://github.com/Pbi0/clutch/tree/pMW_formal/src/diffpriv/private_multiplicative_weights/gif)
+where you will find in the folder `gif/data/` all the distribution that $h$
+went through. The 0 database is the real database.
+In order to get the gif, go in the `gif/` folder and run:
+```bash
+python render_gif.py
+```
+or 
+```bash
+./render_gif.py
+```
+
+It will build the gif under the name of `evolution_distrib.gif`.
+What follows is a output of this function.\
+You can find the parameters for this
+output in [gif/ref_evolution/](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/).
+
+![Evolution of the distribution.](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/evolution_distrib.gif?raw=true "Evolution of the distribution.")
+
+## NOTES
+
+We use the probability sampler from [`noiseSampling.ml`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/numeric_sparse_vector/noiseSampling.ml)
+which is a truncated part 
+of the file [`../differential_privacy.ml`](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/differential_privacy.ml).

src/diffpriv/private_multiplicative_weights/data/README.md

@@ -0,0 +1,23 @@
+# DATA
+
+In this folder you will find a python script which generate random data.
+You can execute it with the following  command:
+```bash
+python gen_data.py
+```
+
+## The script
+
+In the current version the script writes in the file `rd_data.csv` a random 
+sequence of integers between 0 and 9 with a probability of $\frac{1}{4}$ for 1, 
+$\frac{1}{16}$ for 2 and so on (exponential) and stops at 12.
+
+## Other data
+
+Other kind of data can be used.
+As the algorithm uses strings as key for the database any file could 
+be a database. However the bigger is the domain / the number of different
+records in the database / the number of different lines in the file,
+the bigger the number of query will be and then the longer it will take.
+The execution time is exponential in the size of the domain.
+

src/diffpriv/private_multiplicative_weights/data/gen_data.py

@@ -0,0 +1,21 @@
+#!/usr/bin/python3
+
+from random import randint
+
+
+if __name__ == "__main__":
+    size = 1_000_000
+    nb_o = 13
+
+    with open("rd_data.csv", "w", encoding="utf-8") as f:
+        for i in range(size):
+            token = True
+            count = 0
+            while token and count < nb_o:
+                if randint(0, 3) == 0:
+                    f.write(str(count)+"\n")
+                    token = False
+                count += 1
+            if token:
+                f.write(str(nb_o)+"\n")
+

src/diffpriv/private_multiplicative_weights/gif/README.md

@@ -0,0 +1,35 @@
+# GIF
+
+In this folder there are files allowing you to build a gif illustration of the 
+evolution of the distribution during the `pMW`.
+
+Once you have called `main_pmw.ml` with the argument `--gif` then you will 
+have all the databases that the distribution $h$ went through (stored in `data/`). 
+The $0^{th}$ database is the real distribution.
+In order to get the gif, run:
+```bash
+python render_gif.py
+```
+or (if you run before `chmod +x render_gif.py`)
+```bash
+./render_gif.py
+```
+
+The `DB` histogram represents the real database while the `sDB` histogram
+represents the sanitized database. It is the one evolving during the process.
+I the initial database for `sDB` is the uniforme database then there should not 
+have any problem with the axis. However since they are clipped on the values of 
+the real database, the histograms might sometimes overpass the view (but it is 
+really unlikely)
+
+To do something perfect where the axis are clipped and where everything is in
+the view, we should range twice each database to first find the global maximum
+and then to build the plots. We prefer clipping the axis based on `DB` which
+is fixed and who should be the histogram towards which tends `sDB`.
+
+# Illustration of the issue that comes with the lists implementation
+
+In [`heterogenous_database`](https://github.com/Pbi0/clutch/tree/pMW_formal/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/)link to the folder you can find several evolutions and the parameters 
+associated. It illustrates the issue we encountered with the list 
+implementation.
+

src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/README.md

@@ -0,0 +1,60 @@
+# Heterogenous Database
+
+In this folder you can find the representation of the evolution of
+$h$ on a database with a huge domain and the distribution over it
+is far from beeing uniform.
+
+The data under study are from the [programming dp book](https://github.com/uvm-plaid/programming-dp/blob/master/notebooks/adult_with_pii.csv).
+
+## Evolution with the probability distribution (Hasthbl. implmentation)
+
+With the following parameters :
+
+|   Parameter   |    Value   |
+|:--------------|-----------:|
+| $\varepsilon$ |        $1$ |
+| $\alpha$      |     $1/10$ |
+| $\beta$       |     $1/10$ |
+| $\eta$        | $\alpha/2$ |
+
+We get the following evolution :
+
+![Evolution of the distribution.](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib.gif?raw=true "Evolution of the distribution.")
+
+We don't have the issue in the normalizing step.
+
+## Evolution with the count histograms (List. implementation)
+
+With the following parameters :
+
+|   Parameter   |    Value   |
+|:--------------|-----------:|
+| $\varepsilon$ |        $1$ |
+| $\alpha$      |    $1/100$ |
+| $\beta$       |    $1/100$ |
+| $\eta$        | $\alpha$/2 |
+
+We get the following evolution :
+
+![Evolution of the distribution.](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_issue.gif?raw=true "Evolution of the distribution with overestimation of the first elements.")
+
+We can see the issue in the scaling step.
+The firsts elements are overestimated and
+some elements (the small ones) are underestimated.
+
+While with the following parameters :
+
+|   Parameter   |    Value   |
+|:--------------|-----------:|
+| $\varepsilon$ |        $1$ |
+| $\alpha$      |    $1/100$ |
+| $\beta$       |    $1/100$ |
+| $\eta$        | $6*\alpha$ |
+
+We get the following evolution :
+
+![Evolution of the distribution.](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_adapted_factor.gif?raw=true "Evolution of the distribution with an addapted learning factor.")
+
+We can see that there is no longer overestimation and that the convergence is 
+faster as well. However there is more gittering (it is less precise than the
+first example using the Hastbl. implementation.

src/diffpriv/private_multiplicative_weights/gif/ref_evolution/README.md

@@ -0,0 +1,17 @@
+# Reference evolution
+
+This evolution is the one on the database that is generated randomly.
+It uses the List. implementation.
+We see that it converges.
+
+The parameters are the following:
+
+|   Parameter   |    Value   |
+|:--------------|-----------:|
+| $\varepsilon$ |        $1$ |
+| $\alpha$      |    $1/100$ |
+| $\beta$       |    $1/100$ |
+| $\eta$        | $\alpha/2$ |
+
+
+![Evolution of the distribution.](https://github.com/Pbi0/clutch/blob/pMW_formal/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/evolution_distrib.gif?raw=true "Evolution of the distribution.")

src/diffpriv/private_multiplicative_weights/gif/render_gif.py

@@ -0,0 +1,65 @@
+#!/usr/bin/python3
+
+import csv
+import matplotlib.pyplot as plt
+from PIL import Image
+import io
+
+def max_l(l):
+    a = 0
+    for x in l:
+        if a < x:
+            a = x
+    return a
+
+fps = 10
+ts = 20
+
+
+if __name__ == "__main__":
+    images = []
+
+    with open("data/len.csv", "r") as flen:
+        datalen = csv.reader(flen)
+        nb_images = 0
+        for row in datalen:
+            nb_images = int(row[0])
+        step = nb_images/(fps*ts)
+        with open("data/gif0.csv", "r") as f0:
+            data0 = csv.reader(f0)
+            x0 = []
+            y0 = []
+            max_d = 0
+            for row in data0:
+                #x0.append(int(row[0]))
+                x0.append(row[0])
+                y0.append(float(row[1]))
+                if max_d < float(row[1]):
+                    max_d = float(row[1])
+            for i in range(0, nb_images, int(step)):
+                #if i % int(step) == 0:
+                #    print(str(int(1000*i/nb_images)/10) + "%", "\r", end="")
+                print(str(int(1000*i/nb_images)/10) + "%", "\r", end="")
+                with open(f"data/gif{i+1}.csv", "r") as f:
+                    data = csv.reader(f)
+                    x = []
+                    y = []
+                    for row in data:
+                        #x.append(int(row[0]))
+                        x.append(row[0])
+                        y.append(float(row[1]))
+                    fig, ax = plt.subplots()
+                    ax.bar(x0, y0, color='yellow', alpha=0.8, label='DB')
+                    ax.bar(x, y, color='cyan', alpha=0.5, label='sDB')
+                    ax.set_ylim(0, max_d+max_d/10)
+                    plt.legend(loc='upper left')
+
+                    buf = io.BytesIO()
+                    fig.savefig(buf, format='png')
+                    buf.seek(0)
+                    images.append(Image.open(buf))
+                    plt.close()
+    print("exporting")
+    images[0].save('evolution_distrib.gif',
+                   save_all=True, append_images=images[1:],
+                   optimize=False, duration=5*ts)

src/diffpriv/private_multiplicative_weights/main_nsvt.ml

@@ -0,0 +1,59 @@
+#use "numeric_sparse_vector.ml"
+
+let path = "data/"
+let file = "data0"
+let () = Random.self_init ()
+
+let mk_array file =
+  (* turn a column file of numbers into a int Array *)
+  let reader = open_in (path ^ file) in
+  let rec aux reader acc =
+    try
+      let line = input_line reader in
+      aux reader (string_to_int line :: acc)
+    with e ->
+      close_in_noerr reader;
+      acc
+  in
+  Array.of_list (aux reader [])
+
+let count_above t l =
+  Array.fold_left (fun x y -> x + if y > t then 1 else 0) 0 l
+
+let () =
+  let db = mk_array file in
+  let stream_query =
+    let a = ref 1000 in
+    fun bs ->
+      if !a <= 0 then None
+      else (
+        a := !a - 1;
+        Some (count_above !a))
+  in
+  Printf.printf "\nSmall epsilon -->\n";
+  let res = nSVT_stream 1 30 200 20 stream_query db in
+  aff_l_op res;
+
+  let stream_query =
+    let a = ref 1000 in
+    fun bs ->
+      if !a <= 0 then None
+      else (
+        a := !a - 1;
+        Some (count_above !a))
+  in
+  Printf.printf "\nMedium (=1) epsilon -->\n";
+  let res = nSVT_stream 1 1 200 20 stream_query db in
+  aff_l_op res;
+
+  let stream_query =
+    let a = ref 1000 in
+    fun bs ->
+      if !a <= 0 then None
+      else (
+        a := !a - 1;
+        Some (count_above !a))
+  in
+  Printf.printf "\nLarge epsilon -->\n";
+  let res = nSVT_stream 30 1 200 20 stream_query db in
+  aff_l_op res