feat: use withCurrHeartbeats to reset the heartbeat usage for each st…

…ep in `sym_n` (#213)

### Description:

Stacked on:
- [x] #204 
- [x] #207 
- [x] #209 
- [x] #211 

This PR implements "snorkeling" of the heartbeat budget.

This unfortunately does not buy us much, as aggregation for 500 steps
already seems to hit both the recursion limit and heartbeat budget, by
itself.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine? Yes

### 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]>

Tactics/Sym.lean

@@ -232,6 +232,10 @@ elab "explode_step" h_step:term " at " state:term : tactic => withMainContext do
 Symbolically simulate a single step, according the the symbolic simulation
 context `c`, returning the context for the next step in simulation. -/
 def sym1 (whileTac : TSyntax `tactic) : SymM Unit := do
+  /- `withCurrHeartbeats` sets the initial heartbeats to the current heartbeats,
+  effectively resetting our heartbeat budget back to the maximum. -/
+  withCurrHeartbeats <| do
+
   let stateNumber ← getCurrentStateNumber
   withTraceNode m!"(sym1): simulating step {stateNumber}" (tag:="sym1") <|
   withMainContext' do
@@ -395,6 +399,7 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
         sym1 whileTac
 
     traceHeartbeats "symbolic simulation total"
+    withCurrHeartbeats <|
     withTraceNode "Post processing" (tag := "postProccessing") <| do
       let c ← getThe SymContext
       -- Check if we can substitute the final state
@@ -426,4 +431,4 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
         let goal? ← LNSymSimp (← getMainGoal) c.aggregateSimpCtx c.aggregateSimprocs
         replaceMainGoal goal?.toList
 
-    traceHeartbeats "final usage"
+      traceHeartbeats "aggregation"