From 1fd53141dec2919bb10f477d90478eb58e205e10 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 15 Jul 2025 22:42:45 -0700
Subject: [PATCH 1/5] Interleave: do not interleave pragmas in IDE mode, just
 like batch

We've long ignored the pragmas in an fsti when checking an fst
(https://github.com/FStarLang/FStar/pull/1142). This helps in preventing
tons of confusion when checking an fst file, as otherwise the
rlimit/fuel/ifuel can change under the user's feet as they check a file.

However, in the IDE mode, when the pragma was near the top of the
fsti (more specifically in the first chunk that would be interleaved)
in the fst, this was still being interleaved. This is since when try
to find the relevant decls to interleave from the fsti before the
top-level `module Foo` decl, and that returns the empty set, so they
remaing in the `remaining_iface_vals` which are still returned, but were
unfiltered.

This lead to a long headache just now while noticing a file failing in
the IDE, but that had succeeded repeatedly in batch mode.

Fix this by just filtering out all the pragmas before any kind of
interleaving, which should be more robust.
---
 src/tosyntax/FStarC.ToSyntax.Interleave.fst  | 11 +++++++----
 src/tosyntax/FStarC.ToSyntax.Interleave.fsti | 19 ++++++++++++++-----
 2 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/src/tosyntax/FStarC.ToSyntax.Interleave.fst b/src/tosyntax/FStarC.ToSyntax.Interleave.fst
index 909db1d48bb..f739ea68842 100644
--- a/src/tosyntax/FStarC.ToSyntax.Interleave.fst
+++ b/src/tosyntax/FStarC.ToSyntax.Interleave.fst
@@ -30,6 +30,9 @@ open FStarC.Class.PP
 
 module BU = FStarC.Util
 
+let no_pragmas (iface : list decl) : list decl =
+  List.filter (fun d -> not (Pragma? d.d)) iface
+
 (* Some basic utilities *)
 let id_eq_lid i (l:lident) = (string_of_id i) = (string_of_id (ident_of_lid l))
 
@@ -212,10 +215,6 @@ let rec prefix_with_iface_decls
          rest_iface, iface_hd::take_iface@[impl]
        )
 
-     | Pragma _ ->
-        (* Don't interleave pragmas on interface into implementation *)
-        prefix_with_iface_decls iface_tl impl
-
      | _ ->
        let iface, ds = prefix_with_iface_decls iface_tl impl in
        iface, iface_hd::ds
@@ -353,6 +352,8 @@ let prefix_with_interface_decls mname (impl:decl) : E.withenv (list decl) =
       | None ->
         [impl], env
       | Some iface ->
+        (* Don't interleave pragmas on interface into implementation *)
+        let iface = no_pragmas iface in
         let iface = fixup_interleaved_decls iface in
         let iface, impl = prefix_one_decl mname iface impl in
         let env = E.set_iface_decls env (E.current_module env) iface in
@@ -371,6 +372,8 @@ let interleave_module (a:modul) (expect_complete_modul:bool) : E.withenv modul =
       match E.iface_decls env l with
       | None -> a, env
       | Some iface ->
+        (* Don't interleave pragmas on interface into implementation *)
+        let iface = no_pragmas iface in
         let iface = fixup_interleaved_decls iface in
         let iface, impls =
             List.fold_left
diff --git a/src/tosyntax/FStarC.ToSyntax.Interleave.fsti b/src/tosyntax/FStarC.ToSyntax.Interleave.fsti
index ae97d33cdec..0d309cc8423 100644
--- a/src/tosyntax/FStarC.ToSyntax.Interleave.fsti
+++ b/src/tosyntax/FStarC.ToSyntax.Interleave.fsti
@@ -14,14 +14,23 @@
   limitations under the License.
 *)
 module FStarC.ToSyntax.Interleave
-open FStarC.Effect
+
 open FStarC.Effect
 open FStarC.Ident
 open FStarC.Parser.AST
 module DsEnv = FStarC.Syntax.DsEnv
 
-(* GM: If I don't use the full name, I cannot bootstrap *)
+val initialize_interface
+  (mname : lident)
+  (l : list decl)
+  : DsEnv.withenv unit
+
+val prefix_with_interface_decls
+  (mname: lident)
+  (impl: decl)
+  : DsEnv.withenv (list decl)
 
-val initialize_interface:        lident -> list decl -> DsEnv.withenv unit
-val prefix_with_interface_decls: lident -> decl -> DsEnv.withenv (list decl)
-val interleave_module:           modul -> bool -> DsEnv.withenv modul
+val interleave_module
+  (a : modul)
+  (expect_complete_modul : bool)
+  : DsEnv.withenv modul

From f70467b171b7fab2a20b64e7c9ba2860b0694799 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 2/5] 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 bc3f4540335154c0f1f57808edd48ecbeb922ba8 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 3/5] 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 c7eb13f1bf8157600908eb7a381d4814aa90b46a 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 4/5] 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 29ca465e0934c065d8a34b80ed8e7c18107d0665 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 5/5] 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