Skip to content

Update to use the new chList #93

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ErVinuelas merged 4 commits into from
Oct 6, 2025
Merged

Update to use the new chList #93

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0ceaeba
adapt to new chList
ErVinuelas Jul 31, 2025
12b296d
Update to use the 'list choiceType
ErVinuelas Oct 2, 2025
cd56bfd
missing file with notation changes
ErVinuelas Oct 2, 2025
70201c2
spurious comments
ErVinuelas Oct 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 9 additions & 17 deletions theories/Crypt/examples/SecretSharing.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@
(* 'word == notation for Word *)
(* plus == receives two Words and returns the XOR of them *)
(* m ⊕ k == XOR of words m and k *)
(* 'seq t == local choice_type for sequences *)
(* 'set t == local choice_type for sets *)
(******************************************************************************)

Expand Down Expand Up @@ -155,13 +154,6 @@ Qed.
Notation " 'word " := (Word) (in custom pack_type at level 2).
Notation " 'word " := (Word) (at level 2): package_scope.

(* We can't use sequences directly in [choice_type] so instead we use a *)
(* map from natural numbers to the type. *)
Definition chSeq t := chMap 'nat t.

Notation " 'seq t " := (chSeq t) (in custom pack_type at level 2).
Notation " 'seq t " := (chSeq t) (at level 2): package_scope.

(* We can't use sets directly in [choice_type] so instead we use a map to *)
(* units. We can then use [domm] to get the domain, which is a set. *)

Expand All @@ -178,29 +170,29 @@ Definition shares: nat := 0.

Definition SHARE_pkg_tt:
package [interface]
[interface #val #[shares]: ('word × 'word) × 'set 'nat → 'seq 'word ] :=
[interface #val #[shares]: ('word × 'word) × 'set 'nat → 'list 'word ] :=
[package emptym ;
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'nat): 'seq 'word {
if size (domm U) >= 2 then ret emptym
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'nat): 'list 'word {
if size (domm U) >= 2 then ret [::]
else
s0 <$ uniform (2^n) ;;
let s1 := s0 ⊕ ml in
let sh := [fmap (0, s0) ; (1, s1)] in
ret (fmap_of_seq (pmap sh (domm U)))
ret (pmap sh (domm U))
}
].

Definition SHARE_pkg_ff:
package [interface]
[interface #val #[shares]: ('word × 'word) × 'set 'nat → 'seq 'word ] :=
[interface #val #[shares]: ('word × 'word) × 'set 'nat → 'list 'word ] :=
[package emptym ;
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'nat): 'seq 'word {
if size (domm U) >= 2 then ret emptym
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'nat): 'list 'word {
if size (domm U) >= 2 then ret [::]
else
s0 <$ uniform (2^n) ;;
let s1 := s0 ⊕ mr in
let sh := [fmap (0, s0) ; (1, s1)] in
ret (fmap_of_seq (pmap sh (domm U)))
ret (pmap sh (domm U))
}
].

Expand Down Expand Up @@ -266,7 +258,7 @@ Qed.

Theorem unconditional_secrecy LA A:
ValidPackage LA
[interface #val #[shares]: ('word × 'word) × 'set 'nat → 'seq 'word ]
[interface #val #[shares]: ('word × 'word) × 'set 'nat → 'list 'word ]
A_export A ->
Advantage SHARE A = 0%R.
Proof.
Expand Down
29 changes: 10 additions & 19 deletions theories/Crypt/examples/ShamirSecretSharing.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@
(* t' == the maximum number of shares the scheme is secure against. *)
(* n == number of shares. *)
(* p == number of possible messages. It is is a prime. *)
(* 'seq t == local choice_type for sequences *)
(* 'set t == local choice_type for sets *)
(******************************************************************************)

Expand Down Expand Up @@ -109,14 +108,6 @@ Notation " 'word " := (Word) (at level 2): package_scope.
Notation " 'share " := (Share) (in custom pack_type at level 2).
Notation " 'share " := (Share) (at level 2): package_scope.

(* We can't use sequences directly in [choice_type] so instead we use a map *)
(* from natural numbers to the type. *)

Definition chSeq t := chMap 'nat t.

Notation " 'seq t " := (chSeq t) (in custom pack_type at level 2).
Notation " 'seq t " := (chSeq t) (at level 2): package_scope.

(* We can't use sets directly in [choice_type] so instead we use a map to *)
(* units. We can then use [domm] to get the domain, which is a set. *)

Expand Down Expand Up @@ -267,7 +258,7 @@ Lemma sec_poly_bij (U: seq Party) (m m': Word) (q: {poly Word}):
make_shares m q U.
Proof.
move=> H.
by rewrite (sec_poly_bij_rec [::]).
by rewrite (sec_poly_bij_rec nil).
Qed.

Lemma bij_poly_bij (U: seq Party) (m m': Word) (q: {poly Word}):
Expand Down Expand Up @@ -430,29 +421,29 @@ Definition shares : nat := 0.
*)
Definition SHARE_pkg_tt:
package [interface]
[interface #val #[shares]: ('word × 'word) × 'set 'party → 'seq 'share ] :=
[interface #val #[shares]: ('word × 'word) × 'set 'party → 'list 'share ] :=
[package emptym ;
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'party): 'seq 'share {
if size (domm U) >= t then ret emptym
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'party): 'list 'share {
if size (domm U) >= t then ret [::]
else
q <$ uniform (p ^ t') ;;
let q := nat_to_poly t' q in
let sh := make_shares ml q (domm U) in
ret (fmap_of_seq sh)
ret sh
}
].

Definition SHARE_pkg_ff:
package [interface]
[interface #val #[shares]: ('word × 'word) × 'set 'party → 'seq 'share ] :=
[interface #val #[shares]: ('word × 'word) × 'set 'party → 'list 'share ] :=
[package emptym ;
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'party): 'seq 'share {
if size (domm U) >= t then ret emptym
#def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'party): 'list 'share {
if size (domm U) >= t then ret [::]
else
q <$ uniform (p ^ t') ;;
let q := nat_to_poly t' q in
let sh := make_shares mr q (domm U) in
ret (fmap_of_seq sh)
ret sh
}
].

Expand Down Expand Up @@ -510,7 +501,7 @@ Qed.

Theorem unconditional_secrecy LA A:
ValidPackage LA
[interface #val #[shares]: ('word × 'word) × 'set 'party → 'seq 'share ]
[interface #val #[shares]: ('word × 'word) × 'set 'party → 'list 'share ]
A_export A ->
Advantage SHARE A = 0%R.
Proof.
Expand Down
85 changes: 35 additions & 50 deletions theories/Crypt/examples/SymmRatchet.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,15 +38,6 @@ Import Order.POrderTheory.

Section SymmRatchet_example.

(**
We can't use sequences directly in [choice_type] so instead we use a map from
natural numbers to the type.
*)
Definition chSeq t := chMap 'nat t.

Notation " 'seq t " := (chSeq t) (in custom pack_type at level 2).
Notation " 'seq t " := (chSeq t) (at level 2): package_scope.

(**
This function is equivalent to [fmap_of_seq], but its definition is simpler,
which makes it possible to prove that [unzip2] cancels it.
Expand Down Expand Up @@ -99,13 +90,13 @@ Definition attack: nat := 2.
work directly with [seq]), and the final state [a].
*)
Fixpoint map_loop {T} {U A: choice_type} (s: seq T) (a: A) (c: T -> A -> raw_code (U × A)):
raw_code (('seq U) × A) :=
raw_code (('list U) × A) :=
match s with
| [::] => ret (emptym, a)
| [::] => ret ([::], a)
| t :: s' =>
ua1 ← c t a ;;
ua2 ← map_loop s' ua1.2 c ;;
ret (seq_to_chseq (ua1.1 :: unzip2 ua2.1), ua2.2)
ret ((ua1.1 :: ua2.1), ua2.2)
end.

(**
Expand Down Expand Up @@ -192,9 +183,9 @@ Definition CTXT b := if b then CTXT_pkg_tt else CTXT_pkg_ff.
*)
Definition GEN_STRETCH_pkg_tt:
package [interface]
[interface #val #[query]: 'nat → ('seq 'word) × 'word ] :=
[interface #val #[query]: 'nat → ('list 'word) × 'word ] :=
[package emptym ;
#def #[query] (k: 'nat): ('seq 'word) × 'word {
#def #[query] (k: 'nat): ('list 'word) × 'word {
s0 <$ uniform Word_N ;;
map_loop (iota 0 k) s0 (fun _ si =>
ret (PRG si)
Expand All @@ -204,9 +195,9 @@ Definition GEN_STRETCH_pkg_tt:

Definition GEN_STRETCH_pkg_ff:
package [interface]
[interface #val #[query]: 'nat → ('seq 'word) × 'word ] :=
[interface #val #[query]: 'nat → ('list 'word) × 'word ] :=
[package emptym ;
#def #[query] (k: 'nat): ('seq 'word) × 'word {
#def #[query] (k: 'nat): ('list 'word) × 'word {
t ← map_loop (iota 0 k) tt (fun _ _ =>
ti <$ uniform Word_N ;;
ret (ti, tt)
Expand All @@ -223,11 +214,11 @@ Definition GEN_STRETCH b := if b then GEN_STRETCH_pkg_tt else GEN_STRETCH_pkg_ff
*)
Definition ATTACK_pkg_tt:
package [interface]
[interface #val #[attack]: 'seq 'word → ('seq 'word) × 'word ] :=
[interface #val #[attack]: 'list 'word → ('list 'word) × 'word ] :=
[package emptym ;
#def #[attack] (m: 'seq 'word): ('seq 'word) × 'word {
#def #[attack] (m: 'list 'word): ('list 'word) × 'word {
s0 <$ uniform Word_N ;;
map_loop (unzip2 m) s0 (fun mi si =>
map_loop m s0 (fun mi si =>
let xy := PRG si in
ret (enc xy.1 mi, xy.2)
)
Expand All @@ -236,10 +227,10 @@ Definition ATTACK_pkg_tt:

Definition ATTACK_pkg_ff:
package [interface]
[interface #val #[attack]: 'seq 'word → ('seq 'word) × 'word ] :=
[interface #val #[attack]: 'list 'word → ('list 'word) × 'word ] :=
[package emptym ;
#def #[attack] (m: 'seq 'word): ('seq 'word) × 'word {
c ← @map_loop _ Word _ (unzip2 m) tt (fun _ _ =>
#def #[attack] (m: 'list 'word): ('list 'word) × 'word {
c ← @map_loop _ Word _ m tt (fun _ _ =>
ci <$ uniform Word_N ;;
ret (ci, tt)
) ;;
Expand All @@ -252,13 +243,13 @@ Definition ATTACK b := if b then ATTACK_pkg_tt else ATTACK_pkg_ff.

Definition ATTACK_GEN_pkg:
package
[interface #val #[query]: 'nat → ('seq 'word) × 'word ]
[interface #val #[attack]: 'seq 'word → ('seq 'word) × 'word ] :=
[interface #val #[query]: 'nat → ('list 'word) × 'word ]
[interface #val #[attack]: 'list 'word → ('list 'word) × 'word ] :=
[package emptym ;
#def #[attack] (m: 'seq 'word): ('seq 'word) × 'word {
#import {sig #[query]: 'nat → ('seq 'word) × 'word } as query ;;
#def #[attack] (m: 'list 'word): ('list 'word) × 'word {
#import {sig #[query]: 'nat → ('list 'word) × 'word } as query ;;
ts ← query (size m) ;;
c ← map_loop (zip (unzip2 ts.1) (unzip2 m)) tt (fun tm _ =>
c ← map_loop (zip ts.1 m) tt (fun tm _ =>
let (ti, mi) := (tm.1, tm.2) in
ret (enc ti mi, tt)
) ;;
Expand All @@ -268,10 +259,10 @@ Definition ATTACK_GEN_pkg:

Definition ATTACK_HYB_pkg:
package [interface]
[interface #val #[attack]: 'seq 'word → ('seq 'word) × 'word ] :=
[interface #val #[attack]: 'list 'word → ('list 'word) × 'word ] :=
[package emptym ;
#def #[attack] (m: 'seq 'word): ('seq 'word) × 'word {
c ← map_loop (unzip2 m) tt (fun mi _ =>
#def #[attack] (m: 'list 'word): ('list 'word) × 'word {
c ← map_loop m tt (fun mi _ =>
ti <$ uniform Word_N ;;
ret (enc ti mi, tt)
) ;;
Expand All @@ -283,11 +274,11 @@ Definition ATTACK_HYB_pkg:
Definition ATTACK_CTXT_pkg:
package
[interface #val #[ctxt]: 'word → 'word ]
[interface #val #[attack]: 'seq 'word → ('seq 'word) × 'word ] :=
[interface #val #[attack]: 'list 'word → ('list 'word) × 'word ] :=
[package emptym ;
#def #[attack] (m: 'seq 'word): ('seq 'word) × 'word {
#def #[attack] (m: 'list 'word): ('list 'word) × 'word {
#import {sig #[ctxt]: 'word → 'word } as ctxt ;;
c ← map_loop (unzip2 m) tt (fun mi _ =>
c ← map_loop m tt (fun mi _ =>
ci ← ctxt mi ;;
ret (ci, tt)
) ;;
Expand Down Expand Up @@ -316,7 +307,7 @@ Proof.
apply: boolp.funext => y.
by rewrite {1}(lock (y.1)).
}
rewrite -(bind_ret _ (map_loop (unzip2 m) s0 _)).
rewrite -(bind_ret _ (map_loop m s0 _)).
erewrite bind_cong.
2: by [].
2: {
Expand All @@ -326,22 +317,19 @@ Proof.
}
move: (@locked _) => /= X.
ssprove_code_simpl.
rewrite -(size_map snd) -/unzip2.
move: 0 (unzip2 m) => {m} a m.
move: 0 ( m) => {m} a m.
elim: m => [|mi m IHm] /= in X a s0*.
1: by apply: rreflexivity_rule.
rewrite (lock seq_to_chseq).
ssprove_code_simpl.
case: (PRG s0) => [ti si] /=.
rewrite -lock.
erewrite (bind_cong _ _ (@map_loop _ Word _ (iota a.+1 (size m)) si _)).
2: by [].
2: {
apply: boolp.funext => x.
by rewrite unzip2_seq_to_chseq.
by [].
}
ssprove_code_simpl.
by specialize (IHm (fun x => X (seq_to_chseq (enc ti mi :: unzip2 x)))).
by specialize (IHm (fun x => X (enc ti mi :: x))).
Qed.

Lemma ATTACK_HYB_equiv_1:
Expand All @@ -366,30 +354,26 @@ Proof.
apply: boolp.funext => y.
by rewrite {1}(lock (y.1)).
}
erewrite (bind_cong _ _ (map_loop (unzip2 m) tt _)).
erewrite (bind_cong _ _ (map_loop m tt _)).
2: by [].
2: {
apply: boolp.funext => x.
rewrite {1}(surjective_pairing x).
by rewrite {1}(lock x.1).
}
rewrite -(size_map snd) -/unzip2.
move: 0 (unzip2 m) (@locked _) => {m} a m X.
move: 0 (m) (@locked _) => {m} a m X.
elim: m => [|mi m IHm] /= in X a*.
1: by apply: rreflexivity_rule.
rewrite (lock seq_to_chseq).
ssprove_code_simpl.
ssprove_sync_eq=> ci.
rewrite -lock.
erewrite (bind_cong _ _ (@map_loop _ Word _ (iota a.+1 (size m)) tt _)).
erewrite (bind_cong ).
2: by [].
2: {
apply: boolp.funext => x.
rewrite unzip2_seq_to_chseq.
by [].
}
ssprove_code_simpl.
specialize (IHm (fun s => X (seq_to_chseq (enc ci mi :: unzip2 s)))).
specialize (IHm (fun s => X (enc ci mi :: s))).
by simpl in IHm.
Qed.

Expand Down Expand Up @@ -446,15 +430,16 @@ Definition cpa_epsilon := Advantage CTXT.

Lemma forward_secrecy_based_on_prg LA A:
ValidPackage LA
[interface #val #[attack]: 'seq 'word → ('seq 'word) × 'word ]
[interface #val #[attack]: 'list 'word → ('list 'word) × 'word ]
A_export A ->
Advantage ATTACK A <=
prg_epsilon (A ∘ ATTACK_GEN_pkg) +
cpa_epsilon (A ∘ ATTACK_CTXT_pkg).
Proof.
move=> vA.
rewrite Advantage_E Advantage_sym.
ssprove triangle (ATTACK true) [::
ssprove triangle (ATTACK true)
[::
ATTACK_GEN_pkg ∘ GEN_STRETCH true ;
ATTACK_GEN_pkg ∘ GEN_STRETCH false ;
pack ATTACK_HYB_pkg ;
Expand Down
5 changes: 5 additions & 0 deletions theories/Crypt/package/pkg_notation.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@
'unit
'option A
'fin n
'list A
A + B
A × B
{map A → B}
where A and B follow again the same syntax and n is a natural number
Expand Down Expand Up @@ -126,6 +128,8 @@ Module PackageNotation.
Notation " 'unit " := (chUnit) (in custom pack_type at level 2).
Notation " 'word n " := (chWord n) (in custom pack_type at level 2).
Notation " 'option x " := (chOption x) (in custom pack_type at level 2).
Notation " 'list x " := (chList x) (in custom pack_type at level 2).


Notation " 'fin n " :=
(chFin (mkpos n))
Expand All @@ -147,6 +151,7 @@ Module PackageNotation.
Notation " 'unit " := (chUnit) (at level 2) : package_scope.
Notation " 'word n " := (chWord n) (at level 2) : package_scope.
Notation " 'option x " := (chOption x) (at level 2) : package_scope.
Notation " 'list x " := (chList x) (at level 2) : package_scope.

Notation " 'fin x " :=
(chFin (mkpos x))
Expand Down