feat(formal): F-5 render non-collision + real-lift R0 (RealWasm + plan) by hyperpolymath · Pull Request #638 · hyperpolymath/affinescript

hyperpolymath · 2026-06-21T16:48:13Z

Two formal-track deliverables on the shared dev branch (the one-branch policy keeps both here; happy to split if you'd rather review them separately).

Commit 1 — F-5: `render_ty` per-face renaming is injective (no collision)

Mechanizes F-5 (docs/PROOF-NEEDS.adoc). lib/face.ml's render_ty rewrites a fixed type-name vocabulary per face — Unit, Bool, Option[_]. F-5 asks whether that ever collapses two distinct canonical types onto one displayed string — pointedly, Js renders Unit as "null" and Option[T] as "T | null", sharing the "null" lexeme.

formal/F5_RenderFaithful.v models the vocabulary (cty), the displayed lexemes (name), and the rendered form (rty), mirroring render_ty as render : face → cty → rty. Faithful to the whole-string Unit/Bool match and the canonical-inner Option rewrite (Js Option[Option[Int]] ⇒ "Option[Int] | null").

render_inj — every face's renaming is injective (the non-collapse guarantee).
js_no_collapse / cafe_no_collapse / option_never_atom — Unit and Option[T] never read as one type despite the shared "null"/"?" lexeme.

Status: F-5 absent → partial.

Commit 2 — Real-lift R0: `RealWasm.v` + `REAL-LIFT.adoc`

Begins PROOF-NEEDS §6 Wave 3 — replacing the toy models with the real AST + real typed-WASM semantics.

formal/REAL-LIFT.adoc — the engineering plan, grounded in lib/ast.ml (the real ~30-constructor expr) and lib/wasm.ml (the real WebAssembly-1.0 IR). Coq module structure (RealWasm/RealWasmSem/RealAst/RealAstSem/RealCompile/RealPreservation) and a strict-superset fragment ladder R0→R1→R2→R-mem→R-float→R-str→R-call→R-wrap→R-eff, each axiom-free before the next, with the strategy for each hard part (loops/termination via fuel, linear memory, abstract floats, the post-typecheck elaboration nodes, effects gated on tracking: general effect-handler dispatch (post-CORE-02 residual) — silent arm-drop on 3 backends; DECISION: back-port loud failure now? #555).
formal/RealWasm.v — R0, the first stone. Re-targets the actual lib/wasm.ml instr/value_type names (vs the toy K-1's ad-hoc machine) for the pure i32 numeric core: stack-machine wexec, arity checker wcheck, and wexec_sound — arity-checked code never gets stuck, the target-side invariant the real K-1 rests on. i32 ≔ Z (wrap deferred to rung R-wrap).

This concretely settles the "real lift" framing from the gap analysis: it's a milestone ladder, not one monolith, and R0 is landed. R1 (real RealAst/RealAstSem/RealCompile for the int/bool/let fragment → first real ⟦compile p⟧ = ⟦p⟧) is next.

All proofs axiom-free. formal/ now 16 files, 27 Print Assumptions closure reports (verified: full dep-order recompile, no Axioms:). Wired into _CoqProject / justfile / .hypatia-ignore / README.adoc; PROOF-NEEDS.adoc updated (F-5 row, K-1 row, §6 Waves 1 & 3).

🤖 Generated with Claude Code

https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

… collision) Mechanizes F-5 (docs/PROOF-NEEDS.adoc): lib/face.ml's render_ty rewrites a fixed type-name vocabulary per face (Unit, Bool, Option[_]); F-5 asks whether that renaming ever collapses two distinct canonical types onto one displayed string — pointedly, Js renders Unit as "null" and Option[T] as "T | null", sharing the "null" lexeme. F5_RenderFaithful.v models the canonical-type vocabulary (cty), the displayed lexemes (name, distinct constructors), and the rendered form (rty), then mirrors render_ty as render : face -> cty -> rty. Faithful to two OCaml details: Unit/Bool are special-cased only at the whole-type level, and Option's inner is rendered canonically (the global_replace captures the canonical substring), so e.g. Js Option[Option[Int]] => "Option[Int] | null". Theorems (axiom-free): canon_inj; render_inj (every face's renaming injective — the non-collapse guarantee); js_no_collapse / cafe_no_collapse / option_never_atom (Unit and Option never read as one type despite the shared null/? lexeme). Wired into _CoqProject / justfile / .hypatia-ignore / README.adoc. PROOF-NEEDS.adoc: F-5 absent -> partial; section 6 Wave 1 leftover cleared; formal/ now 15 files, 26 axiom-free closure reports. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

github-actions · 2026-06-21T16:49:18Z

🔍 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

Begins the "real lift" (PROOF-NEEDS.adoc section 6 Wave 3): replacing the toy proof models with the real AffineScript AST + real typed-WASM semantics. - formal/REAL-LIFT.adoc: the engineering plan, grounded in lib/ast.ml (the real ~30-constructor expr) and lib/wasm.ml (the real WebAssembly-1.0 IR). Defines the Coq module structure (RealWasm / RealWasmSem / RealAst / RealAstSem / RealCompile / RealPreservation) and a strict-superset fragment ladder R0->R1->R2->R-mem->R-float->R-str->R-call->R-wrap->R-eff, each axiom-free before the next, with the strategy for each hard part (loops/termination via fuel, linear memory, abstract floats, the post-typecheck elaboration nodes, effects gated on #555). - formal/RealWasm.v: R0, the first stone. Re-targets the ACTUAL lib/wasm.ml instr/value_type names (vs the toy K-1's ad-hoc machine) for the pure i32 numeric core, with a stack-machine wexec, an arity checker wcheck, and wexec_sound: arity-checked code never gets stuck — the target-side invariant the real K-1 preservation proof rests on. i32 modelled as Z (wrap deferred to rung R-wrap). Axiom-free. Wired into _CoqProject / justfile / .hypatia-ignore / README.adoc. PROOF-NEEDS.adoc: K-1 row + section 6 Wave 3 note R0 landed; formal/ now 16 files, 27 axiom-free closure reports. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

github-actions · 2026-06-21T17:06:28Z

🔍 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

…e.v) (#640) ## What Climbs the **REAL-LIFT ladder** (`formal/REAL-LIFT.adoc`) from **R0 → R1**: the **first mechanized `⟦compile p⟧ = ⟦p⟧` on the *real* objects** — the actual `lib/wasm.ml` instruction IR and the real (resolved) `lib/ast.ml` expression core. This **retires the toy `K1`/`K1Let` on real objects**. ## `RealWasm.v` (grown for R1) Adds **locals** (`LocalGet`/`LocalSet`) and the comparison ops `I32Eq`/`I32LtS`, threading a mutable locals store through `wexec`. `wexec` is refactored through a per-instruction `step1`, so the sequencing lemmas `wexec_app` / `wexec_seq` (which the preservation proof composes with) are one line each. `wexec_sound` (R0) is retained for the pure (`no_local`) fragment. ## `RealCompile.v` (new, R1) - **`rexpr`** — the resolved int/bool/`let`/binary core of `lib/ast.ml` (de Bruijn **levels**; name resolution is a separate obligation, P-7; bool ≔ 0/1, int ≔ Z, so one observable); - **`eval`** — the reference dynamic semantics (mirrors `lib/interp.ml`); - **`compile`** — lowers `let` to `LocalSet d` into a pre-sized locals array (slot = binding depth `d`; siblings reuse slots), mirroring `lib/codegen.ml`; - **`compile_correct`** — the theorem: ```coq eval env e = Some v → agree env locals → |env| = d → d + depth e ≤ |locals| → ∃ locals', wexec (compile d e) locals st = Some (locals', v :: st) ∧ |locals'| = |locals| ∧ (∀ i < d, nth_error locals' i = nth_error locals i) ``` carrying an **env↔locals agreement** invariant with **fresh-slot allocation** and **low-slot preservation** through the induction (the genuine compiler-correctness simulation); - **`compile_program_correct`** — runs a closed program from the zero-initialised locals array. Concrete end-to-end check (`let x = 2+3 in x*4 ⇒ 20`): `r1_eval_demo` (source) and `r1_exec_demo` (`compile` then `wexec` ⇒ `[20]`). ## Honest scope R1 is the int/bool/`let`/binop fragment on de Bruijn-resolved source; `LocalTee`/i64, structured control, memory, floats, calls, and effects are later rungs (`REAL-LIFT.adoc` §4). **R2** (structured control on a fuel-indexed `wexec`) is next, and is the rung that **settles #601 concretely**. ## Verification All axiom-free — every `Print Assumptions` reports *Closed under the global context*. `formal/` now **17 files, 29 closure reports** (full dep-order recompile, no `Axioms:`). Wired into `_CoqProject` / `justfile` / `.hypatia-ignore`; `README.adoc`, `REAL-LIFT.adoc` (R1 landed, R2 next), and `PROOF-NEEDS.adoc` (K-1 row, §1, §6 Wave 3) updated. Follow-on to #638 (R0 + plan, merged). `QTT-dynamic #637 ✅ → F-5 + R0 #638 ✅ → **R1 (this)**`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- _Generated by [Claude Code](https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr)_ Co-authored-by: hyperpolymath <paraordinate@yahoo.co.uk> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

hyperpolymath changed the title ~~feat(formal): F-5 — render_ty per-face type renaming is injective (no collision)~~ feat(formal): F-5 render non-collision + real-lift R0 (RealWasm + plan) Jun 21, 2026

hyperpolymath marked this pull request as ready for review June 21, 2026 17:04

hyperpolymath merged commit 1eaff91 into main Jun 21, 2026

hyperpolymath deleted the claude/lucid-cray-4a22dp branch June 21, 2026 17:05

hyperpolymath mentioned this pull request Jun 21, 2026

feat(formal): real-lift R1 — first real ⟦compile p⟧ = ⟦p⟧ (RealCompile.v) #640

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(formal): F-5 render non-collision + real-lift R0 (RealWasm + plan)#638

feat(formal): F-5 render non-collision + real-lift R0 (RealWasm + plan)#638
hyperpolymath merged 2 commits into
mainfrom
claude/lucid-cray-4a22dp

hyperpolymath commented Jun 21, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 21, 2026

Uh oh!

github-actions Bot commented Jun 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented Jun 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Commit 1 — F-5: render_ty per-face renaming is injective (no collision)

Commit 2 — Real-lift R0: RealWasm.v + REAL-LIFT.adoc

Uh oh!

github-actions Bot commented Jun 21, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 21, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

hyperpolymath commented Jun 21, 2026 •

edited

Loading

Commit 1 — F-5: `render_ty` per-face renaming is injective (no collision)

Commit 2 — Real-lift R0: `RealWasm.v` + `REAL-LIFT.adoc`