docs: claim-verification pass — fix v0.1.0 status drift (#97) + gate it - #112
Merged
Conversation
A README is a claim about the system, gated the same way as a requirement. Audited every load-bearing README/doc claim against live source and bound the survivors to a claim-check gate so they can't silently rot again. Fixed drift (issue #97): - README status said "v0.1.0 shipped … no real abstract-interpretation logic yet" while the crate is v3.2.4 with 12 published domains + 19 admit-free proofs. Rewrote it to the true v3.2.4 state, with soundness stated SCOPED (mechanized Rocq vs γ-sweep-validated), not flattened. - architecture.md §6 + the feature-loop diagram still described "the v0.1 scaffold" as current (analyze = constant_i32(42); "real fixpoint ⏳"; "pending v0.1.0 tag") — reframed to historical + the shipped reality. Mark → bind → gate: - claims.yaml binds 5 load-bearing claims to predicates RE-DERIVED FROM SOURCE (version vs Cargo.toml, 0 Admitted/admit/Axiom across proofs/rocq/*.v, 12 scry-sai-* crates in publish.rs, WrapAdd.v exists, the scoped-soundness wording) — never a number typed in prose. - tools/claim-check.py (vendored from the skill) + a NEW `count-min` predicate I added: count-max greens a 0-match (measures nothing) for a PRESENCE claim like the version string; count-min is the dual that catches drift-to-absent. Verified the gate bites: version drift → red, a stray admit → red. - CI `claim-check` job runs it on every push/PR. Re-derived counts confirming the honest claims: 19 .v proofs, 0 admits/axioms; 12 published scry-sai-* crates. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
Closes #97. A README is a claim about the system — the same species as a requirement — and it rots for the same reason: no gate. This audits every load-bearing README/doc claim against live source and binds the survivors to a
claim-checkgate.Fixed drift
architecture.md: §6 + the feature-loop diagram described "the v0.1 scaffold" as current (analyze=constant_i32(42); "real fixpoint ⏳"; "pending v0.1.0 tag") → reframed to historical + shipped reality.Mark → bind → gate
claims.yamlbinds 5 load-bearing claims to predicates re-derived from source (version↔Cargo.toml,0 Admitted/admit/Axiomacrossproofs/rocq/*.v, 12scry-sai-*inpublish.rs,WrapAdd.vexists, the scoped-soundness wording) — never a typed number.tools/claim-check.py(vendored) + a newcount-minpredicate I added:count-maxgreens a 0-match for a presence claim (the "oracle that measures nothing" — I hit it on the version claim and fixed it);count-minis the dual that catches drift-to-absent. Verified the gate bites both ways (version drift → red, stray admit → red).claim-checkjob runs it on every push/PR — so the status can't silently rot ~40 versions again.Re-derived: 19
.vproofs, 0 admits/axioms; 12 published crates.rivet validatePASS;claim-check5/5 green.🤖 Generated with Claude Code
Also closes #111 (same stale-status-block drift as #97; both surfaced by the doc-drift audit — this fixes the block to the actual current v3.2.4, past #111's v3.0.0 ask).