diff --git a/.gitignore b/.gitignore
index 6c2506f9..1e3e3f4d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@
 /lake-packages/*
 /.lake/*
 *.log
+/data/*
diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
index ec874fca..484c83fe 100644
--- a/Arm/Insts/Common.lean
+++ b/Arm/Insts/Common.lean
@@ -219,20 +219,32 @@ def CheckSPAlignment (s : ArmState) : Prop :=
 instance : Decidable (CheckSPAlignment s) := by unfold CheckSPAlignment; infer_instance
 
 @[state_simp_rules]
-theorem CheckSPAligment_of_w_different (h : StateField.GPR 31#5 ≠ fld) :
+theorem CheckSPAligment_w_different_eq (h : StateField.GPR 31#5 ≠ fld) :
   CheckSPAlignment (w fld v s) = CheckSPAlignment s := by
   simp_all only [CheckSPAlignment, state_simp_rules, minimal_theory, bitvec_rules]
 
+theorem CheckSPAligment_w_of_ne_sp_of (h : StateField.GPR 31#5 ≠ fld) :
+    CheckSPAlignment s → CheckSPAlignment (w fld v s) := by
+  simp only [CheckSPAligment_w_different_eq h, imp_self]
+
 @[state_simp_rules]
 theorem CheckSPAligment_of_w_sp :
   CheckSPAlignment (w (StateField.GPR 31#5) v s) = (Aligned v 4) := by
   simp_all only [CheckSPAlignment, state_simp_rules, minimal_theory, bitvec_rules]
 
+theorem CheckSPAligment_w_sp_of (h : Aligned v 4) :
+    CheckSPAlignment (w (StateField.GPR 31#5) v s) := by
+  simp only [CheckSPAlignment, read_gpr, r_of_w_same, zeroExtend_eq, h]
+
 @[state_simp_rules]
-theorem CheckSPAligment_of_write_mem_bytes :
+theorem CheckSPAligment_write_mem_bytes_eq :
   CheckSPAlignment (write_mem_bytes n addr v s) = CheckSPAlignment s := by
   simp_all only [CheckSPAlignment, state_simp_rules, minimal_theory, bitvec_rules]
 
+theorem CheckSPAligment_write_mem_bytes_of :
+  CheckSPAlignment s → CheckSPAlignment (write_mem_bytes n addr v s) := by
+  simp only [CheckSPAligment_write_mem_bytes_eq, imp_self]
+
 @[state_simp_rules]
 theorem CheckSPAlignment_AddWithCarry_64_4 (st : ArmState) (y : BitVec 64) (carry_in : BitVec 1)
   (x_aligned : CheckSPAlignment st)
diff --git a/Benchmarks.lean b/Benchmarks.lean
index 7b7fcc0a..cc1f1c6b 100644
--- a/Benchmarks.lean
+++ b/Benchmarks.lean
@@ -3,6 +3,11 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Alex Keizer
 -/
+import Benchmarks.SHA512_75
+import Benchmarks.SHA512_75_noKernel_noLint
 import Benchmarks.SHA512_150
+import Benchmarks.SHA512_150_noKernel_noLint
 import Benchmarks.SHA512_225
+import Benchmarks.SHA512_225_noKernel_noLint
 import Benchmarks.SHA512_400
+import Benchmarks.SHA512_400_noKernel_noLint
diff --git a/Benchmarks/Command.lean b/Benchmarks/Command.lean
index bf605c43..3762f788 100644
--- a/Benchmarks/Command.lean
+++ b/Benchmarks/Command.lean
@@ -12,58 +12,104 @@ initialize
     defValue := false
     descr := "enables/disables benchmarking in `withBenchmark` combinator"
   }
+  registerOption `benchmark.runs {
+    defValue := (5 : Nat)
+    descr := "controls how many runs the `benchmark` command does. \
+    NOTE: this value is ignored when the `profiler` option is set to true"
+  }
+  /- Shouldn't be set directly, instead, use the `benchmark` command -/
+  registerTraceClass `benchmark
 
 variable {m} [Monad m] [MonadLiftT BaseIO m] in
-def withHeartbeatsAndMs (x : m α) : m (α × Nat × Nat) := do
+/-- Measure the heartbeats and time (in milliseconds) taken by `x` -/
+def withHeartbeatsAndMilliseconds (x : m α) : m (α × Nat × Nat) := do
   let start ← IO.monoMsNow
   let (a, heartbeats) ← withHeartbeats x
   let endTime ← IO.monoMsNow
   return ⟨a, heartbeats, endTime - start⟩
 
-elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do
-  logInfo m!"Running {id} benchmark\n"
+/-- Adds a trace node with the `benchmark` class, but only if the profiler
+option is *not* set.
+
+We deliberately suppress benchmarking nodes when profiling, since it generally
+only adds noise
+-/
+def withBenchTraceNode (msg : MessageData) (x : CommandElabM α )
+    : CommandElabM α := do
+  if (← getBoolOption `profiler) then
+    x
+  else
+    withTraceNode `benchmark (fun _ => pure msg) x (collapsed := false)
 
+/--
+Run a benchmark for a set number of times, and report the average runtime.
+
+If the `profiler` option is set true, we run the benchmark only once, with:
+- `trace.profiler` to true, and
+- `trace.profiler.output` set based on the `benchmark.profilerDir` and the
+    id of the benchmark
+-/
+elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do
+  let originalOpts ← getOptions
+  let mut n := originalOpts.getNat `benchmark.runs 5
+  let mut opts := originalOpts
+  opts := opts.setBool `benchmark true
   let stx ← `(command|
-    set_option benchmark true in
     example $declSig:optDeclSig $val:declVal
   )
 
-  let n := 5
-  let mut totalRunTime := 0
-  -- geomean = exp(log((a₁ a₂ ... aₙ)^1/n)) =
-  -- exp(1/n * (log a₁ + log a₂ + log aₙ)).
-  let mut totalRunTimeLog := 0
-  for i in [0:n] do
-    logInfo m!"\n\nRun {i} (out of {n}):\n"
-    let ((), _, runTime) ← withHeartbeatsAndMs <|
-      elabCommand stx
-
-    logInfo m!"Proof took {runTime / 1000}s in total"
-    totalRunTime := totalRunTime + runTime
-    totalRunTimeLog := totalRunTimeLog + Float.log runTime.toFloat
-
-  let avg := totalRunTime.toFloat / n.toFloat / 1000
-  let geomean := (Float.exp (totalRunTimeLog / n.toFloat)) / 1000.0
-  logInfo m!"\
-{id}:
-  average runtime over {n} runs:
-    {avg}s
-  geomean over {n} runs:
-    {geomean}s
-"
+  if (← getBoolOption `profiler) then
+    opts := opts.setBool `trace.profiler true
+    opts := opts.setNat `trace.profiler.threshold 1
+    n := 1 -- only run once, if `profiler` is set to true
+  else
+    opts := opts.setBool `trace.benchmark true
+
+  if n = 0 then
+    return ()
+
+  -- Set options
+  modifyScope fun scope => { scope with opts }
+
+  withBenchTraceNode m!"Running {id} benchmark" <| do
+    let mut totalRunTime := 0
+    -- geomean = exp(log((a₁ a₂ ... aₙ)^1/n)) =
+    -- exp(1/n * (log a₁ + log a₂ + log aₙ)).
+    let mut totalRunTimeLog : Float := 0
+    for i in [0:n] do
+      let runTime ← withBenchTraceNode m!"Run {i+1} (out of {n}):" <| do
+        let ((), _, runTime) ← withHeartbeatsAndMilliseconds <|
+          elabCommand stx
+
+        trace[benchmark] m!"Proof took {runTime / 1000}s in total"
+        pure runTime
+      totalRunTime := totalRunTime + runTime
+      totalRunTimeLog := totalRunTimeLog + Float.log runTime.toFloat
+
+    let avg := totalRunTime.toFloat / n.toFloat / 1000
+    let geomean := (Float.exp (totalRunTimeLog / n.toFloat)) / 1000.0
+    trace[benchmark] m!"\
+  {id}:
+    average runtime over {n} runs:
+      {avg}s
+    geomean over {n} runs:
+      {geomean}s
+  "
+    -- Restore options
+    modifyScope fun scope => { scope with opts := originalOpts }
 
 /-- Set various options to disable linters -/
 macro "disable_linters" "in" cmd:command : command => `(command|
-  set_option linter.constructorNameAsVariable false in
-  set_option linter.deprecated false in
-  set_option linter.missingDocs false in
-  set_option linter.omit false in
-  set_option linter.suspiciousUnexpanderPatterns false in
-  set_option linter.unnecessarySimpa false in
-  set_option linter.unusedRCasesPattern false in
-  set_option linter.unusedSectionVars false in
-  set_option linter.unusedVariables false in
-  $cmd
+set_option linter.constructorNameAsVariable false in
+set_option linter.deprecated false in
+set_option linter.missingDocs false in
+set_option linter.omit false in
+set_option linter.suspiciousUnexpanderPatterns false in
+set_option linter.unnecessarySimpa false in
+set_option linter.unusedRCasesPattern false in
+set_option linter.unusedSectionVars false in
+set_option linter.unusedVariables false in
+$cmd
 )
 
 /-- The default `maxHeartbeats` setting.
@@ -96,7 +142,7 @@ private def withBenchmarkAux (x : m α) (f : Nat → Nat → m Unit)  : m α :=
   if (← getBoolOption `benchmark) = false then
     x
   else
-    let (a, heartbeats, t) ← withHeartbeatsAndMs x
+    let (a, heartbeats, t) ← withHeartbeatsAndMilliseconds x
     f heartbeats t
     return a
 
diff --git a/Benchmarks/SHA512.lean b/Benchmarks/SHA512.lean
index b0901b0c..685a18b7 100644
--- a/Benchmarks/SHA512.lean
+++ b/Benchmarks/SHA512.lean
@@ -15,11 +15,15 @@ namespace Benchmarks
 
 def SHA512Bench (nSteps : Nat) : Prop :=
   ∀ (s0 sf : ArmState)
-    (_h_s0_num_blocks : r (.GPR 2#5) s0 = 10)
+    (_h_s0_num_blocks : r (.GPR 2#5) s0 = 10#64)
     (_h_s0_pc : read_pc s0 = 0x1264c0#64)
     (_h_s0_err : read_err s0 = StateError.None)
     (_h_s0_sp_aligned : CheckSPAlignment s0)
     (_h_s0_program : s0.program = SHA512.program)
     (_h_run : sf = run nSteps s0),
     r StateField.ERR sf = StateError.None
-    ∧ r (.GPR 2#5) sf = BitVec.ofNat _ (9 - (nSteps / 485))
+    ∧ r (.GPR 2#5) sf = BitVec.ofNat 64 (10 - ((nSteps + 467) / 485))
+    -- / -------------------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    -- | This computes the expected value of x2, taking into account that
+    -- | the loop body is 485 instructions long, and that x2 is first
+    -- | decremented after 18 instructions (485 - 18 = 467).
diff --git a/Benchmarks/SHA512_150.lean b/Benchmarks/SHA512_150.lean
index da549001..0cf74cff 100644
--- a/Benchmarks/SHA512_150.lean
+++ b/Benchmarks/SHA512_150.lean
@@ -12,5 +12,6 @@ open Benchmarks
 benchmark sha512_150_instructions : SHA512Bench 150 := fun s0 _ h => by
   intros
   sym_n 150
-  · exact (sorry : Aligned ..)
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
   done
diff --git a/Benchmarks/SHA512_150_noKernel_noLint.lean b/Benchmarks/SHA512_150_noKernel_noLint.lean
new file mode 100644
index 00000000..faec9e9f
--- /dev/null
+++ b/Benchmarks/SHA512_150_noKernel_noLint.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+disable_linters in
+set_option debug.skipKernelTC true in
+benchmark sha512_150_noKernel_noLint : SHA512Bench 150 := fun s0 _ h => by
+  intros
+  sym_n 150
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
+  done
diff --git a/Benchmarks/SHA512_225_noKernel_noLint.lean b/Benchmarks/SHA512_225_noKernel_noLint.lean
new file mode 100644
index 00000000..df2b7a88
--- /dev/null
+++ b/Benchmarks/SHA512_225_noKernel_noLint.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+disable_linters in
+set_option debug.skipKernelTC true in
+benchmark sha512_225_noKernel_noLint : SHA512Bench 225 := fun s0 _ h => by
+  intros
+  sym_n 225
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
+  done
diff --git a/Benchmarks/SHA512_400.lean b/Benchmarks/SHA512_400.lean
index 3be508ee..ae26c4e9 100644
--- a/Benchmarks/SHA512_400.lean
+++ b/Benchmarks/SHA512_400.lean
@@ -12,5 +12,6 @@ open Benchmarks
 benchmark sha512_400_instructions : SHA512Bench 400 := fun s0 _ h => by
   intros
   sym_n 400
-  · exact (sorry : Aligned ..)
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
   done
diff --git a/Benchmarks/SHA512_400_noKernel_noLint.lean b/Benchmarks/SHA512_400_noKernel_noLint.lean
new file mode 100644
index 00000000..cefce28c
--- /dev/null
+++ b/Benchmarks/SHA512_400_noKernel_noLint.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+disable_linters in
+set_option debug.skipKernelTC true in
+benchmark sha512_400_noKernel_noLint : SHA512Bench 400 := fun s0 _ h => by
+  intros
+  sym_n 400
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
+  done
diff --git a/Benchmarks/SHA512_50.lean b/Benchmarks/SHA512_50.lean
new file mode 100644
index 00000000..7e388869
--- /dev/null
+++ b/Benchmarks/SHA512_50.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+benchmark sha512_50 : SHA512Bench 50 := fun s0 _ h => by
+  intros
+  sym_n 50
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
+  done
diff --git a/Benchmarks/SHA512_50_noKernel_noLint.lean b/Benchmarks/SHA512_50_noKernel_noLint.lean
new file mode 100644
index 00000000..f08a6868
--- /dev/null
+++ b/Benchmarks/SHA512_50_noKernel_noLint.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+disable_linters in
+set_option debug.skipKernelTC true in
+benchmark sha512_50_noKernel_noLint : SHA512Bench 50 := fun s0 _ h => by
+  intros
+  sym_n 50
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
+  done
diff --git a/Benchmarks/SHA512_75.lean b/Benchmarks/SHA512_75.lean
new file mode 100644
index 00000000..068b06b3
--- /dev/null
+++ b/Benchmarks/SHA512_75.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+benchmark sha512_75 : SHA512Bench 75 := fun s0 _ h => by
+  intros
+  sym_n 75
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
+  done
diff --git a/Benchmarks/SHA512_75_noKernel_noLint.lean b/Benchmarks/SHA512_75_noKernel_noLint.lean
new file mode 100644
index 00000000..516880c8
--- /dev/null
+++ b/Benchmarks/SHA512_75_noKernel_noLint.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+disable_linters in
+set_option debug.skipKernelTC true in
+benchmark sha512_75_noKernel_noLint : SHA512Bench 75 := fun s0 _ h => by
+  intros
+  sym_n 75
+  simp (config := {failIfUnchanged := false}) only [h, bitvec_rules]
+  all_goals exact (sorry : Aligned ..)
+  done
diff --git a/Makefile b/Makefile
index 00cf37c6..a06a2d1c 100644
--- a/Makefile
+++ b/Makefile
@@ -5,6 +5,8 @@
 SHELL := /bin/bash
 
 LAKE = lake
+LEAN = $(LAKE) env lean
+GIT = git
 
 NUM_TESTS?=3
 VERBOSE?=--verbose
@@ -37,9 +39,25 @@ awslc_elf:
 cosim:
 	time -p lake exe lnsym $(VERBOSE) --num-tests $(NUM_TESTS)
 
+BENCHMARKS = \
+	Benchmarks/SHA512_50.lean \
+	Benchmarks/SHA512_50_noKernel_noLint.lean \
+	Benchmarks/SHA512_75.lean \
+	Benchmarks/SHA512_75_noKernel_noLint.lean \
+	Benchmarks/SHA512_150.lean \
+	Benchmarks/SHA512_150_noKernel_noLint.lean \
+	Benchmarks/SHA512_225.lean \
+	Benchmarks/SHA512_225_noKernel_noLint.lean \
+	Benchmarks/SHA512_400.lean \
+	Benchmarks/SHA512_400_noKernel_noLint.lean
+
 .PHONY: benchmarks
 benchmarks:
-	$(LAKE) build Benchmarks
+	./scripts/benchmark.sh $(BENCHMARKS)
+
+.PHONY: profile
+profile:
+	./scripts/profile.sh $(BENCHMARKS)
 
 .PHONY: clean clean_all
 clean:
diff --git a/README.md b/README.md
index 47939c18..2054fdf4 100644
--- a/README.md
+++ b/README.md
@@ -43,6 +43,8 @@ native-code programs of interest.
 
 `benchmarks`: run benchmarks for the symbolic simulator.
 
+`profiler`: run a single round of each benchmark, with the profiler enabled
+
 ### Makefile variables that can be passed in at the command line
 
 `VERBOSE`: Verbose mode; prints disassembly of the instructions being
diff --git a/Tactics/Attr.lean b/Tactics/Attr.lean
index e6b682e8..37026ee9 100644
--- a/Tactics/Attr.lean
+++ b/Tactics/Attr.lean
@@ -9,8 +9,11 @@ open Lean
 initialize
   -- CSE tactic's non-verbose summary logging.
   registerTraceClass `Tactic.cse.summary
+
   -- enable tracing for `sym_n` tactic and related components
   registerTraceClass `Tactic.sym
+  -- enable verbose tracing
+  registerTraceClass `Tactic.sym.debug
 
   -- enable tracing for heartbeat usage of `sym_n`
   registerTraceClass `Tactic.sym.heartbeats
diff --git a/Tactics/Common.lean b/Tactics/Common.lean
index 50212ce9..9763af33 100644
--- a/Tactics/Common.lean
+++ b/Tactics/Common.lean
@@ -277,6 +277,42 @@ def Lean.Expr.eqReadField? (e : Expr) : Option (Expr × Expr × Expr) := do
     | none
   some (field, state, value)
 
+/-- Return the expression for `Memory` -/
+def mkMemory : Expr := mkConst ``Memory
+
+/-! ## Expr Helpers -/
+
+/-- Throw an error if `e` is not of type `expectedType` -/
+def assertHasType (e expectedType : Expr) : MetaM Unit := do
+  let eType ← inferType e
+  if !(←isDefEq eType expectedType) then
+    throwError "{e} {← mkHasTypeButIsExpectedMsg eType expectedType}"
+
+/-- Throw an error if `e` is not def-eq to `expected` -/
+def assertIsDefEq (e expected : Expr) : MetaM Unit := do
+  if !(←isDefEq e expected) then
+    throwError "expected:\n  {expected}\nbut found:\n  {e}"
+
+/--
+Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`.
+Rewrites with a fresh metavariable as the ambient goal.
+Fails if the rewrite produces any subgoals.
+-/
+-- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477
+def rewrite (e eq : Expr) : MetaM Expr := do
+  let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq
+    | throwError "Expr.rewrite may not produce subgoals."
+  return eq'
+
+/--
+Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`.
+Rewrites with a fresh metavariable as the ambient goal.
+Fails if the rewrite produces any subgoals.
+-/
+-- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477
+def rewriteType (e eq : Expr) : MetaM Expr := do
+  mkEqMP (← rewrite (← inferType e) eq) e
+
 /-! ## Tracing helpers -/
 
 def traceHeartbeats (cls : Name) (header : Option String := none) :
diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
index b0d5621f..fb31ee54 100644
--- a/Tactics/Sym.lean
+++ b/Tactics/Sym.lean
@@ -5,21 +5,23 @@ Author(s): Shilpi Goel, Alex Keizer
 -/
 import Arm.Exec
 import Arm.Memory.MemoryProofs
+import Arm.Memory.SeparateAutomation
 import Tactics.FetchAndDecode
 import Tactics.Sym.Context
 
 import Lean
 
 open BitVec
-open Lean Meta
-open Lean.Elab.Tactic
+open Lean
+open Lean.Meta Lean.Elab.Tactic
 
 open AxEffects SymContext
+open Sym (withTraceNode withVerboseTraceNode)
 
 /-- A wrapper around `evalTactic` that traces the passed tactic script,
 executes those tactics, and then traces the new goal state -/
 private def evalTacticAndTrace (tactic : TSyntax `tactic) : TacticM Unit :=
-  withTraceNode `Tactic.sym (fun _ => pure m!"running: {tactic}") <| do
+  withTraceNode m!"running: {tactic}" <| do
     evalTactic tactic
     trace[Tactic.sym] "new goal state:\n{← getGoals}"
 
@@ -50,7 +52,8 @@ to add a new local hypothesis in terms of `w` and `write_mem`
   `h_step : ?s' = w _ _ (w _ _ (... ?s))`
 -/
 def stepiTac (stepiEq : Expr) (hStep : Name) : SymReaderM Unit := fun ctx =>
-  withMainContext' do
+  withMainContext' <|
+  withVerboseTraceNode m!"stepiTac: {stepiEq}" <| do
     let pc := (Nat.toDigits 16 ctx.pc.toNat).asString
     --  ^^ The PC in hex
     let stepLemma := Name.str ctx.program s!"stepi_eq_0x{pc}"
@@ -89,8 +92,7 @@ Finally, we use this proof to change the type of `h_run` accordingly.
 -/
 def unfoldRun (whileTac : Unit → TacticM Unit) : SymReaderM Unit := do
   let c ← readThe SymContext
-  let msg := m!"unfoldRun (runSteps? := {c.runSteps?})"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <|
+  withTraceNode m!"unfoldRun (runSteps? := {c.runSteps?})" (tag := "unfoldRun") <|
   match c.runSteps? with
     | some (_ + 1) => do
         trace[Tactic.sym] "runSteps is statically known to be non-zero, \
@@ -124,9 +126,9 @@ def unfoldRun (whileTac : Unit → TacticM Unit) : SymReaderM Unit := do
         let subGoal ← mkFreshMVarId
         let _ ← mkFreshExprMVarWithId subGoal subGoalTy
 
-        let msg := m!"runSteps is not statically known, so attempt to prove:\
-          {subGoal}"
-        withTraceNode `Tactic.sym (fun _ => pure msg) <| subGoal.withContext <| do
+        withTraceNode m!"runSteps is not statically known, so attempt to prove:\
+          {subGoal}" <|
+        subGoal.withContext <| do
           setGoals [subGoal]
           whileTac () -- run `whileTac` to attempt to close `subGoal`
 
@@ -166,9 +168,10 @@ add the relevant hypotheses to the local context, and
 store an `AxEffects` object with the newly added variables in the monad state
 -/
 def explodeStep (hStep : Expr) : SymM Unit :=
-  withMainContext' do
+  withMainContext' <|
+  withTraceNode m!"explodeStep {hStep}" (tag := "explodeStep") <| do
     let c ← getThe SymContext
-    let mut eff ← AxEffects.fromEq hStep
+    let mut eff ← AxEffects.fromEq hStep c.effects.stackAlignmentProof?
 
     let stateExpr ← getCurrentState
     /- Assert that the initial state of the obtained `AxEffects` is equal to
@@ -182,47 +185,26 @@ def explodeStep (hStep : Expr) : SymM Unit :=
     eff ← eff.withProgramEq c.effects.programProof
     eff ← eff.withField (← c.effects.getField .ERR).proof
 
-    if let some h_sp := c.h_sp? then
-      let hSp ← SymContext.findFromUserName h_sp
-      -- let effWithSp?
-      eff ← match ← eff.withStackAlignment? hSp.toExpr with
-        | some newEff => pure newEff
-        | none => do
-            trace[Tactic.sym] "failed to show stack alignment"
-            -- FIXME: in future, we'd like to detect when the `sp_aligned`
-            -- hypothesis is actually necessary, and add the proof obligation
-            -- on-demand. For now, however, we over-approximate, and say that
-            -- if the original state was known to be aligned, and something
-            -- writes to the SP, then we eagerly add the obligation to proof
-            -- that the result is aligned as well.
-            -- If you don't want this obligation, simply remove the hypothesis
-            -- that the original state is aligned
-            let spEff ← eff.getField .SP
-            let subGoal ← mkFreshMVarId
-            -- subGoal.setTag <|
-            let hAligned ← do
-              let name := Name.mkSimple s!"h_{← getNextStateName}_sp_aligned"
-              mkFreshExprMVarWithId subGoal (userName := name) <|
-                mkAppN (mkConst ``Aligned) #[toExpr 64, spEff.value, toExpr 4]
-
-            trace[Tactic.sym] "created subgoal to show alignment:\n{subGoal}"
-            let subGoal? ← do
-              let (ctx, simprocs) ←
-                LNSymSimpContext
-                  (config := {failIfUnchanged := false, decide := true})
-                  (decls := #[hSp])
-              LNSymSimp subGoal ctx simprocs
-
-            if let some subGoal := subGoal? then
-              trace[Tactic.sym] "subgoal got simplified to:\n{subGoal}"
-              appendGoals [subGoal]
-            else
-              trace[Tactic.sym] "subgoal got closed by simplification"
-
-            let stackAlignmentProof? := some <|
-              mkAppN (mkConst ``CheckSPAlignment_of_r_sp_aligned)
-                #[eff.currentState, spEff.value, spEff.proof, hAligned]
-            pure { eff with stackAlignmentProof? }
+    if let some hSp := c.effects.stackAlignmentProof? then
+      withVerboseTraceNode m!"discharging side condiitions" <| do
+        for subGoal in eff.sideConditions do
+          trace[Tactic.sym] "attempting to discharge side-condition:\n  {subGoal}"
+          let subGoal? ← do
+            let (ctx, simprocs) ←
+              LNSymSimpContext
+                (config := {failIfUnchanged := false, decide := true})
+                (exprs := #[hSp])
+            LNSymSimp subGoal ctx simprocs
+
+          if let some subGoal := subGoal? then
+            trace[Tactic.sym] "subgoal got simplified to:\n{subGoal}"
+            subGoal.setTag (.mkSimple s!"h_{← getNextStateName}_sp_aligned")
+            appendGoals [subGoal]
+          else
+            trace[Tactic.sym] "subgoal got closed by simplification"
+    else
+      appendGoals eff.sideConditions
+    eff := { eff with sideConditions := [] }
 
     -- Add new (non-)effect hyps to the context, and to the aggregation simpset
     withMainContext' <| do
@@ -251,10 +233,14 @@ 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
+  /- `withCurHeartbeats` sets the initial heartbeats to the current heartbeats,
+  effectively resetting our heartbeat budget back to the maximum. -/
+  withCurrHeartbeats <| do
+
   let stateNumber ← getCurrentStateNumber
-  let msg := m!"(sym1): simulating step {stateNumber}"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do
-    withTraceNode `Tactic.sym (fun _ => pure "verbose context") <| do
+  withTraceNode m!"(sym1): simulating step {stateNumber}" (tag:="sym1") <|
+  withMainContext' do
+    withVerboseTraceNode "verbose context" (tag := "infoDump") <| do
       traceSymContext
       trace[Tactic.sym] "Goal state:\n {← getMainGoal}"
 
@@ -262,12 +248,14 @@ def sym1 (whileTac : TSyntax `tactic) : SymM Unit := do
     let h_step   := Lean.mkIdent (.mkSimple s!"h_step_{stateNumber + 1}")
 
     unfoldRun (fun _ => evalTacticAndTrace whileTac)
+
     -- Add new state to local context
-    let hRunId      := mkIdent <|← getHRunName
-    let nextStateId := mkIdent <|← getNextStateName
-    evalTacticAndTrace <|← `(tactic|
-      init_next_step $hRunId:ident $stepi_eq:ident $nextStateId:ident
-    )
+    withTraceNode "initNextStep" (tag := "initNextStep") <| do
+      let hRunId      := mkIdent <|← getHRunName
+      let nextStateId := mkIdent <|← getNextStateName
+      evalTacticAndTrace <|← `(tactic|
+        init_next_step $hRunId:ident $stepi_eq:ident $nextStateId:ident
+      )
 
     -- Apply relevant pre-generated `stepi` lemma
     withMainContext' <| do
@@ -279,23 +267,18 @@ def sym1 (whileTac : TSyntax `tactic) : SymM Unit := do
     -- `simp` here
     withMainContext' <| do
       let hStep ← SymContext.findFromUserName h_step.getId
-      let lctx ← getLCtx
-      let decls := (← getThe SymContext).h_sp?.bind lctx.findFromUserName?
-      let decls := decls.toArray
-      -- If we know SP is aligned, `simp` with that fact
 
-      if !decls.isEmpty then
-        trace[Tactic.sym] "simplifying {hStep.toExpr} \
-          with {decls.map (·.toExpr)}"
-        -- If `decls` is empty, we have no more knowledge than before, so
-        -- everything that could've been `simp`ed, already should have been
-        let some goal ← do
-            let (ctx, simprocs) ← LNSymSimpContext
-              (config := {decide := false}) (decls := decls)
-            let goal ← getMainGoal
-            LNSymSimp goal ctx simprocs hStep.fvarId
-          | throwError "internal error: simp closed goal unexpectedly"
-        replaceMainGoal [goal]
+      -- If we know SP is aligned, `simp` with that fact
+      if let some hSp := (← getThe AxEffects).stackAlignmentProof? then
+        let msg := m!"simplifying {hStep.toExpr} with {hSp}"
+        withTraceNode msg (tag := "simplifyHStep") <| do
+          let some goal ← do
+              let (ctx, simprocs) ← LNSymSimpContext
+                (config := {decide := false}) (exprs := #[hSp])
+              let goal ← getMainGoal
+              LNSymSimp goal ctx simprocs hStep.fvarId
+            | throwError "internal error: simp closed goal unexpectedly"
+          replaceMainGoal [goal]
       else
         trace[Tactic.sym] "we have no relevant local hypotheses, \
           skipping simplification step"
@@ -314,48 +297,87 @@ def sym1 (whileTac : TSyntax `tactic) : SymM Unit := do
 
       traceHeartbeats
 
+/-! ## simp_mem -/
+
+/-- TODO(@bollu): implement `simpMem` to simplify the
+reads from memory in the given target.
+We *do not* want to iterate over all the hypotheses at this point,
+since that would be way too expensive.
+-/
+def simpMem (_c : SymContext) (mvar : MVarId) : SymM MVarId := do
+  /-
+  This should actually allow us to not need the follow processing in `Proofs/Popcount32`:
+  simp only [←Memory.mem_eq_iff_read_mem_bytes_eq] at *
+  simp only [memory_rules] at *
+  intro n addr h_separate
+  -- (TODO @alex/@bollu) Can we hope to make this shorter after the marriage
+  -- of `sym_n` and `simp_mem`?
+  simp_mem
+  sym_aggregate
+  simp only [*, bitvec_rules]
+  sym_aggregate
+  -/
+  let gs ← getGoals
+  setGoals [mvar]
+  evalTactic (← `(tactic| try simp_mem))
+  let gs' ← getGoals
+  match gs' with
+  | [g'] =>
+     setGoals gs
+     return g'
+  | [] => do
+    throwError "expected `simp_mem` to produce exactly one goal, but it was too clever and closed all goals."
+  | _ => do
+    throwError "expected `simp_mem` to produce only a single goal, but it produced more than one goal: {gs'}"
+
+/-! ## sym_n preprocessing -/
+
 /-- `ensureLessThanRunSteps n` will
 - log a warning and return `m`, if `runSteps? = some m` and `m < n`, or
 - return `n` unchanged, otherwise  -/
 def ensureAtMostRunSteps (n : Nat) : SymM Nat := do
-  let ctx ← getThe SymContext
-  match ctx.runSteps? with
-  | none => pure n
-  | some runSteps =>
-      if n ≤ runSteps then
-        pure n
-      else
-        withMainContext <| do
-          let hRun ← ctx.hRunDecl
-          logWarning m!"Symbolic simulation is limited to at most {runSteps} \
-            steps, because {hRun.toExpr} is of type:\n  {hRun.type}"
-          pure runSteps
-  return n
+  withVerboseTraceNode "" (tag := "ensureAtMostRunSteps") <| do
+    let ctx ← getThe SymContext
+    match ctx.runSteps? with
+    | none => pure n
+    | some runSteps =>
+        if n ≤ runSteps then
+          pure n
+        else
+          withMainContext <| do
+            let hRun ← ctx.hRunDecl
+            logWarning m!"Symbolic simulation is limited to at most {runSteps} \
+              steps, because {hRun.toExpr} is of type:\n  {hRun.type}"
+            pure runSteps
+    return n
 
 /-- Check that the step-thoerem corresponding to the current PC value exists,
 and throw a user-friendly error, pointing to `#genStepEqTheorems`,
 if it does not. -/
-def assertStepTheoremsGenerated : SymM Unit := do
-  let c ← getThe SymContext
-  let pc := c.pc.toHexWithoutLeadingZeroes
-  if !c.programInfo.instructions.contains c.pc then
-    let pcEff ← AxEffects.getFieldM .PC
-    throwError "\
-      Program {c.program} has no instruction at address {c.pc}.
-
-      We inferred this address as the program-counter from {pcEff.proof}, \
-      which has type:
-        {← inferType pcEff.proof}"
-
-  let step_thm := Name.str c.program ("stepi_eq_0x" ++ pc)
-  try
-    let _ ← getConstInfo step_thm
-  catch err =>
-    throwErrorAt err.getRef "{err.toMessageData}\n
-Did you remember to generate step theorems with:
-  #genStepEqTheorems {c.program}"
--- TODO: can we make this error ^^ into a `Try this:` suggestion that
---       automatically adds the right command just before the theorem?
+def assertStepTheoremsGenerated : SymM Unit :=
+  withVerboseTraceNode "" (tag := "assertStepTheoremsGenerated") <| do
+    let c ← getThe SymContext
+    let pc := c.pc.toHexWithoutLeadingZeroes
+    if !c.programInfo.instructions.contains c.pc then
+      let pcEff ← AxEffects.getFieldM .PC
+      throwError "\
+        Program {c.program} has no instruction at address {c.pc}.
+
+        We inferred this address as the program-counter from {pcEff.proof}, \
+        which has type:
+          {← inferType pcEff.proof}"
+
+    let step_thm := Name.str c.program ("stepi_eq_0x" ++ pc)
+    try
+      let _ ← getConstInfo step_thm
+    catch err =>
+      throwErrorAt err.getRef "{err.toMessageData}\n
+  Did you remember to generate step theorems with:
+    #genStepEqTheorems {c.program}"
+  -- TODO: can we make this error ^^ into a `Try this:` suggestion that
+  --       automatically adds the right command just before the theorem?
+
+/-! ## sym_n -/
 
 /- used in `sym_n` tactic to specify an initial state -/
 syntax sym_at := "at" ident
@@ -415,34 +437,37 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
         sym1 whileTac
 
     traceHeartbeats "symbolic simulation total"
-    let c ← getThe SymContext
-    -- Check if we can substitute the final state
-    if c.runSteps? = some 0 then
-      let msg := do
-        let hRun ← userNameToMessageData c.h_run
-        pure m!"runSteps := 0, substituting along {hRun}"
-      withTraceNode `Tactic.sym (fun _ => msg) <| withMainContext' do
-        let sfEq ← mkEq (← getCurrentState) c.finalState
-
-        let goal ← getMainGoal
-        trace[Tactic.sym] "original goal:\n{goal}"
-        let ⟨hEqId, goal⟩ ← do
-          let hRun ← SymContext.findFromUserName c.h_run
-          goal.note `this (← mkEqSymm hRun.toExpr) sfEq
-        goal.withContext <| do
-          trace[Tactic.sym] "added {← userNameToMessageData `this} of type \
-            {sfEq} in:\n{goal}"
-
-        let goal ← subst goal hEqId
-        trace[Tactic.sym] "performed subsitutition in:\n{goal}"
-
-        replaceMainGoal [goal]
-
-    -- Rudimentary aggregation: we feed all the axiomatic effect hypotheses
-    -- added while symbolically evaluating to `simp`
-    let msg := m!"aggregating (non-)effects"
-    withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do
-      let goal? ← LNSymSimp (← getMainGoal) c.aggregateSimpCtx c.aggregateSimprocs
-      replaceMainGoal goal?.toList
-
-    traceHeartbeats "final usage"
+    withCurrHeartbeats <|
+    withTraceNode "Post processing" (tag := "postProccessing") <| do
+      let c ← getThe SymContext
+      -- Check if we can substitute the final state
+      if c.runSteps? = some 0 then
+        let msg := do
+          let hRun ← userNameToMessageData c.h_run
+          pure m!"runSteps := 0, substituting along {hRun}"
+        withMainContext' <|
+        withTraceNode `Tactic.sym (fun _ => msg) <| do
+          let sfEq ← mkEq (← getCurrentState) c.finalState
+
+          let goal ← getMainGoal
+          trace[Tactic.sym] "original goal:\n{goal}"
+          let ⟨hEqId, goal⟩ ← do
+            let hRun ← SymContext.findFromUserName c.h_run
+            goal.note `this (← mkEqSymm hRun.toExpr) sfEq
+          goal.withContext <| do
+            trace[Tactic.sym] "added {← userNameToMessageData `this} of type \
+              {sfEq} in:\n{goal}"
+
+          let goal ← subst goal hEqId
+          trace[Tactic.sym] "performed subsitutition in:\n{goal}"
+          replaceMainGoal [goal]
+
+      -- Rudimentary aggregation: we feed all the axiomatic effect hypotheses
+      -- added while symbolically evaluating to `simp`
+      withMainContext' <|
+      withTraceNode m!"aggregating (non-)effects" (tag := "aggregateEffects") <| do
+        let goal? ← LNSymSimp (← getMainGoal) c.aggregateSimpCtx c.aggregateSimprocs
+        let goal? ← goal?.mapM (simpMem c)
+        replaceMainGoal goal?.toList
+
+      traceHeartbeats "aggregation"
diff --git a/Tactics/Sym/AxEffects.lean b/Tactics/Sym/AxEffects.lean
index 8c8a6aa5..24971f43 100644
--- a/Tactics/Sym/AxEffects.lean
+++ b/Tactics/Sym/AxEffects.lean
@@ -8,10 +8,13 @@ import Arm.State
 import Tactics.Common
 import Tactics.Attr
 import Tactics.Simp
+import Tactics.Sym.Common
+import Tactics.Sym.MemoryEffects
 
 import Std.Data.HashMap
 
 open Lean Meta
+open Sym (withTraceNode withVerboseTraceNode)
 
 /-- A reflected `ArmState` field, see `AxEffects.fields` for more context -/
 structure AxEffects.FieldEffect where
@@ -57,17 +60,8 @@ structure AxEffects where
     where `f₁, ⋯, fₙ` are the keys of `fields`
   -/
   nonEffectProof : Expr
-  /-- An expression of a (potentially empty) sequence of `write_mem`s
-  to the initial state, which describes the effects on memory.
-  See `memoryEffectProof` for more detail -/
-  memoryEffect : Expr
-  /-- An expression that contains the proof of:
-    ```lean
-    ∀ n addr,
-      read_mem_bytes n addr <currentState>
-      = read_mem_bytes n addr <memoryEffect>
-    ``` -/
-  memoryEffectProof : Expr
+  /-- The memory effects -/
+  memoryEffects : MemoryEffects
   /-- A proof that `<currentState>.program = <initialState>.program` -/
   programProof : Expr
   /-- An optional proof of `CheckSPAlignment <currentState>`.
@@ -78,20 +72,24 @@ structure AxEffects where
   However, if SP is written to, no effort is made to prove alignment of the
   new value; the field will be set to `none` -/
   stackAlignmentProof? : Option Expr
+
+  /-- `sideContitions` are proof obligations that come up during effect
+  characterization. -/
+  sideConditions : List MVarId
   deriving Repr
 
 namespace AxEffects
 
-/-! ## Monad getters -/
+/-! ## Monadic getters -/
 
-section Monad
+section MonadicGetters
 variable {m} [Monad m] [MonadReaderOf AxEffects m]
 
 def getCurrentState       : m Expr := do return (← read).currentState
 def getInitialState       : m Expr := do return (← read).initialState
 def getNonEffectProof     : m Expr := do return (← read).nonEffectProof
-def getMemoryEffect       : m Expr := do return (← read).memoryEffect
-def getMemoryEffectProof  : m Expr := do return (← read).memoryEffectProof
+def getMemoryEffect       : m Expr := do return (← read).memoryEffects.effects
+def getMemoryEffectProof  : m Expr := do return (← read).memoryEffects.proof
 def getProgramProof       : m Expr := do return (← read).programProof
 
 def getStackAlignmentProof? : m (Option Expr) := do
@@ -111,7 +109,7 @@ def getCurrentStateName : m Name := do
       | throwError "error: unknown fvar: {state}"
     return decl.userName
 
-end Monad
+end MonadicGetters
 
 /-! ## Initial Reflected State -/
 
@@ -126,21 +124,14 @@ def initial (state : Expr) : AxEffects where
     -- `fun f => rfl`
     mkLambda `f .default (mkConst ``StateField) <|
       mkEqReflArmState <| mkApp2 (mkConst ``r) (.bvar 0) state
-  memoryEffect      := state
-  memoryEffectProof :=
-    -- `fun n addr => rfl`
-    mkLambda `n .default (mkConst ``Nat) <|
-      let bv64 := mkApp (mkConst ``BitVec) (toExpr 64)
-      mkLambda `addr .default bv64 <|
-        mkApp2 (.const ``Eq.refl [1])
-          (mkApp (mkConst ``BitVec) <| mkNatMul (.bvar 1) (toExpr 8))
-          (mkApp3 (mkConst ``read_mem_bytes) (.bvar 1) (.bvar 0) state)
+  memoryEffects     := .initial state
   programProof      :=
     -- `rfl`
     mkAppN (.const ``Eq.refl [1]) #[
       mkConst ``Program,
       mkApp (mkConst ``ArmState.program) state]
   stackAlignmentProof? := none
+  sideConditions := []
 
 /-! ## ToMessageData -/
 
@@ -159,47 +150,23 @@ instance : ToMessageData AxEffects where
       currentState := {eff.currentState},
       fields := {eff.fields},
       nonEffectProof := {eff.nonEffectProof},
-      memoryEffect := {eff.memoryEffect},
-      memoryEffectProof := {eff.memoryEffectProof},
+      memoryEffects := {eff.memoryEffects},
       programProof := {eff.programProof}
     }"
 
 private def traceCurrentState (eff : AxEffects)
-    (header : MessageData := "current state") :
-    MetaM Unit :=
-  withTraceNode `Tactic.sym (fun _ => pure header) do
+    (header : MessageData := "current state") : MetaM Unit :=
+  withTraceNode header <| do
     trace[Tactic.sym] "{eff}"
 
 /-! ## Helpers -/
 
-/--
-Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`.
-
-Rewrites with a fresh metavariable as the ambient goal.
-Fails if the rewrite produces any subgoals.
--/
--- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477
-private def rewrite (e eq : Expr) : MetaM Expr := do
-  let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq
-    | throwError "Expr.rewrite may not produce subgoals."
-  return eq'
-
-/--
-Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`.
-
-Rewrites with a fresh metavariable as the ambient goal.
-Fails if the rewrite produces any subgoals.
--/
--- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477
-private def rewriteType (e eq : Expr) : MetaM Expr := do
-  mkEqMP (← rewrite (← inferType e) eq) e
-
 /-- Given a `field` such that `fields ∉ eff.fields`, return a proof of
   `r field <currentState> = r field <initialState>`
 by constructing an application of `eff.nonEffectProof` -/
 partial def mkAppNonEffect (eff : AxEffects) (field : Expr) : MetaM Expr := do
   let msg := m!"constructing application of non-effects proof"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+  withTraceNode msg (tag := "mkAppNonEffect") <| do
     trace[Tactic.sym] "nonEffectProof: {eff.nonEffectProof}"
 
     let nonEffectProof := mkApp eff.nonEffectProof field
@@ -218,8 +185,7 @@ partial def mkAppNonEffect (eff : AxEffects) (field : Expr) : MetaM Expr := do
 /-- Get the value for a field, if one is stored in `eff.fields`,
 or assemble an instantiation of the non-effects proof otherwise -/
 def getField (eff : AxEffects) (fld : StateField) : MetaM FieldEffect :=
-  let msg := m!"getField {fld}"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+  withTraceNode m!"getField {fld}" (tag := "getField") <| do
     eff.traceCurrentState
 
     if let some val := eff.fields.get? fld then
@@ -231,7 +197,7 @@ def getField (eff : AxEffects) (fld : StateField) : MetaM FieldEffect :=
       let proof  ← eff.mkAppNonEffect (toExpr fld)
       pure { value, proof }
 
-section Monad
+section MonadicGettersAndSetters
 variable {m} [Monad m] [MonadLiftT MetaM m]
 
 variable [MonadReaderOf AxEffects m] in
@@ -259,7 +225,7 @@ This is a specialization of `setFieldEffect`. -/
 def setErrorProof (proof : Expr) : m Unit :=
   setFieldEffect .ERR { value := mkConst ``StateError.None, proof }
 
-end Monad
+end MonadicGettersAndSetters
 
 /-! ## Update a Reflected State -/
 
@@ -270,9 +236,8 @@ and all other fields are updated accordingly.
 Note that no effort is made to preserve `currentStateEq`; it is set to `none`!
 -/
 private def update_write_mem (eff : AxEffects) (n addr val : Expr) :
-    MetaM AxEffects := do
-  trace[Tactic.sym] "adding write of {n} bytes of value {val} \
-    to memory address {addr}"
+    MetaM AxEffects :=
+  Sym.withTraceNode m!"processing: write_mem {n} {addr} {val} …" (tag := "updateWriteMem") <| do
 
   -- Update each field
   let fields ← eff.fields.toList.mapM fun ⟨fld, {value, proof}⟩ => do
@@ -290,11 +255,10 @@ private def update_write_mem (eff : AxEffects) (n addr val : Expr) :
     mkLambdaFVars args proof
     -- ^^ `fun f ... => Eq.trans (@r_of_write_mem_bytes f ...) <proof>`
 
-  -- Update the memory effects proof
-  let memoryEffectProof :=
-    -- `read_mem_bytes_write_mem_bytes_of_read_mem_eq <memoryEffectProof> ...`
-    mkAppN (mkConst ``read_mem_bytes_write_mem_bytes_of_read_mem_eq)
-      #[eff.currentState, eff.memoryEffect, eff.memoryEffectProof, n, addr, val]
+  -- Update the memory effects
+  let memoryEffects ←
+    eff.memoryEffects.updateWriteMem eff.currentState  n addr val
+
 
   -- Update the program proof
   let programProof ←
@@ -304,20 +268,23 @@ private def update_write_mem (eff : AxEffects) (n addr val : Expr) :
         #[eff.currentState, n, addr, val])
       eff.programProof
 
+  -- Update the stack alignment proof
+  let stackAlignmentProof? := eff.stackAlignmentProof?.map fun proof =>
+    mkAppN (mkConst ``CheckSPAligment_write_mem_bytes_of)
+      #[eff.currentState, n, addr, val, proof]
+
   -- Assemble the result
-  let addWrite (e : Expr) :=
-    -- `@write_mem_bytes <n> <addr> <val> <e>`
-    mkApp4 (mkConst ``write_mem_bytes) n addr val e
+  let currentState := -- `@write_mem_bytes <n> <addr> <val> <currentState>`
+    mkApp4 (mkConst ``write_mem_bytes) n addr val eff.currentState
   let eff := { eff with
-    currentState    := addWrite eff.currentState
+    currentState
     fields          := .ofList fields
     nonEffectProof
-    memoryEffect    := addWrite eff.memoryEffect
-    memoryEffectProof
+    memoryEffects
     programProof
+    stackAlignmentProof?
   }
-  withTraceNode `Tactic.sym (fun _ => pure "new state") <| do
-      trace[Tactic.sym] "{eff}"
+  eff.traceCurrentState
   return eff
 
 /-- Execute `w <fld> <val>` against the state stored in `eff`
@@ -328,8 +295,8 @@ Note that no effort is made to preserve `currentStateEq`; it is set to `none`!
 -/
 private def update_w (eff : AxEffects) (fld val : Expr) :
     MetaM AxEffects := do
+  Sym.withTraceNode m!"processing: w {fld} {val} …" (tag := "updateWrite") <| do
   let rField ← reflectStateField fld
-  trace[Tactic.sym] "adding write of value {val} to register {rField}"
 
   -- Update all other fields
   let fields ←
@@ -385,11 +352,8 @@ private def update_w (eff : AxEffects) (fld val : Expr) :
         withLocalDeclD name h_neq_type fun h_neq =>
           k (args.push h_neq) h_neq
 
-  -- Update the memory effect proof
-  let memoryEffectProof :=
-    -- `read_mem_bytes_w_of_read_mem_eq ...`
-    mkAppN (mkConst ``read_mem_bytes_w_of_read_mem_eq)
-      #[eff.currentState, eff.memoryEffect, eff.memoryEffectProof, fld, val]
+  -- Update the memory effects
+  let memoryEffects ← eff.memoryEffects.updateWrite eff.currentState fld val
 
   -- Update the program proof
   let programProof ←
@@ -398,45 +362,61 @@ private def update_w (eff : AxEffects) (fld val : Expr) :
       (mkAppN (mkConst ``w_program) #[fld, val, eff.currentState])
       eff.programProof
 
+  -- Update the stack alignment proof
+  let mut sideConditions := eff.sideConditions
+  let mut stackAlignmentProof? := eff.stackAlignmentProof?
+  if let some proof := stackAlignmentProof? then
+    if rField ≠ StateField.SP then
+      let hNeq ← mkDecideProof <|
+        mkApp3 (.const ``Ne [1])
+          (mkConst ``StateField) (toExpr StateField.SP) fld
+      stackAlignmentProof? := mkAppN (mkConst ``CheckSPAligment_w_of_ne_sp_of)
+        #[fld, eff.currentState, val, hNeq, proof]
+    else
+      let hAligned ← mkFreshExprMVar (some <|
+        mkApp3 (mkConst ``Aligned) (toExpr 64) val (toExpr 4)
+      )
+      sideConditions := hAligned.mvarId! :: sideConditions
+      stackAlignmentProof? := mkAppN (mkConst ``CheckSPAligment_w_sp_of)
+        #[val, eff.currentState, hAligned]
+
   -- Assemble the result
   let eff := { eff with
     currentState    := mkApp3 (mkConst ``w) fld val eff.currentState
     fields := Std.HashMap.ofList fields
     nonEffectProof
-    -- memory effects are unchanged
-    memoryEffectProof
+    memoryEffects
     programProof
+    stackAlignmentProof?
+    sideConditions
   }
   eff.traceCurrentState "new state"
   return eff
 
-/-- Throw an error if `e` is not of type `expectedType` -/
-private def assertHasType (e expectedType : Expr) : MetaM Unit := do
-  let eType ← inferType e
-  if !(←isDefEq eType expectedType) then
-    throwError "{e} {← mkHasTypeButIsExpectedMsg eType expectedType}"
+/-- Given an expression `e : ArmState`,
+which is a sequence of `w`/`write_mem`s to `eff.currentState`,
+return an `AxEffects` where `e` is the new `currentState`. -/
+private partial def updateWithExprAux (eff : AxEffects) (e : Expr) : MetaM AxEffects := do
+  match_expr e with
+  | write_mem_bytes n addr val e =>
+      let eff ← eff.updateWithExprAux e
+      eff.update_write_mem n addr val
+
+  | w field value e =>
+      let eff ← eff.updateWithExprAux e
+      eff.update_w field value
 
-private def assertIsDefEq (e expected : Expr) : MetaM Unit := do
-  if !(←isDefEq e expected) then
-    throwError "expected:\n  {expected}\nbut found:\n  {e}"
+  | _ =>
+      assertIsDefEq e eff.currentState
+      return eff
 
 /-- Given an expression `e : ArmState`,
 which is a sequence of `w`/`write_mem`s to `eff.currentState`,
 return an `AxEffects` where `e` is the new `currentState`. -/
 partial def updateWithExpr (eff : AxEffects) (e : Expr) : MetaM AxEffects := do
   let msg := m!"Updating effects with writes from: {e}"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do match_expr e with
-    | write_mem_bytes n addr val e =>
-        let eff ← eff.updateWithExpr e
-        eff.update_write_mem n addr val
-
-    | w field value e =>
-        let eff ← eff.updateWithExpr e
-        eff.update_w field value
-
-    | _ =>
-        assertIsDefEq e eff.currentState
-        return eff
+  withTraceNode msg (tag := "updateWithExpr") <|
+    updateWithExprAux eff e
 
 /-- Given an expression `e : ArmState`,
 which is a sequence of `w`/`write_mem`s to the some state `s`,
@@ -451,62 +431,67 @@ def fromExpr (e : Expr) : MetaM AxEffects := do
   let eff ← eff.updateWithExpr e
   return { eff with initialState := ← instantiateMVars eff.initialState}
 
-
 /-- Given a proof `eq : s = <currentState>`,
 set `s` to be the new `currentState`, and update all proofs accordingly -/
 def adjustCurrentStateWithEq (eff : AxEffects) (s eq : Expr) :
     MetaM AxEffects := do
-  withTraceNode `Tactic.sym (fun _ => pure "adjusting `currenstState`") do
-    eff.traceCurrentState
+  Sym.withTraceNode m!"adjustCurrentStateWithEq" (tag := "adjustCurrentStateWithEq") do
     trace[Tactic.sym] "rewriting along {eq}"
+    eff.traceCurrentState
+
     assertHasType eq <| mkEqArmState s eff.currentState
     let eq ← mkEqSymm eq
 
     let currentState := s
 
     let fields ← eff.fields.toList.mapM fun (field, fieldEff) => do
-      withTraceNode `Tactic.sym (fun _ => pure m!"rewriting field {field}") do
+      withTraceNode m!"rewriting field {field}" (tag := "rewriteField") do
         trace[Tactic.sym] "original proof: {fieldEff.proof}"
         let proof ← rewriteType fieldEff.proof eq
         trace[Tactic.sym] "new proof: {proof}"
         pure (field, {fieldEff with proof})
     let fields := .ofList fields
 
-    let nonEffectProof ← rewriteType eff.nonEffectProof eq
-    let memoryEffectProof ← rewriteType eff.memoryEffectProof eq
-    -- ^^ TODO: what happens if `memoryEffect` is the same as `currentState`?
-    --    Presumably, we would *not* want to encapsulate `memoryEffect` here
-    let programProof ← rewriteType eff.programProof eq
+    Sym.withTraceNode m!"rewriting other proofs" (tag := "rewriteMisc") <| do
+      let nonEffectProof ← rewriteType eff.nonEffectProof eq
+      let memoryEffects ← eff.memoryEffects.adjustCurrentStateWithEq eq
+      let programProof ← rewriteType eff.programProof eq
+      let stackAlignmentProof? ← eff.stackAlignmentProof?.mapM
+        (rewriteType · eq)
 
-    return { eff with
-      currentState, fields, nonEffectProof, memoryEffectProof, programProof
-    }
+      return { eff with
+        currentState, fields, nonEffectProof, memoryEffects, programProof,
+        stackAlignmentProof?
+      }
 
 /-- Given a proof `eq : ?s = <sequence of w/write_mem to eff.currentState>`,
 where `?s` and `?s0` are arbitrary `ArmState`s,
 return an `AxEffect` with the rhs of the equality as the current state,
 and the (non-)effects updated accordingly -/
 def updateWithEq (eff : AxEffects) (eq : Expr) : MetaM AxEffects :=
-  let msg := m!"Building effects with equality: {eq}"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+  withTraceNode m!"Building effects with equality: {eq}"
+                (tag := "updateWithEq") <| do
     let s ← mkFreshExprMVar mkArmState
     let rhs ← mkFreshExprMVar mkArmState
     assertHasType eq <| mkEqArmState s rhs
 
     let eff ← eff.updateWithExpr (← instantiateMVars rhs)
     let eff ← eff.adjustCurrentStateWithEq s eq
-    withTraceNode `Tactic.sym (fun _ => pure "new state") do
-      trace[Tactic.sym] "{eff}"
+    eff.traceCurrentState "new state"
     return eff
 
 /-- Given a proof `eq : ?s = <sequence of w/write_mem to ?s0>`,
 where `?s` and `?s0` are arbitrary `ArmState`s,
 return an `AxEffect` with `?s0` as the initial state,
 the rhs of the equality as the current state,
-and the (non-)effects updated accordingly -/
-def fromEq (eq : Expr) : MetaM AxEffects := do
+and the (non-)effects updated accordingly
+
+One can optionally pass in a proof that `?s0` has a well-aligned stack pointer.
+-/
+def fromEq (eq : Expr) (stackAlignmentProof? : Option Expr := none) :
+    MetaM AxEffects := do
   let s0 ← mkFreshExprMVar mkArmState
-  let eff := initial s0
+  let eff := { initial s0 with stackAlignmentProof? }
   let eff ← eff.updateWithEq eq
   return { eff with initialState := ← instantiateMVars eff.initialState}
 
@@ -534,8 +519,7 @@ Note: throws an error when `initialState = currentState` *and*
 the field already has a value stored, as the rewrite might produce expressions
 of unexpected types. -/
 def withField (eff : AxEffects) (eq : Expr) : MetaM AxEffects := do
-  let msg := m!"withField {eq}"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+  withTraceNode m!"withField {eq}" (tag := "withField") <| do
     eff.traceCurrentState
     let fieldE ← mkFreshExprMVar (mkConst ``StateField)
     let value ← mkFreshExprMVar none
@@ -570,34 +554,6 @@ def withField (eff : AxEffects) (eq : Expr) : MetaM AxEffects := do
       let fields := eff.fields.insert field { value, proof }
       return { eff with fields }
 
-/-- Given a proof of `CheckSPAlignment <initialState>`,
-attempt to transport it to a proof of `CheckSPAlignment <currentState>`
-and store that proof in `stackAlignmentProof?`.
-
-Returns `none` if the proof failed to be transported,
-i.e., if SP was written to. -/
-def withStackAlignment? (eff : AxEffects) (spAlignment : Expr) :
-    MetaM (Option AxEffects) := do
-  let msg := m!"withInitialStackAlignment? {spAlignment}"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do
-    eff.traceCurrentState
-
-    let { value, proof } ← eff.getField StateField.SP
-    let expected :=
-      mkApp2 (mkConst ``r) (toExpr <| StateField.SP) eff.initialState
-    trace[Tactic.sym] "checking whether value:\n  {value}\n\
-      is syntactically equal to expected value\n  {expected}"
-    if value != expected then
-      trace[Tactic.sym] "failed to transport proof:
-        expected value to be {expected}, but found {value}"
-      return none
-
-    let stackAlignmentProof? := some <|
-      mkAppN (mkConst ``CheckSPAlignment_of_r_sp_eq)
-        #[eff.initialState, eff.currentState, proof, spAlignment]
-    trace[Tactic.sym] "constructed stackAlignmentProof: {stackAlignmentProof?}"
-    return some { eff with stackAlignmentProof? }
-
 /-! ## Composition -/
 
 /- TODO: write a function that combines two effects `left` and `right`,
@@ -621,8 +577,8 @@ NOTE: does not necessarily validate *which* type an expression has,
 validation will still pass if types are different to those we claim in the
 docstrings -/
 def validate (eff : AxEffects) : MetaM Unit := do
-  let msg := "validating that the axiomatic effects are well-formed"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+  Sym.withTraceNode "validating that the axiomatic effects are well-formed"
+                (tag := "validate") <| do
     eff.traceCurrentState
 
     assertHasType eff.initialState mkArmState
@@ -632,13 +588,13 @@ def validate (eff : AxEffects) : MetaM Unit := do
       check fieldEff.value
       check fieldEff.proof
 
+    eff.memoryEffects.validate
     check eff.nonEffectProof
-    check eff.memoryEffect
-    check eff.memoryEffectProof
     check eff.programProof
     if let some h := eff.stackAlignmentProof? then
       check h
 
+
 /-! ## Tactic Environment -/
 section Tactic
 open Elab.Tactic
@@ -657,8 +613,8 @@ that was just added to the local context -/
 def addHypothesesToLContext (eff : AxEffects) (hypPrefix : String := "h_")
     (mvar : Option MVarId := none) :
     TacticM AxEffects :=
-  let msg := m!"adding hypotheses to local context"
-  withTraceNode `Tactic.sym (fun _ => pure msg) do
+  Sym.withTraceNode m!"adding hypotheses to local context"
+                (tag := "addHypothesesToLContext") do
     eff.traceCurrentState
     let mut goal ← mvar.getDM getMainGoal
 
@@ -683,12 +639,14 @@ def addHypothesesToLContext (eff : AxEffects) (hypPrefix : String := "h_")
     let nonEffectProof := Expr.fvar nonEffectProof
     goal := goal'
 
-    trace[Tactic.sym] "adding memory effects with {eff.memoryEffectProof}"
+    trace[Tactic.sym] "adding memory effects with {eff.memoryEffects.proof}"
     let ⟨memoryEffectProof, goal'⟩ ← goal.withContext do
       let name := .mkSimple s!"{hypPrefix}memory_effects"
-      let proof := eff.memoryEffectProof
+      let proof := eff.memoryEffects.proof
       replaceOrNote goal name proof
-    let memoryEffectProof := Expr.fvar memoryEffectProof
+    let memoryEffects := { eff.memoryEffects with
+      proof := Expr.fvar memoryEffectProof
+    }
     goal := goal'
 
     trace[Tactic.sym] "adding program hypothesis with {eff.programProof}"
@@ -714,15 +672,15 @@ def addHypothesesToLContext (eff : AxEffects) (hypPrefix : String := "h_")
 
     replaceMainGoal [goal]
     return {eff with
-      fields, nonEffectProof, memoryEffectProof, programProof,
+      fields, nonEffectProof, memoryEffects, programProof,
       stackAlignmentProof?
     }
 where
   replaceOrNote (goal : MVarId)
       (h : Name) (v : Expr) (t? : Option Expr := none) :
       MetaM (FVarId × MVarId) :=
-    let msg := m!"adding {h} to the local context"
-    withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+    withTraceNode m!"adding {h} to the local context"
+                  (tag := "replaceOrNote") <| do
       trace[Tactic.sym] "with value {v} and type {t?}"
       if let some decl := (← getLCtx).findFromUserName? h then
         let ⟨fvar, goal, _⟩ ← goal.replace decl.fvarId v t?
@@ -734,8 +692,8 @@ where
 /-- Return an array of `SimpTheorem`s of the proofs contained in
 the given `AxEffects` -/
 def toSimpTheorems (eff : AxEffects) : MetaM (Array SimpTheorem) := do
-  let msg := m!"computing SimpTheorems for (non-)effect hypotheses"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+  Sym.withTraceNode m!"computing SimpTheorems for (non-)effect hypotheses"
+                (tag := "toSimpTheorems") <| do
     let lctx ← getLCtx
     let baseName? :=
       if eff.currentState.isFVar then
@@ -747,8 +705,7 @@ def toSimpTheorems (eff : AxEffects) : MetaM (Array SimpTheorem) := do
 
     let add (thms : Array SimpTheorem) (e : Expr) (name : String)
         (prio : Nat := 1000) :=
-      let msg := m!"adding {e} with name {name}"
-      withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+      withTraceNode m!"adding {e} with name {name}" <| do
         let origin : Origin :=
           if e.isFVar then
             .fvar e.fvarId!
@@ -769,7 +726,7 @@ def toSimpTheorems (eff : AxEffects) : MetaM (Array SimpTheorem) := do
       thms ← add thms proof s!"field_{field}" (prio := 1500)
 
     thms ← add thms eff.nonEffectProof "nonEffectProof"
-    thms ← add thms eff.memoryEffectProof "memoryEffectProof"
+    thms ← add thms eff.memoryEffects.proof "memoryEffectProof"
     thms ← add thms eff.programProof "programProof"
     if let some stackAlignmentProof := eff.stackAlignmentProof? then
       thms ← add thms stackAlignmentProof "stackAlignmentProof"
diff --git a/Tactics/Sym/Common.lean b/Tactics/Sym/Common.lean
new file mode 100644
index 00000000..1c571cb7
--- /dev/null
+++ b/Tactics/Sym/Common.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Lean
+
+open Lean
+
+namespace Sym
+
+/-! ## Trace Nodes -/
+section Tracing
+variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadLiftT IO m]
+  [MonadRef m] [AddMessageContext m] [MonadOptions m] {ε : Type}
+  [MonadAlwaysExcept ε m] [MonadLiftT BaseIO m]
+
+def withTraceNode (msg : MessageData) (k : m α)
+    (collapsed : Bool := true)
+    (tag : String := "")
+    : m α := do
+  Lean.withTraceNode `Tactic.sym (fun _ => pure msg) k collapsed tag
+
+def withVerboseTraceNode (msg : MessageData) (k : m α)
+    (collapsed : Bool := true)
+    (tag : String := "")
+    : m α := do
+  Lean.withTraceNode `Tactic.sym.verbose (fun _ => pure msg) k collapsed tag
+
+/-- Create a trace note that folds `header` with `(NOTE: can be large)`,
+and prints `msg` under such a trace node.
+-/
+def traceLargeMsg (header : MessageData) (msg : MessageData) : MetaM Unit :=
+    withTraceNode m!"{header} (NOTE: can be large)" do
+      trace[Tactic.sym] msg
+
+end Tracing
diff --git a/Tactics/Sym/Context.lean b/Tactics/Sym/Context.lean
index 40979b2d..16f00785 100644
--- a/Tactics/Sym/Context.lean
+++ b/Tactics/Sym/Context.lean
@@ -9,6 +9,7 @@ import Lean.Meta
 import Arm.Exec
 import Tactics.Common
 import Tactics.Attr
+import Tactics.Sym.Common
 import Tactics.Sym.ProgramInfo
 import Tactics.Sym.AxEffects
 import Tactics.Sym.LCtxSearch
@@ -33,6 +34,7 @@ and is likely to be deprecated and removed in the near future. -/
 
 open Lean Meta Elab.Tactic
 open BitVec
+open Sym (withTraceNode withVerboseTraceNode)
 
 /-- A `SymContext` collects the names of various variables/hypotheses in
 the local context required for symbolic evaluation -/
@@ -77,9 +79,6 @@ structure SymContext where
   and we assume that no overflow happens
   (i.e., `base - x` can never be equal to `base + y`) -/
   pc : BitVec 64
-  /-- `h_sp?`, if present, is a local hypothesis of the form
-  `CheckSPAlignment state` -/
-  h_sp?  : Option Name
 
   /-- The `simp` context used for effect aggregation.
   This collects references to all (non-)effect hypotheses of the intermediate
@@ -159,17 +158,18 @@ def program : Name := c.programInfo.name
 
 /-- Find the local declaration that corresponds to a given name,
 or throw an error if no local variable of that name exists -/
-def findFromUserName (name : Name) : MetaM LocalDecl := do
-  let some decl := (← getLCtx).findFromUserName? name
-    | throwError "Unknown local variable `{name}`"
-  return decl
+def findFromUserName (name : Name) : MetaM LocalDecl :=
+  withVerboseTraceNode m!"[findFromUserName] {name}" <| do
+    let some decl := (← getLCtx).findFromUserName? name
+      | throwError "Unknown local variable `{name}`"
+    return decl
 
 /-- Find the local declaration that corresponds to `c.h_run`,
 or throw an error if no local variable of that name exists -/
 def hRunDecl : MetaM LocalDecl := do
   findFromUserName c.h_run
 
-section Monad
+section MonadicGetters
 variable {m} [Monad m] [MonadReaderOf SymContext m]
 
 def getCurrentStateNumber : m Nat := do return (← read).currentStateNumber
@@ -187,7 +187,7 @@ def getNextStateName : m Name := do
   let c ← read
   return Name.mkSimple s!"{c.state_prefix}{c.currentStateNumber + 1}"
 
-end Monad
+end MonadicGetters
 
 end
 
@@ -197,26 +197,18 @@ end
 This is not a `ToMessageData` instance because we need access to `MetaM` -/
 def toMessageData (c : SymContext) : MetaM MessageData := do
   let h_run ← userNameToMessageData c.h_run
-  let h_sp?  ← c.h_sp?.mapM userNameToMessageData
 
   return m!"\{ finalState := {c.finalState},
   runSteps? := {c.runSteps?},
   h_run := {h_run},
   program := {c.program},
   pc := {c.pc},
-  h_sp? := {h_sp?},
   state_prefix := {c.state_prefix},
   curr_state_number := {c.currentStateNumber},
   effects := {c.effects} }"
 
-variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadLiftT IO m]
-  [MonadRef m] [AddMessageContext m] [MonadOptions m] {ε : Type}
-  [MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] in
-def withSymTraceNode (msg : MessageData) (k : m α) : m α := do
-  withTraceNode `Tactic.sym (fun _ => pure msg) k
-
 def traceSymContext : SymM Unit :=
-  withTraceNode `Tactic.sym (fun _ => pure m!"SymContext: ") <| do
+  withTraceNode m!"SymContext: " <| do
     let m ← (← getThe SymContext).toMessageData
     trace[Tactic.sym] m
 
@@ -265,7 +257,6 @@ private def initial (state : Expr) : MetaM SymContext := do
       instructions := ∅
     }
     pc := 0
-    h_sp? := none
     aggregateSimpCtx,
     aggregateSimprocs,
     effects := AxEffects.initial state
@@ -400,9 +391,6 @@ protected def searchFor : SearchLCtxForM SymM Unit := do
       modifyThe AxEffects ({ · with
         stackAlignmentProof? := some decl.toExpr
       })
-      modifyThe SymContext ({· with
-        h_sp? := decl.userName
-      })
     )
 
   -- Find `r ?field currentState = ?value`
@@ -440,7 +428,7 @@ we create a new subgoal of this type.
 -/
 def fromMainContext (state? : Option Name) : TacticM SymContext := do
   let msg := m!"Building a `SymContext` from the local context"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do
+  withTraceNode msg (tag := "fromMainContext") <| withMainContext' do
   trace[Tactic.Sym] "state? := {state?}"
   let lctx ← getLCtx
 
@@ -473,18 +461,17 @@ evaluation:
   * the `currentStateNumber` is incremented
 -/
 def prepareForNextStep : SymM Unit := do
-  let s ← getNextStateName
-  let pc ← do
-    let { value, ..} ← AxEffects.getFieldM .PC
-    try
-      reflectBitVecLiteral 64 value
-    catch err =>
-      trace[Tactic.sym] "failed to reflect PC: {err.toMessageData}"
-      pure <| (← getThe SymContext).pc + 4
-
-  modifyThe SymContext (fun c => { c with
-    pc
-    h_sp?       := c.h_sp?.map (fun _ => .mkSimple s!"h_{s}_sp_aligned")
-    runSteps?   := (· - 1) <$> c.runSteps?
-    currentStateNumber := c.currentStateNumber + 1
-  })
+  withVerboseTraceNode "prepareForNextStep" (tag := "prepareForNextStep") <| do
+    let pc ← do
+      let { value, ..} ← AxEffects.getFieldM .PC
+      try
+        reflectBitVecLiteral 64 value
+      catch err =>
+        trace[Tactic.sym] "failed to reflect PC: {err.toMessageData}"
+        pure <| (← getThe SymContext).pc + 4
+
+    modifyThe SymContext (fun c => { c with
+      pc
+      runSteps?   := (· - 1) <$> c.runSteps?
+      currentStateNumber := c.currentStateNumber + 1
+    })
diff --git a/Tactics/Sym/MemoryEffects.lean b/Tactics/Sym/MemoryEffects.lean
new file mode 100644
index 00000000..cbebc4c6
--- /dev/null
+++ b/Tactics/Sym/MemoryEffects.lean
@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer, Siddharth Bhat
+-/
+
+import Arm.State
+import Tactics.Common
+import Tactics.Attr
+import Tactics.Simp
+import Tactics.Sym.Common
+
+import Std.Data.HashMap
+
+open Lean Meta
+
+structure MemoryEffects where
+  /-- An expression of a (potentially empty) sequence of `write_mem`s
+  to the initial state, which describes the effects on memory.
+  See `memoryEffectProof` for more detail -/
+  effects : Expr
+  /-- An expression that contains the proof of:
+    ```lean
+    ∀ n addr,
+      read_mem_bytes n addr <currentState>
+      = read_mem_bytes n addr <all memory effects so far, e.g. (write_mem_bytes n addr val s₀)>
+    ``` -/
+  proof : Expr
+deriving Repr
+
+instance : ToMessageData MemoryEffects where
+  toMessageData eff :=
+    m!"\
+    \{ effects := {eff.effects},
+      proof := {eff.proof
+    }"
+
+namespace MemoryEffects
+
+/-! ## Initial Reflected State -/
+
+/-- An initial `MemoryEffects`, representing no memory changes to the
+initial `state` -/
+def initial (state : Expr) : MemoryEffects where
+  effects := state
+  proof :=
+    -- `fun n addr => rfl`
+    mkLambda `n .default (mkConst ``Nat) <|
+      let bv64 := mkApp (mkConst ``BitVec) (toExpr 64)
+      mkLambda `addr .default bv64 <|
+        mkApp2 (.const ``Eq.refl [1])
+          (mkApp (mkConst ``BitVec) <| mkNatMul (.bvar 1) (toExpr 8))
+          (mkApp3 (mkConst ``read_mem_bytes) (.bvar 1) (.bvar 0) state)
+
+/-- Update the memory effects with a memory write -/
+def updateWriteMem (eff : MemoryEffects) (currentState : Expr)
+    (n addr val : Expr) :
+    MetaM MemoryEffects := do
+  let effects := mkApp4 (mkConst ``write_mem_bytes) n addr val eff.effects
+  let proof :=
+    -- `read_mem_bytes_write_mem_bytes_of_read_mem_eq <memoryEffectProof> ...`
+    mkAppN (mkConst ``read_mem_bytes_write_mem_bytes_of_read_mem_eq)
+      #[currentState, eff.effects, eff.proof, n, addr, val]
+  return { effects, proof }
+
+/-- Update the memory effects with a register write.
+
+This doesn't change the actual effect, but since the `currentState` has changed,
+we need to update proofs -/
+def updateWrite (eff : MemoryEffects) (currentState : Expr)
+    (fld val : Expr) :
+    MetaM MemoryEffects := do
+  let proof := -- `read_mem_bytes_w_of_read_mem_eq ...`
+    mkAppN (mkConst ``read_mem_bytes_w_of_read_mem_eq)
+      #[currentState, eff.effects, eff.proof, fld, val]
+  return { eff with proof }
+
+/-- Transport all proofs along an equality `eq : <currentState> = s`,
+so that `s` is the new `currentState` -/
+def adjustCurrentStateWithEq (eff : MemoryEffects) (eq : Expr) :
+    MetaM MemoryEffects := do
+  let proof ← rewriteType eff.proof eq
+    -- ^^ TODO: what happens if `memoryEffect` is the same as `currentState`?
+    --    Presumably, we would *not* want to encapsulate `memoryEffect` here
+  return { eff with proof }
+
+/-- Convert a `MemoryEffects` into a `MessageData` for logging. -/
+def toMessageData (eff : MemoryEffects) : MetaM MessageData := do
+  let out := m!"effects: {eff.effects}"
+  return out
+
+/-- Trace the current state of `MemoryEffects`. -/
+def traceCurrentState (eff : MemoryEffects) : MetaM Unit := do
+  Sym.traceLargeMsg "memoryEffects" (← eff.toMessageData)
+
+
+
+/-- type check all expressions stored in `eff`,
+throwing an error if one is not type-correct.
+
+In principle, the various `MemoryEffects` definitions should return only
+well-formed expressions, making `validate` a no-op.
+In practice, however, running `validate` is helpful for catching bugs in those
+definitions. Do note that typechecking might be a bit expensive, so we generally
+only call `validate` while debugging, not during normal execution.
+See also the `Tactic.sym.debug` option, which controls whether `validate` is
+called for each step of the `sym_n` tactic.
+
+NOTE: does not necessarily validate *which* type an expression has,
+validation will still pass if types are different to those we claim in the
+docstrings
+-/
+def validate (eff : MemoryEffects) : MetaM Unit := do
+  let msg := "validating that the axiomatic effects are well-formed"
+  Sym.withTraceNode msg do
+    eff.traceCurrentState
+    check eff.effects
+    assertHasType eff.effects mkArmState
+
+    check eff.proof
+
+end MemoryEffects
diff --git a/lakefile.lean b/lakefile.lean
index 7175ad63..66000295 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -33,6 +33,7 @@ lean_lib «Doc» where
   -- add library configuration options here
 
 lean_lib «Benchmarks» where
+  leanOptions := #[⟨`weak.benchmark.runs, (0 : Nat)⟩]
   -- add library configuration options here
 
 @[default_target]
diff --git a/scripts/benchmark.sh b/scripts/benchmark.sh
new file mode 100755
index 00000000..028b2bf4
--- /dev/null
+++ b/scripts/benchmark.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+LAKE=lake
+BENCH="$LAKE env lean -Dweak.benchmark.runs=5"
+OUT="data/benchmarks"
+
+timestamp=$(date +"%Y-%m-%d_%H%M%S")
+rev=$(git rev-parse --short HEAD)
+echo "HEAD is on $rev"
+out="$OUT/${timestamp}_${rev}"
+mkdir -p "$out"
+
+$LAKE build Benchmarks
+for file in "$@"; do
+    echo
+    echo + $file
+    echo
+    base="$(basename "$file" ".lean")"
+    $BENCH $file | tee "$out/$base"
+done
diff --git a/scripts/profile.sh b/scripts/profile.sh
new file mode 100755
index 00000000..ccc1433d
--- /dev/null
+++ b/scripts/profile.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+LAKE=lake
+PROF="$LAKE env lean -Dprofiler=true"
+OUT="data/profiles"
+
+timestamp=$(date +"%Y-%m-%d_%H%M%S")
+rev=$(git rev-parse --short HEAD)
+echo "HEAD is on $rev"
+out="$OUT/${timestamp}_${rev}"
+mkdir -p "$out"
+
+$LAKE build Benchmarks
+for file in "$@"; do
+    echo
+    echo + $file
+    echo
+    base="$(basename "$file" ".lean")"
+    $PROF -Dtrace.profiler.output="$out/$base.json" "$file" | tee "$base.log"
+done