From 0eb7afe6914dd7c41cc214c9ece01d5b68ba2adf Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:49:03 +0100 Subject: [PATCH] =?UTF-8?q?proofs(lean4):=20mechanize=20the=20L1/L2=20core?= =?UTF-8?q?=20=E2=80=94=20hereditary=20substitution,=20grade=20algebras,?= =?UTF-8?q?=20hard=20gates?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit MECH-2 (complete): GradeAlgebra as the ET-4 ordered-semiring law set (16 laws as proof fields) with instances Affine {0,1,w}, tropical Cost (min/+), the generic bounded-distributive-lattice theorem instantiated at Level (Low<=High), and the componentwise product R x S (ET-5: composite disciplines are composition of algebras, proven once). MECH-1 (totality core + stability): intrinsically-kinded type-level STLC with the Keller-Altenkirch rem/wkv/eqv toolkit; beta-normal forms with LEFT-NESTED spines (append is cons, the spine fold is structural); hereditary substitution + normalizer total by a (kindSize, tag, size) lexicographic measure — the Totality Gate (ET-1) discharged by construction. DefEq stated; stability nf_emb : nf (embNf n) = n proven. Soundness/completeness (defEq_iff_nf, decDefEq) recorded OPEN in PROOF-STATUS — stated, never stubbed. Gates (wire-first, watched to fail before trusted): - scripts/check-proofs.sh: MANIFEST-driven; absent prover = FAIL; per-module lake build; whole-package build; mandatory axiom audit pinned to Lean's three-axiom trusted base (a smuggled user axiom fails the gate even though it compiles green). - scripts/scan-dangerous.sh: comment-aware scan incl. axiom/admit/ native_decide; FIXED Lean block-comment stripping ({- -} -> /- -/). - scripts/check-proof-status.sh: drift gate — PROOF-STATUS.adoc must match MANIFEST ground truth or CI fails. - .github/workflows/proofs.yml: sha-pinned actions, elan 4.2.3 from a checksum-verified release tarball, toolchain from lean-toolchain, cache keyed on the toolchain pin. No floating setup actions. All 11 modules gated; audit 12/12 within the trusted base; zero sorry, zero user axioms. Verified failure modes: broken proof, smuggled axiom, absent prover, unlisted file, status drift. Co-Authored-By: Claude Fable 5 --- .github/workflows/proofs.yml | 70 +++++ .gitignore | 3 + Justfile | 8 + build/just/proofs.just | 61 +++++ docs/status/PROOF-STATUS.adoc | 86 ++++-- scripts/check-proof-status.sh | 60 +++++ scripts/check-proofs.sh | 251 ++++++++++++++++++ scripts/scan-dangerous.sh | 75 ++++++ verification/proofs/lean4/MANIFEST | 14 + verification/proofs/lean4/Systemet.lean | 9 + verification/proofs/lean4/Systemet/Audit.lean | 28 ++ .../proofs/lean4/Systemet/L1/Conversion.lean | 81 ++++++ .../proofs/lean4/Systemet/L1/Hsub.lean | 93 +++++++ .../proofs/lean4/Systemet/L1/Normal.lean | 79 ++++++ .../proofs/lean4/Systemet/L1/Syntax.lean | 119 +++++++++ .../lean4/Systemet/L2/GradeAlgebra.lean | 62 +++++ .../lean4/Systemet/L2/Instances/Affine.lean | 82 ++++++ .../lean4/Systemet/L2/Instances/Lattice.lean | 171 ++++++++++++ .../lean4/Systemet/L2/Instances/Product.lean | 64 +++++ .../lean4/Systemet/L2/Instances/Tropical.lean | 107 ++++++++ verification/proofs/lean4/lake-manifest.json | 6 + verification/proofs/lean4/lakefile.toml | 7 + verification/proofs/lean4/lean-toolchain | 1 + 23 files changed, 1516 insertions(+), 21 deletions(-) create mode 100644 .github/workflows/proofs.yml create mode 100644 build/just/proofs.just create mode 100755 scripts/check-proof-status.sh create mode 100755 scripts/check-proofs.sh create mode 100755 scripts/scan-dangerous.sh create mode 100644 verification/proofs/lean4/MANIFEST create mode 100644 verification/proofs/lean4/Systemet.lean create mode 100644 verification/proofs/lean4/Systemet/Audit.lean create mode 100644 verification/proofs/lean4/Systemet/L1/Conversion.lean create mode 100644 verification/proofs/lean4/Systemet/L1/Hsub.lean create mode 100644 verification/proofs/lean4/Systemet/L1/Normal.lean create mode 100644 verification/proofs/lean4/Systemet/L1/Syntax.lean create mode 100644 verification/proofs/lean4/Systemet/L2/GradeAlgebra.lean create mode 100644 verification/proofs/lean4/Systemet/L2/Instances/Affine.lean create mode 100644 verification/proofs/lean4/Systemet/L2/Instances/Lattice.lean create mode 100644 verification/proofs/lean4/Systemet/L2/Instances/Product.lean create mode 100644 verification/proofs/lean4/Systemet/L2/Instances/Tropical.lean create mode 100644 verification/proofs/lean4/lake-manifest.json create mode 100644 verification/proofs/lean4/lakefile.toml create mode 100644 verification/proofs/lean4/lean-toolchain diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml new file mode 100644 index 0000000..84a2301 --- /dev/null +++ b/.github/workflows/proofs.yml @@ -0,0 +1,70 @@ +# SPDX-License-Identifier: MPL-2.0 +# Proof gate: the same scripts/check-proofs.sh a developer runs locally. +# Hermetic by construction — elan comes from a version-pinned release tarball +# with a checksum, the Lean toolchain from the committed lean-toolchain file, +# and no floating setup action is involved. A missing prover FAILS (the gate +# never skips), so this workflow existing is what makes green mean "proved". +name: proofs + +on: + push: + branches: [main] + paths: + - "verification/proofs/**" + - "scripts/check-proofs.sh" + - "scripts/check-proof-status.sh" + - "scripts/scan-dangerous.sh" + - "docs/status/PROOF-STATUS.adoc" + - ".github/workflows/proofs.yml" + pull_request: + paths: + - "verification/proofs/**" + - "scripts/check-proofs.sh" + - "scripts/check-proof-status.sh" + - "scripts/scan-dangerous.sh" + - "docs/status/PROOF-STATUS.adoc" + - ".github/workflows/proofs.yml" + workflow_dispatch: + +permissions: + contents: read + +jobs: + lean4: + name: lean4 proof gate + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + + - name: Cache elan + toolchain (keyed on lean-toolchain pin) + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 + with: + path: ~/.elan + key: elan-4.2.3-${{ runner.os }}-${{ hashFiles('verification/proofs/lean4/lean-toolchain') }} + + - name: Install elan (pinned tarball, checksum-verified) + run: | + set -euo pipefail + if [ ! -x "$HOME/.elan/bin/elan" ]; then + ELAN_VERSION=4.2.3 + ELAN_SHA256=df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2 + curl -sSfL -o /tmp/elan.tar.gz \ + "https://github.com/leanprover/elan/releases/download/v${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz" + echo "${ELAN_SHA256} /tmp/elan.tar.gz" | sha256sum -c - + tar -xzf /tmp/elan.tar.gz -C /tmp + /tmp/elan-init -y --default-toolchain none + fi + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + + - name: Install pinned Lean toolchain + run: elan toolchain install "$(cat verification/proofs/lean4/lean-toolchain)" + + - name: Proof gate (compile + coverage + axiom audit) + run: ./scripts/check-proofs.sh lean4 + + - name: Dangerous-construct scan + run: ./scripts/scan-dangerous.sh + + - name: Status drift gate (PROOF-STATUS must match MANIFEST) + run: ./scripts/check-proof-status.sh diff --git a/.gitignore b/.gitignore index fea81c4..6fd2b85 100644 --- a/.gitignore +++ b/.gitignore @@ -132,3 +132,6 @@ dist/ # Coaptation re-anchor basis (occasional, generated on --reanchor when red; not a baseline) .machine_readable/coaptation/receipts/reanchor-basis.a2ml + +# Lean 4 / lake build artifacts (proofs are rebuilt by the gate, never committed) +verification/proofs/lean4/.lake/ diff --git a/Justfile b/Justfile index a010893..9f28b06 100644 --- a/Justfile +++ b/Justfile @@ -544,6 +544,14 @@ help-me: @echo "" @echo "Include the output of 'just doctor' in your report." +# ═══════════════════════════════════════════════════════════════════════════════ +# FORMAL VERIFICATION (PROOFS) — see build/just/proofs.just +# proof-check-* delegate to scripts/check-proofs.sh: prover absent = FAIL, +# MANIFEST-driven, coverage-enforced. Never reintroduce a skip-on-missing gate. +# ═══════════════════════════════════════════════════════════════════════════════ + +import? "build/just/proofs.just" + # ═══════════════════════════════════════════════════════════════════════════════ # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS) # ═══════════════════════════════════════════════════════════════════════════════ diff --git a/build/just/proofs.just b/build/just/proofs.just new file mode 100644 index 0000000..dfd6334 --- /dev/null +++ b/build/just/proofs.just @@ -0,0 +1,61 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# FORMAL VERIFICATION (PROOFS) +# +# Imported by ../../Justfile via `import? "build/just/proofs.just"`. +# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus +# scan for dangerous/unsafe constructs and report status. Run via +# `just proof-check-all` for the full sweep. + +# Check all formal proofs (Idris2 + Lean4 + Agda + Coq) +proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous + @echo "=== All proof checks complete ===" + +# Each proof-check- delegates to scripts/check-proofs.sh, the single +# source of truth. A missing toolchain is FATAL (never a skip); every module is +# checked from its own source root; a proof file absent from the prover's +# manifest (verification/proofs//MANIFEST) is an error. See the script +# header for the four "checks that could not fail" this replaces. + +# Check Idris2 proofs (per MANIFEST; fatal if idris2 absent) +proof-check-idris2: + @bash scripts/check-proofs.sh idris2 + +# Check Lean4 proofs (per MANIFEST; fatal if lean absent) +proof-check-lean4: + @bash scripts/check-proofs.sh lean4 + +# Check Agda proofs (per MANIFEST; fatal if agda absent) +proof-check-agda: + @bash scripts/check-proofs.sh agda + +# Check Coq proofs (per MANIFEST; fatal if coqc absent) +proof-check-coq: + @bash scripts/check-proofs.sh coq + +# Scan for dangerous constructs USED in proof code (believe_me, sorry, Admitted, +# postulate, ...). Comments are ignored — a comment naming a banned construct +# must not trip the gate. See scripts/scan-dangerous.sh. +proof-scan-dangerous: + @bash scripts/scan-dangerous.sh + +# Show proof status summary +proof-status: + #!/usr/bin/env bash + echo "=== Proof Status ===" + echo "" + echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files" + echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files" + echo "Agda: $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files" + echo "Coq: $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files" + echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files" + echo "" + # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23) + for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do + if [ -f "$candidate" ]; then + grep -E "^\| \*\*Total\*\*|^\| \*Total\*" "$candidate" 2>/dev/null || echo "(No summary row in $candidate)" + exit 0 + fi + done + echo "(No PROOF-STATUS file found at root or docs/status/)" diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index c2a50be..9a80953 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -7,8 +7,12 @@ The obligation *statements* live in `docs/theory/OBLIGATIONS.adoc` (the ET ledger); this file tracks *evidence*. A row is "Done" only when a prover actually ran (locally and in CI via `scripts/check-proofs.sh`) and the axiom -audit is clean. The mechanization PR adds a CI drift gate that recomputes -the summary from the per-prover MANIFESTs and fails if this table disagrees. +audit is clean. `scripts/check-proof-status.sh` (run by CI) recomputes the +summary from the per-prover MANIFESTs and fails if this file disagrees. + +// Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh. +// Do not edit by hand without changing the MANIFEST accordingly. +// gate:lean4 gated=11 quarantined=0 == Summary @@ -16,14 +20,51 @@ the summary from the per-prover MANIFESTs and fails if this table disagrees. |=== | Track | Total | Done | In progress | Open -| ET obligations (DOM — the theory itself) | 15 | 0 | 0 | 15 -| MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | 0 | staged | — -| MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 0 | staged | — +| ET obligations (DOM — the theory itself) | 15 | 1 | 3 | 11 +| MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | — | in progress | — +| MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 1 | — | — |=== -*Overall: 0% proven.* No completed systemet proof exists at this date. The -generic template stubs previously counted here (5 ABI + 2 TP) were template -properties, not systemet obligations; they were removed with the ABI seam. +The Done/In-progress claims above are scoped to the *mechanized core +calculus* (type-level STLC with base constants and the object arrow; +grade algebras as ordered semirings). They are evidence toward the ET +obligations, not proofs of the full-theory statements. + +== Current evidence (verified by `./scripts/check-proofs.sh lean4`) + +All items below compile under Lean 4.32.0 (hermetic, zero dependencies, no +mathlib), pass the MANIFEST coverage check, and pass the axiom audit — +every theorem depends on nothing outside Lean's three-axiom trusted base +(`propext`, `Classical.choice`, `Quot.sound`); no `sorryAx`, no user axioms. + +[cols="1,3,2", options="header"] +|=== +| Covers | Artefact (Lean identifier) | Status + +| ET-1 (Totality Gate, L1 calculus) +| `Systemet.L1.substNf` / `appSp` / `nf` — hereditary substitution and the + normalizer, total by a `(kindSize, tag, size)` lexicographic measure +| *Proven* (totality is by construction; the measure is the proof) + +| ET-2 (equality is conversion) — partial +| `Systemet.L1.DefEq` (β + equivalence + congruence) stated; + `Systemet.L1.nf_emb : nf (embNf n) = n` — normal forms are fixed points + of the normalizer (stability) +| *Stability proven*; soundness/completeness OPEN (below) + +| ET-4 (grade algebras: the law set) +| `Systemet.L2.GradeAlgebra` — ordered-semiring law set (16 laws) as a + class whose fields *are* the proof obligations +| *Proven* for every instance below + +| ET-5 (same rules, different algebra) +| `Systemet.L2.Affine.grade` ({0,1,ω}), `Systemet.L2.Cost.grade` + (tropical min/+), `Systemet.L2.BoundedDistLattice.grade` (generic + theorem: every bounded distributive lattice is a grade algebra, + instantiated at `Level` = Low≤High), `Systemet.L2.prodGrade` (R×S + componentwise — composite disciplines are composition of algebras) +| *Proven* (4 algebras + 1 generic construction) +|=== == Mechanization slots @@ -32,15 +73,18 @@ properties, not systemet obligations; they were removed with the ABI seam. | Slot | Headline artefact | Covers | File target | MECH-1 -| `defEq_iff_nf : DefEq t u ↔ nf t = nf u` + `decDefEq` (β-fragment; - normalizer total by construction) -| ET-1, ET-2, syntactic core of ET-3 +| `defEq_iff_nf : DefEq t u ↔ nf t = nf u` + `decDefEq` (β-fragment). + Landed so far: totality core + stability. Remaining: soundness + (`DefEq t (embNf (nf t))`), completeness (`DefEq t u → nf t = nf u`), + decidable equality of `Nf` — all rest on the substitution-commutation + lemma; statements recorded in `Systemet/L1/Conversion.lean`. +| ET-1 ✓, ET-2 (partial), syntactic core of ET-3 | `verification/proofs/lean4/Systemet/L1/` | MECH-2 | `GradeAlgebra` class (the ET-4 law set) + instances Affine, Tropical - (Cost), Lattice (generic + Low≤High), Product (R×S) -| ET-4, ET-5 + (Cost), Lattice (generic + Low≤High), Product (R×S) — *complete*. +| ET-4 ✓, ET-5 ✓ (for the mechanized law set) | `verification/proofs/lean4/Systemet/L2/` |=== @@ -51,6 +95,7 @@ properties, not systemet obligations; they were removed with the ABI seam. | ID | Target | ET-14 | *TEA erasure — the headline open problem. Never cite as proven.* +| ET-2 (finish) | soundness + completeness + `defEq_iff_nf` + `decDefEq` (MECH-1 milestone 2) | ET-1..3 (η) | η-laws / η-long normal forms extension of MECH-1 | ET-1..3 (NAT) | type-level ℕ + recursor via NbE (stretch; research-adjacent) | ET-6, ET-7 | Structural Gate soundness + refusal characterization @@ -61,19 +106,18 @@ properties, not systemet obligations; they were removed with the ABI seam. == Verification commands -Available after the mechanization PR lands: - [source,bash] ---- -just proof-check-all # every prover with a MANIFEST; absent prover = FAIL -just proof-check-lean4 -just proof-scan-dangerous # comment-aware banned-construct scan +just proof-check-all # every prover with a MANIFEST; absent prover = FAIL +just proof-check-lean4 # compile + coverage + lake build + axiom audit +just proof-scan-dangerous # comment-aware banned-construct scan ./scripts/check-proofs.sh lean4 +./scripts/check-proof-status.sh # this file vs MANIFEST ground truth ---- -Until then there is deliberately *no* proof-check recipe: a recipe that -green-exits with no prover is the estate's known fake-gate pattern and is -not reproduced here. +The gate has been *watched to fail* on all four failure modes (broken +proof; smuggled `axiom` that compiles green; absent prover; proof file on +disk but missing from the MANIFEST) before its green was trusted. == Escape-hatch registry echo (ET-15) diff --git a/scripts/check-proof-status.sh b/scripts/check-proof-status.sh new file mode 100755 index 0000000..3933afe --- /dev/null +++ b/scripts/check-proof-status.sh @@ -0,0 +1,60 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-proof-status.sh — the status-drift gate. +# +# docs/status/PROOF-STATUS.adoc claims numbers; the per-prover MANIFESTs are +# the ground truth check-proofs.sh actually enforces. This script recomputes +# the counts from every MANIFEST and fails if the document disagrees, so the +# status file cannot drift into fiction (the estate's recurring failure mode: +# status docs saying "proved" while nothing was checked). +# +# Contract: for each verification/proofs//MANIFEST the document must +# contain the exact line +# +# // gate: gated= quarantined= +# +# and must not contain such a line for a prover with no MANIFEST. + +set -euo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")/.." +DOC="docs/status/PROOF-STATUS.adoc" +[ -f "$DOC" ] || { echo "FAIL: $DOC missing" >&2; exit 1; } + +fails=0 +found_any=0 + +for mf in verification/proofs/*/MANIFEST; do + [ -f "$mf" ] || continue + found_any=1 + prover="$(basename "$(dirname "$mf")")" + gated="$(awk -F'|' '$0 !~ /^[[:space:]]*(#|$)/ && $3 == "gated"' "$mf" | wc -l)" + quar="$(awk -F'|' '$0 !~ /^[[:space:]]*(#|$)/ && $3 == "quarantine"' "$mf" | wc -l)" + want="// gate:$prover gated=$gated quarantined=$quar" + if grep -qxF "$want" "$DOC"; then + echo "OK: $prover — $gated gated, $quar quarantined (document agrees)" + else + echo "FAIL: $DOC does not contain the line:" + echo " $want" + echo " ($mf ground truth: $gated gated, $quar quarantined)" + fails=$((fails + 1)) + fi +done + +# A marker for a prover with no MANIFEST is a stale claim. +while IFS= read -r line; do + p="$(sed -E 's|^// gate:([A-Za-z0-9_-]+) .*|\1|' <<<"$line")" + if [ ! -f "verification/proofs/$p/MANIFEST" ]; then + echo "FAIL: stale marker in $DOC for prover '$p' (no MANIFEST on disk)" + fails=$((fails + 1)) + fi +done < <(grep -E '^// gate:' "$DOC" || true) + +[ "$found_any" -eq 1 ] || echo "note: no MANIFESTs found — only staleness was checked" + +if [ "$fails" -gt 0 ]; then + echo "RESULT: FAIL ($fails drift(s) between PROOF-STATUS.adoc and MANIFEST ground truth)" + exit 1 +fi +echo "RESULT: PASS — PROOF-STATUS.adoc matches MANIFEST ground truth" diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh new file mode 100755 index 0000000..1afe4a3 --- /dev/null +++ b/scripts/check-proofs.sh @@ -0,0 +1,251 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-proofs.sh prover in: idris2 | lean4 | agda | coq +# +# The single source of truth for "do the proofs in this repo compile?". +# build/just/proofs.just calls this (`just proof-check-`), and CI should +# too, so a green local run and a green CI run mean the same thing. +# +# It replaces four separate "checks that could not fail" that let non-compiling +# proofs sit in estate repos for months while every status file said "proved": +# +# 1. `command -v || { echo SKIP; exit 0; }` — a MISSING TOOLCHAIN +# reported success. A gate that cannot run must never report OK: it +# manufactures false confidence, which is worse than having no gate. +# 2. ` --check ` — Idris2 (and friends) derive the +# expected module name from the path they are handed, so a module checked +# from the wrong directory fails on a name mismatch rather than its real +# errors, and verdicts invert. Every module here is checked from its own +# SOURCE ROOT (declared in the MANIFEST). +# 3. Path-filtered CI that only looked at one directory — nothing checked the +# rest. Here, a proof file present on disk but absent from the MANIFEST is +# an ERROR, so new proofs are gated by default, not by remembering. +# 4. `idris2 --check X && ok` — `idris2 --check` EXITS 0 ON A MISSING IMPORT +# (verified against 0.7.0) while printing `Error: ...`. Testing the exit +# code alone is unsound; for idris2 we require exit 0 AND no `Error:` line. +# +# They share one shape: a null check that emits reassuring text. If you extend +# this script, the test to apply is not "does it pass?" but "have I watched it +# fail?". +# +# CONVENTION: proofs live under verification/proofs// ; the MANIFEST for +# a prover is verification/proofs//MANIFEST, one entry per line: +# +# ||gated|quarantine| +# +# source-root : directory the prover is invoked from, chosen so the module's +# declared name matches its path (getting this wrong is hole #2). +# gated : MUST compile. A failure fails this script and CI. +# quarantine : known-broken, tracked in STATE.a2ml. Must CONTINUE to fail; +# if one starts compiling the script fails and tells you to +# promote it, so the list cannot rot into a permanent excuse. +# +# Blank lines and lines starting with # are ignored. +# +# Exit: 0 = every gated module compiles AND every quarantined module still fails +# AND every proof file on disk is listed; 1 = otherwise; 2 = misuse. + +set -euo pipefail + +PROVER="${1:-}" +case "$PROVER" in + idris2|lean4|agda|coq) ;; + *) echo "usage: $(basename "$0") " >&2; exit 2 ;; +esac + +# This script lives in /scripts/ ; run everything from the repo root. +cd "$(dirname "${BASH_SOURCE[0]}")/.." +ROOT="$PWD" +PROOF_DIR="verification/proofs/$PROVER" +MANIFEST_FILE="$PROOF_DIR/MANIFEST" + +# --- per-prover configuration ------------------------------------------------- +# CMD : executable that must be on PATH (absent => FAIL, never skip). +# EXT : file extension, for the "unlisted proof" coverage scan. +# ERROR_RE : if non-empty, output must not match it even when the exit code is 0. +# Only idris2 needs this (its --check exits 0 on a missing import); +# for lean4 it is a harmless belt-and-braces guard. +case "$PROVER" in + idris2) CMD=idris2; EXT=idr; ERROR_RE='^Error:' ;; + lean4) CMD=lean; EXT=lean; ERROR_RE='error:' ;; + agda) CMD=agda; EXT=agda; ERROR_RE='' ;; + coq) CMD=coqc; EXT=v; ERROR_RE='' ;; +esac + +check_one() { + # $1 source-root (rel to ROOT), $2 module (rel to source-root). + # Sets LAST_OUT to the tool output on failure; returns 0 iff the module compiles. + local root="$1" rel="$2" out rc + set +e + case "$PROVER" in + idris2) out="$(cd "$ROOT/$root" && idris2 --check "$rel" 2>&1)"; rc=$? ;; + lean4) + # In a lake package, per-file `lake env lean` fails on a fresh checkout + # (imports have no .olean yet), so build the module by name instead — + # `lake build Systemet.L1.Normal` compiles its dependency closure and + # exits non-zero on any error. Bare lean covers standalone files. + if [ -f "$ROOT/$root/lakefile.toml" ] || [ -f "$ROOT/$root/lakefile.lean" ]; then + local mod; mod="${rel%.lean}"; mod="${mod//\//.}" + out="$(cd "$ROOT/$root" && lake build "$mod" 2>&1)"; rc=$? + else + out="$(cd "$ROOT/$root" && lean "$rel" 2>&1)"; rc=$? + fi ;; + agda) out="$(cd "$ROOT/$root" && agda --safe "$rel" 2>&1)"; rc=$? ;; + coq) out="$(cd "$ROOT/$root" && coqc "$rel" 2>&1)"; rc=$? ;; + esac + set -e + if [ "$rc" -eq 0 ] && { [ -z "$ERROR_RE" ] || ! grep -qE "$ERROR_RE" <<<"$out"; }; then + LAST_OUT=""; return 0 + fi + LAST_OUT="$out"; return 1 +} + +echo "=== $PROVER proof check ===" + +# --- toolchain: absent means FAIL, never skip --------------------------------- +if ! command -v "$CMD" >/dev/null 2>&1; then + { + echo "FAIL: '$CMD' not found on PATH." + echo + echo "This is deliberately fatal. The previous recipe did 'exit 0' here with" + echo "\"SKIP: $CMD not installed\", so every $PROVER proof reported green on any" + echo "machine that could not check it. Install the $PROVER toolchain, or run" + echo "this in CI where the workflow installs it." + } >&2 + exit 1 +fi +"$CMD" --version 2>/dev/null | head -1 || true +echo + +# --- a repo with proofs but no MANIFEST is itself a failure ------------------- +if [ ! -f "$MANIFEST_FILE" ]; then + if [ -d "$PROOF_DIR" ] && [ -n "$(find "$PROOF_DIR" -name "*.$EXT" 2>/dev/null)" ]; then + echo "FAIL: $PROOF_DIR contains .$EXT proofs but has no MANIFEST." >&2 + echo " Create $MANIFEST_FILE listing each as 'gated' or 'quarantine'." >&2 + exit 1 + fi + echo "no $PROOF_DIR/*.$EXT proofs and no MANIFEST — nothing to check." + exit 0 +fi + +fails=0 +unexpected_pass=0 +listed_tmp="$(mktemp)" +trap 'rm -f "$listed_tmp"' EXIT + +while IFS='|' read -r root rel status note; do + # skip blank lines and comments + [ -z "${root// }" ] && continue + case "${root#"${root%%[![:space:]]*}"}" in \#*) continue ;; esac + printf ' %-30s %-24s ' "$root" "$rel" + echo "$root/$rel" >>"$listed_tmp" + if check_one "$root" "$rel"; then + if [ "$status" = gated ]; then + echo "PASS" + else + echo "PASS -- UNEXPECTED (quarantined module now compiles)" + echo " Promote '$rel' to 'gated' in $MANIFEST_FILE and update STATE.a2ml." + unexpected_pass=$((unexpected_pass + 1)) + fi + else + if [ "$status" = gated ]; then + echo "FAIL" + printf '%s\n' "${LAST_OUT//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + else + echo "fail (quarantined, expected)" + [ -n "${note// }" ] && echo " reason:$note" + fi + fi +done < "$MANIFEST_FILE" + +# --- coverage: every proof on disk must be listed ----------------------------- +# The anti-recurrence rule: proofs went unchecked for months because nothing +# forced them onto anyone's list. A file absent from the MANIFEST is an error. +echo +echo "=== manifest coverage ($PROOF_DIR) ===" +listed="$(sort -u "$listed_tmp")" +found="$(cd "$ROOT" && find "$PROOF_DIR" -name "*.$EXT" -not -path '*/build/*' -not -path '*/.lake/*' 2>/dev/null | sort)" +unlisted="$(comm -13 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" +missing="$(comm -23 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" + +if [ -n "${unlisted//[[:space:]]/}" ]; then + echo "FAIL: .$EXT proofs on disk but absent from $MANIFEST_FILE:" + printf ' %s\n' $unlisted + echo " List each as 'gated' or 'quarantine'; new proofs are gated by default." + fails=$((fails + 1)) +fi +if [ -n "${missing//[[:space:]]/}" ]; then + echo "FAIL: MANIFEST lists modules that do not exist (stale entries):" + printf ' %s\n' $missing + fails=$((fails + 1)) +fi +[ -z "${unlisted//[[:space:]]/}${missing//[[:space:]]/}" ] && \ + echo " all $(printf '%s\n' "$found" | grep -c .) .$EXT file(s) accounted for" + +# --- lean4 lake package: whole-package build + transitive axiom audit --------- +# Per-file checks above prove each MANIFESTed module elaborates, but only a +# package build proves the import graph is complete, and only `#print axioms` +# proves no theorem depends on sorryAx/an axiom smuggled in transitively. +if [ "$PROVER" = lean4 ] && { [ -f "$PROOF_DIR/lakefile.toml" ] || [ -f "$PROOF_DIR/lakefile.lean" ]; }; then + echo + echo "=== lake build ($PROOF_DIR) ===" + set +e + build_out="$(cd "$ROOT/$PROOF_DIR" && lake build 2>&1)"; build_rc=$? + set -e + printf '%s\n' "$build_out" | tail -5 + if [ "$build_rc" -ne 0 ] || grep -qE "declaration uses 'sorry'|error:" <<<"$build_out"; then + echo "FAIL: lake build failed or reported sorry/errors" + fails=$((fails + 1)) + fi + + AUDIT_FILE="$PROOF_DIR/Systemet/Audit.lean" + if [ -f "$AUDIT_FILE" ]; then + echo + echo "=== axiom audit (Systemet/Audit.lean) ===" + set +e + audit_out="$(cd "$ROOT/$PROOF_DIR" && lake env lean Systemet/Audit.lean 2>&1)"; audit_rc=$? + set -e + printf '%s\n' "$audit_out" | sed 's/^/ /' + # The trusted base is exactly Lean's three core axioms (propext, + # Classical.choice, Quot.sound) — they enter via omega/simp/WF recursion + # and are sound. ANYTHING else (sorryAx, a user `axiom`) fails: a stub + # axiom compiles green, so "builds" must never be read as "proved". + expected="$(grep -c '^#print axioms' "$ROOT/$AUDIT_FILE" || true)" + ok=0; bad=0 + while IFS= read -r line; do + case "$line" in + *"does not depend on any axioms"*) ok=$((ok + 1)) ;; + *"depends on axioms:"*) + axlist="${line#*depends on axioms: [}"; axlist="${axlist%%]*}" + rest="$(tr ',' '\n' <<<"$axlist" | sed 's/^ *//; s/ *$//' \ + | grep -vE '^(propext|Classical\.choice|Quot\.sound)$' || true)" + if [ -n "${rest//[[:space:]]/}" ]; then + bad=$((bad + 1)) + echo " DISALLOWED axiom(s) beyond the trusted base: $rest" + else + ok=$((ok + 1)) + fi ;; + esac + done <<<"$audit_out" + if [ "$audit_rc" -ne 0 ] || grep -q 'sorryAx' <<<"$audit_out" || [ "$bad" -ne 0 ] || [ "$ok" -ne "$expected" ]; then + echo "FAIL: axiom audit — $ok/$expected item(s) within the trusted base, $bad with disallowed axioms$(grep -q sorryAx <<<"$audit_out" && echo '; sorryAx PRESENT')" + fails=$((fails + 1)) + else + echo " audit: $ok/$expected headline items within the trusted base (no sorryAx, no user axioms)" + fi + else + echo + echo "FAIL: lake package present but Systemet/Audit.lean missing — the axiom audit is mandatory" + fails=$((fails + 1)) + fi +fi + +echo +if [ "$fails" -gt 0 ] || [ "$unexpected_pass" -gt 0 ]; then + echo "RESULT: FAIL ($fails failure(s), $unexpected_pass unexpected pass(es))" + exit 1 +fi +echo "RESULT: PASS -- gated modules compile; quarantined modules still fail as recorded" diff --git a/scripts/scan-dangerous.sh b/scripts/scan-dangerous.sh new file mode 100755 index 0000000..dbe0dbf --- /dev/null +++ b/scripts/scan-dangerous.sh @@ -0,0 +1,75 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# scan-dangerous.sh — flag dangerous/unsafe constructs USED in proof code. +# +# Dangerous constructs (believe_me, assert_total, postulate, sorry, Admitted, +# unsafeCoerce, Obj.magic) escape the proof obligation and must not appear in +# real proofs. BUT the previous `proof-scan-dangerous` recipe grepped raw +# lines, so a comment that merely NAMED a banned construct — +# -- All proofs MUST be constructive (no believe_me, no assert_total). +# — tripped the gate. A check that fires on its own documentation is a +# false-positive gate: it cries wolf, trains people to override it (violating +# "squabble, don't bypass"), and wired into CI it turns the tree red for +# nothing. This version strips comments first, so only real usage is flagged. +# +# Comment syntax handled: `--` line + `{- -}` block (Idris2/Lean4/Agda), +# `(* *)` block (Coq). Comment bodies are blanked in place, so reported line +# numbers still match the source. +# +# Exit: 0 = clean; 1 = a proof uses a dangerous construct in code. + +set -euo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")/.." + +PATTERNS='believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic|\badmit\b|\baxiom\b|\bAxiom\b|native_decide' +dangerous=0 + +# Blank comment content while preserving line count (so grep -n stays accurate). +strip_comments() { + local ext="${1##*.}" lc bo bc + case "$ext" in + idr|agda) lc='--'; bo='{-'; bc='-}' ;; # line + block comments + lean) lc='--'; bo='/-'; bc='-/' ;; # Lean block comments differ + v) lc=''; bo='(*'; bc='*)' ;; # Coq block comments only + *) lc=''; bo=''; bc='' ;; + esac + awk -v lc="$lc" -v bo="$bo" -v bc="$bc" ' + BEGIN { inblk = 0 } + { + line = $0; out = ""; i = 1; n = length(line) + while (i <= n) { + if (inblk) { + if (bc != "" && substr(line,i,length(bc)) == bc) { inblk = 0; i += length(bc) } + else { i++ } + } else if (bo != "" && substr(line,i,length(bo)) == bo) { + inblk = 1; i += length(bo) + } else if (lc != "" && substr(line,i,length(lc)) == lc) { + break # rest of the line is a line-comment + } else { + out = out substr(line,i,1); i++ + } + } + print out + }' "$1" +} + +while IFS= read -r f; do + [ -z "$f" ] && continue + matches="$(strip_comments "$f" | grep -nE "$PATTERNS" || true)" + if [ -n "$matches" ]; then + echo " DANGEROUS (used in code): $f" + printf '%s\n' "$matches" | sed 's/^/ /' + dangerous=$((dangerous + 1)) + fi +done < <(find verification/proofs \ + \( -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' \) \ + -not -path '*/build/*' 2>/dev/null | sort) + +echo +if [ "$dangerous" -gt 0 ]; then + echo "FAIL: $dangerous file(s) use dangerous constructs in proof CODE (not comments)" + exit 1 +fi +echo "PASS: no dangerous constructs used in proof code" diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST new file mode 100644 index 0000000..b754b5e --- /dev/null +++ b/verification/proofs/lean4/MANIFEST @@ -0,0 +1,14 @@ +# MANIFEST for verification/proofs/lean4 — read by scripts/check-proofs.sh +# ||gated| +# gated = must compile; quarantine = known-broken, must keep failing. +verification/proofs/lean4|Systemet.lean|gated|package root (import graph) +verification/proofs/lean4|Systemet/L1/Syntax.lean|gated|MECH-1: kinds, Ty, rem/wkv/eqv toolkit, substTy +verification/proofs/lean4|Systemet/L1/Normal.lean|gated|MECH-1: Nf/Sp, sizes, spKindLe, weakening +verification/proofs/lean4|Systemet/L1/Hsub.lean|gated|MECH-1: hereditary substitution + normalizer (ET-1) +verification/proofs/lean4|Systemet/L1/Conversion.lean|gated|MECH-1: DefEq, embeddings, stability nf_emb +verification/proofs/lean4|Systemet/L2/GradeAlgebra.lean|gated|MECH-2: the ET-4 law set as a class +verification/proofs/lean4|Systemet/L2/Instances/Affine.lean|gated|MECH-2: {0,1,omega} usage algebra +verification/proofs/lean4|Systemet/L2/Instances/Tropical.lean|gated|MECH-2: Cost = tropical min/+ +verification/proofs/lean4|Systemet/L2/Instances/Lattice.lean|gated|MECH-2: bounded distributive lattice => grade algebra; Level +verification/proofs/lean4|Systemet/L2/Instances/Product.lean|gated|MECH-2: componentwise product algebra (ET-5) +verification/proofs/lean4|Systemet/Audit.lean|gated|axiom audit (#print axioms per headline) diff --git a/verification/proofs/lean4/Systemet.lean b/verification/proofs/lean4/Systemet.lean new file mode 100644 index 0000000..ee0f2db --- /dev/null +++ b/verification/proofs/lean4/Systemet.lean @@ -0,0 +1,9 @@ +import Systemet.L1.Syntax +import Systemet.L1.Normal +import Systemet.L1.Hsub +import Systemet.L1.Conversion +import Systemet.L2.GradeAlgebra +import Systemet.L2.Instances.Affine +import Systemet.L2.Instances.Tropical +import Systemet.L2.Instances.Lattice +import Systemet.L2.Instances.Product diff --git a/verification/proofs/lean4/Systemet/Audit.lean b/verification/proofs/lean4/Systemet/Audit.lean new file mode 100644 index 0000000..d902d30 --- /dev/null +++ b/verification/proofs/lean4/Systemet/Audit.lean @@ -0,0 +1,28 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet +/-! +# Axiom audit — every headline item, transitively axiom-free + +`scripts/check-proofs.sh lean4` runs this file and requires one +"does not depend on any axioms" line per `#print axioms` command below +(and no `sorryAx` anywhere in the output). A theorem that elaborates but +smuggles in an axiom or a `sorry` through an import fails the gate here, +not in a status document. Update the PROOF-STATUS ledger when adding lines. +-/ + +-- MECH-1 (L1): totality core + stability +#print axioms Systemet.L1.substTy +#print axioms Systemet.L1.substNf +#print axioms Systemet.L1.appSp +#print axioms Systemet.L1.nf +#print axioms Systemet.L1.spKindLe +#print axioms Systemet.L1.nf_emb +#print axioms Systemet.L1.nf_embSp + +-- MECH-2 (L2): the grade-algebra law set and its instances +#print axioms Systemet.L2.Affine.grade +#print axioms Systemet.L2.Cost.grade +#print axioms Systemet.L2.BoundedDistLattice.grade +#print axioms Systemet.L2.Level.lattice +#print axioms Systemet.L2.prodGrade diff --git a/verification/proofs/lean4/Systemet/L1/Conversion.lean b/verification/proofs/lean4/Systemet/L1/Conversion.lean new file mode 100644 index 0000000..6b6dba1 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/Conversion.lean @@ -0,0 +1,81 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.Hsub +/-! +# L1 conversion (ET-2: the one primitive relation) + +The declarative judgement `DefEq` — β plus equivalence plus congruence — +and the embedding of normal forms back into terms. + +Proven here: **stability** (`nf_emb : nf (embNf n) = n`) — normal forms are +fixed points of the normalizer, so `nf` is a retraction of `embNf`. + +Stated-but-OPEN (milestone 2 of MECH-1, tracked in +docs/status/PROOF-STATUS.adoc — deliberately *not* stubbed here, per the +no-silent-skip constraint): + +* soundness — `DefEq t (embNf (nf t))`; +* completeness — `DefEq t u → nf t = nf u`; +* their corollary `defEq_iff_nf : DefEq t u ↔ nf t = nf u`, which with + decidable equality of `Nf` yields `decDefEq` and closes ET-2 for this + calculus. Both rest on the substitution-commutation lemma + `DefEq (substTy (embNf t) x (embNf u)) (embNf (substNf t x u))`, by the + same lexicographic induction as `substNf`. +-/ + +namespace Systemet.L1 + +/-- Declarative β-conversion: the least congruent equivalence containing β. + This is L1's one primitive relation — "equality is conversion". -/ +inductive DefEq : {Γ : Ctx} → {k : Kind} → Ty Γ k → Ty Γ k → Prop where + | refl : DefEq t t + | symm : DefEq t u → DefEq u t + | trans : DefEq t u → DefEq u v → DefEq t v + | beta : (b : Ty (k₁ :: Γ) k₂) → (u : Ty Γ k₁) → + DefEq (.app (.lam b) u) (subst0 b u) + | arrowCong : DefEq a a' → DefEq b b' → DefEq (.arrow a b) (.arrow a' b') + | lamCong : DefEq b b' → DefEq (.lam b) (.lam b') + | appCong : DefEq f f' → DefEq a a' → DefEq (.app f a) (.app f' a') + +mutual + /-- Embed a normal form back into raw terms. -/ + def embNf : {Γ : Ctx} → {k : Kind} → Nf Γ k → Ty Γ k + | _, _, .lam b => .lam (embNf b) + | _, _, .base n => .base n + | _, _, .arrow a b => .arrow (embNf a) (embNf b) + | _, _, .ne x sp => embSp (.var x) sp + termination_by _ _ t => nfSize t + decreasing_by all_goals (simp only [nfSize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Embed a spine, folding applications around a head term. -/ + def embSp : {Γ : Ctx} → {a j : Kind} → Ty Γ a → Sp Γ a j → Ty Γ j + | _, _, _, t, .nil => t + | _, _, _, t, .cons sp v => .app (embSp t sp) (embNf v) + termination_by _ _ _ _ sp => spSize sp + decreasing_by all_goals (simp only [spSize]; omega) +end + +mutual + /-- **Stability**: normal forms are fixed points of the normalizer. With + `nf` total this makes `nf` a retraction of `embNf` — every normal form + is reachable, and re-normalizing is the identity on the image. -/ + theorem nf_emb : {Γ : Ctx} → {k : Kind} → (n : Nf Γ k) → nf (embNf n) = n + | _, _, .lam b => by simp [embNf, nf, nf_emb b] + | _, _, .base _ => by simp [embNf, nf] + | _, _, .arrow a b => by simp [embNf, nf, nf_emb a, nf_emb b] + | _, _, .ne x sp => by rw [embNf]; exact nf_embSp x sp + termination_by _ _ n => nfSize n + decreasing_by all_goals (simp only [nfSize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Spine form of `nf_emb`: normalizing a variable applied through an + embedded spine recovers the neutral. -/ + theorem nf_embSp : {Γ : Ctx} → {a j : Kind} → (x : Var Γ a) → (sp : Sp Γ a j) → + nf (embSp (.var x) sp) = .ne x sp + | _, _, _, _, .nil => by simp [embSp, nf] + | _, _, _, x, .cons sp v => by + simp [embSp, nf, nf_embSp x sp, nf_emb v, napp] + termination_by _ _ _ _ sp => spSize sp + decreasing_by all_goals (simp only [spSize]; omega) +end + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/Hsub.lean b/verification/proofs/lean4/Systemet/L1/Hsub.lean new file mode 100644 index 0000000..cf272c0 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/Hsub.lean @@ -0,0 +1,93 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.Normal +/-! +# L1 hereditary substitution and the normalizer (ET-1 evidence) + +Substitution on β-normal forms that re-normalizes on the fly, after +Keller–Altenkirch. Totality is by a `(kindSize, tag, size)` lexicographic +measure — this **is** the Totality Gate for the L1 type-level calculus, +discharged by construction rather than by a separate strong-normalization +proof: + +* substituting under a binder or into a spine keeps the substitution kind + and shrinks the term (`(k, 1, size)` third component); +* hitting the substituted head variable hands off to the spine fold at the + same kind but a smaller tag (`(k, 0, _)`); +* the spine fold β-reduces through a λ only at a *strictly smaller* kind — + `spKindLe` bounds the intermediate arrow kind by the spine's head kind, + so the argument kind drops the first component. + +`nf` then normalizes every `Ty` by one structural pass; all β-work happens +inside the total `appSp`/`napp`. +-/ + +namespace Systemet.L1 + +mutual + /-- Hereditary substitution on normal forms. -/ + def substNf : {Γ : Ctx} → {j : Kind} → Nf Γ j → (x : Var Γ k) → Nf (rem x) k → Nf (rem x) j + | _, _, .lam b, x, u => .lam (substNf b (.vs x) (wkNf .vz u)) + | _, _, .base n, _, _ => .base n + | _, _, .arrow a b, x, u => .arrow (substNf a x u) (substNf b x u) + | _, _, .ne y sp, x, u => + match eqv x y with + | .same => appSp u (substSp sp x u) + | .diff _ y' => .ne y' (substSp sp x u) + termination_by _ _ t _ _ => (kindSize k, 1, nfSize t) + decreasing_by + all_goals simp only [nfSize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.right; apply Prod.Lex.left; omega) + | (apply Prod.Lex.left + have h := spKindLe sp + simp only [kindSize] at h ⊢ + omega) + + /-- Hereditary substitution on spines. -/ + def substSp : {Γ : Ctx} → {a j : Kind} → Sp Γ a j → (x : Var Γ k) → Nf (rem x) k → Sp (rem x) a j + | _, _, _, .nil, _, _ => .nil + | _, _, _, .cons sp v, x, u => .cons (substSp sp x u) (substNf v x u) + termination_by _ _ _ sp _ _ => (kindSize k, 1, spSize sp) + decreasing_by + all_goals simp only [spSize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.right; apply Prod.Lex.left; omega) + + /-- Fold a normal form through a spine, β-reducing at each step. -/ + def appSp : {Γ : Ctx} → {a j : Kind} → Nf Γ a → Sp Γ a j → Nf Γ j + | _, _, _, u, .nil => u + | _, _, _, u, .cons sp v => + match appSp u sp with + | .lam t => substNf t .vz v + | .ne y sp' => .ne y (.cons sp' v) + termination_by _ a _ _ sp => (kindSize a, 0, spSize sp) + decreasing_by + all_goals simp only [spSize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.left + have h := spKindLe sp + simp only [kindSize] at h ⊢ + omega) +end + +/-- Single β-application of normal forms. -/ +def napp : Nf Γ (.arr a b) → Nf Γ a → Nf Γ b + | .lam t, v => substNf t .vz v + | .ne y sp, v => .ne y (.cons sp v) + +/-- The normalizer: every type-level term has a β-normal form, by a + structurally-recursive pass over the term (all β-work is inside the + total `napp`). -/ +def nf : {Γ : Ctx} → {k : Kind} → Ty Γ k → Nf Γ k + | _, _, .var x => .ne x .nil + | _, _, .base n => .base n + | _, _, .arrow a b => .arrow (nf a) (nf b) + | _, _, .lam b => .lam (nf b) + | _, _, .app f a => napp (nf f) (nf a) +termination_by structural _ _ t => t + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/Normal.lean b/verification/proofs/lean4/Systemet/L1/Normal.lean new file mode 100644 index 0000000..7ba780c --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/Normal.lean @@ -0,0 +1,79 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.Syntax +/-! +# L1 β-normal forms (docs/theory/02-l1-equality.adoc) + +Normal forms `Nf` and neutral spines `Sp`, intrinsically kinded like `Ty`. + +Spines are **left-nested**: `Sp Γ a j` is a sequence of arguments taking a +head of kind `a` to kind `j`, and `cons sp v` appends the *last* argument. +This orientation makes "apply a neutral to one more argument" constant-time +(`.ne y (.cons sp v)` — no `snoc`), and makes the spine fold in hereditary +substitution structurally recursive. + +`spKindLe` — the end kind of a spine is bounded by its head kind — is the +one-line invariant the hereditary-substitution termination measure leans on. +-/ + +namespace Systemet.L1 + +/-- Size of a kind — the primary component of the hereditary-substitution + termination measure. -/ +def kindSize : Kind → Nat + | .star => 1 + | .arr a b => kindSize a + kindSize b + 1 + +mutual + /-- β-normal forms. -/ + inductive Nf : Ctx → Kind → Type where + | lam : Nf (k₁ :: Γ) k₂ → Nf Γ (.arr k₁ k₂) + | base : Nat → Nf Γ .star + | arrow : Nf Γ .star → Nf Γ .star → Nf Γ .star + | ne : Var Γ k → Sp Γ k j → Nf Γ j + + /-- Spines, left-nested: `cons sp v` appends the *last* argument. -/ + inductive Sp : Ctx → Kind → Kind → Type where + | nil : Sp Γ k k + | cons : Sp Γ a (.arr b c) → Nf Γ b → Sp Γ a c +end + +mutual + /-- Index-independent size of a normal form (termination measure). -/ + def nfSize : {Γ : Ctx} → {k : Kind} → Nf Γ k → Nat + | _, _, .lam b => nfSize b + 1 + | _, _, .base _ => 1 + | _, _, .arrow a b => nfSize a + nfSize b + 1 + | _, _, .ne _ sp => spSize sp + 1 + + /-- Index-independent size of a spine (termination measure). -/ + def spSize : {Γ : Ctx} → {a j : Kind} → Sp Γ a j → Nat + | _, _, _, .nil => 0 + | _, _, _, .cons sp v => spSize sp + nfSize v + 1 +end + +/-- The end kind of a spine is no larger than its head kind. -/ +theorem spKindLe : {Γ : Ctx} → {a j : Kind} → Sp Γ a j → kindSize j ≤ kindSize a + | _, _, _, .nil => Nat.le_refl _ + | _, _, _, .cons sp _ => + Nat.le_trans (by simp [kindSize]; omega) (spKindLe sp) + +mutual + /-- Weakening of normal forms along one skipped slot. -/ + def wkNf : {Γ : Ctx} → (x : Var Γ k) → Nf (rem x) j → Nf Γ j + | _, x, .lam b => .lam (wkNf (.vs x) b) + | _, _, .base n => .base n + | _, x, .arrow a b => .arrow (wkNf x a) (wkNf x b) + | _, x, .ne y sp => .ne (wkv x y) (wkSp x sp) + termination_by _ _ t => nfSize t + decreasing_by all_goals (simp only [nfSize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Weakening of spines along one skipped slot. -/ + def wkSp : {Γ : Ctx} → (x : Var Γ k) → Sp (rem x) a j → Sp Γ a j + | _, _, .nil => .nil + | _, x, .cons sp v => .cons (wkSp x sp) (wkNf x v) + termination_by _ _ sp => spSize sp + decreasing_by all_goals (simp only [spSize]; omega) +end + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/Syntax.lean b/verification/proofs/lean4/Systemet/L1/Syntax.lean new file mode 100644 index 0000000..fb925e2 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/Syntax.lean @@ -0,0 +1,119 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +/-! +# L1 syntax: the type-level core calculus (docs/theory/00-notation.adoc) + +Kinds, contexts, intrinsically-kinded type-level terms with de Bruijn +variables. `Ty Γ k` is the L1 language: the simply-kinded λ-calculus with a +countable family of base constants at `★` and the object-level arrow as a +constructor. Everything downstream (normal forms, hereditary substitution, +conversion) is indexed the same way, so ill-kinded terms are unrepresentable. + +The `rem`/`wkv`/`EqV` toolkit is Keller–Altenkirch's ("Hereditary +Substitutions for Simple Types", MSFP 2010), ported to Lean 4. Where a +definition matches on an argument whose type mentions `rem x`, the match is +pushed into a term-level `match` (after `x`'s constructor is known) so the +index reduces before the inner patterns elaborate. +-/ + +namespace Systemet.L1 + +/-- Kinds: `★` and type-level function kinds. -/ +inductive Kind : Type where + | star : Kind + | arr : Kind → Kind → Kind +deriving DecidableEq, Repr + +/-- Contexts are lists of kinds (de Bruijn: position = index). -/ +abbrev Ctx := List Kind + +/-- Typed de Bruijn variables: `Var Γ k` is a position of kind `k` in `Γ`. -/ +inductive Var : Ctx → Kind → Type where + | vz : Var (k :: Γ) k + | vs : Var Γ k → Var (k' :: Γ) k +deriving DecidableEq + +/-- Type-level terms, intrinsically kinded. -/ +inductive Ty : Ctx → Kind → Type where + | var : Var Γ k → Ty Γ k + | base : Nat → Ty Γ .star + | arrow : Ty Γ .star → Ty Γ .star → Ty Γ .star + | lam : Ty (k₁ :: Γ) k₂ → Ty Γ (.arr k₁ k₂) + | app : Ty Γ (.arr k₁ k₂) → Ty Γ k₁ → Ty Γ k₂ + +/-- Context minus a variable (Keller–Altenkirch `Γ - x`). -/ +def rem : {Γ : Ctx} → Var Γ k → Ctx + | _ :: Δ, .vz => Δ + | k' :: _, .vs x => k' :: rem x +termination_by structural x => x + +/-- Weaken a variable of `rem x` back into `Γ` (skipping `x`'s slot). -/ +def wkv : {Γ : Ctx} → (x : Var Γ k) → Var (rem x) j → Var Γ j + | _ :: _, .vz => fun y => .vs y + | _ :: _, .vs x => fun y => + match y with + | .vz => .vz + | .vs y => .vs (wkv x y) +termination_by structural x => x + +/-- Comparing two variables: either they are the same slot (same kind), or + the second avoids the first and lives in `rem Γ x`. -/ +inductive EqV : {Γ : Ctx} → Var Γ k → Var Γ j → Type where + | same : EqV x x + | diff : (x : Var Γ k) → (y : Var (rem x) j) → EqV x (wkv x y) + +/-- Decide which case of `EqV` holds. Total by structural recursion. -/ +def eqv : {Γ : Ctx} → (x : Var Γ k) → (y : Var Γ j) → EqV x y + | k₀ :: Δ, .vz => fun y => + match y with + | .vz => .same + | .vs y => EqV.diff (Γ := k₀ :: Δ) .vz y + | k₀ :: Δ, .vs x => fun y => + match y with + | .vz => EqV.diff (Γ := k₀ :: Δ) (.vs x) .vz + | .vs y => + match eqv x y with + | .same => .same + | .diff x y' => EqV.diff (Γ := k₀ :: Δ) (.vs x) (.vs y') +termination_by structural x => x + +/-- Index-independent size of a `Ty` (the termination measure for + weakening/substitution, whose `Ty` argument changes context index). -/ +def tySize : {Γ : Ctx} → {k : Kind} → Ty Γ k → Nat + | _, _, .var _ => 1 + | _, _, .base _ => 1 + | _, _, .arrow a b => tySize a + tySize b + 1 + | _, _, .lam b => tySize b + 1 + | _, _, .app f a => tySize f + tySize a + 1 +termination_by structural _ _ t => t + +/-- Weakening of `Ty` along one skipped slot (needed under binders). -/ +def wkTy : {Γ : Ctx} → (x : Var Γ k) → Ty (rem x) j → Ty Γ j + | _, x, .var y => .var (wkv x y) + | _, _, .base n => .base n + | _, x, .arrow a b => .arrow (wkTy x a) (wkTy x b) + | _, x, .lam b => .lam (wkTy (.vs x) b) + | _, x, .app f a => .app (wkTy x f) (wkTy x a) +termination_by _ _ t => tySize t +decreasing_by all_goals (simp only [tySize]; first | exact Nat.lt_succ_self _ | omega) + +/-- Syntactic (capture-avoiding) substitution on `Ty`, for stating β. + Substitutes slot `x` and removes it from the context. -/ +def substTy : {Γ : Ctx} → Ty Γ j → (x : Var Γ k) → Ty (rem x) k → Ty (rem x) j + | _, .var y, x, u => + match eqv x y with + | .same => u + | .diff _ y' => .var y' + | _, .base n, _, _ => .base n + | _, .arrow a b, x, u => .arrow (substTy a x u) (substTy b x u) + | _, .lam b, x, u => .lam (substTy b (.vs x) (wkTy .vz u)) + | _, .app f a, x, u => .app (substTy f x u) (substTy a x u) +termination_by _ t _ _ => tySize t +decreasing_by all_goals (simp only [tySize]; first | exact Nat.lt_succ_self _ | omega) + +/-- β-substitution of the top variable: `A[a₀ := B]`. + `rem (vz : Var (k::Γ) k) = Γ` definitionally, so this is well-typed. -/ +abbrev subst0 (b : Ty (k :: Γ) j) (u : Ty Γ k) : Ty Γ j := + substTy b .vz u + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L2/GradeAlgebra.lean b/verification/proofs/lean4/Systemet/L2/GradeAlgebra.lean new file mode 100644 index 0000000..5615e6a --- /dev/null +++ b/verification/proofs/lean4/Systemet/L2/GradeAlgebra.lean @@ -0,0 +1,62 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +/-! +# The L2 grade-algebra contract (ET-4) + +This class IS the precise statement of obligation ET-4 +(`docs/theory/OBLIGATIONS.adoc`): the laws a candidate grade algebra must +satisfy to be admissible at L2. An instance proof of this class for a +candidate `R` is the mechanical admissibility check. + +Reading of the components (docs/theory/03-l2-grades.adoc): +* `zero` — the grade of an unused assumption +* `one` — the grade of a single direct use +* `add` — context join (combining two uses of one assumption) +* `mul` — sequential composition / scaling under a graded modality +* `le` — subusage: `le r s` means grade `r` may stand where `s` is demanded + +Deliberately self-contained: no mathlib, so nothing here can drift with an +external library's class hierarchy. +-/ + +namespace Systemet.L2 + +/-- An ordered semiring: the admissibility contract for an L2 grade algebra. -/ +class GradeAlgebra (R : Type) where + add : R → R → R + mul : R → R → R + zero : R + one : R + le : R → R → Prop + /-- `add` is a commutative monoid with unit `zero`. -/ + add_assoc : ∀ a b c : R, add (add a b) c = add a (add b c) + add_comm : ∀ a b : R, add a b = add b a + add_zero : ∀ a : R, add a zero = a + /-- `mul` is a monoid with unit `one`, absorbing at `zero`. -/ + mul_assoc : ∀ a b c : R, mul (mul a b) c = mul a (mul b c) + one_mul : ∀ a : R, mul one a = a + mul_one : ∀ a : R, mul a one = a + zero_mul : ∀ a : R, mul zero a = zero + mul_zero : ∀ a : R, mul a zero = zero + /-- `mul` distributes over `add` on both sides. -/ + left_distrib : ∀ a b c : R, mul a (add b c) = add (mul a b) (mul a c) + right_distrib : ∀ a b c : R, mul (add a b) c = add (mul a c) (mul b c) + /-- `le` is a partial order. -/ + le_refl : ∀ a : R, le a a + le_trans : ∀ a b c : R, le a b → le b c → le a c + le_antisymm : ∀ a b : R, le a b → le b a → a = b + /-- The operations are monotone with respect to `le`. -/ + add_mono : ∀ a b c d : R, le a b → le c d → le (add a c) (add b d) + mul_mono : ∀ a b c d : R, le a b → le c d → le (mul a c) (mul b d) + +namespace GradeAlgebra + +variable {R : Type} [GradeAlgebra R] + +/-- `zero + a = a` — derived, so instances need not prove both unit laws. -/ +theorem zero_add (a : R) : add zero a = a := by + rw [add_comm]; exact add_zero a + +end GradeAlgebra + +end Systemet.L2 diff --git a/verification/proofs/lean4/Systemet/L2/Instances/Affine.lean b/verification/proofs/lean4/Systemet/L2/Instances/Affine.lean new file mode 100644 index 0000000..76fde9e --- /dev/null +++ b/verification/proofs/lean4/Systemet/L2/Instances/Affine.lean @@ -0,0 +1,82 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L2.GradeAlgebra +/-! +# The Affine grade algebra — `grade = Affine` (ET-5 instance) + +Carrier `{0, 1, ω}`: unused / exactly-once-available / unrestricted. +This is AffineScript's usage algebra (README §"Disciplines as a one-line +change of algebra"). The carrier is finite, so every law closes by `decide`. +-/ + +namespace Systemet.L2 + +inductive Affine : Type where + | zero : Affine + | one : Affine + | omega : Affine +deriving DecidableEq, Repr + +namespace Affine + +/-- Context join: a second use of anything makes it unrestricted. -/ +def add : Affine → Affine → Affine + | .zero, b => b + | a, .zero => a + | _, _ => .omega + +/-- Scaling: `zero` absorbs; `one` is neutral; `ω·ω = ω`. -/ +def mul : Affine → Affine → Affine + | .zero, _ => .zero + | _, .zero => .zero + | .one, b => b + | a, .one => a + | .omega, .omega => .omega + +/-- Subusage as a decidable Bool: `ω` accepts anything; otherwise exact. -/ +def leB : Affine → Affine → Bool + | .zero, .zero => true + | .one, .one => true + | _, .omega => true + | _, _ => false + +def le (a b : Affine) : Prop := leB a b = true + +instance (a b : Affine) : Decidable (le a b) := + inferInstanceAs (Decidable (leB a b = true)) + +/- Core Lean has no `Fintype`, so quantified goals over `Affine` are closed + by exhaustive case analysis rather than `decide`. Every case computes. -/ +instance grade : GradeAlgebra Affine where + add := add + mul := mul + zero := .zero + one := .one + le := le + add_assoc := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + add_comm := by intro a b; cases a <;> cases b <;> rfl + add_zero := by intro a; cases a <;> rfl + mul_assoc := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + one_mul := by intro a; cases a <;> rfl + mul_one := by intro a; cases a <;> rfl + zero_mul := by intro a; cases a <;> rfl + mul_zero := by intro a; cases a <;> rfl + left_distrib := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + right_distrib := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + le_refl := by intro a; cases a <;> rfl + le_trans := by + intro a b c hab hbc + cases a <;> cases b <;> cases c <;> simp_all [le, leB] + le_antisymm := by + intro a b hab hba + cases a <;> cases b <;> simp_all [le, leB] + add_mono := by + intro a b c d hab hcd + cases a <;> cases b <;> cases c <;> cases d <;> simp_all [le, leB, add] + mul_mono := by + intro a b c d hab hcd + cases a <;> cases b <;> cases c <;> cases d <;> simp_all [le, leB, mul] + +end Affine + +end Systemet.L2 diff --git a/verification/proofs/lean4/Systemet/L2/Instances/Lattice.lean b/verification/proofs/lean4/Systemet/L2/Instances/Lattice.lean new file mode 100644 index 0000000..16a5783 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L2/Instances/Lattice.lean @@ -0,0 +1,171 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L2.GradeAlgebra +/-! +# Lattice grade algebras — `grade = Low <= High` (ET-5 instance) + +The generic theorem: **every bounded distributive lattice is a grade +algebra**, with + +* `add` = `meet` (joining two uses takes the lower bound of what both allow), +* `mul` = `join` (sequential composition escalates), +* `zero` = `⊤` (an unused assumption constrains nothing), +* `one` = `⊥`, +* `le a b` = `meet a b = a` (the induced lattice order). + +Instantiated at the two-point information-flow lattice `Low ≤ High`. +The order-theoretic facts (idempotence, the meet/join characterizations of +the order, monotonicity of both operations) are derived from the absorption +laws in the classical way — nothing is assumed beyond the lattice axioms. +-/ + +namespace Systemet.L2 + +/-- A bounded distributive lattice, self-contained (no mathlib). -/ +class BoundedDistLattice (L : Type) where + meet : L → L → L + join : L → L → L + top : L + bot : L + meet_assoc : ∀ a b c : L, meet (meet a b) c = meet a (meet b c) + meet_comm : ∀ a b : L, meet a b = meet b a + join_assoc : ∀ a b c : L, join (join a b) c = join a (join b c) + join_comm : ∀ a b : L, join a b = join b a + absorb_meet : ∀ a b : L, meet a (join a b) = a + absorb_join : ∀ a b : L, join a (meet a b) = a + meet_top : ∀ a : L, meet a top = a + join_bot : ∀ a : L, join a bot = a + /-- Distributivity of `join` over `meet` (the direction `mul`-over-`add` + that the grade-algebra laws need). -/ + join_distrib : ∀ a b c : L, join a (meet b c) = meet (join a b) (join a c) + +namespace BoundedDistLattice + +variable {L : Type} [BoundedDistLattice L] + +theorem meet_idem (a : L) : meet a a = a := by + have h := absorb_meet a (meet a a) + rw [absorb_join] at h + exact h + +theorem join_idem (a : L) : join a a = a := by + have h := absorb_join a (meet a a) + rw [meet_idem] at h + rw [meet_idem] at h + exact h + +theorem join_top (a : L) : join a top = top := by + have h := absorb_join top a + rw [meet_comm, meet_top] at h + rw [join_comm] + exact h + +/-- The two order characterizations agree: `meet a b = a ↔ join a b = b`. -/ +theorem le_iff_join {a b : L} : meet a b = a ↔ join a b = b := by + constructor + · intro h + have := absorb_join b (meet b a) + calc join a b = join (meet a b) b := by rw [h] + _ = join b (meet b a) := by rw [join_comm, meet_comm] + _ = b := absorb_join b a + · intro h + calc meet a b = meet a (join a b) := by rw [h] + _ = a := absorb_meet a b + +/-- AC shuffle for `meet`: `(a∧c)∧(b∧d) = (a∧b)∧(c∧d)`. -/ +theorem meet_ac (a b c d : L) : + meet (meet a c) (meet b d) = meet (meet a b) (meet c d) := by + rw [meet_assoc, meet_assoc] + congr 1 + rw [← meet_assoc, ← meet_assoc] + congr 1 + exact meet_comm c b + +/-- AC shuffle for `join`. -/ +theorem join_ac (a b c d : L) : + join (join a c) (join b d) = join (join a b) (join c d) := by + rw [join_assoc, join_assoc] + congr 1 + rw [← join_assoc, ← join_assoc] + congr 1 + exact join_comm c b + +/-- Every bounded distributive lattice is an L2 grade algebra. -/ +instance grade : GradeAlgebra L where + add := meet + mul := join + zero := top + one := bot + le a b := meet a b = a + add_assoc := meet_assoc + add_comm := meet_comm + add_zero := meet_top + mul_assoc := join_assoc + one_mul := fun a => by rw [join_comm]; exact join_bot a + mul_one := join_bot + zero_mul := fun a => by rw [join_comm]; exact join_top a + mul_zero := join_top + left_distrib := join_distrib + right_distrib := fun a b c => by + rw [join_comm, join_distrib, join_comm, join_comm c] + le_refl := meet_idem + le_trans := fun a b c hab hbc => by + calc meet a c = meet (meet a b) c := by rw [hab] + _ = meet a (meet b c) := meet_assoc a b c + _ = meet a b := by rw [hbc] + _ = a := hab + le_antisymm := fun a b hab hba => by + calc a = meet a b := hab.symm + _ = meet b a := meet_comm a b + _ = b := hba + add_mono := fun a b c d hab hcd => by + calc meet (meet a c) (meet b d) = meet (meet a b) (meet c d) := meet_ac a b c d + _ = meet a c := by rw [hab, hcd] + mul_mono := fun a b c d hab hcd => by + have hab' := le_iff_join.mp hab + have hcd' := le_iff_join.mp hcd + apply le_iff_join.mpr + calc join (join a c) (join b d) = join (join a b) (join c d) := join_ac a b c d + _ = join b d := by rw [hab', hcd'] + +end BoundedDistLattice + +/-- The two-point information-flow lattice: `Low ≤ High`. -/ +inductive Level : Type where + | low : Level + | high : Level +deriving DecidableEq, Repr + +namespace Level + +/-- `meet` (with `Low` as bottom-of-information, `High` as top). -/ +def meet : Level → Level → Level + | .high, .high => .high + | _, _ => .low + +def join : Level → Level → Level + | .low, .low => .low + | _, _ => .high + +instance lattice : BoundedDistLattice Level where + meet := meet + join := join + top := .high + bot := .low + meet_assoc := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + meet_comm := by intro a b; cases a <;> cases b <;> rfl + join_assoc := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + join_comm := by intro a b; cases a <;> cases b <;> rfl + absorb_meet := by intro a b; cases a <;> cases b <;> rfl + absorb_join := by intro a b; cases a <;> cases b <;> rfl + meet_top := by intro a; cases a <;> rfl + join_bot := by intro a; cases a <;> rfl + join_distrib := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + +/-- `Level` is a grade algebra — via the generic theorem, not a bespoke proof. + This is ET-5's "same rules, different algebra" in one line. -/ +example : GradeAlgebra Level := inferInstance + +end Level + +end Systemet.L2 diff --git a/verification/proofs/lean4/Systemet/L2/Instances/Product.lean b/verification/proofs/lean4/Systemet/L2/Instances/Product.lean new file mode 100644 index 0000000..7344c37 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L2/Instances/Product.lean @@ -0,0 +1,64 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L2.GradeAlgebra +/-! +# The product construction — `grade = Latency x Billing` (ET-5 instance) + +If `R` and `S` are grade algebras, so is `R × S`, componentwise. This is the +point of the README's `Latency x Billing` row: a composite discipline is +*composition of algebras*, not a new checker. Proven once, generically. +-/ + +namespace Systemet.L2 + +open GradeAlgebra + +instance prodGrade {R S : Type} [GradeAlgebra R] [GradeAlgebra S] : GradeAlgebra (R × S) where + add a b := (add a.1 b.1, add a.2 b.2) + mul a b := (mul a.1 b.1, mul a.2 b.2) + zero := (zero, zero) + one := (one, one) + le a b := le a.1 b.1 ∧ le a.2 b.2 + add_assoc a b c := by + show (_, _) = (_, _) + rw [add_assoc a.1 b.1 c.1, add_assoc a.2 b.2 c.2] + add_comm a b := by + show (_, _) = (_, _) + rw [add_comm a.1 b.1, add_comm a.2 b.2] + add_zero a := by + show (_, _) = (_, _) + rw [add_zero a.1, add_zero a.2] + mul_assoc a b c := by + show (_, _) = (_, _) + rw [mul_assoc a.1 b.1 c.1, mul_assoc a.2 b.2 c.2] + one_mul a := by + show (_, _) = (_, _) + rw [one_mul a.1, one_mul a.2] + mul_one a := by + show (_, _) = (_, _) + rw [mul_one a.1, mul_one a.2] + zero_mul a := by + show (_, _) = (_, _) + rw [zero_mul a.1, zero_mul a.2] + mul_zero a := by + show (_, _) = (_, _) + rw [mul_zero a.1, mul_zero a.2] + left_distrib a b c := by + show (_, _) = (_, _) + rw [left_distrib a.1 b.1 c.1, left_distrib a.2 b.2 c.2] + right_distrib a b c := by + show (_, _) = (_, _) + rw [right_distrib a.1 b.1 c.1, right_distrib a.2 b.2 c.2] + le_refl a := ⟨le_refl a.1, le_refl a.2⟩ + le_trans a b c hab hbc := + ⟨le_trans _ _ _ hab.1 hbc.1, le_trans _ _ _ hab.2 hbc.2⟩ + le_antisymm a b hab hba := by + have h1 := le_antisymm _ _ hab.1 hba.1 + have h2 := le_antisymm _ _ hab.2 hba.2 + exact Prod.ext h1 h2 + add_mono a b c d hab hcd := + ⟨add_mono _ _ _ _ hab.1 hcd.1, add_mono _ _ _ _ hab.2 hcd.2⟩ + mul_mono a b c d hab hcd := + ⟨mul_mono _ _ _ _ hab.1 hcd.1, mul_mono _ _ _ _ hab.2 hcd.2⟩ + +end Systemet.L2 diff --git a/verification/proofs/lean4/Systemet/L2/Instances/Tropical.lean b/verification/proofs/lean4/Systemet/L2/Instances/Tropical.lean new file mode 100644 index 0000000..58ed6cf --- /dev/null +++ b/verification/proofs/lean4/Systemet/L2/Instances/Tropical.lean @@ -0,0 +1,107 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L2.GradeAlgebra +/-! +# The Cost grade algebra — `grade = Cost * Nat` (ET-5 instance) + +Tropical-style cost accounting over `ℕ ∪ {∞}`: + +* `add` = `min` — joining two uses keeps the cheaper bound; +* `mul` = numeric `+` — sequential composition accumulates cost; +* `zero` = `∞` — an unused assumption consumes no budget (identity for `min`, + absorbing for `+`); +* `one` = `0` — a single direct use is free at this layer; +* `le` — `fin m ≤ fin n ↔ m ≤ n`, and everything is `≤ inf`. + +This fixes one of the two sensible readings named in +docs/theory/09-grade-algebra-catalogue.adoc; the checklist there is +"verified" for exactly this reading. +-/ + +namespace Systemet.L2 + +inductive Cost : Type where + | fin : Nat → Cost + | inf : Cost +deriving DecidableEq, Repr + +namespace Cost + +/-- `Nat.min` is monotone in both arguments (`omega` treats `min` as opaque, + so this is discharged by unfolding to the conditional first). -/ +private theorem nat_min_le_min {a b c d : Nat} (h1 : a ≤ b) (h2 : c ≤ d) : + Nat.min a c ≤ Nat.min b d := by + simp only [Nat.min_def] + split <;> split <;> omega + +/-- Join = min: `inf` is the identity. -/ +def add : Cost → Cost → Cost + | .fin m, .fin n => .fin (Nat.min m n) + | .inf, b => b + | a, .inf => a + +/-- Sequential composition = plus: `inf` absorbs. -/ +def mul : Cost → Cost → Cost + | .fin m, .fin n => .fin (m + n) + | _, _ => .inf + +/-- The natural cost order, with `inf` on top. -/ +def le : Cost → Cost → Prop + | .fin m, .fin n => m ≤ n + | _, .inf => True + | .inf, .fin _ => False + +instance : (a b : Cost) → Decidable (le a b) + | .fin _, .fin _ => inferInstanceAs (Decidable (_ ≤ _)) + | .fin _, .inf => inferInstanceAs (Decidable True) + | .inf, .inf => inferInstanceAs (Decidable True) + | .inf, .fin _ => inferInstanceAs (Decidable False) + +instance grade : GradeAlgebra Cost where + add := add + mul := mul + zero := .inf + one := .fin 0 + le := le + add_assoc := by + intro a b c + cases a <;> cases b <;> cases c <;> simp [add, Nat.min_assoc] + add_comm := by + intro a b + cases a <;> cases b <;> simp [add, Nat.min_comm] + add_zero := by intro a; cases a <;> rfl + mul_assoc := by + intro a b c + cases a <;> cases b <;> cases c <;> simp [mul, Nat.add_assoc] + one_mul := by intro a; cases a <;> simp [mul] + mul_one := by intro a; cases a <;> simp [mul] + zero_mul := by intro a; cases a <;> rfl + mul_zero := by intro a; cases a <;> rfl + left_distrib := by + intro a b c + cases a <;> cases b <;> cases c <;> simp [mul, add, Nat.add_min_add_left] + right_distrib := by + intro a b c + cases a <;> cases b <;> cases c <;> simp [mul, add, Nat.add_min_add_right] + le_refl := by intro a; cases a <;> simp [le] + le_trans := by + intro a b c hab hbc + cases a <;> cases b <;> cases c <;> simp_all [le] <;> omega + le_antisymm := by + intro a b hab hba + cases a <;> cases b <;> simp_all [le] <;> omega + add_mono := by + intro a b c d hab hcd + cases a <;> cases b <;> cases c <;> cases d <;> simp_all [le, add] <;> + first + | omega + | (apply nat_min_le_min <;> assumption) + | (exact Nat.le_trans (Nat.min_le_left _ _) (by assumption)) + | (exact Nat.le_trans (Nat.min_le_right _ _) (by assumption)) + mul_mono := by + intro a b c d hab hcd + cases a <;> cases b <;> cases c <;> cases d <;> simp_all [le, mul] <;> omega + +end Cost + +end Systemet.L2 diff --git a/verification/proofs/lean4/lake-manifest.json b/verification/proofs/lean4/lake-manifest.json new file mode 100644 index 0000000..5683af0 --- /dev/null +++ b/verification/proofs/lean4/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "systemet", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/verification/proofs/lean4/lakefile.toml b/verification/proofs/lean4/lakefile.toml new file mode 100644 index 0000000..388426a --- /dev/null +++ b/verification/proofs/lean4/lakefile.toml @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +# Hermetic by design: no `require` lines — core Lean only, nothing can float. +name = "systemet" +defaultTargets = ["Systemet"] + +[[lean_lib]] +name = "Systemet" diff --git a/verification/proofs/lean4/lean-toolchain b/verification/proofs/lean4/lean-toolchain new file mode 100644 index 0000000..94b9f49 --- /dev/null +++ b/verification/proofs/lean4/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.0