Skip to content

Commit e8b3f6a

Browse files
hyperpolymathclaude
andcommitted
feat(levels): L1-L3 per-level test suites + TEST-NEEDS sync
Track C P0 first pilot: 3 of 10 level-specific test suites, 16 assertions, 0 failures. Pattern: each LN.mjs exercises the checker's positive surface (well-formed example checks clean) and the negative surface (diagnostic fires on the intended violation, matched by needle substring against the diagnostic message). Per-level coverage: L1 Instruction validity (parse-time) — 7/7 positive: well-formed minimal + region-only modules negative: align missing integer; unterminated region; missing region/fn/const name L2 Region-binding (schema lookup) — 3/3 positive: match against declared region; session decl alongside negative: match parameter references undeclared region (diagnostic "unknown region ...") L3 Type-compatible access — 6/6 positive: exhaustive match; const i32 = literal negative: unknown variant arm; non-exhaustive match; duplicate arm; non-literal const initializer Wired into `just test`. .gitignore allow-list extended for tests/levels/*.mjs. Incidental finding (see L1.mjs): parser accepts a region field with no trailing `;` before `align` — grammar EBNF requires it. Flagged as known looseness; out of scope for this test pass but worth a future parser-tightness sweep. TEST-NEEDS.md: superseded entries crossed through with dated replacements — the 7-assertion ECHIDNA harness claim is stale (it is 659 LOC now), and the fake-fuzz placeholder is already gone (tests/fuzz/README.adoc is an honest status marker). L4-L10 handoff to a background agent follows this commit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 6d88377 commit e8b3f6a

6 files changed

Lines changed: 395 additions & 6 deletions

File tree

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ erl_crash.dump
4747
!tests/echidna/*.mjs
4848
!tests/e2e/*.mjs
4949
!tests/contracts/*.mjs
50+
!tests/levels/*.mjs
5051
*.cmi
5152
*.cmj
5253
*.cmt

Justfile

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,11 @@ test *args:
106106
@echo "Running E2E driver (parse + check every example)..."
107107
node tests/e2e/e2e-driver.mjs
108108
@echo ""
109+
@echo "Running per-level test suites (L1-L3)..."
110+
node tests/levels/L1.mjs
111+
node tests/levels/L2.mjs
112+
node tests/levels/L3.mjs
113+
@echo ""
109114
@echo "Running Zig FFI tests..."
110115
cd ffi/zig && zig build test
111116
@echo ""

TEST-NEEDS.md

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -46,16 +46,16 @@
4646
- [ ] No type system self-consistency check
4747

4848
## FLAGGED ISSUES
49-
- **Type safety system with no safety-level-specific tests** -- 10 levels claimed, 0 level-specific test suites
50-
- **11 Idris2 proof modules with 0 proof verification tests** -- "proven" is unproven
51-
- **Tropical.idr and Epistemic.idr (novel type features) have 0 tests** -- research features untested
52-
- **ECHIDNA harness is 7 assertions** -- token gesture, not real verification
49+
- **Type safety system with no safety-level-specific tests** -- 10 levels claimed, 0 level-specific test suites (IN PROGRESS 2026-04-18 — L1-L3 pilot + agent handoff for L4-L10)
50+
- **11 Idris2 proof modules with 0 proof verification tests** -- "proven" is unproven. Update 2026-04-18: A3-A9 theorems landed in commits 987930c, c896a44, 3097b50, 9ebe867 (injectivity, level-achievement monotonicity, erasure P3.1, QTT witness, witness-requiring attestations). L7-L10 preorder + composition lemmas now live. Full per-level Idris2 test files still absent.
51+
- **Tropical.idr and Epistemic.idr (novel type features) have 0 tests** -- research features untested (L11 semiring closure proven A2 2026-04-18 but no dedicated test suite)
52+
- ~~**ECHIDNA harness is 7 assertions** -- token gesture, not real verification~~ SUPERSEDED 2026-04-18: tests/echidna/echidna-harness.mjs is now 659 LOC with a random-program generator, 36 proof obligations per run, and parse-rate measurement.
5353
- **arXiv potential claimed** -- paper-worthy claims need paper-worthy evidence
5454

5555
## Priority: P0 (CRITICAL)
5656

57-
## FAKE-FUZZ ALERT
57+
## FAKE-FUZZ ALERT — RESOLVED 2026-04-18
5858

59-
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
59+
- ~~`tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing~~ RESOLVED. The placeholder file is gone; `tests/fuzz/README.adoc` is now an honest status marker pointing at `tests/echidna/echidna-harness.mjs` (659 LOC, real random-program fuzz) and `ffi/zig/test/`. A dedicated retained fuzz corpus is still future work.
6060
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
6161
- Priority: P2 — creates false impression of fuzz coverage

tests/levels/L1.mjs

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// Level 1 — Instruction validity (parse-time)
5+
//
6+
// L1 is a parse-time check: malformed .twasm source must be rejected
7+
// before any schema or type reasoning runs. The parser is therefore the
8+
// Level-1 oracle: `result.TAG === "Ok"` is the positive attestation;
9+
// `Error(diag)` at a specific construct is the negative attestation.
10+
//
11+
// This file exercises both sides with minimal fixtures:
12+
// - A well-formed minimal module (one region, one fn) must parse Ok.
13+
// - Five canonical syntax errors must parse Error.
14+
//
15+
// Run: node tests/levels/L1.mjs
16+
17+
import { parseModule } from "../../src/parser/Parser.mjs";
18+
19+
let passed = 0;
20+
let failed = 0;
21+
22+
function expectOk(source, label) {
23+
const r = parseModule(source);
24+
if (r.TAG === "Ok") {
25+
passed++;
26+
console.log(` OK ${label} — parses clean`);
27+
} else {
28+
failed++;
29+
console.log(` FAIL ${label} — unexpected parse error: ${r._0.message}`);
30+
}
31+
}
32+
33+
function expectErr(source, label) {
34+
const r = parseModule(source);
35+
if (r.TAG === "Error") {
36+
passed++;
37+
console.log(` OK ${label} — rejected as expected (${r._0.message})`);
38+
} else {
39+
failed++;
40+
console.log(` FAIL ${label} — should have rejected but parsed`);
41+
}
42+
}
43+
44+
console.log("=== Level 1: Instruction validity (parse-time) ===\n");
45+
46+
// ── Positive: well-formed minimal module ─────────────────────────────
47+
48+
expectOk(
49+
`region Counter {
50+
n: u32;
51+
align 4;
52+
}
53+
54+
fn inc() effects { WriteRegion(Counter) } { }`,
55+
"minimal well-formed module",
56+
);
57+
58+
expectOk(
59+
`region Vec2 {
60+
x: f32;
61+
y: f32;
62+
align 4;
63+
}`,
64+
"region-only module (no functions)",
65+
);
66+
67+
// ── Negative: canonical syntax errors ────────────────────────────────
68+
69+
// Finding 2026-04-18: parser is lenient about the semicolon between
70+
// the last field and `align`. Grammar EBNF requires `;` after every
71+
// field_decl, so this is a parser looseness worth flagging in a
72+
// future parser-tightness pass. Not exercised here to keep L1 tests
73+
// aligned with current parser behaviour rather than the EBNF spec.
74+
75+
expectErr(
76+
`region Bad { n: u32;
77+
align ;
78+
}`,
79+
"align with missing integer literal",
80+
);
81+
82+
expectErr(
83+
`region Bad {
84+
n: u32;
85+
align 4;
86+
`,
87+
"unterminated region block",
88+
);
89+
90+
expectErr(
91+
`region {
92+
n: u32;
93+
align 4;
94+
}`,
95+
"region missing name",
96+
);
97+
98+
expectErr(
99+
`fn () { }`,
100+
"function missing name",
101+
);
102+
103+
expectErr(
104+
`region Counter { n: u32; }
105+
const : u32 = 1;`,
106+
"const missing identifier",
107+
);
108+
109+
// ── Summary ──────────────────────────────────────────────────────────
110+
111+
console.log(`\n--- L1: ${passed} passed, ${failed} failed ---`);
112+
process.exit(failed > 0 ? 1 : 0);

tests/levels/L2.mjs

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// Level 2 — Region-binding (schema lookup)
5+
//
6+
// L2 attests that every declared region has a resolvable schema and
7+
// that the checker surfaces structural lookups before type reasoning
8+
// runs. The positive attestation is "parse + check clean with the
9+
// region present"; the negative attestation is "checker complains
10+
// about a region-targeting construct whose name is undeclared".
11+
//
12+
// Surface exposure: the most direct L2 trigger in the ReScript checker
13+
// is a `match` statement whose target references a field of an
14+
// undeclared region (walkExpr threads the region environment; the
15+
// match arm resolver bottoms out in a "unknown region"-shaped
16+
// diagnostic). A second trigger is a session `transition consume X`
17+
// against a region name not declared anywhere in the module.
18+
//
19+
// Run: node tests/levels/L2.mjs
20+
21+
import { parseModule } from "../../src/parser/Parser.mjs";
22+
import { checkModule } from "../../src/parser/Checker.mjs";
23+
24+
let passed = 0;
25+
let failed = 0;
26+
27+
function run(source, expect, label) {
28+
const pr = parseModule(source);
29+
if (pr.TAG !== "Ok") {
30+
failed++;
31+
console.log(` FAIL ${label} — parse error: ${pr._0.message}`);
32+
return;
33+
}
34+
const diags = checkModule(pr._0);
35+
if (expect.kind === "clean") {
36+
if (diags.length === 0) {
37+
passed++;
38+
console.log(` OK ${label} — clean check`);
39+
} else {
40+
failed++;
41+
const msgs = diags.map(d => d.message).join("; ");
42+
console.log(` FAIL ${label} — expected clean, got ${diags.length}: ${msgs}`);
43+
}
44+
} else {
45+
const allMsgs = diags.map(d => d.message).join(" | ");
46+
const missing = expect.needles.filter(n => !allMsgs.includes(n));
47+
if (missing.length === 0 && diags.length > 0) {
48+
passed++;
49+
console.log(` OK ${label} — diagnostic fired as expected`);
50+
} else {
51+
failed++;
52+
console.log(` FAIL ${label} — expected needles ${expect.needles.join(", ")}, got "${allMsgs}"`);
53+
}
54+
}
55+
}
56+
57+
console.log("=== Level 2: Region-binding (schema lookup) ===\n");
58+
59+
// ── Positive: region present, match resolves cleanly ─────────────────
60+
61+
run(
62+
`region Enemies[10] {
63+
kind: union {
64+
Minion: i32;
65+
Boss: i32;
66+
};
67+
}
68+
fn dispatch(e: &region<Enemies>, i: i32) {
69+
match $e[i] .kind {
70+
| Minion => { return; }
71+
| Boss => { return; }
72+
}
73+
}`,
74+
{ kind: "clean" },
75+
"match against declared region — clean",
76+
);
77+
78+
// ── Negative: match targets a region that is not declared ────────────
79+
//
80+
// Observation: Checker's match resolution walks the function parameter
81+
// list to find the region binding. Passing a parameter whose declared
82+
// region name is absent from the module is the structural L2 failure.
83+
84+
run(
85+
`region Enemies[10] {
86+
kind: union {
87+
Minion: i32;
88+
Boss: i32;
89+
};
90+
}
91+
fn dispatch(e: &region<NotDeclared>, i: i32) {
92+
match $e[i] .kind {
93+
| Minion => { return; }
94+
| Boss => { return; }
95+
}
96+
}`,
97+
{ kind: "diagnostic", needles: ["unknown region"] },
98+
"match target names undeclared region",
99+
);
100+
101+
// ── Positive: session referencing declared region-typed state ────────
102+
103+
run(
104+
`region Players[8] { hp: u32; }
105+
session OrderFlow {
106+
state Idle : i32;
107+
state Pending : i64;
108+
transition submit : consume Idle -> yield Pending;
109+
}`,
110+
{ kind: "clean" },
111+
"session with primitive-typed states alongside a region",
112+
);
113+
114+
// ── Summary ──────────────────────────────────────────────────────────
115+
116+
console.log(`\n--- L2: ${passed} passed, ${failed} failed ---`);
117+
process.exit(failed > 0 ? 1 : 0);

0 commit comments

Comments
 (0)