From b7ad2493a1178793dad2f15353bbbdc10ab9fca8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 15 Jul 2025 23:33:47 -0700
Subject: [PATCH 1/4] FStar.*Set: remove some pragmas

---
 ulib/FStar.GSet.fst      | 2 +-
 ulib/FStar.GSet.fsti     | 2 --
 ulib/FStar.GhostSet.fst  | 2 +-
 ulib/FStar.GhostSet.fsti | 2 --
 ulib/FStar.Set.fst       | 2 +-
 ulib/FStar.Set.fsti      | 3 ---
 ulib/FStar.TSet.fst      | 1 -
 ulib/FStar.TSet.fsti     | 4 +---
 8 files changed, 4 insertions(+), 14 deletions(-)

diff --git a/ulib/FStar.GSet.fst b/ulib/FStar.GSet.fst
index e40395eb314..c0f5682d996 100644
--- a/ulib/FStar.GSet.fst
+++ b/ulib/FStar.GSet.fst
@@ -16,7 +16,7 @@
 *)
 module FStar.GSet
 (** Computational sets (on Types): membership is a boolean function *)
-#set-options "--fuel 0 --ifuel 0"
+
 open FStar.FunctionalExtensionality
 module F = FStar.FunctionalExtensionality
 
diff --git a/ulib/FStar.GSet.fsti b/ulib/FStar.GSet.fsti
index 0e3bb4e0a6c..79b6726917e 100644
--- a/ulib/FStar.GSet.fsti
+++ b/ulib/FStar.GSet.fsti
@@ -16,7 +16,6 @@
 *)
 module FStar.GSet
 (** Computational sets (on Types): membership is a boolean function *)
-#set-options "--fuel 0 --ifuel 0"
 
 (*
  * AR: mark it must_erase_for_extraction temporarily until CMI comes in
@@ -116,7 +115,6 @@ let disjoint_not_in_both (a:Type) (s1:set a) (s2:set a) :
   FStar.Classical.forall_intro f
 
 (* Converting lists to sets *)
-#reset-options //restore fuel usage here
 
 let rec as_set' (#a:Type) (l:list a) : set a = 
   match l with
diff --git a/ulib/FStar.GhostSet.fst b/ulib/FStar.GhostSet.fst
index 1cf3203160a..5c49de28ee4 100644
--- a/ulib/FStar.GhostSet.fst
+++ b/ulib/FStar.GhostSet.fst
@@ -16,7 +16,7 @@
 *)
 module FStar.GhostSet
 (** Ghost computational sets: membership is a ghost boolean function *)
-#set-options "--fuel 0 --ifuel 0"
+
 open FStar.FunctionalExtensionality
 module F = FStar.FunctionalExtensionality
 
diff --git a/ulib/FStar.GhostSet.fsti b/ulib/FStar.GhostSet.fsti
index c55c509bac3..6789e252804 100644
--- a/ulib/FStar.GhostSet.fsti
+++ b/ulib/FStar.GhostSet.fsti
@@ -16,7 +16,6 @@
 *)
 module FStar.GhostSet
 (** Ghost computational sets: membership is a ghost boolean function *)
-#set-options "--fuel 0 --ifuel 0"
 
 [@@must_erase_for_extraction; erasable]
 val set (a: Type u#a) : Type u#a
@@ -115,7 +114,6 @@ let disjoint_not_in_both (a:Type) (s1:set a) (s2:set a) :
   FStar.Classical.forall_intro f
 
 (* Converting lists to sets *)
-#reset-options //restore fuel usage here
 
 let rec as_set' (#a:Type) (f:decide_eq a) (l:list a) : set a = 
   match l with
diff --git a/ulib/FStar.Set.fst b/ulib/FStar.Set.fst
index f9703a08702..290c60abf22 100644
--- a/ulib/FStar.Set.fst
+++ b/ulib/FStar.Set.fst
@@ -16,7 +16,7 @@
 *)
 module FStar.Set
 (** Computational sets (on eqtypes): membership is a boolean function *)
-#set-options "--fuel 0 --ifuel 0"
+
 open FStar.FunctionalExtensionality
 module F = FStar.FunctionalExtensionality
 
diff --git a/ulib/FStar.Set.fsti b/ulib/FStar.Set.fsti
index 99992e2a0d9..4da1b2173bf 100644
--- a/ulib/FStar.Set.fsti
+++ b/ulib/FStar.Set.fsti
@@ -17,7 +17,6 @@
 
 module FStar.Set
 (** Computational sets (on eqtypes): membership is a boolean function *)
-#set-options "--fuel 0 --ifuel 0"
 
 val set (a:eqtype)
   : Type0
@@ -120,8 +119,6 @@ val disjoint_not_in_both (a:eqtype) (s1:set a) (s2:set a)
 
 (* Converting lists to sets *)
 
-(* WHY IS THIS HERE? It is not strictly part of the interface *)
-#reset-options //restore fuel usage here
 let rec as_set' (#a:eqtype) (l:list a) : set a =
   match l with
   | [] -> empty
diff --git a/ulib/FStar.TSet.fst b/ulib/FStar.TSet.fst
index 5888d616d65..0bc967b15b8 100644
--- a/ulib/FStar.TSet.fst
+++ b/ulib/FStar.TSet.fst
@@ -17,7 +17,6 @@
 (** Propositional sets (on any types): membership is a predicate *)
 module FStar.TSet
 
-#set-options "--fuel 0 --ifuel 0"
 module F = FStar.FunctionalExtensionality
 
 (*
diff --git a/ulib/FStar.TSet.fsti b/ulib/FStar.TSet.fsti
index 26535a454f9..62ab3ee3fec 100644
--- a/ulib/FStar.TSet.fsti
+++ b/ulib/FStar.TSet.fsti
@@ -17,8 +17,6 @@
 (** Propositional sets (on any types): membership is a predicate *)
 module FStar.TSet
 
-#set-options "--fuel 0 --ifuel 0"
-
 (*
  * AR: mark it must_erase_for_extraction temporarily until CMI comes in
  *)
@@ -120,7 +118,7 @@ val lemma_mem_map (#a:Type) (#b:Type) (f:(a -> Tot b)) (s:set a) (x:b)
   :Lemma ((exists (y:a). {:pattern (mem y s)} mem y s /\ x == f y) <==> mem x (map f s))
          [SMTPat (mem x (map f s))]
 
-#reset-options
+// #reset-options
 let rec as_set' (#a:Type) (l:list a) : Tot (set a) =
   match l with
   | [] -> empty

From f58cdec28ecd3dfdb7a227d969aaade8fed90464 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 16 Jul 2025 00:23:49 -0700
Subject: [PATCH 2/4] Introduce @@admitted

---
 src/parser/FStarC.Parser.Const.fst        |  1 +
 src/tosyntax/FStarC.ToSyntax.ToSyntax.fst | 14 ++++++++++----
 ulib/FStar.Attributes.fsti                |  4 ++++
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/parser/FStarC.Parser.Const.fst b/src/parser/FStarC.Parser.Const.fst
index c41a423c44f..37a3eafeaa4 100644
--- a/src/parser/FStarC.Parser.Const.fst
+++ b/src/parser/FStarC.Parser.Const.fst
@@ -374,6 +374,7 @@ let no_auto_projectors_decls_attr = attr "no_auto_projectors_decls"
 let no_auto_projectors_attr = attr "no_auto_projectors"
 let no_subtping_attr_lid = attr "no_subtyping"
 let admit_termination_lid = attr "admit_termination"
+let admitted_lid = attr "admitted"
 let unrefine_binder_attr = pconst "unrefine"
 let do_not_unrefine_attr = pconst "do_not_unrefine"
 let desugar_of_variant_record_lid = attr "desugar_of_variant_record"
diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst
index 5b2e9096796..e65ea964d0e 100644
--- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst
@@ -3697,7 +3697,7 @@ and desugar_redefine_effect env d d_attrs trans_qual quals eff_name eff_binders
     env, [se]
 
 
-and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) =
+and desugar_decl_maybe_fail_attr env (d: decl) (attrs : list S.term) : (env_t & sigelts) =
   let no_fail_attrs (ats : list S.term) : list S.term =
       List.filter (fun at -> Option.isNone (get_fail_attr1 false at)) ats
   in
@@ -3706,8 +3706,6 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) =
    * If it does, check that the errors match as we normally do.
    * If it doesn't fail, leave it alone! The typechecker will check the failure. *)
   let env, sigelts =
-    let attrs = List.map (desugar_term env) d.attrs in
-    let attrs = U.deduplicate_terms attrs in
     match get_fail_attr false attrs with
     | Some (expected_errs, err_rng, lax) ->
       // The `fail` attribute behaves
@@ -3771,7 +3769,14 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) =
 
 and desugar_decl env (d:decl) :(env_t & sigelts) =
   FStarC.GenSym.reset_gensym ();
-  let env, ses = desugar_decl_maybe_fail_attr env d in
+  let attrs = List.map (desugar_term env) d.attrs in
+  let attrs = U.deduplicate_terms attrs in
+  let env, ses = desugar_decl_maybe_fail_attr env d attrs in
+  let ses =
+    if U.has_attribute attrs Const.admitted_lid
+    then ses |> List.map (fun se -> { se with sigmeta = { se.sigmeta with sigmeta_admit = true } })
+    else ses
+  in
   env, ses |> List.map generalize_annotated_univs
 
 and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) =
@@ -4319,6 +4324,7 @@ and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) =
         let quals = d'.quals @ d.quals in
         let attrs = d'.attrs @ d.attrs in
         desugar_decl_maybe_fail_attr env { d' with quals; attrs; drange=d.drange; interleaved=d.interleaved }
+           (attrs |> List.map (desugar_term env) |> U.deduplicate_terms)
   )
 
   | DeclToBeDesugared tbs -> (
diff --git a/ulib/FStar.Attributes.fsti b/ulib/FStar.Attributes.fsti
index b36c911124b..dbca99c1f7d 100644
--- a/ulib/FStar.Attributes.fsti
+++ b/ulib/FStar.Attributes.fsti
@@ -413,6 +413,10 @@ val no_auto_projectors_decls : unit
 *)
 val no_subtyping : unit
 
+(* This can be attached to a top-level declaration to admit its verification
+   conditions. *)
+val admitted : unit
+
 (* This can be attached to a recursive definition to admit its proof
    of termination (but nothing else). *)
 val admit_termination : unit

From b04f3c89b94a339e01fbbbc8f0f588816fe6f179 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 15 Jul 2025 23:41:58 -0700
Subject: [PATCH 3/4] Machine integers: use @@admitted for the unsafe cast

This avoids having a pragma in the interface.

Also tidy up fuel usage/pragmas in these files.
---
 .scripts/FStar.IntN.fstip  | 11 +++++------
 .scripts/FStar.UIntN.fstip | 14 +++++---------
 .scripts/mk_int.sh         |  1 +
 ulib/FStar.Int128.fsti     | 11 +++++------
 ulib/FStar.Int16.fsti      | 11 +++++------
 ulib/FStar.Int32.fsti      | 11 +++++------
 ulib/FStar.Int64.fsti      | 11 +++++------
 ulib/FStar.Int8.fsti       | 11 +++++------
 ulib/FStar.UInt16.fsti     | 14 +++++---------
 ulib/FStar.UInt32.fsti     | 14 +++++---------
 ulib/FStar.UInt64.fsti     | 14 +++++---------
 ulib/FStar.UInt8.fsti      | 15 ++++++---------
 12 files changed, 57 insertions(+), 81 deletions(-)

diff --git a/.scripts/FStar.IntN.fstip b/.scripts/FStar.IntN.fstip
index 323414b4de6..a00957179bc 100644
--- a/.scripts/FStar.IntN.fstip
+++ b/.scripts/FStar.IntN.fstip
@@ -1,8 +1,6 @@
 open FStar.Int
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (* NOTE: anything that you fix/update here should be reflected in [FStar.UIntN.fstp], which is mostly
  * a copy-paste of this module. *)
 
@@ -118,6 +116,7 @@ unfold let ( >=^ ) = gte
 unfold let ( <^ )  = lt
 unfold let ( <=^ ) = lte
 
+#push-options "--fuel 0 --ifuel 0"
 inline_for_extraction
 let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
   let mask = a >>>^ UInt32.uint_to_t (n - 1) in
@@ -136,6 +135,7 @@ let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
     UInt.lemma_lognot_value #n (to_uint (v a))
     end;
   (a ^^ mask) -^ mask
+#pop-options
 
 (* To input / output constants *)
 (* .. in decimal representation *)
@@ -143,7 +143,6 @@ val to_string: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -151,8 +150,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __int_to_t (x:int) : Tot t
-    = int_to_t x
-#reset-options
+let __int_to_t (x:int) : t =
+  int_to_t x
diff --git a/.scripts/FStar.UIntN.fstip b/.scripts/FStar.UIntN.fstip
index e95d5b6fa03..6cc9ab73d14 100644
--- a/.scripts/FStar.UIntN.fstip
+++ b/.scripts/FStar.UIntN.fstip
@@ -22,8 +22,6 @@
 open FStar.UInt
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (** Abstract type of machine integers, with an underlying
     representation using a bounded mathematical integer *)
 new val t : eqtype
@@ -227,8 +225,6 @@ let minus (a:t) = add_mod (lognot a) (uint_to_t 1)
 inline_for_extraction
 let n_minus_one = UInt32.uint_to_t (n - 1)
 
-#set-options "--z3rlimit 80 --fuel 1"
-
 (** A constant-time way to compute the equality of
     two machine integers.
 
@@ -236,6 +232,7 @@ let n_minus_one = UInt32.uint_to_t (n - 1)
 
     Note, the branching on [a=b] is just for proof-purposes.
   *)
+#push-options "--z3rlimit 80 --fuel 1"
 [@ CNoInline ]
 let eq_mask (a:t) (b:t)
   : Pure t
@@ -294,7 +291,7 @@ let gte_mask (a:t) (b:t)
     lemma_msb_gte (v x) (v y);
     lemma_msb_gte (v y) (v x);
     c
-#reset-options
+#pop-options
 
 (*** Infix notations *)
 unfold let ( +^ )  = add
@@ -332,7 +329,6 @@ val to_string_hex_pad: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -340,8 +336,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __uint_to_t (x:int) : Tot t
-    = uint_to_t x
-#reset-options
+let __uint_to_t (x:int) : t =
+  uint_to_t x
diff --git a/.scripts/mk_int.sh b/.scripts/mk_int.sh
index 8f8fe406b07..be23cc7ecc5 100755
--- a/.scripts/mk_int.sh
+++ b/.scripts/mk_int.sh
@@ -116,6 +116,7 @@ unfold let n = $i
 EOF
   cat $D/FStar.UIntN.fstip >> $f
   if [ $i -eq 8 ]; then
+    echo >> $f
     echo "unfold inline_for_extraction type byte = t" >> $f
   fi
   if [ $i -eq 128 ]; then
diff --git a/ulib/FStar.Int128.fsti b/ulib/FStar.Int128.fsti
index 9dbfa9f8428..539cf4616ea 100644
--- a/ulib/FStar.Int128.fsti
+++ b/ulib/FStar.Int128.fsti
@@ -22,8 +22,6 @@ unfold let n = 128
 open FStar.Int
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (* NOTE: anything that you fix/update here should be reflected in [FStar.UIntN.fstp], which is mostly
  * a copy-paste of this module. *)
 
@@ -139,6 +137,7 @@ unfold let ( >=^ ) = gte
 unfold let ( <^ )  = lt
 unfold let ( <=^ ) = lte
 
+#push-options "--fuel 0 --ifuel 0"
 inline_for_extraction
 let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
   let mask = a >>>^ UInt32.uint_to_t (n - 1) in
@@ -157,6 +156,7 @@ let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
     UInt.lemma_lognot_value #n (to_uint (v a))
     end;
   (a ^^ mask) -^ mask
+#pop-options
 
 (* To input / output constants *)
 (* .. in decimal representation *)
@@ -164,7 +164,6 @@ val to_string: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -172,11 +171,11 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __int_to_t (x:int) : Tot t
-    = int_to_t x
-#reset-options
+let __int_to_t (x:int) : t =
+  int_to_t x
 
 val mul_wide: a:Int64.t -> b:Int64.t -> Pure t
   (requires True)
diff --git a/ulib/FStar.Int16.fsti b/ulib/FStar.Int16.fsti
index 6b3de25bf8c..786d949f67e 100644
--- a/ulib/FStar.Int16.fsti
+++ b/ulib/FStar.Int16.fsti
@@ -22,8 +22,6 @@ unfold let n = 16
 open FStar.Int
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (* NOTE: anything that you fix/update here should be reflected in [FStar.UIntN.fstp], which is mostly
  * a copy-paste of this module. *)
 
@@ -139,6 +137,7 @@ unfold let ( >=^ ) = gte
 unfold let ( <^ )  = lt
 unfold let ( <=^ ) = lte
 
+#push-options "--fuel 0 --ifuel 0"
 inline_for_extraction
 let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
   let mask = a >>>^ UInt32.uint_to_t (n - 1) in
@@ -157,6 +156,7 @@ let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
     UInt.lemma_lognot_value #n (to_uint (v a))
     end;
   (a ^^ mask) -^ mask
+#pop-options
 
 (* To input / output constants *)
 (* .. in decimal representation *)
@@ -164,7 +164,6 @@ val to_string: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -172,8 +171,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __int_to_t (x:int) : Tot t
-    = int_to_t x
-#reset-options
+let __int_to_t (x:int) : t =
+  int_to_t x
diff --git a/ulib/FStar.Int32.fsti b/ulib/FStar.Int32.fsti
index cda2be1e473..ceddc4b393a 100644
--- a/ulib/FStar.Int32.fsti
+++ b/ulib/FStar.Int32.fsti
@@ -22,8 +22,6 @@ unfold let n = 32
 open FStar.Int
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (* NOTE: anything that you fix/update here should be reflected in [FStar.UIntN.fstp], which is mostly
  * a copy-paste of this module. *)
 
@@ -139,6 +137,7 @@ unfold let ( >=^ ) = gte
 unfold let ( <^ )  = lt
 unfold let ( <=^ ) = lte
 
+#push-options "--fuel 0 --ifuel 0"
 inline_for_extraction
 let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
   let mask = a >>>^ UInt32.uint_to_t (n - 1) in
@@ -157,6 +156,7 @@ let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
     UInt.lemma_lognot_value #n (to_uint (v a))
     end;
   (a ^^ mask) -^ mask
+#pop-options
 
 (* To input / output constants *)
 (* .. in decimal representation *)
@@ -164,7 +164,6 @@ val to_string: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -172,8 +171,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __int_to_t (x:int) : Tot t
-    = int_to_t x
-#reset-options
+let __int_to_t (x:int) : t =
+  int_to_t x
diff --git a/ulib/FStar.Int64.fsti b/ulib/FStar.Int64.fsti
index d9e84126856..c2682c99af7 100644
--- a/ulib/FStar.Int64.fsti
+++ b/ulib/FStar.Int64.fsti
@@ -22,8 +22,6 @@ unfold let n = 64
 open FStar.Int
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (* NOTE: anything that you fix/update here should be reflected in [FStar.UIntN.fstp], which is mostly
  * a copy-paste of this module. *)
 
@@ -139,6 +137,7 @@ unfold let ( >=^ ) = gte
 unfold let ( <^ )  = lt
 unfold let ( <=^ ) = lte
 
+#push-options "--fuel 0 --ifuel 0"
 inline_for_extraction
 let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
   let mask = a >>>^ UInt32.uint_to_t (n - 1) in
@@ -157,6 +156,7 @@ let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
     UInt.lemma_lognot_value #n (to_uint (v a))
     end;
   (a ^^ mask) -^ mask
+#pop-options
 
 (* To input / output constants *)
 (* .. in decimal representation *)
@@ -164,7 +164,6 @@ val to_string: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -172,8 +171,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __int_to_t (x:int) : Tot t
-    = int_to_t x
-#reset-options
+let __int_to_t (x:int) : t =
+  int_to_t x
diff --git a/ulib/FStar.Int8.fsti b/ulib/FStar.Int8.fsti
index 5cfc4d010a9..65be4ebef63 100644
--- a/ulib/FStar.Int8.fsti
+++ b/ulib/FStar.Int8.fsti
@@ -22,8 +22,6 @@ unfold let n = 8
 open FStar.Int
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (* NOTE: anything that you fix/update here should be reflected in [FStar.UIntN.fstp], which is mostly
  * a copy-paste of this module. *)
 
@@ -139,6 +137,7 @@ unfold let ( >=^ ) = gte
 unfold let ( <^ )  = lt
 unfold let ( <=^ ) = lte
 
+#push-options "--fuel 0 --ifuel 0"
 inline_for_extraction
 let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
   let mask = a >>>^ UInt32.uint_to_t (n - 1) in
@@ -157,6 +156,7 @@ let ct_abs (a:t{min_int n < v a}) : Tot (b:t{v b = abs (v a)}) =
     UInt.lemma_lognot_value #n (to_uint (v a))
     end;
   (a ^^ mask) -^ mask
+#pop-options
 
 (* To input / output constants *)
 (* .. in decimal representation *)
@@ -164,7 +164,6 @@ val to_string: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -172,8 +171,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __int_to_t (x:int) : Tot t
-    = int_to_t x
-#reset-options
+let __int_to_t (x:int) : t =
+  int_to_t x
diff --git a/ulib/FStar.UInt16.fsti b/ulib/FStar.UInt16.fsti
index 077c69133ab..2fc83a35c2d 100644
--- a/ulib/FStar.UInt16.fsti
+++ b/ulib/FStar.UInt16.fsti
@@ -43,8 +43,6 @@ unfold let n = 16
 open FStar.UInt
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (** Abstract type of machine integers, with an underlying
     representation using a bounded mathematical integer *)
 new val t : eqtype
@@ -248,8 +246,6 @@ let minus (a:t) = add_mod (lognot a) (uint_to_t 1)
 inline_for_extraction
 let n_minus_one = UInt32.uint_to_t (n - 1)
 
-#set-options "--z3rlimit 80 --fuel 1"
-
 (** A constant-time way to compute the equality of
     two machine integers.
 
@@ -257,6 +253,7 @@ let n_minus_one = UInt32.uint_to_t (n - 1)
 
     Note, the branching on [a=b] is just for proof-purposes.
   *)
+#push-options "--z3rlimit 80 --fuel 1"
 [@ CNoInline ]
 let eq_mask (a:t) (b:t)
   : Pure t
@@ -315,7 +312,7 @@ let gte_mask (a:t) (b:t)
     lemma_msb_gte (v x) (v y);
     lemma_msb_gte (v y) (v x);
     c
-#reset-options
+#pop-options
 
 (*** Infix notations *)
 unfold let ( +^ )  = add
@@ -353,7 +350,6 @@ val to_string_hex_pad: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -361,8 +357,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __uint_to_t (x:int) : Tot t
-    = uint_to_t x
-#reset-options
+let __uint_to_t (x:int) : t =
+  uint_to_t x
diff --git a/ulib/FStar.UInt32.fsti b/ulib/FStar.UInt32.fsti
index 2f737e0015a..19dd1f2626b 100644
--- a/ulib/FStar.UInt32.fsti
+++ b/ulib/FStar.UInt32.fsti
@@ -43,8 +43,6 @@ unfold let n = 32
 open FStar.UInt
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (** Abstract type of machine integers, with an underlying
     representation using a bounded mathematical integer *)
 new val t : eqtype
@@ -248,8 +246,6 @@ let minus (a:t) = add_mod (lognot a) (uint_to_t 1)
 inline_for_extraction
 let n_minus_one = uint_to_t (n - 1)
 
-#set-options "--z3rlimit 80 --fuel 1"
-
 (** A constant-time way to compute the equality of
     two machine integers.
 
@@ -257,6 +253,7 @@ let n_minus_one = uint_to_t (n - 1)
 
     Note, the branching on [a=b] is just for proof-purposes.
   *)
+#push-options "--z3rlimit 80 --fuel 1"
 [@ CNoInline ]
 let eq_mask (a:t) (b:t)
   : Pure t
@@ -315,7 +312,7 @@ let gte_mask (a:t) (b:t)
     lemma_msb_gte (v x) (v y);
     lemma_msb_gte (v y) (v x);
     c
-#reset-options
+#pop-options
 
 (*** Infix notations *)
 unfold let ( +^ )  = add
@@ -353,7 +350,6 @@ val to_string_hex_pad: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -361,8 +357,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __uint_to_t (x:int) : Tot t
-    = uint_to_t x
-#reset-options
+let __uint_to_t (x:int) : t =
+  uint_to_t x
diff --git a/ulib/FStar.UInt64.fsti b/ulib/FStar.UInt64.fsti
index 82871a8ef0e..59d8e570194 100644
--- a/ulib/FStar.UInt64.fsti
+++ b/ulib/FStar.UInt64.fsti
@@ -43,8 +43,6 @@ unfold let n = 64
 open FStar.UInt
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (** Abstract type of machine integers, with an underlying
     representation using a bounded mathematical integer *)
 new val t : eqtype
@@ -248,8 +246,6 @@ let minus (a:t) = add_mod (lognot a) (uint_to_t 1)
 inline_for_extraction
 let n_minus_one = UInt32.uint_to_t (n - 1)
 
-#set-options "--z3rlimit 80 --fuel 1"
-
 (** A constant-time way to compute the equality of
     two machine integers.
 
@@ -257,6 +253,7 @@ let n_minus_one = UInt32.uint_to_t (n - 1)
 
     Note, the branching on [a=b] is just for proof-purposes.
   *)
+#push-options "--z3rlimit 80 --fuel 1"
 [@ CNoInline ]
 let eq_mask (a:t) (b:t)
   : Pure t
@@ -315,7 +312,7 @@ let gte_mask (a:t) (b:t)
     lemma_msb_gte (v x) (v y);
     lemma_msb_gte (v y) (v x);
     c
-#reset-options
+#pop-options
 
 (*** Infix notations *)
 unfold let ( +^ )  = add
@@ -353,7 +350,6 @@ val to_string_hex_pad: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -361,8 +357,8 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __uint_to_t (x:int) : Tot t
-    = uint_to_t x
-#reset-options
+let __uint_to_t (x:int) : t =
+  uint_to_t x
diff --git a/ulib/FStar.UInt8.fsti b/ulib/FStar.UInt8.fsti
index 498df8fb061..e3266535ee7 100644
--- a/ulib/FStar.UInt8.fsti
+++ b/ulib/FStar.UInt8.fsti
@@ -43,8 +43,6 @@ unfold let n = 8
 open FStar.UInt
 open FStar.Mul
 
-#set-options "--fuel 0 --ifuel 0"
-
 (** Abstract type of machine integers, with an underlying
     representation using a bounded mathematical integer *)
 new val t : eqtype
@@ -248,8 +246,6 @@ let minus (a:t) = add_mod (lognot a) (uint_to_t 1)
 inline_for_extraction
 let n_minus_one = UInt32.uint_to_t (n - 1)
 
-#set-options "--z3rlimit 80 --fuel 1"
-
 (** A constant-time way to compute the equality of
     two machine integers.
 
@@ -257,6 +253,7 @@ let n_minus_one = UInt32.uint_to_t (n - 1)
 
     Note, the branching on [a=b] is just for proof-purposes.
   *)
+#push-options "--z3rlimit 80 --fuel 1"
 [@ CNoInline ]
 let eq_mask (a:t) (b:t)
   : Pure t
@@ -315,7 +312,7 @@ let gte_mask (a:t) (b:t)
     lemma_msb_gte (v x) (v y);
     lemma_msb_gte (v y) (v x);
     c
-#reset-options
+#pop-options
 
 (*** Infix notations *)
 unfold let ( +^ )  = add
@@ -353,7 +350,6 @@ val to_string_hex_pad: t -> Tot string
 
 val of_string: string -> Tot t
 
-#set-options "--admit_smt_queries true"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
@@ -361,9 +357,10 @@ val of_string: string -> Tot t
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
+[@@admitted]
 private
 unfold
-let __uint_to_t (x:int) : Tot t
-    = uint_to_t x
-#reset-options
+let __uint_to_t (x:int) : t =
+  uint_to_t x
+
 unfold inline_for_extraction type byte = t

From 808d79b58cdb3219a9b5b642da630bec2c9db79c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 16 Jul 2025 00:43:52 -0700
Subject: [PATCH 4/4] Tweak flaky proof

---
 ulib/FStar.UInt128.fst | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst
index 7dc7aa71551..2d2c4199c18 100644
--- a/ulib/FStar.UInt128.fst
+++ b/ulib/FStar.UInt128.fst
@@ -953,6 +953,7 @@ val u32_product_bound : a:nat{a < pow2 32} -> b:nat{b < pow2 32} ->
 let u32_product_bound a b =
   uint_product_bound #32 a b
 
+#push-options "--z3rlimit 15 --retry 5" // sporadically fails
 let mul32 x y =
   let x0 = u64_mod_32 x in
   let x1 = U64.shift_right x u32_32 in
@@ -979,6 +980,7 @@ let mul32 x y =
   mul32_digits (U64.v x) (U32.v y);
   assert (U64.v x * U32.v y == U64.v x1y' * pow2 32 + U64.v x0y);
   r
+#pop-options
 
 let l32 (x: UInt.uint_t 64) : UInt.uint_t 32 = x % pow2 32
 let h32 (x: UInt.uint_t 64) : UInt.uint_t 32 = x / pow2 32