PMW formal - #72

Open

Pbi0 wants to merge 91 commits into

logsem:mainfrom

Pbi0:pMW_formal

Commits on Jun 2, 2026

add: nSVT.v
Langlois
committed
682c83e
fix: README
Langlois
committed
04b1b67

Commits on Jun 3, 2026

proof_cpl: nAT spec
Langlois
committed
4e5d5f5

Commits on Jun 4, 2026

add: def+spec+proof onSVT
Langlois
committed
262a14f
fix: nSVT, right coeffs
Langlois
committed
28e2b1a

Commits on Jun 8, 2026

rename & clean: nSVT.v -> numeric_sparse_vector_technique.v
Langlois
committed
1e73f5e
nSVT interpreted but not compiled
Langlois
committed
375c002

Commits on Jun 9, 2026

add: branch for dev / for compile, pmw
Langlois
committed
d3621b2
compiled ?
Langlois
committed
90c1bed

Commits on Jun 10, 2026

fix: option Z and add the stream client + proof
Langlois
committed
db2713a
merge & end: numeric_sparse_vector_technique
Langlois
committed
17c55a8
clean: nSVT
Langlois
committed
8af8acb
add: OCaml implementation of nSVT, 1/epsilon
Langlois
committed
f552447
add: OCaml nSVT implementation
Langlois
committed
39aa42e
add: nSVT main.ml intermediate epsilon
Langlois
committed
6573d29

Commits on Jun 11, 2026

add: pmw OCaml implementation, no good tests yet
Langlois
committed
c9d3edd
clean: numeric_sparse_vector_technique.v
Langlois
committed
e8d2c96

Commits on Jun 15, 2026

fix: srcs nsvt & pmw
Langlois
committed
90c7546
add: pmw.v
Langlois
committed
6c7e4c1

Commits on Jun 16, 2026

pmw.ml: results, not what expected but still RESULTSgit add db_sampling.ml main_pmw.ml private_multiplicative_weights.ml
Langlois
committed
bbeb919
format: implem OCaml
Langlois
committed
56145a9

Commits on Jun 17, 2026

clean: rename main in numeric_spares_vector implem
Langlois
committed
10871d7
add: README for the ocaml implementation of nSVT and PMW
Langlois
committed
b5c42a6
fix: README implem OCaml
Langlois
committed
b285efd
fix: ref README implem OCaml
Langlois
committed
57c27c3
fix: all ref README implem OCaml
Langlois
committed
799418b
fix: titles README implem OCaml
Langlois
committed
6f0814b
fix: math README.md
Langlois
committed
40884f1
fix: 2 math README.md
Langlois
committed
a38b101

Commits on Jun 19, 2026

pmw.v: befor big change
Langlois
committed
ea1e7be
implem pmw: fixs to stay the same as the formal algo
Langlois
committed
d764b33

Commits on Jun 24, 2026

before change in the algorithm
Langlois
committed
d707929
Issue: q distrib in pMW.v
Langlois
committed
2b725ce
Before breaking changes: pmw.ml
Langlois
committed
53252f2
after change: still issue on weird convergence of the distribution
Langlois
committed
6fecc1d
add: data for ocaml implem
Langlois
committed
de49a33
add: implem ocaml, db utils and gen db
Langlois
committed
f6682a3

Commits on Jun 25, 2026

Convergence: almost ok, still issue on threshold
Langlois
committed
a347c07
clean: data src
Langlois
committed
874aed7
add: README data src
Langlois
committed
28d35e5
fix: READMEs src
Langlois
committed
811c490
almost working: src pmw (still issue with threshold + matches with reame
Langlois
committed
4f17c46
fix: precision->size pmw
Langlois
committed
5336ae0
clean & factorisation: implementation OCaml
Langlois
committed
06fd4ce
pmw data: change in the distribution
Langlois
committed
1d8a8ac
fix: wrong normalization in mk_histo
Langlois
committed
c3c4d94
change name nsvt -> pmw
Langlois
committed
8b47e37
proof: before change in algo
Langlois
committed
95849bb
add: gif representation of the evolution of the distrib
Langlois
committed
0de22d9
clear: jpg for gif
Langlois
committed
76a7238
add: data for gif
Langlois
committed
a764a4a
clean: data for gif
Langlois
committed
c42cf2a
add: readme for pmw ml gif
Langlois
committed
0634480

Commits on Jun 26, 2026

clean: nsvt.v
Langlois
committed
0c0b29f
determinism of q in use: still an issue with upd _ db _
Langlois
committed
82dc09b
fix: main_pmw.ml, no gif.
Langlois
committed
0eb4265
fix: readme pmw
Langlois
committed
a947248
PMW: First proof with qed
Langlois
committed
39bccba
fix: pmw, add 1sens hyp for f1 & f2
Langlois
committed
072bace

Commits on Jul 2, 2026

src: Update README
Langlois
committed
2e89764
src: major clean
Langlois
committed
6ff64de

Commits on Jul 6, 2026

fix: gen_data -> str, render -> everyting is automatic
Langlois
committed
eb10afe
list: implementation as in rocq
Langlois
committed
0b62172
update: REAMES automated calls
Langlois
committed
1f4e648
modif: distrib + gif
Langlois
committed
67697fa
clean + adapt coefs src
Langlois
committed
9862253
try: add gif in readme
Langlois
committed
0fa9ce4
src: list part in int lists
Langlois
committed
0a3fd95
src: gif render linear and not constant clip for the y axis
Langlois
committed
46891e1
src: utils clean
Langlois
committed
777f793
add: src, description of --list
Langlois
committed
70f485a

Commits on Jul 8, 2026

fix: proof for pmw with lists
Langlois
committed
409160b

Commits on Jul 9, 2026

fix: src render + readme
Langlois
committed
364c83f
upd: src alpha + render + evolution gif
Langlois
committed
fced8cb
fix: src, gif opti
Langlois
committed
8d72636

Commits on Jul 10, 2026

fix: src render time
Langlois
committed
f556d43
fix: src var name card_q -> log_card_q
Langlois
committed
e5d795e

Commits on Jul 13, 2026

proof: before change in the compute query
Langlois
committed
71a5f7f
src: c_query as in rocq
Langlois
committed
74ef536

Commits on Jul 15, 2026

src: anum aden ... manipulates integers
Langlois
committed
e425a51

Commits on Jul 17, 2026

proof: almost complete 4 same admit and some lemmas assumed, won't have the time to prove them
Langlois
committed
0c1cb2b
src: Heterogenous Data
Langlois
committed
e7c3ae8
src: add gif 1 readme
Langlois
committed
82a7675
src: overestimation issue
Langlois
committed
f634619
src: fix readmes
Langlois
committed
3dc67d3
src: illustration of issue of the list implementation
Langlois
committed
a1c6345
src: fix readme
Langlois
committed
992935a
src: readme add source
Langlois
committed
dbd6023
fix: issue threhold ?
Langlois
committed
c640ab2
src: fix readme
Langlois
committed
2e66c6b
src: fix readme
Langlois
committed
9e69b8a