From ea66a2abdab1edc682dc960a1f605de17d6b8273 Mon Sep 17 00:00:00 2001 From: developtheweb Date: Thu, 9 Jul 2026 19:21:13 -0400 Subject: [PATCH] Gate CI on ratified conformance --- .github/workflows/ci.yml | 34 +++++ conformance/JUDGMENT_CALLS.md | 274 ++++++++++++++++++++++++++++++++++ 2 files changed, 308 insertions(+) create mode 100644 conformance/JUDGMENT_CALLS.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7108842..0c49ff0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -41,3 +41,37 @@ jobs: - name: Run interpreter tests run: node --test "js/test/*.test.mjs" + + conformance: + runs-on: ubuntu-latest + steps: + - name: Check out + uses: actions/checkout@v4 + + - name: Set up JDK 21 + uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: '21' + + - name: Set up Node 24 + uses: actions/setup-node@v4 + with: + node-version: '24' + + # Gates on ratified entries only. Exits 0 vacuously while nothing is + # ratified — unratified observations must never become a CI gate. + - name: Ratified conformance corpus passes + run: node conformance/harness/run.mjs --ratified + + # Locked decision: the corpus is downstream of the syntax truth. Every + # program must parse, except must-reject entries whose expected error + # is parse-class — the grammar rejects those too (verified in C3). + - name: Grammar accepts every runnable corpus program + run: | + runnable=$(for d in conformance/corpus/*/; do + if [ -f "${d}expected.out" ]; then echo "${d}program.mpl" + elif ! grep -qE '^err_(char|escape|string|comment|expect|unexpected|def_target|assign_target)$' "${d}expected.err"; then echo "${d}program.mpl" + fi + done | tr '\n' ' ') + ./gradlew -q parseCheck --args="$runnable" diff --git a/conformance/JUDGMENT_CALLS.md b/conformance/JUDGMENT_CALLS.md new file mode 100644 index 0000000..c7efb9f --- /dev/null +++ b/conformance/JUDGMENT_CALLS.md @@ -0,0 +1,274 @@ +# JUDGMENT_CALLS — semantic decisions awaiting ratification + +Every section below is a semantic question the interpreter currently +answers by accident of implementation. Nothing here is ratified. Each +section states the question, what `js/mpl.js` observably does today, and +which corpus entries pin that behavior. The `RULING:` line is blank on +purpose — rulings are Reverend's, in Stage 3, in batches. A ruling either +blesses the observed behavior (the pinning entries flip to `ratified`) or +overrules it (the interpreter changes, the entries are re-recorded, then +ratified). + +## 1. Division by zero + +Question: what does `x ÷ 0` do — error, infinity, or ⊥? +Observed: raises `err_div0` (both `÷` and `/`, integer or float operands). +Pins: `043_div_zero`. + +RULING: + +## 2. The value of a ∀ expression + +Question: what does `∀ x ∈ list : body` evaluate to? +Observed: the value of the last body evaluation; `⊥` for an empty list. +Pins: `018_forall_value`, `019_forall_scope`. + +RULING: + +## 3. Result when no guard matches + +Question: what is `(false ⟹ e)` with no `|` fallback? +Observed: an internal no-match that surfaces as `⊥` everywhere except +directly to the left of `|`. +Pins: `021_no_guard_match`, `023_alt_chain`. + +RULING: + +## 4. Integer vs float display + +Question: is `4 ÷ 2` shown as `2` or `2.0`? Are all numbers one type? +Observed: all numbers are IEEE doubles; integral values display with no +decimal point (`2`), non-integral as JS renders them (`0.5`, and +`0.1 + 0.2` shows `0.30000000000000004`). Literals normalize (`007` → `7`, +`0.50` → `0.5`). +Pins: `006_number_display`, `007_float_arithmetic`. + +RULING: + +## 5. ✎ formatting per type + +Question: exactly how does `✎` render each value type? +Observed: numbers via host `String()`; strings bare at top level but +quoted inside lists; booleans `true`/`false`; lists `[a, b]` with +one-space separation; closures as `λ`; `⊥` as `⊥`. +Pins: `009_string_concat`, `011_list_display`, `031_show_all_types`. + +RULING: + +## 6. ⊥ display and propagation + +Question: is `⊥` a first-class value or a poison that propagates? +Observed: a first-class value — it displays as `⊥`, concatenates into +strings (`"x" + ⊥` → `x⊥`), sits in lists, but arithmetic on it is +`err_num`. +Pins: `030_bot`, `052_bot_arith`. + +RULING: + +## 7. Equality across types + +Question: what does `=` mean across types and on structures? +Observed: structural (JSON-serialization) equality — lists compare +element-wise, cross-type comparisons are `false` (`1 = "1"` → `false`), +and `⊥ = ⊥` → `true`. Comparing a self-referential closure crashes with a +keyless host error (unpinnable by the corpus). +Pins: `034_cross_type_equality`, `033_string_compare`. + +RULING: + +## 8. Ordering across types + +Question: what do `< > ≤ ≥` do on mixed or non-numeric operands? +Observed: raw host comparison with JS coercion — `1 < "2"` → `true`, +`"10" < 9` → `false`, `true < 2` → `true`; strings order lexicographically. +Pins: `035_mixed_compare`, `033_string_compare`. + +RULING: + +## 9. Closure capture + +Question: do closures capture values at definition time or the +environment? +Observed: the environment — later mutation of a captured variable is +visible on the next call (`013` prints 11 then 21). +Pins: `013_closure_capture`, `026_def_vs_assign_scope`. + +RULING: + +## 10. Recursion depth + +Question: what bounds recursion, and how does exceeding it surface? +Observed: the host JS stack — deep recursion dies as a keyless RangeError +before the 500 000-step budget can trigger, so the corpus cannot pin it +(no error key). Iteration-heavy programs do hit the budget and raise +`err_steps`. Depth ~500 is comfortably safe. +Pins: `016_recursion_sum` (works at 500), `053_step_budget` (`err_steps`). + +RULING: + +## 11. The step budget itself + +Question: is "500 000 evaluation steps, then `err_steps`" part of the +language, and is that the right number? +Observed: hard-coded 500 000; nested `∀` loops over a 10-element list six +deep exceed it. +Pins: `053_step_budget`. + +RULING: + +## 12. String escape round-tripping + +Question: which string escapes exist, and what does an unknown one mean? +Observed: `\n` and `\t` expand; `\"` and `\\` escape themselves; any other +`\x` silently drops the backslash (`"drop\qme"` → `dropqme`). The ANTLR +grammar instead REJECTS unknown escapes — a recorded divergence. +Pins: `008_string_escapes`; divergence in DIVERGENCES.md ("drop\qme" and +the `"a\zb"` fuzz entry). + +RULING: + +## 13. Guard condition truthiness + +Question: what may a guard condition be? +Observed: `true` and non-zero numbers fire the guard; `false`, `0`, +strings, lists and `⊥` do not (they yield the no-match path) — so numbers +are truthy for `⟹` but nothing else is. +Pins: `022_guard_truthiness`. + +RULING: + +## 14. ∧ ∨ operand truth + +Question: do `∧`/`∨` accept the same truthiness as `⟹`? +Observed: no — operands are tested with strict boolean equality, so +`1 ∧ true` → `false` while `(1 ⟹ x)` fires. Both operators short-circuit +(observable by side effect). This asymmetry with #13 is the sharpest +accident in the surface. +Pins: `036_logic_ops`, `037_logic_short_circuit`. + +RULING: + +## 15. Block scoping + +Question: does `{ … }` create a scope? +Observed: no — bindings made inside a brace block leak out (`028` prints +9). Only λ bodies and each `∀` iteration scope. +Pins: `028_block_no_scope`, `027_block_sequencing`. + +RULING: + +## 16. ≜ vs ← scoping and creation + +Question: how do define and assign differ? +Observed: `≜` always binds in the current scope; `←` mutates the nearest +enclosing binding and silently creates one in the current scope when +nothing is bound (assignment-before-definition is legal). Both are +expressions returning the value; both rebind freely (`x ≜ 1; x ≜ 3` is +legal re-definition). +Pins: `024_def_assign_rebind`, `025_def_assign_value`, +`026_def_vs_assign_scope`. + +RULING: + +## 17. Type constraints + +Question: does `λx∈ℕ:` constrain anything? +Observed: the constraint parses (including supplementary-plane `𝔹`) and +is discarded unevaluated — `g ≜ λs∈𝔹: s + "!"` happily takes a string. +Matches the site's "parsed today, not yet enforced" claim. +Pins: `039_type_constraint_unenforced`. + +RULING: + +## 18. Nullary calls and zero-parameter λ + +Question: `f()` parses — but can any function be called that way? +Observed: no zero-parameter λ can be written (`λ: e` is a parse error), +so every `f()` is a runtime `err_arity`. The call syntax exists; nothing +can satisfy it. +Pins: `046_arity_nullary`, `047_arity_extra`. + +RULING: + +## 19. ∗ as multiplication + +Question: is `∗` (U+2217) an operator, and what does it mean? +Observed: exactly `×` — same token, same precedence. +Pins: `041_asterisk_multiplication`. + +RULING: + +## 20. Divergence: empty program + +Question: is the empty program valid? +Observed: the grammar accepts it; the JS interpreter rejects it +(`err_unexpected` at 1:1). +Pins: none possible until ruled (decision 3 — divergent programs cannot +enter the corpus). Repro in DIVERGENCES.md (fuzz index 49). + +RULING: + +## 21. Divergence: sequences inside parentheses + +Question: is `( e1 ; e2 )` valid? DECISIONS.md says `(...)` contains one +seqExpr; the JS parser allows exactly one expression. +Observed: the grammar accepts `(42;)` and `(a; b)`; the JS interpreter +rejects both (`err_expect`). +Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 86, 119, +247, 233, 279, 406, 468, 101…). + +RULING: + +## 22. Divergence: `∘` composition + +Question: does function composition exist in M0? +Observed: the grammar parses `f ∘ g`; the JS interpreter lexes `∘` (it +even has the `\circ` escape) but has no parse rule for it — every use is +`err_expect`. +Pins: none until ruled. Repro in DIVERGENCES.md (fuzz index 9). + +RULING: + +## 23. Divergence: set literals + +Question: `{a, b}` is a set per the grammar's brace disambiguation — does +the M0 core have sets? +Observed: the grammar accepts `({5, "a b"})` and friends; the JS +interpreter has no set support and rejects them (`err_expect`). +Pins: none until ruled. Repros in DIVERGENCES.md (multiple fuzz indexes). + +RULING: + +## 24. Divergence: record literals + +Question: `{k: v}` is a record per the grammar — does the M0 core have +records? +Observed: the grammar accepts `({y: 0})`; the JS interpreter rejects +(`err_expect`). +Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 25, 212, +425, 427, 447). + +RULING: + +## 25. Divergence: parenthesized λ parameters + +Question: DECISIONS.md rejected `λ(a, b):` as a second parameter spelling +— but who enforces that? +Observed: inverted from every other divergence — the GRAMMAR rejects +`λ(a, b): e` (honoring the decision) while the JS interpreter accepts it. +The interpreter carries a syntax form the language explicitly rejected. +Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 13, 29, +76, …). + +RULING: + +## 26. Divergence: bare λ and Greek letters as identifiers + +Question: the grammar tokenizes Greek letters (LAMBDA_VAR et al.) as +identifiers, so `{λ}` parses; the JS interpreter only knows λ as the +abstraction head. +Observed: grammar accepts `({λ})`; JS rejects (`err_expect` — λ demands a +parameter list). +Pins: none until ruled. Repro in DIVERGENCES.md (fuzz index 52). + +RULING: