chore: cleanup

Arm/Memory/SeparateAutomation.lean

@@ -212,21 +212,6 @@ def SimpMemM.findOverlappingReadHyp (hyps : Array Memory.Hypothesis) (er : ReadB
   return none
 
 
-def Expr.kindStr (e : Expr) : String :=
-  match e with
-  | Expr.forallE .. => "forall"
-  | Expr.letE ..  => "let"
-  | Expr.const .. => "const"
-  | Expr.sort .. => "sort"
-  | Expr.lam .. => "lam"
-  | Expr.mdata .. => "mdata"
-  | Expr.proj .. => "proj"
-  | Expr.app .. => "app"
-  | Expr.mvar .. => "mvar"
-  | Expr.bvar .. => "bvar"
-  | Expr.fvar .. => "fvar"
-  | Expr.lit .. => "lit"
-
 mutual
 
 /--
@@ -282,7 +267,7 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Memory.Hypothesis) :
       return out
 
 partial def SimpMemM.walkExpr (e : Expr) (hyps : Array Memory.Hypothesis) : SimpMemM (Option SimplifyResult) := do
-  withTraceNode (traceClass := `simp_mem.expr_walk_trace) m!"🎯 {e} | kind:{Expr.kindStr e}" (collapsed := false) do
+  withTraceNode (traceClass := `simp_mem.expr_walk_trace) m!"🎯 {e} | kind:{Expr.ctorName e}" (collapsed := false) do
   let e ← instantiateMVars e
   match e.consumeMData with
   | .app f x =>

Proofs/Experiments/Max/MaxTandem.lean

@@ -173,7 +173,6 @@ info: 'MaxTandem.program.stepi_0x894_cut' depends on axioms: [propext, Classical
 #guard_msgs in #print axioms program.stepi_0x894_cut
 
 -- 2/15: str  w0, [sp, #12]  ; sp[12] = w0_a
-set_option trace.simp_mem.info true in
 theorem program.stepi_0x898_cut (s sn : ArmState)
   (h_program : s.program = program)
   (h_pc : r StateField.PC s = 0x898#64)

Proofs/SHA512/SHA512Prelude.lean

@@ -115,8 +115,6 @@ in this proof. This will hopefully go down, once we optimize `sym_aggregate`.
 -/
 set_option maxRecDepth 8000 in
 set_option linter.unusedVariables false in
-set_option trace.simp_mem.info true in
-set_option trace.simp_mem.expr_walk_trace true in
 theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   -- We fix the number of blocks to hash to 1.
   (h_N : N = 1#64)