split SmtMap into SMT Array and finite map

this is meant to enable the development of a library of infinite arrays (as SMT arrays from int)
EasyCrypt · Oct 8, 2024 · 6942bd0 · 6942bd0
1 parent edc5f72
commit 6942bd0
Show file tree

Hide file tree

Showing 28 changed files with 1,040 additions and 1,045 deletions.
diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec
@@ -1,4 +1,4 @@
-require import AllCore List Int IntDiv Real SmtMap Distr DBool DList DProd FSet PROM SplitRO FelTactic.
+require import AllCore List Int IntDiv Real FMap Distr DBool DList DProd FSet PROM SplitRO FelTactic.
 require import FinType.
 
 require (****) Subtype Ske RndProd Indistinguishability Monoid EventPartitioning.

diff --git a/examples/ChaChaPoly/ske.ec b/examples/ChaChaPoly/ske.ec
@@ -1,4 +1,4 @@
-require import AllCore List DBool SmtMap.
+require import AllCore List DBool FMap.
 
 abstract theory SKE.
 

diff --git a/examples/MEE-CBC/CBC.eca b/examples/MEE-CBC/CBC.eca
@@ -1,6 +1,6 @@
 (*** A proof that CBC mode turns any weak PRP into an IND$- CPA-secure
  symmetric encryption scheme **when used with random IVs** ***)
-require import AllCore Int Real Distr List FSet SmtMap.
+require import AllCore Int Real Distr List FSet FMap.
 require import StdRing StdOrder DList.
 require (*ab*) PRP PRF SKE_INDR. (* Definitions and Security Notions *)
 (*---*) import RField RealOrder.

diff --git a/examples/PRG.ec b/examples/PRG.ec
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-require import AllCore List Distr FSet SmtMap.
+require import AllCore List Distr FSet FMap.
 require import IntDiv Mu_mem StdRing StdOrder StdBigop.
 (*---*) import Bigint Ring.IntID RField IntOrder RealOrder BIA.
 require (*--*) FinType.

diff --git a/examples/UC/MapAux.ec b/examples/UC/MapAux.ec
@@ -2,7 +2,7 @@
 
 prover [""].
 
-require import AllCore SmtMap FSet StdOrder.
+require import AllCore FMap FSet StdOrder.
 import IntOrder.
 
 lemma get_none (m : ('a, 'b) fmap, x : 'a) :

diff --git a/examples/UC/RndO.ec b/examples/UC/RndO.ec
@@ -2,7 +2,7 @@
 
 prover [""].
 
-require import AllCore List MapAux SmtMap FSet Distr.
+require import AllCore List MapAux FMap FSet Distr.
 require IterProc.
 
 type flag = [ Unknown | Known ]. (* map setting known by distinguisher? *)

diff --git a/examples/br93.ec b/examples/br93.ec
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-require import AllCore List FSet SmtMap.
+require import AllCore List FSet FMap.
 require import Distr DBool.
 require (*--*) BitWord OW ROM.
 
@@ -287,7 +287,7 @@ seq 8 5: ( ={glob A, glob LRO, glob Log, pk, sk, b}
 + auto; call (: ={glob Log, glob LRO}
  /\ (forall x, x \in Log.qs{1} <=> x \in LRO.m{1})).
  + proc; inline LRO.o.
- by auto=> /> &2 log_is_dom y _; smt(@SmtMap).
+ by auto=> /> &2 log_is_dom y _; smt(@FMap).
  by inline *; auto=> /> _ _ x; rewrite mem_empty.
 (* We now deal with everything that happens after the programs differ: *)
 (* - until r gets queried to the random oracle by the adversary *)

diff --git a/examples/prg-tutorial/PRF.eca b/examples/prg-tutorial/PRF.eca
@@ -1,5 +1,5 @@
 (*** A formalization of pseudo-random functions **)
-require import Int Real FSet SmtMap Distr.
+require import Int Real FSet FMap Distr.
 
 (** A PRF is a family of functions F from domain D to finite range R
  indexed by a keyspace K equipped with a distribution dK. *)

diff --git a/examples/prg-tutorial/PRGc.ec b/examples/prg-tutorial/PRGc.ec
@@ -5,7 +5,7 @@
  * ac9b6e7bc63468cbcc2367fefc1e7fb073a15642 *)
 
 (* Loading core datatype theories *)
-require import AllCore List FSet SmtMap.
+require import AllCore List FSet FMap.
 (* Loading algebraic theories *)
 require import StdRing StdOrder StdBigop.
 (*---*) import Ring.IntID RField IntOrder RealOrder Bigreal BRA.

diff --git a/theories/crypto/PRF.eca b/theories/crypto/PRF.eca
@@ -31,7 +31,7 @@ module IND (F : PRF) (D : Distinguisher) = {
 
 (* -------------------------------------------------------------------- *)
 abstract theory RF.
-require import SmtMap.
+require import FMap.
 
 op dR: { D -> R distr | forall x, is_lossless (dR x) } as dR_ll.
 

diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec
@@ -1,7 +1,7 @@
 pragma +implicits.
 
 (* -------------------------------------------------------------------- *)
-require import AllCore SmtMap Distr Mu_mem.
+require import AllCore FMap Distr Mu_mem.
 require import FinType.
 require import StdBigop FelTactic.
 

diff --git a/theories/crypto/PRP.eca b/theories/crypto/PRP.eca
@@ -64,7 +64,7 @@ end StrongPRP.
 (** Ideal and Real functionalities **)
 (* -------------------------------------------------------------------- *)
 abstract theory RP.
-require import SmtMap FSet.
+require import FMap FSet.
 require import Dexcepted.
 (*---*) import StdOrder.RealOrder RField.
 

diff --git a/theories/crypto/ROM.eca b/theories/crypto/ROM.eca
@@ -37,7 +37,7 @@ module Exp (H : Oracle) (D : Distinguisher) = {
 
 (* -------------------------------------------------------------------- *)
 theory Lazy.
-require import SmtMap.
+require import FMap.
 
 module LRO : Oracle = {
  var m : (in_t, out_t) fmap
@@ -92,7 +92,7 @@ end Lazy.
 
 (* -------------------------------------------------------------------- *)
 abstract theory FiniteEager.
-require import List SmtMap.
+require import List FMap.
 require import FinType.
 
 (** TODO: expose finiteness assumption **)
@@ -151,7 +151,7 @@ end FiniteEager.
 
 (* -------------------------------------------------------------------- *)
 abstract theory LazyEager.
-require import List SmtMap PROM.
+require import List FMap PROM.
 require import FinType.
 
 clone import FinType with
@@ -433,7 +433,7 @@ end SetLog.
 
 (* -------------------------------------------------------------------- *)
 abstract theory ROM_BadCall.
-require import FSet SmtMap.
+require import FSet FMap.
 
 op qH : int.
 

diff --git a/theories/crypto/SplitRO.ec b/theories/crypto/SplitRO.ec
@@ -1,4 +1,4 @@
-require import AllCore PROM SmtMap Distr DProd.
+require import AllCore PROM FMap Distr DProd.
 
 abstract theory Split.
 

diff --git a/theories/crypto/assumptions/AEAD.ec b/theories/crypto/assumptions/AEAD.ec
@@ -1,5 +1,5 @@
-require import AllCore List FSet SmtMap Distr DBool DList.
-(*require import AllCore Distr FSet SmtMap DBool. *)
+require import AllCore List FSet FMap Distr DBool DList.
+(*require import AllCore Distr FSet FMap DBool. *)
 
 type K.
 type Msg.

diff --git a/theories/crypto/assumptions/CRHash.ec b/theories/crypto/assumptions/CRHash.ec
@@ -1,4 +1,4 @@
-require import AllCore FSet SmtMap Distr.
+require import AllCore FSet FMap Distr.
 (* Formalisation of collision resistance:
  CR : Collision resistance game 
  RealHash/IdealHash: 

diff --git a/theories/crypto/assumptions/DHIES.ec b/theories/crypto/assumptions/DHIES.ec
@@ -1,4 +1,4 @@
-require import AllCore FSet CoreMap SmtMap List.
+require import AllCore FSet CoreMap FMap List.
 require import Distr DList DJoin DMap StdOrder.
 require import AEAD.
 require (*--*) MRPKE.
@@ -107,7 +107,7 @@ theory DHIES.
  i <- i-1;
  }
 
- return SmtMap.ofassoc cphList;
+ return FMap.ofassoc cphList;
  }
 
  proc decrypt (sk : Sk, tag : Tag, ctxt : CTxt) : PTxt option = {
@@ -146,7 +146,7 @@ theory DHIES.
  keys <- map (fun pk => (pk, (g ^ eph, hash (pk ^ eph)))) pkl;
  (* cphs : (Pk * (group * Cph)) *)
  cphs <$ mencDHIES tag ptxt keys;
- cph <- SmtMap.ofassoc cphs;
+ cph <- FMap.ofassoc cphs;
  return cph;
  }
  proc mencDHIES1(tag : AData, ptxt : Msg, kks : (Pk * (group * K)) list)
@@ -255,7 +255,7 @@ theory DHIES.
  outline {1} [1] { cph <@ MEncrypt_map.S.sample(
  dlet_locked (mkeyDHIES (elems mpk))
  (mencDHIES tag ptxt),
- SmtMap.ofassoc <: Pk, group * Cph> ); }.
+ FMap.ofassoc <: Pk, group * Cph> ); }.
  + by inline*; auto; rewrite dlet_lockedE.
  rewrite equiv[{1} 1 MEncrypt_map.sample].
  inline*; swap{1} 2 1.
@@ -344,8 +344,8 @@ module Adv1_Procs (ODHOrcl : ODH_OrclT) : MRPKE_OrclT = {
  keys <@ ODHOrcl.ror(pks);
  skeylist <- map (fun x:_*(_*_)=>((x.`1,x.`2.`1),x.`2.`2)) (oget keys);
  enclist <$ mencDHIES tag (if MRPKE_lor.b then m1 else m0) (oget keys);
- cph <- SmtMap.ofassoc enclist;
- skeys <- skeys + SmtMap.ofassoc skeylist;
+ cph <- FMap.ofassoc enclist;
+ skeys <- skeys + FMap.ofassoc skeylist;
  MRPKE_lor.lorlist <- MRPKE_lor.lorlist ++ fold_encs pks tag cph;
  ro <- Some cph;
  }
@@ -409,10 +409,10 @@ lemma tagmem_foldenc pk t c pks tag mctxt:
 proof. by move=> /mapP [x [Hx //]]. qed.
 
 lemma ctxt1mem_foldenc pk t c pks tag mctxt:
- (pk,t,c) \in fold_encs pks tag (SmtMap.ofassoc mctxt) => c.`1=(oget (assoc mctxt pk)).`1.
+ (pk,t,c) \in fold_encs pks tag (FMap.ofassoc mctxt) => c.`1=(oget (assoc mctxt pk)).`1.
 proof.
 move=> /mapP [x [Hx //=]] [<<- [? ->]].
-by rewrite SmtMap.ofassoc_get.
+by rewrite FMap.ofassoc_get.
 qed.
 
 lemma mem_mencDHIES cphs tag ptxt kk:
@@ -429,7 +429,7 @@ qed.
 lemma ephmem_foldenc pk t c pks tag ptxt mctxt kk:
  (pk \in map fst kk)%List =>
  mctxt \in mencDHIES tag ptxt kk =>
- (pk,t,c) \in fold_encs pks tag (SmtMap.ofassoc mctxt) =>
+ (pk,t,c) \in fold_encs pks tag (FMap.ofassoc mctxt) =>
  c.`1 = fst (oget (assoc kk pk)).
 proof.
 move=> Hin2 /mem_mencDHIES Hmap ? .
@@ -499,14 +499,14 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
  rewrite (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
  by apply/(supp_dlist_size _ _ _ _ H12)/size_ge0.
  move=> /= ? ?.
- rewrite joinE; pose E := (_ \in _)%SmtMap; case: E; rewrite /E; clear E; last smt().
+ rewrite joinE; pose E := (_ \in _)%FMap; case: E; rewrite /E; clear E; last smt().
  rewrite -map_comp /(\o) /= ofassoc_get mem_ofassoc -map_comp /(\o) /=.
  move=> /mapP [pk' [Hpk' /= [-> ->]]] _; smt (mem_fdom memE).
  + move: H16 H17 H18; rewrite !H /=.
  rewrite (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
  by apply/(supp_dlist_size _ _ _ _ H12)/size_ge0.
  move=> /= ? ?.
- rewrite joinE; pose E := (_ \in _)%SmtMap; case: E; rewrite /E; clear E; last smt().
+ rewrite joinE; pose E := (_ \in _)%FMap; case: E; rewrite /E; clear E; last smt().
  rewrite -map_comp /(\o) /= ofassoc_get.
  move => ? ?; exists ephL.
  move: (assoc_some _ _ _ H20) => /mapP [v [? /= [[? ?] ?]]]; smt().
@@ -534,7 +534,7 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
  + move: H16 H17 H19; rewrite !H /= (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
  by apply/(supp_dlist_size _ _ _ _ H12)/size_ge0.
  move=> /= ? ?.
- rewrite joinE; pose E := (_ \in _)%SmtMap; case: E; rewrite /E; clear E; last smt().
+ rewrite joinE; pose E := (_ \in _)%FMap; case: E; rewrite /E; clear E; last smt().
  rewrite -map_comp /(\o) /= ofassoc_get => ? ?.
  move: (assoc_some _ _ _ H20) => /mapP [v [? /= [[? ?] ?]]].
  rewrite H24 H23 -H22.
@@ -580,8 +580,8 @@ module MRPKErnd_lor = {
  if (pks \subset fdom MRPKE_lor.pklist /\ size (elems pks) < q_maxn) {
  keys <$ mrndkeyDHIES (elems pks);
  enclist <$ mencDHIES tag (if MRPKE_lor.b then m1 else m0) keys;
- cph <- SmtMap.ofassoc enclist;
- skeys <- skeys + SmtMap.ofassoc (map (fun x:_*(_*_) => ((x.`1,x.`2.`1),x.`2.`2)) keys);
+ cph <- FMap.ofassoc enclist;
+ skeys <- skeys + FMap.ofassoc (map (fun x:_*(_*_) => ((x.`1,x.`2.`1),x.`2.`2)) keys);
  MRPKE_lor.lorlist <- MRPKE_lor.lorlist ++ fold_encs pks tag cph;
  ro <- Some cph;
  }
@@ -729,12 +729,12 @@ module Adv2_Procs (AEADmul_Orcl : AEADmul_OraclesT) : MRPKE_OrclT = {
  aeadcph <@ AEADmul_Orcl.lor(size (elems pks),tag,m0,m1);
  if (aeadcph <> None) {
  (* (pk, gx), kidx *)
- kindex <- kindex + SmtMap.ofassoc (zip (map (fun pk => (pk, gx)) (elems pks))
+ kindex <- kindex + FMap.ofassoc (zip (map (fun pk => (pk, gx)) (elems pks))
  (map fst (oget aeadcph)));
- ro <- Some (SmtMap.ofassoc (zip (elems pks)
+ ro <- Some (FMap.ofassoc (zip (elems pks)
  ((map (fun cph => (gx,snd cph)) (oget aeadcph)))));
  MRPKErnd_lor.skeys <- MRPKErnd_lor.skeys +
- SmtMap.ofassoc (map (fun pk => ((pk, gx),witness)) (elems pks));
+ FMap.ofassoc (map (fun pk => ((pk, gx),witness)) (elems pks));
  }
  MRPKE_lor.lorlist <- MRPKE_lor.lorlist ++ (fold_encs pks tag (oget ro));
  }
@@ -778,11 +778,11 @@ module Adv2(A : MRPKE_Adv, O : AEADmul_OraclesT) = {
 lemma mem_fold_encs pk tag x pks l:
  pk \in elems pks =>
  assoc (zip (elems pks) l) pk = Some x =>
- (pk, tag, x) \in fold_encs pks tag (SmtMap.ofassoc (zip (elems pks) l)).
+ (pk, tag, x) \in fold_encs pks tag (FMap.ofassoc (zip (elems pks) l)).
 proof.
 rewrite /fold_encs => ? ?.
 have ->: (pk,tag,x)
- = (fun pk => (pk, tag, oget (SmtMap.ofassoc (zip (elems pks) l)).[pk])) pk.
+ = (fun pk => (pk, tag, oget (FMap.ofassoc (zip (elems pks) l)).[pk])) pk.
  by rewrite /= ofassoc_get H0.
 rewrite mem_map // => a b; smt().
 qed.
@@ -898,15 +898,15 @@ last by wp; skip; rewrite /inv /= => />; smt (fdom0 emptyE).
  + move: H12; rewrite mem_cat; move=> [?|]. smt (size_ge0).
  move=> /mapP [[y1 y2] /=] /> /mem_zip_fst; smt (size_ge0 mem_iota).
  + move: H12; rewrite /= joinE.
- pose E:= ((pk, eph) \in _)%SmtMap; case: E => ?; last smt().
+ pose E:= ((pk, eph) \in _)%FMap; case: E => ?; last smt().
  rewrite ofassoc_get assoc_zip unzip1_zip; first 3 smt (size_map size_iota size_ge0).
  move=> ?; move: (onth_some_mem _ _ _ H13); smt (size_ge0 mem_iota).
  + move: H12; rewrite joinE.
- pose E:= ((pk, eph) \in _)%SmtMap; case: E => ?; last smt(size_ge0).
+ pose E:= ((pk, eph) \in _)%FMap; case: E => ?; last smt(size_ge0).
  rewrite ofassoc_get assoc_zip unzip1_zip; first 3 smt (size_map size_iota size_ge0).
  move=> ?; move: (onth_some_mem _ _ _ H14). smt (size_ge0 mem_iota).
  + move: H12; rewrite /= joinE mem_cat.
- pose E:= ((pk, eph) \in _)%SmtMap; case: E => ? ?; last first.
+ pose E:= ((pk, eph) \in _)%FMap; case: E => ? ?; last first.
  have T: (i, tag0, c) \in AEADmul_Oracles.lorlist{2}.
  move: H13; rewrite mem_cat; move=> [? /#|?].
  move: H13 => /mapP [[iy cy] /= [?]]; progress.
@@ -935,12 +935,12 @@ last by wp; skip; rewrite /inv /= => />; smt (fdom0 emptyE).
  rewrite (nth_map witness); smt (mem_iota size_ge0).
  rewrite (map_comp snd snd) unzip2_zip 1:size_map 1:/#.
  by rewrite -map_comp /(\o) /= map_id.
- move: H12; pose E:= ((pk, eph) \in _)%SmtMap; case: E => ? ?; last first.
- pose E':= ((pk, eph) \in _)%SmtMap; case: E' => ?; last first.
+ move: H12; pose E:= ((pk, eph) \in _)%FMap; case: E => ? ?; last first.
+ pose E':= ((pk, eph) \in _)%FMap; case: E' => ?; last first.
  rewrite (H6 pk eph i) //; smt (nth_cat).
  move: H12 H14; rewrite /E /E' !mem_ofassoc !unzip1_zip;
  smt (size_iota size_ge0 size_map).
- pose E':= ((pk, eph) \in _)%SmtMap; case: E' => ?; last first.
+ pose E':= ((pk, eph) \in _)%FMap; case: E' => ?; last first.
  move: H12 H14; rewrite /E /E' !mem_ofassoc !unzip1_zip; smt (size_iota size_ge0 size_map).
  move: H13; rewrite !ofassoc_get.
  move=> /assoc_some_onth_mem => [[idx]] /onth_zip_some /= [].

diff --git a/theories/crypto/assumptions/MRPKE.ec b/theories/crypto/assumptions/MRPKE.ec
@@ -1,4 +1,4 @@
-require import AllCore FSet List SmtMap Distr DBool.
+require import AllCore FSet List FMap Distr DBool.
 
 (*******************************************)
 (* Multirecipient PKE *)

diff --git a/theories/crypto/assumptions/ODH.ec b/theories/crypto/assumptions/ODH.ec
@@ -1,4 +1,4 @@
-require import DBool SmtMap FSet DList Int List.
+require import DBool FMap FSet DList Int List.
 require (****) Group.
 
 (* Multiple Oracle-DH *)

diff --git a/theories/crypto/assumptions/PKSMK.ec b/theories/crypto/assumptions/PKSMK.ec
@@ -1,4 +1,4 @@
-require import AllCore Distr DInterval FSet List SmtMap.
+require import AllCore Distr DInterval FSet List FMap.
 require PROM PlugAndPray.
 
 (***************************************)

diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca
@@ -1,4 +1,4 @@
-require import AllCore Distr List FSet SmtMap.
+require import AllCore Distr List FSet FMap.
 require import Dexcepted.
 require (*--*) PRP.
 (*---*) import RField StdOrder.RealOrder.

diff --git a/theories/crypto/ske/NewSKE.eca b/theories/crypto/ske/NewSKE.eca
@@ -1,4 +1,4 @@
-require import Bool FSet SmtMap.
+require import Bool FSet FMap.
 
 type key, plain, cipher.