chore: checkpoint tactic state before in CSE and restore on failure […

…1/4?] (#114)

This fixes the bug reported by @shigoel, where we would get a `no goals
to be solved` failure after the `cse` tactic was run on all hypotheses
--- we were incorrectly backtracking, which is fixed now.

The next PRs will improve scaling issues by the following:
1. adding a custom amount of fuel that will allow the CSE tactic to stop
gracefully.
2. Not CSEing small objects such as `Nat` literals which are ubiquitous,
as well as pointless to CSE.

We will also make improvements to debug logging in a separate commit. 
Thus, we anticipate this patch set to have four patches, which will be
peeled from #113

Proofs/SHA512/SHA512Sym.lean

@@ -25,7 +25,7 @@ that the register `x2` is decremented early on in this program:
 
 In the near future, we'd like to prove that the hash computed for this
 one input block matches the expected value, i.e., one dictated by
-`SHA2.sha512`. 
+`SHA2.sha512`.
 
 Also see `Tests.SHA2.SHA512ProgramTest` for an example of a concrete
 run that checks the implementation against the specification.
@@ -47,6 +47,7 @@ abbrev ktbl_addr : BitVec 64 := 0x1b4300#64
 -- set_option profiler true in
 -- set_option profiler.threshold 1 in
 -- set_option pp.deepTerms false in
+set_option maxHeartbeats 9999999 in -- To be fixed by https://github.com/leanprover/LNSym/pull/113
 theorem sha512_block_armv8_1block (s0 sf : ArmState)
   -- (FIXME) Ignore the `stp` instruction for now.
   (h_s0_pc : read_pc s0 = 0x1264c4#64)
@@ -71,15 +72,15 @@ theorem sha512_block_armv8_1block (s0 sf : ArmState)
                   ktbl_addr      (SHA2.k_512.length * 8))
   -- (FIXME) Use program.length instead of 20 here (depends on the
   -- performance of the new symbolic simulation tactic).
-  (h_run : sf = run 20 s0) :  
+  (h_run : sf = run 20 s0) :
   r (StateField.GPR 2#5) sf = 0#64 ∧
   r StateField.ERR sf = StateError.None := by
   sym_n 20
   /-
   (FIXME @bollu) cse fails with the following message:
   no goals to be solved
   -/
-  -- cse (config := { processHyps := .allHyps })
+  cse (config := { processHyps := .allHyps })
   -- Final Steps
   unfold run at h_run
   subst sf

Tactics/CSE.lean

@@ -223,6 +223,7 @@ def CSEM.generalize (arg : GeneralizeArg) : CSEM Bool := do
   let e := arg.expr
 
   let mvarId ← getMainGoal
+  let checkpoint ← Tactic.saveState
   mvarId.withContext do
     -- implementation modeled after `Lean.Elab.Tactic.evalGeneralize`.
     trace[Tactic.cse.generalize] "{tryEmoji} Generalizing {hname} : {e} = {xname}"
@@ -246,6 +247,7 @@ def CSEM.generalize (arg : GeneralizeArg) : CSEM Bool := do
       trace[Tactic.cse.generalize] "{checkEmoji} succeeded in generalizing {hname}. ({← getMainGoal})"
       return true
     catch e =>
+      checkpoint.restore
       trace[Tactic.cse.generalize] "{bombEmoji} failed to generalize {hname}"
       return false