[Property Coverage] Prove view-function correctness & read-only properties for Counter and Vault - #2056
Merged
Merged
Conversation
Add three kernel-verified theorems (zero sorry, zero new axioms) for the Counter contract's previously-unproven preview view functions: - previewAddTwice_correct: closed-form result add (add count delta) delta - previewAddTwice_preserves_state: read-only (state unchanged) - previewOps_preserves_state: pure arithmetic pipeline is read-only Regenerate manifest, PrintAxioms, verification_status, and doc theorem counts (291 -> 294 proven). List the three lemma-style properties in property_exclusions.json, consistent with existing Counter read-only exclusions. Co-Authored-By: Claude <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
…tions Adds six fully-proven theorems (zero sorry, zero new axioms) for the Vault example's view functions, which previously had no proofs: - totalAssets_meets_spec / totalAssets_preserves_state - totalSupply_meets_spec / totalSupply_preserves_state - balanceOf_meets_spec / balanceOf_preserves_state Each meets_spec establishes the closed-form read result against the existing Contracts.Vault.Spec; each preserves_state establishes the function is read-only. Regenerates manifest, exclusions, verification status, PrintAxioms, and README/llms.txt theorem counts (294 -> 300 proven).
Th0rgal
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.
Summary
Increases the proven fragment by 9 fully-proven theorems (zero
sorry, zero new axioms) coveringview-family functions on two example contracts that previously had no proofs. Proven theorem count: 291 → 300.Counter
previewview functions (+3)previewAddTwice_correct— closed-form result:previewAddTwice deltareturnsadd (add (count) delta) delta.previewAddTwice_preserves_state—previewAddTwiceis read-only (state unchanged).previewOps_preserves_state— the pure arithmetic pipelinepreviewOpsis read-only (state unchanged).Vault view functions (+6)
totalAssets_meets_spec/totalAssets_preserves_state— slot-0 read meetstotalAssets_spec; read-only.totalSupply_meets_spec/totalSupply_preserves_state— slot-1 read meetstotalSupply_spec; read-only.balanceOf_meets_spec/balanceOf_preserves_state— mapping (slot 2) read meetsbalanceOf_spec; read-only.Each
*_meets_specis proven against the existing spec surface inContracts.Vault.Spec/Contracts.Counter.Spec; each*_preserves_stateestablishes the function never writes storage.Changes
Contracts/Counter/Proofs/Preview.lean(new) — the three Counter theorems.Contracts/Counter.lean— import the new Counter proofs module.Contracts/Vault/Proofs/Correctness.lean— replace placeholder with the six Vault view-function theorems.test/property_exclusions.json— list the nine read-only/closed-form lemmas as coverage exclusions (consistent with existing read-only/preservation exclusions).test/property_manifest.json,PrintAxioms.lean,artifacts/verification_status.json,docs/VERIFICATION_STATUS.md, README/llms.txt theorem counts.Test plan
lake build Contracts.Counterandlake build Contracts.Vault.Proofs.Correctnesscompile green, zero warnings (proofs verified by the Lean kernel).python3 scripts/property_pipeline.py check— manifest/coverage/lean-sync all pass.generate_verification_status.py --check,generate_print_axioms.py --check,update_doc_numbers.py --check,check_verification_status_doc.py,lean_lint --only proof_lengthall pass.sorry; zero new custom axioms (AXIOMS.md unchanged).