feat(formal): stand up Coq formal/ track + mechanize the K-1 Wave-0 seed

[hyperpolymath]

What

Wave 0 of the docs/PROOF-NEEDS.adoc programme, on the keystone obligation K-1 (codegen → typed-WASM semantic-preservation). Stands up the formal/ directory (the dir #513 names) and lands a fully mechanized, axiom-free Coq proof for a minimal fragment.

Prover: Coq/Rocq 8.18 — chosen for K-1 because the typed-WASM target semantics interoperate with typed-wasm and ephapax, both of which use Coq Semantics.v.

The proof — formal/K1_CodegenPreservation.v

A complete compiler-correctness theorem with no Admitted, no axioms (Print Assumptions → "Closed under the global context"):

Definition K1_preservation : Prop :=
  forall e v, seval e = Some v -> wexec (compile e) [] = Some [obs v].

Theorem k1_preservation_holds : K1_preservation.   (* proven *)

i.e. whenever the source big-step evaluates to v, the compiled stack-machine code run on the empty operand stack yields exactly the corresponding wasm value [obs v]. The fragment (nat/bool · add/and → a little stack machine standing in for typed-WASM) is deliberately tiny; the real AST + real typed-WASM operational semantics remain the open obligation, expanded later the way solo-core's Duet/Ensemble tracks expand Solo. This mirrors how invariant-path/proofs/SameCube.agda grounds F-2 with a real proof rather than a hole.

Coq .v policy carve-out (the point you raised)

.v is shared by Coq, Verilog, and the estate-banned V-lang (→ Zig). Coq is neither — so this PR makes the distinction explicit so nothing can sweep it up:

• .hypatia-ignore — explicit formal/*.v exemption from cicd_rules/vlang_detected (+ banned_language_file). Coq ships no v.mod, so vmod_detected never fires.
• .claude/CLAUDE.md — new "Formal-methods Coq .v (NOT V-lang)" note: documents the estate path_allow_prefixes carve-out for Coq proof scripts, the no-Admitted/no-axiom rule, the Coq-vs-Idris2 prover split (Coq here for typed-wasm interop; solo-core stays Idris2), and "do not migrate/delete these as V-lang."

Track scaffolding

README.adoc, _CoqProject, justfile (check recipe type-checks and asserts the proof is axiom-free), .gitignore for Coq artifacts.

Docs synced

• PROOF-NEEDS.adoc: K-1 prose → partial; formal/ now exists; Wave-0 row marked in progress.
• FRG-PROFILE.adoc: the "no formalisation directory" honest-gap is met (grade stays E — D needs type-preservation/progress for the affine calculus, a theorem distinct from this codegen-preservation seed).

How to check

just -f formal/justfile check        # or:  cd formal && coqc K1_CodegenPreservation.v

Requires Coq 8.18+. Verified locally: compiles clean, Print Assumptions closed.

🤖 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