chore: update F*

Inria-Prosecco · Sep 17, 2024 · 3362b9a · 3362b9a
1 parent ad173bc
commit 3362b9a
Show file tree

Hide file tree

Showing 10 changed files with 16 additions and 17 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/fstar/common/proofs/MLS.Crypto.Derived.Lemmas.fst b/fstar/common/proofs/MLS.Crypto.Derived.Lemmas.fst
@@ -2,7 +2,7 @@ module MLS.Crypto.Derived.Lemmas
 
 open MLS.Crypto.Derived
 
-#push-options "--fuel 0 --ifuel 0"
+#set-options "--fuel 0 --ifuel 0"
 
 val get_mls_label_inj:
   l1:valid_label -> l2:valid_label ->

diff --git a/fstar/common/proofs/MLS.MiscLemmas.fst b/fstar/common/proofs/MLS.MiscLemmas.fst
@@ -3,7 +3,7 @@ module MLS.MiscLemmas
 open FStar.List.Tot
 open Comparse
 
-#push-options "--fuel 1 --ifuel 1"
+#set-options "--fuel 1 --ifuel 1"
 
 val list_for_all_eq:
   #a:eqtype ->

diff --git a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
@@ -9,7 +9,7 @@ open MLS.Crypto.Derived.Lemmas
 open MLS.Symbolic
 open MLS.Result
 
-#push-options "--fuel 0 --ifuel 0"
+#set-options "--fuel 0 --ifuel 0"
 
 (*** Split predicate for SignWithLabel ***)
 

diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst
@@ -5,7 +5,7 @@ open DY.Core
 open MLS.Crypto
 open MLS.Result
 
-#push-options "--fuel 0 --ifuel 0"
+#set-options "--fuel 0 --ifuel 0"
 
 (*** Typeclass instantiation on DY* ***)
 

diff --git a/fstar/treedem/MLS.TreeDEM.Keys.fst b/fstar/treedem/MLS.TreeDEM.Keys.fst
@@ -98,7 +98,6 @@ let ratchet_next_state #bytes #cb st =
     generation = st.generation + 1;
   })
 
-//#push-options "--fuel 1 --ifuel 1"
 val ratchet_get_generation_key:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   st:ratchet_state bytes -> i:nat{st.generation <= i} ->

diff --git a/fstar/treesync/code/MLS.TreeSync.Refined.Operations.fst b/fstar/treesync/code/MLS.TreeSync.Refined.Operations.fst
@@ -14,7 +14,7 @@ open MLS.TreeSync.Invariants.ValidLeaves.Proofs
 open MLS.TreeSync.Refined.Types
 open MLS.Result
 
-#push-options "--fuel 0 --ifuel 0"
+#set-options "--fuel 0 --ifuel 0"
 
 val tree_create:
   #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes ->

diff --git a/hacl-star-snapshot/lib/Lib.IntTypes.fst b/hacl-star-snapshot/lib/Lib.IntTypes.fst
@@ -2,7 +2,7 @@ module Lib.IntTypes
 
 open FStar.Math.Lemmas
 
-#push-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 200"
+#set-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 200"
 
 let pow2_2 _   = assert_norm (pow2 2 = 4)
 let pow2_3 _   = assert_norm (pow2 3 = 8)
@@ -768,6 +768,7 @@ let shift_left #t #l a b =
   | S32  -> Int32.shift_left a b
   | S64  -> Int64.shift_left a b
   | S128 -> Int128.shift_left a b
+#pop-options
 
 #push-options "--max_fuel 1"
 
@@ -1009,6 +1010,7 @@ let conditional_subtract #t #l t' a =
   let a3 = a `sub` pow2_bits in
   logand_lemma mask pow2_bits;
   a3 `add` (mask `logand` pow2_bits)
+#pop-options
 
 #push-options "--z3rlimit 500 --quake 1/25"
 let cast_mod #t #l t' l' a =
@@ -1025,8 +1027,6 @@ let cast_mod #t #l t' l' a =
     end
 #pop-options
 
-#pop-options
-
 [@(strict_on_arguments [0])]
 let div #t x y =
   match t with

diff --git a/hacl-star-snapshot/lib/Lib.IntTypes.fsti b/hacl-star-snapshot/lib/Lib.IntTypes.fsti
@@ -2,7 +2,7 @@ module Lib.IntTypes
 
 open FStar.Mul
 
-#push-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 20"
+#set-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 20"
 
 // Other instances frollow from `FStar.UInt.pow2_values` which is in
 // scope of every module depending on Lib.IntTypes

diff --git a/hacl-star-snapshot/lib/Lib.Vec.Lemmas.fsti b/hacl-star-snapshot/lib/Lib.Vec.Lemmas.fsti
@@ -7,7 +7,7 @@ open Lib.Sequence.Lemmas
 
 module Loops = Lib.LoopCombinators
 
-#push-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 \
+#set-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 \
   --using_facts_from '-* +Prims +FStar.Pervasives +FStar.Math.Lemmas +FStar.Seq \
     +Lib.IntTypes +Lib.Sequence +Lib.Sequence.Lemmas +Lib.LoopCombinators +Lib.Vec.Lemmas'"