Merge pull request #2 from fdupress/merge-infinite-arrays

Rename SmtMap to FMap
MM45 · Sep 25, 2024 · 9e5bb27 · 9e5bb27
2 parents 02164e5 + 9fd0d65
commit 9e5bb27
Show file tree

Hide file tree

Showing 12 changed files with 12 additions and 12 deletions.
diff --git a/proofs/acai/EUFRMA_Interactive_Equiv.ec b/proofs/acai/EUFRMA_Interactive_Equiv.ec
@@ -1,4 +1,4 @@
-require import AllCore List Distr SmtMap.
+require import AllCore List Distr FMap.
 require (*--*) DigitalSignatures PROM.
 
 (* -- Types -- *)

diff --git a/proofs/acai/FL_XMSS_TW.ec b/proofs/acai/FL_XMSS_TW.ec
@@ -1,6 +1,6 @@
 (* --- Require/Import --- *)
 (* -- Built-In (Standard Library) -- *)
-require import AllCore List Distr DList IntDiv RealExp StdOrder SmtMap BitEncoding FinType.
+require import AllCore List Distr DList IntDiv RealExp StdOrder FMap BitEncoding FinType.
 require (*--*) Word Subtype.
 (*---*) import RField IntOrder RealOrder BS2Int.
 

diff --git a/proofs/acai/HashThenSign.eca b/proofs/acai/HashThenSign.eca
@@ -1,6 +1,6 @@
 (* --- Require/Import --- *)
 (* -- Built-In (Standard Library) -- *)
-require import AllCore List Distr DList IntDiv RealExp StdOrder SmtMap BitEncoding FinType.
+require import AllCore List Distr DList IntDiv RealExp StdOrder FMap BitEncoding FinType.
 require (*--*) Word Subtype ROM.
 (*---*) import RField IntOrder RealOrder BS2Int.
 

diff --git a/proofs/acai/KeyedHashFunctions.eca b/proofs/acai/KeyedHashFunctions.eca
@@ -18,7 +18,7 @@
 
 (* --- Require/Import --- *)
 (* -- Built-in (i.e, standard library) -- *)
-require import AllCore StdOrder List Distr DInterval Finite SmtMap.
+require import AllCore StdOrder List Distr DInterval Finite FMap.
 require (*--*) PlugAndPray.
 (*---*) import RField RealOrder.
 

diff --git a/proofs/acai/Reprogramming.ec b/proofs/acai/Reprogramming.ec
@@ -1,4 +1,4 @@
-require import AllCore List Int Distr RealExp SmtMap FinType StdOrder StdBigop.
+require import AllCore List Int Distr RealExp FMap FinType StdOrder StdBigop.
 (*---*) import Bigreal.BRA Bigreal RField RealOrder.
 require (*--*) ROM.
 

diff --git a/proofs/acai/WOTS_TW.ec b/proofs/acai/WOTS_TW.ec
@@ -1,6 +1,6 @@
 (* --- Require/Import --- *)
 (* -- Built-In (Standard Library) -- *)
-require import AllCore List Distr DList DInterval IntDiv RealExp StdOrder SmtMap StdBigop BitEncoding FinType.
+require import AllCore List Distr DList DInterval IntDiv RealExp StdOrder FMap StdBigop BitEncoding FinType.
 require (*--*) Word Subtype.
 (*---*) import RField IntOrder RealOrder Bigreal Bigint BIA BS2Int.
 

diff --git a/proofs/fsai/EUFRMA_Interactive_Equiv.ec b/proofs/fsai/EUFRMA_Interactive_Equiv.ec
@@ -1,4 +1,4 @@
-require import AllCore List Distr SmtMap.
+require import AllCore List Distr FMap.
 require (*--*) DigitalSignatures PROM.
 
 (* -- Types -- *)

diff --git a/proofs/fsai/FL_XMSS_TW.ec b/proofs/fsai/FL_XMSS_TW.ec
@@ -1,6 +1,6 @@
 (* --- Require/Import --- *)
 (* -- Built-In (Standard Library) -- *)
-require import AllCore List Distr DList IntDiv RealExp StdOrder SmtMap BitEncoding FinType.
+require import AllCore List Distr DList IntDiv RealExp StdOrder FMap BitEncoding FinType.
 require (*--*) Word Subtype.
 (*---*) import RField IntOrder RealOrder BS2Int.
 

diff --git a/proofs/fsai/HashThenSign.eca b/proofs/fsai/HashThenSign.eca
@@ -1,6 +1,6 @@
 (* --- Require/Import --- *)
 (* -- Built-In (Standard Library) -- *)
-require import AllCore List Distr DList IntDiv RealExp StdOrder SmtMap BitEncoding FinType.
+require import AllCore List Distr DList IntDiv RealExp StdOrder FMap BitEncoding FinType.
 require (*--*) Word Subtype ROM.
 (*---*) import RField IntOrder RealOrder BS2Int.
 

diff --git a/proofs/fsai/KeyedHashFunctions.eca b/proofs/fsai/KeyedHashFunctions.eca
@@ -18,7 +18,7 @@
 
 (* --- Require/Import --- *)
 (* -- Built-in (i.e, standard library) -- *)
-require import AllCore StdOrder List Distr DInterval Finite SmtMap.
+require import AllCore StdOrder List Distr DInterval Finite FMap.
 require (*--*) PlugAndPray.
 (*---*) import RField RealOrder.
 

diff --git a/proofs/fsai/Reprogramming.ec b/proofs/fsai/Reprogramming.ec
@@ -1,4 +1,4 @@
-require import AllCore List Int Distr RealExp SmtMap FinType StdOrder StdBigop.
+require import AllCore List Int Distr RealExp FMap FinType StdOrder StdBigop.
 (*---*) import Bigreal.BRA Bigreal RField RealOrder.
 require (*--*) ROM.
 

diff --git a/proofs/fsai/WOTS_TW.ec b/proofs/fsai/WOTS_TW.ec
@@ -1,6 +1,6 @@
 (* --- Require/Import --- *)
 (* -- Built-In (Standard Library) -- *)
-require import AllCore List Distr DList DInterval IntDiv RealExp StdOrder SmtMap StdBigop BitEncoding FinType.
+require import AllCore List Distr DList DInterval IntDiv RealExp StdOrder FMap StdBigop BitEncoding FinType.
 require (*--*) Word Subtype.
 (*---*) import RField IntOrder RealOrder Bigreal Bigint BIA BS2Int.