feat: expand sym_aggregate search to include equalities `?state.pro…

…gram = ?program` (#236)

### Issues:

Resolves a [TODO in
SHA512Prelude](https://github.com/leanprover/LNSym/blob/2e4d59cbd6f76eb8d63ed41ccbda38b49dd9c7ae/Proofs/SHA512/SHA512Prelude.lean#L144)

### Description:

We add the capability for `sym_aggregate` to rewrite along hypotheses
about the program of an ArmState.

### Testing:

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

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

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

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?