hyperpolymath · hyperpolymath · Jun 2, 2026 · Jun 2, 2026 · Jun 2, 2026
@@ -0,0 +1,48 @@
+# SPDX-License-Identifier: MPL-2.0
+# Machine-check BetLang's formal proofs on every push/PR.
+# See docs/AFFINESCRIPT-ALIGNMENT.adoc (Phase 1).
+name: Proofs
+permissions: read-all
+
+on:
+  push:
+    branches: [ main, develop ]
+  pull_request:
+    branches: [ main, develop ]
+  workflow_dispatch:
+
+jobs:
+  # Banned soundness escape hatches (sorry/admit/Admitted/postulate/...).
+  # Portable shell gate; the interim stand-in for `panic-attack assail
+  # --proofs-only` until panic-attack is available estate-wide.
+  banned-patterns:
+    name: Banned-pattern gate
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
+      - name: Scan proof sources
+        run: bash tools/proof-scan.sh .
+
+  # Build (= type-check) the Lean 4 formalisation. A green build is a
+  # machine-checked proof of Progress, Preservation and the monad laws.
+  lean4:
+    name: Lean 4 (lake build)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
+      - name: Install elan (Lean toolchain manager)
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            -o elan-init.sh
+          sha256sum elan-init.sh
+          bash elan-init.sh -y --default-toolchain "$(cat lean-toolchain)"
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Show toolchain
+        run: lake --version && lean --version
+      - name: Build proofs
+        run: lake build
@@ -43,3 +43,9 @@ deps/
 .cache/
 build/
 dist/
+
+# Lean 4 / Lake (proofs)
+.lake/
+*.olean
+lake-packages/
+lakefile.olean
@@ -82,6 +82,24 @@ test-tooling:
 clean-tooling:
     cargo clean
 
+# ============================================================================
+# PROOFS (formal verification — see docs/AFFINESCRIPT-ALIGNMENT.adoc)
+# ============================================================================
+
+# Machine-check the Lean 4 formalisation (proofs/BetLang.lean)
+proof-check-lean4:
+    @echo "Building Lean 4 proofs (lake build)..."
+    lake build
+
+# Scan proof sources for banned soundness escape hatches
+proof-scan:
+    @echo "Scanning proofs for banned patterns..."
+    bash tools/proof-scan.sh .
+
+# Run all available proof checks (scan + machine-check)
+proof-check-all: proof-scan proof-check-lean4
+    @echo "All proof checks complete."
+
 # ============================================================================
 # CODE QUALITY
 # ============================================================================

@@ -1,10 +1,72 @@
-# PROOF-NEEDS.md
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -->
+<!-- Defines proof obligations. Completion tracked in PROOF-STATUS.md. -->
+<!-- Aligned to the AffineScript estate PROOF-NEEDS format. -->
 
-## Template ABI Cleanup (2026-03-29)
+# PROOF-NEEDS.md — BetLang
 
-Template ABI removed -- was creating false impression of formal verification.
-The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
-scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.
+This file defines *what* must be proven. Completion is tracked in
+`PROOF-STATUS.md`; the phased plan is in
+`docs/AFFINESCRIPT-ALIGNMENT.adoc`; the trusted-base ledger is in
+`docs/proof-debt.adoc`.
 
-When this project needs formal ABI verification, create domain-specific Idris2 proofs
-following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.
+## Obligation Categories
+
+| Code | Category | Default prover | Rationale |
+|------|----------|----------------|-----------|
+| TP   | Typing / metatheory | Lean4 | Core calculus soundness (progress/preservation, monad laws) |
+| SEM  | Semantics | Lean4 | Operational ↔ denotational adequacy; continuous measure semantics |
+| STAT | Statistics | Lean4 | Limit theorems, entropy bounds, MC convergence |
+| ABI  | ABI / FFI | Idris2 | Rust/Julia FFI boundary safety (mandatory, mirrors AffineScript) |
+| CONC | Concurrency | TLA+ | Parallel bet-execution model |
+
+## Required Proofs
+
+| ID | Obligation | Category | Prover | Priority | Status |
+|----|------------|----------|--------|----------|--------|
+| TP-1   | Progress (well-typed ⇒ value or steps)             | TP   | Lean4  | P1 | ✅ done |
+| TP-2   | Preservation (typing preserved under step)          | TP   | Lean4  | P1 | ✅ done |
+| TP-3   | Distribution monad laws (×3)                        | TP   | Lean4  | P1 | ✅ done |
+| TP-4   | Discharge `substTop_preserves_typing` axiom         | TP   | Lean4  | P1 | remaining |
+| SEM-1  | Continuous measure-theoretic denotation             | SEM  | Lean4  | P2 | remaining |
+| STAT-1 | Maximum entropy of uniform ternary = log₂3          | STAT | Lean4  | P2 | remaining |
+| STAT-2 | SLLN for bet sample means                           | STAT | Lean4  | P2 | remaining |
+| ABI-1  | FFI non-null pointer safety                         | ABI  | Idris2 | P1 | remaining |
+| ABI-2  | FFI memory-layout correctness                       | ABI  | Idris2 | P1 | remaining |
+| ABI-3  | Platform type-size proofs                           | ABI  | Idris2 | P1 | remaining |
+| ABI-4  | Foreign return-type proofs                          | ABI  | Idris2 | P1 | remaining |
+| ABI-5  | C-ABI compliance                                    | ABI  | Idris2 | P1 | remaining |
+| CONC-1 | Parallel bet-execution model                        | CONC | TLA+   | P3 | remaining |
+
+## Banned Patterns
+
+No `sorry` / `admit` (Lean), `Admitted` (Coq), `postulate` /
+`believe_me` / `assert_total` (Idris2/Agda), `unsafeCoerce`. A single
+**classified** `axiom` is permitted under the standards#203
+trusted-base-reduction policy and must be registered in
+`docs/proof-debt.adoc`. Enforced by `tools/proof-scan.sh`.
+
+## How to Add a Proof
+
+1. Choose the prover (see categories above).
+2. Place the file in the correct home (Lean: `proofs/`; others:
+   `proofs/<prover>/`, exposed via `verification/proofs/`).
+3. Lean: rely on `lake build`; Idris2: `%default total`.
+4. Run `just proof-check-all`.
+5. Update `PROOF-STATUS.md` and, for any new escape hatch,
+   `docs/proof-debt.adoc`.
+
+---
+
+## Historical Note — Template ABI Cleanup (2026-03-29)
+
+Template ABI removed — was creating a false impression of formal
+verification. The removed files (`Types.idr`, `Layout.idr`,
+`Foreign.idr`) contained only RSR template scaffolding with unresolved
+`{{PROJECT}}`/`{{AUTHOR}}` placeholders and no domain-specific proofs.
+
+When this project needs formal ABI verification (obligations **ABI-1..5**
+above, Phase 3), create domain-specific Idris2 proofs following the
+pattern in repos like `typed-wasm`, `proven`, `echidna`, or
+`boj-server`, and in the AffineScript estate
+(`affinescript-vite/verification/proofs/idris2/ABI/`).
@@ -0,0 +1,84 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -->
+<!-- Tracks proof completion. Obligations defined in PROOF-NEEDS.md. -->
+<!-- Aligned to the AffineScript estate PROOF-STATUS format. -->
+
+# Proof Status — BetLang
+
+See `docs/AFFINESCRIPT-ALIGNMENT.adoc` for the phased plan and
+`docs/proof-debt.adoc` for the trusted-base reduction ledger.
+
+## Summary
+
+| Category | Total | Done | In Progress | Blocked | Remaining |
+|----------|-------|------|-------------|---------|-----------|
+| Typing / metatheory (TP)   | 4 | 3 | 0 | 0 | 1 |
+| Semantics (SEM)            | 1 | 0 | 0 | 0 | 1 |
+| Statistics (STAT)          | 2 | 0 | 0 | 0 | 2 |
+| ABI / FFI (ABI)            | 5 | 0 | 0 | 0 | 5 |
+| Concurrency (CONC)         | 1 | 0 | 0 | 0 | 1 |
+| **Total**                  | **13** | **3** | **0** | **0** | **10** |
+
+**Overall**: 23% proven (3 / 13). Lean core metatheory mechanised and
+(as of Phase 1) machine-checked in CI.
+
+## Proofs Done
+
+| ID | Proof | Prover | File | Verified By |
+|----|-------|--------|------|-------------|
+| TP-1 | Progress — well-typed closed term is a value or steps | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
+| TP-2 | Preservation — typing preserved under reduction | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
+| TP-3 | Distribution monad laws (left id, right id, assoc) | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
+
+> Note: TP-2 currently depends on the classified necessary axiom
+> `substTop_preserves_typing` (`proofs/BetLang.lean`). It is an explicit
+> axiom, **not** a `sorry` — see `docs/proof-debt.adoc` §(c). Discharging
+> it (TP-4) yields an axiom-free core.
+
+## Proofs In Progress
+
+| ID | Proof | Prover | Notes |
+|----|-------|--------|-------|
+| — | — | — | — |
+
+## Proofs Blocked
+
+| ID | Proof | Blocked By | Notes |
+|----|-------|------------|-------|
+| — | — | — | — |
+
+## Proofs Remaining
+
+| ID | Proof | Category | Prover | Phase | Priority |
+|----|-------|----------|--------|-------|----------|
+| TP-4   | Discharge `substTop_preserves_typing` (de Bruijn subst lemma) | TP   | Lean4  | 2 | P1 |
+| SEM-1  | Continuous measure-theoretic denotational semantics           | SEM  | Lean4  | 2 | P2 |
+| STAT-1 | Maximum entropy of uniform ternary = log₂3 bits               | STAT | Lean4  | 2 | P2 |
+| STAT-2 | SLLN for bet sample means (a.s. convergence to expectation)   | STAT | Lean4  | 2 | P2 |
+| ABI-1  | FFI non-null pointer safety                                   | ABI  | Idris2 | 3 | P1 |
+| ABI-2  | FFI memory-layout correctness                                 | ABI  | Idris2 | 3 | P1 |
+| ABI-3  | Platform type-size proofs                                     | ABI  | Idris2 | 3 | P1 |
+| ABI-4  | Foreign return-type proofs                                    | ABI  | Idris2 | 3 | P1 |
+| ABI-5  | C-ABI compliance                                             | ABI  | Idris2 | 3 | P1 |
+| CONC-1 | Parallel bet-execution model                                 | CONC | TLA+   | 3 | P3 |
+
+## Verification Commands
+
+```bash
+just proof-check-all      # banned-pattern scan + lake build
+just proof-check-lean4    # machine-check the Lean 4 formalisation
+just proof-scan           # banned-pattern gate only
+```
+
+## Banned Patterns
+
+`sorry` / `admit` (Lean), `Admitted` (Coq), `postulate` / `believe_me` /
+`assert_total` (Idris2/Agda), `unsafeCoerce`. Enforced by
+`tools/proof-scan.sh` in CI (`.github/workflows/proofs.yml`). The single
+classified `axiom` is permitted by policy (standards#203).
+
+## Changelog
+
+| Date | Change | By |
+|------|--------|-----|
+| 2026-06-02 | Phase 1: Lean proofs made CI-machine-checked; status table created. | alignment branch |