diff --git a/Proofs/MultiInsts.lean b/Proofs/MultiInsts.lean
index ce2decf1..e23a8591 100644
--- a/Proofs/MultiInsts.lean
+++ b/Proofs/MultiInsts.lean
@@ -21,17 +21,16 @@ def test_program : Program :=
 theorem small_asm_snippet_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x12650c#64)
   (h_s0_program : s0.program = test_program)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_run : s_final = run 4 s0) :
   read_sfp 128 26#5 s_final = read_sfp 128 0#5 s0 ∧
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic Simulation
-  sym_n 4 h_s0_program
+  sym_n 4
   -- Wrapping up the result:
   unfold run at h_run
-  subst s_final s4
   simp_all (config := {decide := true}) only [state_simp_rules, minimal_theory, bitvec_rules]
   rw [@zeroExtend_eq 128]
   done
diff --git a/Proofs/Sha512_block_armv8.lean b/Proofs/Sha512_block_armv8.lean
index a1790b41..828834c3 100644
--- a/Proofs/Sha512_block_armv8.lean
+++ b/Proofs/Sha512_block_armv8.lean
@@ -26,22 +26,24 @@ def sha512_program_test_1 : Program :=
      ]
 
 -- set_option profiler true in
+-- set_option trace.profiler.output "new_sym.log" in
+-- set_option trace.profiler.output.pp true in
 -- set_option pp.deepTerms true in
 theorem sha512_program_test_1_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x126538#64)
   (h_s0_sp_aligned : CheckSPAlignment s0 = true)
   (h_s0_program : s0.program = sha512_program_test_1)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_run : s_final = run 4 s0) :
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  sym_n 4 h_s0_program
+  sym_n 4
   -- Final steps
   unfold run at h_run
-  subst s_final s4
-  simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
+  subst s_final
+  simp only [h_s4_err]
   done
 
 ----------------------------------------------------------------------
@@ -62,17 +64,16 @@ def sha512_program_test_2 : Program :=
 theorem sha512_program_test_2_sym (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x126538#64)
   (h_s0_program : s0.program = sha512_program_test_2)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_run : s_final = run 6 s0) :
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  sym_n 6 h_s0_program
+  sym_n 6
   -- Final steps
   unfold run at h_run
-  subst s_final s6
-  simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
+  simp only [h_run, h_s6_err]
   done
 
 ----------------------------------------------------------------------
@@ -91,7 +92,7 @@ def sha512_program_test_3 : Program :=
 set_option pp.deepTerms false in
 set_option pp.deepTerms.threshold 10 in
 theorem sha512_block_armv8_test_3_sym (s0 s_final : ArmState)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_s0_sp_aligned : CheckSPAlignment s0 = true)
   (h_s0_pc : read_pc s0 = 0x1264c0#64)
   (h_s0_program : s0.program = sha512_program_test_3)
@@ -100,11 +101,11 @@ theorem sha512_block_armv8_test_3_sym (s0 s_final : ArmState)
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  sym_n 4 h_s0_program
+  sym_n 4
   -- Final steps
   unfold run at h_run
-  subst s_final s4
-  simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
+  subst s_final
+  apply h_s4_err
   done
 
 ----------------------------------------------------------------------
@@ -113,73 +114,43 @@ theorem sha512_block_armv8_test_3_sym (s0 s_final : ArmState)
 -- simulation test for the AWS-LC production SHA512 code (the program
 -- we'd like to verify).
 
-example : StateError.None = StateError.None := by decide
-
 -- set_option profiler true in
 -- set_option profiler.threshold 10 in
+-- set_option trace.profiler.output.pp true in
 theorem sha512_block_armv8_test_4_sym (s0 s_final : ArmState)
-  (h_s0_ok : read_err s0 = StateError.None)
+  (h_s0_err : read_err s0 = StateError.None)
   (h_s0_sp_aligned : CheckSPAlignment s0 = true)
   (h_s0_pc : read_pc s0 = 0x1264c0#64)
   (h_s0_program : s0.program = sha512_program_map)
-  (h_run : s_final = run 32 s0) :
+  (h_run : s_final = run 10 s0) :
   read_err s_final = StateError.None := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic simulation
-  -- sym_n 5 h_s0_program
-  -- sym_i_n 0 1 h_s0_program
-  -- init_next_step h_run
-  -- rename_i s1 h_step_1 h_run
-  -- -- fetch_and_decode_inst h_step_1 h_s0_program
-  -- simp only [*, stepi, state_simp_rules, minimal_theory, bitvec_rules] at h_step_1
-  -- rw [fetch_inst_from_program] at h_step_1
-  -- simp only [h_s0_program] at h_step_1
-  -- conv at h_step_1 =>
-  --   pattern Map.find? _ _
-  --   tactic => set_option maxRecDepth 3000 in
-  --             simp (config := {ground := true}) only [reduceMapFind?]
-  -- (try dsimp only at h_step_1)
-  -- conv at h_step_1 =>
-  --   pattern decode_raw_inst _
-  --   tactic =>
-  --     simp (config := {ground := true}) only
-  -- (try dsimp only at h_step_1)
-  -- simp (config := {decide := true}) only
-  --   [exec_inst, state_simp_rules, minimal_theory]
-  --   at h_step_1
-  sym_i_n 0 1 h_s0_program
-  init_next_step h_run
-  rename_i s2 h_step_2 h_run
-  -- project_program_and_error_fields h_step_1
-  -- fetch_and_decode_inst h_step_2 h_s0_program
-  simp only [stepi, state_simp_rules, minimal_theory, bitvec_rules] at h_step_2
-  rw [fetch_inst_from_program] at h_step_2
-  have h_s1_program : s1.program = s0.program := by
-    simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
-  have h_s1_err : r StateField.ERR s1 = StateError.None := by
-    simp only [*, state_simp_rules, minimal_theory, bitvec_rules]
-  have h_s1_pc : r StateField.PC s1 = (1205444#64) := by
-    simp_all only [state_simp_rules, minimal_theory, bitvec_rules]
-  simp only [h_s0_program, h_s1_program, h_s1_err, h_s1_pc] at h_step_2
-  conv at h_step_2 =>
-    pattern Map.find? _ _
-    tactic => set_option maxRecDepth 3000 in
-              simp only [reduceMapFind?]
-  (try dsimp only at h_step_2)
-  conv at h_step_2 =>
-    pattern decode_raw_inst _
-    tactic =>
-      simp (config := {ground := true}) only
-  (try dsimp only at h_step_2)
-  (try clear h_s1_program h_s1_err)
-  -- exec_inst h_step_2
-  explode_step h_step_1
-  have h_s1_gpr31 : r (StateField.GPR 31#5) s1 = (r (StateField.GPR 31#5) s0 + 18446744073709551600#64) := by
-    simp_all only [stepi, state_simp_rules, minimal_theory, bitvec_rules]
-  simp (config := { decide := true }) only [*, -h_step_1, exec_inst, state_simp_rules, minimal_theory, bitvec_rules] at h_step_2
-  (try (repeat simp (config := {ground := true}) only [↓reduceIte, state_simp_rules, minimal_theory, bitvec_rules] at h_step_2))
-
+  -- sym_n 32
+  -- sym_n 10
+  -- -- Final Steps
+  -- unfold run at h_run
+  -- simp only [h_run, h_s10_err]
+  -- done
+  sym_n 10
+  -- sym_i_n 0 1
+  -- sym_i_n 1 1
+  -- sym_i_n 2 1
+  -- sym_i_n 3 1
+  -- sym_i_n 4 1
+  -- sym_i_n 5 1
+  -- sym_i_n 6 1
+  -- sym_i_n 7 1
+  -- sym_i_n 8 1
+  -- sym_i_n 9 1
+  -- Final Steps
+  unfold run at h_run
+  subst s_final
+  -- save
+  -- rw [h_s10_err]
+  -- apply h_s10_err
+  -- done
   sorry
 
 ----------------------------------------------------------------------
diff --git a/Tactics.lean b/Tactics.lean
index c71e95a0..eec217af 100644
--- a/Tactics.lean
+++ b/Tactics.lean
@@ -7,3 +7,4 @@ Author(s): Shilpi Goel
 -- Import modules here that should be built as part of the library.
 import «Tactics».Sym
 import «Tactics».ExplodeStep
+
diff --git a/Tactics/Common.lean b/Tactics/Common.lean
new file mode 100644
index 00000000..ef2076aa
--- /dev/null
+++ b/Tactics/Common.lean
@@ -0,0 +1,34 @@
+/-
+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): Shilpi Goel
+-/
+
+import Lean
+import Arm.Exec
+open Lean Elab Tactic Expr Meta
+open BitVec
+
+
+/- Obtain `Array α` from `Array (Option α)` by discarding any `none`
+elements. -/
+private def optionArraytoArray (array : Array (Option α)) : Array α :=
+  Array.foldl (fun acc val =>
+    match val with
+    | none => acc
+    | some v => acc.append #[v])
+  #[] array
+
+/- Find all declarations in the `LocalContext` whose username begins
+with `pfxUserName`. -/
+def filterDeclsWithPrefix (lctx : LocalContext) (pfxUserName : Name)
+  : (Array LocalDecl) :=
+  optionArraytoArray
+  (PersistentArray.toArray
+    (PersistentArray.filter
+      lctx.decls
+      (fun decl =>
+        match decl with
+          | none      => false
+          | some decl => String.isPrefixOf (toString pfxUserName)
+                                           (toString decl.userName))))
diff --git a/Tactics/ExecInst.lean b/Tactics/ExecInst.lean
new file mode 100644
index 00000000..6d0f2017
--- /dev/null
+++ b/Tactics/ExecInst.lean
@@ -0,0 +1,50 @@
+/-
+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): Shilpi Goel
+-/
+import Arm.Exec
+import Tactics.Common
+import Tactics.Simp
+import Lean
+open Lean Elab Tactic Expr Meta
+open BitVec
+
+----------------------------------------------------------------------
+
+def execInst (goal : MVarId) (h_step : Expr) (hyp_prefix : String)
+  : TacticM Bool := goal.withContext do
+  -- Find all the FVars in the local context whose name begins with
+  -- hyp_prefix.
+  let lctx ← getLCtx
+  let matching_decls := filterDeclsWithPrefix lctx hyp_prefix.toName
+  -- logInfo m!"matching_decls: {matching_decls[0]!.userName}"
+  let (ctx, simprocs) ←
+    LNSymSimpContext (config := {decide := true, ground := true})
+                     (simp_attrs := #[`minimal_theory, `bitvec_rules, `state_simp_rules])
+                     (decls_to_unfold := #[``exec_inst])
+                     (thms := #[])
+                     (decls := matching_decls)
+                     (simprocs := #[``reduceIte])
+  let maybe_goal ← LNSymSimp goal ctx simprocs (fvarid := h_step.fvarId!)
+  match maybe_goal with
+  | none =>
+    logInfo m!"[execInst] The goal appears to be solved, but this tactic \
+                  is not a finishing tactic! Something went wrong?"
+    return false
+  | some goal' =>
+    replaceMainGoal [goal']
+    return true
+
+def execInstElab (h_step : Name) (hyp_prefix : String) : TacticM Unit :=
+  withMainContext
+  (do
+    let h_step ← getFVarFromUserName h_step
+    let success ← execInst (← getMainGoal) h_step hyp_prefix
+    if ! success then
+      failure)
+
+elab "exec_inst" h_step:ident hyp_prefix:str : tactic =>
+  execInstElab (h_step.getId) (hyp_prefix.getString)
+
+----------------------------------------------------------------------
diff --git a/Tactics/ExplodeStep.lean b/Tactics/ExplodeStep.lean
index 6ae8ee80..ad570376 100644
--- a/Tactics/ExplodeStep.lean
+++ b/Tactics/ExplodeStep.lean
@@ -124,12 +124,6 @@ partial def explodeWriteNest (goal : MVarId)
               match p_simp? with
               | none => []
               | some (_, p_simp_mvarid) => [p_simp_mvarid]
-            -- let new_goals ←
-            --   evalTacticAt
-            --     (← `(tactic|
-            --           (simp (config := {decide := true}) only
-            --                        [state_simp_rules, minimal_theory, bitvec_rules])))
-            --     p
             -- logInfo m!"new_goals: {new_goals}"
             let (_, goal') ← MVarId.intro1P $ ← Lean.MVarId.assert goal name new_prop_type new_prop_val
             explodeWriteNest goal' st_var rest (field_str :: seen_fields) (rest_goals ++ new_goals)
@@ -226,7 +220,7 @@ example (s0 s1 : ArmState)
   (h : s1 = w (StateField.GPR 31#5) 12#64
               (w StateField.PC 1#64
                 (w (StateField.GPR 31#5) 13#64 s0))) :
-  r StateField.PC s1 = 1#64 := by
+  (r StateField.PC s1) + 1#64 = 2#64 := by
   explode_step h
-  assumption
+  simp (config := {decide := true}) [h_s1_pc]
   done
diff --git a/Tactics/FetchAndDecode.lean b/Tactics/FetchAndDecode.lean
new file mode 100644
index 00000000..a377c19a
--- /dev/null
+++ b/Tactics/FetchAndDecode.lean
@@ -0,0 +1,167 @@
+/-
+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): Shilpi Goel
+-/
+import Arm.Exec
+import Tactics.IntroHyp
+import Lean
+open Lean Elab Tactic Expr Meta
+open BitVec
+
+----------------------------------------------------------------------
+
+/- `fetchAndDecodeInst` simplifies the hypothesis
+
+`h_step: s_next = stepi s`
+
+by unfolding `stepi`, and then simplifying `fetch_inst` and
+`decode_raw_inst`, which results in the following:
+
+`h_step: s_next = exec_inst <decoded_instruction> s`
+
+First, the function `stepi` is unfolded, which yields a term
+containing `fetch_inst`. This function is then rewritten using the
+lemma `fetch_inst_from_program` to a call of `Map.find?`; we expect
+that `Map.find?` will have ground arguments (program counter and
+program). We reduce this call of `Map.find?` via the simproc
+`reduceMapFind?`. The function `decode_raw_inst` is also expected to
+be called on a ground 32-bit instruction. We reduce this call by using
+`simp/ground`.
+
+Fetching and decoding an instruction relies upon knowing the values of
+three components of the current state: error, program counter, and
+program (see the definitions of `fetch_inst` and
+`decode_raw_inst`). We expect that these values can be gleaned from
+the local context. Moreover, we expect that there exist hypotheses in
+the local context of the form
+
+`<name>: r <fld> <state> = value
+
+whose user-facing names describe both the field and the state. (Such
+hypotheses are added by the tactic "introduce_fetch_lemmas").
+
+As such, `fetchAndDecodeInst` also adds any hypotheses in the context
+whose usernames begin with the supplied prefix `hyp_prefix` to the
+simp set.  It is the caller's responsibility to provide the
+appropriate `hyp_prefix` here.
+
+TODO: More error checks: e.g., checks whether `h_step` and the
+resulting hypothesis have the expected forms (i.e., in terms of
+`stepi` and `exec_inst`, respectively).
+-/
+def fetchAndDecodeInst (goal : MVarId) (h_step : Expr) (hyp_prefix : String)
+  : TacticM Bool := goal.withContext do
+  -- Find all the FVars in the local context whose name begins with
+  -- hyp_prefix.
+  let lctx ← getLCtx
+  let matching_decls := filterDeclsWithPrefix lctx hyp_prefix.toName
+  -- logInfo m!"matching_decls: {matching_decls[0]!.userName}"
+
+  -- Simplify `fetch_inst` and `decode_raw_inst`: note: using
+  -- `ground := true` here causes maxRecDepth to be reached. Use
+  -- reduceMapFind? instead.
+  let (ctx, simprocs) ←
+    LNSymSimpContext (config := {decide := true})
+                     (simp_attrs := #[`minimal_theory, `bitvec_rules, `state_simp_rules])
+                     (decls_to_unfold := #[``stepi])
+                     (thms := #[``fetch_inst_from_program])
+                     (decls := matching_decls)
+                     (simprocs := #[``reduceMapFind?])
+  let maybe_goal ← LNSymSimp goal ctx simprocs (fvarid := h_step.fvarId!)
+  match maybe_goal with
+  | none =>
+    logInfo m!"[fetchAndDecodeInst] The goal appears to be solved, but this tactic \
+                  is not a finishing tactic! Something went wrong?"
+    return false
+  | some goal' =>
+      replaceMainGoal [goal']
+      return true
+
+def fetchAndDecodeElab (h_step : Name) (hyp_prefix : String) : TacticM Unit :=
+  withMainContext
+  (do
+    let h_step ← getFVarFromUserName h_step
+    let success ← fetchAndDecodeInst (← getMainGoal) h_step hyp_prefix
+    if ! success then
+      failure)
+
+elab "fetch_and_decode" h_step:ident hyp_prefix:str : tactic =>
+  fetchAndDecodeElab (h_step.getId) (hyp_prefix.getString)
+
+----------------------------------------------------------------------
+
+def introFetchDecodeLemmas (goal : MVarId) (hStep : Expr) (hProgram : Expr)
+  (hyp_prefix : String) :
+  TacticM Bool := goal.withContext do
+  let_expr Eq _ st_var nest ← (← inferType hStep) | return false
+  let_expr Eq _ _ program ← (← inferType hProgram) | return false
+  -- Find all the FVars in the local context whose name begins with
+  -- hyp_prefix.
+  let lctx ← getLCtx
+  let matching_decls := filterDeclsWithPrefix lctx hyp_prefix.toName
+  -- logInfo m!"matching_decls: {matching_decls[0]!.userName}"
+  let (ctx, simprocs) ←
+    LNSymSimpContext (config := {decide := true})
+                     (simp_attrs := #[`minimal_theory, `bitvec_rules, `state_simp_rules])
+                     (decls_to_unfold := #[])
+                     (thms := #[])
+                     (decls := matching_decls)
+                     (simprocs := #[])
+  let st_var := consumeMData st_var
+  let nest := consumeMData nest
+  if ! (st_var.isFVar && nest.isApp) then
+    logInfo m!"[introFetchLemmasExpr] Unexpected hStep expression. We expect \
+                the state variable on the LHS to be an FVar and the \
+                term on the RHS to be a function application. Here is \
+                what they actually are: \
+                st_var: {st_var.ctorName}; nest: {nest.ctorName}."
+    return false
+  let st_var_str := toString (← (getFVarLocalDecl st_var)).userName
+  -- Introduce a hypothesis (and attempt to prove) that the error field in the
+  -- new state is `StateError.None`.
+  let (goal', err_goals) ←
+    introLNSymHyp goal st_var (gen_hyp_name st_var_str "err")
+      (mkAppN (Expr.const ``Eq [1])
+            #[(mkConst ``StateError),
+              (mkAppN (Expr.const ``r []) #[(mkConst ``StateField.ERR), st_var]),
+              (mkConst ``StateError.None)])
+      ctx simprocs
+  -- Obtain the new PC value from the nest of updates, and add its
+  -- corresponding read hypothesis to the context.
+  let some pc_val := getArmStateComponentNoMem (mkConst ``StateField.PC) nest |
+    logInfo m!"[introFetchDecodeLemmas] We only parse function calls `w` and `write_mem_bytes` \
+                in the state update equation. Right now, we cannot determine the PC value \
+                from the expression: {nest}."
+    return false
+  let (goal', pc_goals) ←
+    introLNSymHyp goal' st_var (gen_hyp_name st_var_str "pc")
+      (mkAppN (Expr.const ``Eq [1])
+        #[(← inferType pc_val),
+          (mkAppN (Expr.const ``r []) #[(mkConst ``StateField.PC), st_var]),
+          pc_val])
+      ctx simprocs
+  -- Introduce a hypothesis (and attempt to prove) that the program in
+  -- the new state is the same as it was earlier in `hProgram`.
+  let (goal', prog_goals) ←
+    introLNSymHyp goal' st_var (gen_hyp_name st_var_str "program")
+      (mkAppN (Expr.const ``Eq [1])
+        #[(mkConst ``Program),
+          (mkAppN (Expr.const ``ArmState.program []) #[st_var]),
+          program])
+      ctx simprocs
+  replaceMainGoal (goal' :: (err_goals ++ prog_goals ++ pc_goals))
+  return true
+
+def introFetchDecodeLemmasElab (h_step : Name) (h_program : Name) (hyp_prefix : String)
+  : TacticM Unit :=
+  withMainContext
+  (do
+    let h_step ← getFVarFromUserName h_step
+    let h_program ← getFVarFromUserName h_program
+    let success ← introFetchDecodeLemmas (← getMainGoal) h_step h_program hyp_prefix
+    if ! success then
+      failure)
+
+elab "intro_fetch_decode_lemmas" h_step:ident h_program:ident hyp_prefix:str : tactic =>
+  introFetchDecodeLemmasElab (h_step.getId) (h_program.getId) (hyp_prefix.getString)
diff --git a/Tactics/IntroHyp.lean b/Tactics/IntroHyp.lean
new file mode 100644
index 00000000..be854f3d
--- /dev/null
+++ b/Tactics/IntroHyp.lean
@@ -0,0 +1,58 @@
+/-
+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): Shilpi Goel
+-/
+import Lean
+import Tactics.Common
+import Tactics.Simp
+open Lean Elab Tactic Expr Meta
+open BitVec
+
+/- Given a `goal`, where `st_var` represents a state variable,
+`introLNSymHyp` introduces a hypothesis of the form `name : term` in
+the context. This function also tries to prove `term` by first
+attempting to substitute `st_var` and then calling `LNSymSimp`. This
+function returns the original goal that may have the new hypothesis in
+its context, and also any unsolved goals that result from the proof
+attempt of the new hypothesis.
+
+The responsibility of providing a well-formed `term` lies with the
+caller of this function. -/
+partial def introLNSymHyp (goal : MVarId)
+  (st_var : Expr) (name : Name) (term : Expr)
+  (ctx : Simp.Context) (simprocs : Array Simp.Simprocs) :
+  TacticM (MVarId × (List MVarId)) :=
+  goal.withContext do
+  let mvar_expr ← mkFreshExprMVar term MetavarKind.syntheticOpaque name
+  -- logInfo m!"New goal: {mvar_expr.mvarId!}"
+  let subst_mvar_expr ← substVar? mvar_expr.mvarId! st_var.fvarId!
+  let term_mvarid ←
+    match subst_mvar_expr with
+    | none =>
+      logInfo m!"[introLNSymHyp] Could not substitute {st_var} in \
+                  goal {mvar_expr.mvarId!}"
+      return (goal, [])
+    | some mvarid =>
+      let new_goal ← LNSymSimp mvarid ctx simprocs
+      let (_, goal') ← MVarId.intro1P $ ← Lean.MVarId.assert goal name term mvar_expr
+      return (goal', (if Option.isNone new_goal then [] else [Option.get! new_goal]))
+
+
+def gen_hyp_name (st_name : String) (suffix : String) : Name :=
+  Lean.Name.mkSimple ("h_" ++ st_name ++ "_" ++ suffix)
+
+/- Get the value written to `field` (which is an expression
+corresponding to a `StateField` value), in the expression `nest`,
+which is assumed to be a nest of updates made to the Arm state. If
+`nest` does not include an update to `field`, return none. -/
+partial def getArmStateComponentNoMem (field : Expr) (nest : Expr) : Option Expr :=
+  match_expr nest with
+  | w w_field val rest =>
+    if field == w_field then
+      some val
+    else
+      getArmStateComponentNoMem field rest
+  | write_mem_bytes _ _ _ rest =>
+    getArmStateComponentNoMem field rest
+  | _ => none
diff --git a/Tactics/Simp.lean b/Tactics/Simp.lean
new file mode 100644
index 00000000..568ed188
--- /dev/null
+++ b/Tactics/Simp.lean
@@ -0,0 +1,69 @@
+/-
+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): Shilpi Goel
+-/
+import Lean
+import Arm.Attr
+open Lean Elab Tactic Expr Meta
+open BitVec
+
+/- Create a context for using the `simp` tactic during symbolic
+simulation in LNSym proofs. -/
+def LNSymSimpContext
+  (config : Simp.Config := {decide := true})
+  (simp_attrs : Array Name := #[`minimal_theory, `bitvec_rules, `state_simp_rules])
+  -- Functions to unfold during simp.
+  (decls_to_unfold : Array Name := #[])
+  -- Theorems to use during simp.
+  (thms : Array Name := #[])
+  -- Local hypotheses to use during simp.
+  (decls : Array LocalDecl := #[])
+  -- Simprocs to add to the default set.
+  (simprocs : Array Name := #[])
+  : TacticM (Simp.Context ×  Array Simp.Simprocs) := do
+  let mut ext_simpTheorems := #[]
+  for a in simp_attrs do
+    let some ext ← (getSimpExtension? a) |
+                   throwError m!"[LNSymSimpContext] Error: {a} simp attribute not found!"
+    ext_simpTheorems := #[(← ext.getTheorems)] ++ ext_simpTheorems
+  let mut const_simpTheorems := ({} : SimpTheorems)
+  for d in decls_to_unfold do
+    const_simpTheorems ← const_simpTheorems.addDeclToUnfold d
+  for t in thms do
+    const_simpTheorems ← const_simpTheorems.addConst t
+  for l in decls do
+    let proof := l.toExpr
+    let fvar := l.fvarId
+    const_simpTheorems ← const_simpTheorems.add (.fvar fvar) #[] proof
+  let all_simpTheorems := (#[const_simpTheorems] ++ ext_simpTheorems)
+  let (ctx : Simp.Context) := { config := config,
+                                simpTheorems := all_simpTheorems,
+                                congrTheorems := (← Meta.getSimpCongrTheorems) }
+  let default_simprocs ← Simp.getSimprocs
+  let mut all_simprocs := (#[default_simprocs] : Simp.SimprocsArray)
+  for s in simprocs do
+    all_simprocs ← Simp.SimprocsArray.add all_simprocs s false  
+  return (ctx, all_simprocs)
+
+/- Invoke the `simp` tactic during symbolic simulation in LNSym
+proofs. -/
+def LNSymSimp (goal : MVarId)
+   (ctx : Simp.Context) (simprocs : Array Simp.Simprocs)
+  -- Provide an FVarID (i.e., a hypothesis) to simplify; when none is provided,
+  -- the goal is simplified.
+   (fvarid : Option FVarId := none) : TacticM (Option MVarId) := goal.withContext do
+  match fvarid with
+  | none =>
+    let (new_goal, _) ← simpGoal goal ctx simprocs
+                        (simplifyTarget := true) (discharge? := none)
+    match new_goal with
+    | none => return none
+    | some (_, goal') => return goal'
+  | some fid =>
+    let (new_goal, _) ← simpLocalDecl goal fid ctx simprocs
+    match new_goal with
+    | none => return none
+    | some (_, goal') => return goal'
+
+----------------------------------------------------------------------
diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
index cf5476eb..279b0708 100644
--- a/Tactics/Sym.lean
+++ b/Tactics/Sym.lean
@@ -5,13 +5,24 @@ Author(s): Shilpi Goel
 -/
 import Arm.Exec
 import Arm.MemoryProofs
+import Tactics.FetchAndDecode
+import Tactics.ExecInst
 
 import Lean.Elab
 import Lean.Expr
 
 open BitVec
 
--- init_next_step breaks 'h_s: s_next = run n s' into 'run (n-1) s' and one step.
+/- `init_next_step h_run` splits the hypothesis
+
+`h_run: s_final = run n s`
+
+introduces a new state variable, say `s_next` and two new hypotheses:
+`h_step: s_next = stepi s`
+`h_run': s_final = run (n-1) s_next`
+
+The new state variable and the hypotheses are not named yet.
+-/
 macro "init_next_step" h_s:ident : tactic =>
   `(tactic|
     (rw [run_onestep] at $h_s:ident <;> try omega
@@ -21,30 +32,6 @@ macro "init_next_step" h_s:ident : tactic =>
      rename_i h_s'
      simp (config := {ground := true}) only at h_s'))
 
--- Given 'h_step: s_next = stepi s', fetch_and_decode_inst unfolds stepi,
--- simplifies fetch_inst and decode_raw_inst.
-macro "fetch_and_decode_inst" h_step:ident h_program:ident : tactic =>
-  `(tactic|
-    (simp only [*, stepi, state_simp_rules, minimal_theory, bitvec_rules] at $h_step:ident
-     rw [fetch_inst_from_program] at $h_step:ident
-     simp only [$h_program:ident] at $h_step:ident
-     conv at $h_step:ident =>
-      pattern Map.find? _ _
-      tactic => set_option maxRecDepth 3000 in
-                simp only [reduceMapFind?]
-     (try dsimp only at $h_step:ident);
-     conv at $h_step:ident =>
-      pattern decode_raw_inst _
-      simp (config := {ground := true}) only
-     (try dsimp only at $h_step:ident)))
-
--- Given hstep which is the result of fetch_and_decode_inst, exec_inst executes
--- an instruction and generates 's_next = w .. (w .. (... s))'.
-macro "exec_inst" h_step:ident : tactic =>
-  `(tactic|
-    (simp (config := { decide := true }) only [*, exec_inst, state_simp_rules, minimal_theory, bitvec_rules] at $h_step:ident;
-     (try (repeat simp (config := {ground := true}) only [↓reduceIte, state_simp_rules, minimal_theory, bitvec_rules] at $h_step:ident))))
-
 -- Given h_step which is 's_next = w .. (w .. (... s))', it creates assumptions
 -- 'read .. s_next = value'.
 -- TODO: update_invariants must add all register and memory updates as
@@ -87,42 +74,34 @@ macro "exec_inst" h_step:ident : tactic =>
 --         try (rw [write_mem_bytes_program])
 --         assumption))
 
-def sym_one (curr_state_number : Nat) (prog : Lean.Ident) :
-    Lean.Elab.Tactic.TacticM Unit :=
+def sym_one (curr_state_number : Nat) : Lean.Elab.Tactic.TacticM Unit :=
   Lean.Elab.Tactic.withMainContext do
     let n_str := toString curr_state_number
     let n'_str := toString (curr_state_number + 1)
-    -- let pcexpr := Lean.mkNatLit (pc_begin + 4 * (curr_state_number + 1))
-    -- let pcbv :=  ← (Lean.Elab.Term.exprToSyntax (Lean.mkApp2 (Lean.mkConst ``BitVec.ofNat)
-    --                           (Lean.mkNatLit 64)
-    --                           pcexpr))
-    -- let pcbv := ← (Lean.mkApp2 (Lean.mkConst ``BitVec.ofNat) (Lean.mkNatLit 64)
-    --                            pcexpr).toSyntax
-    -- Question: how can I convert this pcbv into Syntax?
     let mk_name (s : String) : Lean.Name :=
       Lean.Name.mkStr Lean.Name.anonymous s
+    -- h_st: prefix of user names of hypotheses about state st
+    let h_st_prefix := Lean.Syntax.mkStrLit ("h_s" ++ n_str)
+    -- h_st_program: name of the hypothesis about the program at state st
+    let h_st_program := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_program"))
+    let h_st_pc := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_pc"))
+    let h_st_err := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_err"))
     -- st': name of the next state
     let st' := Lean.mkIdent (mk_name ("s" ++ n'_str))
-    -- let h_st_ok := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_ok"))
-    -- let h_st'_ok := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_ok"))
-    -- let h_st_pc := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_pc"))
-    -- let h_st'_pc := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_pc"))
-    -- let h_st_program := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_program"))
-    -- let h_st'_program := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_program"))
-    -- let h_st_sp_aligned := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_sp_aligned"))
-    -- let h_st'_sp_aligned := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_sp_aligned"))
-    -- Temporary hypotheses
+    -- h_run: name of the hypothesis with the `run` function
     let h_run := Lean.mkIdent (mk_name "h_run")
-    let h_step_n := Lean.mkIdent (mk_name ("h_step_" ++ n_str))
+    -- h_step_n': name of the hypothesis with the `stepi` function
     let h_step_n' := Lean.mkIdent (mk_name ("h_step_" ++ n'_str))
     Lean.Elab.Tactic.evalTactic (←
       `(tactic|
          (init_next_step $h_run:ident
           rename_i $st':ident $h_step_n':ident $h_run:ident
           -- Simulate one instruction
-          fetch_and_decode_inst $h_step_n':ident $prog:ident
-          (try clear $h_step_n:ident)
-          exec_inst $h_step_n':ident
+          fetch_and_decode $h_step_n':ident $h_st_prefix:str
+          -- (try clear $h_step_n:ident)
+          exec_inst $h_step_n':ident $h_st_prefix:str
+          intro_fetch_decode_lemmas $h_step_n':ident $h_st_program:ident $h_st_prefix:str
+          (try clear $h_st_pc:ident $h_st_program:ident $h_st_err:ident)
           -- Update invariants
           -- update_invariants $st':ident $prog:ident
           --                   $h_st'_ok:ident
@@ -131,15 +110,15 @@ def sym_one (curr_state_number : Nat) (prog : Lean.Ident) :
           --                   $h_st'_program $h_step_n':ident $pcbv:term
           -- clear $h_st_ok:ident $h_st_sp_aligned:ident $h_st_pc:ident $h_step_n':ident
           --       $h_st_program:ident
-                )))
+      )))
 
 -- sym_n tactic symbolically simulates n instructions.
-elab "sym_n" n:num prog:ident : tactic => do
+elab "sym_n" n:num : tactic => do
   for i in List.range n.getNat do
-    sym_one i prog
+    sym_one i
 
 -- sym_n tactic symbolically simulates n instructions from
 -- state number i.
-elab "sym_i_n" i:num n:num prog:ident : tactic => do
+elab "sym_i_n" i:num n:num : tactic => do
   for j in List.range n.getNat do
-    sym_one (i.getNat + j) prog
+    sym_one (i.getNat + j)