You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
fix(#624): fence Lean/Why3 on early return; finish the soundness-gate small calls (#633)
Follow-up to #631. Closes one of the two holes the gate's pins watch,
and finishes the "small calls."
## #624 — Lean/Why3 silently drop `return` → now fail loud
The experimental emitters' `gen_block` skipped non-`let` statements, so
`fn f(){ return 1; … }` lowered to `:= ()`. Added
`Ast.fn_body_contains_return`; `codegen_lean`/`codegen_why3` now return
`Error` on an early `return`.
**The pinned-residual discipline, exercised end-to-end (by running, not
eyeballing):**
1. Made the fence → ran the harness → it reported `XPASS
test_stub_backend_return_xfail` and exited non-zero: *"is the hole
fixed? update docs/SOUNDNESS.adoc"*.
2. Followed that instruction: moved the `#555-stub` row `residual
(pinned)` → `loud-fail`, and converted the xfail pin to a **positive
fence-check** `test_stub_backend_return_fenced` (asserts `codegen_lean`
returns `Error`).
## Small calls — done
- **Content-bind suite files.** The manifest now seals `suite:` anchors
(whole-file hash); `test/test_borrow_polonius.ml` is included. Verified
property 3 catches a mutation to it. The ledger's "each anchor is
content-bound" is now fully true (caveat removed).
- **Branch-freshness (stamp).** Added a best-effort,
`origin/main`-guarded check to property 4: if main moved a soundness
path under the branch, the gate asks for a rebase. Skips (never
false-fails) when `origin/main` is absent.
- **#560 → #624.** The stub row cites #624; #560 is *variable-string
wasm ops*, unrelated. No live doc still mis-tracks it.
## A gate bug that running (not reading) caught
`pinned_row_pins` matched the status word *anywhere* in a row, so the
prose "the row moves `residual (pinned)` → `loud-fail`" made the gate
think the now-`loud-fail` row was still pinned. Fixed to match the
**status cell** (`| \`status\``). This is the kind of thing only
surfaces by executing the gate.
## Verification (all run)
- `dune build` + `dune runtest` green — **534 tests**.
- All 5 gate properties green; 3 sibling gates green.
- Self-tests red as expected: property 3 on a fixture mutation **and**
on a suite-file mutation; the XPASS→ledger-update flip.
## Not done — and why
**#623** (interpreter non-tail resume, `5` not `105`) is left for
owner-steer: it needs a CPS/delimited-continuation rewrite of
`Interp.eval` (blocked on OCaml 4.14 + the jsoo constraint) — exactly
the architecture-level change the soundness handoff says not to start
silently. Its xfail pin stays live (`XFAIL-OK`). Say the word if you
want me to scope it (or do a narrower "fail loud on non-tail resume"
interim).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa
---
_Generated by [Claude
Code](https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa)_
Co-authored-by: Claude <noreply@anthropic.com>
0 commit comments