feat(efficacy): D5 tooling — evaluator, frontier writer, validator - #70
Merged
Conversation
Implements the executable half of docs/EFFICACY-PROTOCOL.adoc as a new registered component, vexometer-efficacy (Rust, serde only): - `report` computes G_m, collateral deltas, D_ISA under the METRICS.adoc default weights, the capability proxy, and the six-verdict acceptance rule with its precedence order, emitting vexometer-efficacy-v2. - `attempt` maintains vexometer-frontier-v1 records and enforces the monotone-frontier invariant before writing. - `validate` recomputes every derived number in both document shapes; bare paths are routed by the document's own version field. Where the protocol is normatively undecided (issue #69, D1a–D1d) the tool refuses with an explicit awaiting-ruling error (exit 2) or warns (D1d) instead of guessing; D1e lifting is deliberately unimplemented. The protocol's own example JSON blocks are extracted from the .adoc at test time and used as fixtures: the validator must accept both and the evaluator must reproduce the efficacy example value-for-value (including isa_delta -2.71). Protocol/implementation drift fails `cargo test` loudly. Registered in run-must-gates.sh, generate/verify-manifest.sh, and the Justfile (build/test wiring plus efficacy-report / efficacy-attempt / efficacy-validate with positional-arguments forwarding). Full scaffolding: README/ROADMAP/SECURITY, Mustfile, Trustfile.a2ml, generated trust manifest, committed Cargo.lock. `just ci-gate` green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
Resolves the Hypatia code-scanning alert (code_safety/unwrap_without_check, CWE-754) raised on PR #70: the frontier writer returned the just-pushed attempt via .last().unwrap(). Logically infallible, but now expressed as a total ok_or_else in the same style as the surrounding error paths. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Important Approval pendingCodeRabbit has no unresolved comments, but it has not reviewed the latest commit. Use the checkbox below to review the latest commit. CodeRabbit will approve the changes if it finds no blocking issues.
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. Comment |
hyperpolymath
added a commit
that referenced
this pull request
Sep 1, 2026
…ATE/TOPOLOGY (D2+D3) (#72) 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 #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](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <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
2 participants
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.
Implements debt item D5 from the merged sitrep (
docs/sitrep-2026-09-01.adoc): the executable half ofdocs/EFFICACY-PROTOCOL.adoc, as a new Rust componentvexometer-efficacy/.What it does
report— computesG_m, collateral deltas, weightedD_ISA(METRICS.adoc weights), the 13-probe capability proxy, applies the six-verdict acceptance rule with its precedence order, and emitsvexometer-efficacy-v2documents.attempt— maintainsvexometer-frontier-v1records under the monotone-frontier invariant (refuses to append to a record that already violates it).validate— recomputes every derived number in both document shapes; bare file arguments are auto-routed by theirversionfield.Exposed at the monorepo root as
just efficacy-report / efficacy-attempt / efficacy-validate.Refuses where the protocol is undecided
Where an open question from issue #69 (D1) bites, the tool refuses with an explicit error naming the question (exit 2) instead of silently picking a semantic: D1a (zero baseline), D1b (aggregate vs per-probe gate disagreement), D1c (mixed multi-target outcomes). D1d (plural targets with singular
frontier_record) warns; D1e (v1→v2 lifting) is unimplemented. After rulings land, these become the ruled semantics in the v2.1 amendment.The protocol's examples are the test fixtures
The integration tests extract the JSON example blocks from
docs/EFFICACY-PROTOCOL.adocat test time and require the evaluator to reproduce the efficacy example value-for-value (includingisa_delta = -2.71). Protocol and implementation cannot drift apart silently. 15 tests, all green.Component registration
Full scaffolding per the scaffold-before-sweep ruling: README/ROADMAP/SECURITY (AsciiDoc), Mustfile, Trustfile.a2ml, generated trust manifest; registered in
run-must-gates.shand both trust scripts; wired intobuild-all,test-all,clean,fmt-check,lint.just ci-gate(must-all + trust-manifest-verify + test-all) passes locally end-to-end.Notes for review
set positional-arguments := true(supported since just 0.9.x) rather than the per-recipe[positional-arguments]attribute (needs just ≥ 1.29) because CI installs just from apt — ubuntu-latest ships 1.21, where an unknown attribute is a parse error that would kill every recipe.just fmt-checkandjust lintfail on main insidevext(formatting drift + 4 clippy findings in vext-core). Neither is part ofci-gateor the Quality Gates workflow.vexometer-efficacyitself is fmt- and clippy-clean under-D warnings.Closes nothing; relates to #69.
🤖 Generated with Claude Code