fix: better handling of unconditional branches (#143)

### Description:

We now attempt to reflect the PC after each step, only falling back to
blindly incrementing if reflection failed.
With this change, `sym_n` is able to deal with unconditional branches,
and I've fixed the `AddLoop` example accordingly.

The `reflectBitVecValue` used here does involve a `whnfD`, which might
be a expensive.
However, this reduction only happens when the value of the PC is not a
literal (i.e., for conditional branches), where reflection of the PC
really is necessary.
On non-branching instructions, or even unconditional branches, the call
should be basically free,
so there is little downside to this approach.

### Testing:

`make all` ran locally

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

---------

Co-authored-by: Shilpi Goel <[email protected]>

Proofs/Experiments/AddLoop/AddLoop.lean

@@ -306,21 +306,8 @@ theorem effects_of_nextc_from_0x4005a4
   -- TODO: Tactic to "explode" conjunctions?
   obtain ⟨h_s0_pc, h_s0_program, h_s0_err, h_s0_sp_aligned⟩ := h_pre
   -- Symbolic simulation
-  -- (FIXME) sym_n doesn't play well with unconditional branches.
-  /-
-  application type mismatch
-  program.stepi_0x4005a8 s1 s2 h_s1_program h_s1_pc
-  argument
-  h_s1_pc
-  has type
-  r StateField.PC s1 = 0x4005b0#64 : Prop
-  but is expected to have type
-  r StateField.PC s1 = 0x4005a8#64 : Prop
-  -/
-  -- sym_n 2
-  sym_n 1 at s0
-  sym_n 1 at s1
-  simp (config := {ground := true}) only [*, state_simp_rules, bitvec_rules, minimal_theory]
+  sym_n 2
+  simp (config := {ground := true}) only []
   rw [AddWithCarry.all_ones_zero_flag_64]
   done
 

Tactics/Sym.lean

@@ -181,7 +181,11 @@ def withoutHyp (hyp : Name) (k : TacticM Unit) : TacticM (Option FVarId) :=
 
 /-- Given an equality `h_step : s{i+1} = w ... (... (w ... s{i})...)`,
 add hypotheses that axiomatically describe the effects in terms of
-reads from `s{i+1}` -/
+reads from `s{i+1}`.
+
+Return the context for the next step (see `SymContext.next`), where
+we attempt to determine the new PC by reflecting the obtained effects,
+falling back to incrementing the PC if reflection failed. -/
 def explodeStep (c : SymContext) (hStep : Expr) : TacticM SymContext :=
   withMainContext do
     let mut eff ← AxEffects.fromEq hStep
@@ -249,7 +253,21 @@ def explodeStep (c : SymContext) (hStep : Expr) : TacticM SymContext :=
         eff.validate
 
       eff.addHypothesesToLContext s!"h_{c.next_state}_"
-    return { c with axHyps := axHyps ++ c.axHyps}
+    let c := { c with axHyps := axHyps ++ c.axHyps}
+
+    -- Attempt to reflect the new PC
+    let nextPc ← eff.getField .PC
+    let nextPc? ← try
+      let nextPc ← reflectBitVecLiteral 64 nextPc.value
+      -- NOTE: `reflectBitVecLiteral` is fast when the value is a literal,
+      -- but might involve an expensive reduction when it is not
+      pure <| some nextPc
+    catch err =>
+      trace[Tactic.sym] "failed to reflect {nextPc.value}\n\n\
+        {err.toMessageData}"
+      pure none
+
+    return c.next nextPc?
 
 /-- A tactic wrapper around `explodeStep`.
 Note the use of `SymContext.fromLocalContext`,
@@ -313,7 +331,7 @@ def sym1 (c : SymContext) (whileTac : TSyntax `tactic) : TacticM SymContext :=
           skipping simplification step"
 
     -- Prepare `h_program`,`h_err`,`h_pc`, etc. for next state
-    let c ← withMainContext <| do
+    withMainContext <| do
       let hStep ← SymContext.findFromUserName h_step.getId
       -- ^^ we can't reuse `hStep` from before, since its fvarId might've been
       --    changed by `simp`
@@ -325,8 +343,6 @@ def sym1 (c : SymContext) (whileTac : TSyntax `tactic) : TacticM SymContext :=
 
       return c
 
-    return c.next
-
 /- used in `sym_n` tactic to specify an initial state -/
 syntax sym_at := "at" ident