diff --git a/README.md b/README.md
index 5e68ed4e6..f81707514 100644
--- a/README.md
+++ b/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.
diff --git a/src/diffpriv/private_multiplicative_weights/README.md b/src/diffpriv/private_multiplicative_weights/README.md
new file mode 100644
index 000000000..151af6848
--- /dev/null
+++ b/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).
diff --git a/src/diffpriv/private_multiplicative_weights/data/README.md b/src/diffpriv/private_multiplicative_weights/data/README.md
new file mode 100644
index 000000000..97946ee05
--- /dev/null
+++ b/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.
+
diff --git a/src/diffpriv/private_multiplicative_weights/data/gen_data.py b/src/diffpriv/private_multiplicative_weights/data/gen_data.py
new file mode 100755
index 000000000..82e3d72a5
--- /dev/null
+++ b/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")
+
diff --git a/src/diffpriv/private_multiplicative_weights/gif/README.md b/src/diffpriv/private_multiplicative_weights/gif/README.md
new file mode 100644
index 000000000..dfc32902e
--- /dev/null
+++ b/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.
+
diff --git a/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/README.md b/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/README.md
new file mode 100644
index 000000000..f38441a47
--- /dev/null
+++ b/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.
diff --git a/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib.gif b/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib.gif
new file mode 100644
index 000000000..b6b33193d
Binary files /dev/null and b/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib.gif differ
diff --git a/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_adapted_factor.gif b/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_adapted_factor.gif
new file mode 100644
index 000000000..1b2173030
Binary files /dev/null and b/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_adapted_factor.gif differ
diff --git a/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_issue.gif b/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_issue.gif
new file mode 100644
index 000000000..89e47603d
Binary files /dev/null and b/src/diffpriv/private_multiplicative_weights/gif/heterogenous_database/evolution_distrib_issue.gif differ
diff --git a/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/README.md b/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/README.md
new file mode 100644
index 000000000..120f4e4d5
--- /dev/null
+++ b/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.")
diff --git a/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/evolution_distrib.gif b/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/evolution_distrib.gif
new file mode 100644
index 000000000..a309202c8
Binary files /dev/null and b/src/diffpriv/private_multiplicative_weights/gif/ref_evolution/evolution_distrib.gif differ
diff --git a/src/diffpriv/private_multiplicative_weights/gif/render_gif.py b/src/diffpriv/private_multiplicative_weights/gif/render_gif.py
new file mode 100755
index 000000000..ae7f6da28
--- /dev/null
+++ b/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)
diff --git a/src/diffpriv/private_multiplicative_weights/main_nsvt.ml b/src/diffpriv/private_multiplicative_weights/main_nsvt.ml
new file mode 100644
index 000000000..3d8c3ec2f
--- /dev/null
+++ b/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
diff --git a/src/diffpriv/private_multiplicative_weights/main_pmw.ml b/src/diffpriv/private_multiplicative_weights/main_pmw.ml
new file mode 100644
index 000000000..5fc707cc4
--- /dev/null
+++ b/src/diffpriv/private_multiplicative_weights/main_pmw.ml
@@ -0,0 +1,102 @@
+#use "private_multiplicative_weights.ml"
+let () = Random.self_init ()
+
+let path = "data/"
+let file = "state.csv"
+(* let file = "adult_with_pii_sanitized_short.csv" *)
+
+let path_gif = "gif/data/"
+let file_gif = "gif"
+
+let () =
+  let file = match List.find_index (fun x -> x = "--file") (Array.to_list Sys.argv) with
+    | Some i -> Sys.argv.(i+1)
+    | None -> "rd_data.csv"
+  in
+  if (Array.mem "--list" Sys.argv) then (
+    let size, index, db = mk_histo_l (path ^ file) in
+    let log_card_q = List.length index in
+    let nb_q = 1_000 * log_card_q in
+    let stream_query =
+      let a = ref nb_q in
+      fun bs ->
+        if !a <= 0 then None
+        else (
+          a := !a - 1;
+          Some
+            (get_rd_query_l index))
+    in
+    let res, db', nb_upd, c, t =
+      oPMW_l
+        size
+        db
+        index
+        (get_unif_l index size)
+        stream_query
+        (float_of_int log_card_q)
+        1 1 1 100 1 100
+        ~gif:(if (Array.mem "--gif" Sys.argv) then Some (path_gif ^ file_gif) else None)
+    in
+    if (Array.mem "--gif" Sys.argv) then (
+      let writer = open_out (path_gif ^ "len.csv") in
+      Printf.fprintf writer "%d\n" nb_upd;
+      close_out writer
+    );
+    Printf.(
+      printf "c: %d\nt: %d\n" c t;
+      printf "- NB UPDATE : %d\n- ORIGINAL DB :\n" nb_upd;
+      aff_db_l db index;
+      printf "\n\n- SANITIZED DB :\n";
+      aff_db_l db' index;
+      printf "\n\n- UNIF DB :\n";
+      aff_db_l (get_unif_l index size) index;
+      printf "\n\n- LIST RESULT :\n";
+      printf "%d\n" (max_l2 res);
+      printf "size init : %d | size fin : %d\n" (sum_l db) (sum_l db');
+      ()
+    )
+  )
+  else (
+    let size, domaine, db = mk_histo (path ^ file) in
+    (* Printf.printf "tl: %d\n" (pow 2 (List.length domaine)); *)
+    (* let card_q = pow 2 (List.length domaine) in *)
+    (* let nb_q = 2 * card_q in *)
+    let log_card_q = List.length domaine in
+    let nb_q = 10000 * log_card_q in
+    let stream_query =
+      let a = ref nb_q in
+      fun bs ->
+        if !a <= 0 then None
+        else (
+          a := !a - 1;
+          Some
+            (get_rd_query domaine))
+    in
+    let res, db', nb_upd, c, t =
+      oPMW
+        size
+        domaine
+        db
+        (get_unif domaine)
+        stream_query
+        (float_of_int log_card_q)
+        1 1 0.01 0.01
+        ~gif:(if (Array.mem "--gif" Sys.argv) then Some (path_gif ^ file_gif) else None)
+    in
+    if (Array.mem "--gif" Sys.argv) then (
+      let writer = open_out (path_gif ^ "len.csv") in
+      Printf.fprintf writer "%d\n" nb_upd;
+      close_out writer
+    );
+    Printf.(
+      printf "c: %f\nt: %f\n" c t;
+      printf "- NB UPDATE : %d\n- ORIGINAL DB :\n" nb_upd;
+      aff_db db;
+      printf "\n\n- SANITIZED DB :\n";
+      aff_db db';
+      printf "\n\n- LIST RESULT :\n";
+      printf "%f\n" (max_l res);
+      printf "Above 0.1: %f (%d/%d)\n" ( float_of_int (count_above res 0.1) /. float_of_int nb_q) (count_above res 0.1) nb_q;
+      printf "Above 0.01: %f (%d/%d)\n" ( float_of_int (count_above res 0.01) /. float_of_int nb_q) (count_above res 0.01) nb_q
+    )
+  )
diff --git a/src/diffpriv/private_multiplicative_weights/noiseSampling.ml b/src/diffpriv/private_multiplicative_weights/noiseSampling.ml
new file mode 100644
index 000000000..1a35746bb
--- /dev/null
+++ b/src/diffpriv/private_multiplicative_weights/noiseSampling.ml
@@ -0,0 +1,125 @@
+(** Sampling Noise from the ClutchProcjet https://github.com/logsem/clutch *)
+module Q = struct
+  type t = int * int
+
+  let num_den_of_q (x : t) : int * int = x
+  let inverse (num, den) = (den, num)
+  let float_of_q (num, den) = float_of_int num /. float_of_int den
+  let mk num den = (num, den)
+  let rec gcd a b = if b = 0 then a else gcd b (a mod b)
+
+  let normalize (num, den) =
+    let k = gcd num den in
+    (num / k, den / k)
+
+  let sub (x_num, x_den) (y_num, y_den) =
+    let k = gcd x_den y_den in
+    let y' = y_den / k in
+    ((x_num * y') - (y_num * (x_den / k)), x_den * y')
+
+  let lt (x_num, x_den) (y_num, y_den) = x_num * y_den < y_num * x_den
+
+  let mult (x_num, x_den) (y_num, y_den) =
+    normalize (x_num * y_num, x_den * y_den)
+end
+
+let sample_distr d n =
+  let rec f n xs = if n = 0 then xs else f (n - 1) (d () :: xs) in
+  f n []
+
+let geo () =
+  let rec geo_rec n = if Random.bool () then n else geo_rec (n + 1) in
+  geo_rec 0
+
+(* Most of the sampling code below is hand-ported from SampCert *)
+let rec probWhile cond body state =
+  if cond state then probWhile cond body (body state) else state
+
+let probUntil body cond =
+  probWhile (fun v -> not (cond v)) (fun _st -> body ()) (body ())
+
+let bernoulli_sample num den =
+  let d = Random.full_int den in
+  d < num
+
+let bernoulliExpNegSampleUnitLoop num den (_, st2) : bool * int =
+  let a = bernoulli_sample num (st2 * den) in
+  (a, st2 + 1)
+
+let bernoulliExpNegSampleUnitAux num den : int =
+  probWhile fst (bernoulliExpNegSampleUnitLoop num den) (true, 1) |> snd
+
+let bernoulliExpNegSampleUnit num den =
+  let k = bernoulliExpNegSampleUnitAux num den in
+  k mod 2 = 0
+
+let rec bernoulliExpNegSampleGenLoop iter =
+  match iter with
+  | 0 -> true
+  | _ ->
+      let b = bernoulliExpNegSampleUnit 1 1 in
+      if not b then b else bernoulliExpNegSampleGenLoop (iter - 1)
+
+let bernoulliExpNegSample num den =
+  if num <= den then bernoulliExpNegSampleUnit num den
+  else
+    let b =
+      bernoulliExpNegSampleGenLoop
+        (let gamf = num / den in
+         gamf)
+    in
+    if b then bernoulliExpNegSampleUnit (num mod den) den else false
+
+let discreteLaplaceSampleLoopIn1Aux (t : int) : int * bool =
+  let u = Random.full_int t in
+  let d = bernoulliExpNegSample u t in
+  (u, d)
+
+let discreteLaplaceSampleLoopIn1 (t : int) : int =
+  probUntil (fun () -> discreteLaplaceSampleLoopIn1Aux t) snd |> fst
+
+let discreteLaplaceSampleLoopIn2Aux num den k =
+  let a = bernoulliExpNegSample num den in
+  (a, snd k + 1)
+
+let discreteLaplaceSampleLoopIn2 num den =
+  probWhile fst (discreteLaplaceSampleLoopIn2Aux num den) (true, 0) |> snd
+
+let discreteLaplaceSampleLoop' num den : bool * int =
+  let u = discreteLaplaceSampleLoopIn1 num in
+  let v = discreteLaplaceSampleLoopIn2 1 1 in
+  let v' = v - 1 in
+  let x = u + (num * v') in
+  let y = x / den in
+  let b = Random.bool () in
+  (b, y)
+
+let discreteLaplaceSampleLoop num den =
+  let v = discreteLaplaceSampleLoopIn2 den num in
+  let v' = v - 1 in
+  let b = Random.bool () in
+  (b, v')
+
+let discreteLaplaceSample num den : int =
+  let r =
+    probUntil
+      (fun () -> discreteLaplaceSampleLoop num den)
+      (fun x -> not (fst x && snd x = 0))
+  in
+  if fst r then -snd r else snd r
+
+let discreteLaplaceSampleOptimized num den : int =
+  let r =
+    probUntil
+      (fun () -> discreteLaplaceSampleLoop' num den)
+      (fun x -> not (fst x && snd x = 0))
+  in
+  if fst r then -snd r else snd r
+
+(* differential privacy style inverted scale *)
+let laplace_discrete (scale : Q.t) (mean : int) =
+  let num, den = Q.num_den_of_q scale in
+  let x = discreteLaplaceSample den num in
+  x + mean
+
+(** End of noize sampling from clutch *)
diff --git a/src/diffpriv/private_multiplicative_weights/numeric_sparse_vector.ml b/src/diffpriv/private_multiplicative_weights/numeric_sparse_vector.ml
new file mode 100644
index 000000000..07d57e78b
--- /dev/null
+++ b/src/diffpriv/private_multiplicative_weights/numeric_sparse_vector.ml
@@ -0,0 +1,34 @@
+#use "noiseSampling.ml"
+#use "utils.ml"
+
+let num_above_threshold num den t =
+  let t' = laplace_discrete (Q.mk (4 * num) (9 * den)) t in
+  fun db q ->
+    let vi = laplace_discrete (Q.mk (2 * num) (9 * den)) (q db) in
+    if t' <= vi then Some (laplace_discrete (Q.mk num (9 * den)) (q db))
+    else None
+
+let num_sparse_vector num den t n =
+  let count = ref (n - 1) in
+  let nAT = ref (num_above_threshold num den t) in
+  fun db qi ->
+    let bq = !nAT db qi in
+    if !count <= 0 || bq = None then ()
+    else (
+      nAT := num_above_threshold num den t;
+      count := !count + 1);
+    bq
+
+let nSVT_stream num den t n stream_qs db =
+  let f = num_sparse_vector num den t n in
+  let rec nSVT i bs =
+    if i = n then bs
+    else
+      begin match stream_qs bs with
+      | None -> bs (* end of stream *)
+      | Some q ->
+          let b = f db q in
+          nSVT (if b = None then i else i + 1) (b :: bs)
+      end
+  in
+  nSVT 0 []
diff --git a/src/diffpriv/private_multiplicative_weights/private_multiplicative_weights.ml b/src/diffpriv/private_multiplicative_weights/private_multiplicative_weights.ml
new file mode 100644
index 000000000..196c29272
--- /dev/null
+++ b/src/diffpriv/private_multiplicative_weights/private_multiplicative_weights.ml
@@ -0,0 +1,81 @@
+#use "numeric_sparse_vector.ml"
+(* #use "db_query.ml" *)
+
+(* Hashtbl. implementation *)
+let mw x f v eta =
+  let r = Hashtbl.copy f in
+  if v >= c_query f x then Hashtbl.iter (fun a b -> Hashtbl.replace r a (1. -. b)) r;
+  Hashtbl.iter (fun a b -> Hashtbl.replace r a ((exp ((-.eta) *. b)) *. (Hashtbl.find x a))) r;
+  norm r;
+  r
+
+let oPMW ?(gif=None) size domaine db unif stream_q log_card_q num den alpha beta =
+  write_db db gif 0;
+  let c = 4. *. (log (float_of_int (List.length domaine))) /.  (alpha *. alpha) in
+  (* let t = 0.000005 *. (float_of_int size) *. ((float_of_int den) *. 18. *. c *. (log (2.) +. log_card_q +. log (4. *. c) -. log beta)) /. ((float_of_int num) *. (float_of_int size)) in *)
+  let t = ((float_of_int den) *. 18. *. c *. (log (2.) +. log_card_q +. log (4. *. c) -. log beta)) /. ((float_of_int num) *. (float_of_int size)) in
+  let f = num_sparse_vector num den (int_of_float t) (int_of_float c) db in
+  let rec aux i bs distrib =
+    match stream_q bs with
+    | None -> (bs, distrib, i, c, t) (* no more queries we stop *)
+    | Some q -> (
+        if i >= int_of_float c then (* we retrun only from the distribution *)
+          aux i ((abs_f (c_query q db -. c_query q distrib)) :: bs) distrib
+        else (
+          (match f (fun x' -> int_of_float ((float_of_int size) *. (c_query q x' -. c_query q distrib))) with
+          | None -> ( match f (fun x' -> int_of_float ((float_of_int size) *. (c_query q distrib -. c_query q x'))) with
+              | None -> aux i ((abs_f (1. -. c_query q db /. c_query q distrib)) :: bs) distrib
+              | Some v -> (
+                  write_db distrib gif (i +1) ;
+                  let a = c_query q distrib -. float_of_int v /. (float_of_int size) in
+                  aux (i + 1) ((abs_f (1. -. c_query q db /. a)) :: bs) (mw distrib q a  (alpha /. 2.))))
+          | Some v -> (
+              write_db distrib gif (i +1) ;
+              let a = c_query q distrib +. float_of_int v /. (float_of_int size) in
+              aux (i + 1) ((abs_f (1.-. c_query q db /. a)) :: bs) (mw distrib q a  (alpha /. 2.)))
+          )
+        )
+    )
+  in
+  aux 0 [] unif
+
+(* List implementation *)
+let mw_l db size q v etanum etaden =
+  if c_query_l q db < v
+  then normalize_l (List.mapi (fun i x -> int_of_float(exp (-. ((float_of_int etanum) /. (float_of_int etaden)) *. (if List.nth q i then 0. else 1.)) *. (float_of_int x))) db) size
+  else normalize_l (List.mapi (fun i x -> int_of_float(exp (-. ((float_of_int etanum) /. (float_of_int etaden)) *. (if List.nth q i then 1. else 0.)) *. (float_of_int x))) db) size
+
+let oPMW_large gif size db index unif stream_q log_card_q enum eden anum aden bnum bden c t upd f1 f2=
+  write_db_l index db gif 0;
+  let f = num_sparse_vector enum eden t c db in
+  let rec aux i bs distrib =
+    match stream_q bs with
+    | None -> (bs, distrib, i, c, t) (* no more queries we stop *)
+    | Some q -> (
+        if i >= c then (* we retrun only from the distribution *)
+          aux i ((abs (c_query_l q db - c_query_l q distrib)) :: bs) distrib
+        else (
+          (match f (f1 q distrib) with
+          | None -> (match f (f2 q distrib) with
+              | None -> aux i ((abs (c_query_l q db - c_query_l q distrib)) :: bs) distrib
+              | Some v -> (
+                  write_db_l index distrib gif (i +1) ;
+                  let a = c_query_l q distrib - v in
+                  aux (i + 1) ((abs (c_query_l q db - a)) :: bs) (upd distrib size q a  (anum) (2*aden) )))
+          | Some v -> (
+              write_db_l index distrib gif (i +1) ;
+              let a = c_query_l q distrib + v in
+              aux (i + 1) ((abs (c_query_l q db - a)) :: bs) (upd distrib size q a  (anum) (2*aden)))
+          )
+        )
+    )
+  in
+  aux 0 [] unif
+
+let oPMW_l ?(gif=None) size db index unif stream_q log_card_q enum eden anum aden bnum bden =
+  write_db_l index db gif 0;
+  let c = int_of_float (4. *. (log (float_of_int (List.length db))) *. (float_of_int aden *. float_of_int aden) /.  (float_of_int anum *. float_of_int anum)) in
+  let t = int_of_float (1. *. ((float_of_int eden) *. 18. *. (float_of_int c) *. (log (2.) +. log_card_q +. log (4. *. (float_of_int c)) -. log (float_of_int bnum)) +. log (float_of_int bden)) /. ((float_of_int enum) *. (float_of_int size))) in
+  let f1 = (fun q distrib x' -> c_query_l q x' - c_query_l q distrib) in
+  let f2 = (fun q distrib x' -> c_query_l q distrib - c_query_l q x') in
+  oPMW_large gif size db index unif stream_q log_card_q enum eden anum aden bnum bden c t (mw_l) (f1) f2
diff --git a/src/diffpriv/private_multiplicative_weights/utils.ml b/src/diffpriv/private_multiplicative_weights/utils.ml
new file mode 100644
index 000000000..64678695f
--- /dev/null
+++ b/src/diffpriv/private_multiplicative_weights/utils.ml
@@ -0,0 +1,172 @@
+(** Various functions *)
+
+let rec pow m n =
+  if n = 0 then 1
+  else if n mod 2 = 0 then pow (m * m) (n / 2)
+  else m * pow (m * m) ((n - 1) / 2)
+
+let abs_f x =
+  if x<0. then -.x else x
+
+let string_to_int s =
+  let l = String.length s in
+  let res = ref 0 in
+  for i = 0 to l - 1 do
+    res := !res + (Char.(code s.[l - 1 - i] - code '0') * pow 10 i)
+  done;
+  !res
+
+let int_to_string i =
+  if i = 0 then "0"
+  else (
+  let rec aux i s =
+    if i = 0 then s
+    else aux (i/10) (String.make 1 Char.(chr (i mod 10 + code '0')) ^ s)
+  in aux i ""
+ )
+
+let aff_flst l =
+  List.iter (fun x -> Printf.printf "%f|" x) l;
+  Printf.printf "\n"
+
+let max_l l =
+  List.fold_left max 0. l
+
+let count_above l n =
+  List.fold_left (fun acc x -> if x > n then acc + 1 else acc) 0 l
+
+let aff_l_op l =
+  List.fold_left
+    (fun _ y ->
+      match y with
+      | None -> Printf.printf "⊥\n"
+      | Some n -> Printf.printf "%d\n" n)
+    () l
+
+
+(** Utils function for the Hashtbl. implementation *)
+
+let norm htbl =
+  (* normalizes a hashtabl *)
+  let sum = Hashtbl.fold (fun _ b acc -> acc +. b) htbl 0. in
+  Hashtbl.iter (fun a b -> Hashtbl.replace htbl a (b /. sum)) htbl
+
+let mk_histo file =
+  (* compute the histogram of the db contained in file *)
+  let reader = open_in 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
+  let ht = Hashtbl.create 150 in
+  let rec mk_domaine lst acc =
+    match lst with
+    | [] -> acc
+    | h::t ->
+      if Hashtbl.mem ht h then (
+        Hashtbl.replace ht h (1. +. Hashtbl.find ht h);
+        mk_domaine t acc)
+      else (
+        Hashtbl.add ht h 1.;
+        mk_domaine t (h::acc))
+  in
+  let raw = aux reader [] in
+  let size = List.length raw in
+  let domain = mk_domaine raw [] in
+  norm ht;
+  (size, domain, ht)
+
+let write_db db gif i =
+  (* when gif = Some file, write the database in file_i.csv *)
+  match gif with
+  | Some file ->
+    let writer = open_out (file ^ (int_to_string i) ^ ".csv") in
+    Hashtbl.iter (fun a b -> Printf.fprintf writer "%s,%f\n" a b) db;
+    close_out writer
+  | _ -> ()
+
+let get_rd_query domaine =
+  (* given a domaine returns a random query (random map of domain -> {0, 1}) *)
+  let res = Hashtbl.create 150 in
+  List.iter (fun x -> Hashtbl.add res x (float_of_int (Random.int 2))) domaine;
+  res
+
+let c_query q db =
+  (* given a query and a db compute the result (scalar product) *)
+  Hashtbl.fold
+    (fun a b acc -> acc +. (b *. (Hashtbl.find db a))) q 0.
+
+let get_unif domaine =
+  (* returns the uniform db on domaine *)
+  let res = Hashtbl.create 150
+  and s = List.length domaine in
+  List.iter (fun x -> Hashtbl.add res x (1. /. float_of_int s)) domaine;
+  res
+
+let aff_db db =
+  (* displays db *)
+  Printf.printf "Aff_db ---\n---";
+  Hashtbl.iter (fun a b -> Printf.printf " %s: %f\n---" a b) db;
+  Printf.printf "> OK\n"
+
+let aff_bq bq  =
+  (* displays the boolean query *)
+  Printf.printf "Aff_bq ---\n---";
+  Hashtbl.iter (fun a b -> Printf.printf "%s:%d|" a (int_of_float b)) bq;
+  Printf.printf "\n"
+
+
+(** Utils functions for the list implementation *)
+
+let sum_l l =
+  List.fold_left (fun acc x -> acc + x) 0 l
+
+let normalize_l l size =
+  let s = sum_l l in
+  let ln = List.map (fun x -> (size * x)/s) l in
+  let s' = sum_l ln and
+      lln = List.length ln in
+  List.mapi (fun i x -> (if i <= size - s' - 1 mod lln then 1 else 0) + (((size - s'))/lln) + x) ln
+
+let mk_histo_l file =
+  let (size, index, ht) = mk_histo file in
+  (size, index, normalize_l (List.map (fun x -> int_of_float (Hashtbl.find ht x *. (float_of_int size))) index) size)
+
+let write_db_l domain db gif i =
+  (* when gif = Some file, write the database in file_i.csv *)
+  match gif with
+  | Some file ->
+    let writer = open_out (file ^ (int_to_string i) ^ ".csv") in
+    List.iteri (fun i x -> Printf.fprintf writer "%s,%d\n" x (List.nth db i)) domain;
+    close_out writer
+  | _ -> ()
+
+let get_rd_query_l domaine =
+  (* given a domaine returns a random query (random map of domain -> {0, 1}) *)
+  List.map (fun x -> (0 = Random.int 2)) domaine
+
+let get_unif_l domaine size =
+  (* returns the uniform db on domaine *)
+  normalize_l List.(init (length domaine) (fun i -> 1)) size
+
+let c_query_l q db =
+  (* given a query and a db compute the result (scalar product) *)
+  snd List.(
+      if length db <= length q
+      then
+        fold_left (fun acc x -> (fst acc +1, snd acc + if nth q (fst acc) then x else 0)) (0, 0) db
+      else
+        fold_left (fun acc x -> (fst acc +1, snd acc + if x then nth db (fst acc) else 0)) (0, 0) q)
+
+let aff_db_l db index =
+  (* displays db *)
+  Printf.printf "Aff_db ---\n---";
+  List.iteri (fun i a -> Printf.printf " %s: %d\n---" a (List.nth db i)) index;
+  Printf.printf "> OK\n"
+
+let max_l2 l =
+  List.fold_left max 0 l
diff --git a/theories/diffpriv/examples/numeric_sparse_vector_technique.v b/theories/diffpriv/examples/numeric_sparse_vector_technique.v
new file mode 100644
index 000000000..0e486a90d
--- /dev/null
+++ b/theories/diffpriv/examples/numeric_sparse_vector_technique.v
@@ -0,0 +1,355 @@
+From iris.base_logic Require Export na_invariants.
+From clutch.common Require Import inject.
+From clutch.prelude Require Import tactics.
+From clutch.prob Require Import differential_privacy.
+From clutch.diffpriv Require Import adequacy diffpriv proofmode.
+From clutch.diffpriv.examples Require Import list.
+
+Section nsvt.
+  Context `{!diffprivGS Σ}.
+
+  #[local] Open Scope R.
+
+  Lemma Rdiv_pos_pos x y a (div_pos: 0 < x/y) (den_pos : 0 < a) : 0 < x / (a*y).
+  Proof.
+    destruct (Rdiv_pos_cases _ _ div_pos) as [[]|[]].
+    - apply Rdiv_pos_pos ; real_solver.
+    - apply Rdiv_neg_neg ; try real_solver.
+      rewrite Rmult_comm.
+      apply Rmult_neg_pos => //.
+  Qed.
+
+  Lemma Rdiv_nneg_nneg x y a (div_nneg: 0 <= x/y) (den_nneg : 0 <= a) : 0 <= x / (a*y).
+  Proof.
+    destruct (Rle_lt_or_eq _ _ div_nneg) as [|h].
+    - destruct (Rle_lt_or_eq _ _ den_nneg).
+      + left. apply Rdiv_pos_pos => //.
+      + subst. rewrite Rmult_0_l. rewrite Rdiv_0_r. done.
+    - rewrite Rmult_comm. rewrite Rdiv_mult_distr. rewrite -h. rewrite /Rdiv. lra.
+  Qed.
+
+  Lemma Rdiv_pos_den_0 x y (div_pos : 0 < x/y) : ¬ y = 0.
+  Proof.
+    intro d0. rewrite d0 in div_pos. rewrite Rdiv_0_r in div_pos. lra.
+  Qed.
+
+  (** Numeric Above Threshold **)
+
+  Definition num_above_threshold : val :=
+    λ:"num" "den" "T",
+      let: "T'" := Laplace (#4*"num") (#9*"den") "T" #() in
+      λ:"db" "qi",
+        let: "vi" := Laplace (#2*"num") (#9*"den") ("qi" "db") #() in
+        if: "T'" ≤ "vi" then SOME (Laplace (#1*"num") (#9*"den") ("qi" "db") #()) else NONEV.
+
+  (* The spec that nAT satisfies after initialising T'. *)
+
+  Definition nAT_spec (c : R) (AUTH : iProp Σ) (f f' : val) : iProp Σ :=
+    □ ∀ `(dDB : Distance DB) (db db' : DB) (_ : dDB db db' <= c) (q : val) (K0 : list ectx_item),
+      □ wp_sensitive q 1 dDB dZ -∗
+      AUTH -∗
+      ⤇ fill K0 (f' (inject db') q) -∗
+      WP f (inject db) q
+        {{ v, ∃ (b : option Z), ⌜v = inject b⌝ ∗ ⤇ fill K0 (inject b) ∗
+                                       (⌜v = NONEV⌝ -∗ AUTH) }}.
+
+  (* We prove the (non-pw) spec for onAT from hoare_couple_laplace_choice. *)
+  Lemma num_above_threshold_online_nAT_spec (num den T : Z) (εpos : 0 < IZR num / IZR den) K :
+    ↯m (1 * (IZR num / IZR den)) -∗
+    ⤇ fill K ((Val num_above_threshold) #num #den #T)
+    -∗ WP (Val num_above_threshold) #num #den #T
+         {{ f, ∃ (f' : val) (AUTH : iProp Σ),
+               ⤇ fill K (Val f') ∗ AUTH ∗ nAT_spec 1 AUTH f f' }}.
+  Proof with (tp_pures ; wp_pures).
+    iIntros "ε rhs". rewrite /num_above_threshold...
+    tp_bind (Laplace _ _ _ _). wp_bind (Laplace _ _ _ _).
+    set (ε := (IZR num / IZR den)). replace ε with ((1*ε) / 9 + (4*ε) / 9 + (4*ε) / 9) by real_solver.
+    fold ε in εpos. repeat rewrite Rmult_plus_distr_l.
+    iDestruct (ecm_split with "ε") as "[ε ε3]". 1,2: real_solver.
+    iDestruct (ecm_split with "ε") as "[ε2 ε1]". 1,2: real_solver.
+    iApply (hoare_couple_laplace _ _ 1%Z 1%Z with "[$rhs ε1]") => //; first by lia.
+    { 1: repeat rewrite mult_IZR ; repeat apply Rdiv_pos_pos.
+      2: real_solver.
+     rewrite -Rmult_div_assoc. apply Rmult_lt_0_compat; first lra. subst ε. apply εpos. }
+    { iApply ecm_eq. 2: iFrame. subst ε. replace (IZR (4 * num)) with (4 * IZR num).
+      2: qify_r ; zify_q ; lia.
+      replace (4 * (IZR num / IZR den) / 9) with (4 * IZR num / IZR (9 * den)).
+      1: reflexivity.
+      rewrite Rmult_div_assoc.
+      rewrite -Rdiv_mult_distr.
+      rewrite mult_IZR.
+      replace (9 * IZR den) with (IZR den * 9).
+      1: reflexivity.
+      by rewrite Rmult_comm. }
+    iIntros (T') "!> rhs" => /=...
+    iModIntro. iExists _. iFrame "rhs".
+    iExists (↯m (ε / 9) ∗ ↯m (4 * ε / 9))%I. repeat rewrite Rmult_1_l. iFrame "ε2 ε3". clear K.
+    rewrite /nAT_spec.
+    iModIntro. iIntros (?????? K) "#q_sens ε rhs"...
+    tp_bind (q _) ; wp_bind (q _).
+    iCombine "q_sens" as "q_sens'".
+    rewrite /wp_sensitive.
+    iSpecialize ("q_sens" $! _ _ db db' with "rhs").
+    Unshelve. 2: lra.
+    iApply (wp_strong_mono'' with "q_sens [ε]") => //.
+    iIntros (?) "(%vq_l & %vq_r & -> & rhs & %adj')" => /=...
+    assert (-1 <= vq_l - vq_r <= 1)%Z as [].
+    {
+      rewrite Rmult_1_l in adj'.
+      assert (dZ vq_l vq_r <= 1) as h by (etrans ; eauto).
+      revert h. rewrite /dZ/distance Rabs_Zabs.
+      apply Zabs_ind ; intros ? h; split.
+      all: pose proof (le_IZR _ _ h) ; lia.
+    }
+    tp_bind (Laplace _ _ _ _); wp_bind (Laplace _ _ _ _).
+    iDestruct "ε" as "(ε1 & ε2)".
+    iApply (hoare_couple_laplace_choice vq_l (vq_r) T' with "[$]") => //.
+    1: apply Zabs_ind ; lia.
+    1: { repeat rewrite mult_IZR ; apply Rdiv_pos_pos. 2: real_solver. subst ε. lra. }
+    { subst ε. rewrite -Rmult_div_assoc. rewrite -Rdiv_mult_distr.
+      repeat rewrite Rmult_div_assoc. repeat rewrite mult_IZR. repeat rewrite Rdiv_mult_distr.
+      rewrite -Rmult_assoc. replace (2 * 2) with 4. 1, 2: lra. }
+    iIntros "%z !> (%z' & rhs & hh)".
+    iDestruct "hh" as "[%h_above | [%h_below ε]]".
+    - (* above the threshold *)
+      simpl... case_bool_decide as Hf1; case_bool_decide as Hf2.
+      2, 3, 4: lia.
+      wp_if_true; tp_if_true...
+      tp_bind (q _); wp_bind (q _).
+      iSpecialize ("q_sens'" $! _ _ db db' with "rhs").
+      Unshelve. 2: lra.
+      (* We apply q_sens a second time that is why it is now persistent in the spec *)
+      iApply (wp_strong_mono'' with "q_sens' [ε1]") => //.
+      iIntros (?) "(%vq_l' & %vq_r' & -> & rhs & %adj'')" => /=...
+      tp_bind (Laplace _ _ _ _); wp_bind (Laplace _ _ _ _).
+      iApply (hoare_couple_laplace _ _ 0 1 with "[$rhs ε1]") => //.
+      + rewrite Z.add_comm. rewrite -Zplus_0_r_reverse.
+        apply le_IZR. rewrite abs_IZR.
+        lra.
+      + subst ε. repeat rewrite mult_IZR. rewrite Rdiv_mult_distr. lra.
+      + iApply ecm_eq. 2: iFrame. subst ε. repeat rewrite mult_IZR. rewrite Rdiv_mult_distr. lra.
+      + iIntros (v) "!> rhs" => /=...
+        iModIntro.
+        iExists (Some v).
+        rewrite -Zplus_0_r_reverse.
+        iFrame.
+        iSplitL.
+        1: by iPureIntro.
+        iIntros "%Hfalse".
+        inversion Hfalse.
+    - (* under the threshold *)
+      simpl... destruct h_below. case_bool_decide as Hf1; case_bool_decide as Hf2.
+      1, 2, 3: lia.
+      tp_if_false; wp_if_false.
+      iModIntro.
+      iExists None.
+      iFrame.
+      iSplitR; first by iPureIntro.
+      by iIntros (Hfin) => //.
+  Qed.
+
+  (* ALT def to use tiple *)
+  Definition nAT_spec_triple (c : R) (AUTH : iProp Σ) (f f' : val) : iProp Σ :=
+    □ ∀ `(dDB : Distance DB) (db db' : DB) (_ : dDB db db' <= c) (q : val) (K0 : list ectx_item),
+      {{{ □ wp_sensitive q 1 dDB dZ ∗ AUTH ∗ ⤇ fill K0 (f' (inject db') q) }}}
+      f (inject db) q
+      {{{ v, RET v; ∃ (b : option Z), ⌜v = inject b⌝ ∗ ⤇ fill K0 (inject b) ∗
+                                             (⌜v = NONEV⌝ -∗ AUTH) }}}.
+  (*Lemma num_above_threshold_online_nAT_spec_triple (num den T : Z) (εpos : 0 < IZR num / IZR den) K :
+    {{{ ↯m (1 * (IZR num / IZR den)) ∗ ⤇ fill K ((Val num_above_threshold) #num #den #T) }}}
+      (Val num_above_threshold) #num #den #T
+    {{{ f, RET f; ∃ (f' : val) (AUTH : iProp Σ),
+               ⤇ fill K (Val f') ∗ AUTH ∗ nAT_spec 1 AUTH f f' }}}.
+  Proof.
+    iIntros (Φ) "[Hε Hres] HΦ".
+
+    iApply (wp_strong_mono'' with "HΦ").*)
+
+
+  (** Numeric Sparse Vector **)
+
+  Definition onSVT : val :=
+    λ:"num" "den" "T" "N",
+      let: "count" := ref ("N" - #1) in
+      let: "nAT" := ref (num_above_threshold "num" "den" "T") in
+      λ:"db" "qi",
+        let: "bq" := !"nAT" "db" "qi" in
+        (if: !"count" <= #0 `or` "bq" = NONEV then
+           #()
+         else ("nAT" <- (num_above_threshold "num" "den" "T") ;;
+            "count" <- !"count" - #1)) ;;
+        "bq".
+
+  Definition nSVT_spec (f f' : val) (inSVT : nat → iProp Σ) : iProp Σ :=
+    (∀ `(dDB : Distance DB) (db db' : DB) (adj : dDB db db' <= 1) (q : val) K,
+          □ wp_sensitive (Val q) 1 dDB dZ -∗
+          ⤇ fill K (Val f' (inject db') q) -∗
+          ∀ n, inSVT (S n) -∗
+               WP Val f (inject db) q
+               {{v, ⤇ fill K (Val v) ∗ ∃ (b : option Z), ⌜v = inject b⌝ ∗
+                              inSVT (if bool_decide(v = NONEV) then S n
+                                                               else n) }}
+      ).
+
+  Lemma nSVT_online_diffpriv (num den T : Z) (N : nat) (Npos : (0 < N)%nat) K :
+    let ε := IZR num / IZR den in
+    ∀ (εpos : 0 < ε),
+      ↯m (N * ε) -∗
+      ⤇ fill K (onSVT #num #den #T #N) -∗
+      WP onSVT #num #den #T #N
+        {{ f,
+             ∃ (f' : val) (inSVT : nat → iProp Σ),
+              ⤇ fill K f' ∗
+              inSVT N ∗
+             □ nSVT_spec f f' inSVT }}.
+
+  Proof with (tp_pures ; wp_pures).
+    (* make sure we have at least enough credit to initialise nAT once *)
+    destruct N as [|N'] ; [lia|] ; clear Npos.
+    iIntros (??) "SNε rhs". rewrite /onSVT...
+    tp_alloc as count_r "count_r"; wp_alloc count_l as "count_l"...
+    tp_bind (num_above_threshold _ _ _) ; wp_bind (num_above_threshold _ _ _).
+    assert (INR (N'+1)%nat ≠ 0).
+    { replace 0 with (INR 0) => //. intros ?%INR_eq. lia. }
+    replace (S N' * ε) with (ε + N' * ε).
+    2:{ replace (S N') with (N'+1)%nat by lia. replace (INR (N'+1)) with (N' + 1) by real_solver. lra. }
+    iDestruct (ecm_split with "SNε") as "[ε Nε]". 1,2: real_solver.
+    opose proof (num_above_threshold_online_nAT_spec num den T _) as nAT; first done.
+    iPoseProof (nAT with "[ε] [rhs]") as "nAT" => // ; clear nAT. 1: by rewrite Rmult_1_l.
+    iApply (wp_strong_mono'' with "nAT").
+    replace (S N') with (N'+1)%nat by lia.
+    iIntros "%f (%f' & %AUTH & rhs & auth & nAT) /=".
+    tp_alloc as ref_f' "ref_f'"; wp_alloc ref_f as "ref_f"...
+    iModIntro. iExists _. iFrame "rhs".
+    set (inSVT := (λ n : nat,
+                    if Nat.ltb 0%nat n then
+                      let n' := (n-1)%nat in
+                      count_l ↦ #n' ∗ count_r ↦ₛ #n' ∗
+                      ↯m (n' * ε) ∗ ∃ token f f',
+                          token ∗ ref_f ↦ f ∗ ref_f' ↦ₛ f' ∗ nAT_spec 1 token f f'
+                    else emp
+                 )%I). iExists inSVT.
+    iSplitL.
+    { rewrite /inSVT /=. destruct (0 <? N'+1)%nat => //.
+      replace ((N'+1)%nat-1)%Z with (Z.of_nat N') by lia.
+      replace (N'+1-1)%nat with N' by lia. iFrame. }
+    clear f f'.
+    rewrite /nSVT_spec.
+    iIntros "!>" (???????) "#q_sens rhs %n (count_l & count_r & nε & (%TOKEN & %f & %f' & auth & ref_f & ref_f' & #nAT))"...
+    tp_load ; wp_load.
+    tp_bind (f' _ _); wp_bind (f _ _).
+    iCombine "nAT" as "nAT_cpy".
+    iSpecialize ("nAT" $! _ _ _ _ adj) as #.
+    iSpecialize ("nAT" with "q_sens auth rhs").
+    iApply (wp_strong_mono'' with "nAT").
+    iIntros "%vq (%b & -> & rhs & maybe_auth)".
+    iSimpl in "rhs"...
+    case_bool_decide as H1.
+    - (* Case where the returned value is None *)
+      destruct b; first inversion H1.
+      simpl... rewrite /= !Nat.sub_0_r. simplify_eq.
+      tp_load ; wp_load...
+      iSpecialize ("maybe_auth" $! eq_refl).
+      destruct n as [|n']...
+      { rewrite /inSVT. iFrame.
+        iExists None. iSplitR => //. simpl. iFrame.
+        iExists TOKEN. iFrame. done.
+      }
+      iModIntro.
+      iFrame. iExists None ; iSplitR => //.
+      iSimpl. iFrame. iExists TOKEN. iFrame. done.
+
+    - (* Case where the returned value is Some(v) *)
+      tp_load ; wp_load...
+      rewrite /= !Nat.sub_0_r.
+      destruct b; last done.
+      destruct n as [|n']...
+      { (* Case where n <= 0 *)
+        rewrite /inSVT. iFrame. iExists (Some z). iModIntro. iPureIntro. done.
+      }
+      (* Case where n>0 *)
+      replace (S n' * ε) with (ε + n' * ε).
+      2:{ replace (S n') with (n'+1)%nat by lia. replace (INR (n'+1)) with (n' + 1) by real_solver. lra. }
+      iDestruct (ecm_split with "nε") as "[ε n'ε]". 1,2: real_solver.
+      simpl. simplify_eq...
+      tp_bind (num_above_threshold _ _ _) ; wp_bind (num_above_threshold _ _ _).
+      opose proof (num_above_threshold_online_nAT_spec num den T _) as nAT_pw; first done.
+      iPoseProof (nAT_pw with "[ε] [rhs]") as "nAT_pw" => // ; clear nAT_pw; first by rewrite Rmult_1_l.
+      iApply (wp_strong_mono'' with "nAT_pw [-]").
+      iIntros "%g (%g' & %AUTH' & rhs & auth & nAT') /=".
+      tp_store ; wp_store... tp_load... tp_store ; wp_load... wp_store.
+      iFrame. iExists (Some z). iSplitR; first done.
+      rewrite /inSVT.
+      case_bool_decide as H1'; first done.
+      simpl.
+      replace ((n' - 0)%nat) with n' by lia.
+      iFrame.
+      replace (Z.of_nat (S n') - 1)%Z with (Z.of_nat n') by lia. iFrame. done.
+  Qed.
+
+  Definition nSVT_stream : val :=
+    λ:"num" "den" "T" "N" "stream_qs" "db",
+      let: "f" := onSVT "num" "den" "T" "N" in
+      (rec: "nSVT" "i" "bs" :=
+         if: "i" = "N" then "bs" else
+           match: "stream_qs" "bs" with
+           | NONE => "bs"
+           | SOME "q" =>
+               let: "b" := "f" "db" "q" in
+               "nSVT" (if: "b" = NONEV then "i" else ("i" + #1)) (list_cons "b" "bs")
+           end) #0 list_nil.
+
+  #[local] Definition nSVT_stream_body (N : nat) (stream_qs : val) {DB} {_ : Inject DB val} (db : DB) (f : val) := (rec: "nSVT" "i" "bs" :=
+        if: "i" = #N then "bs"
+        else match: stream_qs "bs" with
+               InjL <> => "bs"
+             | InjR "q" =>
+               let: "b" := f (Val (inject db)) "q" in
+               "nSVT" (if: "b" = NONEV then "i" else ("i" + #1)) (list_cons "b" "bs")
+             end)%V.
+
+
+  Lemma nSVT_stream_diffpriv (num den T : Z) (N : nat) (Npos : (0 < N)%nat) (stream_qs : val) `(dDB : Distance DB) :
+    let ε := IZR num / IZR den in
+    ∀ (εpos : 0 < ε),
+      □ (∀ K (bs : val),
+            ⤇ fill K (stream_qs bs) -∗
+            WP stream_qs bs
+              {{ qopt, ⤇ fill K (Val qopt) ∗
+                       (⌜qopt = NONEV⌝ ∨ ∃ q : val, ⌜qopt = SOMEV q⌝ ∗ □ wp_sensitive q 1 dDB dZ) }}) -∗
+      ∀ (db db' : DB) (adj : dDB db db' <= 1) K,
+      ↯m (N * ε) -∗
+      ⤇ fill K (nSVT_stream #num #den #T #N stream_qs (Val (inject db'))) -∗
+      WP nSVT_stream #num #den #T #N stream_qs (Val (inject db))
+        {{ v, ⤇ fill K (Val v) }}.
+  Proof with (tp_pures ; wp_pures).
+    iIntros (ε εpos) "#sens % % % % Nε rhs". rewrite /nSVT_stream...
+    tp_bind (onSVT _ _ _ _) ; wp_bind (onSVT _ _ _ _).
+    iPoseProof (nSVT_online_diffpriv with "Nε rhs") as "spec" => //.
+    iApply (wp_strong_mono'' with "spec"). iIntros "%f (%f' & % & rhs & inSVT & spec) /=".
+    do 4 tp_pure. do 4 wp_pure. rewrite -!/(nSVT_stream_body _ _ _ _).
+    set (i := 0%Z). set (N' := N). rewrite {1 3}/N'.
+    assert (0 <= i)%Z as ipos by lia. assert (N' + i = N)%Z as hi by lia.
+    set (bs := InjLV #()). rewrite {1}/bs. generalize i N' bs hi ipos. clear i N' hi ipos bs.
+    intros. iRevert (i N' bs hi ipos) "rhs inSVT spec". iLöb as "IH". iIntros (i N' bs hi ipos) "rhs inSVT #spec".
+    rewrite {3 4}/nSVT_stream_body...
+    case_bool_decide... 1: done.
+    tp_bind (stream_qs _) ; wp_bind (stream_qs _).
+    iPoseProof ("sens" $! _ bs with "rhs") as "sens_bs".
+    iApply (wp_strong_mono'' with "sens_bs").
+    iIntros "%qopt (rhs & [->|(%q & -> & #sens_q)]) /="... 1: done.
+    tp_bind (f' _ _) ; wp_bind (f _ _).
+    iCombine "spec" as "spec_i".
+    assert (not (i = N)). 1: intros h ; subst ; auto.
+    assert (∃ N'', N' = S N'') as [? ->]. { destruct N'. 1: lia. eauto. }
+    iEval (rewrite /nSVT_spec) in "spec_i".
+    iSpecialize ("spec_i" $! _ _ db db' adj with "sens_q rhs inSVT") => //.
+    iApply (wp_strong_mono'' with "spec_i").
+    rewrite -!/(nSVT_stream_body _ _ _ _).
+    iIntros "% (rhs & %b & -> & inSVT) /="...
+    destruct b. rewrite /list_cons...
+    - iApply ("IH" with "[] [] rhs inSVT"). 3: done. 1,2: iPureIntro. 2: lia. lia.
+    - iApply ("IH" with "[] [] rhs [inSVT]"). 3,4: done. 1,2: iPureIntro. 2: lia. lia.
+  Qed.
+
+End nsvt.
diff --git a/theories/diffpriv/examples/private_multiplicative_weights.v b/theories/diffpriv/examples/private_multiplicative_weights.v
new file mode 100644
index 000000000..bfcb72e22
--- /dev/null
+++ b/theories/diffpriv/examples/private_multiplicative_weights.v
@@ -0,0 +1,674 @@
+From iris.base_logic Require Export na_invariants.
+From clutch.common Require Import inject.
+From clutch.prelude Require Import tactics.
+From clutch.prob Require Import differential_privacy.
+From clutch.diffpriv Require Import adequacy diffpriv proofmode.
+From clutch.prob_lang.gwp Require Import gen_weakestpre arith list.
+From clutch.diffpriv.examples Require Import list numeric_sparse_vector_technique.
+
+Section pmw.
+  Context `{!diffprivGS Σ}.
+
+  #[local] Open Scope R.
+
+
+  (* For the proof we need to adapt the algo from the book. *)
+  (* Indeed, in order to get result on the call to `f`, *)
+  (* the numeric sparse vector technique, we need to call *)
+  (* it again for e2 only when we know that e1 is None. *)
+  (* Otherwise, we can not state no result on e2 since if *)
+  (* e1 returned a value then we would not have the right inSVT hypothesis. *)
+  (* Knowing that even if e1 and e2 are values, then we will *)
+  (* not use e2. Hence we call it only when necessary. *)
+
+  (* We are giving to the oPMW technique a lot of functions in *)
+  (* parameters. We also make a lot of assumptions about those *)
+  (* functions in the specification. *)
+  (* That is why this is only a partial implementation of the *)
+  (* private multiplicative weight technique. *)
+  (* Moreover I'm not convinced about the specification. *)
+  (* Our functions should "here" take any val in args *)
+  (* and return a val... this seems like a very strong hypothese ? *)
+
+  (** Query implementation *)
+  (* We assume that there exists an indexation on the elements of the domain χ. *)
+  (* Hence to represent a database, we will use an array. *)
+
+  Definition c_query : val :=
+    λ: "q" "db",
+      Snd
+        (if: list_length "db" <= list_length "q"
+        then
+          list_fold (λ: "acc" "x",
+              ((Fst "acc")+#1, (Snd "acc") + (if: (list_nth "q" (Fst "acc")) then "x" else #0))) (#0, #0) "db"
+        else
+          list_fold (λ: "acc" "x",
+              ((Fst "acc")+#1, (Snd "acc") + (if: "x" then list_nth "db" (Fst "acc") else #0))) (#0, #0) "db").
+
+  Lemma c_query_det :
+    ∀ K (vq vdb: val) (q : list bool) (db : list nat),
+      ⌜ is_list q vq ⌝ -∗ ⌜ is_list db vdb ⌝ -∗
+      ⤇ fill K (c_query vq vdb) -∗
+      WP c_query vq vdb {{ v, ⤇ fill K (Val v) ∗ ∃ (n : nat), ⌜ v = #n ⌝ }}.
+   Proof with (wp_pures; tp_pures).
+     iIntros (K vq vdb q db) "%H1  %H2 hrs".
+     rewrite /c_query...
+     (* proove that iteri has the same comportement *)
+     (* iApply (wp_list_iteri db (λ: "i" "x", if: list_nth vq "i" then #rest <- "x" + ! #rest else #()) *)
+     (*           vdb _ (λ i x, ∃ (n : nat), resw ↦ #n ∗ rest ↦ₛ #n)%I (λ i x, ∃ (n : nat), resw ↦ #n ∗ rest ↦ₛ #n)%I). *)
+     (* Doable *)
+     Admitted.
+
+  Lemma c_query_1_sens :
+    ∀ (vq : val) (q : list bool),
+      ⌜ is_list q vq ⌝ -∗ wp_sensitive (c_query vq) 1 (dlist nat) (dZ).
+  Proof with (tp_pures; wp_pures).
+    iIntros.
+    rewrite /wp_sensitive.
+    iIntros (_ K x x') "rhs".
+    rewrite /c_query.
+    wp_lam; tp_lam...
+    (* issue, in wp_sensitive, x and x' are list nat not especially lists of the same size...*)
+    (* need to show that for each elements of the lists if they are distant of n then the queue of the list is distant of d - n *)
+    (* More Difficult *)
+    Admitted.
+
+  Definition sum_db : val :=
+    λ: "db",
+      list_fold (λ: "acc" "x", "acc" + "x") #0 "db".
+
+  Definition dN : val :=
+    λ: "a" "b",
+      if: "a" < "b"
+      then "b" - "a"
+      else "a" - "b".
+
+  Definition normalize : val :=
+    (* TODO check, there is certainely a modulo function that exists *)
+    λ: "db" "size",
+      let: "s" := sum_db "db" in
+      let: "ln" := list_map (λ: "x", ("size" * "x") `quot` "s") "db" in
+      let: "s'" := sum_db "ln" in
+      let: "lln" := list_length "ln" in
+      list_mapi (λ: "i" "x", (if: "i" < ("size" - "s'" - #1) `rem` "lln" then #1 else #0) + (("size" - "s'") `quot` "lln") + "x") "ln".
+
+  Definition get_unif : val :=
+    λ: "size_dom" "size_db",
+      normalize (list_init "size_dom" (λ: "i", #1)) "size_db".
+
+  Definition mw_upd : val :=
+   λ: "exp" "ηnum" "ηden" "size" "db" "q" "v",
+     if: c_query "q" "db" < "v"
+     then normalize (list_mapi (λ: "i" "x", "exp" (-"eta" * (if: list_nth "q" "i" then #0 else #1)) * "x") "db") "size"
+     else normalize (list_mapi (λ: "i" "x", "exp" (-"eta" * (if: list_nth "q" "i" then #1 else #0)) * "x") "db") "size".
+
+  Definition det_int_fun (f : val) : Prop :=
+    ∀ K (n : nat),
+      ⤇ fill K (f #n) -∗
+      WP f #n {{v, ⤇ fill K (Val v) ∗ ∃ (n' : Z), ⌜ v = #n ⌝ }}.
+
+  Definition det_q (q : val) : Prop :=
+    ∀ K (vdb : val) (db : list nat),
+      ⌜ is_list db vdb ⌝ -∗
+      ⤇ fill K (q vdb) -∗
+      WP q vdb {{v, ⤇ fill K (Val v) ∗ ∃ r : Z, ⌜ v = #r ⌝ }}.
+
+  Definition spec_upd (upd : val) : Prop :=
+    (∀ K (vdb vq : val) (l : Z) (db : list nat) (q : list bool),
+           (* The update returns a database of the right size for the "right" inputs *)
+         ⌜is_list db vdb⌝ ∗ ⌜is_list q vq⌝ ∗
+         ⤇ fill K ((upd vdb) vq #l) -∗
+         WP upd vdb vq #l
+         {{ v, ⤇ fill K (Val v) ∗ ∃ db' : list nat, ⌜is_list db' v⌝ }}).
+
+  Definition spec_stream (stream_q : val) (size_dom : nat) : Prop :=
+    (∀ K (bs : val),
+           (* stream_q returns a boolean query of the right size *)
+         ⤇ fill K (stream_q bs) -∗
+         WP stream_q bs
+         {{ qopt, ⤇ fill K (Val qopt) ∗
+                    (⌜qopt = NONEV⌝ ∨ ∃ (vq : val) (q : list bool),
+                        ⌜is_list q vq⌝ ∗ ⌜length q = size_dom⌝ ∗ ⌜qopt = SOMEV vq⌝)}}).
+
+  Definition spec_f (f : val) : Prop :=
+     (∀ K (vq vdb: val) (db : list nat) (q : list bool),
+            (* f returns a 1sens deterministic query for the "right" inputs *)
+          ⌜is_list db vdb⌝ ∗ ⌜is_list q vq⌝ ∗
+          ⤇ fill K (f vq vdb) -∗
+          WP f vq vdb
+          {{ v, ⤇ fill K (Val v) ∗ □ wp_sensitive v 1 (dlist nat) dnat ∗ ⌜ det_q v ⌝ }}).
+
+  Lemma upd_deterministic :
+    (* If we have the good arguments then we get a distribution of the same size *)
+    ∀ K (vdb vq : val) (db : list nat) (q : list bool) (l size ηnum ηden : nat) (exp : val),
+          ⌜ det_int_fun exp ⌝ -∗
+          ⌜ is_list q vq ⌝ ∗ ⌜ is_list db vdb ⌝ -∗
+          ⤇ fill K (mw_upd exp #ηnum #ηden #size vdb vq #l) -∗
+          WP mw_upd exp #ηnum #ηden #size vdb vq #l
+          {{ v, ⤇ fill K (Val v) ∗ ∃ (db' : list nat), ⌜ is_list db' v ⌝ }}.
+  Proof with (tp_pures; wp_pures).
+    iIntros (K vdb vq db q l size ηnum ηden exp) "%Hexp (%H1 & %H2) hrs".
+    rewrite /mw_upd...
+    wp_bind (c_query _ _); tp_bind (c_query _ _).
+    iPoseProof (c_query_det _ vq vdb q db $! _ _ with "hrs") as "Hcqd".
+    Unshelve.
+    2, 3: done.
+    iApply (wp_strong_mono'' with "Hcqd").
+    iIntros (vr) "(rhs & %r & ->)".
+    simpl.
+  Admitted.
+
+  Lemma upd_partial :
+    ∀ K (exp : val) (ηnum ηden size_db : nat),
+      ⤇ fill K (mw_upd exp #ηnum #ηden #size_db) -∗
+      WP mw_upd exp #ηnum #ηden #size_db {{ f,
+          ⤇ fill K (Val f) ∗
+          □ (∀ K' (vdb vq : val) (v : Z) (db : list nat) (q : list bool),
+            ⌜ is_list db vdb ⌝ -∗
+            ⌜ is_list q vq ⌝ -∗
+            ⤇ fill K' (f vdb vq #v) -∗
+            WP f vdb vq #v {{ vdb',
+                ⤇ fill K' (Val vdb') ∗ ∃ (db' : list nat), ⌜is_list db' vdb'⌝
+            }})
+      }}.
+  Proof with (tp_pures; wp_pures).
+    iIntros (K exp ηnum ηden size_db) "rhs".
+    rewrite /mw_upd.
+  Admitted.
+
+  Lemma get_unif_det :
+    ∀ K (size_db size_dom : nat),
+      ⤇ fill K (get_unif #size_db #size_dom) -∗
+      WP get_unif #size_db #size_dom {{ vu,
+           ⤇ fill K (Val vu) ∗ ∃ (u : list nat), ⌜ is_list u vu ⌝
+      }}.
+  Proof.
+  Admitted.
+  (** General implementation *)
+  Definition oPMW_large : val :=
+    λ: "x" "stream_q" "num" "den" "c" "t" "unif" "upd" "f1" "f2",
+      let: "f" := (onSVT "num" "den" "t" "c") in
+      (rec: "aux" "i" "bs" "distrib" :=
+         match: "stream_q" "bs" with
+         | NONE => "bs"  (* No more queries *)
+         | SOME "q" =>
+             if: "i" = "c" then (* We made too many updates *)
+               "aux" "i" (list_cons (c_query "q" "distrib") "bs") "distrib"
+             else (
+               match: "f" "x" ("f1" "q" "distrib") with
+               | NONE =>
+                   match: "f" "x" ("f2" "q" "distrib") with
+                   | NONE => "aux" "i" (list_cons (c_query "q" "distrib") "bs") "distrib"
+                   (* The answer is under the threshold *)
+                   | SOME "v" => "aux" ("i" + #1) (list_cons "v" "bs") ("upd" "distrib" "q" (c_query "q" "distrib" + "v"))
+                   end
+               | SOME "v" => "aux" ("i" + #1) (list_cons "v" "bs") ("upd" "distrib" "q" (c_query "q" "distrib" - "v"))
+               end)
+         end) #0 list_nil "unif".
+
+  Definition oPMW : val :=
+    λ: "εnum" "εden" "αnum" "αden" "βnum" "βden" "ηnum" "ηden" "db" "size_db" "size_dom" "stream_q" "nb_q" "fc" "ft" "exp",
+      let: "c" := "fc" "size_dom" "αden" "αnum" in
+      let: "t" := "ft" "εnum" "εden" "βnum" "βden" "c" "nb_q" "size_db" in
+      let: "f1" := (λ: "q" "distrib" "x", c_query "q" "x" - c_query "q" "distrib") in
+      let: "f2" := (λ: "q" "distrib" "x", c_query "q" "distrib" - c_query "q" "x") in
+      let: "unif" := get_unif "size_dom" "size_db" in
+      let: "upd" := mw_upd "exp" "ηnum" "ηden" "size_db" in
+      oPMW_large "db" "stream_q" "εnum" ("c"*"εden") "c" "t" "unif" "upd" "f1" "f2".
+
+  (* Lemma f1_deterministic `(dDB : DistanceDB): *)
+  (*   ⊢ □ (∀ K (distrib q : DB), (* we get back a 1sens query *) *)
+  (*         (wp_sensitive q 1 dDB dZ) -∗ (* we need the original query to be 1 sensitive *) *)
+  (*         ⤇ fill K ((λ: "x" "size", c_query "x" q "size" - c_query distrib q "size") q distrib) -∗ *)
+  (*         WP (λ: "x" "size", c_query "x" q "size" - c_query distrib q "size") q distrib *)
+  (*         {{ v, ⤇ fill K (Val v) ∗ □ wp_sensitive v 1 dDB dZ }}). *)
+
+  #[local] Definition pMW_body (c : nat) (stream_q : val) {_ : Inject (list nat) val} (db : list nat) (f : val) (upd f1 f2: val) :=
+       (rec: "aux" "i" "bs" "distrib" :=
+                  match: stream_q "bs" with
+                    InjL <> => "bs"
+                  | InjR "q" =>
+                    if: "i" = #c then "aux" "i" (list_cons (c_query "q" "distrib") "bs") "distrib"
+                    else match: f (list.inject_list db) (f1 "q" "distrib") with
+                           InjL <> =>
+                             match: f (list.inject_list db) (f2 "q" "distrib") with
+                               InjL <> => "aux" "i" (list_cons (c_query "q" "distrib") "bs") "distrib"
+                             | InjR "v" => "aux" ("i" + #1) (list_cons "v" "bs") (upd "distrib" "q" (c_query "q" "distrib" + "v"))
+                             end
+                         | InjR "v" => "aux" ("i" + #1) (list_cons "v" "bs") (upd "distrib" "q" (c_query "q" "distrib" - "v"))
+                         end
+                  end)%V.
+
+  Lemma pMW_general_diffpriv (num den c t : nat) (stream_q : val) (upd f1 f2 vunif : val) (unif : list nat) :
+    let ε := IZR num / IZR den in
+    let size_dom := length unif in
+    ⌜ is_list unif vunif ⌝ -∗
+    ∀ (εpos : 0 < ε) (cpos : (0 < c)%nat) (tpos : (0 < t)%nat),
+      □ (∀ K (bs : val),
+            (* stream_q returns a boolean query of the right size *)
+          ⤇ fill K (stream_q bs) -∗
+          WP stream_q bs
+          {{ qopt, ⤇ fill K (Val qopt) ∗
+                     (⌜qopt = NONEV⌝ ∨ ∃ (vq : val) (q : list bool),
+                         ⌜is_list q vq⌝ ∗ ⌜qopt = SOMEV vq⌝)}}) -∗
+      □ (∀ K (vdb vq : val) (l : Z) (db : list nat) (q : list bool),
+            (* The update returns a database of the right size for the "right" inputs *)
+          ⌜is_list db vdb⌝ -∗ ⌜is_list q vq⌝ -∗
+          ⤇ fill K ((upd vdb) vq #l) -∗
+          WP upd vdb vq #l
+          {{ v, ⤇ fill K (Val v) ∗ ∃ db' : list nat, ⌜is_list db' v⌝ }}) -∗
+      □ (∀ K (vq vdb: val) (db : list nat) (q : list bool),
+            (* f returns a 1sens deterministic query for the "right" inputs *)
+          ⌜is_list db vdb⌝ -∗ ⌜is_list q vq⌝ -∗
+          ⤇ fill K (f1 vq vdb) -∗
+          WP f1 vq vdb
+          {{ v, ⤇ fill K (Val v) ∗ □ wp_sensitive v 1 (dlist nat) dZ ∗ ⌜ det_q v ⌝ }}) -∗
+      □ (∀ K (vq vdb: val) (db : list nat) (q : list bool),
+            (* f returns a 1sens deterministic query for the "right" inputs *)
+          ⌜is_list db vdb⌝ -∗ ⌜is_list q vq⌝ -∗
+          ⤇ fill K (f2 vq vdb) -∗
+          WP f2 vq vdb
+          {{ v, ⤇ fill K (Val v) ∗ □ wp_sensitive v 1 (dlist nat) dZ ∗ ⌜ det_q v ⌝ }}) -∗
+      ∀ (db db' : list nat) (adj : (dlist nat) db db' <= 1) K,
+      ↯m (c * ε) -∗
+      ⤇ fill K (oPMW_large (inject db') stream_q #num #den #c #t vunif upd f1 f2) -∗
+      WP oPMW_large (inject db) stream_q #num #den #c #t vunif upd f1 f2
+      {{ v, ⤇ fill K (Val v) }}.
+  Proof with (tp_pures; wp_pures).
+    iIntros (ε size_dom) "#Hvunif %εpos %cpos %tpos #Hstream #Hupdate #Hf1 #Hf2 % % % % ε rhs".
+    rewrite /oPMW_large...
+    tp_bind (onSVT _ _ _ _); wp_bind (onSVT _ _ _ _).
+    iPoseProof (nSVT_online_diffpriv with "ε rhs") as "spec" => //.
+    iApply (wp_strong_mono'' with "spec").
+    iIntros "%f (%f' & % & rhs & inSVT & spec) /=".
+    do 4 tp_pure; do 4 wp_pure.
+    rewrite -!/(pMW_body _ _ _ _ _ _ _).
+    set (vdistrib := vunif).
+    set (distrib := unif).
+    set (bs := InjLV #()). rewrite {1}/bs.
+    set (i := 0%Z). set (c' := c). rewrite {1 3}/c'.
+    assert (0 <= i)%Z as ipos by lia. assert (c' + i = c)%Z as hi by lia.
+    generalize i c' bs hi ipos vdistrib distrib. clear i c' bs hi ipos vdistrib distrib.
+    intros.
+    iRevert (i c' bs hi ipos vdistrib distrib) "Hvunif rhs inSVT spec".
+    iLöb as "IH".
+    iIntros (i c' bs hi ipos vdistrib distrib) "#Hvdistrib rhs inSVT #spec".
+    rewrite {3 4}/pMW_body...
+    wp_bind (stream_q _); tp_bind (stream_q _).
+    iPoseProof ("Hstream" $! _  with "rhs") as "H_bs".
+    iApply (wp_strong_mono'' with "H_bs").
+    iIntros "%qopt (rhs & [->|(%vq & %q & #hq & %Hvq)]) /="... 1: done.
+    subst qopt...
+    case_bool_decide...
+    - (* Case where we have already proceed all the allowed updates *)
+      do 2 rewrite -/(pMW_body _ _ _ _ _ _ _).
+      wp_bind (c_query _ _); tp_bind (c_query _ _).
+      iPoseProof (c_query_det _ vq vdistrib q distrib with "hq Hvdistrib") as "h_c_query".
+      iPoseProof ("h_c_query" with "rhs") as "h_c_query_det'".
+      iApply (wp_strong_mono'' with "h_c_query_det'").
+      iIntros (v) "[rhs _]"...
+      simpl.
+      rewrite /list_cons...
+      iApply ("IH" with "[] [] Hvdistrib rhs inSVT"). 3: done. 1,2: iPureIntro. 1,2: lia.
+    - (* We will deal with the nsvt *)
+      do 2 rewrite -/(pMW_body _ _ _ _ _ _ _).
+      wp_bind (f _ _); tp_bind (f' _ _).
+      wp_bind (f1 _ _); tp_bind (f1 _ _).
+      iSpecialize ("Hf1" $! _ vq vdistrib distrib q with "Hvdistrib hq").
+      iPoseProof ("Hf1" with "rhs") as "Hf1'".
+      iApply (wp_strong_mono'' with "Hf1'").
+      iIntros (q1) "[rhs [#sens_q1 #det_q1]]".
+      tp_bind (f' _ _).
+      iCombine "spec" as "spec_i".
+      iEval (rewrite /nSVT_spec) in "spec_i".
+      assert (not (i = c)). 1: intros h ; subst ; auto.
+      assert (∃ c'', c' = S c'') as [? ->]. { destruct c'. 1: lia. eauto. }
+      iSpecialize ("spec_i" $! _ _ db db' adj q1 _ with "sens_q1 rhs inSVT") => //.
+      iApply (wp_strong_mono'' with "spec_i").
+      iIntros "% (rhs & %e1 & -> & inSVT) /="...
+      destruct e1...
+      + (* e1 is a value (not none) *)
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iPoseProof (c_query_det _ vq vdistrib q distrib with "hq Hvdistrib") as "h_c_query".
+        iPoseProof ("h_c_query" with "rhs") as "h_c_query_det'".
+        iApply (wp_strong_mono'' with "h_c_query_det'").
+        iIntros (v) "[rhs [%nv %htv]]"...
+        simpl.
+        subst v.
+        wp_binop; tp_binop.
+        wp_bind (upd _ _ _ ); tp_bind (upd _ _ _ ).
+        iPoseProof ("Hupdate" $! _ vdistrib vq _ distrib q with "Hvdistrib hq rhs") as "Hupdate'".
+        iApply (wp_strong_mono'' with "Hupdate'").
+        iIntros (vdistrib') "(rhs & %distrib' & #Hvdistrib')".
+        simpl.
+        rewrite /list_cons...
+        iApply ("IH" with "[] [] Hvdistrib' rhs inSVT"). 3: done. 1,2: iPureIntro. 1,2: lia.
+      + (* e1 is none but we have inSVT (S x) *)
+        iSimpl in "inSVT"...
+        wp_bind (f _ _); tp_bind (f' _ _).
+        wp_bind (f2 _ _); tp_bind (f2 _ _).
+        iSpecialize ("Hf2" $! _ vq vdistrib distrib q with "Hvdistrib hq").
+        iPoseProof ("Hf2" with "rhs") as "Hf2'".
+        iApply (wp_strong_mono'' with "Hf2'").
+        iIntros (q2) "[rhs [#sens_q2 #det_q2]]".
+        tp_bind (f' _ _).
+        iCombine "spec" as "spec_i".
+        iEval (rewrite /nSVT_spec) in "spec_i".
+        iSpecialize ("spec_i" $! _ _ db db' adj q2 _ with "sens_q2 rhs inSVT") => //.
+        iApply (wp_strong_mono'' with "spec_i").
+        iIntros "% (rhs & %e2 & -> & inSVT) /=".
+        destruct e2...
+        -- (* e2 is a value (not none) *)
+          wp_bind (c_query _ _); tp_bind (c_query _ _).
+          iPoseProof (c_query_det _ vq vdistrib q distrib with "hq Hvdistrib") as "h_c_query".
+          iPoseProof ("h_c_query" with "rhs") as "h_c_query_det'".
+          iApply (wp_strong_mono'' with "h_c_query_det'").
+          iIntros (v) "[rhs [%nv %htv]]"...
+          simpl.
+          subst v.
+
+          wp_binop; tp_binop.
+          wp_bind (upd _ _ _ ); tp_bind (upd _ _ _ ).
+          iPoseProof ("Hupdate" $! _ vdistrib vq _ distrib q with "Hvdistrib hq rhs") as "Hupdate'".
+          iApply (wp_strong_mono'' with "Hupdate'").
+          iIntros (vdistrib') "(rhs & %distrib' & #Hvdistrib')".
+          simpl.
+          rewrite /list_cons...
+          iApply ("IH" with "[] [] Hvdistrib' rhs inSVT"). 3: done. 1,2: iPureIntro. 1,2: lia.
+        -- (* both answers are under the threshold *)
+          wp_bind (c_query _ _); tp_bind (c_query _ _).
+          iPoseProof (c_query_det _ vq vdistrib q distrib with "hq Hvdistrib") as "h_c_query".
+          iPoseProof ("h_c_query" with "rhs") as "h_c_query_det'".
+          iApply (wp_strong_mono'' with "h_c_query_det'").
+          iIntros (v) "[rhs [%nv %htv]]"...
+          simpl.
+          subst v.
+          rewrite /list_cons...
+          iApply ("IH" with "[] [] Hvdistrib rhs inSVT"). 3: done. 1,2: iPureIntro. 1,2: lia.
+  Qed.
+
+  Lemma pMW_diffpriv (εnum εden αnum αden βnum βden ηnum ηden size_db size_dom nb_q : nat) (stream_q fc ft exp : val) :
+    let ε := IZR εnum / IZR εden in
+    ∀ (εpos : 0 < ε),
+      □ (∀ K (bs : val),
+            (* stream_q returns a boolean query of the right size *)
+          ⤇ fill K (stream_q bs) -∗
+          WP stream_q bs
+          {{ qopt, ⤇ fill K (Val qopt) ∗
+                     (⌜qopt = NONEV⌝ ∨ ∃ (vq : val) (q : list bool),
+                         ⌜is_list q vq⌝ ∗ ⌜qopt = SOMEV vq⌝)}}) -∗
+      □ (∀ K (a1 a2 a3 : nat),
+        ⤇ fill K (fc #a1 #a2 #a3) -∗
+        WP fc #a1 #a2 #a3 {{ v, ⤇ fill K (Val v) ∗ ∃ (n : nat ), ⌜ v = #n ⌝ ∗ ⌜ 0 < n ⌝ }}) -∗
+      □ (∀ K (a1 a2 a3 a4 a5 a6 a7 : nat),
+        ⤇ fill K (ft #a1 #a2 #a3 #a4 #a5 #a6 #a7) -∗
+        WP ft #a1 #a2 #a3 #a4 #a5 #a6 #a7 {{ v, ⤇ fill K (Val v) ∗ ∃ (n : nat ), ⌜ v = #n ⌝ ∗ ⌜ 0 < n ⌝ }}) -∗
+      (* hypothesis on the maths functions *)
+      □ (∀ K (a : nat),
+        ⤇ fill K (exp #a) -∗
+        WP exp #a {{ v, ⤇ fill K (Val v) ∗ ∃ (n : nat), ⌜ v = #n ⌝ }}) -∗
+      ∀ K (db db' : list nat) (adj : (dlist nat) db db' <= 1),
+        ↯m (ε) -∗
+        ⤇ fill K (oPMW #εnum #εden #αnum #αden #βnum #βden #ηnum #ηden (Val (inject db')) #size_db #size_dom stream_q #nb_q fc ft exp) -∗
+        WP oPMW #εnum #εden #αnum #αden #βnum #βden #ηnum #ηden (Val (inject db)) #size_db #size_dom stream_q #nb_q fc ft exp
+        {{ v, ⤇ fill K (Val v) }}.
+  Proof with (wp_pures; tp_pures).
+    iIntros (ε εpos) "#Hstream #Hfc #Hft #Hexp".
+    iIntros (K db db' ddb) "Hε rhs".
+    rewrite /oPMW.
+    simpl...
+    tp_bind (fc _ _ _); wp_bind (fc _ _ _).
+    iPoseProof ("Hfc" $! _ _ _ _ with "rhs") as "Hfc'".
+    iApply (wp_strong_mono'' with "Hfc'").
+    iIntros (tmpC) "(rhs & %c & %HtmpC & %HposC)".
+    rewrite HtmpC.
+    simpl...
+    wp_bind (ft _ _ _ _ _ _ _); tp_bind (ft _ _ _ _ _ _ _).
+    iPoseProof ("Hft" $! _ _ _ with "rhs") as "Hft'".
+    iApply (wp_strong_mono'' with "Hft'").
+    iIntros (tmpT) "(rhs & %t & %HtmpT & %HposT)".
+    rewrite HtmpT.
+    simpl...
+
+    wp_bind (get_unif _ _); tp_bind (get_unif _ _).
+    (* iPoseProof get_unif_det as "Hunif_det". *)
+    (* iCombine *)
+    iPoseProof (get_unif_det _ _ _ with "rhs") as "Hunif_det".
+    iApply (wp_strong_mono'' with "Hunif_det").
+    iIntros (vunif) "(rhs & %unif & %Hunif)".
+    simpl...
+
+    wp_bind (mw_upd _ _ _ _); tp_bind (mw_upd _ _ _ _).
+    (* iPoseProof upd_partial as "Hupd_partial". *)
+    iPoseProof (upd_partial _ _ _ _ _ with "rhs") as "Hupd_partial".
+    iApply (wp_strong_mono'' with "Hupd_partial").
+    iIntros (upd) "[rhs #Hupd]"...
+    iPoseProof (pMW_general_diffpriv εnum (c * εden) c t stream_q upd (λ: "q" "distrib" "x", c_query "q" "x" - c_query "q" "distrib")%V
+                  (λ: "q" "distrib" "x", c_query "q" "distrib" - c_query "q" "x")%V vunif unif) as "pMWG".
+    iSpecialize ("pMWG" $! _).
+    Unshelve.
+    2: { by apply Hunif. }
+    iSpecialize ("pMWG" $! _ _ _).
+    Unshelve.
+    3 : { real_solver. }
+    3 : { real_solver. }
+    2: {
+         do 2 rewrite -INR_IZR_INZ.
+         rewrite mult_INR Rmult_comm Rdiv_mult_distr.
+         replace (INR εnum / INR εden) with ε.
+         {
+           apply RIneq.Rdiv_pos_pos.
+           1, 2: done.
+         }
+         subst ε.
+         do 2 rewrite -INR_IZR_INZ.
+         done.
+    }
+
+    (* Hypothesis of stream query *)
+    iSpecialize ("pMWG" with "Hstream").
+
+    (* Hyposthesis of update *)
+    iSpecialize ("pMWG" with "Hupd").
+
+    (* Hyposthesis of f1 *)
+    iSpecialize ("pMWG" with "[]" ).
+    {
+      iModIntro.
+      iIntros (K' vq' vh h q') "%Hlh %Hlq' rhs".
+      tp_pures; wp_pures.
+      iModIntro.
+      iFrame.
+      iSplit.
+      - iModIntro.
+        rewrite /wp_sensitive.
+        iIntros (_ Kw x x') "rhs"...
+        iPoseProof (c_query_1_sens vq' q') as "Hq1s".
+        iSpecialize ("Hq1s" $! _).
+        iPoseProof (c_query_det _ vq' vh q' h) as "Hqdet".
+        iSpecialize ("Hqdet" $! _ _).
+        rewrite /wp_sensitive.
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iPoseProof ("Hqdet" with "rhs") as "Hqdet'".
+        iApply (wp_strong_mono'' with "Hqdet'").
+        iIntros (vres_f1_d) "(rhs & %res_f1_d & ->)".
+
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iSpecialize ("Hq1s" $! _ _ x x').
+        iPoseProof ("Hq1s" with "rhs") as "Hq1s'".
+        iApply (wp_strong_mono'' with "Hq1s'").
+        iIntros (vres_f1_n1) "(%res_f1_n1 & %res_f1_n2 & -> & rhs & %Hdisf1)"...
+        (* Set Printing All. *)
+        iModIntro.
+        simpl.
+        iExists (res_f1_n1 - res_f1_d)%Z.
+        iExists (res_f1_n2 - res_f1_d)%Z.
+        (* Set Printing All. *)
+        (* replace (BinOp MinusOp (Val (LitV (LitInt res_f1_n2))) (Val (LitV (LitInt res_f1_d)))) with (LitV (LitInt (Z.sub res_f1_n2 res_f1_d))). *)
+        iSplit. 1: done.
+        iSplit.
+        {
+          replace (BinOp MinusOp (Val (LitV (LitInt res_f1_n2))) (Val (LitV (LitInt res_f1_d)))) with (Val (LitV (LitInt (Z.sub res_f1_n2 res_f1_d)))).
+          1: done.
+          (* Set Printing All. *)
+          admit.
+        }
+        iPureIntro.
+        replace (res_f1_n1 - res_f1_d - (res_f1_n2 - res_f1_d))%Z with (res_f1_n1 - res_f1_n2)%Z.
+        { done. }.
+        lia.
+
+        Unshelve.
+        1, 2, 3: done.
+        lra.
+
+      - iPureIntro.
+        rewrite /det_q.
+        iIntros (K'' vdb'' db'') "%Hldb'' rhs".
+        tp_pures; wp_pures.
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iPoseProof (c_query_det _ vq' vh q' h) as "Hqdet".
+        iSpecialize ("Hqdet" $! _ _).
+        iPoseProof ("Hqdet" with "rhs") as "Hqdet'".
+        iApply (wp_strong_mono'' with "Hqdet'").
+        iIntros (vres_f1_d') "(rhs & %res_f1_d' & ->)".
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iClear "Hqdet".
+        iPoseProof (c_query_det _ vq' vdb'' q' db'') as "Hqdet".
+        iSpecialize ("Hqdet" $! _ _).
+        iPoseProof ("Hqdet" with "rhs") as "Hqdet'".
+        iApply (wp_strong_mono'' with "Hqdet'").
+        iIntros (vres_f1_d'') "(rhs & %res_f1_d'' & ->)".
+        simpl...
+        iModIntro.
+        iSplit.
+        {
+          replace (BinOp MinusOp (Val (LitV (LitInt res_f1_d''))) (Val (LitV (LitInt res_f1_d')))) with (Val (LitV (LitInt (Z.sub res_f1_d'' res_f1_d')))).
+          1: done.
+          (* Set Printing All. *)
+          admit. }
+        iExists (res_f1_d'' - res_f1_d')%Z.
+        iPureIntro.
+        done.
+
+        Unshelve.
+        1, 2, 3, 4: done.
+    }
+
+    (* Hyposthesis of f2 *)
+    iSpecialize ("pMWG" with "[]" ).
+    {
+      iModIntro.
+      iIntros (K' vq' vh h q') "%Hlh %Hlq' rhs".
+      tp_pures; wp_pures.
+      iModIntro.
+      iFrame.
+      iSplit.
+      - iModIntro.
+        rewrite /wp_sensitive.
+        iIntros (_ Kw x x') "rhs"...
+        iPoseProof (c_query_1_sens vq' q') as "Hq2s".
+        iSpecialize ("Hq2s" $! _).
+        rewrite /wp_sensitive.
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iSpecialize ("Hq2s" $! _ _ x x').
+        iPoseProof ("Hq2s" with "rhs") as "Hq2s'".
+        iApply (wp_strong_mono'' with "Hq2s'").
+        iIntros (vres_f2_n1) "(%res_f2_n1 & %res_f2_n2 & -> & rhs & %Hdisf2)"...
+        simpl...
+
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iPoseProof (c_query_det _ vq' vh q' h) as "Hqdet".
+        iSpecialize ("Hqdet" $! _ _).
+        iPoseProof ("Hqdet" with "rhs") as "Hqdet'".
+        iApply (wp_strong_mono'' with "Hqdet'").
+        iIntros (vres_f1_d) "(rhs & %res_f1_d & ->)".
+        simpl...
+
+        iModIntro.
+        iExists (res_f1_d - res_f2_n1)%Z.
+        iExists (res_f1_d - res_f2_n2)%Z.
+        iSplit.
+        { done. }
+        iSplit.
+        {
+          replace (BinOp MinusOp (Val (LitV (LitInt res_f1_d))) (Val (LitV (LitInt res_f2_n2)))) with (Val (LitV (LitInt (Z.sub res_f1_d res_f2_n2)))).
+          1: done.
+          (* Set Printing All. *)
+          admit. }
+
+        iPureIntro.
+        replace (res_f1_d - res_f2_n1 - (res_f1_d - res_f2_n2))%Z with (- res_f2_n1 + res_f2_n2)%Z.
+        { replace (Rabs (IZR (- res_f2_n1 + res_f2_n2))) with (Rabs (IZR (res_f2_n1 - res_f2_n2))).
+          1: done.
+          do 2 rewrite plus_IZR opp_IZR.
+          replace (IZR res_f2_n1 + - IZR res_f2_n2) with (-(- IZR res_f2_n1 + IZR res_f2_n2)).
+          1: by rewrite Rabs_Ropp.
+          lra. }
+        lia.
+
+        Unshelve.
+        2: lra.
+        1, 2, 3: done.
+
+      - iPureIntro.
+        rewrite /det_q.
+        iIntros (K'' vdb'' db'') "%Hldb'' rhs".
+        tp_pures; wp_pures.
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iPoseProof (c_query_det _ vq' vdb'' q' db'') as "Hqdet".
+        iSpecialize ("Hqdet" $! _ _).
+        iPoseProof ("Hqdet" with "rhs") as "Hqdet'".
+        iApply (wp_strong_mono'' with "Hqdet'").
+        iIntros (vres_f1_d'') "(rhs & %res_f1_d'' & ->)".
+        iClear "Hqdet".
+        simpl...
+
+        wp_bind (c_query _ _); tp_bind (c_query _ _).
+        iPoseProof (c_query_det _ vq' vh q' h) as "Hqdet".
+        iSpecialize ("Hqdet" $! _ _).
+        iPoseProof ("Hqdet" with "rhs") as "Hqdet'".
+        iApply (wp_strong_mono'' with "Hqdet'").
+        iIntros (vres_f1_d') "(rhs & %res_f1_d' & ->)".
+        simpl...
+
+        iModIntro.
+        iSplit.
+        {
+          replace (BinOp MinusOp (Val (LitV (LitInt res_f1_d'))) (Val (LitV (LitInt res_f1_d'')))) with (Val (LitV (LitInt (Z.sub res_f1_d' res_f1_d'')))).
+          1: done.
+          (* Set Printing All. *)
+
+          admit. }
+        iExists (res_f1_d' - res_f1_d'')%Z.
+        iPureIntro.
+        done.
+
+        Unshelve.
+        1, 2, 3, 4: done.
+    }
+
+    iSpecialize ("pMWG" $! db db' ddb K).
+    iSpecialize ("pMWG" with "[Hε]").
+    {
+      subst ε.
+      (* Set Printing Coercions. *)
+      replace (INR c * (IZR (Z.of_nat εnum) / IZR (Z.of_nat (c * εden)))) with (IZR (Z.of_nat εnum) / IZR (Z.of_nat εden)). 1: done.
+      do 3 rewrite -INR_IZR_INZ.
+      rewrite mult_INR Rmult_div_assoc Rdiv_mult_distr Rmult_div_r.
+      1: done.
+      lra.
+    }
+
+    (* Set Printing Coercions. *)
+    simpl...
+    replace (Val #(LitInt (Z.of_nat (c * εden)))) with (Val #(LitInt (Z.of_nat c * Z.of_nat εden))).
+    { iApply ("pMWG" with "rhs"). }
+    do 3 f_equal.
+    lia.
+    (* It would be greate if I could find a way to get rid of these 4 same goal. *)
+Admitted.
+
+
+
+End pmw.