fix(#624): fence Lean/Why3 on early `return`; finish the soundness-gate small calls by hyperpolymath · Pull Request #633 · hyperpolymath/affinescript

hyperpolymath · 2026-06-21T14:12:21Z

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):

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".
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.
codegen wall 1: variable-string wasm backend ops (String.length / indexing / startsWith / fromCharCode) #560 → tracking: Lean and Why3 (experimental) backends drop return control flow — early returns silently mis-emitted #624. The stub row cites tracking: Lean and Why3 (experimental) backends drop return control flow — early returns silently mis-emitted #624; codegen wall 1: variable-string wasm backend ops (String.length / indexing / startsWith / fromCharCode) #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.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa

Generated by Claude Code

github-actions · 2026-06-21T14:13:23Z

🔍 Hypatia Security Scan

Findings: 41 issues detected

Severity	Count
🔴 Critical	2
🟠 High	23
🟡 Medium	16

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action denoland/setup-deno@v2 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (32 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (29 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (3 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/ffi.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

The experimental Lean/Why3 emitters silently dropped early `return` statements (gen_block skipped them, lowering `fn f(){ return 1; … }` to `:= ()`). Add an Ast.fn_body_contains_return fence so codegen_lean/codegen_why3 return Error instead. The hole moves residual(pinned) -> loud-fail; the xfail pin flipped to XPASS (verified by running the harness) and is converted to a positive fence-check (test_stub_backend_return_fenced). Also (the "small calls"): - Content-bind suite-file anchors too (whole-file hash) — the manifest now seals test/test_borrow_polonius.ml; verified property 3 catches a mutation to it. Ledger's "each anchor content-bound" claim is now fully true. - Add a best-effort branch-freshness check to property 4 (origin/main-guarded): if main moved a soundness path under the branch, the gate asks for a rebase. - Fix a gate false-positive: pinned_row_pins now matches the STATUS CELL, not a prose mention of the status word (caught by running the gate, not eyeballing). - #555-stub row cites #624 (not #560 — that's variable-string wasm ops). Verified: dune build + dune runtest green (534 tests); all 5 gate properties + the three sibling gates green; self-tests for content-binding (incl. suite) red as expected. #623 (interp non-tail resume) left for owner-steer — it needs a CPS rewrite of eval, not a small fix. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa

github-actions · 2026-06-21T14:17:12Z

🔍 Hypatia Security Scan

Findings: 41 issues detected

Severity	Count
🔴 Critical	2
🟠 High	23
🟡 Medium	16

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action denoland/setup-deno@v2 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (32 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (29 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (3 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/ffi.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…ain) (#635) Greens `main`, which #633 left red. ## Root cause The soundness gate's property 5 ran `dune build test/xfail/test_xfail_pins.exe`. CI reaches dune only via `opam exec -- dune`, not bare `dune` on `PATH`, so this failed with *"ERROR (property 5): cannot build test/xfail/test_xfail_pins.exe"* — and the `build` job exited there (before `@fmt`). It greened locally because my dev box has `dune` at `/usr/bin/dune`; that environment difference is exactly what a local-only run can't catch. ## Fix The harness exe is already built by the `dune build` / `dune runtest` steps that run *before* the gate, so the gate now prefers the **pre-built binary** (`_build/default/...`) and only builds — with whatever dune is available (`dune`, else `opam exec -- dune`) — if it's missing. Fail-closed if it still isn't there. ## Verified (the actual CI condition, not just locally) Built the exe, then ran the gate with `dune`/`opam` removed from `PATH`: ``` dune on restricted PATH? NO OK: soundness ledger — all 5 properties hold (...) rc=0 ``` ## Note #633's `build` died at this gate, so `@fmt` never ran on its `lib/*.ml` edits (the `return`-fence). With the gate fixed, CI here will reach `@fmt`; if it flags those lib edits I'll follow up (I can't run `ocamlformat` in my environment, so I'd apply the diff from the CI log). 🤖 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>

hyperpolymath marked this pull request as ready for review June 21, 2026 14:16

hyperpolymath force-pushed the claude/fence-stub-returns branch from eaa69e9 to 3f16b47 Compare June 21, 2026 14:16

hyperpolymath merged commit f020a6f into main Jun 21, 2026
12 of 13 checks passed

hyperpolymath deleted the claude/fence-stub-returns branch June 21, 2026 14:16

hyperpolymath mentioned this pull request Jun 21, 2026

fix(ci): soundness gate must not assume bare dune on PATH (greens main) #635

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

fix(#624): fence Lean/Why3 on early `return`; finish the soundness-gate small calls#633

fix(#624): fence Lean/Why3 on early `return`; finish the soundness-gate small calls#633
hyperpolymath merged 1 commit into
mainfrom
claude/fence-stub-returns

hyperpolymath commented Jun 21, 2026

Uh oh!

github-actions Bot commented Jun 21, 2026

Uh oh!

Uh oh!

github-actions Bot commented Jun 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 21, 2026

#624 — Lean/Why3 silently drop return → now fail loud

Small calls — done

A gate bug that running (not reading) caught

Verification (all run)

Not done — and why

Uh oh!

github-actions Bot commented Jun 21, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

github-actions Bot commented Jun 21, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

#624 — Lean/Why3 silently drop `return` → now fail loud