WAST conformance is compile-only: 383 assertions in tests/wast are never checked, and the official testsuite is absent (kiln has a gate, synth does not)

[avrabe]

synth ships 383 spec-style assertions in tests/wast/ and checks none of them. The
only path CI runs against those files asserts that synth compile exits 0 — the
assert_return values are parsed and discarded. Separately, the official
WebAssembly testsuite is absent from this repo, so the compiler has never been
graded against the standard at all.

Sibling comparison is the sharp end: kiln (the interpreter) has a real conformance
gate; synth (the compiler) has none — and synth is the one whose output runs on
target.

Verified on 97bd6db (v0.55.0).

1. The wired path is compile-only

crates/synth-cli/tests/wast_compile.rs is the only consumer of tests/wast/ that
CI executes. Its own header states the scope:

//! Integration tests: compile every WAST file through synth and verify ELF output.
//! Each WAST file in tests/wast/ is compiled with --all-exports --cortex-m.

and every one of its ~59 cases bottoms out in:

assert!(result.status.success(), "synth compile failed for {} ...")

There is no assert_return / expected-value comparison anywhere in the file
(grep -n 'assert_return\|expected' crates/synth-cli/tests/wast_compile.rs → only an
unrelated relocation-count message).

Meanwhile the data those files carry:

in tests/wast/ (25 files)	count
assert_return	381
assert_trap	2
checked by CI	0

So i32_div.wast, i32_rotate.wast, control_factorial.wast etc. are graded on
"did the compiler emit an ELF", not "is the ELF correct". A codegen change that
made i32.rem_s return the wrong value would keep this suite green. That is the
same shape as #911 (cargo test -- <no match> exits 0) and the v0.54
sret_decide_differential.py gate that printed MISMATCH <-- BUG and exited 0 —
but here it is the primary correctness suite of the backend.

2. The runner that can check values is not wired, and can't run in CI as built

crates/synth-test/ genuinely parses assertions — WastTestRunner::parse_file()
yields WastTestCase { args, expected, expected_trap, test_type }, and
runner.rs:174 really does compare ExecutionResult::Return(actual) against the
expected value. The infrastructure is there. Two things stop it from counting:

• Zero references in CI. grep -rn "synth-test" .github/ scripts/ → 0 hits
  (only scripts/mythos/rank.md mentions the path). It is in no workflow, no
  bazel target, no gate.
• Renode-only execution. run_test() opens with
  self.controller.as_mut().context("Renode not connected")? and drives Renode over
  telnet, so it cannot run on a stock CI runner regardless.
• Its only two #[test]s (test_parse_simple_wast, test_robot_generation) parse a
  3-assertion inline string; neither touches tests/wast/.

Net: the value-checking runner exists, is correct-looking, and has never graded the
381 assertions.

3. The official testsuite is absent

WebAssembly/testsuite is not vendored, submoduled, or fetched anywhere in synth.
The 25 hand-written files are synth's own, so even if they were checked, coverage
would be whatever we happened to write — not the standard.

Suggested fix: adopt kiln's gate, don't build a second one

kiln already solved this in-org and the model is good. Please reuse it rather than
inventing a parallel mechanism:

• external/testsuite as a pinned submodule (.gitmodules → WebAssembly/testsuite),
  so conformance is reproducible, plus the monthly repin workflow (kiln#360).
• safety/wast-conformance-baseline.txt — the known-failing list.
• scripts/wast-conformance-gate.sh + .github/workflows/wast-conformance.yml —
  fails the build on any file failing that is not in the baseline, and surfaces
  newly-passing files as a notice so the baseline ratchets tighter.

For synth the only genuinely new part is the execution backend, since grading a
compiler means running its output. synth-test's parser needs no change — it already
produces args + expected. It needs an executor that works on a CI runner:

• native aarch64 on an arm64 runner is the cheapest honest option — synth's
  aarch64 backend output can be linked and called directly, no emulator;
• qemu-system-arm for the thumb-2/cortex-m path (already used elsewhere in the repo);
• keep Renode as the on-target/optional backend it is today.

A frontier note so the gate stays honest: a module synth declines must be reported
as declined, not passed and not failed — otherwise the baseline hides the
frontier. Only accepted-then-wrong should fail.

Why this matters more for synth than for kiln

kiln can be wrong and produce a wrong answer at runtime. synth is wrong in the
artifact that ships, and its consumers are exactly the targets that can't observe the
error. The compiler having weaker conformance evidence than the interpreter is the
wrong way round.

[avrabe]

I built the executor this issue asks for and ran it, so the gap is now measured rather
than inferred — and the headline is good news for the backend and bad news for the test
data.

Two results:

1. synth's AArch64 codegen is correct on everything I could execute — 350 of synth's
   own assertions and 907 assertions from the official WebAssembly testsuite, zero
   miscompiles.
2. 8 of the 383 assertions in tests/wast/ state the wrong expected value. They are
   wrong in the source data, not in the compiler. That is only possible because nothing
   has ever executed them — which is the concrete proof of this issue.

How it was built (no new WAST machinery)

Per "adopt, don't reinvent": the parser is synth-test used unmodified as a library.
WastParser::parse_file() already yields WastTestCase { function, args, expected, test_type }; nothing about WAST handling was rewritten. The only added piece is the one
synth lacks — an executor that runs on a plain arm64 host instead of Renode:

.wast → [synth-test parser, unmodified] → module + assertions
      → synth compile -b aarch64 --all-exports --relocatable
      → ld.lld -T (flat .text at 0)          ← required; see note below
      → mmap MAP_JIT, x28 = linear memory, blr
      → compare to the spec's own expected value

Each assertion runs in a forked child, so a brk #0 trap is observed as a signal death
instead of killing the harness — that gives assert_trap for free.

Result 1 — the 8 wrong expectations

ramp_pwm(current, target) reads ramp_rate from memory[28]. The module has no data
segment, so ramp_rate is 0. With rate 0, the guard diff > rate is true whenever
target != current, so the function returns current + 0 = current. The file's
comment — "with ramp_rate=0 (uninit'd memory), ramp_pwm snaps directly to target" —
misreads its own code, and 7 assertions encode that misreading.

Verified against wasmtime as an independent oracle:

ramp_pwm(cur, tgt)	.wast expects	wasmtime	synth aarch64
(0, 100)	100	0	0
(0, 500)	500	0	0
(500, 0)	0	500	500
(100, 100)	100	100	100
(800, 1000)	1000	800	800
(1000, 800)	800	1000	1000
(0, 0)	0	0	0
(0, 1000)	1000	0	0
(1000, 0)	0	1000	1000

The only two that pass are the two where current == target — i.e. where returning the
wrong operand is indistinguishable from returning the right one.

Also large_function.wast: large_compute(1) is asserted to be 287; wasmtime and synth
both compute 3538945.

These 8 need the expectations corrected (or the functions changed to match intent). I
have not touched them.

Result 2 — the official testsuite passes

Against WebAssembly/testsuite (257 files), executing on AArch64:

passed:      907
failed:        0
skipped:      64   (assertion shapes the executor can't drive)
declined:     68   (SYNTH refused the module — synth's frontier)
unsupported: 166   (the HARNESS can't model the file — my limit, not synth's)

i32.wast 374/374 and i64.wast 384/384 pass, traps included. Every decline is
loud and specific — multi-memory (#406, 17 files), table ops, v128, exceptions — so there
is no silent-wrong-answer anywhere in what ran. That is a genuinely strong result for the
backend; it just had no way to be known before.

Two things that would raise coverage a lot

The unsupported: 166 is dominated by one parser limitation, worth fixing in synth-test
itself:

• ParsedWast keeps only one module. current_module_binary is overwritten by each
  WastDirective::Module (lib.rs:240), and test_cases carries no module association. So
  for a multi-module file (elem.wast has 76, type-subtyping.wast 46, linking.wast 21)
  there is no way to know which module an assertion belongs to. Worse, an assertion can
  silently resolve against a different module's identically-named export. Associating each
  test case with the module in scope when it was parsed would unlock most of those 166 files.
• No element/global/start initialisation in my executor, so table- and global-dependent
  files are refused wholesale rather than graded.

A trap worth recording for whoever wires this up

The relocatable object must be linked before its .text is executed. A raw
--only-section=.text copy leaves R_AARCH64_ADR_PREL_PG_HI21/ADD_ABS_LO12_NC (for
__synth_func_table) and JUMP26 unresolved, so adrp points at garbage and perfectly
correct call_indirect code traps. Read naively that looks like a critical codegen bug;
it isn't. ld.lld -T with .text at 0 fixes it and makes each symbol's st_value its
offset into the blob.

Equally: my own first full-suite run reported 20+ "miscompiles" that were all harness
artifacts — multi-module resolution, and unapplied data segments (linking.wast "want 104,
got 0" was simply memory I never initialised). A conformance gate that reports those as
compiler bugs is worse than no gate, so the runner now refuses any file it cannot model
faithfully and reports unsupported separately from synth's own declined. Whatever
lands in-tree should keep that distinction — collapsing the two would misreport the
compiler's frontier in both directions.

Happy to hand over the executor if it is useful as a starting point; it is ~380 lines and
its only dependencies beyond synth-test are object, wasmparser, and libc.