diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index d03e55e..964986a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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. diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index dfcab62..43abe09 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -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 <>). Debt item D2 of `docs/sitrep-2026-09-01.adoc`. +Every claim here carries the command that measured it (<>). -* *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 + <>). +* *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) +---- diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index 1388033..2df6e37 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -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