feat(formal): F-1 preservation + grow K-1 (let/vars) + state P-2/P-3/F-3/F-4

[hyperpolymath]

What

Continues the formal/ Wave-0 programme in the order you gave — 3 → 1 → 2 (F-1, then grow K-1, then state the siblings). All Coq/Rocq 8.18, all axiom-free (Print Assumptions → "Closed under the global context"); no Admitted.

3 — F-1 (F1_TransformerPreservation.v, mechanized)

The real same-cube theorem, composing on K-1: models a face surface fexp + parser sugar, the transform elaborate : fexp → sexp (ADR-010's T_F), and the face's own semantics feval. Proves the transform preserves meaning —

Theorem f1_transform_preserves_eval : forall f, feval f = seval (elaborate f).

— then chains K-1's k1_preservation_holds for end-to-end codegen preservation (f1_codegen_preservation), plus a cross-face same-cube corollary (faces landing on the same canonical AST emit identical code). The observational trailing-statement/tail split stays in invariant-path/proofs/SameCube.agda (F-2).

1 — grow K-1 (K1Let_CodegenPreservation.v, mechanized)

Re-proves codegen preservation for a richer fragment: de Bruijn variables, let, and an environment. The target machine gains a locals register, and compilation balances IBind/IUnbind so locals scope correctly. (if/structured control is the next increment — it needs a target control construct + a termination measure.)

2 — state the siblings (Siblings_Stated.v, statements only)

P-2 (progress + preservation), P-3 (borrow soundness + the explicit "reject #554" obligation), F-3 (pragma locality + alias-table functionality), F-4 (error-vocabulary faithfulness as a class/referent simulation). Each is a Definition ..._statement : Prop over Section Variables, discharged at End into closed, universally-quantified props — the Coq analogue of solo-core's statement-only skeleton. Nothing is claimed proven, and there are no axioms/Parameters.

Wiring & docs

• justfile check compiles all four in dependency order (F-1 Requires K-1) and asserts no axioms; _CoqProject + README.adoc updated.
• .hypatia-ignore extends the Coq-.v-is-not-V-lang carve-out to the three new files.
• PROOF-NEEDS.adoc: F-1 absent → partial, F-3/F-4 absent → stated, formal/ file list + Wave-0 row refreshed.

Check

just -f formal/justfile check

Verified locally: 4 closure reports, zero axioms.

🤖 Generated with Claude Code

https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

---

Generated by Claude Code

[github-actions]

🔍 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