ch05_closure_nat_return trapped once in a full conformance run (unreproducible in ~960 attempts) — suspected rare runtime/GC flake in a CI gate

[aallan]

Summary

tests/conformance/ch05_closure_nat_return.vera (run level) trapped once during a full scripts/check_conformance.py run, and has not reproduced since:

FAIL (run): ch05_closure_nat_return
  Error: Reached `unreachable` WASM instruction
  Source backtrace: in main  (.../ch05_closure_nat_return.vera:41-57)

The only trap sites in main's emitted WAT are the sentinel assert(@Nat.0 == 42) and the two GC shadow-stack-overflow guards — so that one run either computed apply_fn(abs, -42) != 42 or hit a shadow-stack guard.

Reproduction attempts (all clean)

• ~750 isolated executions of the program (500 tight-sequential + 150 parallel + 30 under VERA_EAGER_GC=1 + hash-seed sweeps) — 0 failures.
• 12 further full check_conformance.py runs at the time of capture — 1 failure in 13 total.
• A dedicated 12× full-suite batch (12 × 153 programs) after the fact — 0 failures.
• The emitted WAT for the closure is deterministic and arithmetically correct (-42 → 0-(-42)=42 → guard false → 42), verified by inspection and ~40 boundary executions.

Assessment

Not attributable to the #984 guard logic (deterministic WAT, massive clean-run evidence); most consistent with a rare pre-existing runtime/GC/wasmtime interaction that this two-closure-plus-assert program happens to be able to surface. Filed because the program sits in a pre-commit + CI gate: even a ≪1% flake will eventually red an unrelated PR, and when it does, the failure should resolve here rather than start a fresh investigation.

If it fires again

Capture: the full check_conformance.py output, wasmtime --version, OS/arch, and whether the run was under parallel load. The shadow-stack guards in main are the prime suspect ($gc_sp overflow checks); VERA_EAGER_GC=1 did not reproduce, so a load-dependent GC timing interaction is the leading hypothesis.

Captured during the PR #995 review round — the verbatim failure output, trap-site analysis from the preserved WAT, full reproduction-attempt table, and environment details are documented in the first comment below.

[aallan]

Durable evidence record (the issue body's "session record" reference is superseded by this comment).

The captured failure — verbatim

One full scripts/check_conformance.py run during the PR #995 review round produced:

FAIL (run): ch05_closure_nat_return
  Error: Reached `unreachable` WASM instruction
  Source backtrace: in main  (.../ch05_closure_nat_return.vera:41-57)

That is the complete failure signal — exit 1 from the run stage, backtrace pointing into main (lines 41–57), no further diagnostics. Every other program in the same run passed.

Trap-site analysis (from the preserved emitted WAT)

The reviewer disassembled the compiled module and inspected main's emission. The only unreachable sites reachable from main are:

1. the sentinel assert(@Nat.0 == 42) — i.e. that run computed apply_fn(abs, -42) != 42, or
2. the two GC shadow-stack overflow guards ($gc_sp bounds checks).

The abs closure's own emission ($anon_0) is deterministic and arithmetically correct: -42 → else-branch → 0 − (−42) = 42 → guard (42 < 0) false → returns 42, verified by inspection and by ~40 boundary-value executions. There is no data-dependent or randomized instruction in the path.

Reproduction attempts — all clean

Attempt	Count	Result
Isolated executions, tight sequential	500	0 failures
Isolated, parallel load	150	0 failures
Isolated, VERA_EAGER_GC=1	30	0 failures
Isolated, PYTHONHASHSEED sweep	13	0 failures
Full check_conformance.py runs at capture time	13	1 failure (the capture above)
Dedicated 12× full-suite batch afterward	12 × 153 programs	0 failures
Related panel replays of adjacent closure programs	~180	0 failures

Aggregate: one failure in roughly 960 opportunities, observed only under a full-suite run (fresh subprocess per program, machine under multi-agent load at the time).

Environment at capture

• macOS 26.5.1, arm64
• wasmtime (Python) 46.0.1
• Repo at PR fix(verifier/codegen): obligate and guard the @Int -> @Nat narrowing at closure returns #995 head (cdfaf86); the program is unchanged since except a comment.

Working hypothesis

Not the #984 guard logic (deterministic WAT, massive clean-run evidence). Most consistent with a rare runtime/GC/wasmtime timing interaction — the shadow-stack guards are the prime suspect since VERA_EAGER_GC=1 did not reproduce but the single failure occurred under parallel system load. If it fires again: capture the full check_conformance.py output, wasmtime version, OS/arch, and whether the machine was under load, and attach here.

[aallan]

Cross-link: #996 and #1121 are the two known sources of spurious CI red in the suite — worth tracking together, though they differ sharply in tractability.

• ch05_closure_nat_return trapped once in a full conformance run (unreproducible in ~960 attempts) — suspected rare runtime/GC flake in a CI gate #996 — ch05_closure_nat_return trapped once in a full conformance run and has resisted ~960 reproduction attempts. Cause unknown; suspected rare runtime/GC issue. Currently observation-only.
• test_rounding_relation_not_proved asserts stricter than its docstring — spurious failure when Z3 falls to Tier 3 #1121 — test_rounding_relation_not_proved asserts the obligation is violated where its own docstring also sanctions Tier 3, so it fails whenever Z3 exhausts its budget — reliably the windows-latest cell, which runs ~19m of test time against ~3m on the macOS/Linux cells. Cause known; the fix is widening one assertion.

Shared operational cost: both red-flag PRs whose diffs cannot have caused them — #1121 surfaced on #1114, a formatter-only change touching formatter.py, test_formatter.py, CHANGELOG.md, and TESTING.md.

Neither indicates a soundness regression. In #1121's case the verifier did not prove the false property; it fell back conservatively to Tier 3, which is the safe direction and exactly what the test's docstring permits.