docs: PROOF-NEEDS regenerated against reality; measured figures in STATE/TOPOLOGY (D2+D3)

[hyperpolymath]

Closes debt items D2 and D3 from docs/sitrep-2026-09-01.adoc.

D2 — PROOF-NEEDS.adoc (full regeneration)

The 2026-03-29 revision no longer described the tree: it claimed Obj.magic sites in ReScript files that left main with the eradication, claimed the ABI .idr files were removed (they exist, and the vexometer/ set is real domain content), and omitted the Ada core entirely. The regenerated doc:

• three-tier .idr inventory: real domain specs (vexometer/src/abi/*, vext/Types.idr with its length-indexed Chain giving append-monotonicity by construction) / one unresolved {{PROJECT}} placeholder (vext/Layout.idr) / self-describing customization stubs;
• new Ada core section: exactly 4 Pre/Post aspects (vexometer-metrics.ads), no SPARK_Mode — with the 09-01 Aggregate_Profile undefined-memory defect as the concrete motivation for SPARK flow analysis;
• new efficacy evaluator proof candidates (D_ISA arithmetic, frontier monotonicity, acceptance-rule totality) and the forbid(unsafe_code) ratchet gap (present only in lazy-eliminator);
• a verification-commands appendix — every command was re-run immediately before commit and the outputs match the claims (one claim was corrected in the process: the {{ grep also hits satellite-template's Foreign.idr, but only in a by-design TODO comment).

D3 — STATE.a2ml / TOPOLOGY.adoc (measured or labeled)

Done-condition: figures carry the command that measured them; assertion count distinguishes sites from executions.

• STATE.a2ml: every measured figure now names its command — cargo test sums per crate (lazy-eliminator 55, vext 36, efficacy 15, all re-run today) and the exact static-assertion-site count 52 via grep -cE '^ *Assert_True *\(' vexometer/tests/test_runner.adb (replaces the untethered "~55"); the 1282 executions-vs-sites NOTE stays and now points at the exact command.
• The 25-vs-70 completion contradiction is resolved by single-sourcing: completion-percentage mirrors the TOPOLOGY dashboard OVERALL row and is explicitly labeled an estimate.
• TOPOLOGY.adoc: SPDX + the Last updated comment its own Update Protocol references but lacked; an estimates legend (percentages are estimates, measured figures live in STATE.a2ml); an Efficacy Evaluator row (60%, per the Update Protocol's add-a-row rule after PR feat(efficacy): D5 tooling — evaluator, frontier writer, validator #70); OVERALL de-tilded to 70%.

Noted assumption: dashboard percentages remain labeled estimates rather than being eradicated — nothing measures "completion"; manufacturing a proxy (e.g. roadmap-checkbox ratios) would be fake precision. Shout if you'd rather drop the percentages entirely.

None of the three files is trust-manifest-tracked (verified by grep); must-all and trust-manifest-verify pass locally.

🤖 Generated with Claude Code

[coderabbitai]

Warning

Review limit reached

Next included review available in 37 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Team

Run ID: 98d763e3-8d5a-4fb5-a2dc-cd3fb66c77fd

📥 Commits

Reviewing files that changed from the base of the PR and between e768bf1 and e4c43de.

📒 Files selected for processing (3)

• .machine_readable/6a2/STATE.a2ml
• PROOF-NEEDS.adoc
• TOPOLOGY.adoc

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}