diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index ce17bb6..9b556ad 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -46,12 +46,24 @@ jobs: uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Set up Node.js - uses: actions/setup-node@v6 + uses: actions/setup-node@2028fbc5c25fe9cf00d9f06a71cc4710d4507903 # v6.0.0 with: - node-version: '22' + node-version: '25' + + - name: Install npm deps (rescript build prerequisite) + run: npm install --no-audit --no-fund --silent + + - name: Build ReScript parser + run: node_modules/.bin/rescript build - name: Run smoke test - run: node tests/e2e/e2e-smoke.mjs + run: node tests/smoke/e2e-smoke.mjs + + - name: Run aspect test (claim envelope) + run: node tests/aspect/claim-envelope.mjs + + - name: Run parser benchmark (smoke; full run is local) + run: BENCH_ITERS=20 node benchmarks/parser-bench.mjs # -------------------------------------------------------------------------- # Job 3: Full Idris2 + Zig build then E2E @@ -65,12 +77,15 @@ jobs: uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 # ---- Idris2 ---- + # 0.8.0 is the version the src/abi/ proofs are written against + # (Proofs.idr:629 "verified with Idris2 0.8.0"; Layout.idr / Types.idr + # carry 0.8-specific workarounds for reduction + interface resolution). + # Older versions will fail the standalone build. - name: Install Idris2 run: | sudo apt-get update -qq sudo apt-get install -y libgmp-dev - # Install Idris2 from binary release - IDRIS2_VERSION="0.7.0" + IDRIS2_VERSION="0.8.0" curl -fsSL \ "https://github.com/idris-lang/Idris2/releases/download/v${IDRIS2_VERSION}/idris2-${IDRIS2_VERSION}-ubuntu-20.04.tar.gz" \ -o /tmp/idris2.tar.gz || true @@ -79,9 +94,13 @@ jobs: fi # ---- Zig ---- + # 0.15.1 is the version ffi/zig/build.zig is written against (header + # comment "Updated for Zig 0.15+ API (addLibrary / createModule + # pattern)"). 0.12 lacks `b.addLibrary` and the `.root_module` field + # and will not parse the build script. - name: Install Zig run: | - ZIG_VERSION="0.12.0" + ZIG_VERSION="0.15.1" curl -fsSL \ "https://ziglang.org/download/${ZIG_VERSION}/zig-linux-x86_64-${ZIG_VERSION}.tar.xz" \ -o /tmp/zig.tar.xz @@ -90,9 +109,9 @@ jobs: # ---- Node (for smoke test within E2E script) ---- - name: Set up Node.js - uses: actions/setup-node@v6 + uses: actions/setup-node@2028fbc5c25fe9cf00d9f06a71cc4710d4507903 # v6.0.0 with: - node-version: '22' + node-version: '25' # ---- Full E2E ---- - name: Run full E2E (with build checks) diff --git a/.gitignore b/.gitignore index 446ffef..9082dce 100644 --- a/.gitignore +++ b/.gitignore @@ -52,6 +52,8 @@ erl_crash.dump !tests/e2e/*.mjs !tests/contracts/*.mjs !tests/levels/*.mjs +!tests/aspect/*.mjs +!benchmarks/*.mjs *.cmi *.cmj *.cmt diff --git a/Justfile b/Justfile index d77eb1a..7c6a944 100644 --- a/Justfile +++ b/Justfile @@ -146,7 +146,8 @@ test-contract: test-e2e: @echo "Running end-to-end tests..." rescript build - node tests/e2e/e2e-smoke.mjs + node tests/smoke/e2e-smoke.mjs + node tests/e2e/e2e-driver.mjs # Aspect tests for cross-surface claim coherence test-aspect: diff --git a/LEVEL-STATUS.md b/LEVEL-STATUS.md index c081f16..d789ebe 100644 --- a/LEVEL-STATUS.md +++ b/LEVEL-STATUS.md @@ -75,10 +75,14 @@ time; they are not needed at runtime. ## What "draft" means -Levels 11-12 currently have draft Idris2 files and example syntax, but they are -not part of `typed-wasm.ipkg` and, as of 2026-03-30, both standalone checks -fail. Zero dangerous patterns is not enough here: a file that does not -type-check is not a claimable proof artefact. Wiring these levels into the +Levels 11-12 are draft for surface semantics, not for ipkg membership. +As of 2026-04-18 (commit A1) both `Tropical.idr` and `Epistemic.idr` are +in `typed-wasm.ipkg` and build clean under Idris2 0.8.0 — see the +2026-05-18 reconciliation in `PROOF-NEEDS.md`. The "draft" label +applies to the level semantics themselves (Tropical cost-tracking and +Epistemic freshness propagation under concurrent writes remain +research-grade): theorems live, but the surface language and Zig FFI +do not yet expose them. Wiring these levels through the rest of the toolchain remains future work. ## Proof inventory diff --git a/README.adoc b/README.adoc index b6ae063..9764d3e 100644 --- a/README.adoc +++ b/README.adoc @@ -79,9 +79,10 @@ WASM instructions with zero overhead. | 10 | Linearity | Linear resource usage |=== -L11-L12 research files exist in the repository, but they are not part of the -default checked Idris2 package and are not currently claimed as integrated or -machine-checked proof surface. +L11-L12 (Tropical, Epistemic) are in `typed-wasm.ipkg` and build clean under +Idris2 0.8.0 as of 2026-04-18 (see `PROOF-NEEDS.md` reconciliation). Their +surface semantics remain research-grade — the parser, Zig FFI and downstream +tooling do not yet expose L11/L12 features. == The Killer Feature: Multi-Module Type Safety diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 2f53ca2..ea30b7e 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -26,7 +26,10 @@ Key capabilities delivered: Known audit constraints: -* L11-L12 draft files are not part of `typed-wasm.ipkg` and currently fail standalone type-checking +* L11 (Tropical) and L12 (Epistemic) are in `typed-wasm.ipkg` since 2026-04-18 + (commit A1) and build clean under Idris2 0.8.0 (PROOF-NEEDS.md reconciliation + 2026-05-18). Treat them as research/draft for surface semantics, not for + ipkg membership. * Release/build/container metadata still contains template residue * Benchmark and venue-facing paper claims require evidence cleanup before submission diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md index 485ac40..1291de5 100644 --- a/TEST-NEEDS.md +++ b/TEST-NEEDS.md @@ -6,41 +6,63 @@ | Category | Count | Details | |----------|-------|---------| -| **Source modules** | 21 | 11 Idris2 ABI (Region, TypedAccess, Levels, Pointer, Effects, Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic), 3 ReScript parser (Ast, Parser, Lexer), 3 Idris2 interface ABI, 2 Zig FFI + cache | -| **Unit tests** | 1 file | ParserTests.res (~82 assertions) | -| **Integration tests** | 0 | None | -| **E2E tests** | 1 | e2e-smoke.mjs (~43 assertions) | -| **Property-based tests** | 1 | property_test.mjs (10 properties, ~40+ assertions) | -| **Benchmarks** | 0 | None | -| **ECHIDNA harness** | 1 | echidna-harness.mjs (7 assertions) | +| **Source modules** | 21 | 11 Idris2 ABI (Region, TypedAccess, Levels, Pointer, Effects, Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic), 4 ReScript parser (Ast, Parser, Lexer, Checker), 3 Idris2 interface ABI, 2 Zig FFI + cache, 1 Rust verifier crate (typed-wasm-verify, ~1.6k LOC + 53 tests) | +| **Unit tests** | 2 files | ParserTests.res (88 assertions), crates/typed-wasm-verify (43 unit + 10 cross-compat) | +| **Integration tests** | 1 | tests/contracts/airborne-step-state-contract.mjs (14 assertions) | +| **E2E tests** | 2 | tests/smoke/e2e-smoke.mjs (40 assertions), tests/e2e/e2e-driver.mjs (corpus driver) | +| **Per-level tests** | 10 | tests/levels/L1.mjs .. L10.mjs (56 assertions total) | +| **Aspect tests** | 1 | tests/aspect/claim-envelope.mjs (49 assertions — added 2026-05 to catch cross-doc claim drift after deep audit found 5 such drifts) | +| **Property-based tests** | 0 | tests/property/property_test.mjs claimed DONE 2026-04-04 but file is absent — stale entry being scrubbed | +| **Benchmarks** | 1 | benchmarks/parser-bench.mjs (per-example wallclock; median/p95/min/throughput; JSON summary on stderr; added 2026-05) | +| **ECHIDNA harness** | 1 | tests/echidna/echidna-harness.mjs (659 LOC, 124 local assertions, remote prover-wars submission) | ## What's Missing ### P2P Tests -- [x] **DONE 2026-04-04**: Property-based tests added (`tests/property/property_test.mjs`, 10 properties, ~40+ assertions) +- [ ] **REVOKED 2026-05**: prior "DONE 2026-04-04 property tests" entry was + false — `tests/property/property_test.mjs` was never committed. + Aspect test now catches this drift class automatically. - [ ] No tests for Idris2 ABI type checking with Zig FFI - [ ] No tests for ReScript parser feeding into Idris2 type checker ### E2E Tests -- [ ] e2e-smoke exists but only 43 assertions for a type system with 10 safety levels -- [ ] No WASM module compilation and execution test -- [ ] No multi-module linking test (MultiModule.idr untested) +- [x] **DONE 2026-05**: `tests/e2e/e2e-driver.mjs` exercises every + example through parse + check with skip/expect-clean/expect-diagnostic + pragmas. Smoke test still narrow (40 assertions) but now augmented + by the per-level suite (56 more) and the aspect test (49 more). +- [ ] No WASM module compilation and execution test (blocked on codegen) +- [ ] No multi-module linking test (MultiModule.idr untested at runtime) ### Aspect Tests -- [ ] **Security**: No memory safety violation detection tests (this IS the product's purpose) -- [ ] **Performance**: No benchmarks for type checking overhead vs raw WASM +- [x] **DONE 2026-05**: `tests/aspect/claim-envelope.mjs` — 49 checks that + cross-document claims (README/ROADMAP/LEVEL-STATUS/EXPLAINME) stay + consistent with actual artefacts (ipkg, Rust constants, CI pins, + example corpus, RSR surface). Built in response to a deep audit + finding five drifts the test now catches. +- [ ] **Security**: No memory safety violation detection tests (this IS the + product's purpose) +- [ ] **Performance**: see Benchmarks below - [ ] **Concurrency**: No concurrent WASM module compilation tests -- [ ] **Error handling**: No tests for invalid type annotations, malformed WASM +- [ ] **Error handling**: 10/10 per-level test suites (`tests/levels/L*.mjs`) + include negative cases — partial coverage ### Build & Execution - [ ] 11 Idris2 modules with 0 Idris2-level tests -- are proofs checked? + (PROOF-NEEDS.md 2026-05-18 reconciliation: ipkg builds clean, but + no Idris2 *test* layer beyond compile-time totality / type-checking) - [ ] Zig FFI integration_test.zig likely a template placeholder -### Benchmarks Needed (CRITICAL) -- [ ] Type checking overhead per WASM instruction -- [ ] Memory region tracking performance -- [ ] Lifetime analysis scaling with module size +### Benchmarks +- [x] **DONE 2026-05**: `benchmarks/parser-bench.mjs` — per-example parse + + check wallclock with median / p95 / min / throughput and JSON summary + for trend tracking. Only the parser is end-to-end today, so that's + where benchmark evidence has to start. +- [ ] Type-checking overhead per WASM instruction (blocked on codegen + + Zig FFI runtime path) +- [ ] Memory region tracking performance (blocked on codegen) +- [ ] Lifetime analysis scaling with module size (blocked on codegen) - [ ] Comparison: typed-wasm overhead vs raw WASM execution + (blocked on codegen) ### Self-Tests - [ ] No type system self-consistency check diff --git a/benchmarks/parser-bench.mjs b/benchmarks/parser-bench.mjs new file mode 100644 index 0000000..ab3220b --- /dev/null +++ b/benchmarks/parser-bench.mjs @@ -0,0 +1,224 @@ +#!/usr/bin/env node +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +// +// Parser benchmark. +// +// The only end-to-end pipeline that ships today is parse + check on .twasm +// source — Idris2 proofs are static, Zig FFI runs out-of-process, and the +// post-codegen Rust verifier consumes wasm, not .twasm. So the parser is +// where benchmark evidence has to live until L1-L6 codegen exists. +// +// Per-example wallclock measurements with the warm-up + repeat-N pattern +// the maintenance standard expects (`.machine_readable/policies/ +// MAINTENANCE-AXES.a2ml` axis-3 effects-evidence). Reports median + p95 + +// min + throughput (KB/s of source parsed-and-checked) per example, plus +// an aggregate roll-up. Skips examples that the parser rejects with a +// reason (L11/L12 grammar not in the v1.5 parser). +// +// Output: +// - Human-readable table on stdout +// - JSON summary on stderr (machine-readable for trend tracking) +// +// Invocation: +// node benchmarks/parser-bench.mjs # default: 200 iters +// BENCH_ITERS=1000 node benchmarks/parser-bench.mjs +// BENCH_FORMAT=json node benchmarks/parser-bench.mjs > metrics.json + +import { readFileSync, readdirSync } from "node:fs"; +import { resolve, dirname, basename } from "node:path"; +import { fileURLToPath } from "node:url"; +import { parseModule } from "../src/parser/Parser.mjs"; +import { checkModule } from "../src/parser/Checker.mjs"; + +const __dirname = dirname(fileURLToPath(import.meta.url)); +const ROOT = resolve(__dirname, ".."); +const EXAMPLES = resolve(ROOT, "examples"); + +const ITERS = Number(process.env.BENCH_ITERS ?? 200); +const WARMUP = Math.max(10, Math.floor(ITERS / 10)); +const FORMAT = process.env.BENCH_FORMAT ?? "human"; // human | json + +// ───────────────────────────────────────────────────────────────────────── +// Stats helpers +// ───────────────────────────────────────────────────────────────────────── + +function quantile(sorted, q) { + if (sorted.length === 0) return NaN; + const idx = Math.min(sorted.length - 1, Math.floor(q * sorted.length)); + return sorted[idx]; +} + +function summarise(samplesMs, bytes) { + const sorted = [...samplesMs].sort((a, b) => a - b); + const median = quantile(sorted, 0.5); + const p95 = quantile(sorted, 0.95); + const min = sorted[0]; + const max = sorted[sorted.length - 1]; + const mean = samplesMs.reduce((a, b) => a + b, 0) / samplesMs.length; + // Throughput from the median: kilobytes parsed-and-checked per second. + const throughput_kBs = median > 0 ? (bytes / 1024) / (median / 1000) : Infinity; + return { median_ms: median, p95_ms: p95, min_ms: min, max_ms: max, mean_ms: mean, throughput_kBs }; +} + +function fmtMs(x) { + if (!Number.isFinite(x)) return "n/a"; + if (x < 1) return `${(x * 1000).toFixed(0)}µs`; + return `${x.toFixed(2)}ms`; +} +function fmtKBs(x) { + if (!Number.isFinite(x)) return "n/a"; + if (x >= 1024) return `${(x / 1024).toFixed(2)}MB/s`; + return `${x.toFixed(0)}kB/s`; +} + +// ───────────────────────────────────────────────────────────────────────── +// Pragma extraction (mirrors e2e-driver: skip examples whose grammar isn't +// in the v1.5 parser, so the benchmark doesn't measure "parser fails fast") +// ───────────────────────────────────────────────────────────────────────── + +function shouldSkip(source) { + for (const line of source.split("\n")) { + const m = line.match(/\/\/\s*E2E:\s*skip(?:\s+(.+))?/); + if (m) return m[1] ?? "(no reason)"; + } + return null; +} + +// ───────────────────────────────────────────────────────────────────────── +// One-shot timing +// ───────────────────────────────────────────────────────────────────────── + +function timeOne(source) { + const t0 = process.hrtime.bigint(); + const r = parseModule(source); + if (r.TAG !== "Ok") { + const t1 = process.hrtime.bigint(); + return { ok: false, ms: Number(t1 - t0) / 1e6, reason: `parse failed: ${r._0.message}` }; + } + checkModule(r._0); + const t1 = process.hrtime.bigint(); + return { ok: true, ms: Number(t1 - t0) / 1e6 }; +} + +// ───────────────────────────────────────────────────────────────────────── +// Per-example benchmark +// ───────────────────────────────────────────────────────────────────────── + +function benchExample(filename) { + const path = resolve(EXAMPLES, filename); + const source = readFileSync(path, "utf-8"); + const bytes = Buffer.byteLength(source, "utf8"); + + const skipReason = shouldSkip(source); + if (skipReason) { + return { filename, bytes, status: "skip", reason: skipReason }; + } + + // Warm-up: JIT primes V8's optimiser; throws away samples to avoid + // pulling the median toward cold-cache cost. + for (let i = 0; i < WARMUP; i++) { + const r = timeOne(source); + if (!r.ok) return { filename, bytes, status: "fail", reason: r.reason }; + } + + const samples = []; + for (let i = 0; i < ITERS; i++) { + const r = timeOne(source); + if (!r.ok) return { filename, bytes, status: "fail", reason: r.reason }; + samples.push(r.ms); + } + return { filename, bytes, status: "ok", ...summarise(samples, bytes) }; +} + +// ───────────────────────────────────────────────────────────────────────── +// Run +// ───────────────────────────────────────────────────────────────────────── + +const exampleFiles = readdirSync(EXAMPLES).filter((f) => f.endsWith(".twasm")).sort(); + +if (exampleFiles.length === 0) { + console.error("No examples/*.twasm found — nothing to benchmark"); + process.exit(1); +} + +if (FORMAT === "human") { + console.log(`typed-wasm parser benchmark`); + console.log(` examples : ${exampleFiles.length}`); + console.log(` iters : ${ITERS} (warmup ${WARMUP})`); + console.log(` node : ${process.version}`); + console.log(""); + console.log( + ` ${"example".padEnd(36)} ${"bytes".padStart(7)} ${"median".padStart(10)} ${"p95".padStart(10)} ${"min".padStart(10)} ${"throughput".padStart(11)}`, + ); + console.log(` ${"-".repeat(36)} ${"-".repeat(7)} ${"-".repeat(10)} ${"-".repeat(10)} ${"-".repeat(10)} ${"-".repeat(11)}`); +} + +const results = []; +let totalBytes = 0; +let totalMedianMs = 0; +let okCount = 0; +let failCount = 0; +let skipCount = 0; + +for (const f of exampleFiles) { + const r = benchExample(f); + results.push(r); + if (r.status === "ok") { + okCount++; + totalBytes += r.bytes; + totalMedianMs += r.median_ms; + if (FORMAT === "human") { + console.log( + ` ${basename(f).padEnd(36)} ${String(r.bytes).padStart(7)} ${fmtMs(r.median_ms).padStart(10)} ${fmtMs(r.p95_ms).padStart(10)} ${fmtMs(r.min_ms).padStart(10)} ${fmtKBs(r.throughput_kBs).padStart(11)}`, + ); + } + } else if (r.status === "skip") { + skipCount++; + if (FORMAT === "human") { + console.log(` ${basename(f).padEnd(36)} ${String(r.bytes).padStart(7)} ${"SKIP".padStart(10)} (${r.reason})`); + } + } else { + failCount++; + if (FORMAT === "human") { + console.log(` ${basename(f).padEnd(36)} ${String(r.bytes).padStart(7)} ${"FAIL".padStart(10)} (${r.reason})`); + } + } +} + +const aggregateThroughput = + totalMedianMs > 0 ? (totalBytes / 1024) / (totalMedianMs / 1000) : Infinity; + +if (FORMAT === "human") { + console.log(""); + console.log(` Aggregate: ${okCount} ok, ${skipCount} skip, ${failCount} fail`); + console.log(` Total bytes parsed-and-checked: ${totalBytes}`); + console.log(` Sum of medians: ${fmtMs(totalMedianMs)}`); + console.log(` Aggregate throughput: ${fmtKBs(aggregateThroughput)}`); +} + +// JSON summary always to stderr so `BENCH_FORMAT=json node parser-bench.mjs` +// can redirect stdout to a metrics file while still keeping stderr human. +const summary = { + schema: "typed-wasm/parser-bench/1", + iters: ITERS, + warmup: WARMUP, + node_version: process.version, + examples: results, + aggregate: { + ok: okCount, + skip: skipCount, + fail: failCount, + total_bytes: totalBytes, + sum_median_ms: totalMedianMs, + throughput_kBs: aggregateThroughput, + }, +}; + +if (FORMAT === "json") { + process.stdout.write(JSON.stringify(summary, null, 2) + "\n"); +} else { + process.stderr.write(JSON.stringify(summary) + "\n"); +} + +process.exit(failCount > 0 ? 1 : 0); diff --git a/crates/typed-wasm-verify/src/cross.rs b/crates/typed-wasm-verify/src/cross.rs index 3b4d60f..7396477 100644 --- a/crates/typed-wasm-verify/src/cross.rs +++ b/crates/typed-wasm-verify/src/cross.rs @@ -25,9 +25,7 @@ use wasmparser::{FunctionBody, Parser, Payload}; use crate::section::parse_ownership_section_payload; use crate::verify::{count_op_range, CallOf}; -use crate::{ - CrossError, FuncInterface, OwnershipKind, VerifyError, OWNERSHIP_SECTION_NAME, -}; +use crate::{CrossError, FuncInterface, OwnershipKind, VerifyError, OWNERSHIP_SECTION_NAME}; // ---------------------------------------------------------------------- // Interface extraction (callee side) @@ -164,8 +162,7 @@ pub fn verify_cross_module( for (import_slot, import_name) in &linear_imports { for (local_idx, body) in bodies.iter().enumerate() { let caller_func_idx = (local_idx as u32) + import_count; - let (min_calls, max_calls) = - count_op_range(body.clone(), &CallOf(*import_slot))?; + let (min_calls, max_calls) = count_op_range(body.clone(), &CallOf(*import_slot))?; if max_calls == 0 { // Function never calls this import: not a violation. @@ -525,14 +522,12 @@ mod tests { match verify_cross_module(&iface, &caller) { Err(VerifyError::Cross(errs)) => { assert_eq!(errs.len(), 2); - assert!(errs.iter().any(|e| matches!( - e, - CrossError::LinearImportDroppedOnSomePath { .. } - ))); - assert!(errs.iter().any(|e| matches!( - e, - CrossError::LinearImportCalledMultiple { count: 2, .. } - ))); + assert!(errs + .iter() + .any(|e| matches!(e, CrossError::LinearImportDroppedOnSomePath { .. }))); + assert!(errs + .iter() + .any(|e| matches!(e, CrossError::LinearImportCalledMultiple { count: 2, .. }))); } other => panic!("expected 2 errors, got {:?}", other), } diff --git a/crates/typed-wasm-verify/src/lib.rs b/crates/typed-wasm-verify/src/lib.rs index b25ce35..ae6359f 100644 --- a/crates/typed-wasm-verify/src/lib.rs +++ b/crates/typed-wasm-verify/src/lib.rs @@ -20,7 +20,9 @@ pub mod cross; pub mod section; pub mod verify; pub use cross::{extract_exports, verify_cross_module}; -pub use section::{build_ownership_section_payload, parse_ownership_section_payload, OwnershipEntry}; +pub use section::{ + build_ownership_section_payload, parse_ownership_section_payload, OwnershipEntry, +}; pub use verify::{count_uses_range, verify_function}; /// Ownership kinds matching the OCaml `Codegen.ownership_kind` enum. @@ -63,10 +65,18 @@ pub enum OwnershipError { LinearDroppedOnSomePath { func_idx: u32, param_idx: u32 }, #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param loaded {count} times on some path (exactly 1 required; possible duplication)")] - LinearUsedMultiple { func_idx: u32, param_idx: u32, count: u32 }, + LinearUsedMultiple { + func_idx: u32, + param_idx: u32, + count: u32, + }, #[error("Level 7 violation: function {func_idx}, param {param_idx} — ExclBorrow (mut) param aliased ({count} simultaneous references; at most 1 permitted)")] - ExclBorrowAliased { func_idx: u32, param_idx: u32, count: u32 }, + ExclBorrowAliased { + func_idx: u32, + param_idx: u32, + count: u32, + }, /// Level 13 (module isolation, negative form). Mirrors OCaml /// `Tw_verify.ModuleNotIsolated` (affinescript PR #280, issue #35): diff --git a/crates/typed-wasm-verify/src/section.rs b/crates/typed-wasm-verify/src/section.rs index 0249cfe..e47d7e0 100644 --- a/crates/typed-wasm-verify/src/section.rs +++ b/crates/typed-wasm-verify/src/section.rs @@ -49,7 +49,11 @@ pub fn parse_ownership_section_payload(payload: &[u8]) -> Vec { .map(|_| OwnershipKind::from_byte(r.read_u8())) .collect(); let ret_kind = OwnershipKind::from_byte(r.read_u8()); - OwnershipEntry { func_idx, param_kinds, ret_kind } + OwnershipEntry { + func_idx, + param_kinds, + ret_kind, + } }) .collect() } @@ -69,12 +73,19 @@ pub fn parse_ownership_section_payload(payload: &[u8]) -> Vec { /// than 255 params (the engine limit is far lower), so this is /// unreachable in practice. pub fn build_ownership_section_payload(entries: &[OwnershipEntry]) -> Vec { - let count: u32 = entries.len().try_into().expect("entry count must fit in u32"); + let count: u32 = entries + .len() + .try_into() + .expect("entry count must fit in u32"); let mut out = Vec::with_capacity(4 + entries.len() * 8); out.extend_from_slice(&count.to_le_bytes()); for entry in entries { out.extend_from_slice(&entry.func_idx.to_le_bytes()); - let n_params: u8 = entry.param_kinds.len().try_into().expect("param count must fit in u8"); + let n_params: u8 = entry + .param_kinds + .len() + .try_into() + .expect("param count must fit in u8"); out.push(n_params); for k in &entry.param_kinds { out.push(k.to_byte()); @@ -121,7 +132,11 @@ mod tests { use OwnershipKind::*; fn entry(func_idx: u32, params: Vec, ret: OwnershipKind) -> OwnershipEntry { - OwnershipEntry { func_idx, param_kinds: params, ret_kind: ret } + OwnershipEntry { + func_idx, + param_kinds: params, + ret_kind: ret, + } } #[test] @@ -145,11 +160,15 @@ mod tests { #[test] fn single_entry_with_all_kinds() { // count=1, func_idx=42, n_params=4, params=[Linear, Unrestricted, ExclBorrow, SharedBorrow], ret=Linear - let payload = [1, 0, 0, 0, 42, 0, 0, 0, 4, 1, 0, 3, 2, 1]; + let payload = [1, 0, 0, 0, 42, 0, 0, 0, 4, 1, 0, 3, 2, 1]; let parsed = parse_ownership_section_payload(&payload); assert_eq!( parsed, - vec![entry(42, vec![Linear, Unrestricted, ExclBorrow, SharedBorrow], Linear)] + vec![entry( + 42, + vec![Linear, Unrestricted, ExclBorrow, SharedBorrow], + Linear + )] ); } diff --git a/crates/typed-wasm-verify/src/verify.rs b/crates/typed-wasm-verify/src/verify.rs index da9578a..5aaca03 100644 --- a/crates/typed-wasm-verify/src/verify.rs +++ b/crates/typed-wasm-verify/src/verify.rs @@ -65,7 +65,9 @@ impl Frame { *then_min += m; *then_max += x; } - Frame::IfElse { else_min, else_max, .. } => { + Frame::IfElse { + else_min, else_max, .. + } => { *else_min += m; *else_max += x; } @@ -151,9 +153,7 @@ pub(crate) fn count_op_range( }); } Operator::Else => { - let top = stack - .last_mut() - .expect("frame stack underflow at Else"); + let top = stack.last_mut().expect("frame stack underflow at Else"); match *top { Frame::IfThen { then_min, then_max } => { *top = Frame::IfElse { @@ -299,9 +299,7 @@ pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError> { let import = import?; match import.ty { wasmparser::TypeRef::Func(_) => import_count += 1, - wasmparser::TypeRef::Memory(_) - if imported_shared.is_none() => - { + wasmparser::TypeRef::Memory(_) if imported_shared.is_none() => { imported_shared = Some(format!( "module owns linear memory yet imports \ memory '{}.{}' (cross-module shared memory \ @@ -309,9 +307,7 @@ pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError> { import.module, import.name )); } - wasmparser::TypeRef::Table(_) - if imported_shared.is_none() => - { + wasmparser::TypeRef::Table(_) if imported_shared.is_none() => { imported_shared = Some(format!( "module owns linear memory yet imports table \ '{}.{}' (externally-backed table breaks L13 \ @@ -354,7 +350,12 @@ pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError> { } } - for OwnershipEntry { func_idx, param_kinds, .. } in entries { + for OwnershipEntry { + func_idx, + param_kinds, + .. + } in entries + { // Global func index → body index: skip imports. let Some(body_idx) = func_idx.checked_sub(import_count) else { // Imported function: no body to inspect (the import's host @@ -386,8 +387,8 @@ mod tests { use crate::section::build_ownership_section_payload; use crate::OwnershipEntry; use wasm_encoder::{ - CodeSection, CustomSection, Function, FunctionSection, ImportSection, Instruction, - Module, TypeSection, ValType, + CodeSection, CustomSection, Function, FunctionSection, ImportSection, Instruction, Module, + TypeSection, ValType, }; /// Build a single-function wasm module with the given function body @@ -605,7 +606,10 @@ mod tests { Err(VerifyError::Ownership(errs)) => { assert!(matches!( errs.as_slice(), - [OwnershipError::LinearNotUsed { func_idx: 0, param_idx: 0 }] + [OwnershipError::LinearNotUsed { + func_idx: 0, + param_idx: 0 + }] )); } other => panic!("expected LinearNotUsed, got {:?}", other), @@ -633,7 +637,10 @@ mod tests { Err(VerifyError::Ownership(errs)) => { assert!(matches!( errs.as_slice(), - [OwnershipError::LinearDroppedOnSomePath { func_idx: 0, param_idx: 0 }] + [OwnershipError::LinearDroppedOnSomePath { + func_idx: 0, + param_idx: 0 + }] )); } other => panic!("expected LinearDroppedOnSomePath, got {:?}", other), @@ -653,7 +660,11 @@ mod tests { Err(VerifyError::Ownership(errs)) => { assert!(matches!( errs.as_slice(), - [OwnershipError::LinearUsedMultiple { func_idx: 0, param_idx: 0, count: 2 }] + [OwnershipError::LinearUsedMultiple { + func_idx: 0, + param_idx: 0, + count: 2 + }] )); } other => panic!("expected LinearUsedMultiple, got {:?}", other), @@ -673,7 +684,11 @@ mod tests { Err(VerifyError::Ownership(errs)) => { assert!(matches!( errs.as_slice(), - [OwnershipError::ExclBorrowAliased { func_idx: 0, param_idx: 0, count: 2 }] + [OwnershipError::ExclBorrowAliased { + func_idx: 0, + param_idx: 0, + count: 2 + }] )); } other => panic!("expected ExclBorrowAliased, got {:?}", other), @@ -724,9 +739,7 @@ mod tests { /// Always carries an (empty) ownership section so the isolation /// check is reached (gated behind it, like the OCaml port). fn isolation_module(import_memory: bool) -> Vec { - use wasm_encoder::{ - EntityType, MemorySection, MemoryType, - }; + use wasm_encoder::{EntityType, MemorySection, MemoryType}; let mut module = Module::new(); if import_memory { diff --git a/crates/typed-wasm-verify/tests/cross_compat.rs b/crates/typed-wasm-verify/tests/cross_compat.rs index 139a8cb..bb552c1 100644 --- a/crates/typed-wasm-verify/tests/cross_compat.rs +++ b/crates/typed-wasm-verify/tests/cross_compat.rs @@ -44,8 +44,7 @@ use typed_wasm_verify::{ build_ownership_section_payload, extract_exports, verify_cross_module, verify_from_module, - CrossError, OwnershipEntry, OwnershipError, OwnershipKind, VerifyError, - OWNERSHIP_SECTION_NAME, + CrossError, OwnershipEntry, OwnershipError, OwnershipKind, VerifyError, OWNERSHIP_SECTION_NAME, }; use wasm_encoder::{ BlockType, CodeSection, CustomSection, EntityType, ExportKind, ExportSection, Function, diff --git a/tests/aspect/claim-envelope.mjs b/tests/aspect/claim-envelope.mjs new file mode 100644 index 0000000..95691bc --- /dev/null +++ b/tests/aspect/claim-envelope.mjs @@ -0,0 +1,324 @@ +#!/usr/bin/env node +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +// +// Claim-envelope aspect test. +// +// Every claim this repo makes in human-readable docs (README.adoc, +// ROADMAP.adoc, LEVEL-STATUS.md, EXPLAINME.adoc) is also a contract with +// the artefacts it ships (src/abi/typed-wasm.ipkg, src/parser/*, Rust +// crate constants, CI toolchain pins). When docs and artefacts drift, +// nobody notices until an audit week later. +// +// This test catches the drift class directly. Each assertion picks a +// claim made somewhere in the doc estate and checks it against the +// artefact that should embody it. It exits non-zero on any drift. +// +// The 2026-05 deep audit caught five drifts that this test is designed +// to have caught automatically: +// - "L11/L12 are not in typed-wasm.ipkg" (three doc files said so; +// the ipkg listed them) +// - "believe_me: 0" badge but unverified +// - OWNERSHIP_SECTION_NAME / wire-byte layout vs README spec +// - Justfile/Justfile/e2e.sh referencing renamed files +// - CI toolchain pins lagging source-required versions +// +// Run with: node tests/aspect/claim-envelope.mjs +// Wired into Justfile `test-aspect` and `quality` umbrella. + +import { readFileSync, existsSync, readdirSync } from "node:fs"; +import { resolve, dirname, join } from "node:path"; +import { fileURLToPath } from "node:url"; + +const ROOT = resolve(dirname(fileURLToPath(import.meta.url)), "..", ".."); + +let passed = 0; +let failed = 0; +let skipped = 0; +const failures = []; + +function ok(msg) { console.log(` OK ${msg}`); passed++; } +function bad(msg) { console.log(` FAIL ${msg}`); failed++; failures.push(msg); } +function skip(msg) { console.log(` SKIP ${msg}`); skipped++; } +function section(name) { console.log(`\n=== ${name} ===`); } + +function read(rel) { + return readFileSync(join(ROOT, rel), "utf8"); +} + +// ---------------------------------------------------------------------- +// 1. ipkg membership ⇔ documentation +// ---------------------------------------------------------------------- +section("1. ipkg membership matches doc claims"); + +const ipkg = read("src/abi/typed-wasm.ipkg"); +const ipkgModules = ipkg + .split("\n") + .map((l) => l.replace(/^[\s,]+/, "").trim()) + .filter((l) => /^[A-Z][A-Za-z0-9_.]+$/.test(l)); + +if (ipkgModules.length === 0) { + bad("could not parse any modules out of typed-wasm.ipkg"); +} else { + ok(`typed-wasm.ipkg lists ${ipkgModules.length} modules`); +} + +// Specific claim: L11/L12 (Tropical, Epistemic) status across docs vs ipkg. +// Audit fallout 2026-05: three doc files said "L11/L12 not in ipkg" when +// they were. We assert the docs match the actual ipkg state. +const tropicalInPkg = ipkgModules.includes("TypedWasm.ABI.Tropical"); +const epistemicInPkg = ipkgModules.includes("TypedWasm.ABI.Epistemic"); + +if (tropicalInPkg) { + ok("Tropical (L11) is in typed-wasm.ipkg"); +} else { + bad("Tropical (L11) missing from typed-wasm.ipkg"); +} +if (epistemicInPkg) { + ok("Epistemic (L12) is in typed-wasm.ipkg"); +} else { + bad("Epistemic (L12) missing from typed-wasm.ipkg"); +} + +// Now the contrapositive: if L11/L12 are in-package, no doc may claim +// "not part of the default checked Idris2 package" or similar without +// being marked superseded. +function assertDocsAgreeOnL11L12(path, regex) { + if (!existsSync(join(ROOT, path))) { + skip(`${path} not found — cannot cross-check L11/L12 claim`); + return; + } + const text = read(path); + const m = text.match(regex); + if (m && (tropicalInPkg || epistemicInPkg)) { + bad( + `${path}: still claims "${m[0].slice(0, 60).replace(/\s+/g, " ")}..." ` + + `while L11/L12 are in the ipkg`, + ); + } else { + ok(`${path} L11/L12 claims do not contradict the ipkg`); + } +} + +// Pattern that matches the dangerous stale wording. Designed conservatively +// to false-positive only on the exact "not in package / not part of ipkg" +// stale phrasing. +const stalePattern = + /L11.{0,4}L12[^\n]{0,180}?(not part of|not in.*(?:package|ipkg)|standalone.*fail)/i; +assertDocsAgreeOnL11L12("ROADMAP.adoc", stalePattern); +assertDocsAgreeOnL11L12("LEVEL-STATUS.md", stalePattern); +assertDocsAgreeOnL11L12("README.adoc", stalePattern); + +// ---------------------------------------------------------------------- +// 2. believe_me / postulate / assert_total badge +// ---------------------------------------------------------------------- +section("2. unsound-pattern badge truthfulness"); + +const idrisFiles = []; +function collectIdris(dir) { + for (const entry of readdirSync(join(ROOT, dir), { withFileTypes: true })) { + const sub = `${dir}/${entry.name}`; + if (entry.isDirectory()) collectIdris(sub); + else if (entry.name.endsWith(".idr")) idrisFiles.push(sub); + } +} +collectIdris("src/abi"); + +const banned = /\b(believe_me|postulate|assert_total|really_believe_me|Admitted|sorry|prim__crash|idris_crash)\b/; +let badPatternHits = 0; +for (const f of idrisFiles) { + const lines = read(f).split("\n"); + for (let i = 0; i < lines.length; i++) { + const line = lines[i]; + // Skip comment lines (-- ...) and block-comment-like (| header) + if (/^\s*(--|\|\|\|)/.test(line)) continue; + if (banned.test(line)) { + bad(`${f}:${i + 1} has banned pattern: ${line.trim()}`); + badPatternHits++; + } + } +} +if (badPatternHits === 0) { + ok(`all ${idrisFiles.length} .idr files: 0 non-comment occurrences of banned patterns`); +} + +// Now cross-check that the README badge actually says 0. +const readme = read("README.adoc"); +if (/believe__me-0/.test(readme)) { + ok("README badge claims believe_me=0 (matches reality)"); +} else if (/believe__me-[0-9]+/.test(readme)) { + bad("README badge no longer claims believe_me=0 — does it still match reality?"); +} else { + skip("README has no believe_me badge to cross-check"); +} + +// ---------------------------------------------------------------------- +// 3. Wire format: OwnershipKind enum matches README spec +// ---------------------------------------------------------------------- +section("3. Rust crate constants match README spec"); + +const libRs = read("crates/typed-wasm-verify/src/lib.rs"); + +// Spec from crates/typed-wasm-verify/README.md: +// u8 param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow) +const expectedWire = [ + ["Unrestricted", 0], + ["Linear", 1], + ["SharedBorrow", 2], + ["ExclBorrow", 3], +]; +for (const [name, byte] of expectedWire) { + const re = new RegExp(`${name}\\s*=\\s*${byte}\\b`); + if (re.test(libRs)) { + ok(`OwnershipKind::${name} = ${byte} (matches README spec)`); + } else { + bad(`OwnershipKind::${name} = ${byte} not found in lib.rs`); + } +} + +// Section name constant +if (/OWNERSHIP_SECTION_NAME:\s*&str\s*=\s*"affinescript\.ownership"/.test(libRs)) { + ok("OWNERSHIP_SECTION_NAME = \"affinescript.ownership\" (matches doc claims)"); +} else { + bad("OWNERSHIP_SECTION_NAME constant drifted from \"affinescript.ownership\""); +} + +// ---------------------------------------------------------------------- +// 4. Test-file paths referenced from CI / Justfile actually exist +// ---------------------------------------------------------------------- +section("4. CI + Justfile path references are real"); + +function assertReferencedPathsExist(file, regex, label) { + if (!existsSync(join(ROOT, file))) { + skip(`${file} not found — cannot scan for ${label}`); + return; + } + const text = read(file); + let m; + const seen = new Set(); + while ((m = regex.exec(text)) !== null) { + const path = m[1]; + if (seen.has(path)) continue; + seen.add(path); + if (existsSync(join(ROOT, path))) { + ok(`${file} -> ${path}`); + } else { + bad(`${file} references ${path} which does not exist`); + } + } +} + +// Justfile recipe bodies: capture `node tests/...mjs` and `bash tests/...sh`. +assertReferencedPathsExist( + "Justfile", + /(?:node|bash)\s+(tests\/[^\s]+\.(?:mjs|sh)|benchmarks\/[^\s]+\.mjs)/g, + "Justfile invoked test/bench files", +); + +// tests/e2e.sh referenced paths (the file-existence check arrays). +assertReferencedPathsExist( + "tests/e2e.sh", + /"(tests\/[^"]+\.mjs|[A-Z][^"\s]+\.(?:adoc|md))"/g, + "tests/e2e.sh referenced files", +); + +// ---------------------------------------------------------------------- +// 5. CI toolchain pins match what the source actually requires +// ---------------------------------------------------------------------- +section("5. CI toolchain pins match source intent"); + +const e2eYml = existsSync(join(ROOT, ".github/workflows/e2e.yml")) + ? read(".github/workflows/e2e.yml") + : ""; +const buildZig = existsSync(join(ROOT, "ffi/zig/build.zig")) + ? read("ffi/zig/build.zig") + : ""; +const proofsIdr = existsSync(join(ROOT, "src/abi/TypedWasm/ABI/Proofs.idr")) + ? read("src/abi/TypedWasm/ABI/Proofs.idr") + : ""; + +// Zig: source intent comes from build.zig header comment. +// CI pin lives in e2e.yml as `ZIG_VERSION="x.y.z"`. +const zigSrcWantMatch = buildZig.match(/Zig\s+(\d+\.\d+)/); +const zigCiMatch = e2eYml.match(/ZIG_VERSION="(\d+)\.(\d+)\.\d+"/); +if (zigSrcWantMatch && zigCiMatch) { + const wantMajorMinor = zigSrcWantMatch[1]; + const haveMajorMinor = `${zigCiMatch[1]}.${zigCiMatch[2]}`; + // build.zig says "0.15+", so CI's major.minor must be >= source intent. + const [wantMaj, wantMin] = wantMajorMinor.split(".").map(Number); + const [haveMaj, haveMin] = haveMajorMinor.split(".").map(Number); + if (haveMaj > wantMaj || (haveMaj === wantMaj && haveMin >= wantMin)) { + ok(`Zig CI pin ${haveMajorMinor}.x >= build.zig requirement ${wantMajorMinor}+`); + } else { + bad(`Zig CI pin ${haveMajorMinor}.x < build.zig requirement ${wantMajorMinor}+`); + } +} else { + skip("could not extract both Zig source intent and CI pin"); +} + +// Idris2: source intent comes from Proofs.idr header comment. +const idrisSrcWantMatch = proofsIdr.match(/Idris2\s+(\d+\.\d+\.\d+)/); +const idrisCiMatch = e2eYml.match(/IDRIS2_VERSION="(\d+\.\d+\.\d+)"/); +if (idrisSrcWantMatch && idrisCiMatch) { + if (idrisSrcWantMatch[1] === idrisCiMatch[1]) { + ok(`Idris2 CI pin ${idrisCiMatch[1]} matches Proofs.idr "${idrisSrcWantMatch[1]}"`); + } else { + bad(`Idris2 CI pin ${idrisCiMatch[1]} != Proofs.idr "verified with ${idrisSrcWantMatch[1]}"`); + } +} else { + skip("could not extract both Idris2 source intent and CI pin"); +} + +// ---------------------------------------------------------------------- +// 6. Example corpus parses (or is documented skipped) +// ---------------------------------------------------------------------- +section("6. .twasm example corpus is exercised"); + +const exampleDir = "examples"; +const examples = existsSync(join(ROOT, exampleDir)) + ? readdirSync(join(ROOT, exampleDir)).filter((f) => f.endsWith(".twasm")) + : []; +if (examples.length === 0) { + bad("examples/*.twasm corpus is empty"); +} else { + ok(`${examples.length} .twasm examples present`); + // The e2e driver tests these; we only verify presence here so the + // aspect test stays decoupled from parser availability. +} + +// ---------------------------------------------------------------------- +// 7. RSR / surface files claimed by docs actually exist +// ---------------------------------------------------------------------- +section("7. RSR surface files exist"); + +const rsrFiles = [ + "README.adoc", + "EXPLAINME.adoc", + "SECURITY.md", + "CONTRIBUTING.md", + "LICENSE", + "Justfile", + "0-AI-MANIFEST.a2ml", + "LEVEL-STATUS.md", + "ROADMAP.adoc", + "PROOF-NEEDS.md", + "TEST-NEEDS.md", +]; +for (const f of rsrFiles) { + if (existsSync(join(ROOT, f))) ok(`RSR file: ${f}`); + else bad(`RSR file missing: ${f}`); +} + +// ---------------------------------------------------------------------- +// Summary +// ---------------------------------------------------------------------- +console.log(""); +console.log("=============================="); +console.log(` Aspect (claim envelope): ${passed} passed, ${failed} failed, ${skipped} skipped`); +console.log("=============================="); +if (failed > 0) { + console.log("\nClaim-envelope drift detected:"); + for (const f of failures) console.log(` - ${f}`); + process.exit(1); +} +process.exit(0); diff --git a/tests/e2e.sh b/tests/e2e.sh index 1ef8916..15dc3bd 100755 --- a/tests/e2e.sh +++ b/tests/e2e.sh @@ -256,7 +256,7 @@ RSR_FILES=( "README.adoc" "EXPLAINME.adoc" "SECURITY.md" - "CONTRIBUTING.adoc" + "CONTRIBUTING.md" "LICENSE" "Justfile" "0-AI-MANIFEST.a2ml" @@ -279,7 +279,7 @@ SPDX_CHECK_FILES=( "src/parser/Parser.res" "src/parser/Lexer.res" "ffi/zig/src/main.zig" - "tests/e2e/e2e-smoke.mjs" + "tests/smoke/e2e-smoke.mjs" ) for f in "${SPDX_CHECK_FILES[@]}"; do @@ -300,9 +300,9 @@ done section "9. Smoke test invocability" if command -v node &>/dev/null; then - echo " Invoking: node tests/e2e/e2e-smoke.mjs" - if node tests/e2e/e2e-smoke.mjs 2>&1 | tail -5; then - if node tests/e2e/e2e-smoke.mjs 2>&1 | grep -q "passed"; then + echo " Invoking: node tests/smoke/e2e-smoke.mjs" + if node tests/smoke/e2e-smoke.mjs 2>&1 | tail -5; then + if node tests/smoke/e2e-smoke.mjs 2>&1 | grep -q "passed"; then pass "Smoke test ran and reports passed" else fail "Smoke test ran but reported failures or no 'passed' summary"