Prove the partial correctness of a small program with a loop #91
Conversation
|
Any idea what's up with the mismatch here? |
No, it's bizarre. Didn't touch any instruction semantics. Trying to debug... |
|
I couldn't reproduce the alleged mismatch. I'm inclined to think the failure is bogus, but I don't know how to isolate the problem yet. |
|
@shigoel Another nice thing would be to print the random seed we use so we can rerun a test. |
|
We do print out the inputs to the |
|
@alexkeizer Whenever you get the chance, it'd be great to have your eyes here from the point of view of symbolic simulation automation. (We could discuss in person next week too). |
| -- (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 () | ||
|
|
There was a problem hiding this comment.
Cool! I think this would be useful to have more broadly; especially since we name step-theorems according to their address in hex
There was a problem hiding this comment.
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...
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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
Proofs/Experiments/AbsVCG.lean
Outdated
| -- (FIXME) We don't really need the stack pointer to be aligned, but the | ||
| -- `sym1_n` tactic expects this. Can we make this optional? | ||
| CheckSPAlignment s |
There was a problem hiding this comment.
Yes, we totally can make it optional (I wasn't sure if there was a need for that, but seems like there is)
| theorem nextc_to_run_from_0x4005d0 (h : abs_pre s0) : | ||
| (Correctness.nextc (Sys.run s0 1)) = run 4 s0 := by | ||
| simp only [abs_pre, state_simp_rules] at h | ||
| obtain ⟨h_s0_pc, h_s0_program, h_s0_err, h_s0_sp_aligned⟩ := h | ||
| simp only | ||
| [Correctness.nextc, Correctness.arm_run, | ||
| Spec'.cut, minimal_theory] | ||
|
|
There was a problem hiding this comment.
Interesting. I assume this serves to decouple the reasoning about the number of steps to take from the reasoning about the effects of these steps (so that we can use existing symbolic eval machinery for the latter).
It does feel a bit repetitive, so I imagine we would still like to integrate some of this step-by-step reasoning into the tactic
There was a problem hiding this comment.
Yes, that's exactly right. And I'm glad this appears repetitive --- that was the goal, to see if there's a pattern that can be mechanized.
I'm hoping we can avoid such nextc_to_run.. theorems entirely, and provide automation for theorems like effects_of_nextc_.. directly where the number of steps to simulate and the effects are determined "dynamically" in tandem. If possible, it'd be good to build support for this atop the existing symbolic eval machinery so that we're not married to the VCG approach for all LNSym proofs. E.g., the VCG approach is pretty tedious for verifying straight-line code but convenient for loops. For the former, we could use the existing symbolic eval machinery to simulate the code and then immediately reason about the program's effects. For the latter, we could use the VCG-supporting symbolic eval machinery.
Proofs/Experiments/AddLoop.lean
Outdated
| -- (FIXME) Obtain *_cut theorems for each instruction automatically. | ||
|
|
||
| theorem program.stepi_0x4005a4_cut (s sn : ArmState) | ||
| (h_program : s.program = program) | ||
| (h_pc : r StateField.PC s = 0x4005a4#64) | ||
| (h_err : r StateField.ERR s = StateError.None) | ||
| (h_sp_aligned : CheckSPAlignment s) | ||
| (h_step : sn = run 1 s) : | ||
| cut sn = false ∧ | ||
| r StateField.PC sn = 0x4005b0#64 ∧ | ||
| r StateField.ERR sn = .None ∧ | ||
| sn.program = program ∧ | ||
| CheckSPAlignment sn := by | ||
| have := program.stepi_0x4005a4 s (stepi s) h_program h_pc h_err | ||
| simp only [minimal_theory] at this | ||
| simp_all only [run, cut, this, | ||
| state_simp_rules, bitvec_rules, minimal_theory] | ||
| done |
There was a problem hiding this comment.
What do we want out of the _cut theorems exactly? It seems to combine axiomatizing the effects with reasoning about whether some specific instruction is a cutpoint.
I guess you mean we should incorporate the axiomatic effects into the regular stepi theorems, and then build a second layer on top that adds a conjunct with cut sn = true/false to it?
There was a problem hiding this comment.
I guess you mean we should incorporate the axiomatic effects into the regular
stepitheorems, and then build a second layer on top that adds a conjunct withcut sn = true/falseto it?
Yes, that'd certainly be helpful. All these _cut theorems do is help in the unwinding of Correctness.nextc: cut sn = true/false is there for obvious reasons, but the rest of the conjuncts help in relieving the hyps. of the next applicable _cut theorem.
Proofs/Experiments/AddLoop.lean
Outdated
| -- TODO: Tactic to "explode" conjunctions? | ||
| obtain ⟨h_s0_pc, h_s0_program, h_s0_err, h_s0_sp_aligned⟩ := h_pre | ||
| -- Symbolic simulation | ||
| -- (FIXME) sym1_n doesn't play well with unconditional branches. |
There was a problem hiding this comment.
Good point, right now I've assumed the PC simply increments each instruction. I should implement something more sophisticated
| -- (FIXME) better stepi lemma generation | ||
| simp (config := {ground := true}) only at h_step_2 |
There was a problem hiding this comment.
What, concretely, needs improving here?
There was a problem hiding this comment.
Badly placed comment there. sym1_n 1 at s1 (the previous tactic) generates proof state with subterms like:
(AddWithCarry (r (StateField.GPR 0x0#5) s1)
(Decidable.rec (fun h => (0x0#1, 0x0#64)) (fun h => (0x1#1, 0xffffffffffffffff#64))
(instDecidableEqBitVec 0x1#1 0x1#1)).snd
(Decidable.rec (fun h => (0x0#1, 0x0#64)) (fun h => (0x1#1, 0xffffffffffffffff#64))
(instDecidableEqBitVec 0x1#1 0x1#1)).fst)
which are simplified to the following with simp/ground.
(AddWithCarry (r (StateField.GPR 0x0#5) s1) 0xffffffffffffffff#64 0x1#1)
In an ideal world, we shouldn't need this simp/ground.
…ts.SHA2.SHA512Program in proofs
Description:
Used the verification condition generation framework to prove the partial correctness of a simple (memory access free) program with a loop that computes the addition of two numbers
xandyby incrementingyby onextimes. Proof of termination remains to be done.Also simplified the
AbsVCGproof by leveraging thesym1_ntactic.Testing:
make allsucceeds.License:
By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.