Reference evaluator (ADR-0015, Rust): als-ref with λ_almd agreement 49/49, three gates, abstain ledger 429/602, first two reference findings

[O6lvl4]

Frontier #1 of the aviation-quality arc, first slice: the judge-owned reference evaluator (#10, ADR-0015 — ratified, then amended to Rust with the user before any code existed).

What lands

• ref/ — als-ref, a fresh, source-level evaluator of Almide programs written from the ALS chapters and the EBNF: stable Rust pinned to 1.95.0 = Ferrocene 26.05.0's upstream (rebuild under criticalup is a CI-step change), zero dependencies, no almide-* crate, behind the black-box protocol als-ref run <file> --json → {exit, stdout, stderr} | {abstain: {class, reason}} | {error}.
• Aviation-quality clauses, structural: clippy.toml forbids HashMap/HashSet (clause 1) and the std string/number/sort methods whose behaviour the ALS specifies (clause 5); F64 implements no Display; every AST match is exhaustive, unimplemented forms are explicit classified abstains (clause 2); rust-toolchain.toml pins the channel (clause 4); the independence gate reads cargo tree (clause 6).
• proofs/kernel-conformance/ — the λ_almd corpus carried in with provenance (48 programs + the nine-line kAll trace).
• Three gates, wired into gates.yml (cached cargo, ~1 min): check-ref-kernel.py (agreement 49/49, twice — floor 1.0, determinism), check-ref-independence.sh, check-ref-totality.py (+ proofs/ref-abstain.toml, shrink-only).
• docs/ref/PARSER-NOTES.md: 13 decisions where text and corpus disagreed, the rules the evaluator abstains on until the ALS states them, and the findings below.

Measured at this commit (spec/wasm_cross + spec/programs, 602 programs)

λ_almd kernel	49/49 byte-identical, run twice
evaluated	173 — of the 172 comparable against the native target, 171 agree
abstained	429 in 152 classes (long tail: list.map 38, list.fold 17, bytes.new 14, int.parse 14, value.int 13, float.to_string 12, …) — the ratchet's work
evaluator faults	0

Findings — the class limitation 2 said agreement could not see

• F1 grain_functions.almd labeled_args6: the fixture's own comment says evaluation order is the WRITTEN order; ALS-E26 says 先頭から順; the implementation evaluates named args in PARAMETER order (second then first). The evaluator follows the written order and disagrees → ALS-E26 must decide, then either the comment or the implementation is wrong.
• F2 effect_assign_unwrap.almd: xs[0] = step(10) (index-assign of an effect call, no !) is accepted and the Int slot receives the unwrapped value — a residual implicit-propagation site after ADR-0008. The evaluator keeps the Result and cannot type the next call → semantics:type-mismatch.
• Stale ALS text surfaced: ALS-M4 still describes auto-?; ALS-M14's carrier paragraph predates the UInt64 upper-half lane (C-179); ALS-E10's "束縛は実体化" predates #1400 (C-238).

Not in this PR (next)

scripts/conformance.py --legs ref (verdict legs == ref) + selftest scenarios + runner-coverage ledger; the stdlib long tail against the ledger; ADR-0016's numeric rules for the float/overflow abstains.

🤖 Generated with Claude Code