chore: update F* (#72)

* chore: update F* * also update Comparse
REPROSEC · Oct 1, 2024 · ac82925 · ac82925
1 parent 652bf22
commit ac82925
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 7 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/src/core/DY.Core.Bytes.fst b/src/core/DY.Core.Bytes.fst
@@ -2173,6 +2173,7 @@ let dh_pk_preserves_publishability tr sk =
 
 /// Lemma for attacker knowledge theorem.
 
+#push-options "--z3rlimit 25"
 val dh_preserves_publishability:
   {|crypto_invariants|} -> tr:trace ->
   sk:bytes -> pk:bytes ->
@@ -2187,6 +2188,7 @@ let dh_preserves_publishability tr sk pk =
   reveal_opaque (`%dh) (dh);
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label
+#pop-options
 
 /// User lemma (dh_pk well-formedness)
 
@@ -2642,6 +2644,7 @@ let kem_pk_preserves_publishability #ci tr sk =
 
 /// Lemma for attacker knowledge theorem.
 
+#push-options "--z3rlimit 25"
 val kem_encap_preserves_publishability:
   {|crypto_invariants|} -> tr:trace ->
   pk:bytes -> nonce:bytes ->
@@ -2660,6 +2663,7 @@ let kem_encap_preserves_publishability #ci tr pk nonce =
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label;
   assert(is_publishable tr (KemSecretShared nonce))
+#pop-options
 
 /// Lemma for attacker knowledge theorem.
 

diff --git a/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst b/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst
@@ -236,7 +236,7 @@ let get_hpke_sk_label_hpke_pk #cu tr sk = ()
 /// It is a bit more complex than `DY.Core.Bytes.bytes_invariant_pk_enc`,
 /// the additional complexity is explained in the comments.
 
-#push-options "--ifuel 2"
+#push-options "--ifuel 2 --z3rlimit 25"
 val bytes_invariant_hpke_enc:
   {|crypto_invariants|} -> {|hpke_crypto_invariants|} ->
   tr:trace ->