From d75eed1728645f7255b5a41380a73405303641c0 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 20 Sep 2026 14:26:00 +0000 Subject: [PATCH] docs(phase4): taxonomy audit, Idris2-only proofs, honest N/A benches Catalogue 18 test categories against proven-tests-and-benches without vacuous import. Continue Idris2 (not Lean4). Build-time benches only. Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- Justfile | 1 + benches/README.adoc | 5 +- docs/reports/PHASE-4-VERIFICATION.adoc | 39 +++++++++ docs/reports/proven-tests-contribution.adoc | 10 +++ docs/status/ROADMAP.adoc | 3 + docs/status/TEST-NEEDS.adoc | 94 +++++++++++++-------- tests/taxonomy_spec.sh | 20 +++++ verification/proofs/idris2/TaxonomyDecl.idr | 50 +++++++++++ 8 files changed, 183 insertions(+), 39 deletions(-) create mode 100644 docs/reports/PHASE-4-VERIFICATION.adoc create mode 100644 docs/reports/proven-tests-contribution.adoc create mode 100755 tests/taxonomy_spec.sh create mode 100644 verification/proofs/idris2/TaxonomyDecl.idr diff --git a/Justfile b/Justfile index 7735649..dc0d3d2 100644 --- a/Justfile +++ b/Justfile @@ -198,6 +198,7 @@ spec-tests: bash tests/manifest_spec.sh bash tests/backend_spec.sh bash tests/projection_spec.sh + bash tests/taxonomy_spec.sh bash scripts/emit-manifest.sh >/dev/null # Run the full merge-requirement test suite diff --git a/benches/README.adoc b/benches/README.adoc index 4a6f1b2..21d7543 100644 --- a/benches/README.adoc +++ b/benches/README.adoc @@ -2,5 +2,6 @@ // Copyright (c) Jonathan D.A. Jewell = benches -`template_bench.sh` — Zig build/test + workflow validation timings. -Not a Core-language benchmark (no checker yet). +`template_bench.sh` — Zig build/test + workflow validation timings +(**build** category, not latency/throughput). No Core hot path. FFI-overhead +and Six Sigma baselines are Phase 8. diff --git a/docs/reports/PHASE-4-VERIFICATION.adoc b/docs/reports/PHASE-4-VERIFICATION.adoc new file mode 100644 index 0000000..28a6b97 --- /dev/null +++ b/docs/reports/PHASE-4-VERIFICATION.adoc @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Phase 4 — Tests, benchmarks, proofs +:revdate: 2026-09-20 + +== 4.1 Tests + +First source: https://github.com/hyperpolymath/proven-tests-and-benches +(cloned 2026-09-20). That suite is **Idris2 AffineScript / type-safe +subcategories**, not panoply Core. Adapting it wholesale would be a +vacuous import. + +Applicable draw: taxonomy enumerations + “honest N/A > vacuous pass”. +Panoply’s live tests stay Zig FFI units + ABI↔FFI P2P + spec gates. + +Did **not** open a PR on proven-tests-and-benches: nothing here is a +generic suite member yet (refused-manifest is panoply-charter specific). +Contribution sketch: `docs/reports/proven-tests-contribution.adoc`. + +== 4.2 Benchmarks + +`benches/template_bench.sh` = **build-time** (Zig compile, zig test, +workflow validation). Not latency/throughput of Core. + +FFI-overhead benches need a real hot path. Marked N/A until then. +Idris2 `benchmarks/Benchmark.idr` in proven-tests is a framework, not +panoply numbers — not vendored. + +== 4.3 Proofs + +Preference (protocol): continue **existing** assistant = **Idris2** +(ABI-1..5 + Types.idr). Lean4 default does **not** apply. + +Checked: `just proof-check-idris2` SKIP if no `idris2`. Dangerous-pattern +scan on `verification/proofs/**/*.idr`. + +Do now: ABI-1 (`SafePtr`, `checkPtrZeroIsNothing`). +Phase 8: ABI-2..5 typecheck in CI with idris2; Core preservation (TP) +after a checker exists. No Lean/Agda/Coq/TLA trees. diff --git a/docs/reports/proven-tests-contribution.adoc b/docs/reports/proven-tests-contribution.adoc new file mode 100644 index 0000000..a3f2571 --- /dev/null +++ b/docs/reports/proven-tests-contribution.adoc @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Contribution sketch → proven-tests-and-benches +:revdate: 2026-09-20 + +Not submitted. When Core exists, a TypeSafe/Dependent fixture for +“refused evidence ⇒ empty earned envelopes” belongs in +`hyperpolymath/proven-tests-and-benches` as a shared language-discipline +test, using `templates/test-template.idr`. Until then a PR would be a +stub that looks like coverage. diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index e9e639a..b1b1120 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -39,3 +39,6 @@ Design phase. Charter + RSR spine + Core/Evidence *specs*. No Core checker. * [ ] Cleave: map ABI/FFI/API dial once a SNIF/host exists * [ ] Spline: only with a live groove session * [ ] Gossamer / burble: only if a GUI or voice projection appears +* [ ] Proofs: ABI-2..5 typecheck in CI with idris2; Core preservation after a checker +* [ ] Tests: PBT/FUZ/TSF when Core parser exists; no fake harnesses +* [ ] Benches: FFI-overhead once there is a hot path; Six Sigma baselines then diff --git a/docs/status/TEST-NEEDS.adoc b/docs/status/TEST-NEEDS.adoc index 6abc432..1fcf393 100644 --- a/docs/status/TEST-NEEDS.adoc +++ b/docs/status/TEST-NEEDS.adoc @@ -1,57 +1,77 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = TEST-NEEDS: panoply +:revdate: 2026-09-20 == Current State -Panoply is at the design phase (see `.machine_readable/6a2/STATE.deed`): -the Core, Evidence, and Manifest artefacts described by the charter are not -yet implemented. Test infrastructure at this stage necessarily covers the -Idris2 ABI / Zig FFI scaffold, not language semantics. +Design phase. Tests cover the Idris2 ABI / Zig FFI scaffold and charter +specs, not Core semantics. First draw: +https://github.com/hyperpolymath/proven-tests-and-benches — suite is +AffineScript/type-safe, not imported wholesale (would be vacuous). + +== Taxonomy (18 categories) + +Honest N/A is required. Vacuous pass is forbidden. + +[cols="1,1,3", options="header"] +|=== +| Cat | Status | Evidence / justification + +| UT | Present | Zig unit tests in `src/interface/ffi/src/main.zig` +| P2P | Present | `tests/p2p.sh` — ABI `Result` ↔ Zig `Result` seam +| E2E | Present | `tests/e2e.sh` — zig (required); idris2 SKIP if absent +| BLD | Present | `zig build`; idris2 `--build` when present +| EXE | N/A | No VM / interpreter / REPL +| REF | Present | `just doctor` (weak; not a runtime) +| LCY | Present | `tests/lifecycle.sh` +| SMK | Present | `just test-smoke` (`zig build`) +| PBT | N/A | No Core parser to generate against +| MUT | N/A | CRG X; mutation of Zig FFI is Phase 8 +| FUZ | N/A | No untrusted input surface; `verification/fuzzing/` is a README only — not a fake harness +| CTR | N/A | No `must` CLI in CI; Mustfile is a pointer +| REG | N/A | No fixed production bugs yet +| CHS | N/A | Not a distributed system +| CMP | N/A | No versioned wire/persist format +| PRF | Present | `verification/proofs/idris2/`; `just proof-check-idris2` SKIP without idris2 +| TSF | N/A | No Idris2 `failing` blocks for Core yet +| CDF | Present | P2P coupling test is the drift check for Result tags +|=== + +== Aspects (14) + +SAF (dangerous-pattern scan) and SEC (SPDX) are in `tests/aspect_tests.sh`. +Others N/A or covered only as docs until there is a product runtime: +DEP USA IOP PER FUN VER ACC MNT PRI OBS RPR PRT — see +`docs/reports/PHASE-4-VERIFICATION.adoc`. + +== Inventory [cols="2,1,4", options="header"] |=== | Category | Count | Details | *Source modules* | 3 | Idris2 ABI (`src/interface/Abi/{Types,Layout,Foreign}.idr`) -| *FFI modules* | 1 | `src/interface/ffi/src/main.zig` (11 exported functions) -| *Unit tests* | 3 | Inline `test` blocks in `main.zig` (lifecycle, error handling, version) -| *Integration tests* | 15 | `src/interface/ffi/test/integration_test.zig` — exercises every exported FFI function (lifecycle, process, process_array incl. null-buffer, strings, version/build_info, error handling, callbacks) -| *E2E tests* | 1 | `tests/e2e.sh` — preflight (idris2/zig on PATH) + `idris2 --build src/interface/abi.ipkg` + `zig build test` -| *Aspect tests* | 1 | `tests/aspect_tests.sh` — SPDX headers (ignores `.zig-cache`) + dangerous-pattern scan on *code* (prohibition comments / `.adoc` are not hits) -| *Lifecycle tests* | 1 | `tests/lifecycle.sh` — zig build/test/clean; skips Idris2 if absent -| *P2P tests* | 1 | `tests/p2p.sh` — honest SKIP until a peer protocol exists; FAIL if P2P-shaped source appears untested -| *Core spec tests* | 1 | `tests/core_spec.sh` — guards issue #5 specification artefacts -| *Evidence spec tests* | 1 | `tests/evidence_spec.sh` — kinds + refused example (#6) -| *Manifest spec tests* | 1 | `tests/manifest_spec.sh` — schema + refused example (#7, no emitter) -| *Workflow tests* | 1 | `tests/workflows/validate_workflows_test.sh` -| *Benchmarks* | 3 | `benches/template_bench.sh` (Zig build, Zig tests, workflow validation) -| *Fuzz tests* | 0 | `verification/fuzzing/` scaffold present; no harness wired yet +| *FFI modules* | 1 | `src/interface/ffi/src/main.zig` +| *Unit tests* | 3 | Inline `test` in `main.zig` +| *Integration tests* | 15 | `src/interface/ffi/test/integration_test.zig` +| *Spec gates* | 6 | core, evidence, manifest, backend, projection, taxonomy +| *Benchmarks* | 3 | `benches/template_bench.sh` — **build** timings only |=== -== Verified 2026-07-27 - -* `zig fmt --check .` — exit 0 -* `idris2 --build src/interface/abi.ipkg` — exit 0 (builds `Abi.Types`, `Abi.Layout`, `Abi.Foreign`) -* `cd src/interface/ffi && zig build` — exit 0 -* `zig build test --summary all` — exit 0, 20/20 tests pass (3 unit + 17 integration checks across 15 `test` blocks) -* `bash tests/e2e.sh` — PASS=2 FAIL=0 -* `bash tests/aspect_tests.sh` — PASS=2 FAIL=1 (the known Admitted/sorry doc-prose false positive above) - -== What was removed +== Benchmarks -The template-distribution machinery that does not apply to an instantiated -downstream repository has been removed: +Build-time only. No Core latency/throughput/FFI-overhead baseline. +Six Sigma classification does not apply until a hot path exists. -* `scripts/validate-template.sh` (8-phase template-distribution validator) -* `tests/e2e/template_instantiation_test.sh` (clone-and-substitute E2E test) +== Proofs -`benches/template_bench.sh` had benchmark sections gated on both scripts; -those sections were removed and the remaining benchmarks (Zig build, Zig -test, workflow validation) were kept and renumbered. +Continue **Idris2** (partial ABI work in-tree). Not Lean4. +ABI-1 constructive. ABI-2..5 + Core TP → Phase 8. == Next Steps -* [ ] Wire a fuzz harness once the Core parser/checker exists (`verification/fuzzing/`) -* [ ] Add readiness/CRG-grade tests once there is a component to grade beyond the ABI scaffold -* [ ] Expand integration tests as the Core/Evidence/Manifest artefacts land +* [ ] Fuzz harness once a Core parser exists +* [ ] Property tests once Core has generators +* [ ] Idris2 `failing` blocks (TSF) for Core judgements +* [ ] Contribute refused-envelope fixture to proven-tests-and-benches when it is a real test diff --git a/tests/taxonomy_spec.sh b/tests/taxonomy_spec.sh new file mode 100755 index 0000000..144e3b8 --- /dev/null +++ b/tests/taxonomy_spec.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +set -euo pipefail +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$ROOT" +FAIL=0 +fail() { echo "FAIL: $*"; FAIL=$((FAIL+1)); } +pass() { echo "PASS: $*"; } + +[[ -f docs/status/TEST-NEEDS.adoc ]] && pass "TEST-NEEDS" || fail "TEST-NEEDS" +[[ -f docs/reports/PHASE-4-VERIFICATION.adoc ]] && pass "phase4 report" || fail "phase4" +[[ -f verification/proofs/idris2/TaxonomyDecl.idr ]] && pass "TaxonomyDecl" || fail "TaxonomyDecl" +grep -q 'eighteenCategories' verification/proofs/idris2/TaxonomyDecl.idr && pass "count pin" || fail "count" +for c in UT P2P E2E BLD EXE REF LCY SMK PBT MUT FUZ CTR REG CHS CMP PRF TSF CDF; do + grep -q "$c" docs/status/TEST-NEEDS.adoc && pass "needs $c" || fail "needs $c" +done +[[ -f tests/p2p.sh ]] && pass "CDF/P2P artefact" || fail "p2p" +echo "FAIL=$FAIL" +exit "$FAIL" diff --git a/verification/proofs/idris2/TaxonomyDecl.idr b/verification/proofs/idris2/TaxonomyDecl.idr new file mode 100644 index 0000000..17232bf --- /dev/null +++ b/verification/proofs/idris2/TaxonomyDecl.idr @@ -0,0 +1,50 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- Local taxonomy declaration. Does not vendor proven-tests-and-benches. +-- Category 18 (coupling) is ABI↔FFI Result tags (tests/p2p.sh). + +module TaxonomyDecl + +%default total + +public export +data Applicability = Present | HonestNA + +public export +record Cat where + constructor MkCat + code : String + status : Applicability + +||| Eighteen taxonomy categories. Present = an artefact exists in-tree. +public export +categories : List Cat +categories = + [ MkCat "UT" Present + , MkCat "P2P" Present + , MkCat "E2E" Present + , MkCat "BLD" Present + , MkCat "EXE" HonestNA + , MkCat "REF" Present + , MkCat "LCY" Present + , MkCat "SMK" Present + , MkCat "PBT" HonestNA + , MkCat "MUT" HonestNA + , MkCat "FUZ" HonestNA + , MkCat "CTR" HonestNA + , MkCat "REG" HonestNA + , MkCat "CHS" HonestNA + , MkCat "CMP" HonestNA + , MkCat "PRF" Present + , MkCat "TSF" HonestNA + , MkCat "CDF" Present + ] + +public export +categoryCount : Nat +categoryCount = length categories + +export +eighteenCategories : TaxonomyDecl.categoryCount = 18 +eighteenCategories = Refl