Repository navigation
fix: require the postcondition at the final state in Omni.loopDone - #315
Conversation
The loopDone rule concluded Omni for an arbitrary postcondition from the bounds check alone, so any zero-iteration loop satisfied every postcondition, including one rejecting all outcomes. Add the premise Q (some (st, ())), mirroring skip, and discharge it in the two affected proofs (Omni.frame's loopDone case, STHoare.loopDone_intro). No handwritten theorem statement changes.
Five theorems pin the repaired behavior: an empty loop's Omni judgment is equivalent to the postcondition at the unchanged state, preserves the state and returns unit, rejects an always-false postcondition at both the Omni and STHoare levels, and preserves any separation-logic precondition. The Tests glob picks the module up automatically.
iamrecursion
left a comment
iamrecursion
left a comment
There was a problem hiding this comment.
Thanks so much for your contribution!
Fundamentally the change is sound. What I've suggested here is some minor cleanups more than anything!
| #print axioms empty_loop_iff | ||
| #print axioms empty_loop_preserves_state | ||
| #print axioms empty_loop_rejects_false | ||
| #print axioms empty_loop_triple | ||
| #print axioms empty_loop_rejects_false_triple |
There was a problem hiding this comment.
These don't check anything, so I think they can be removed.
There was a problem hiding this comment.
Removed the five #print axioms commands.
| theorem empty_loop_preserves_state (p : Prime) (Γ : Env) (st : State p) | ||
| {lo hi : U s} {body : U s → Expr (Tp.denote p) tp} (hle : lo ≥ hi) : | ||
| Omni p Γ st (.loop lo hi body) (fun result => result = some (st, ())) := by | ||
| exact Omni.loopDone hle rfl | ||
|
|
||
| theorem empty_loop_rejects_false (p : Prime) (Γ : Env) (st : State p) | ||
| {lo hi : U s} {body : U s → Expr (Tp.denote p) tp} (hle : lo ≥ hi) : | ||
| ¬ Omni p Γ st (.loop lo hi body) (fun _ => False) := by | ||
| intro h | ||
| exact (empty_loop_iff p Γ st _ hle).mp h | ||
|
|
||
| theorem empty_loop_triple (p : Prime) (Γ : Env) (P : SLP (State p)) | ||
| {lo hi : U s} {body : U s → Expr (Tp.denote p) tp} (hle : lo ≥ hi) : | ||
| STHoare p Γ P (.loop lo hi body) (fun _ => P) := by | ||
| intro H st hp | ||
| apply Omni.loopDone hle | ||
| exact SLP.ent_star_top st hp |
There was a problem hiding this comment.
These all fall out directly, so it is probably worth a comment that empty_loop_iff and empty_loop_rejects_false_triple are sufficient to pin the fixed behaviour. I would keep these three for documentation clarity, however.
There was a problem hiding this comment.
Kept all three and added the comment naming empty_loop_iff and empty_loop_rejects_false_triple as sufficient.
| exact SLP.ent_star_top st hp | ||
|
|
||
| theorem empty_loop_rejects_false_triple (p : Prime) (Γ : Env) : | ||
| ¬ STHoare p Γ ⟦⟧ (.loop (0 : U 32) 0 (fun _ => .skip)) (fun _ => ⟦False⟧) := by |
There was a problem hiding this comment.
This should take hle the same way as its siblings and be general over any lo ≥ hi.
There was a problem hiding this comment.
Generalized it to arbitrary bounds and body, with hle : lo ≥ hi.
| intro h | ||
| exact (empty_loop_iff p Γ st _ hle).mp h | ||
|
|
||
| theorem empty_loop_triple (p : Prime) (Γ : Env) (P : SLP (State p)) |
There was a problem hiding this comment.
This honestly probably makes more sense as a library lemma. It is strictly stronger than loopDone_intro with (⟦⟧, lo = lo) so I suggest moving it next to that so others can benefit.
There was a problem hiding this comment.
Moved the proof to STHoare.loopDone_intro_of_ge beside loopDone_intro. Kept empty_loop_triple as a one-line wrapper.
- Remove the five #print axioms commands (they only logged output). - Note that empty_loop_iff and empty_loop_rejects_false_triple pin the fixed behaviour; keep the three derived theorems for documentation. - Generalize empty_loop_rejects_false_triple over any lo >= hi with hle. - Move the general empty-loop triple into Hoare/SepTotal.lean as loopDone_intro_of_ge, beside loopDone_intro.
|
Thanks for the review! All four addressed. |
iamrecursion
left a comment
iamrecursion
left a comment
There was a problem hiding this comment.
Looks great! Thank you so much!
2 participants
Fixes #314.
The
loopDonerule concluded theOmnijudgment for an arbitrary postcondition from the bounds check alone, so a zero-iteration loop satisfied every postcondition, and throughletInit discharged any continuation's obligation unchecked. Details and reproduction are in #314.This adds the premise
Q (some (st, ())), mirroringskip, and repairs the two proofs that build the rule directly: theloopDonecase ofOmni.frameandSTHoare.loopDone_intro. No handwritten theorem statement changes.Tests/LoopDone.leanadds five regression theorems; the existingTestsglob discovers the module.Verified at the pinned
leanprover/lean4:v4.29.1toolchain on top of919a387:lake build Lampeandlake build Testsare clean before and after, and the exploit proofs from #314 no longer elaborate.