Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prove the partial correctness of a small program with a loop #91

Merged
merged 12 commits into from
Aug 20, 2024
Merged

Prove the partial correctness of a small program with a loop #91

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
9626294
Prove the partial correctness of a small program with a loop
shigoel Aug 16, 2024
c9db156
Merge branch 'main' into add_loop_vcg
shigoel Aug 16, 2024
a93740d
Cosim: Print uniqueBaseName in case of a mismatch
shigoel Aug 16, 2024
9654cdf
Merge branch 'main' into add_loop_vcg
shigoel Aug 16, 2024
da148df
Merge branch 'main' into add_loop_vcg
shigoel Aug 19, 2024
950b9d5
Add missing Copyright header for Correctness/ArmSpec.lean
shigoel Aug 19, 2024
3948c2d
Merge branch 'main' into add_loop_vcg
shigoel Aug 19, 2024
796c414
Fix build; use genEqStepThms
shigoel Aug 20, 2024
0e95f55
Merge branch 'main' into add_loop_vcg
shigoel Aug 20, 2024
de6f994
Merge branch 'main' into add_loop_vcg
shigoel Aug 20, 2024
a395bba
Use `sym_n` instead of `sym1_n`; delete old #genStepTheorems, use Tes…
shigoel Aug 20, 2024
65d6660
Fix case in file names
shigoel Aug 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions Arm/Cosim.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}"
Expand All @@ -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.
Expand Down
2 changes: 2 additions & 0 deletions Arm/MinTheory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 16 additions & 0 deletions Correctness/ArmSpec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,4 +18,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 ()

Comment on lines +30 to +45
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cool! I think this would be useful to have more broadly; especially since we name step-theorems according to their address in hex

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One reason why I'm hesitant re. this unexpander is that register indices also appear in hex then. E.g., StateField.GPR 0xc#5 and StateField.SFP 0xd#5, which is inconvenient.

Maybe we need more directed unexpanders...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Something I've been thinking about: it might be nice to introduce a simple abbreviation for addresses and raw instructions

abbrev Address := BitVec 64

abbrev RawInstr := BitVec 32

Then, we could somehow define the unexpanders to apply just for those types, not for all bitvectors

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that's a good idea, regardless of the unexpander issue.

Note that it also helps to see machine components' values as hex; for instance, consider:

r (StateField.GPR 1#5) s = 18446744073709551614#64

vs.

r (StateField.GPR 1#5) s = 0xfffffffffffffffe#64

end Correctness
3 changes: 2 additions & 1 deletion Correctness/Correctness.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand Down
Loading