Merge branch 'main' into rename-sym-debug

leanprover · Oct 13, 2024 · 8d9c69e · 8d9c69e
2 parents 1b2f627 + 3b8f5f1
commit 8d9c69e
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/Proofs/SHA512/SHA512Prelude.lean b/Proofs/SHA512/SHA512Prelude.lean
@@ -141,9 +141,8 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   -- cse (config := { processHyps := .allHyps })
   simp only [SHA512.prelude, bitvec_rules, minimal_theory]
   -- Opening up `prelude`:
-  -- (FIXME @alex) Why does `s16.program = program` remain even after aggregation?
   sym_aggregate
-  simp only [h_s16_program, ←add_eq_sub_16, minimal_theory]
+  simp only [←add_eq_sub_16, minimal_theory]
   -- The following discharges
   --  InputBase + 0x40#64 + 0x40#64 =
   --  InputBase + 0x80#64

diff --git a/Tactics/Aggregate.lean b/Tactics/Aggregate.lean
@@ -106,6 +106,15 @@ elab "sym_aggregate" simpConfig?:(config)? loc?:(location)? : tactic => withMain
           (expectedType := do
             let state ← mkFreshExprMVar mkArmState
             return mkApp (mkConst ``CheckSPAlignment) state)
+        -- `?state.program = ?program`
+        searchLCtxFor (whenFound := whenFound)
+          (expectedType := do
+            let mkProgramTy := mkConst ``Program
+            let state ← mkFreshExprMVar mkArmState
+            let program ← mkFreshExprMVar mkProgramTy
+            return mkApp3 (.const ``Eq [1]) mkProgramTy
+              (mkApp (mkConst ``ArmState.program) state)
+              program)
 
     let loc := (loc?.map expandLocation).getD (.targets #[] true)
     aggregate axHyps loc simpConfig?