Retire [@@must_erase_for_extraction]

examples/Cfg.fst.config.json

@@ -5,5 +5,6 @@
     "--z3version", "4.13.3"
   ],
   "include_dirs": [
+    "crypto"
   ]
 }

examples/crypto/OPLSS.AE.fst

@@ -238,13 +238,15 @@ let keygen () =
   Key ka ke
 
 
+#push-options "--z3rlimit 10"
 /// encrypt:
 ///       We return a cipher, preserve the invariant,
 ///       and extend the log by exactly one entry
 let encrypt k plain =
   let c = CPA.encrypt k.enc plain in
   let t = MAC.mac k.mac c in
   (c, t)
+#pop-options
 
 /// decrypt:
 ///     In the ideal case, we prove it functionally correct and secure

src/typechecker/FStarC.TypeChecker.Env.fst

@@ -945,13 +945,8 @@ let cache_in_fv_tab (tab:SMap.t 'a) (fv:fv) (f:unit -> (bool & 'a)) : 'a =
 let fv_has_erasable_attr env fv =
   let f () =
      let ex, erasable = fv_exists_and_has_attr env fv.fv_name.v Const.erasable_attr in
-     ex,erasable
-     //unfortunately, treating the Const.must_erase_for_extraction_attr
-     //in the same way here as erasable_attr leads to regressions in fragile proofs,
-     //notably in FStar.ModifiesGen, since this expands the class of computation types
-     //that can be promoted from ghost to tot. That in turn results in slightly different
-     //smt encodings, leading to breakages. So, sadly, I'm not including must_erase_for_extraction
-     //here. In any case, must_erase_for_extraction is transitionary and should be removed
+     let ex, must_erase_for_extraction = fv_exists_and_has_attr env fv.fv_name.v Const.must_erase_for_extraction_attr in
+     ex, erasable || must_erase_for_extraction
   in
   cache_in_fv_tab env.erasable_types_tab fv f
 
@@ -1047,12 +1042,21 @@ let rec non_informative env t =
       || fv_eq_lid fv Const.erased_lid
       || fv_has_erasable_attr env fv
     | Tm_app {hd=head} -> non_informative env head
+    | Tm_abs {body} -> non_informative env body
     | Tm_uinst (t, _) -> non_informative env t
     | Tm_arrow {comp=c} ->
       (is_pure_or_ghost_comp c && non_informative env (comp_result c))
       || is_erasable_effect env (comp_effect_name c)
+    | Tm_meta {tm} -> non_informative env tm
     | _ -> false
 
+let rec non_informative_sort t =
+  match (U.unrefine t).n with
+  | Tm_fvar fv when fv_eq_lid fv Const.prop_lid -> true
+  | Tm_arrow {comp=c} -> non_informative_sort (comp_result c)
+  | Tm_meta {tm} -> non_informative_sort tm
+  | _ -> false
+
 let num_effect_indices env name r =
   let sig_t = name |> lookup_effect_lid env |> SS.compress in
   match sig_t.n with

src/typechecker/FStarC.TypeChecker.Env.fsti

@@ -347,7 +347,16 @@ val fv_with_lid_has_attr   : env -> fv_lid:lid -> attr_lid:lid -> bool
 val fv_has_attr            : env -> fv -> attr_lid:lid -> bool
 val fv_has_strict_args     : env -> fv -> option (list int)
 val fv_has_erasable_attr   : env -> fv -> bool
+
+(* `non_informative env t` is true if the type family `t: (... -> Type) is noninformative,
+   i.e., any `x: t ...` can be erased to `()`. *)
 val non_informative        : env -> typ -> bool
+
+(* `non_informative_sort t` is `true` if the type family `t: ... -> Type` only ranges over noninformative types,
+   i.e., any `x: s ...` such that `s ... : t ...` can be erased.
+   (practically, this means that `t` is of the form `... -> prop`) *)
+val non_informative_sort   : typ -> bool
+
 val try_lookup_effect_lid  : env -> lident -> option term
 val lookup_effect_lid      : env -> lident -> term
 val lookup_effect_abbrev   : env -> universes -> lident -> option (binders & comp)

src/typechecker/FStarC.TypeChecker.Normalize.fst

@@ -2774,6 +2774,8 @@ let non_info_norm env t =
   let steps = [UnfoldUntil delta_constant;
                AllowUnboundUniverses;
                EraseUniverses;
+               Primops;
+               Beta; Iota;
                HNF;
                (* We could use Weak too were it not that we need
                 * to descend in the codomain of arrows. *)
@@ -2783,6 +2785,21 @@ let non_info_norm env t =
   in
   non_informative env (normalize steps env t)
 
+let non_info_sort_norm env t =
+  let steps = [UnfoldUntil (Env.delta_depth_of_fv env (S.fvconst PC.prop_lid)); // do not unfold prop
+               AllowUnboundUniverses;
+               EraseUniverses;
+               Primops;
+               Beta; Iota;
+               HNF;
+               (* We could use Weak too were it not that we need
+                * to descend in the codomain of arrows. *)
+               Unascribe;   //remove ascriptions
+               ForExtraction //and refinement types
+               ]
+  in
+  non_informative_sort (normalize steps env t)
+
 (*
  * Ghost T to Pure T promotion
  *

src/typechecker/FStarC.TypeChecker.Normalize.fsti

@@ -35,6 +35,7 @@ val unfold_whnf':         steps -> Env.env -> term -> term
 val unfold_whnf:          Env.env -> term -> term
 val reduce_uvar_solutions:Env.env -> term -> term
 val non_info_norm: Env.env -> term -> bool
+val non_info_sort_norm: Env.env -> term -> bool
 
 (*
  * The maybe versions of ghost_to_pure only promote

src/typechecker/FStarC.TypeChecker.Quals.fst

@@ -199,6 +199,26 @@ let check_sigelt_quals_pre (env:FStarC.TypeChecker.Env.env) se =
         then err []
       | _ -> ()
 
+// A faster under-approximation of non_info_norm.
+// We call this function on every let-binding that has an interface val
+// (while non_info_norm is only called on types),
+// so it needs to be fast and shouldn't unfold too much.
+// The regular non_info_norm doesn't set Weak,
+// which makes the normalizer reduce lets.
+let non_info_norm_weak env t =
+  let steps = [UnfoldUntil delta_constant;
+               AllowUnboundUniverses;
+               EraseUniverses;
+               Primops;
+               Beta; Iota;
+               HNF;
+               Weak;
+               Unascribe;   //remove ascriptions
+               ForExtraction //and refinement types
+               ]
+  in
+  non_informative env (N.normalize steps env t)
+
 let check_erasable env quals (r:Range.range) se =
   let lids = U.lids_of_sigelt se in
   let val_exists =
@@ -221,6 +241,29 @@ let check_erasable env quals (r:Range.range) se =
            text "Mismatch of attributes between declaration and definition.";
            text "Definition is marked `erasable` but the declaration is not.";
          ];
+  if not se_has_erasable_attr && not (Options.ide ()) then begin
+    match se.sigel with
+    | Sig_let {lbs=(false, [lb])} ->
+      let lbname = BU.right lb.lbname in
+      let has_iface_val = match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with
+        | Some iface_decls -> iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v))
+        | None -> false in
+      let val_decl = Env.try_lookup_val_decl env lbname.fv_name.v in
+      if has_iface_val && Some? val_decl then
+        let _, body, _ = U.abs_formals lb.lbdef in
+          let Some ((us, t), _) = val_decl in
+        let known_to_be_erasable =
+          let env = Env.push_univ_vars env us in
+          N.non_info_sort_norm env t in
+        if not known_to_be_erasable && non_info_norm_weak env body then
+          log_issue lbname Error_MustEraseMissing [
+            text (BU.format1 "Values of type `%s` will be erased during extraction, \
+                  but its interface hides this fact." (show lbname));
+            text (BU.format1 "Add the `erasable` \
+                  attribute to the `val %s` declaration for this symbol in the interface" (show lbname));
+          ]
+    | _ -> ()
+  end;
   if se_has_erasable_attr
   then begin
     match se.sigel with
@@ -259,47 +302,6 @@ let check_erasable env quals (r:Range.range) se =
         ]
   end
 
-(*
- *  Given `val t : Type` in an interface
- *  and   `let t = e`    in the corresponding implementation
- *  The val declaration should contains the `must_erase_for_extraction` attribute
- *  if and only if `e` is a type that's non-informative (e..g., unit, t -> unit, etc.)
- *)
-let check_must_erase_attribute env se =
-  if Options.ide() then () else
-  match se.sigel with
-  | Sig_let {lbs; lids=l} ->
-    begin match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with
-     | None ->
-       ()
-
-     | Some iface_decls ->
-       snd lbs |> List.iter (fun lb ->
-           let lbname = BU.right lb.lbname in
-           let has_iface_val =
-               iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v))
-           in
-           if has_iface_val
-           then
-               let must_erase = TcUtil.must_erase_for_extraction env lb.lbdef in
-               let has_attr = Env.fv_has_attr env lbname C.must_erase_for_extraction_attr in
-               if must_erase && not has_attr
-               then log_issue lbname Error_MustEraseMissing [
-                        text (BU.format1 "Values of type `%s` will be erased during extraction, \
-                               but its interface hides this fact." (show lbname));
-                        text (BU.format1 "Add the `must_erase_for_extraction` \
-                               attribute to the `val %s` declaration for this symbol in the interface" (show lbname));
-                      ]
-               else if has_attr && not must_erase
-               then log_issue lbname Error_MustEraseMissing [
-                        text (BU.format1 "Values of type `%s` cannot be erased during extraction, \
-                               but the `must_erase_for_extraction` attribute claims that it can."
-                               (show lbname));
-                        text "Please remove the attribute.";
-                      ])
-  end
-  | _ -> ()
-
 let check_typeclass_instance_attribute env (rng:Range.range) se =
   let is_tc_instance =
       se.sigattrs |> BU.for_some
@@ -354,6 +356,5 @@ let check_sigelt_quals_post env se =
   let quals = se.sigquals in
   let r = se.sigrng in
   check_erasable env quals r se;
-  check_must_erase_attribute env se;
   check_typeclass_instance_attribute env r se;
   ()

src/typechecker/FStarC.TypeChecker.Quals.fsti

@@ -28,7 +28,6 @@ after the function is typechecked.
 
 Currently, the only things that must be checked after the function is typechecked are:
 - The erasable attribute, since the defn must be elaborated. See #3253.
-- The must_erase attribute
 - The instance attribute for typeclasses
 *)
 

src/typechecker/FStarC.TypeChecker.Util.fst

@@ -3251,40 +3251,9 @@ let maybe_add_implicit_binders (env:env) (bs:binders) : binders =
 
 
 let must_erase_for_extraction (g:env) (t:typ) =
-    let rec descend env t = //t is expected to b in WHNF
-      match (SS.compress t).n with
-      | Tm_arrow _ ->
-           let bs, c = U.arrow_formals_comp t in
-           let env = FStarC.TypeChecker.Env.push_binders env bs in
-           (Env.is_erasable_effect env (U.comp_effect_name c))  //includes GHOST
-           || (U.is_pure_or_ghost_comp c && aux env (U.comp_result c))
-      | Tm_refine {b={sort=t}} ->
-           aux env t
-      | Tm_app {hd=head}
-      | Tm_uinst (head, _) ->
-           descend env head
-      | Tm_fvar fv ->
-           //special treatment for must_erase_for_extraction here
-           //See Env.type_is_erasable for more explanations
-           Env.fv_has_attr env fv C.must_erase_for_extraction_attr
-      | _ -> false
-    and aux env t =
-        let t = N.normalize [Env.Primops;
-                             Env.Weak;
-                             Env.HNF;
-                             Env.UnfoldUntil delta_constant;
-                             Env.Beta;
-                             Env.AllowUnboundUniverses;
-                             Env.Zeta;
-                             Env.Iota;
-                             Env.Unascribe] env t in
-//        debug g (fun () -> BU.print1 "aux %s\n" (show t));
-        let res = Env.non_informative env t || descend env t in
-        if !dbg_Extraction
-        then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t);
-        res
-    in
-    aux g t
+  let res = N.non_info_norm g t in
+  if !dbg_Extraction then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t);
+  res
 
 let effect_extraction_mode env l =
   l |> Env.norm_eff_name env

tests/micro-benchmarks/MustEraseForExtraction.fst

@@ -17,7 +17,8 @@ module MustEraseForExtraction
 [@@(expect_failure [318])]
 let t1 = unit
 
+[@@erasable]
 let t2 = unit
 
-[@@(expect_failure [318])]
+[@@(expect_failure [162])]
 let t3 = bool

tests/micro-benchmarks/MustEraseForExtraction.fsti

@@ -17,8 +17,8 @@ module MustEraseForExtraction
 
 val t1 : Type0
 
-[@@must_erase_for_extraction]
+[@@erasable]
 val t2 : Type0
 
-[@@must_erase_for_extraction]
+[@@erasable]
 val t3 : Type0

tests/tactics/Postprocess.fst.output.expected

@@ -482,11 +482,11 @@ in
 [@ ]
 visible let  apply_feq_lem  : ($f:(uu___:a@1:(Tm_unknown) -> Tot b@1:(Tm_unknown)) -> $g:(uu___:a@2:(Tm_unknown) -> Tot b@2:(Tm_unknown)) -> Lemma (unit)) = (fun $f $g -> (congruence_fun f@1:(Tm_unknown) g@0:(Tm_unknown) ()))
 [@ ]
-visible let  fext  : (uu___:unit -> Tac (unit)) = (fun uu___ -> let  uu___#1096  : unit = (apply_lemma `(apply_feq_lem)[])
+visible let  fext  : (uu___:unit -> Tac (unit)) = (fun uu___ -> let  uu___#1098  : unit = (apply_lemma `(apply_feq_lem)[])
 in
-let  uu___#1097  : unit = (dismiss ())
+let  uu___#1099  : unit = (dismiss ())
 in
-let  uu___#1098  : (list binding) = (forall_intros ())
+let  uu___#1100  : (list binding) = (forall_intros ())
 in
 (ignore uu___@0:(Tm_unknown)))
 [@ ]

ulib/FStar.Attributes.fsti

@@ -119,19 +119,7 @@ val tcnorm : unit
     construction to track position information in generated VCs *)
 val dm4f_bind_range : unit
 
-(** We erase all ghost functions and unit-returning pure functions to
-    [()] at extraction. This creates a small issue with abstract
-    types. Consider a module that defines an abstract type [t] whose
-    (internal) definition is [unit] and also defines [f: int -> t]. [f]
-    would be erased to be just [()] inside the module, while the
-    client calls to [f] would not, since [t] is abstract. To get
-    around this, when extracting interfaces, if we encounter an
-    abstract type, we tag it with this attribute, so that
-    extraction can treat it specially.
-
-    Note, since the use of cross-module inlining (the [--cmi] option),
-    this attribute is no longer necessary. We retain it for legacy,
-    but will remove it in the future. *)
+[@@deprecated "use [@@erasable] instead"]
 val must_erase_for_extraction : unit
 
 (** When attached a top-level definition, the typechecker will succeed

ulib/FStar.Fin.fsti

@@ -90,9 +90,9 @@ type binary_relation (a: Type) = a -> a -> bool
     Use reveal_opaque when you really need it. Or use refl/trans/symm lemmas
     below to keep the context clean. *)
 
-val is_reflexive (#a:Type) (r: binary_relation a) : Type0
-val is_symmetric (#a:Type) (r: binary_relation a) : Type0
-val is_transitive (#a:Type) (r: binary_relation a) : Type0
+val is_reflexive (#a:Type) (r: binary_relation a) : prop
+val is_symmetric (#a:Type) (r: binary_relation a) : prop
+val is_transitive (#a:Type) (r: binary_relation a) : prop
 
 val is_reflexive_intro (#a:Type) (r: binary_relation a)
   : Lemma (requires forall (x:a). r x x) (ensures is_reflexive r)

ulib/FStar.GSet.fsti

@@ -18,13 +18,10 @@ module FStar.GSet
 (** Computational sets (on Types): membership is a boolean function *)
 #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
 
-(*
- * AR: mark it must_erase_for_extraction temporarily until CMI comes in
- *)
-[@@must_erase_for_extraction]
+[@@erasable]
 val set (a: Type u#a) : Type u#a
 
-val equal (#a:Type) (s1:set a) (s2:set a) : Type0
+val equal (#a:Type) (s1:set a) (s2:set a) : prop
 
 (* destructors *)
 
@@ -44,7 +41,7 @@ let disjoint (#a:Type) (s1: set a) (s2: set a) =
   equal (intersect s1 s2) empty
 
 (* ops *)
-type subset (#a:Type) (s1:set a) (s2:set a) :Type0 = forall x. mem x s1 ==> mem x s2
+type subset (#a:Type) (s1:set a) (s2:set a) :prop = forall x. mem x s1 ==> mem x s2
 
 (* Properties *)
 val mem_empty: #a:Type -> x:a -> Lemma

ulib/FStar.GhostSet.fsti

@@ -18,12 +18,12 @@ module FStar.GhostSet
 (** Ghost computational sets: membership is a ghost boolean function *)
 #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
 
-[@@must_erase_for_extraction; erasable]
+[@@erasable]
 val set (a: Type u#a) : Type u#a
 
 let decide_eq a = x:a -> y:a -> GTot (b:bool { b <==> (x==y) })
 
-val equal (#a:Type) (s1:set a) (s2:set a) : Type0
+val equal (#a:Type) (s1:set a) (s2:set a) : prop
 
 (* destructors *)
 
@@ -43,7 +43,7 @@ let disjoint (#a:Type) (s1: set a) (s2: set a) =
   equal (intersect s1 s2) empty
 
 (* ops *)
-type subset (#a:Type) (s1:set a) (s2:set a) :Type0 = forall x. mem x s1 ==> mem x s2
+type subset (#a:Type) (s1:set a) (s2:set a) :prop = forall x. mem x s1 ==> mem x s2
 
 (* Properties *)
 val mem_empty: #a:Type -> x:a -> Lemma