Interleave: do not interleave pragmas in IDE mode, just like batch

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

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

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