resalgebraNoAxioms: Verify global validity of ghost locations#43
Merged
Conversation
Adds a product-of-in-use-values invariant to GlobalMem() and proves all four ghost operations maintain it. The new product.gobra builds up ProductOfSeq with the structural lemmas (Concat, AdjacentSwap, MoveFront, ExtractOne, ExtractThree) and the maintenance lemmas (ProductSplitEq, ProductMergeAt, ProductFPUEq); the structural ones are pure so they can be applied inside forall bodies via `let _ := lemma(...)`. The previous `assume` in GhostOp2WI is replaced by an assert-forall that calls ExtractThreeValid on the captured value seq. Verified with `--noassumeInjectivityOnInhale` (CI flag). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
jcp19
commented
Apr 25, 2026
- Trim docstrings (drop redundant "non-empty"/"pure so it can be used"/"Pure recursion on k" notes)
- Use `0 < len(...)` instead of `len(...) >= 1`
- Mark `pure func ... Unit` lemmas as `opaque` (cuts verification from ~35 min to ~2.5 min)
- Drop trailing `let _ := X in Unit{}` in favor of just `X` since `asserting`/RA-method calls already return Unit
- Drop redundant `len` and `IsElem` clauses already implied by other pre/postconditions
The `requires forall j :: IsElem(s[j])` in ExtractOneValid is kept because it's needed for well-formedness of the immediately-following `requires ra.IsValid(ProductOfSeq(s, ra))`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…perproject/gobra-libs into proof-remaining-assumption-resalgebra
- loc.gobra: drop wildcard `_` permission amounts in pure-func preconditions (`acc(&inUseIdx, _)` → `acc(&inUseIdx)`); idxPos: drop redundant `requires len(s) >= 1` (implied by `x elem s`). - product.gobra: drop redundant `IsElem` ensures clauses in ExtractOneValid, ProductSplitEq, ProductMergeAt, and ProductFPUEq (callers can derive them from the input precondition / from RA.Compose's IsElem ensures). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
jcp19
commented
Apr 27, 2026
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
jcp19
commented
Apr 27, 2026
| requires 0 < len(s1) && 0 < len(s2) | ||
| requires forall j int :: { s1[j] } 0 <= j && j < len(s1) ==> ra.IsElem(s1[j]) | ||
| requires forall j int :: { s2[j] } 0 <= j && j < len(s2) ==> ra.IsElem(s2[j]) | ||
| ensures forall j int :: { (s1 ++ s2)[j] } 0 <= j && j < len(s1 ++ s2) ==> ra.IsElem((s1 ++ s2)[j]) |
Collaborator
Author
There was a problem hiding this comment.
postcondition may be unnecessary?
| ghost | ||
| opaque | ||
| requires ra != nil | ||
| requires len(s) >= 3 |
Collaborator
Author
There was a problem hiding this comment.
precondition might be unnecessary? it is implied by
requires 0 <= p1 && p1 < len(s)
requires 0 <= p2 && p2 < len(s)
requires 0 <= p3 && p3 < len(s)
requires p1 != p2 && p1 != p3 && p2 != p3
| // (Non-pure variant retained for the lemma chain in maintenance proofs.) | ||
| ghost | ||
| requires ra != nil | ||
| requires 0 < len(s) |
Collaborator
Author
There was a problem hiding this comment.
precondition unnecessary
| // The merged value lives at min(p1, p2); max(p1, p2) is removed. | ||
| ghost | ||
| requires ra != nil | ||
| requires len(s) >= 2 |
Collaborator
Author
There was a problem hiding this comment.
Suggested change
| requires len(s) >= 2 |
| let pmax := p1 < p2 ? p2 : p1 in | ||
| let merged := ra.Compose(s[p1], s[p2]) in | ||
| let s2 := s[:pmin] ++ seq[Elem]{merged} ++ s[pmin+1:pmax] ++ s[pmax+1:] in | ||
| len(s2) == len(s) - 1 && |
Collaborator
Author
There was a problem hiding this comment.
drop conjunct, probably unnecessary
| requires IsFramePreservingUpdate(ra, e1, e2) | ||
| requires ra.IsValid(ProductOfSeq(s, ra)) | ||
| ensures let s2 := s[:posI] ++ seq[Elem]{e2} ++ s[posI+1:] in | ||
| len(s2) == len(s) && |
Collaborator
Author
There was a problem hiding this comment.
conjunct probably unnecessary
- ProductOfSeqConcat: drop redundant `forall j .. IsElem((s1++s2)[j])` ensures - ExtractThreeValid: drop `requires len(s) >= 3` (implied by the three position bounds with distinctness); reorder so the position requires precede `ra.IsValid(ProductOfSeq(s, ra))` (the latter calls ProductOfSeq, whose own precondition needs `0 < len(s)`, which Gobra derives from a position bound only if it appears earlier in the requires list) - ExtractOneValid: drop `requires 0 < len(s)` (implied by `0 <= p && p < len(s)`); reorder for the same well-formedness reason - ProductMergeAt: drop `requires len(s) >= 2` (implied by two distinct in-bounds positions) The `len ==` ensures clauses on AdjacentSwapProduct, ProductOfSeqMoveFront, ExtractOneValid, ProductMergeAt, ProductFPUEq are kept — removing them caused `GhostOp1WI`/`GhostOp2WI`'s maintenance proofs to time out (Gobra needs the explicit length facts at the call sites; deriving them on the fly from the seq construction triggered exponential search). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
jcp19
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a product-of-in-use-values invariant to GlobalMem() and proves all four ghost operations maintain it. The new
product.gobrabuilds upProductOfSeqwith the structural lemmas (Concat,AdjacentSwap,MoveFront,ExtractOne,ExtractThree) and the maintenance lemmas (ProductSplitEq,ProductMergeAt,ProductFPUEq).