Some cleanups

.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,23 +135,23 @@ 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 *)
 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,
 //rather than an expensive verification check.
 //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

.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,15 +225,14 @@ 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.
 
     With inspiration from https://git.zx2c4.com/WireGuard/commit/src/crypto/curve25519-hacl64.h?id=2e60bb395c1f589a398ec606d611132ef9ef764b
 
     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,16 +329,15 @@ 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,
 //rather than an expensive verification check.
 //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

.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

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"

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 -> (

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

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
 

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

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
 

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

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,26 +156,26 @@ 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 *)
 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,
 //rather than an expensive verification check.
 //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)

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,23 +156,23 @@ 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 *)
 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,
 //rather than an expensive verification check.
 //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

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,23 +156,23 @@ 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 *)
 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,
 //rather than an expensive verification check.
 //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