diff --git a/.github/workflows/proof-corpus.yml b/.github/workflows/proof-corpus.yml new file mode 100644 index 0000000..be9c620 --- /dev/null +++ b/.github/workflows/proof-corpus.yml @@ -0,0 +1,67 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# proof-corpus.yml — machine-checks the git-reticulator Idris2 proof corpus. +# +# First mechanized proofs for the lattice core (see PROOF-NEEDS.md): elementary +# order theory (P1a witnessed, P2a essence). The gate fails if the corpus stops +# typechecking under idris2 0.8.0, or if a proof-escape symbol is introduced. +# Mirrors the canonical vcl-ut `proof-corpus.yml`, plus `libgmp-dev` (required by +# the Idris2 RefC support lib and missing from the vcl-ut recipe). + +name: Proof Corpus + +on: + pull_request: + branches: ['**'] + push: + branches: [main, master] + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + machine-check: + name: idris2 0.8.0 --build git-reticulator-proofs + runs-on: ubuntu-latest + timeout-minutes: 30 + + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + + # Idris2 0.8.0 from PINNED official source (tag v0.8.0 == this commit). + # No maintained setup action exists; a SHA-pinned source build is + # deterministic and depends on no third-party action. + - name: Build & install Idris2 0.8.0 from pinned source + run: | + set -euo pipefail + sudo apt-get update -qq + sudo apt-get install -y --no-install-recommends chezscheme make gcc libgmp-dev + git clone --no-checkout https://github.com/idris-lang/Idris2.git /tmp/Idris2 + git -C /tmp/Idris2 checkout 15a3e4e70843f7a34100f6470c04b791330788df + make -C /tmp/Idris2 bootstrap SCHEME=chezscheme + make -C /tmp/Idris2 install PREFIX="$HOME/.idris2" + echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" + echo "IDRIS2_PREFIX=$HOME/.idris2" >> "$GITHUB_ENV" + + - name: Proof-escape audit (no believe_me / postulate / assert_* / sorry) + run: | + set -euo pipefail + files="verification/proofs/Lattice/Order.idr" + if grep -nE '\b(believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry)\b' \ + $files | grep -vE ':\s*(--|\|\|\|)' ; then + echo "::error::proof-escape symbol found in the corpus" + exit 1 + fi + echo "OK: zero proof-escape symbols outside comments" + + - name: Build the proof corpus + run: | + set -euo pipefail + idris2 --version + cd verification/proofs && idris2 --build git-reticulator-proofs.ipkg diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index e6e3d2e..2eede0e 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -5,8 +5,11 @@ ## Current State - **LOC**: ~237 Rust (host) + ~100 AffineScript (`.affine`, not compilable). -- **Existing proofs**: **NONE.** No `*.idr`, `*.v`, `*.lean`, `*.agda`, `*.fst`, - `*.tla`, `*.ads`. The 2026-05-26 estate tech-debt audit recorded +- **Existing proofs**: **first corpus landed (2026-06-04)** — + `verification/proofs/Lattice/Order.idr` (Idris2 0.8.0, `%default total`, zero + proof escapes), CI-gated by `.github/workflows/proof-corpus.yml`. It proves the + *abstract* order theory, **not yet** bound to the Rust graph (see below). Before + this there were zero proofs. The 2026-05-26 estate tech-debt audit recorded "Proof debt: none / Recommended next move: none" — that verdict is **wrong** for a project whose headline noun is *lattice*. A lattice is a mathematical claim with discharge obligations; asserting it without proof is exactly the @@ -36,6 +39,15 @@ Honest categorisation. **Proved** = mechanically checked (Idris2/Coq/SPARK). (`src/lattice/mod.rs`) — a rung *below* proof. git-reticulator has **zero mechanized proofs**; what exists is tested. +### Done (mechanized — first corpus, 2026-06-04) +- **Abstract order theory** (`verification/proofs/Lattice/Order.idr`, Idris2 0.8.0, + `%default total`, zero proof escapes; CI-gated by `proof-corpus.yml`): the + partial-order laws are witnessed (`natOrder`: reflexive + transitive + + antisymmetric) and **antisymmetry ⇒ no 2-cycle** (`noTwoCycle`) is proved — the + order-theoretic heart of why the SCC condensation is a DAG (**P2a**). **Scope + honesty:** proved on an *abstract* `PartialOrder`, **not yet** on the actual Rust + graph in `src/lattice/mod.rs`; binding the two is the ADR-006 Idris2 ABI seam. + ### Done (tested, not proved) - **P2a** SCC condensation is acyclic — `Condensation::is_acyclic` (Kahn topological sort, a genuine runtime check, not a trust assertion) + tests @@ -60,7 +72,9 @@ mechanized proofs**; what exists is tested. is zero-because-empty. Recorded so it is never mistaken for rigour we lack. ### Structural blockers -- No prover wired (Idris2 recommended, absent; no proof-corpus CI gate). +- Idris2 prover **now wired** (`verification/proofs/` + `proof-corpus.yml`, idris2 + 0.8.0); first module verified. Remaining: bind the proofs to the Rust graph and + discharge the rest of P1–P7. - The verifiable core is migrating to AffineScript (ADR-006), itself alpha with the CORE-01 soundness gap. - The Rust/SPARK Idris2/Zig ABI seam is **N/A until git-reticulator exposes an diff --git a/verification/proofs/.gitignore b/verification/proofs/.gitignore new file mode 100644 index 0000000..7127129 --- /dev/null +++ b/verification/proofs/.gitignore @@ -0,0 +1,2 @@ +# Idris2 build outputs +build/ diff --git a/verification/proofs/Lattice/Order.idr b/verification/proofs/Lattice/Order.idr new file mode 100644 index 0000000..9a343c2 --- /dev/null +++ b/verification/proofs/Lattice/Order.idr @@ -0,0 +1,84 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +||| +||| Elementary order-theory obligations for the git-reticulator core, machine +||| checked. This is the first mechanized proof in the repo (PROOF-NEEDS.md: +||| "zero proofs" -> a foothold on P1a/P2a), %default total, zero proof escapes, +||| matching the estate's vcl-ut corpus discipline. +||| +||| It does NOT yet prove the properties of the *actual* Rust graph in +||| `src/lattice/mod.rs`; it proves the order-theoretic facts that justify why +||| that code is correct, on an abstract model, and exhibits a concrete witness. +||| Connecting these to the running condensation is the next step (ADR-006: the +||| Idris2 ABI seam will carry these as obligations). +module Lattice.Order + +%default total + +-------------------------------------------------------------------------------- +-- Order-theoretic predicates (the shape a genuine partial order must have) +-------------------------------------------------------------------------------- + +||| Reflexivity of a relation. +public export +IsRefl : {a : Type} -> (rel : a -> a -> Type) -> Type +IsRefl {a} rel = (x : a) -> rel x x + +||| Transitivity of a relation. +public export +IsTrans : {a : Type} -> (rel : a -> a -> Type) -> Type +IsTrans {a} rel = {x, y, z : a} -> rel x y -> rel y z -> rel x z + +||| Antisymmetry of a relation. +public export +IsAntisym : {a : Type} -> (rel : a -> a -> Type) -> Type +IsAntisym {a} rel = {x, y : a} -> rel x y -> rel y x -> x = y + +||| A partial order bundles a relation with proofs of the three laws. +public export +record PartialOrder (a : Type) where + constructor MkPO + rel : a -> a -> Type + prf_refl : IsRefl rel + prf_trans : IsTrans rel + prf_antisym : IsAntisym rel + +-------------------------------------------------------------------------------- +-- P2a (essence): antisymmetry forbids cycles +-------------------------------------------------------------------------------- + +||| The condensation order computed in `src/lattice/mod.rs` is antisymmetric by +||| construction (distinct strongly-connected components cannot mutually reach). +||| Antisymmetry is exactly what makes it a DAG: any two-cycle collapses to a +||| single point. This is the order-theoretic heart of `Condensation::is_acyclic`. +export +noTwoCycle : {x, y : a} -> (po : PartialOrder a) -> rel po x y -> rel po y x -> x = y +noTwoCycle po p q = prf_antisym po p q + +-------------------------------------------------------------------------------- +-- A concrete witness: <= on Nat is a partial order (so the bundle is inhabited) +-------------------------------------------------------------------------------- + +||| Standing in for "component a reaches component b" on the acyclic condensation. +public export +data Leq : Nat -> Nat -> Type where + LeZ : Leq Z n + LeS : Leq m n -> Leq (S m) (S n) + +leqRefl : (n : Nat) -> Leq n n +leqRefl Z = LeZ +leqRefl (S k) = LeS (leqRefl k) + +leqTrans : {x, y, z : Nat} -> Leq x y -> Leq y z -> Leq x z +leqTrans LeZ _ = LeZ +leqTrans (LeS p) (LeS q) = LeS (leqTrans p q) + +leqAntisym : {x, y : Nat} -> Leq x y -> Leq y x -> x = y +leqAntisym LeZ LeZ = Refl +leqAntisym (LeS p) (LeS q) = cong S (leqAntisym p q) + +||| P1a (witnessed): the reachability order on the condensation is a genuine +||| partial order — reflexive, transitive, antisymmetric. +public export +natOrder : PartialOrder Nat +natOrder = MkPO Leq leqRefl leqTrans leqAntisym diff --git a/verification/proofs/git-reticulator-proofs.ipkg b/verification/proofs/git-reticulator-proofs.ipkg new file mode 100644 index 0000000..1cf8e5c --- /dev/null +++ b/verification/proofs/git-reticulator-proofs.ipkg @@ -0,0 +1,14 @@ +package git-reticulator-proofs + +-- SPDX-License-Identifier: MPL-2.0 +-- git-reticulator Idris2 proof corpus. First mechanized proofs (PROOF-NEEDS.md): +-- elementary order theory (P1a witnessed, P2a essence) for the lattice core. +-- %default total, zero proof-escape symbols — matches the vcl-ut corpus bar. + +version = 0.1.0 +authors = "Jonathan D.A. Jewell " +brief = "git-reticulator order-theory proof corpus (P1a/P2a)" +license = "MPL-2.0" + +sourcedir = "." +modules = Lattice.Order