Popcount32 functional correctness and (non)effects characterization (#…

…159)

### Description:

Prove that the popcount32 program correctly computes the bitcount of its
input, and prove that certain state components were left unmodified by
this program.

### Testing:

`make all` ran locally.

### License:

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

---------

Co-authored-by: Alex Keizer <[email protected]>

Arm/State.lean

@@ -336,7 +336,7 @@ def r (fld : StateField) (s : ArmState) : (state_value fld) :=
 /-!
 
 We define helpers for reading and writing registers on the `ArmState` with the colloquial
-names. For example, the stack pointer (`sp`) refers to register 31. 
+names. For example, the stack pointer (`sp`) refers to register 31.
 These mnemonics make it much easier to read and write theorems about assembly programs.
 
 -/
@@ -1142,7 +1142,7 @@ theorem Memory.eq_of_read_mem_bytes_eq {m₁ m₂ : Memory}
   rw [BitVec.zero_append, BitVec.zero_append] at h
   simpa only [Nat.reduceAdd, BitVec.cast_eq] using h
 
-theorem mem_eq_iff_read_mem_bytes_eq {s₁ s₂ : ArmState} :
+theorem Memory.mem_eq_iff_read_mem_bytes_eq {s₁ s₂ : ArmState} :
     s₁.mem = s₂.mem
     ↔ ∀ n addr, read_mem_bytes n addr s₁ = read_mem_bytes n addr s₂ := by
   simp only [memory_rules]
@@ -1156,7 +1156,7 @@ theorem read_mem_bytes_write_mem_bytes_of_read_mem_eq
     read_mem_bytes n₁ addr₁ (write_mem_bytes n₂ addr₂ val s₁)
     = read_mem_bytes n₁ addr₁ (write_mem_bytes n₂ addr₂ val s₂) := by
   revert n₁ addr₁
-  simp only [← mem_eq_iff_read_mem_bytes_eq] at h ⊢
+  simp only [← Memory.mem_eq_iff_read_mem_bytes_eq] at h ⊢
   simp only [memory_rules, h]
 
 /- Helper lemma for `state_eq_iff_components_eq` -/

Proofs/Popcount32.lean

@@ -1,11 +1,14 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author(s): Nathan Wetzler
+Author(s): Nathan Wetzler, Shilpi Goel, Alex Keizer
 -/
 import Arm.Exec
 import Arm.Util
+import Arm.Syntax
+import Arm.Memory.SeparateAutomation
 import Tactics.Sym
+import Tactics.Aggregate
 import Tactics.StepThms
 
 section popcount32
@@ -26,7 +29,7 @@ int popcount_32 (unsigned int v) {
 
 def popcount32_spec_rec (i : Nat) (x : BitVec 32) : (BitVec 32) :=
   match i with
-  | 0 => BitVec.zero 32
+  | 0 => 0#32
   | i' + 1 =>
     let bit_idx := BitVec.getLsbD x i'
     ((BitVec.zeroExtend 32 (BitVec.ofBool bit_idx)) + (popcount32_spec_rec i' x))
@@ -68,44 +71,57 @@ def popcount32_program : Program :=
 
 #genStepEqTheorems popcount32_program
 
-theorem popcount32_sym_no_error (s0 s_final : ArmState)
+theorem popcount32_sym_meets_spec (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x4005b4#64)
   (h_s0_program : s0.program = popcount32_program)
   (h_s0_sp_aligned : CheckSPAlignment s0)
   (h_s0_err : read_err s0 = StateError.None)
   (h_run : s_final = run 27 s0) :
-  read_err s_final = StateError.None := by
+  read_gpr 32 0#5 s_final = popcount32_spec (read_gpr 32 0#5 s0) ∧
+  read_err s_final = StateError.None ∧
+  (∀ f, f ≠ (.GPR 0#5) ∧ f ≠ (.GPR 1#5) ∧ f ≠ (.GPR 31#5) ∧ f ≠ .PC →
+       r f s_final = r f s0) ∧
+  (∀ (n : Nat) (addr : BitVec 64),
+    mem_separate' addr n (r (.GPR 31) s0 - 16#64) 16 →
+    s_final[addr, n] = s0[addr, n]) := by
   -- Prelude
   simp_all only [state_simp_rules, -h_run]
   -- Symbolic Simulation
   sym_n 27
-  done
-
--- theorem popcount32_sym_meets_spec (s0 s_final : ArmState)
---   (h_s0_pc : read_pc s0 = 0x4005b4#64)
---   (h_s0_program : s0.program = popcount32_program)
---   (h_s0_sp_aligned : CheckSPAlignment s0)
---   (h_s0_err : read_err s0 = StateError.None)
---   (h_run : s_final = run 27 s0) :
---   read_gpr 32 0#5 s_final = popcount32_spec (read_gpr 32 0#5 s0) ∧
---   read_err s_final = StateError.None := by
---   -- Prelude
---   simp_all only [state_simp_rules, -h_run]
---   -- Symbolic Simulation
---   sym_n 27
---   try (clear h_step_1 h_step_2 h_step_3 h_step_4;
---        clear h_step_5 h_step_6 h_step_7 h_step_8;
---        clear h_step_9 h_step_10;
---        clear h_step_11 h_step_12 h_step_13 h_step_14;
---        clear h_step_15 h_step_16 h_step_17 h_step_18;
---        clear h_step_19 h_step_20;
---        clear h_step_21 h_step_22 h_step_23 h_step_24;
---        clear h_step_25 h_step_26)
---   -- Final Steps
---   unfold run at h_run
---   subst s_final
---   unfold popcount32_spec
---   sorry
+  -- Final Steps
+  -- Split all the Ands in the conclusion.
+  repeat' apply And.intro
+  · simp only [popcount32_spec,
+               fst_AddWithCarry_eq_add,
+               fst_AddWithCarry_eq_sub_neg]
+    simp only [popcount32_spec_rec]
+    bv_decide
+  · sym_aggregate
+  · -- (TODO @alex) Let's do away with
+    -- ∀ (n : Nat) (addr : BitVec 64), read_mem_bytes n addr s₁ = read_mem_bytes n addr s₂
+    -- in favor of
+    -- s₁.mem = s₂.mem
+    -- as Sid said.
+    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 (config := {ground := true}) only
+          [fst_AddWithCarry_eq_add, fst_AddWithCarry_eq_sub_neg]
+    simp only [*, bitvec_rules]
+    simp_mem
+    sym_aggregate
+
+    simp (config := {ground := true}) only
+          [fst_AddWithCarry_eq_add, fst_AddWithCarry_eq_sub_neg]
+    simp only [*, bitvec_rules]
+    simp_mem
+    rfl
+
+
+-------------------------------------------------------------------------------
 
 /-! ## Tests for step theorem generation -/
 section Tests

Tactics/Aggregate.lean

@@ -11,15 +11,25 @@ open Lean Meta Elab.Tactic
 
 namespace Sym
 
+/-- The default `simp` configuration for `aggregate` -/
+def aggregate.defaultSimpConfig : Simp.Config := {
+  decide := true,     -- to discharge side-conditions for non-effect hypotheses
+  contextual := true, -- to automatically prove non-effect goals
+  failIfUnchanged := false,
+}
+
 /-- Given an array of (non-)effects hypotheses, aggregate these effects by
 `simp`ing at the specified location -/
-def aggregate (axHyps : Array LocalDecl) (location : Location) : TacticM Unit :=
+def aggregate (axHyps : Array LocalDecl) (location : Location)
+    (simpConfig? : Option Simp.Config := none) :
+    TacticM Unit :=
   let msg := m!"aggregating (non-)effects"
   withTraceNode `Tactic.sym (fun _ => pure msg) <| do
     trace[Tactic.sym] "using hypotheses: {axHyps.map (·.toExpr)}"
 
+    let config := simpConfig?.getD aggregate.defaultSimpConfig
     let (ctx, simprocs) ← LNSymSimpContext
-        (config := {decide := true, failIfUnchanged := false})
+        (config := config)
         (decls := axHyps)
 
     withLocation location
@@ -35,18 +45,26 @@ def aggregate (axHyps : Array LocalDecl) (location : Location) : TacticM Unit :=
       )
       (fun _ => pure ())
 
-open Parser.Tactic (location) in
+open Parser.Tactic (location config) in
 /--
 `sym_aggregate` will search for all local hypotheses of the form
   `r ?fld ?state = _` or `∀ f ..., r ?fld ?state = _`,
 and use those hypotheses to simplify the goal
 
 `sym_aggregate at ...` will use those same hypotheses to simplify at the
 specified locations, using the same syntax as `simp at ...`
+
+`sym_aggregate (config := ...)` will pass the specified configuration through
+to the `simp` call, for fine-grained control. Note that if you do this,
+you'll likely want to set `decide := true` yourself, or you might find that
+non-effect theorems no longer apply automatically
 -/
-elab "sym_aggregate" loc:(location)? : tactic => withMainContext do
+elab "sym_aggregate" simpConfig?:(config)? loc?:(location)? : tactic => withMainContext do
   let msg := m!"aggregating local (non-)effect hypotheses"
   withTraceNode `Tactic.sym (fun _ => pure msg) <| do
+    let simpConfig? ← simpConfig?.mapM fun cfg =>
+      elabSimpConfig (mkNullNode #[cfg]) (kind := .simp)
+
     let lctx ← getLCtx
     -- We keep `expectedRead`/`expectedAlign` as monadic values,
     -- so that we get new metavariables for each localdecl we check
@@ -76,5 +94,5 @@ elab "sym_aggregate" loc:(location)? : tactic => withMainContext do
               trace[Tactic.sym] "{Lean.crossEmoji} no match"
               return axHyps
 
-    let loc := (loc.map expandLocation).getD (.targets #[] true)
-    aggregate axHyps loc
+    let loc := (loc?.map expandLocation).getD (.targets #[] true)
+    aggregate axHyps loc simpConfig?