Do not unnecessarily invoke prover in impure specs.

Author: gebner

lib/common/Pulse.Lib.Core.fsti

@@ -50,6 +50,17 @@ val pulse_eager_elim : unit
 val pulse_eager_intro : unit
 val pulse_intro : unit
 
+(**
+Tags stateful functions where we don't need to run the prover to resolve the
+output in impure specs.
+
+This happens when all the variables in the rhs of the rewrites_to are only in
+mkeys, e.g. in unobservable functions like Array.sub that are only stateful to
+ensure the requirement that we only extract `x + n` for live pointers, but where
+ther result of the function does not depend on the slprop context.
+*)
+val pulse_impure_spec_no_proof_required : unit
+
 (** This attribute allows to do ambiguous proving when calling a function. *)
 val allow_ambiguous : unit
 

lib/core/Pulse.Lib.Core.fst

@@ -30,6 +30,8 @@ let pulse_eager_elim = ()
 let pulse_eager_intro = ()
 let pulse_intro = ()
 
+let pulse_impure_spec_no_proof_required = ()
+
 let allow_ambiguous = ()
 
 let slprop = slprop

lib/pulse/lib/Pulse.Lib.Array.Core.fsti

@@ -231,6 +231,7 @@ ghost fn gsub_elim u#a (#t: Type u#a) (arr: array t) #f (#mask: nat->prop) (i j:
     pure (Seq.length v' == length arr /\
       (forall (k:nat). k < j - i ==> Seq.index v k == Seq.index v' (k + i)))
 
+[@@pulse_impure_spec_no_proof_required]
 unobservable
 fn sub u#a (#t: Type u#a) (arr: array t) #f #mask (i: SZ.t) (j: erased nat)
     (#v: erased (Seq.seq (option t)) { SZ.v i <= j /\ j <= Seq.length (reveal v) })

lib/pulse/lib/Pulse.Lib.Reference.Array.fsti

@@ -22,6 +22,7 @@ open Pulse.Class.PtsTo
 open Pulse.Lib.Core
 open Pulse.Lib.Reference
 
+[@@pulse_impure_spec_no_proof_required]
 inline_for_extraction
 unobservable
 fn to_array u#a (#a: Type u#a) (r: ref a) #p (#v: erased a)

lib/pulse/lib/Pulse.Lib.Reference.fsti

@@ -157,6 +157,7 @@ fn pts_to_uninit_not_null u#a (#a: Type u#a) (r:ref a)
 
 val to_array_ghost #a (r: ref a) : GTot (array a)
 
+[@@pulse_impure_spec_no_proof_required]
 unobservable
 fn to_array_mask u#a (#a: Type u#a) (r: ref a) #p (#v: erased a)
   requires r |-> Frac p v
@@ -175,6 +176,7 @@ fn return_to_array_mask u#a (#a: Type u#a) (r: ref a) #p #v #m
 
 val array_at_ghost (#a: Type u#a) (arr: array a) (i: nat { i < length arr }) : GTot (r:ref a { to_array_ghost r == gsub arr i (i+1) })
 
+[@@pulse_impure_spec_no_proof_required]
 unobservable
 fn array_at u#a (#a: Type u#a) (arr: array a) (i: SizeT.t) #p
     (#v: erased (Seq.seq (option a)) { SizeT.v i < length arr /\ length arr == Seq.length v /\ Some? (Seq.index v (SizeT.v i)) }) #mask
@@ -185,6 +187,7 @@ fn array_at u#a (#a: Type u#a) (arr: array a) (i: SizeT.t) #p
   ensures r |-> Frac p (Some?.v (Seq.index v (SizeT.v i)))
   ensures pts_to_mask arr #p v (fun k -> mask k /\ k <> SizeT.v i)
 
+[@@pulse_impure_spec_no_proof_required]
 unobservable
 fn array_at_uninit u#a (#a: Type u#a) (arr: array a) (i: SizeT.t)
     (#v: erased (Seq.seq (option a)) { SizeT.v i < length arr /\ length arr == Seq.length v }) #mask

src/checker/Pulse.Checker.ImpureSpec.fst

@@ -65,6 +65,9 @@ let prove (g: env) (goal: slprop) (ctxt: slprop) (r: range) : T.Tac unit =
   let (| g', ctxt', _ |) = Pulse.Checker.Prover.prove r g ctxt goal allow_amb in
   ()
 
+let is_no_proof_app (g: env) (t: term) : T.Tac bool =
+  Pulse.Reflection.Util.head_has_attr_string "Pulse.Lib.Core.pulse_impure_spec_no_proof_required" t
+
 let symb_eval_stateful_app (g: env) (ctxt: slprop) (t: term) : T.Tac R.term =
   let t, ty, _ = tc_term_phase1 g t in
   debug g (fun _ -> [ text "impure spec inferred type"; pp t; pp ty ]);
@@ -87,7 +90,7 @@ let symb_eval_stateful_app (g: env) (ctxt: slprop) (t: term) : T.Tac R.term =
       ] (Some (RU.range_of_term t))
     | Some rwr ->
       let allow_amb = true in
-      prove g pre ctxt (RU.range_of_term t);
+      (if not (is_no_proof_app g t) then prove g pre ctxt (RU.range_of_term t));
       debug g (fun _ -> [text "evaluated" ^/^ pp t ^/^ text "to" ^/^ pp rwr]);
       let rwr = RU.deep_compress rwr in // TODO: maybe this fails on uvars...
       rwr