Prove the partial correctness of a small program with a loop

Arm/Cosim.lean

@@ -205,13 +205,15 @@ def nzcv_mismatch (x1 x2 : BitVec 4) : IO String := do
       acc := acc ++ s!"Flag{flag} machine {f1} model {f2}"
   pure acc
 
-def regStates_match (input o1 o2 : regState) : IO Bool := do
+def regStates_match (uniqueBaseName : String) (input o1 o2 : regState) : 
+  IO Bool := do
   if o1 == o2 then
      pure true
   else
      let gpr_mismatch ← gpr_mismatch o1.gpr o2.gpr
      let nzcv_mismatch ← nzcv_mismatch o1.nzcv o2.nzcv
      let sfp_mismatch  ← sfp_mismatch o1.sfp o2.sfp
+     IO.println s!"ID: {uniqueBaseName}"
      IO.println s!"Instruction: {decode_raw_inst input.inst}"
      IO.println s!"input: {toString input}"
      IO.println s!"Mismatch found: {gpr_mismatch} {nzcv_mismatch} {sfp_mismatch}"
@@ -224,7 +226,7 @@ def one_test (inst : BitVec 32) (uniqueBaseName : String) : IO Bool := do
   let machine_st := machine_to_regState inst machine
   let model      := run 1 (regState_to_armState input)
   let model_st := model_to_regState inst model
-  regStates_match input machine_st model_st
+  regStates_match uniqueBaseName input machine_st model_st
 
 /--
 Make a task for running a single test.

Arm/Memory/Separate.lean

@@ -582,7 +582,7 @@ theorem read_mem_bytes_write_mem_bytes_eq_extract_LsB_of_mem_subset
           rw [BitVec.le_def] at hstart
           omega
     · simp only [h₁, bitvec_rules, minimal_theory]
-      intros h
+      intros 
       apply BitVec.getLsb_ge
       omega
 

Arm/MinTheory.lean

@@ -94,6 +94,8 @@ attribute [minimal_theory] bne_iff_ne
 attribute [minimal_theory] Bool.false_eq
 attribute [minimal_theory] Bool.and_eq_false_imp
 
+attribute [minimal_theory] Decidable.not_not
+
 attribute [minimal_theory] Nat.le_zero_eq
 attribute [minimal_theory] Nat.zero_add
 attribute [minimal_theory] Nat.zero_eq

Correctness/ArmSpec.lean

@@ -1,3 +1,12 @@
+/-
+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
+
+Specializing the Correctness module for use with our specification of the Arm
+ISA.
+-/
+
 import Arm.Exec
 import Correctness.Correctness
 
@@ -18,4 +27,20 @@ theorem arm_run (n : Nat) (s : ArmState) :
     simp only [Sys.run, Sys.next, run]
     rw [h]
 
+-- (TODO) Move to Arm/BitVec.lean?
+/-- Unexpander to represent bitvector literals in hexadecimal -- this overrides
+  the unexpander in the Lean BitVec library. -/
+@[app_unexpander BitVec.ofNat] def unexpandBitVecOfNatToHex : Lean.PrettyPrinter.Unexpander
+  | `($(_) $n:num $i:num) =>
+      let i' := i.getNat
+      let n' := n.getNat
+      let trimmed_hex := -- Remove leading zeroes...
+        String.dropWhile (BitVec.ofNat n' i').toHex
+                         (fun c => c = '0')
+                         -- ... but keep one if the literal is all zeros.
+      let trimmed_hex := if trimmed_hex.isEmpty then "0" else trimmed_hex
+      let bv := Lean.Syntax.mkNumLit s!"0x{trimmed_hex}#{n'}"
+      `($bv:num)
+  | _ => throw ()
+
 end Correctness

Correctness/Correctness.lean

@@ -142,7 +142,8 @@ theorem partial_correctness_from_verification_conditions [Sys σ] [Spec' σ]
     (v1 : ∀ s0 : σ, pre s0 → assert s0 s0)
     (v2 : ∀ sf : σ, exit sf → cut sf)
     (v3 : ∀ s0 sf : σ, assert s0 sf → exit sf → post s0 sf)
-    (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (nextc (next si)))
+    -- We prefer to use `run` instead of `step`.
+    (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (nextc (run si 1)))
     : PartialCorrectness σ :=
   fun s0 n hp hexit =>
     let rec find (i : Nat) (h : assert s0 (run s0 i)) (hle : i ≤ n) :