tactics: making t_smt_sync take an explicit vconfig

Also: - exposing {get,set}_vconfig - adding smt_sync' with explicit fuels
FStarLang · mtzguido · Apr 18, 2023 · Nov 14, 2022 · Nov 29, 2022 · Nov 29, 2022
commit a6578efb6928ae9e22c46a3ebe94ce0964ba2483
diff --git a/src/tactics/FStar.Tactics.Basic.fst b/src/tactics/FStar.Tactics.Basic.fst
@@ -31,6 +31,7 @@ open FStar.Tactics.Types
 open FStar.Tactics.Monad
 open FStar.Tactics.Printing
 open FStar.Syntax.Syntax
+open FStar.VConfig
 
 module BU     = FStar.Compiler.Util
 module Cfg    = FStar.TypeChecker.Cfg
@@ -782,11 +783,6 @@ let norm (s : list EMB.norm_step) : tac unit =
 
 let norm_term_env (e : env) (s : list EMB.norm_step) (t : term) : tac term = wrap_err "norm_term" <| (
     let! ps = get in
-    (* We need a set of options, but there might be no goals, so do this *)
-    let opts = match ps.goals with
-               | g::_ -> g.opts
-               | _ -> FStar.Options.peek ()
-    in
     if_verbose (fun () -> BU.print1 "norm_term_env: t = %s\n" (Print.term_to_string t)) ;!
     // only for elaborating lifts and all that, we don't care if it's actually well-typed
     let! t, _, _ = __tc_lax e t in
@@ -2201,19 +2197,52 @@ let term_eq_old (t1:term) (t2:term) : tac bool
 
 let with_compat_pre_core (n:Z.t) (f:tac 'a) : tac 'a =
     mk_tac (fun ps ->
-            FStar.Options.push ();
-            let res = FStar.Options.set_options ("--compat_pre_core 0") in
-            let r = run f ps in
-            FStar.Options.pop ();
-            r)
+      Options.with_saved_options (fun () ->
+        let _res = FStar.Options.set_options ("--compat_pre_core 0") in
+        run f ps))
 
-let smt_sync () : tac unit = wrap_err "smt_sync" <| (
+let get_vconfig () : tac vconfig =
+  let! g = cur_goal in
+ (* Restore goal's optionstate (a copy is needed) and read vconfig.
+  * This is an artifact of the options API being stateful in many places,
+  * morally this is just (get_vconfig g.opts) *)
+  let vcfg = Options.with_saved_options (fun () ->
+               FStar.Options.set (Util.smap_copy g.opts);
+               Options.get_vconfig ())
+  in
+  ret vcfg
+
+let set_vconfig (vcfg : vconfig) : tac unit =
+  (* Same comment as for get_vconfig applies, this is really just
+   * let g' = { g with opts = set_vconfig vcfg g.opts } *)
+  let! g = cur_goal in
+  let opts' = Options.with_saved_options (fun () ->
+                FStar.Options.set (Util.smap_copy g.opts);
+                Options.set_vconfig vcfg;
+                Options.peek ())
+  in
+  let g' = { g with opts = opts' } in
+  replace_cur g'
+
+let t_smt_sync (vcfg : vconfig) : tac unit = wrap_err "t_smt_sync" <| (
     let! goal = cur_goal in
     match get_phi goal with
     | None -> fail "Goal is not irrelevant"
     | Some phi ->
       let e = goal_env goal in
-      let ans : bool = e.solver.solve_sync None e phi in
+      let ans : bool =
+        (* Set goal's optionstate before asking solver, to respect
+         * its vconfig among other things. *)
+        Options.with_saved_options (fun () ->
+          (* NOTE: we ignore the goal's options, the rationale is that
+           * any verification-relevant option is inside the vconfig, so we
+           * should not need read the optionstate. Of course this vconfig
+           * will probably come in large part from a get_vconfig, which does
+           * read the goal's options. *)
+          Options.set_vconfig vcfg;
+          e.solver.solve_sync None e phi
+        )
+      in
       if ans
       then (
         mark_uvar_as_already_checked goal.goal_ctx_uvar;

diff --git a/src/tactics/FStar.Tactics.Basic.fsti b/src/tactics/FStar.Tactics.Basic.fsti
@@ -117,7 +117,11 @@ val comp_to_string         : comp -> tac string
 
 val term_eq_old            : term -> term -> tac bool
 val with_compat_pre_core   : Z.t -> tac 'a -> tac 'a
-val smt_sync               : unit -> tac unit
+
+val get_vconfig            : unit -> tac VConfig.vconfig
+val set_vconfig            : VConfig.vconfig -> tac unit
+
+val t_smt_sync             : VConfig.vconfig -> tac unit
 
 (***** Callbacks for the meta DSL framework *****)
 

diff --git a/src/tactics/FStar.Tactics.Interpreter.fst b/src/tactics/FStar.Tactics.Interpreter.fst
@@ -529,9 +529,17 @@ let () =
         (fun _ -> with_compat_pre_core) e_any e_int (e_tactic_thunk e_any) e_any
         (fun _ -> with_compat_pre_core) NBET.e_any NBET.e_int (e_tactic_nbe_thunk NBET.e_any) NBET.e_any;
 
-      mk_tac_step_1 0 "smt_sync"
-        smt_sync e_unit e_unit
-        smt_sync NBET.e_unit NBET.e_unit;
+      mk_tac_step_1 0 "get_vconfig"
+        get_vconfig e_unit e_vconfig
+        get_vconfig NBET.e_unit NBET.e_vconfig;
+
+      mk_tac_step_1 0 "set_vconfig"
+        set_vconfig e_vconfig e_unit
+        set_vconfig NBET.e_vconfig NBET.e_unit;
+
+      mk_tac_step_1 0 "t_smt_sync"
+        t_smt_sync e_vconfig e_unit
+        t_smt_sync NBET.e_vconfig NBET.e_unit;
 
       // reflection typechecker callbacks (part of the DSL framework)
 

diff --git a/tests/tactics/SMTSync.fst b/tests/tactics/SMTSync.fst
@@ -11,3 +11,12 @@ let test2 x = assert (1 + x == x + 2)
 
 let test3 x = assert (1 + x == x + 2)
   by (try smt_sync () with |_ -> tadmit ())
+
+let l = [1;2;3;4;5;6;7;8;9]
+
+(* smt_sync' takes explicit fuels *)
+
+[@@expect_failure]
+let test4 () = assert (List.Tot.length l == 9) by (smt_sync' 9 0)
+
+let test5 () = assert (List.Tot.length l == 9) by (smt_sync' 10 0)
diff --git a/ulib/FStar.Tactics.Builtins.fsti b/ulib/FStar.Tactics.Builtins.fsti
@@ -26,6 +26,7 @@ open FStar.Reflection.Data
 open FStar.Reflection.Const
 open FStar.Tactics.Types
 open FStar.Tactics.Result
+open FStar.VConfig
 
 (** Observe a sealed value. See Sealed.seal too. *)
 val unseal : #a:Type -> sealed a -> Tac a
@@ -428,9 +429,19 @@ It is an escape hatch for maintaining backward compatibility
 for code that breaks with the core typechecker. *)
 val with_compat_pre_core : #a:Type -> n:int -> f:(unit -> Tac a) -> Tac a
 
-(** Attempt to solve the current goal with SMT immediately, and
-fail if it cannot be solved. *)
-val smt_sync : unit -> Tac unit
+(** Get the [vconfig], including fuel, ifuel, rlimit, etc,
+associated with the current goal. *)
+val get_vconfig : unit -> Tac vconfig
+
+(** Set the [vconfig], including fuel, ifuel, rlimit, etc, associated
+with the current goal. This vconfig will be used if the goal is
+attempted by SMT at the end of a tactic run. *)
+val set_vconfig : vconfig -> Tac unit
+
+(** Attempt to solve the current goal with SMT immediately, and fail
+if it cannot be solved. The vconfig specifies fuels, limits, etc. The
+current goal's vconfig is ignored in favor of this one. *)
+val t_smt_sync : vconfig -> Tac unit
 
 
 (***** APIs used in the meta DSL framework *****)

diff --git a/ulib/FStar.Tactics.Derived.fst b/ulib/FStar.Tactics.Derived.fst
@@ -24,6 +24,7 @@ open FStar.Tactics.Builtins
 open FStar.Tactics.Result
 open FStar.Tactics.Util
 open FStar.Tactics.SyntaxHelpers
+open FStar.VConfig
 
 module L = FStar.List.Tot
 module V = FStar.Tactics.Visit
@@ -958,3 +959,14 @@ let lem_trans #a #x #z #y e1 e2 = ()
 
 (** Transivity of equality: reduce [x == z] to [x == ?u] and [?u == z].  *)
 let trans () : Tac unit = apply_lemma (`lem_trans)
+
+(* Alias to just use the current vconfig *)
+let smt_sync () : Tac unit = t_smt_sync (get_vconfig ())
+
+(* smt_sync': as smt_sync, but using a particular fuel/ifuel *)
+let smt_sync' (fuel ifuel : nat) : Tac unit =
+    let vcfg = get_vconfig () in
+    let vcfg' = { vcfg with initial_fuel = fuel; max_fuel = fuel
+                          ; initial_ifuel = ifuel; max_ifuel = ifuel }
+    in
+    t_smt_sync vcfg'