Prove the counting invariant (CVE-2024-53104 core) sorry-free; add roadmap and open challenges - #2
Merged
Merged
Conversation
…invariant, parse_no_div (statements, sorry)
lakefile.lean required Aeneas from ../../../aeneas-project/... which only exists locally, so the Lean project could not build from a clean clone (blocking the external prover). Convert to a git dependency pinned to the exact version the spike uses — AeneasVerif/aeneas @ c2015b8668ba6d5b41f5f19d00a881c12bbb0b5d (charon-pin 909ff09a / v0.1.220), subdir backends/lean, Lean/mathlib v4.31.0. Verified from a clean state (fresh dir, no .lake/manifest): lake update + lake exe cache get + lake build all exit 0 and build UvcParse + NoPanic. Regenerated lake-manifest.json records aeneas as a git dep at that commit (subDir backends/lean); it also corrects a stale root package name copied from the Binder spike (spike_binder_verif -> uvc_parse_verif). No proof, theorem, or NoPanic/UvcParse content changed (axiom audit identical: 5 sorry-free, 5 sorryAx). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…found the unbounded-a,b,c statement false); dischargeable from WellFormed (iv) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ph's decomposition), statements only
…tness loop principle (loop_ok_inv)
…ay_gen + monotone overflow discharge)
…ounting invariant block complete
… loop, contribution tasks
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.
Proves the counting-vs-writes invariant block of theorem (A), the core of the CVE-2024-53104 property, machine-checked sorry-free (counting_monotone, step_replay(_gen), replay, additive, plus a reusable Aeneas loop-invariant principle loop_ok_inv). #print axioms confirms standard axioms only.
Remaining for full (A): parse_no_div, frame_loop_invariant, assembly (tracked in ROADMAP.md).
Also adds ROADMAP.md (honest proof status, known hard problems) and OPEN_CHALLENGES.md (takeable contribution tasks).