Skip to content

test(borrow): #225 PR3b — affine-capture obligation discharged by composition#237

Merged
hyperpolymath merged 1 commit into
mainfrom
stage-c/225-pr3b-affine-capture
May 19, 2026
Merged

test(borrow): #225 PR3b — affine-capture obligation discharged by composition#237
hyperpolymath merged 1 commit into
mainfrom
stage-c/225-pr3b-affine-capture

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

#225 PR 3b — affine-capture obligation discharged by composition

ADR-013 obligation 1 (a linear/owned local captured into the continuation env is consumed exactly once; double-resumption impossible) requires no transform-aware static machinery. Discharged by composition:

  • (a) the borrow checker runs on the straight-line AST before the codegen CPS transform (verified pipeline order in bin/main.ml) — a double consume of an owned local across the async let is rejected there, exactly as in any synchronous body;
  • (b) the PR2 once-resumption trap guarantees the continuation runs at most once, so the transformed code performs each consume the same number of times the checker already verified.

This PR pins (a) with two regressions in test_effects.ml (new frontend_borrow = parse→resolve→typecheck→Borrow.check_program):

  • owned local captured across the async split + consumed twice ⇒ use-after-move, rejected by the existing checker (no new rule);
  • same shape consumed once ⇒ accepted (rule not over-rejecting the captured-once case the transform relies on).

No compiler/codegen change — test-only + in-code rationale (the PR3a recogniser docstring already states the argument). dune test --force 260 (was 258, +2); tools/run_codegen_wasm_tests.sh green (unaffected, confirmed).

Slice 2 of former PR3. Refs #225 #160 (NOT Closes — joint-close is the final #225 PR).

🤖 Generated with Claude Code

…position

ADR-013 obligation 1 (a linear/owned local captured into the
continuation env is consumed exactly once; double-resumption
impossible) requires NO transform-aware static machinery. It is
discharged by composition:

  (a) the borrow checker runs on the straight-line AST BEFORE the
      codegen CPS transform (verified pipeline order, bin/main.ml), so
      a double consume of an owned local across the async let is
      rejected there exactly as in any synchronous body; and
  (b) the PR2 once-resumption trap guarantees the continuation runs at
      most once, so the transformed code performs each consume the
      same number of times the checker already verified.

This commit pins (a) with two regressions in test_effects.ml
(frontend_borrow = parse->resolve->typecheck->Borrow.check_program):
- owned local captured across the async split + consumed TWICE ⇒
  use-after-move, rejected by the existing checker (no new rule);
- the same capture shape consumed ONCE ⇒ accepted (the rule is not
  over-rejecting the captured-once case the transform relies on).

The rationale is documented in-code (test_effects.ml block comment;
the codegen recogniser docstring already states it from PR3a). No
compiler/codegen change. dune test --force 260 (was 258, +2);
tools/run_codegen_wasm_tests.sh green (unaffected, confirmed). Refs
#225 #160
@hyperpolymath hyperpolymath merged commit f61034b into main May 19, 2026
11 of 12 checks passed
@hyperpolymath hyperpolymath deleted the stage-c/225-pr3b-affine-capture branch May 19, 2026 08:17
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 44 issues detected

Severity Count
🔴 Critical 12
🟠 High 21
🟡 Medium 11

⚠️ 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": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "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": "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 added a commit that referenced this pull request May 19, 2026
…lete)

Both targets of the portable Http primitive are green:
- Deno-ESM #160 — PR #226 (shipped).
- typed-wasm #225 — the ADR-013 CPS line PR1..PR3d all merged:
  #227 (PR1 verified Thenable foundation), #233 (PR2 base case),
  #236 (PR3a env capture), #237 (PR3b affine-capture obligation),
  #238 (PR3c Async→Async chaining), #266 (PR3d typed Response reader
  + http_fetch-parity wasm e2e).

The transparent `fetch/get -> Response` source surface is delivered on
both targets; ADR-013's delivery plan is complete. Ledger STDLIB-01 +
the ADR-013 delivery plan truthed. Two follow-ups remain independently
tracked (NOT part of this slice): effect-threaded boundary
generalisation #234; estate-wide #199/#205 re-validation #235.

Gate: `dune test --force` 278/278 (docs only; zero regression).

Closes #160
Closes #225
hyperpolymath added a commit that referenced this pull request May 19, 2026
…lete) (#268)

Both targets of the portable Http primitive are green:
- Deno-ESM #160 — PR #226 (shipped).
- typed-wasm #225 — the ADR-013 CPS line PR1..PR3d all merged:
  #227 (PR1 verified Thenable foundation), #233 (PR2 base case),
  #236 (PR3a env capture), #237 (PR3b affine-capture obligation),
  #238 (PR3c Async→Async chaining), #266 (PR3d typed Response reader
  + http_fetch-parity wasm e2e).

The transparent `fetch/get -> Response` source surface is delivered on
both targets; ADR-013's delivery plan is complete. Ledger STDLIB-01 +
the ADR-013 delivery plan truthed. Two follow-ups remain independently
tracked (NOT part of this slice): effect-threaded boundary
generalisation #234; estate-wide #199/#205 re-validation #235.

Gate: `dune test --force` 278/278 (docs only; zero regression).

Closes #160
Closes #225
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.

1 participant