Skip to content

feat(borrow): CFG-join for ExprHandle + ExprTry catch arms (CORE-01 pt3 Slice C-light, Refs #177)#358

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/bold-brahmagupta-0T7Bh
May 25, 2026
Merged

feat(borrow): CFG-join for ExprHandle + ExprTry catch arms (CORE-01 pt3 Slice C-light, Refs #177)#358
hyperpolymath merged 1 commit into
mainfrom
claude/bold-brahmagupta-0T7Bh

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

CORE-01 Phase 3 Slice C-light — CFG-join semantics for ExprHandle handler arms and ExprTry catch arms. Both were previously checked sequentially against a shared state, so moves/borrows from arm i polluted the state seen by arm i+1 — even though only one arm runs at runtime. This PR mirrors the snapshot-restore-merge pattern that ExprMatch already does inline, and factors the merge logic into a merge_arm_results helper that all CFG-join sites can share.

Before (sequential)

fn catch_arm_isolation() -> Unit {
  let y = 100;
  try { 0 } catch {
    0 => drop_int(y),
    1 => drop_int(y),     // ← spurious UseAfterMove: arm 0 polluted state.moved
    _ => ()
  }
}

After (isolated)

Each arm runs against the post-body state independently; the merge takes intersection of borrows and union of moves.

Mechanics

New helper near check_expr in lib/borrow.ml:

val merge_arm_results :
  state -> borrow list -> move_record list ->
  (unit result * borrow list * move_record list) list ->
  unit result
  • Errors: propagates the first error seen.
  • Borrows: intersection across arms (branch-local borrows die at arm-block exit anyway; this just formalises the join).
  • Moves: union across arms, deduplicated against the base — a place is moved post-join if any arm moved it (conservative-sound).

Wired into ExprHandle and ExprTry. ExprMatch's inlined logic is deliberately untouched — same semantics, but PR-scope discipline says don't refactor a stable code path here.

For ExprTry: check_block(body) runs first (its block-local borrows are cleaned at block exit; moves persist). The snapshot is taken after check_block, so catch arms see the body's moves in base_moved. The merge's dedupe-against-base preserves them through the join. finally runs deterministically after the merge.

Tests (E2E Borrow Graph, +2)

Fixture Direction Expected
slice_c_catch_arm_isolation.affine positive Ok — two arms independently move y, currently rejected with spurious UseAfterMove
slice_c_body_move_persists.affine anti-regression UseAfterMove on read_int(y) after the body moved y, even with a _ => catch arm

Scope of this PR

ExprHandle is implemented in parallel but has no dedicated test fixture — the AffineScript test corpus has no live handle expressions outside the parser's grammar tests, so an end-to-end borrow-graph fixture for it would be the first. The code path is exercised whenever a real handle appears; until then, soundness is by symmetry with ExprTry.

Deferred (Slices C-full / C' / D):

  • Slice C-full — true Polonius origin/region variables on TyRef/TyMut with subset constraints + datalog-style loan-live-at-point solver. Architectural change to the type system; ADR-gated.
  • Slice C' — loop soundness via a 2-iteration check on StmtWhile/StmtFor. Coupled to a StmtAssign clear-on-rewrite fix (assignment is currently treated as a read of LHS, so the naive 2-iter spuriously fails on legitimate re-assignment loops).
  • Ref-to-ref bindingr = some_other_ref_var (RHS not a direct &place) still leaves the ref-binding stale. Symmetric let/assign limitation.
  • Slice D — tighter quantity-checker integration for captured linears.

Docs

  • STATE.a2ml borrow-checkerphase-3-parts-1-3-Slices-A-B-C-light-landed
  • CAPABILITY-MATRIX.adoc borrow-checker row records Slice C-light
  • TECH-DEBT-alt.adoc CORE-01 row narrows residual to C-full / C' / D + ref-to-ref binding

Test plan

  • CI build (opam exec -- dune build) green
  • CI Run tests (opam exec -- dune runtest) — E2E Borrow Graph count +2
  • Existing try_catch_* / try_finally fixtures (single-arm Int expressions, no move/borrow) untouched

Local-build caveat: container has no OCaml toolchain; CI is the source of truth.

Refs #177


Generated by Claude Code

@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 112 issues detected

Severity Count
🔴 Critical 15
🟠 High 47
🟡 Medium 50

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
    "type": "banned",
    "file": "AI.a2ml",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Superseded by 0-AI-MANIFEST.a2ml",
    "type": "banned",
    "file": "AI.djot",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "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": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/example/smoke_driver.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/cli.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/compile.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/runner.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath force-pushed the claude/bold-brahmagupta-0T7Bh branch from 31397e1 to 9ff097f Compare May 25, 2026 22:44
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 108 issues detected

Severity Count
🔴 Critical 15
🟠 High 49
🟡 Medium 44

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
    "type": "banned",
    "file": "AI.a2ml",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Superseded by 0-AI-MANIFEST.a2ml",
    "type": "banned",
    "file": "AI.djot",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "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": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/example/smoke_driver.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/cli.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/compile.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/runner.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath enabled auto-merge (squash) May 25, 2026 22:46
@hyperpolymath hyperpolymath force-pushed the claude/bold-brahmagupta-0T7Bh branch from 9ff097f to 56a251b Compare May 25, 2026 23:36
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 108 issues detected

Severity Count
🔴 Critical 15
🟠 High 48
🟡 Medium 45

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
    "type": "banned",
    "file": "AI.a2ml",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Superseded by 0-AI-MANIFEST.a2ml",
    "type": "banned",
    "file": "AI.djot",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "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": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/example/smoke_driver.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/cli.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/compile.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/runner.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…t3 Slice C-light, Refs #177)

Until now, `ExprHandle` handler arms and `ExprTry` catch arms were
checked *sequentially* against a shared state — so moves and
borrows from arm i polluted the state seen by arm i+1, even though
only one arm runs at runtime.  This produced spurious UseAfterMove
on the second of two catch arms that independently move the same
value, etc.

Slice C-light closes this for handlers and try/catch by mirroring
the snapshot-restore-merge pattern that `ExprMatch` already does
inline.  The merge logic — intersection-on-borrows, union-on-
moves, first-error propagation, dedupe against the base — is now
factored into a single helper, `merge_arm_results`, so all CFG-
join sites agree on "what state survives the join":

- Errors: propagate the first error seen, left-to-right.
- Borrows: intersection across arms (a borrow survives the join
  only if it survived every arm; branch-local borrows naturally
  die at arm exit via `check_block`'s borrows_at_entry restore).
- Moves: union across arms, deduplicated against the base — a
  place is reported as moved post-join if any arm moved it
  (conservative-sound).

`ExprMatch`'s inlined logic is *deliberately left untouched* — same
semantics as the new helper, but its tests have been stable since
PR #240; refactoring it would add risk without ergonomic upside
on this PR.  A future cleanup can converge them.

ExprHandle (`handle body { return(_) => ..., op(p1, p2) => ... }`):
mutually exclusive continuations dispatched on whether the body
returned normally or performed an effect-op.  Body runs against
the current state, then each arm runs against the post-body state
independently via the helper.

ExprTry (`try { body } catch { p => arm; ... } finally { ... }`):
body runs first via `check_block` (so its block-local borrows are
cleaned at block exit; its moves persist).  The snapshot is taken
*after* check_block — so the catch arms run against a state that
already includes the body's moves (conservatively assuming body
might have moved before throwing).  Catch arms merge via the
helper; `finally` then runs deterministically against the merged
post-catch state.

Tests (E2E Borrow Graph, +2):

- `slice_c_catch_arm_isolation.affine` (positive): three catch
  arms, two of which independently `drop_int(y)`.  Pre-Slice-C
  this was rejected — arm 2's `drop_int(y)` saw arm 1's move and
  fired UseAfterMove.  Post-Slice-C every arm starts from the
  post-body state and succeeds independently.

- `slice_c_body_move_persists.affine` (anti-regression): the
  try-body moves `y`; the catch arm matches `_` and ignores `y`;
  after the `try`, a `read_int(y)` must still fail
  UseAfterMove because the body might have moved before throwing.
  This pins that the helper's dedupe-against-base correctly
  preserves body-side moves through the merge.  The current
  `state.moved` propagation does this for free (the snapshot
  *captures* body's moves into base_moved, and the merge sets
  `state.moved <- base_moved @ unique_new`), but the test pins
  the invariant so a future refactor cannot drop it.

ExprHandle is implemented in parallel but has no dedicated test
fixture: the AffineScript test corpus has no live `handle`
expressions outside the parser's own grammar tests, so an
end-to-end borrow-graph fixture for it would be the first.  The
code path is exercised whenever a real `handle` appears; until
then, soundness is by symmetry-with-ExprTry.

Anti-regression sweep: all existing borrow / linear-arrow /
quantity fixtures audited.  The `try_catch_*` and `try_finally`
fixtures already in the gate (e/Try semantics smoke tests) are
single-arm and don't touch moves, so they go through the new path
unchanged.  Move-or-borrow scenarios crossing `ExprHandle`/
`ExprTry` are net-new fixtures here.

Docs updated:
- `STATE.a2ml` borrow-checker → "phase-3-parts-1-3-Slices-A-B-C-light-landed"
- `CAPABILITY-MATRIX.adoc` borrow-checker row records Slice C-light
- `TECH-DEBT-alt.adoc` CORE-01 row narrows residual to
  C-full (origin variables, ADR-gated), C' (loop soundness),
  D (quantity integration), plus ref-to-ref binding.

NOTE: container has no OCaml toolchain; `dune build` / `dune runtest`
not run locally. CI is the source of truth.  Mechanically scoped to
two arms of `check_expr` plus one new helper.
@hyperpolymath hyperpolymath force-pushed the claude/bold-brahmagupta-0T7Bh branch from 56a251b to 770be85 Compare May 25, 2026 23:45
@hyperpolymath hyperpolymath merged commit 4b83c1a into main May 25, 2026
14 of 17 checks passed
@hyperpolymath hyperpolymath deleted the claude/bold-brahmagupta-0T7Bh branch May 25, 2026 23:45
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 103 issues detected

Severity Count
🔴 Critical 15
🟠 High 42
🟡 Medium 46

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "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": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/example/smoke_driver.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/cli.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/compile.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/runner.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-deno-test/lib/discover.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/affinescript/affinescript/packages/affine-js/types.d.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants