hyperpolymath · hyperpolymath · Sep 1, 2026 · Sep 1, 2026
@@ -10,10 +10,11 @@ status = "active"
 
 [project-context]
 name = "vexometer"
-# NOTE: 25 here vs ~70% on the TOPOLOGY.adoc dashboard — neither is a measured
-# value; reconciliation is debt D3 in docs/sitrep-2026-09-01.adoc. Kept as-is
-# until a figure exists that names the command that produced it.
-completion-percentage = 25
+# NOTE (D3, 2026-09-01): this is an ESTIMATE, not a measurement — no command
+# produces it. Single source is the TOPOLOGY.adoc Completion Dashboard OVERALL
+# row; this field mirrors it so the two files can no longer contradict each
+# other (they previously said 25 vs ~70). Update TOPOLOGY first, then mirror.
+completion-percentage = 70
 phase = "CRG C achieved for both sub-projects (2026-04-04); CI gates first green 2026-09-01"
 
 [crg-status]
@@ -22,13 +23,27 @@ vexometer-ada = "CRG C: 1282 assertions (unit+P2P+E2E+contract+aspect), benchmar
 overall = "CRG C achieved 2026-04-04"
 
 [test-coverage]
-# Rust (lazy-eliminator)
+# Measurement convention (D3, 2026-09-01): every figure below names the
+# command that produced it; figures without a command are labeled estimates.
+# Rust counts = sum of `test result:` lines from `cargo test` in the crate dir.
+
+# Rust (lazy-eliminator) — measured 2026-09-01:
+#   cd lazy-eliminator && cargo test   -> 3+0+20+16+16 = 55 passed
 rust-unit-tests = "3 (analyzer.rs)"
 rust-e2e-tests = "16 (full pipeline)"
 rust-property-tests = "16 (proptest)"
 rust-aspect-tests = "20 (security/robustness/concurrency)"
 rust-benchmarks = "1 suite (Criterion)"
-rust-total = "55 tests, 100% pass rate"
+rust-total = "55 tests, 100% pass rate (lazy-eliminator only)"
+
+# Rust (vext) — measured 2026-09-01:
+#   cd vext && cargo test   -> 14+11+11 = 36 passed
+vext-total = "36 tests, 100% pass rate"
+
+# Rust (vexometer-efficacy) — measured 2026-09-01:
+#   cd vexometer-efficacy && cargo test   -> 15 passed
+#   (protocol JSON examples are the fixtures)
+efficacy-total = "15 tests, 100% pass rate"
 
 # Ada (vexometer core)
 ada-unit-tests = "6 (core, CII, patterns, probes, JSON loading)"
@@ -38,5 +53,8 @@ ada-contract-tests = "9 (CII bounds, ISA bounds, completeness)"
 ada-aspect-tests = "16 (empty input, long text, saturation, false-positive, probe invariants)"
 ada-benchmarks = "2 suites (10000 iterations each: pattern analysis + CII)"
 ada-total = "1282 assertions, 100% pass rate"
-# NOTE: counts assertion EXECUTIONS (p2p loops amplify 4 properties x 100
-# iterations), not static assertion sites (~55). See TEST-NEEDS.adoc.
+# NOTE: 1282 counts assertion EXECUTIONS at runtime (p2p loops amplify
+# 4 properties x 100 iterations), not static sites. Static sites — measured
+# 2026-09-01: grep -cE '^ *Assert_True *\(' vexometer/tests/test_runner.adb
+# -> 52 (all assertions route through Assert_True in test_runner.adb).
+# See TEST-NEEDS.adoc for the counting-convention discussion.
@@ -1,55 +1,145 @@
-== PROOF-NEEDS.md
+// SPDX-License-Identifier: CC-BY-SA-4.0
+== Proof Needs — vexometer monorepo
 
-=== Current State
+Regenerated 2026-09-01 against main (`e768bf1`); supersedes the
+2026-03-29 revision, whose inventory no longer matched the tree
+(see <<corrections>>). Debt item D2 of `docs/sitrep-2026-09-01.adoc`.
+Every claim here carries the command that measured it (<<verification>>).
 
-* *LOC*: ~32,000
-* *Languages*: Rust, ReScript, Idris2, Zig
-* *Existing ABI proofs*: `+lazy-eliminator/src/abi/*.idr+`
-(template-level)
-* *Dangerous patterns*:
-** `+vext/vext-tools/src/bindings/Std.res+`: 2 `+Obj.magic+` for CLI
-argument parsing
-** `+vext/vext-tools/src/hooks/Git.res+`: 1 `+Obj.magic+` for
-notification serialization
+=== Current State
 
+* *Languages*: Ada 2022 (ISA analysis core), Rust (vext, lazy-eliminator,
+  vexometer-efficacy), Idris2 (ABI specifications), Zig (FFI shim).
+  ReScript is gone from main — zero `.res` files remain, so the
+  historical `Obj.magic` sites in `vext/vext-tools` no longer exist.
+* *Rust memory safety*: `lazy-eliminator` declares
+  `#![forbid(unsafe_code)]` (lib.rs line 14). `vext` and
+  `vexometer-efficacy` contain no `unsafe` blocks but do NOT yet carry
+  the forbid attribute — adding it is a cheap ratchet (see
+  <<what-needs-proving>>).
+* *Ada contracts*: exactly 4 Pre/Post aspects, all in
+  `vexometer/src/vexometer-metrics.ads`. No `SPARK_Mode` anywhere; the
+  contracts are runtime-checked when assertions are enabled, not
+  statically proven.
+* *Not proofs*: the 1,282 Ada test-assertion executions counted in
+  `.machine_readable/6a2/STATE.a2ml` are test executions, not proof
+  obligations.
+
+=== Formal artifact inventory (10 `.idr` files, three tiers)
+
+*Tier 1 — real domain specifications:*
+
+* `vexometer/src/abi/Types.idr`, `Foreign.idr`, `Layout.idr` — the
+  Ada↔Zig FFI contract for the analysis engine: metric-category
+  encodings matching `Metric_Category` in `vexometer-core.ads`, FFI
+  declarations implemented by `vexometer/ffi/zig/src/main.zig`, and
+  struct layout/alignment statements for the C-convention records.
+* `vext/src/abi/Types.idr` — `%default total`; the length-indexed
+  `Chain : Nat -> Type` makes append-monotonicity hold *by
+  construction* (`appendIncreases : Chain n -> String -> Chain (S n)`).
+  Of the three properties its header claims, only this one is
+  mechanized; attestation-requires-valid-chain and
+  verification-is-constructive are stated intent.
+
+*Tier 2 — template with an unresolved placeholder:*
+
+* `vext/src/abi/Layout.idr` — generic layout-proof module still named
+  `module {{PROJECT}}.ABI.Layout`; it cannot compile as-is and is the
+  last *unresolved* `{{...}}` placeholder in the monorepo
+  (`satellite-template`'s Foreign.idr also mentions `{{project}}`, but
+  only in a TODO comment telling template users to substitute it —
+  that one is by design).
+
+*Tier 3 — self-describing customization stubs* (each carries a NOTE
+saying it awaits per-component content): `Foreign.idr` in `vext`,
+`vext-email-gateway`, `vexometer-satellites`, `lazy-eliminator`, and
+`satellite-template`.
+
+No escape hatches: zero `believe_me` / `assert_total` / `postulate`
+across all ABI modules.
+
+[#what-needs-proving]
 === What Needs Proving
 
-==== Lazy Eliminator Analysis (lazy-eliminator/)
+==== Ada ISA core (vexometer/)
 
-* `+analyzer.rs+`, `+detection.rs+`, `+patterns.rs+` — static analysis
-for lazy evaluation elimination
-* Prove: analysis correctly identifies lazy evaluation patterns (no
-false negatives)
-* Prove: elimination suggestions preserve program semantics
+* SPARK-mode the metrics and aggregation packages and discharge the
+  existing 4 Pre/Post contracts statically (`gnatprove`). Motivation is
+  not hypothetical: the 2026-09-01 campaign found `Aggregate_Profile`
+  leaving five `Model_Profile` fields unassigned — undefined memory
+  reaching every report, surfacing as a nondeterministic E2E verdict.
+  SPARK flow analysis rejects exactly this defect class at compile time.
 
-==== Trace System (lazy-eliminator/src/trace.rs)
+==== Efficacy evaluator (vexometer-efficacy/)
 
-* Execution tracing — prove traces are faithful to execution order
+* D_ISA arithmetic, frontier monotonicity, and totality of the
+  acceptance rule (verdict function covers all input regions; the
+  protocol's rounding rules round-trip). The 15 protocol-fixture tests
+  execute examples; they do not establish the properties. Property
+  tests are the pragmatic first step, Idris2/Lean model second.
+* Add `#![forbid(unsafe_code)]` here and in `vext` to turn the current
+  no-unsafe observation into a compiler-enforced invariant.
 
-==== Fuzz Target (lazy-eliminator/fuzz/)
+==== ABI layout agreement (vexometer/src/abi/ ↔ ffi/zig ↔ Ada)
 
-* Fuzzing exists but formal proofs of analysis correctness would be
-stronger
+* Prove (or at minimum, CI-check) that the Idris2 layout statements,
+  the Zig `extern struct` definitions, and the Ada C-convention records
+  agree on size/alignment/field order. Today agreement is by
+  discipline, not by check.
 
-==== Vext Tools Obj.magic
+==== Lazy Eliminator analysis (lazy-eliminator/)
 
-* Minor — CLI argument parsing and notification serialization
-* Low priority but should use typed bindings
+* `analyzer.rs`, `detection.rs`, `patterns.rs` — prove the analysis
+  identifies lazy-evaluation patterns without false negatives, and that
+  elimination suggestions preserve program semantics. Fuzzing exists
+  (`fuzz/`); formal statements would be stronger.
 
-=== Recommended Prover
+==== Vext hash chains (vext/)
 
-* *Idris2* for analysis correctness specification
-* *Lean4* alternative for the semantic preservation proofs
+* Mechanize the two unproven header claims of `Types.idr`
+  (attestation validity, constructive verification) and resolve the
+  Tier-2 `Layout.idr` placeholder or delete the module.
 
-=== Priority
+=== Recommended Provers
 
-*LOW* — Developer tooling. Analysis correctness is desirable but false
-positives/negatives are inconveniences, not safety issues. The
-`+Obj.magic+` uses are minimal and non-critical.
+* *Idris2* for ABI and analysis-correctness specifications (already the
+  spec language in-tree).
+* *SPARK/gnatprove* for the Ada core — contracts already exist as
+  Ada 2022 aspects; SPARK is the natural discharge route.
 
-=== Template ABI Cleanup (2026-03-29)
+=== Priority
 
-Template ABI removed – was creating false impression of formal
-verification. The removed files (Types.idr, Layout.idr, Foreign.idr)
-contained only RSR template scaffolding with unresolved
-\{\{PROJECT}}/\{\{AUTHOR}} placeholders and no domain-specific proofs.
+*MEDIUM* for the efficacy evaluator and the Ada core: the evaluator
+emits accept/reject verdicts (arithmetic errors change decisions), and
+the Ada core has already shipped one undefined-memory defect that
+contracts+flow analysis would have caught. *LOW* for the rest —
+developer tooling where wrong answers are inconveniences.
+
+[#corrections]
+=== Corrections to the 2026-03-29 revision
+
+* It claimed `Obj.magic` sites in `vext/vext-tools` — that code left
+  main with the ReScript eradication.
+* It claimed Types.idr/Layout.idr/Foreign.idr were "removed" as
+  template scaffolding — they exist, and the `vexometer/` and
+  `vext/Types.idr` modules now carry real domain content (only
+  `vext/Layout.idr` still matches the old description).
+* It omitted the Ada core entirely.
+
+[#verification]
+=== Verification commands (run 2026-09-01, main @ e768bf1)
+
+[listing]
+----
+find . -name '*.res' | wc -l                             # 0
+grep -rn 'Obj.magic' --include='*.res' --include='*.rs' . # no matches
+find . -name '*.idr' | sort                              # the 10 files above
+grep -rn 'SPARK_Mode\|Contract_Cases' vexometer/src      # no matches
+grep -c 'with Pre\|with Post\|Pre =>\|Post =>' vexometer/src/vexometer-metrics.ads  # 4
+grep -l 'forbid(unsafe_code)' vext/src/*.rs lazy-eliminator/src/*.rs vexometer-efficacy/src/*.rs
+                                                         # lazy-eliminator/src/lib.rs only
+grep -n 'believe_me\|assert_total\|postulate' */src/abi/*.idr  # no matches
+grep -rln '{{' --include='*.idr' .                       # vext/src/abi/Layout.idr
+                                                         # + satellite-template Foreign.idr
+                                                         #   (TODO comment, by design)
+----
@@ -1,3 +1,5 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Last updated: 2026-09-01
 == VEX Toolkit (vexometer) — Project Topology
 
 ____
@@ -47,12 +49,19 @@ ____
 
 === Completion Dashboard
 
+NOTE: Percentages are maintainer *estimates* — no command measures them
+(D3, `docs/sitrep-2026-09-01.adoc`). Measured figures (test counts,
+assertion sites) live in `.machine_readable/6a2/STATE.a2ml`, each with
+the command that produced it. `STATE.a2ml`'s `completion-percentage`
+mirrors the OVERALL row below; update this dashboard first.
+
 ....
 COMPONENT                          STATUS              NOTES
 ─────────────────────────────────  ──────────────────  ─────────────────────────────────
 ISA & INTERVENTION
   ISA (vexometer analyser)          ████████░░  80%    Core metrics, JSON loaders, and CLI/report wiring implemented
   ISA Satellites                    █████░░░░░  45%    Protocol/docs exist; most satellites still planned
+  Efficacy Evaluator                ██████░░░░  60%    Evaluator/validator + 15 fixture tests shipped (PR #70); D1 rulings pending (#69); no satellite runs yet
   Lazy Eliminator                   ████████░░  75%    Core analyzer tested; polish/integration pending
   Satellite Template                █████████░  90%    Template structure stable by design
 
@@ -67,7 +76,7 @@ REPO INFRASTRUCTURE
   Consolidation (2026)              ██████████ 100%    6 repos successfully merged
 
 ─────────────────────────────────────────────────────────────────────────────
-OVERALL:                            ███████░░░  ~70%   Core operational; ecosystem integration still maturing
+OVERALL:                            ███████░░░  70%    Estimate; core operational, ecosystem integration still maturing
 ....
 
 === Key Dependencies