From dfaf642359c524413aef4a1db81d1c838ed8d17a Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 00:15:34 -0500 Subject: [PATCH 01/10] ci: check statement files for the headline results and reject opaque constants spec/Spec.lean restates each headline result with sorry as its proof. spec/Check.lean compares every statement there with the library declaration of the same name: equal types up to binder names, a theorem with a proof term, axioms within propext, Classical.choice and Quot.sound, and a statement that is sorry rather than proved. CI runs it and requires a statement for every headline result. The headline list moves to one workflow-level variable read by both checks. The environment check now also rejects opaque constants, which neither #print axioms nor a text search reports, and its self-test fixture declares both an axiom and an opaque constant. The obligation behind the two continuum theorems gets a citable name, gap:pde-infra, in their docstrings and the docs. AGENTS.md describes the checks as they now run and adds a sandbox for elaborating prover output. --- .github/workflows/lean_action_ci.yml | 89 +++++++++++----- AGENTS.md | 49 +++++++-- CdFormal/Theorems.lean | 10 +- README.md | 5 +- docs/explanation/axiom-boundary.md | 4 + docs/reference/theorems.md | 4 +- docs/reference/verification-audit.md | 9 +- lakefile.toml | 6 ++ spec/Check.lean | 74 +++++++++++++ spec/Spec.lean | 149 +++++++++++++++++++++++++++ 10 files changed, 355 insertions(+), 44 deletions(-) create mode 100644 spec/Check.lean create mode 100644 spec/Spec.lean diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 6ac820a..faba940 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -14,6 +14,17 @@ concurrency: env: ELAN_HOME: /home/runner/.elan + # The headline results. Kept in the workflow, not in Verify.lean or spec/, so that dropping one + # from the axiom dashboard or from the statement files fails CI. + HEADLINE_RESULTS: >- + SemioticBVP.exists_isWeakCoherentConfiguration + SemioticBVP.exists_pos_isWeakCoherentConfiguration + SemioticGraph.exists_pos_graph + SemioticGraph.exists_pos_graph_of_unweighted + spectral_characterization_1d + linfty_bound_algebraic + monotone_fixed_point_between + scaling_uniqueness jobs: # CONTRACT: org ruleset requires this exact check name 'build' @@ -86,7 +97,7 @@ jobs: run: lake lint # Verify.lean lists the selected declarations, which must include the headline results named - # below. Each needs exactly one record, and every record may use only propext, + # in HEADLINE_RESULTS. Each needs exactly one record, and every record may use only propext, # Classical.choice and Quot.sound. - name: Check axioms if: ${{ !cancelled() && steps.build.outcome == 'success' }} @@ -94,7 +105,7 @@ jobs: set -o pipefail lake env lean -DwarningAsError=true CdFormal/Verify.lean 2>&1 | tee "$RUNNER_TEMP/axioms.txt" python3 - "$RUNNER_TEMP/axioms.txt" <<'EOF' - import collections, pathlib, re, sys + import collections, os, pathlib, re, sys source = pathlib.Path("CdFormal/Verify.lean").read_text(encoding="utf-8") expected = re.findall(r"^#print axioms (\S+)\s*$", source, re.M) lines = [] @@ -116,13 +127,9 @@ jobs: errors.append(f"{m[1]} uses {sorted(used - allowed)}") if not expected: errors.append("Verify.lean selects no declarations") - # Kept here, not in Verify.lean, so that deselecting a headline result fails the check. - headline = ["SemioticBVP.exists_isWeakCoherentConfiguration", - "SemioticBVP.exists_pos_isWeakCoherentConfiguration", - "SemioticGraph.exists_pos_graph", - "SemioticGraph.exists_pos_graph_of_unweighted", - "spectral_characterization_1d", "linfty_bound_algebraic", - "monotone_fixed_point_between", "scaling_uniqueness"] + headline = os.environ["HEADLINE_RESULTS"].split() + if not headline: + errors.append("HEADLINE_RESULTS is empty") for name in headline: if name not in expected: errors.append(f"headline result {name} is not selected in Verify.lean") @@ -142,6 +149,32 @@ jobs: "results, one record each, using only propext, Classical.choice and Quot.sound.") EOF + # spec/Spec.lean restates each headline result with `sorry` as its proof: the statement is + # the specification. spec/Check.lean compares every statement there with the library + # declaration of the same name (type up to binder names, a theorem with a proof term, + # axioms within the allowlist) and rejects a statement file that proves instead of states. + - name: Check statement files + if: ${{ !cancelled() && steps.build.outcome == 'success' }} + run: | + set -o pipefail + lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt" + # The statement files may warn only about their own `sorry` proofs. + other=$(grep -E '^(warning|error)' "$RUNNER_TEMP/spec-build.txt" | + grep -v 'declaration uses `sorry`' || true) + if [ -n "$other" ]; then + echo "::error::the statement files build with a warning other than their sorry proofs" + exit 1 + fi + lake env lean spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" + missing="" + for name in $HEADLINE_RESULTS; do + grep -qx "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name" + done + if [ -n "$missing" ]; then + echo "::error::headline results without a matching statement:$missing" + exit 1 + fi + # Every Lean name written in inline code in the README and the docs, and every declaration # shown in a Lean code block there, must resolve. - name: Check documented names @@ -177,29 +210,35 @@ jobs: fi echo "$(grep -c '^#check' "$RUNNER_TEMP/DocNames.lean") documented names resolve." - # No axiom may be declared in any CdFormal module, even one that no selected declaration - # uses. The check reads the compiled environment, so it cannot be fooled by layout. It first - # proves it can fail: a module declaring a two-line axiom must be reported. - - name: Check that no axiom is declared + # No axiom and no opaque constant may be declared in any CdFormal module, even one that no + # selected declaration uses: the kernel cannot see an opaque constant's value, and neither + # #print axioms nor a text search reports one. The check reads the compiled environment, so + # it cannot be fooled by layout. It first proves it can fail: a module declaring a two-line + # axiom and an opaque constant must have both reported. + - name: Check that no axiom or opaque constant is declared if: ${{ !cancelled() && steps.build.outcome == 'success' }} run: | cat > "$RUNNER_TEMP/axiom_check.lean" <<'EOF' open Lean in #eval show CoreM Unit from do let env ← getEnv - let mut found := #[] + let mut axioms := #[] + let mut opaques := #[] let mut modules := 0 for mod in env.header.moduleNames, data in env.header.moduleData do if mod.getRoot == `CdFormal then modules := modules + 1 for c in data.constants do - if c matches .axiomInfo _ then found := found.push c.name - unless found.isEmpty do throwError "axioms declared in CdFormal: {found}" - IO.println s!"no axiom declared in any of {modules} CdFormal modules" + if c matches .axiomInfo _ then axioms := axioms.push c.name + if c matches .opaqueInfo _ then opaques := opaques.push c.name + unless axioms.isEmpty && opaques.isEmpty do + throwError "axioms declared in CdFormal: {axioms}; opaque constants: {opaques}" + IO.println s!"no axiom or opaque constant declared in {modules} CdFormal modules" EOF fixture=CdFormal/CiAxiomFixture.lean trap 'rm -f "$fixture" .lake/build/lib/lean/CdFormal/CiAxiomFixture.*' EXIT - printf 'import CdFormal.Basic\n\naxiom\n ciAxiomFixture : False\n' > "$fixture" + printf '%s\n' 'import CdFormal.Basic' '' 'axiom' ' ciAxiomFixture : False' '' \ + 'opaque ciOpaqueFixture : Nat' > "$fixture" lake build CdFormal.CiAxiomFixture { echo 'import CdFormal.CiAxiomFixture'; cat "$RUNNER_TEMP/axiom_check.lean"; } \ > "$RUNNER_TEMP/SelfTest.lean" @@ -207,9 +246,9 @@ jobs: status=0 lake env lean "$RUNNER_TEMP/SelfTest.lean" > "$RUNNER_TEMP/selftest.txt" 2>&1 || status=$? cat "$RUNNER_TEMP/selftest.txt" - if [ "$status" -eq 0 ] || - ! grep -qF 'axioms declared in CdFormal: [ciAxiomFixture]' "$RUNNER_TEMP/selftest.txt"; then - echo "::error::the axiom self-test did not report ciAxiomFixture" + expected='axioms declared in CdFormal: [ciAxiomFixture]; opaque constants: [ciOpaqueFixture]' + if [ "$status" -eq 0 ] || ! grep -qF "$expected" "$RUNNER_TEMP/selftest.txt"; then + echo "::error::the self-test did not report ciAxiomFixture and ciOpaqueFixture" exit 1 fi rm -f "$fixture" .lake/build/lib/lean/CdFormal/CiAxiomFixture.* @@ -223,7 +262,8 @@ jobs: shell: python run: | import pathlib, re, subprocess, sys - files = subprocess.run(["git", "ls-files", "CdFormal.lean", "CdFormal/*.lean"], + files = subprocess.run(["git", "ls-files", "CdFormal.lean", "CdFormal/*.lean", + "spec/*.lean"], capture_output=True, text=True, check=True).stdout.split() header = re.compile(r"/-\nCopyright \(c\) 20\d\d [^\n]+\. All rights reserved\.\n" r"Released under Apache 2\.0 license as described in the file LICENSE\.\n" @@ -243,8 +283,9 @@ jobs: sys.exit("header check failed:\n " + "\n ".join(bad or ["no files"])) print(f"{len(files)} files have a copyright header and a module docstring after the imports.") - # 'sorry' and 'sorryAx' may not appear anywhere in the Lean sources, comments included, and - # no axiom may be declared. + # 'sorry' and 'sorryAx' may not appear anywhere in the library sources, comments included. + # The statement files under spec/ are outside this audit: their proofs are sorry by design, + # and the statement-file check requires it. - name: Audit placeholders if: ${{ !cancelled() }} run: | diff --git a/AGENTS.md b/AGENTS.md index d5c4ebb..4461c3d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -28,7 +28,9 @@ A formalization of the existence theory for the Creative Determinant problem ## Invariants -- **No `sorry` on the default branch.** Every declaration is fully proved before merge. +- **No `sorry` in the library on the default branch.** Every declaration under `CdFormal/` is + fully proved before merge. The statement files under `spec/` are the one exception: each + restates a headline result with `sorry` as its proof, and CI requires that. - **No `axiom` declarations.** Classical results that are not proved are assumed through a typeclass or structure field (see *Assumed results*, which needs approval), never through `axiom`. @@ -59,13 +61,20 @@ lake exe cache get # Mathlib oleans; never bui lake build --wfail # warnings are errors (includes sorry) lake lint # Mathlib environment linters lake env lean -DwarningAsError=true /Verify.lean # axiom dashboard +lake build Spec && lake env lean spec/Check.lean # statement files against the library ``` - `CdFormal/Verify.lean` holds exactly one `#print axioms` record per selected declaration: every headline result and the supporting declarations the docs cite. The headline results - are listed in the CI workflow, not in `Verify.lean`, so dropping one from the dashboard - fails CI; add a new headline result to both. Every record may use only `propext`, - `Classical.choice` and `Quot.sound`. + are listed once, in the CI workflow (`HEADLINE_RESULTS`), not in `Verify.lean` or `spec/`, + so dropping one from the dashboard or from the statement files fails CI. Add a new headline + result to all three: the workflow list, a `#print axioms` record, and a statement in + `spec/Spec.lean` copied from the source with its proof replaced by `sorry`. Every record may + use only `propext`, `Classical.choice` and `Quot.sound`. +- A statement file states; it does not prove. `spec/Check.lean` rejects a statement whose proof + is not `sorry`, a statement whose type differs from the library declaration of the same name + (binder names and annotations aside), a library declaration that is not a theorem, and a + library proof whose axioms leave the allowlist. - If the sandbox cannot install Lean or fetch the Mathlib cache, push to a draft PR and let CI build and verify. Report which checks ran where; never claim a local build that did not happen. @@ -76,9 +85,12 @@ lake env lean -DwarningAsError=true /Verify.lean # axiom dashboard - Test the checkers themselves. An axiom or `sorry` gate that silently passes is worse than none (a pipe without `pipefail` once hid Lean failures here). When you add or change a gate, also add a small negative fixture that must fail it and a snapshot of expected - axiom output that its parser must accept. This repo's CI has neither yet: after changing - the axiom check or the audit, test it by hand against a file that uses `sorry` or declares - an `axiom`. + axiom output that its parser must accept. In this repo's CI only the environment check + carries a fixture (an `axiom` and an `opaque` constant it must report). After changing the + axiom dashboard parser, the statement-file comparator or the audit, test them by hand: a + file that uses `sorry`, a statement with a changed hypothesis, a statement proved instead + of stated, and a library proof that uses native evaluation (which declares an auxiliary + axiom under Lean v4.34.1). - Change `lake-manifest.json` only in an intentional dependency bump. No CI guard enforces this here; check the diff yourself. - If a repo has a docs site, `uv run zensical build` must succeed; CI also checks the @@ -88,14 +100,18 @@ lake env lean -DwarningAsError=true /Verify.lean # axiom dashboard - `lake build --wfail` of the root and every module, then `lake lint`; - the axiom check: the selection includes every headline result, one record each, all within the allowlist; + - the statement-file check: every headline result has a statement in `spec/Spec.lean`, and + every statement there matches its library declaration as described above; - the documented-names check: every inline-code token in the README and docs that looks like a Lean name containing an uppercase letter, `_` or `.`, and every declaration shown in a Lean code block there, must resolve (all-lowercase names are not checked); - the header check: every file has the copyright header and a module docstring after the imports (Lean itself rejects an `import` after any command, so imports come first); - - the placeholder audit: no `sorry` or `sorryAx` anywhere, and no line that starts an - `axiom` declaration (a text search; `#print axioms` still catches any axiom a selected - result uses); + - the placeholder audit: no `sorry` or `sorryAx` anywhere in the library sources, comments + included (a text search; `spec/` is outside it by design); + - the environment check: no module of the library declares an `axiom` or an `opaque` + constant, read from the compiled environment, after a self-test with a fixture that + declares both; - the docs build, and a link check that also verifies fragments. Everything else in this file is a convention to follow, not an automated gate. - If a repo has a `Makefile`, use its targets (`build`, `verify`, `audit`, `lint`) as @@ -407,5 +423,18 @@ Aristotle grinds leaf lemmas and detects dependencies. It is not the theorem arc `pp.all`; none of them belongs in a leaf proof. - Rebuild with `lake build --wfail`: Aristotle doesn't run the project's style linters. - Before trusting output, check Aristotle's Lean version against `lean-toolchain`. +- Elaborating a file runs code (`#eval`, `initialize`, tactics, macros), so elaborate a + returned file in a sandbox before it touches the repository: no network, home directory + hidden, the project read-only. With bubblewrap, from the project root: + + ```bash + bwrap --ro-bind /usr /usr --symlink usr/lib /lib --symlink usr/lib /lib64 \ + --symlink usr/bin /bin --ro-bind /etc /etc --tmpfs "$HOME" \ + --ro-bind "$HOME/.elan" "$HOME/.elan" --ro-bind "$PWD" "$PWD" \ + --ro-bind /untrusted --proc /proc --dev /dev --tmpfs /tmp \ + --unshare-all --die-with-parent --chdir "$PWD" lake env lean /untrusted/.lean + ``` + + Adjust the binds to where elan and the toolchain live on your machine. - Keep raw prover artifacts and run logs out of the public repository. Commit only the rewritten proofs, and credit Aristotle in the README. diff --git a/CdFormal/Theorems.lean b/CdFormal/Theorems.lean index 184c608..8ba4a39 100644 --- a/CdFormal/Theorems.lean +++ b/CdFormal/Theorems.lean @@ -93,7 +93,10 @@ checked; the hypotheses are assumed and appear as arguments. -/ Uses `PDEInfra.T_compact`, `PDEInfra.linfty_bound`, `PDEInfra.schaefer`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. With the default - `SemioticBVP.equation`, Φ ≡ 0 is already a solution (`zero_solves_equation`). -/ + `SemioticBVP.equation`, Φ ≡ 0 is already a solution (`zero_solves_equation`). + + Conditional: the obligation to meet these hypotheses is the named gap `gap:pde-infra` + (docs/explanation/axiom-boundary.md). -/ theorem SemioticBVP.exists_isWeakCoherentConfiguration (bvp : SemioticBVP n M) (solOp : SolutionOperator bvp) @@ -117,7 +120,10 @@ theorem SemioticBVP.exists_isWeakCoherentConfiguration Note: The paper's Thm 3.16 says "assume the hypotheses of Thm 3.12" (including bounded b). This Lean statement omits `B`/`hB` because `monotone_iteration` uses sub/super-solution theory that does not - require an explicit bound on b. -/ + require an explicit bound on b. + + Conditional: the obligation to meet these hypotheses is the named gap `gap:pde-infra` + (docs/explanation/axiom-boundary.md). -/ theorem SemioticBVP.exists_pos_isWeakCoherentConfiguration (bvp : SemioticBVP n M) (solOp : SolutionOperator bvp) diff --git a/README.md b/README.md index 6054f03..6603b39 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ A Lean 4 and Mathlib (v4.34.1) formalization of the existence theory in N. Spence, *The Creative Determinant: Autopoietic Closure as a Nonlinear Elliptic Boundary Value Problem with Lean 4-Verified Existence Conditions* (2026). The problem is −ΔΦ = a|∇Φ| + bΦ − c(Φ₊)ᵖ in M with Φ = 0 on ∂M, where a = κγμ and p > 1. Documentation: [docs.projectnavi.ai/cd-formalization](https://docs.projectnavi.ai/cd-formalization/). -- **Continuum results (conditional).** `SemioticBVP.exists_isWeakCoherentConfiguration` gives a nonnegative solution when `b` is bounded above, and `SemioticBVP.exists_pos_isWeakCoherentConfiguration` one that is positive at some interior point when a supplied principal eigenvalue is negative. Both are derived from the hypotheses `PDEInfra` and `SolutionOperator`, which stand in for elliptic results not proved here; the manifold's Laplacian, gradient norm and boundary are abstract data. +- **Continuum results (conditional).** `SemioticBVP.exists_isWeakCoherentConfiguration` gives a nonnegative solution when `b` is bounded above, and `SemioticBVP.exists_pos_isWeakCoherentConfiguration` one that is positive at some interior point when a supplied principal eigenvalue is negative. Both are derived from the hypotheses `PDEInfra` and `SolutionOperator`, which stand in for elliptic results not proved here; the manifold's Laplacian, gradient norm and boundary are abstract data. The open obligation is the named gap `gap:pde-infra` (see the assumption boundary page). - **Finite graphs (proved).** For the discretization selected here, on a finite weighted graph with a Dirichlet boundary, `SemioticGraph.exists_pos_graph` gives a solution positive at every interior vertex when the interior graph is connected, the principal eigenvalue of L − diag(b) is negative, and a(x) ≤ √w(x,y) and a(y) ≤ √w(x,y) for every edge of positive weight between distinct interior vertices x and y. The operators and eigendata are constructed. The edge condition is sufficient for this proof, not claimed necessary, and holds for 0/1 weights (`SemioticGraph.exists_pos_graph_of_unweighted`). - **Supporting lemmas**, among them `spectral_characterization_1d`, `linfty_bound_algebraic`, `monotone_fixed_point_between` (Knaster–Tarski) and `scaling_uniqueness`. @@ -14,9 +14,10 @@ The [assumption boundary](https://docs.projectnavi.ai/cd-formalization/explanati lake exe cache get lake build --wfail lake env lean -DwarningAsError=true CdFormal/Verify.lean +lake build Spec && lake env lean spec/Check.lean ``` -`CdFormal/Verify.lean` prints the axioms of the headline results and the declarations the documentation cites; CI requires each to use only `propext`, `Classical.choice` and `Quot.sound`. This check cannot see hypotheses: `PDEInfra` appears in the signatures of the conditional theorems. +`CdFormal/Verify.lean` prints the axioms of the headline results and the declarations the documentation cites; CI requires each to use only `propext`, `Classical.choice` and `Quot.sound`. This check cannot see hypotheses: `PDEInfra` appears in the signatures of the conditional theorems. `spec/Spec.lean` states every headline result with `sorry` as its proof; `spec/Check.lean` checks the library against those statements, so a reader can audit a headline claim from the statement file alone. ## Credit and license diff --git a/docs/explanation/axiom-boundary.md b/docs/explanation/axiom-boundary.md index be1de62..6e405db 100644 --- a/docs/explanation/axiom-boundary.md +++ b/docs/explanation/axiom-boundary.md @@ -95,6 +95,10 @@ Classically: \(\varepsilon\varphi_1\) is a sub-solution, a large constant is a s Replacing a field by a proof would also require the operators to be constructed from the metric and the boundary to be the boundary of a manifold with boundary. +## The named gap + +The obligation the two continuum theorems leave open is named `gap:pde-infra`, so that it can be cited wherever they are. It is: for the concrete problem on a compact manifold with boundary, construct a solution operator and prove the fields of `PDEInfra` and `SolutionOperator` (and, for the second theorem, construct the principal eigendata), or prove the conclusions without them. Until then `SemioticBVP.exists_isWeakCoherentConfiguration` and `SemioticBVP.exists_pos_isWeakCoherentConfiguration` are implications. Nothing in the library instantiates their hypotheses, and an axiom report cannot show whether they can be met: `#print axioms` lists Lean axioms, not hypotheses. The statement file `spec/Spec.lean` shows both theorems with every hypothesis written out. + ## The finite-graph theorem `SemioticGraph.exists_pos_graph` takes no hypothesis of the kind above. On a finite graph the Laplacian and the gradient norm are defined from the weights, the principal eigenvalue is defined as an infimum, attained when the interior is nonempty, and shown to have a positive eigenvector when the interior graph is connected, and the fixed point comes from `monotone_fixed_point_between`. Its hypotheses (a connected interior graph, a negative principal eigenvalue, and the edge-dominance condition) are mathematical conditions stated in its signature; see the [theorem catalog](../reference/theorems.md#finite-graph-existence). diff --git a/docs/reference/theorems.md b/docs/reference/theorems.md index 8a9391f..46abbc7 100644 --- a/docs/reference/theorems.md +++ b/docs/reference/theorems.md @@ -50,7 +50,7 @@ theorem SemioticBVP.exists_isWeakCoherentConfiguration (∀ x, Phi x ≥ 0) ``` -Uses `PDEInfra.T_compact`, `PDEInfra.linfty_bound`, `PDEInfra.schaefer`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. With the default equation, \(\Phi \equiv 0\) is already such a solution (`zero_solves_equation`, below). +Uses `PDEInfra.T_compact`, `PDEInfra.linfty_bound`, `PDEInfra.schaefer`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. With the default equation, \(\Phi \equiv 0\) is already such a solution (`zero_solves_equation`, below). Conditional on the named gap `gap:pde-infra` ([assumption boundary](../explanation/axiom-boundary.md)). ### Solution positive at an interior point (Paper Theorem 3.16) @@ -68,7 +68,7 @@ theorem SemioticBVP.exists_pos_isWeakCoherentConfiguration (∃ x, x ∉ bvp.boundary ∧ Phi x > 0) ``` -Uses `PDEInfra.monotone_iteration`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. Positivity is at one interior point. +Uses `PDEInfra.monotone_iteration`, `PDEInfra.fixed_point_nonneg` and `SolutionOperator.T_fixed_point`. Positivity is at one interior point. Conditional on the named gap `gap:pde-infra` ([assumption boundary](../explanation/axiom-boundary.md)). ## Algebra and real analysis diff --git a/docs/reference/verification-audit.md b/docs/reference/verification-audit.md index b3ede6a..ded7a2f 100644 --- a/docs/reference/verification-audit.md +++ b/docs/reference/verification-audit.md @@ -15,8 +15,8 @@ What is checked, how, and what remains outside the formalization. Toolchain and | Lemma 3.7 (compactness of \(T\)) | `PDEInfra.T_compact` | Hypothesis | | Lemma 3.10 (L∞ bound) | `PDEInfra.linfty_bound`; `linfty_bound_algebraic` | Hypothesis; algebraic step proved | | Lemma 3.11 (\(C^{1,\alpha}\) bound) | none | Not formalized | -| Theorem 3.12 (existence) | `SemioticBVP.exists_isWeakCoherentConfiguration` | Proved from `PDEInfra` | -| Theorem 3.16 (nontrivial existence) | `SemioticBVP.exists_pos_isWeakCoherentConfiguration` | Proved from `PDEInfra`; positive at one interior point | +| Theorem 3.12 (existence) | `SemioticBVP.exists_isWeakCoherentConfiguration` | Proved from `PDEInfra`; named gap `gap:pde-infra` | +| Theorem 3.16 (nontrivial existence) | `SemioticBVP.exists_pos_isWeakCoherentConfiguration` | Proved from `PDEInfra`; named gap `gap:pde-infra`; positive at one interior point | | Section 3.4 (spectral condition, 1D) | `spectral_characterization_1d` | Algebraic inequality proved; eigenvalue identification not formalized | | Open Problem 3 (uniqueness) | `scaling_uniqueness` | Rules out solution multiples \(k\Phi\), \(k > 1\); uniqueness open | @@ -32,14 +32,15 @@ The required `build` job, on every pull request and on `main`: - runs the Mathlib environment linters (`lake lint`); - runs `CdFormal/Verify.lean` with warnings as errors and requires exactly one `#print axioms` record for each listed declaration, each using only `propext`, `Classical.choice` and `Quot.sound`; - fails if a headline result is missing from that list: the two continuum existence theorems, `SemioticGraph.exists_pos_graph` and its unweighted corollary, and the supporting lemmas the README names; +- checks the statement files: `spec/Spec.lean` restates every headline result with `sorry` as its proof, and `spec/Check.lean` requires each statement there to match the library declaration of the same name (the same type up to binder names and annotations, a theorem with a proof term, axioms within the allowlist), each statement's proof to be `sorry`, and every headline result to have a statement; - resolves, with `#check`, every inline-code token in the README and on these pages that looks like a Lean name containing an uppercase letter, `_` or `.`, and every declaration shown in a Lean code block there (all-lowercase names are not checked); - checks that every Lean file has the copyright header and a module docstring after its imports (Lean itself requires imports to come first); - fails if `sorry` or `sorryAx` appears anywhere in the Lean sources, comments included; -- fails if any module of the library declares an `axiom`, by inspecting the compiled environment rather than the source text; the check first confirms it reports an `axiom` declared across two lines. +- fails if any module of the library declares an `axiom` or an opaque constant, by inspecting the compiled environment rather than the source text; the check first confirms it reports both, an `axiom` declared across two lines and an `opaque` constant. An opaque constant is not an axiom, but the kernel cannot see its value and neither `#print axioms` nor a text search reports it. A proof by native evaluation (the tactic native_decide) declares an auxiliary axiom under Lean v4.34.1, so it fails this check and the axiom dashboard, and Mathlib's linter rejects it under warnings as errors. The `docs` job builds this site, checks that every navigation page is built and every built page is in the navigation, and checks local links, assets and anchors. It does not check external links. -These checks establish that the proofs compile against the pinned Mathlib and use no further axioms. They do not discharge hypotheses such as `PDEInfra`, and resolving a name does not show that the prose describes the statement; the statements on these pages are copied from the source. +These checks establish that the proofs compile against the pinned Mathlib and use no further axioms. They do not discharge hypotheses such as `PDEInfra` (the named gap `gap:pde-infra`), and resolving a name does not show that the prose describes the statement; the statements on these pages are copied from the source. ## Known limitations diff --git a/lakefile.toml b/lakefile.toml index 80f2ce1..d5de635 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -25,3 +25,9 @@ rev = "v4.34.1" [[lean_lib]] name = "CdFormal" + +# Statement files: the headline results restated with `sorry` as the specification, compared +# with the library by spec/Check.lean in CI. Not a default target; never imported by CdFormal. +[[lean_lib]] +name = "Spec" +srcDir = "spec" diff --git a/spec/Check.lean b/spec/Check.lean new file mode 100644 index 0000000..f1b24fb --- /dev/null +++ b/spec/Check.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 Nelson Spence. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nelson Spence +-/ +import CdFormal +import Spec + +/-! +# Comparator for the statement files + +`#check_statements` takes every theorem `Spec.name` in the module `Spec` (`spec/Spec.lean`) and +checks it against the library declaration `name`: + +1. the statement's proof uses `sorryAx`, so the statement file states and does not prove; +2. the library declaration exists and is a theorem, not an axiom or an opaque constant; +3. the two types are equal up to binder names and annotations, after the statement's universe + parameters are replaced by the library's; +4. the library proof uses no axiom outside `propext`, `Classical.choice` and `Quot.sound` + (the walk is `Lean.collectAxioms`, transitive over the proof term). + +It prints `SPEC OK name` for each match and fails with every mismatch listed. CI also requires +each headline result to have a `SPEC OK` line. Run with `lake env lean spec/Check.lean` after +`lake build Spec`. +-/ + +open Lean Elab Command + +/-- The axioms a library proof may use. -/ +def specAllowedAxioms : List Name := [``propext, ``Classical.choice, ``Quot.sound] + +/-- Check every statement of the module `Spec`; see the module docstring. -/ +elab "#check_statements" : command => do + let env ← getEnv + let mut statements : Array ConstantInfo := #[] + for mod in env.header.moduleNames, data in env.header.moduleData do + if mod == `Spec then + statements := data.constants.filter (fun c => !c.name.isInternal) + if statements.isEmpty then + throwError "no statements found in the module Spec" + let mut errors : Array MessageData := #[] + for s in statements do + let name := s.name.replacePrefix `Spec Name.anonymous + unless s matches .thmInfo _ do + errors := errors.push m!"{s.name}: a statement file may declare theorems only" + continue + unless (← collectAxioms s.name).contains ``sorryAx do + errors := errors.push m!"{s.name}: the statement is proved; its proof must be sorry" + continue + let some d := env.find? name + | errors := errors.push m!"{name}: no library declaration"; continue + unless d matches .thmInfo _ do + errors := errors.push m!"{name}: the library declaration is not a theorem" + continue + unless s.levelParams.length == d.levelParams.length do + errors := errors.push m!"{name}: {s.levelParams.length} universe parameters in the \ + statement, {d.levelParams.length} in the library" + continue + let sType := s.type.instantiateLevelParams s.levelParams (d.levelParams.map Level.param) + unless sType == d.type do + errors := errors.push m!"{name}: the statement differs from the library\n \ + statement: {sType}\n library: {d.type}" + continue + let axioms ← collectAxioms name + let bad := axioms.filter (fun a => !specAllowedAxioms.contains a) + unless bad.isEmpty do + errors := errors.push m!"{name}: the library proof uses {bad}" + continue + logInfo m!"SPEC OK {name}" + unless errors.isEmpty do + throwError m!"statement check failed:\n{MessageData.joinSep errors.toList "\n"}" + logInfo m!"{statements.size} statements match the library" + +#check_statements diff --git a/spec/Spec.lean b/spec/Spec.lean new file mode 100644 index 0000000..0ec6505 --- /dev/null +++ b/spec/Spec.lean @@ -0,0 +1,149 @@ +/- +Copyright (c) 2026 Nelson Spence. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nelson Spence +-/ +import CdFormal + +/-! +# Statement files for the headline results + +Each declaration below restates one headline result of the library with its statement written +out in full and its proof replaced by `sorry`. The `sorry` is deliberate: this file is the +specification, not the proof. `spec/Check.lean` compares the type of every statement here with +the type of the library declaration of the same name (alpha-equivalence after instantiating the +universe parameters), confirms that the library declaration is a theorem with a proof term, and +walks its axioms. CI runs that comparison, so a reader can check a headline claim against this +file alone, and a change to a library statement that is not mirrored here fails CI. + +This library is not a default target, is never imported by `CdFormal`, and lies outside the +placeholder audit, which covers the `CdFormal` tree only. + +## The named gap `gap:pde-infra` + +`SemioticBVP.exists_isWeakCoherentConfiguration` and +`SemioticBVP.exists_pos_isWeakCoherentConfiguration` take the class `PDEInfra` and the +structures `SolutionOperator` and `PrincipalEigendata` as hypotheses. Their fields are +propositions that no file instantiates, and `#print axioms` cannot see them. The statements +below show those hypotheses in full; the two theorems are implications, and the obligation to +discharge their hypotheses for a concrete operator is the gap named `gap:pde-infra` in +docs/explanation/axiom-boundary.md and docs/reference/verification-audit.md. +-/ + +-- The proofs below are `sorry` by design, so every hypothesis is unused. +set_option linter.unusedVariables false + +noncomputable section + +open scoped Manifold Bundle + +namespace Spec + +section Continuum + +variable {n : ℕ} {M : Type*} + [TopologicalSpace M] + [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] + [IsManifold (SemioticModel n) ⊤ M] + [MetricSpace M] [CompactSpace M] [ConnectedSpace M] + [SemioticManifold n M] + +/-- Statement of `SemioticBVP.exists_isWeakCoherentConfiguration` (paper Theorem 3.12). + Conditional: `gap:pde-infra`. -/ +theorem SemioticBVP.exists_isWeakCoherentConfiguration + (bvp : SemioticBVP n M) + (solOp : SolutionOperator bvp) + [infra : PDEInfra bvp solOp] + (B : ℝ) (hB : ∀ x, bvp.ctx.b x ≤ B) : + ∃ Phi : M → ℝ, + IsWeakCoherentConfiguration bvp Phi ∧ + (∀ x, Phi x ≥ 0) := sorry + +/-- Statement of `SemioticBVP.exists_pos_isWeakCoherentConfiguration` (paper Theorem 3.16). + Conditional: `gap:pde-infra`. -/ +theorem SemioticBVP.exists_pos_isWeakCoherentConfiguration + (bvp : SemioticBVP n M) + (solOp : SolutionOperator bvp) + [infra : PDEInfra bvp solOp] + (beta : ℝ) + (eig : PrincipalEigendata bvp beta) + (eigval_neg : eig.eigval < 0) : + ∃ Phi : M → ℝ, + IsWeakCoherentConfiguration bvp Phi ∧ + (∀ x, Phi x ≥ 0) ∧ + (∃ x, x ∉ bvp.boundary ∧ Phi x > 0) := sorry + +/-- Statement of `scaling_uniqueness`: no solution has a solution multiple kΦ with k > 1 at a + point where c > 0 and Φ > 0. Unconditional. -/ +theorem scaling_uniqueness + (ops : SemioticOperators n M) + (ctx : SemioticContext n M) + (Φ : M → ℝ) (k : ℝ) + (hk : k > 1) + (hΦ_eq : ∀ x, -(ops.laplacian Φ x) = + (ctx.a x) * (ops.gradNorm Φ x) + (ctx.b x) * (Φ x) - + (ctx.c x) * (max (Φ x) 0) ^ ctx.p) + (hkΦ_eq : ∀ x, + -(ops.laplacian (fun y ↦ k * Φ y) x) = + (ctx.a x) * (ops.gradNorm (fun y ↦ k * Φ y) x) + + (ctx.b x) * (k * Φ x) - + (ctx.c x) * (max (k * Φ x) 0) ^ ctx.p) + (x₀ : M) (hc : ctx.c x₀ > 0) (hΦpos : Φ x₀ > 0) : + False := sorry + +end Continuum + +/-- Statement of `spectral_characterization_1d`: for b > 0, β above the threshold + (π/L)²/b gives (π/L)² − βb < 0. Arithmetic; the eigenvalue identification is classical. -/ +theorem spectral_characterization_1d + (L : ℝ) (b : ℝ) (beta : ℝ) (hb : b > 0) : + let beta_star := viabilityThreshold L b + beta > beta_star → (Real.pi / L) ^ 2 - beta * b < 0 := sorry + +/-- Statement of `linfty_bound_algebraic`: from b·v ≥ c·v^p, v ≤ (b/c)^{1/(p−1)}. -/ +theorem linfty_bound_algebraic + (v b c p : ℝ) (hv : v > 0) (hc : c > 0) (hp : p > 1) + (h : b * v ≥ c * v ^ p) : + v ≤ (b / c) ^ (1 / (p - 1)) := sorry + +section Order + +universe u + +variable {α : Type u} [CompleteLattice α] (f : α →o α) + +/-- Statement of `monotone_fixed_point_between`: a monotone self-map of a complete lattice has a + fixed point between an ordered sub-fixed point and super-fixed point. -/ +theorem monotone_fixed_point_between + {sub super : α} + (h_sub : sub ≤ f sub) + (h_super : f super ≤ super) + (h_le : sub ≤ super) : + ∃ x : α, f x = x ∧ sub ≤ x ∧ x ≤ super := sorry + +end Order + +section Graph + +variable {V : Type*} [Fintype V] (G : SemioticGraph V) + +/-- Statement of `SemioticGraph.exists_pos_graph` (paper Theorem 3.23): connected interior, + the edge condition and a negative principal eigenvalue give a solution positive at every + interior vertex. Unconditional. -/ +theorem SemioticGraph.exists_pos_graph (hconn : G.interiorGraph.Connected) + (hdom : ∀ x y, x ∉ G.boundary → y ∉ G.boundary → x ≠ y → 0 < G.w x y → + G.a x ≤ √(G.w x y)) + (hneg : G.principalEigenvalue < 0) : + ∃ u : V → ℝ, G.IsSolution u ∧ ∀ x, x ∉ G.boundary → 0 < u x := sorry + +/-- Statement of `SemioticGraph.exists_pos_graph_of_unweighted`: with 0/1 weights the edge + condition is automatic. Unconditional. -/ +theorem SemioticGraph.exists_pos_graph_of_unweighted (hw : ∀ x y, G.w x y = 0 ∨ G.w x y = 1) + (hconn : G.interiorGraph.Connected) (hneg : G.principalEigenvalue < 0) : + ∃ u : V → ℝ, G.IsSolution u ∧ ∀ x, x ∉ G.boundary → 0 < u x := sorry + +end Graph + +end Spec + +end From c811982f80de50f1fba72cdc671a4962c2797eba Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 00:42:35 -0500 Subject: [PATCH 02/10] ci: fail the statement-file check when the headline list is empty The loop over HEADLINE_RESULTS passed vacuously on an empty list. The axiom check already rejects one; this step now does too, without relying on it. --- .github/workflows/lean_action_ci.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index faba940..efba313 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -157,6 +157,10 @@ jobs: if: ${{ !cancelled() && steps.build.outcome == 'success' }} run: | set -o pipefail + if [ -z "${HEADLINE_RESULTS// /}" ]; then + echo "::error::HEADLINE_RESULTS is empty" + exit 1 + fi lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt" # The statement files may warn only about their own `sorry` proofs. other=$(grep -E '^(warning|error)' "$RUNNER_TEMP/spec-build.txt" | From a8fc3028f298349d77b3f6a2f48ba934f0b1e4d0 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 00:52:54 -0500 Subject: [PATCH 03/10] ci: excuse only the statement file's own sorry warnings and treat grep errors as failures The warning filter excused a sorry warning from any file and swallowed a grep error with || true. It now allows only spec/Spec.lean's sorry warnings and fails on a grep exit above 1. Headline names are matched as fixed strings, so a dot in a name cannot match any character. --- .github/workflows/lean_action_ci.yml | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index efba313..cfc9af5 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -162,17 +162,29 @@ jobs: exit 1 fi lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt" - # The statement files may warn only about their own `sorry` proofs. - other=$(grep -E '^(warning|error)' "$RUNNER_TEMP/spec-build.txt" | - grep -v 'declaration uses `sorry`' || true) - if [ -n "$other" ]; then + # The only warnings allowed are the sorry proofs of spec/Spec.lean itself. A grep exit + # above 1 is an error, never "no match". + status=0 + grep -E '^(warning|error)' "$RUNNER_TEMP/spec-build.txt" > "$RUNNER_TEMP/spec-warnings.txt" || + status=$? + if [ "$status" -gt 1 ]; then + echo "::error::could not scan the statement-file build log (grep exit $status)" + exit 1 + fi + status=0 + grep -v -E '^warning: spec/Spec\.lean:[0-9]+:[0-9]+: declaration uses `sorry`$' \ + "$RUNNER_TEMP/spec-warnings.txt" || status=$? + if [ "$status" -eq 0 ]; then echo "::error::the statement files build with a warning other than their sorry proofs" exit 1 + elif [ "$status" -gt 1 ]; then + echo "::error::could not filter the statement-file warnings (grep exit $status)" + exit 1 fi lake env lean spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" missing="" for name in $HEADLINE_RESULTS; do - grep -qx "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name" + grep -qxF "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name" done if [ -n "$missing" ]; then echo "::error::headline results without a matching statement:$missing" From 82db5430b330cae7ff99b4087c418eb93115500c Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 01:12:05 -0500 Subject: [PATCH 04/10] ci: read the statement file's messages as JSON instead of filtering Lake's text The text filter examined only lines starting with warning or error, so a warning in another format would pass. The step now elaborates spec/Spec.lean with lake lean --json, which applies the package's linters (lake env lean does not), and accepts only its hasSorry warnings, matched by resolved path; any other message or any non-JSON output fails. spec/ may hold Spec.lean and Check.lean only, and Check.lean runs with warnings as errors. Warnings in library modules remain the build step's, which runs with warnings as errors. --- .github/workflows/lean_action_ci.yml | 54 ++++++++++++++++++---------- AGENTS.md | 3 ++ 2 files changed, 38 insertions(+), 19 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index cfc9af5..9f20c65 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -161,27 +161,43 @@ jobs: echo "::error::HEADLINE_RESULTS is empty" exit 1 fi - lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt" - # The only warnings allowed are the sorry proofs of spec/Spec.lean itself. A grep exit - # above 1 is an error, never "no match". - status=0 - grep -E '^(warning|error)' "$RUNNER_TEMP/spec-build.txt" > "$RUNNER_TEMP/spec-warnings.txt" || - status=$? - if [ "$status" -gt 1 ]; then - echo "::error::could not scan the statement-file build log (grep exit $status)" - exit 1 - fi - status=0 - grep -v -E '^warning: spec/Spec\.lean:[0-9]+:[0-9]+: declaration uses `sorry`$' \ - "$RUNNER_TEMP/spec-warnings.txt" || status=$? - if [ "$status" -eq 0 ]; then - echo "::error::the statement files build with a warning other than their sorry proofs" - exit 1 - elif [ "$status" -gt 1 ]; then - echo "::error::could not filter the statement-file warnings (grep exit $status)" + # spec/ holds the statement file and its checker, nothing else. + others=$(git ls-files 'spec/*' | grep -v -x -e spec/Spec.lean -e spec/Check.lean || true) + if [ -n "$others" ]; then + echo "::error::unexpected files in spec/: $others" exit 1 fi - lake env lean spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" + lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt" + # The statement file's own messages, read as JSON from Lean with the package's options + # (linters included), not by filtering Lake's text output. Allowed: its sorry warnings. + # Any other message, or any output that is not JSON, fails the step. Warnings in the + # library are the build step's concern: it runs with warnings as errors. + lake --quiet lean spec/Spec.lean -- --json > "$RUNNER_TEMP/spec-messages.jsonl" + python3 - "$RUNNER_TEMP/spec-messages.jsonl" <<'EOF' + import json, os, sys + spec = os.path.realpath("spec/Spec.lean") + sorries, other = 0, [] + for line in open(sys.argv[1], encoding="utf-8"): + if not line.strip(): + continue + m = json.loads(line) + if m["severity"] == "information": + continue + if (m["severity"] == "warning" and m.get("kind") == "hasSorry" + and os.path.realpath(m["fileName"]) == spec): + sorries += 1 + continue + other.append(f'{m["fileName"]}:{m["pos"]["line"]}: {m["severity"]}: {m["data"]}') + if other: + print("::error::the statement file has a message other than its sorry warnings") + print("\n".join(other)) + sys.exit(1) + if sorries == 0: + print("::error::the statement file reports no sorry warning") + sys.exit(1) + print(f"{sorries} sorry warnings and no other message in spec/Spec.lean") + EOF + lake env lean -DwarningAsError=true spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" missing="" for name in $HEADLINE_RESULTS; do grep -qxF "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name" diff --git a/AGENTS.md b/AGENTS.md index 4461c3d..71fdab5 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -71,6 +71,9 @@ lake build Spec && lake env lean spec/Check.lean # statement files agains result to all three: the workflow list, a `#print axioms` record, and a statement in `spec/Spec.lean` copied from the source with its proof replaced by `sorry`. Every record may use only `propext`, `Classical.choice` and `Quot.sound`. +- `spec/` holds `Spec.lean` and `Check.lean` only; CI rejects any other file there. The only + messages `spec/Spec.lean` may produce are its own `sorry` warnings, read by CI as Lean's JSON + messages with the package's linters on. - A statement file states; it does not prove. `spec/Check.lean` rejects a statement whose proof is not `sorry`, a statement whose type differs from the library declaration of the same name (binder names and annotations aside), a library declaration that is not a theorem, and a From bba273026e3f57f7be6fb2b611736fdc5763fcd2 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 01:13:08 -0500 Subject: [PATCH 05/10] ci: fail the statement-file check on any message other than its sorry warnings Information messages were skipped, so an #eval in the statement file could run and print unchecked. Now every message other than its own sorry warnings fails the step, as AGENTS.md states, and output that is not JSON fails with the offending line. --- .github/workflows/lean_action_ci.yml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 9f20c65..4caacd0 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -170,7 +170,8 @@ jobs: lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt" # The statement file's own messages, read as JSON from Lean with the package's options # (linters included), not by filtering Lake's text output. Allowed: its sorry warnings. - # Any other message, or any output that is not JSON, fails the step. Warnings in the + # Any other message (information included: the file must not print), or any output that + # is not JSON, fails the step. Warnings in the # library are the build step's concern: it runs with warnings as errors. lake --quiet lean spec/Spec.lean -- --json > "$RUNNER_TEMP/spec-messages.jsonl" python3 - "$RUNNER_TEMP/spec-messages.jsonl" <<'EOF' @@ -180,9 +181,11 @@ jobs: for line in open(sys.argv[1], encoding="utf-8"): if not line.strip(): continue - m = json.loads(line) - if m["severity"] == "information": - continue + try: + m = json.loads(line) + except json.JSONDecodeError: + print(f"::error::output from Lean that is not JSON: {line.strip()}") + sys.exit(1) if (m["severity"] == "warning" and m.get("kind") == "hasSorry" and os.path.realpath(m["fileName"]) == spec): sorries += 1 From 874eedf6a1ef38c2656c377cca5821ff267fae91 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 01:14:12 -0500 Subject: [PATCH 06/10] ci: stop the statement-file step if spec/ cannot be listed A failing git ls-files fed an empty list to the filter, and || true then let the extra-file check pass. The listing now runs on its own under -e, and a grep exit above 1 fails the step. --- .github/workflows/lean_action_ci.yml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 4caacd0..dd43957 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -162,7 +162,14 @@ jobs: exit 1 fi # spec/ holds the statement file and its checker, nothing else. - others=$(git ls-files 'spec/*' | grep -v -x -e spec/Spec.lean -e spec/Check.lean || true) + specfiles=$(git ls-files 'spec/*') + status=0 + others=$(printf '%s\n' "$specfiles" | grep -v -x -e spec/Spec.lean -e spec/Check.lean) || + status=$? + if [ "$status" -gt 1 ]; then + echo "::error::could not list spec/ (grep exit $status)" + exit 1 + fi if [ -n "$others" ]; then echo "::error::unexpected files in spec/: $others" exit 1 From d09412c11493c2fb675f6ef5d9a9e20d3f245289 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 01:25:20 -0500 Subject: [PATCH 07/10] ci: close two false passes in the statement-file step A tracked file such as spec/SpecXlean passed the spec/ listing, because grep -x read the allowed names as regular expressions; they are now fixed strings. An example with sorry in the statement file passed, because any number of sorry warnings was accepted; the count must now equal the number of statements the comparator checked. The headline list is split on all whitespace, so a list of only newlines or tabs counts as empty. --- .github/workflows/lean_action_ci.yml | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index dd43957..d530619 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -157,14 +157,16 @@ jobs: if: ${{ !cancelled() && steps.build.outcome == 'success' }} run: | set -o pipefail - if [ -z "${HEADLINE_RESULTS// /}" ]; then + # Split on any whitespace, so a list of only newlines or tabs counts as empty. + read -r -d '' -a headline <<< "$HEADLINE_RESULTS" || true + if [ "${#headline[@]}" -eq 0 ]; then echo "::error::HEADLINE_RESULTS is empty" exit 1 fi # spec/ holds the statement file and its checker, nothing else. specfiles=$(git ls-files 'spec/*') status=0 - others=$(printf '%s\n' "$specfiles" | grep -v -x -e spec/Spec.lean -e spec/Check.lean) || + others=$(printf '%s\n' "$specfiles" | grep -v -x -F -e spec/Spec.lean -e spec/Check.lean) || status=$? if [ "$status" -gt 1 ]; then echo "::error::could not list spec/ (grep exit $status)" @@ -181,7 +183,7 @@ jobs: # is not JSON, fails the step. Warnings in the # library are the build step's concern: it runs with warnings as errors. lake --quiet lean spec/Spec.lean -- --json > "$RUNNER_TEMP/spec-messages.jsonl" - python3 - "$RUNNER_TEMP/spec-messages.jsonl" <<'EOF' + python3 - "$RUNNER_TEMP/spec-messages.jsonl" "$RUNNER_TEMP/spec-sorries.txt" <<'EOF' import json, os, sys spec = os.path.realpath("spec/Spec.lean") sorries, other = 0, [] @@ -205,11 +207,20 @@ jobs: if sorries == 0: print("::error::the statement file reports no sorry warning") sys.exit(1) + open(sys.argv[2], "w").write(f"{sorries}\n") print(f"{sorries} sorry warnings and no other message in spec/Spec.lean") EOF lake env lean -DwarningAsError=true spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" + # One sorry warning per statement: a sorry anywhere else (an example, say) is not a + # statement the comparator checked. + statements=$(sed -n 's/^\([0-9][0-9]*\) statements match the library$/\1/p' "$RUNNER_TEMP/spec.txt") + sorries=$(cat "$RUNNER_TEMP/spec-sorries.txt") + if [ -z "$statements" ] || [ "$statements" -ne "$sorries" ]; then + echo "::error::$sorries sorry warnings for ${statements:-no} checked statements" + exit 1 + fi missing="" - for name in $HEADLINE_RESULTS; do + for name in "${headline[@]}"; do grep -qxF "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name" done if [ -n "$missing" ]; then From 3b02c6da71f1695b7cb23cd707b7eccfbea4fce6 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 01:28:15 -0500 Subject: [PATCH 08/10] ci: require each statement's proof to be sorry itself and fail on Lean panics A statement proved around a sorry (have : True := sorry, then the library theorem) depended on sorryAx and passed; the comparator now requires the proof, under the statement's binders, to be an application of sorryAx. It reads the proof from the theorem record: ConstantInfo.value! panics on theorems in v4.34.1, and a panic substitutes a default value and continues with exit code 0, so the step now fails on any PANIC line and on stderr output from the JSON elaboration. The statement count is compared as a single number, so a malformed count cannot fall through. --- .github/workflows/lean_action_ci.yml | 19 +++++++++++++++++-- spec/Check.lean | 15 ++++++++++----- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index d530619..d3fa846 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -182,7 +182,13 @@ jobs: # Any other message (information included: the file must not print), or any output that # is not JSON, fails the step. Warnings in the # library are the build step's concern: it runs with warnings as errors. - lake --quiet lean spec/Spec.lean -- --json > "$RUNNER_TEMP/spec-messages.jsonl" + lake --quiet lean spec/Spec.lean -- --json > "$RUNNER_TEMP/spec-messages.jsonl" \ + 2> "$RUNNER_TEMP/spec-stderr.txt" + if [ -s "$RUNNER_TEMP/spec-stderr.txt" ]; then + echo "::error::Lean wrote to stderr while elaborating the statement file" + cat "$RUNNER_TEMP/spec-stderr.txt" + exit 1 + fi python3 - "$RUNNER_TEMP/spec-messages.jsonl" "$RUNNER_TEMP/spec-sorries.txt" <<'EOF' import json, os, sys spec = os.path.realpath("spec/Spec.lean") @@ -211,11 +217,20 @@ jobs: print(f"{sorries} sorry warnings and no other message in spec/Spec.lean") EOF lake env lean -DwarningAsError=true spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" + # A Lean panic prints, substitutes a default value and continues with exit code 0. + status=0 + grep -q -F 'PANIC' "$RUNNER_TEMP/spec.txt" || status=$? + if [ "$status" -ne 1 ]; then + echo "::error::Lean panicked while checking the statement files (grep exit $status)" + exit 1 + fi # One sorry warning per statement: a sorry anywhere else (an example, say) is not a # statement the comparator checked. statements=$(sed -n 's/^\([0-9][0-9]*\) statements match the library$/\1/p' "$RUNNER_TEMP/spec.txt") sorries=$(cat "$RUNNER_TEMP/spec-sorries.txt") - if [ -z "$statements" ] || [ "$statements" -ne "$sorries" ]; then + # String comparison of two single numbers: a malformed count must not fall through. + if ! [[ "$statements" =~ ^[0-9]+$ && "$sorries" =~ ^[0-9]+$ ]] || + [ "$statements" != "$sorries" ]; then echo "::error::$sorries sorry warnings for ${statements:-no} checked statements" exit 1 fi diff --git a/spec/Check.lean b/spec/Check.lean index f1b24fb..9709e1c 100644 --- a/spec/Check.lean +++ b/spec/Check.lean @@ -12,7 +12,8 @@ import Spec `#check_statements` takes every theorem `Spec.name` in the module `Spec` (`spec/Spec.lean`) and checks it against the library declaration `name`: -1. the statement's proof uses `sorryAx`, so the statement file states and does not prove; +1. the statement's proof is `sorry` itself (an application of `sorryAx` under the statement's + binders), so the statement file states and does not prove; 2. the library declaration exists and is a theorem, not an axiom or an opaque constant; 3. the two types are equal up to binder names and annotations, after the statement's universe parameters are replaced by the library's; @@ -41,10 +42,14 @@ elab "#check_statements" : command => do let mut errors : Array MessageData := #[] for s in statements do let name := s.name.replacePrefix `Spec Name.anonymous - unless s matches .thmInfo _ do - errors := errors.push m!"{s.name}: a statement file may declare theorems only" - continue - unless (← collectAxioms s.name).contains ``sorryAx do + let .thmInfo st := s + | errors := errors.push m!"{s.name}: a statement file may declare theorems only"; continue + -- The proof must be `sorry` itself, under the statement's binders: depending on `sorryAx` + -- somewhere inside an otherwise real proof is not enough. + let mut v := st.value.consumeMData + while v.isLambda do + v := v.bindingBody!.consumeMData + unless v.isAppOf ``sorryAx do errors := errors.push m!"{s.name}: the statement is proved; its proof must be sorry" continue let some d := env.find? name From 492c101810fc9f390c31f53955eed51155866a78 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 01:29:30 -0500 Subject: [PATCH 09/10] docs: state the statement-file rules as CI now checks them --- AGENTS.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 71fdab5..89cec8d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -72,8 +72,9 @@ lake build Spec && lake env lean spec/Check.lean # statement files agains `spec/Spec.lean` copied from the source with its proof replaced by `sorry`. Every record may use only `propext`, `Classical.choice` and `Quot.sound`. - `spec/` holds `Spec.lean` and `Check.lean` only; CI rejects any other file there. The only - messages `spec/Spec.lean` may produce are its own `sorry` warnings, read by CI as Lean's JSON - messages with the package's linters on. + messages `spec/Spec.lean` may produce are its own `sorry` warnings, one per statement, read by + CI as Lean's JSON messages with the package's linters on. Each statement's proof is `sorry` + itself, not a proof that uses `sorry` somewhere. - A statement file states; it does not prove. `spec/Check.lean` rejects a statement whose proof is not `sorry`, a statement whose type differs from the library declaration of the same name (binder names and annotations aside), a library declaration that is not a theorem, and a From c490d7c1ce69f08004e8a12c4bf22aeb2d3814a1 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Fri, 9 Oct 2026 01:40:05 -0500 Subject: [PATCH 10/10] ci: reject an applied sorry in the statement files MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The check accepted any term headed by sorryAx, so (sorry : A → T) a passed, including a sorry applied to the library proof itself. A statement's proof must now be exactly Lean's sorry under its binders: sorryAx with its type, the synthetic flag false, and a closed label made of Lean.Name constructors and Nat literals, applied to nothing else. The kernel already fixes the sorry's type to the conclusion, so the types are not compared again (a let in a statement is stored as a non-dependent let there and a dependent one in the sorry's type). --- spec/Check.lean | 37 +++++++++++++++++++++++++++++-------- 1 file changed, 29 insertions(+), 8 deletions(-) diff --git a/spec/Check.lean b/spec/Check.lean index 9709e1c..651447c 100644 --- a/spec/Check.lean +++ b/spec/Check.lean @@ -12,8 +12,9 @@ import Spec `#check_statements` takes every theorem `Spec.name` in the module `Spec` (`spec/Spec.lean`) and checks it against the library declaration `name`: -1. the statement's proof is `sorry` itself (an application of `sorryAx` under the statement's - binders), so the statement file states and does not prove; +1. the statement's proof is `sorry` itself (`isBareSorry`: exactly Lean's sorry under the + statement's binders, not applied to anything), so the statement file states and does not + prove; 2. the library declaration exists and is a theorem, not an axiom or an opaque constant; 3. the two types are equal up to binder names and annotations, after the statement's universe parameters are replaced by the library's; @@ -30,6 +31,29 @@ open Lean Elab Command /-- The axioms a library proof may use. -/ def specAllowedAxioms : List Name := [``propext, ``Classical.choice, ``Quot.sound] +/-- Whether `v`, the proof of a statement, is `sorry` itself: under the statement's binders, + Lean's labelled sorry `sorryAx (∀ tag : Name, T) false tag`, with a closed label built from + `Lean.Name` constructors and `Nat` literals only, or the unlabelled `sorryAx T false`. A sorry + applied to further arguments, wrapped in `let` or `have`, or inside an otherwise real proof + is not. The kernel has already checked that `T` is the statement's conclusion. -/ +def isBareSorry (v : Expr) : Bool := Id.run do + let mut v := v.consumeMData + while v.isLambda do + v := v.bindingBody!.consumeMData + unless v.isAppOf ``sorryAx do return false + match v.getAppArgs with + | #[_, synthetic] => return synthetic.isConstOf ``Bool.false + | #[t, synthetic, tag] => + -- The label is data: `Lean.Name` constructors and `Nat` literals (`OfNat.ofNat`). + let nameOnly := tag.getUsedConstants.all (fun c => (`Lean.Name).isPrefixOf c || + [``OfNat.ofNat, ``Nat, ``instOfNatNat].contains c) + match t.consumeMData with + | .forallE _ (.const ``Lean.Name []) body _ => + return synthetic.isConstOf ``Bool.false && !tag.hasLooseBVars && !tag.hasFVar && + !tag.hasMVar && nameOnly && !body.hasLooseBVar 0 + | _ => return false + | _ => return false + /-- Check every statement of the module `Spec`; see the module docstring. -/ elab "#check_statements" : command => do let env ← getEnv @@ -44,12 +68,9 @@ elab "#check_statements" : command => do let name := s.name.replacePrefix `Spec Name.anonymous let .thmInfo st := s | errors := errors.push m!"{s.name}: a statement file may declare theorems only"; continue - -- The proof must be `sorry` itself, under the statement's binders: depending on `sorryAx` - -- somewhere inside an otherwise real proof is not enough. - let mut v := st.value.consumeMData - while v.isLambda do - v := v.bindingBody!.consumeMData - unless v.isAppOf ``sorryAx do + -- The proof must be `sorry` itself (see `isBareSorry`): depending on `sorryAx` somewhere, + -- or applying a sorry to further arguments, is not enough. + unless isBareSorry st.value do errors := errors.push m!"{s.name}: the statement is proved; its proof must be sorry" continue let some d := env.find? name