docs(interp): CESK port plan for #623 + formal: Rows.v record-row scaffold by hyperpolymath · Pull Request #639 · hyperpolymath/affinescript

hyperpolymath · 2026-06-21T17:38:27Z

What

Two forward-looking artifacts: the engineering plan to close the last silent
soundness hole (#623), and the proof scaffold for the easiest-to-pursue
substructural obligation (record rows).

1. `docs/INTERP-CESK-PORT.adoc` — interpreter CESK port plan (closes #623)

The staged plan to port the production tree-walking interpreter
(lib/interp.ml) onto a CESK abstract machine with reified, defunctionalised
continuations, so resume re-enters the handled computation instead of merely
returning a value. This closes the residual (pinned) row on the soundness
ledger — interpreter non-tail single-shot resume (the 5-not-105 shape), the
one genuinely-still-silent hole in the language — and delivers ADR-0025 M2
for the real interpreter surface.

Grounded in the actual code:

Target: lib/interp.ml — a Result-monad tree-walker whose perform =
Error (PerformEffect …) unwinds and discards the OCaml continuation, so
resume structurally cannot re-enter the body.
Proven template: lib/solo_cesk.ml — the M1 Solo-core machine that
already implements deep handlers + multi-shot + non-tail resume with a
defunctionalised (data, not host-closure) continuation, hence
js_of_ocaml/OCaml-4.14-compatible.
Why not OCaml 5 effects: jsoo + 4.14 pin; a defunctionalised kont needs
no runtime support.

Staged M2-0 → M2-4 behind a differential oracle so dune runtest stays
green at every step; §5 enumerates the exact ledger flips — the xfail pin
test_resume_nontail_xfail goes XFAIL → XPASS, which (per the Pinned-residual
discipline) is the trigger to promote the pin and move the ledger row
residual (pinned) → fixed. The content-bound/stamped soundness gate couples
the ledger edit to the test flip in one PR.

2. `formal/Rows.v` — record-row soundness scaffold (W0 seed)

Progress + preservation for STLC + extensible records (empty / extend /
select / restrict over a lacks-checked row). Modeled on P2_Stlc.v
(funext-free; the Software-Foundations Records.v list-encoding so no
mutual-induction scheme is needed), with the obligation stated via a local
mirror of the Siblings_Stated.v parametric-Prop pattern and discharged for
the concrete model. Rung W0 (monomorphic records); row-variable
polymorphism is the named W1 next rung.

⚠️ Rows.v is UNVERIFIED in this environment. No Coq toolchain
(coqc/rocq) is available in this container, so the file is not wired
into formal/_CoqProject and not in formal/justfile's check list — it
cannot affect dune build or the formal check. The proofs are complete
attempts in the proven idiom, not a machine-checked result. The file's
banner lists the owner's wire-in gate: coqc-clean, Print Assumptions
closed (no axioms / Admitted), add to _CoqProject + README.adoc, and
lift the statement into Siblings_Stated.v (e.g. as P-11). Same transparency
discipline as the earlier ocamlformat flag — flagging what I could not run.

Discoverability (ungated)

NAVIGATION.adoc and ADR-0025 now link the port plan. SOUNDNESS.adoc was
deliberately not touched, so its content-bound + stamp-fresh gate is
unaffected.

Verification (run locally)

dune build — clean (exit 0).
tools/check-soundness-ledger.sh — passes (all 5 properties: anchors +
back-links + content-bound + stamp-fresh + pins live).
xfail harness — XFAIL-OK on the tracking: interpreter non-tail single-shot resume returns the resumed value (shallow continuation) — needs delimited-continuation/CPS rewrite #623 pin, FENCE-OK on tracking: Lean and Why3 (experimental) backends drop return control flow — early returns silently mis-emitted #624 (unchanged:
this PR is the plan + scaffold, not the fix itself).
Rows.v un-wiring confirmed: absent from _CoqProject and the justfile
check list; no CI lint scans formal/*.v for membership.

Not in scope

The interpreter port itself (this is the plan; implementation is M2-0…M2-4).
Backend effect lowering stays loud-fail (ADR-0025 — wasm cannot express
reified continuations).
Claiming Rows.v as a discharged obligation — it is an unverified seed
until the owner coqcs and wires it.

🤖 Generated with Claude Code

Generated by Claude Code

…ffold Two forward-looking artifacts toward the substructural-typing proof and the last silent soundness hole. 1. docs/INTERP-CESK-PORT.adoc — the staged engineering plan to port the production tree-walking interpreter (lib/interp.ml) onto a CESK abstract machine with reified, defunctionalised continuations, closing the #623 non-tail single-shot resume residual (the `5`-not-`105` shape; the one genuinely-still-silent row on the soundness ledger). Grounded in the real code: interp.ml (the Result-monad tree-walker whose `perform` discards the OCaml continuation), value.ml (the value/error domain), and the proven template lib/solo_cesk.ml (M1 Solo-core machine: deep handlers, multi-shot, non-tail resume, jsoo-compatible). Delivers ADR-0025 M2 for the real surface. Staged M2-0..M2-4 with a differential oracle so `dune runtest` stays green at every step; §5 enumerates the exact ledger flips (the xfail pin test_resume_nontail_xfail XFAIL->XPASS) that the gate couples to the fix. 2. formal/Rows.v — proof scaffold for record-row soundness (progress + preservation for STLC + extensible records: empty/extend/select/restrict over a lacks-checked row). Modeled on P2_Stlc.v conventions (funext-free, the Software-Foundations Records list-encoding), stated via a local mirror of the Siblings_Stated parametric-Prop pattern and discharged for the concrete model. Rung W0 (monomorphic records); row-variable polymorphism is the named W1 next rung. HONESTY CAVEAT: Rows.v is UNVERIFIED in this environment — no Coq toolchain (coqc/rocq) is available here, so it is NOT wired into formal/_CoqProject and NOT in formal/justfile's `check` list, and cannot affect `dune build` or the formal check. The proofs are complete attempts in the proven idiom, not a machine-checked result. The file's banner lists the owner's wire-in gate: coqc-clean, Print Assumptions closed, add to _CoqProject + README, and lift the statement into Siblings_Stated.v. Plus discoverability cross-links (ungated; SOUNDNESS.adoc deliberately untouched so its content-bound/stamped gate is unaffected): NAVIGATION.adoc and ADR-0025 now point to the port plan. Verified locally: `dune build` clean; tools/check-soundness-ledger.sh passes (all 5 properties); xfail harness reports XFAIL-OK on the #623 pin and FENCE-OK on #624 (unchanged — these are plans/scaffold, not the fix itself). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa

github-actions · 2026-06-21T17:39:25Z

🔍 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

…tcher) .hypatia-ignore matches `${rule}:${path}` as fixed-string whole-line equality (grep -qxF), not a glob — so each formal/*.v needs its own two lines. The new Rows.v scaffold is a Coq proof script like its 16 siblings; add the same vlang_detected + banned_language_file exemptions so a sweep cannot mis-flag it as V-lang. (Rows.v stays un-wired from _CoqProject — the exemption is about the file in the tree, independent of the build graph.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa

github-actions · 2026-06-21T17:41:27Z

🔍 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

## What `Rows.v` (P-11, record-row soundness) landed in #639 as an **explicitly-unverified scaffold** — the authoring container had no Coq toolchain, so it shipped un-wired with a loud UNVERIFIED banner. This PR closes that loop: I installed **Coq 8.18.0 (OCaml 4.14.1 — the repo's pinned toolchain)** and verified it. ``` coqc -Q . ASFormal Rows.v → clean Print Assumptions progress / preservation → "Closed under the global context" ``` The hand-written proofs compiled **first try**, axiom-free, no `Admitted`. So the scaffold is promoted to a real, wired obligation. ## Changes - **`formal/_CoqProject` + `formal/justfile` `check`**: add `Rows` (the recipe fails on any axiom/`Admitted`, so this now gates `Rows` too). - **`formal/Rows.v`**: UNVERIFIED banner → verified/wired note; dropped the stale "Target:" / "lift into Siblings_Stated" wording. - **`formal/README.adoc`**: contents-table row + a "Record rows (P-11)" prose section. - **`docs/PROOF-NEEDS.adoc`**: new **P-11** obligation row (`mechanized`); refreshed Coq-core counts to **18 files / 31 `Print Assumptions` reports** (also fixes the long-stale "13 files" intro line). - **`.hypatia-ignore`**: de-stale the `Rows.v` comment (now mechanized + wired). ## Verification (run in this environment) - Full track re-compiled end to end via the justfile check list: **18 files, 31 closure reports, zero axioms**. - `Rows.v` re-verified standalone after the comment edits. - `dune build` clean; `tools/check-soundness-ledger.sh` green (`SOUNDNESS.adoc` untouched). ## Scope Unchanged from #639: **Wave W0** (monomorphic extensible records — empty/extend/select/restrict over a `lacks`-checked row). Row-*variable* polymorphism (true row polymorphism) is the **W1** increment, noted on the P-11 row as the next rung. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- _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 17:40

hyperpolymath merged commit 41dfce9 into main Jun 21, 2026
13 checks passed

hyperpolymath deleted the claude/interp-port-and-rows-scaffold branch June 21, 2026 17:40

hyperpolymath mentioned this pull request Jun 21, 2026

feat(formal): verify + wire Rows.v (P-11 record-row soundness) #648

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

docs(interp): CESK port plan for #623 + formal: Rows.v record-row scaffold#639

docs(interp): CESK port plan for #623 + formal: Rows.v record-row scaffold#639
hyperpolymath merged 2 commits into
mainfrom
claude/interp-port-and-rows-scaffold

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

What

1. docs/INTERP-CESK-PORT.adoc — interpreter CESK port plan (closes #623)

2. formal/Rows.v — record-row soundness scaffold (W0 seed)

Discoverability (ungated)

Verification (run locally)

Not in scope

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

1. `docs/INTERP-CESK-PORT.adoc` — interpreter CESK port plan (closes #623)

2. `formal/Rows.v` — record-row soundness scaffold (W0 seed)