Skip to content

Commit bd4a599

Browse files
hyperpolymathhyperpolymath
authored
proofs: commence AffineScript alignment (Phase 1 — proof foundation) (#53)
Add lakefile.lean + lean-toolchain (buildable Lake package, pure-core no Mathlib), .github/workflows/proofs.yml (lake build + banned-pattern gate), tools/proof-scan.sh, PROOF-STATUS.md, verification/ RSR pillars, docs/AFFINESCRIPT-ALIGNMENT.adoc, and Justfile proof-check recipes. Lean 4 (lake build) machine-checks Progress + Preservation + monad laws in CI; 0 sorry, 1 classified axiom (substTop_preserves_typing).
1 parent 65a73e1 commit bd4a599

19 files changed

Lines changed: 735 additions & 12 deletions

‎.github/workflows/proofs.yml‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Machine-check BetLang's formal proofs on every push/PR.
3+
# See docs/AFFINESCRIPT-ALIGNMENT.adoc (Phase 1).
4+
name: Proofs
5+
permissions: read-all
6+
7+
on:
8+
push:
9+
branches: [ main, develop ]
10+
pull_request:
11+
branches: [ main, develop ]
12+
workflow_dispatch:
13+
14+
jobs:
15+
# Banned soundness escape hatches (sorry/admit/Admitted/postulate/...).
16+
# Portable shell gate; the interim stand-in for `panic-attack assail
17+
# --proofs-only` until panic-attack is available estate-wide.
18+
banned-patterns:
19+
name: Banned-pattern gate
20+
runs-on: ubuntu-latest
21+
timeout-minutes: 5
22+
steps:
23+
- name: Checkout code
24+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
25+
- name: Scan proof sources
26+
run: bash tools/proof-scan.sh .
27+
28+
# Build (= type-check) the Lean 4 formalisation. A green build is a
29+
# machine-checked proof of Progress, Preservation and the monad laws.
30+
lean4:
31+
name: Lean 4 (lake build)
32+
runs-on: ubuntu-latest
33+
timeout-minutes: 30
34+
steps:
35+
- name: Checkout code
36+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
37+
- name: Install elan (Lean toolchain manager)
38+
run: |
39+
set -euo pipefail
40+
curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
41+
-o elan-init.sh
42+
sha256sum elan-init.sh
43+
bash elan-init.sh -y --default-toolchain "$(cat lean-toolchain)"
44+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
45+
- name: Show toolchain
46+
run: lake --version && lean --version
47+
- name: Build proofs
48+
run: lake build

‎.gitignore‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,3 +43,9 @@ deps/
4343
.cache/
4444
build/
4545
dist/
46+
47+
# Lean 4 / Lake (proofs)
48+
.lake/
49+
*.olean
50+
lake-packages/
51+
lakefile.olean

‎Justfile‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,24 @@ test-tooling:
8282
clean-tooling:
8383
cargo clean
8484

85+
# ============================================================================
86+
# PROOFS (formal verification — see docs/AFFINESCRIPT-ALIGNMENT.adoc)
87+
# ============================================================================
88+
89+
# Machine-check the Lean 4 formalisation (proofs/BetLang.lean)
90+
proof-check-lean4:
91+
@echo "Building Lean 4 proofs (lake build)..."
92+
lake build
93+
94+
# Scan proof sources for banned soundness escape hatches
95+
proof-scan:
96+
@echo "Scanning proofs for banned patterns..."
97+
bash tools/proof-scan.sh .
98+
99+
# Run all available proof checks (scan + machine-check)
100+
proof-check-all: proof-scan proof-check-lean4
101+
@echo "All proof checks complete."
102+
85103
# ============================================================================
86104
# CODE QUALITY
87105
# ============================================================================

‎PROOF-NEEDS.md‎

Lines changed: 69 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,72 @@
1-
# PROOF-NEEDS.md
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -->
3+
<!-- Defines proof obligations. Completion tracked in PROOF-STATUS.md. -->
4+
<!-- Aligned to the AffineScript estate PROOF-NEEDS format. -->
25

3-
## Template ABI Cleanup (2026-03-29)
6+
# PROOF-NEEDS.md — BetLang
47

5-
Template ABI removed -- was creating false impression of formal verification.
6-
The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
7-
scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.
8+
This file defines *what* must be proven. Completion is tracked in
9+
`PROOF-STATUS.md`; the phased plan is in
10+
`docs/AFFINESCRIPT-ALIGNMENT.adoc`; the trusted-base ledger is in
11+
`docs/proof-debt.adoc`.
812

9-
When this project needs formal ABI verification, create domain-specific Idris2 proofs
10-
following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.
13+
## Obligation Categories
14+
15+
| Code | Category | Default prover | Rationale |
16+
|------|----------|----------------|-----------|
17+
| TP | Typing / metatheory | Lean4 | Core calculus soundness (progress/preservation, monad laws) |
18+
| SEM | Semantics | Lean4 | Operational ↔ denotational adequacy; continuous measure semantics |
19+
| STAT | Statistics | Lean4 | Limit theorems, entropy bounds, MC convergence |
20+
| ABI | ABI / FFI | Idris2 | Rust/Julia FFI boundary safety (mandatory, mirrors AffineScript) |
21+
| CONC | Concurrency | TLA+ | Parallel bet-execution model |
22+
23+
## Required Proofs
24+
25+
| ID | Obligation | Category | Prover | Priority | Status |
26+
|----|------------|----------|--------|----------|--------|
27+
| TP-1 | Progress (well-typed ⇒ value or steps) | TP | Lean4 | P1 | ✅ done |
28+
| TP-2 | Preservation (typing preserved under step) | TP | Lean4 | P1 | ✅ done |
29+
| TP-3 | Distribution monad laws (×3) | TP | Lean4 | P1 | ✅ done |
30+
| TP-4 | Discharge `substTop_preserves_typing` axiom | TP | Lean4 | P1 | remaining |
31+
| SEM-1 | Continuous measure-theoretic denotation | SEM | Lean4 | P2 | remaining |
32+
| STAT-1 | Maximum entropy of uniform ternary = log₂3 | STAT | Lean4 | P2 | remaining |
33+
| STAT-2 | SLLN for bet sample means | STAT | Lean4 | P2 | remaining |
34+
| ABI-1 | FFI non-null pointer safety | ABI | Idris2 | P1 | remaining |
35+
| ABI-2 | FFI memory-layout correctness | ABI | Idris2 | P1 | remaining |
36+
| ABI-3 | Platform type-size proofs | ABI | Idris2 | P1 | remaining |
37+
| ABI-4 | Foreign return-type proofs | ABI | Idris2 | P1 | remaining |
38+
| ABI-5 | C-ABI compliance | ABI | Idris2 | P1 | remaining |
39+
| CONC-1 | Parallel bet-execution model | CONC | TLA+ | P3 | remaining |
40+
41+
## Banned Patterns
42+
43+
No `sorry` / `admit` (Lean), `Admitted` (Coq), `postulate` /
44+
`believe_me` / `assert_total` (Idris2/Agda), `unsafeCoerce`. A single
45+
**classified** `axiom` is permitted under the standards#203
46+
trusted-base-reduction policy and must be registered in
47+
`docs/proof-debt.adoc`. Enforced by `tools/proof-scan.sh`.
48+
49+
## How to Add a Proof
50+
51+
1. Choose the prover (see categories above).
52+
2. Place the file in the correct home (Lean: `proofs/`; others:
53+
`proofs/<prover>/`, exposed via `verification/proofs/`).
54+
3. Lean: rely on `lake build`; Idris2: `%default total`.
55+
4. Run `just proof-check-all`.
56+
5. Update `PROOF-STATUS.md` and, for any new escape hatch,
57+
`docs/proof-debt.adoc`.
58+
59+
---
60+
61+
## Historical Note — Template ABI Cleanup (2026-03-29)
62+
63+
Template ABI removed — was creating a false impression of formal
64+
verification. The removed files (`Types.idr`, `Layout.idr`,
65+
`Foreign.idr`) contained only RSR template scaffolding with unresolved
66+
`{{PROJECT}}`/`{{AUTHOR}}` placeholders and no domain-specific proofs.
67+
68+
When this project needs formal ABI verification (obligations **ABI-1..5**
69+
above, Phase 3), create domain-specific Idris2 proofs following the
70+
pattern in repos like `typed-wasm`, `proven`, `echidna`, or
71+
`boj-server`, and in the AffineScript estate
72+
(`affinescript-vite/verification/proofs/idris2/ABI/`).

‎PROOF-STATUS.md‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -->
3+
<!-- Tracks proof completion. Obligations defined in PROOF-NEEDS.md. -->
4+
<!-- Aligned to the AffineScript estate PROOF-STATUS format. -->
5+
6+
# Proof Status — BetLang
7+
8+
See `docs/AFFINESCRIPT-ALIGNMENT.adoc` for the phased plan and
9+
`docs/proof-debt.adoc` for the trusted-base reduction ledger.
10+
11+
## Summary
12+
13+
| Category | Total | Done | In Progress | Blocked | Remaining |
14+
|----------|-------|------|-------------|---------|-----------|
15+
| Typing / metatheory (TP) | 4 | 3 | 0 | 0 | 1 |
16+
| Semantics (SEM) | 1 | 0 | 0 | 0 | 1 |
17+
| Statistics (STAT) | 2 | 0 | 0 | 0 | 2 |
18+
| ABI / FFI (ABI) | 5 | 0 | 0 | 0 | 5 |
19+
| Concurrency (CONC) | 1 | 0 | 0 | 0 | 1 |
20+
| **Total** | **13** | **3** | **0** | **0** | **10** |
21+
22+
**Overall**: 23% proven (3 / 13). Lean core metatheory mechanised and
23+
(as of Phase 1) machine-checked in CI.
24+
25+
## Proofs Done
26+
27+
| ID | Proof | Prover | File | Verified By |
28+
|----|-------|--------|------|-------------|
29+
| TP-1 | Progress — well-typed closed term is a value or steps | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
30+
| TP-2 | Preservation — typing preserved under reduction | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
31+
| TP-3 | Distribution monad laws (left id, right id, assoc) | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
32+
33+
> Note: TP-2 currently depends on the classified necessary axiom
34+
> `substTop_preserves_typing` (`proofs/BetLang.lean`). It is an explicit
35+
> axiom, **not** a `sorry` — see `docs/proof-debt.adoc` §(c). Discharging
36+
> it (TP-4) yields an axiom-free core.
37+
38+
## Proofs In Progress
39+
40+
| ID | Proof | Prover | Notes |
41+
|----|-------|--------|-------|
42+
| — | — | — | — |
43+
44+
## Proofs Blocked
45+
46+
| ID | Proof | Blocked By | Notes |
47+
|----|-------|------------|-------|
48+
| — | — | — | — |
49+
50+
## Proofs Remaining
51+
52+
| ID | Proof | Category | Prover | Phase | Priority |
53+
|----|-------|----------|--------|-------|----------|
54+
| TP-4 | Discharge `substTop_preserves_typing` (de Bruijn subst lemma) | TP | Lean4 | 2 | P1 |
55+
| SEM-1 | Continuous measure-theoretic denotational semantics | SEM | Lean4 | 2 | P2 |
56+
| STAT-1 | Maximum entropy of uniform ternary = log₂3 bits | STAT | Lean4 | 2 | P2 |
57+
| STAT-2 | SLLN for bet sample means (a.s. convergence to expectation) | STAT | Lean4 | 2 | P2 |
58+
| ABI-1 | FFI non-null pointer safety | ABI | Idris2 | 3 | P1 |
59+
| ABI-2 | FFI memory-layout correctness | ABI | Idris2 | 3 | P1 |
60+
| ABI-3 | Platform type-size proofs | ABI | Idris2 | 3 | P1 |
61+
| ABI-4 | Foreign return-type proofs | ABI | Idris2 | 3 | P1 |
62+
| ABI-5 | C-ABI compliance | ABI | Idris2 | 3 | P1 |
63+
| CONC-1 | Parallel bet-execution model | CONC | TLA+ | 3 | P3 |
64+
65+
## Verification Commands
66+
67+
```bash
68+
just proof-check-all # banned-pattern scan + lake build
69+
just proof-check-lean4 # machine-check the Lean 4 formalisation
70+
just proof-scan # banned-pattern gate only
71+
```
72+
73+
## Banned Patterns
74+
75+
`sorry` / `admit` (Lean), `Admitted` (Coq), `postulate` / `believe_me` /
76+
`assert_total` (Idris2/Agda), `unsafeCoerce`. Enforced by
77+
`tools/proof-scan.sh` in CI (`.github/workflows/proofs.yml`). The single
78+
classified `axiom` is permitted by policy (standards#203).
79+
80+
## Changelog
81+
82+
| Date | Change | By |
83+
|------|--------|-----|
84+
| 2026-06-02 | Phase 1: Lean proofs made CI-machine-checked; status table created. | alignment branch |

0 commit comments

Comments
 (0)