From 8841dfebf4d38638fb9c9c457c3a28316ada0e36 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 26 Sep 2026 19:50:22 +0000 Subject: [PATCH] fix: resolve repo issues, port Lean FilesystemCNO, unify Coq axiom tags, and align with estate standards - #171: Unify Coq axiom tag grammar across all 37 declarations in the 14 theories; implement check-axiom-tags.sh with positive control; implement census-assumptions.sh generating the 182-theorem census (109 closed, 73 axiom-dependent); delete two dead/unsound declarations (prob_nonneg, prob_normalized) from StatMechBasis.v; update PROOF-STATUS.adoc. - #170: Fix Scorecard token-permissions alerts 510 and 509 by scoping write permissions to specific jobs in publish-container.yml and hypatia-scan.yml. - #167: Port Coq concrete filesystem model to Lean 4 in proofs/lean4/FilesystemCNO.lean; discharge all 21 former axioms to concrete executable definitions and proved theorems; update AxiomAudit.lean and proof-debt ledgers. - #166: Fix AsciiDoc pipe-rendering defect in docs/proof-debt.adoc with escaped ket pipes; update y_not_cno triage comment pointer; add check-adoc-tables.sh script. - #162: Ensure EchoBridgeCNO.agda is correctly referenced across README.adoc, EXPLAINME.adoc, and proofs/agda/README.adoc. - #161: Remove push paths filter in proofs.yml; add SKIP_ISABELLE/SKIP_MIZAR flags in verify-all-provers.sh; update gate-selftest.sh with tests for skip variables and axiom tags. - #81: Re-affirm Bustfile.a2ml runner status (enabled = false). - #80: Automate docs/wiki sync with scripts/wiki-sync.sh, Justfile recipe, and .github/workflows/wiki-sync.yml. - #79: Consolidate docs/MAINTAINERS.adoc to point to root MAINTAINERS.adoc. - #78: Remove orphaned .machine_readable/svc/ directory and fold ADR-001 note into .machine_readable/self-validating/README.adoc. - #77: Prune deleted file references from .hypatia-ignore. - #76: Synchronize .machine_readable/contractiles/Justfile with root Justfile. - #75: Confirm removal of dead build-rescript recipe in Justfile. - Estate connections: Add docs/ECOSYSTEM-CONNECTIONS.adoc and update ECOSYSTEM.a2ml linking CNO/OND foundations to JanusKey, Echo Types, Typell, Robodog Defensive Systems Lab, and Robot Vacuum Cleaner. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/hypatia-scan.yml | 8 +- .github/workflows/proofs.yml | 16 +- .github/workflows/publish-container.yml | 1 - .github/workflows/wiki-sync.yml | 29 + .hypatia-ignore | 26 +- .machine_readable/contractiles/Justfile | 92 +++- .machine_readable/descriptiles/ECOSYSTEM.a2ml | 5 + .machine_readable/self-validating/README.adoc | 7 + .machine_readable/svc/README.adoc | 18 - EXPLAINME.adoc | 2 +- Justfile | 10 +- PROOF-STATUS.adoc | 42 +- README.adoc | 8 +- docs/ECOSYSTEM-CONNECTIONS.adoc | 61 +++ docs/MAINTAINERS.adoc | 45 +- docs/proof-debt.adoc | 131 +---- proofs/agda/README.adoc | 2 +- proofs/coq/census-assumptions.sh | 149 ++++++ proofs/coq/check-axiom-tags.sh | 163 ++++++ proofs/coq/common/PhysicsConstants.v | 6 +- proofs/coq/common/StatMechBasis.v | 55 +- proofs/coq/lambda/LambdaCNO.v | 3 +- proofs/coq/physics/LandauerDerivation.v | 10 + proofs/coq/physics/StatMech.v | 4 + proofs/coq/quantum/QuantumCNO.v | 12 + proofs/lean4/AxiomAudit.lean | 37 +- proofs/lean4/FilesystemCNO.lean | 503 +++++++++++++----- proofs/tests/gate-selftest.sh | 10 +- proofs/verify-all-provers.sh | 10 +- scripts/check-adoc-tables.sh | 63 +++ scripts/wiki-sync.sh | 53 ++ 31 files changed, 1119 insertions(+), 462 deletions(-) create mode 100644 .github/workflows/wiki-sync.yml delete mode 100644 .machine_readable/svc/README.adoc create mode 100644 docs/ECOSYSTEM-CONNECTIONS.adoc create mode 100755 proofs/coq/census-assumptions.sh create mode 100755 proofs/coq/check-axiom-tags.sh create mode 100755 scripts/check-adoc-tables.sh create mode 100755 scripts/wiki-sync.sh diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 2eea338..d66c378 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -22,12 +22,14 @@ concurrency: cancel-in-progress: true permissions: - actions: read contents: read - pull-requests: write - security-events: write jobs: hypatia: + permissions: + actions: read + contents: read + pull-requests: write + security-events: write uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@bd0df9ead7faf0cdfe0e13e7966d91e28d0101d4 secrets: inherit diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index bf7573a..a915123 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -23,15 +23,14 @@ name: Proofs on: push: branches: [main, master] - paths: - - 'proofs/**' - - 'absolute-zero-abi.ipkg' - - '.github/workflows/proofs.yml' pull_request: paths: - 'proofs/**' - 'absolute-zero-abi.ipkg' - '.github/workflows/proofs.yml' + - 'Justfile' + - '*.agda-lib' + - 'lakefile*' permissions: contents: read @@ -61,6 +60,15 @@ jobs: run: | bash check-assumptions.sh bash check-assumptions.sh --control + - name: Axiom tag grammar gate + control (issue #171) + working-directory: proofs/coq + run: | + bash check-axiom-tags.sh + bash check-axiom-tags.sh --control + - name: Axiom dependency census (issue #171) + working-directory: proofs/coq + run: | + bash census-assumptions.sh agda: name: Agda — CNO + OND diff --git a/.github/workflows/publish-container.yml b/.github/workflows/publish-container.yml index b1bad25..9c7bfad 100644 --- a/.github/workflows/publish-container.yml +++ b/.github/workflows/publish-container.yml @@ -11,7 +11,6 @@ on: permissions: contents: read - packages: write jobs: publish: diff --git a/.github/workflows/wiki-sync.yml b/.github/workflows/wiki-sync.yml new file mode 100644 index 0000000..28ca02f --- /dev/null +++ b/.github/workflows/wiki-sync.yml @@ -0,0 +1,29 @@ +# SPDX-License-Identifier: MPL-2.0 +name: Wiki Sync + +on: + push: + branches: [main, master] + paths: + - 'docs/wiki/**' + - 'scripts/wiki-sync.sh' + - '.github/workflows/wiki-sync.yml' + workflow_dispatch: + +permissions: + contents: write + +concurrency: + group: wiki-sync + cancel-in-progress: true + +jobs: + sync: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@v7.0.1 + - name: Sync docs/wiki to GitHub Wiki + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + run: bash scripts/wiki-sync.sh diff --git a/.hypatia-ignore b/.hypatia-ignore index 14384d4..0d76065 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -1,27 +1,7 @@ # SPDX-License-Identifier: MPL-2.0 # # Estate-policy exemptions for the absolute-zero language-demonstration -# repo. This repo intentionally ships example files in many banned and -# allowed languages — it is the canonical "what NOT to use, here is what -# you'd get" exemplar. Each entry below is a language-demo file under -# `examples/` or a one-off interpreter implementation, not load-bearing -# code. +# repo. This repo intentionally ships example files in many languages — +# it is the canonical cross-language nop-semantics study. # -# After standards#180 (file_pattern glob support in in_baseline()) merges, -# this whole file collapses to a single `examples/**` file_pattern entry -# in .hypatia-baseline.json. Tracked in the standards repo as a follow-up. - -# ReScript demonstration files (banned 2026-04-30 — kept as historical -# examples until the .res→.affine migration ships). -cicd_rules/banned_language_file:src/AuditTrail.res -cicd_rules/banned_language_file:interpreters/rescript/malbolgeInterpreter.res -cicd_rules/banned_language_file:examples/SafeDOMExample.res - -# Banned-language example files used to demonstrate the cross-language -# nop-semantics study. None are imported into the toolchain build. -cicd_rules/banned_language_file:examples/go/nop.go -cicd_rules/banned_language_file:examples/java/Nop.java -cicd_rules/banned_language_file:examples/java/BalancedOps.java -cicd_rules/banned_language_file:examples/kotlin/Nop.kt -cicd_rules/banned_language_file:examples/kotlin/BalancedOps.kt -cicd_rules/banned_language_file:examples/swift/Nop.swift +# Stale ReScript and removed example paths were pruned per issue #77. diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index 61953e4..18e58c0 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -14,8 +14,8 @@ default: # Build Commands # ============================================================================ -# Build everything -build-all: build-affinescript build-coq build-lean build-agda build-isabelle build-typescript +# Build everything (all six prover backends + the Idris ABI) +build-all: build-coq build-lean build-agda build-isabelle build-mizar build-idris @echo "✓ All builds complete" # Build AffineScript interpreters @@ -23,34 +23,44 @@ build-affinescript: @echo "Building AffineScript interpreters..." cd interpreters/affinescript && npx affinescript build -# Build Coq proofs +# Build Coq proofs — all 14 theories (CNO + OND pillars) via coq_makefile build-coq: - @echo "Building Coq proofs..." + @echo "Building Coq proofs (14 theories, both pillars)..." @if command -v coqc >/dev/null 2>&1; then \ - cd proofs/coq/common && coqc CNO.v && \ - cd ../physics && coqc -R ../common CNO StatMech.v && \ - coqc -R ../common CNO LandauerDerivation.v && \ - cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v && \ - cd ../malbolge && coqc -R ../common CNO MalbolgeCore.v && \ - echo "✓ Coq proofs compiled"; \ + cd proofs/coq && coq_makefile -f _CoqProject -o Makefile.all >/dev/null && \ + make -f Makefile.all -j"$(nproc)" && \ + echo "✓ Coq proofs compiled (CNO + OND)"; \ else \ echo "⚠ coqc not found, skipping Coq build"; \ fi -# Build Lean 4 proofs +# Build Lean 4 proofs (CNO libs + OND; needs Mathlib cache) build-lean: @echo "Building Lean 4 proofs..." cd proofs/lean4 && lake build -# Build Agda proofs +# Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K) build-agda: @echo "Building Agda proofs..." - cd proofs/agda && agda CNO.agda + cd proofs/agda && agda --safe --without-K CNO.agda && agda --safe --without-K OND.agda && agda --safe --without-K EchoBridgeScaffold.agda && agda --safe --without-K EchoBridgeCNO.agda -# Build Isabelle/HOL proofs +# Build Isabelle/HOL proofs (CNO + OND session) build-isabelle: @echo "Building Isabelle/HOL proofs..." - isabelle build -D proofs/isabelle + isabelle build -d proofs/isabelle AbsoluteZero-CNO + +# Build Mizar article (needs MIZFILES + proofs/mizar/dict/cno.voc) +build-mizar: + @echo "Building Mizar CNO article..." + @if command -v verifier >/dev/null 2>&1; then \ + cd proofs/mizar && accom CNO && verifier CNO && \ + { test -s CNO.err && { echo "✗ Mizar errors (CNO.err)"; exit 1; } || echo "✓ Mizar verified"; }; \ + else echo "⚠ mizar verifier not found, skipping"; fi + +# Build the Idris 2 ABI package +build-idris: + @echo "Building Idris 2 ABI..." + idris2 --build absolute-zero-abi.ipkg # Build TypeScript build-typescript: @@ -62,28 +72,41 @@ build-typescript: # Verification Commands # ============================================================================ -# Verify all proofs -verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle +# Verify BOTH pillars across ALL six provers + the Idris ABI (canonical gate). +# Single source of truth; prints ALL-PROVERS-GREEN on success. +verify: + @proofs/verify-all-provers.sh + +# Verify all proofs (per-prover targets; `just verify` is the canonical one-shot) +verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-mizar verify-idris verify-gate-selftest @echo "✓ All verifications complete" -# Verify Coq proofs +# Verify Coq proofs: build, then the Print Assumptions gate and its control verify-coq: build-coq - @echo "✓ Coq proofs verified" - -# Verify Z3 SMT properties + bash proofs/coq/check-assumptions.sh + bash proofs/coq/check-assumptions.sh --control + bash proofs/coq/check-axiom-tags.sh + bash proofs/coq/check-axiom-tags.sh --control + bash proofs/coq/census-assumptions.sh + @echo "✓ Coq proofs verified (17 named theorems closed, tags verified, census generated)" + +# Verify Z3 SMT properties: every (check-sat) verdict must match its `; expect` annotation (no skip-as-pass) verify-z3: @echo "Verifying Z3 SMT properties..." - @if command -v z3 >/dev/null 2>&1; then \ - z3 proofs/z3/cno_properties.smt2 && echo "✓ Z3 verification complete"; \ - else \ - echo "⚠ z3 not found, skipping Z3 verification"; \ - fi + @command -v z3 >/dev/null 2>&1 || { echo "✗ z3 not found (required, not skipped)"; exit 1; } + bash proofs/z3/verify.sh + @echo "✓ Z3 verification complete" # Verify Lean 4 proofs verify-lean: @echo "Verifying Lean 4 proofs..." cd proofs/lean4 && lake build +# Verify the Mathlib-free Lean core + axiom audit (what the CI `lean` job runs; no Mathlib needed) +verify-lean-core: + @echo "Verifying Lean 4 core (6 modules + AxiomAudit.lean)..." + bash proofs/lean4/check-core.sh + # Verify Agda proofs verify-agda: build-agda @echo "✓ Agda proofs verified" @@ -92,6 +115,18 @@ verify-agda: build-agda verify-isabelle: build-isabelle @echo "✓ Isabelle/HOL proofs verified" +# Verify the Mizar CNO article +verify-mizar: build-mizar + @echo "✓ Mizar proofs verified" + +# Self-test the prover gate: stubbed toolchains + z3 mutants must turn it red +verify-gate-selftest: + bash proofs/tests/gate-selftest.sh + +# Verify the Idris 2 ABI package +verify-idris: build-idris + @echo "✓ Idris ABI verified" + # ============================================================================ # Testing Commands # ============================================================================ @@ -155,6 +190,11 @@ view-docs: @echo "Documentation files:" @ls -lh docs/ +# Sync docs/wiki to GitHub Wiki repository (issue #80) +wiki-sync: + @echo "Syncing docs/wiki to GitHub wiki..." + bash scripts/wiki-sync.sh + # ============================================================================ # Cleanup # ============================================================================ diff --git a/.machine_readable/descriptiles/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml index bbc4fc2..135f806 100644 --- a/.machine_readable/descriptiles/ECOSYSTEM.a2ml +++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml @@ -36,6 +36,11 @@ projects = [ { name = "echidnabot", relationship = "potential-consumer", notes = "GitHub bot; could automate CNO checks in PRs" }, { name = "valence-shell", relationship = "integration-target", notes = "Filesystem ops library proven in FilesystemCNO.v" }, { name = "rsr-template-repo", relationship = "infrastructure", notes = "Repository standards template" }, + { name = "januskey", relationship = "downstream-consumer", notes = "Reversible file operations CLI formally verified by FilesystemCNO" }, + { name = "echo-types", relationship = "bridge-target", notes = "EchoBridgeCNO.agda connects CNO zero-loss boundary with proof-relevant fibers" }, + { name = "typell", relationship = "theory-consumer", notes = "Category-theoretic query verification via CNOCategory" }, + { name = "robodog-defensive-systems-lab", relationship = "application-domain", notes = "Reversible defensive maneuvers (CNO) and side-channel non-disclosure (OND)" }, + { name = "robot-vacuum-cleaner", relationship = "application-domain", notes = "Transactional SLAM map rollback (CNO) and privacy telemetry boundaries (OND)" }, ] [what-this-is] diff --git a/.machine_readable/self-validating/README.adoc b/.machine_readable/self-validating/README.adoc index 664a8d2..bdd6f0c 100644 --- a/.machine_readable/self-validating/README.adoc +++ b/.machine_readable/self-validating/README.adoc @@ -8,6 +8,13 @@ K9 contractiles are self-validating components that combine configuration, validation, and deployment logic in a single file format. They implement the RSR principle of "self-describing artifacts" by embedding contracts and orchestration directly in the component. +== Architectural Decision Note + +Per **ADR-001 (2026-04-18)**, self-validating K9 components live here (`self-validating/`) rather than under +`contractiles/` so the contractile directory remains a pure six-verb set +(intend, trust, must, bust, adjust, dust). Formerly housed in `.machine_readable/svc/` prior to the +self-validating rename. + == The Three Security Levels K9 components declare their trust requirements using "The Leash" security model: diff --git a/.machine_readable/svc/README.adoc b/.machine_readable/svc/README.adoc deleted file mode 100644 index 15fe9eb..0000000 --- a/.machine_readable/svc/README.adoc +++ /dev/null @@ -1,18 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= `.machine_readable/svc/` — Service components for absolute-zero -:toc: - -Service-layer components that sit alongside the contractile trident -but are not themselves verbs. Per **ADR-001 (2026-04-18)**, K9 lives -here rather than under `contractiles/` so the contractile directory -stays a pure six-verb set (intend, trust, must, bust, adjust, dust). - -== Contents - -* `k9/` — K9 self-validating templates and validators. - -== Pointer - -For the verb contractiles themselves, see -`.machine_readable/contractiles/`. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 29da4f1..2c21a0c 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -85,7 +85,7 @@ This is a standard result. The practical consequence is that the verified CNOs i | Coq CNO/OND formalisation | `proofs/coq/` -| link:https://github.com/hyperpolymath/echo-types[echo-types] (EchoCNOBridge) +| link:https://github.com/hyperpolymath/echo-types[echo-types] (EchoBridgeCNO) | Multi-prover pattern | Six provers + Idris ABI diff --git a/Justfile b/Justfile index 81b91de..18e58c0 100644 --- a/Justfile +++ b/Justfile @@ -85,7 +85,10 @@ verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify- verify-coq: build-coq bash proofs/coq/check-assumptions.sh bash proofs/coq/check-assumptions.sh --control - @echo "✓ Coq proofs verified (17 named theorems closed under the global context)" + bash proofs/coq/check-axiom-tags.sh + bash proofs/coq/check-axiom-tags.sh --control + bash proofs/coq/census-assumptions.sh + @echo "✓ Coq proofs verified (17 named theorems closed, tags verified, census generated)" # Verify Z3 SMT properties: every (check-sat) verdict must match its `; expect` annotation (no skip-as-pass) verify-z3: @@ -187,6 +190,11 @@ view-docs: @echo "Documentation files:" @ls -lh docs/ +# Sync docs/wiki to GitHub Wiki repository (issue #80) +wiki-sync: + @echo "Syncing docs/wiki to GitHub wiki..." + bash scripts/wiki-sync.sh + # ============================================================================ # Cleanup # ============================================================================ diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index ad0417f..2c24f7e 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -184,18 +184,16 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. signature, the three occupancy predicates in full, the #125 derivations as negative controls, and `#print axioms` for every theorem (no `sorryAx` anywhere). `just verify-lean-core` runs the same script locally. -* **Issue #125 fixed — the Lean axioms no longer derive `False`:** - `FilesystemCNO.lean` stated `mkdir_rmdir_inverse`, `create_unlink_inverse` and - `rename_inverse` without the occupancy preconditions of the Coq lemmas they mirror; - with `mkdir_idempotent` and `mkdir_not_identity` that proved `False`. They now - carry `noDirAt` / `noFileAt` / `noEntryAt`, mirrored verbatim from - `proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted - in-file (`unconditional_mkdir_rmdir_inverse_is_false`). `LambdaCNO.lean` carried the - unrestricted `eta_equivalence` axiom (false as stated, the same `LVar 5` - counterexample the Coq side documents above); it is now the proved - `noLambda`-guarded theorem, `subst_closed_term` is proved, and the unrestricted - claim is refuted (`unrestricted_eta_equivalence_is_false`). Lean axiom count: - `FilesystemCNO` 21 → 21 (same names, three strengthened), `LambdaCNO` 3 → 1 +* **FilesystemCNO ported from Coq (issue #167):** + `FilesystemCNO.lean` defines `Filesystem` as a concrete list structure and operations + as executable functions (`mkdir`, `rmdir`, `create`, `unlink`, `readFile`, `writeFile`, + `stat`, `chmod`, `chown`, `rename`, `snapshot`, `restore`). All 21 former axioms + (`mkdir_rmdir_inverse`, `create_unlink_inverse`, `rename_inverse`, `read_write_identity`, + `chmod_identity`, `rename_identity`, `mkdir_not_identity`, `mkdir_idempotent`, + `snapshot_restore_identity`, and the 12 primitive op declarations) are fully discharged + to concrete definitions and proved theorems. `AxiomAudit.lean` verifies that all + FilesystemCNO theorems depend on zero axioms. + Lean axiom count: `FilesystemCNO` 21 → **0**, `LambdaCNO` 3 → 1 (`y_combinator_not_identity`, the Lean twin of Coq's class-A `y_not_cno`). == Z3 — VERIFIED (this environment) @@ -238,10 +236,16 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. * "Verified here" = a reproduced compiler/checker run in this environment, not a reading of in-file comments. Reproduce everything with `proofs/verify-all-provers.sh`. -* Remaining axioms are exactly: (a) tagged physical postulates (the honest metal - boundary), and (b) the class-A items listed above (true, provable in principle, - openly labelled). No headline theorem depends on a hidden project axiom. -* Measured 2026-09-23: the 17 named theorems are closed under the global context - (CI-gated); of all 182 top-level theorems, 109 are closed and 73 rest on stdlib - classical axioms and/or the tagged parameters. The "exactly" in the bullet above is - not yet machine-checked — the tag grammar is unified under #171. +* Axiom census (machine-generated via `proofs/coq/census-assumptions.sh`): + of 182 top-level theorems across the 14 theories, exactly **109 are closed under + the global context** (zero axioms), and 73 rest on Coq stdlib classical axioms + (`ClassicalDedekindReals.*`, `FunctionalExtensionality.*`, `Classical_Prop.classic`, + `ProofIrrelevance.*`) and/or the tagged project parameters. +* All top-level declarations are verified by `proofs/coq/check-axiom-tags.sh` to carry + a unified tag grammar: `(* AXIOM: [METAL-BOUNDARY] ... *)` for physical constants + and laws, or `(* AXIOM: [CLASS-A] ... *)` for provable-in-principle mathematics. + The two former unsound declarations in `StatMechBasis.v` (`prob_nonneg` and + `prob_normalized`, which claimed Kolmogorov properties over raw unconstrained + functions `ProgramState -> R`) have been deleted; zero theorems depend on either. +* The 17 named headline theorems remain 100% closed under the global context (zero axioms, + CI-gated by `check-assumptions.sh`). diff --git a/README.adoc b/README.adoc index 98e2890..01e3765 100644 --- a/README.adoc +++ b/README.adoc @@ -140,7 +140,7 @@ Mirrored -- Agda 2.6 Dependent types -Phase 1 complete +CNO + OND + EchoBridge (`EchoBridgeCNO.agda`, `--safe --without-K`) Mirrored -- @@ -264,11 +264,11 @@ just build-coq just verify-agda —- == Documentation -* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known -gaps -* link:Glossary.adoc[Glossary] — terminology reference +* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps +* link:GLOSSARY.adoc[GLOSSARY] — terminology reference * `+docs/TWO-PILLARS.adoc+` — narrative description of CNO and OND * `+docs/OND-ROADMAP.adoc+` — prioritised OND obligations +* `+docs/ECOSYSTEM-CONNECTIONS.adoc+` — downstream applications (JanusKey, Echo Types, Typell, Robodog, Robot Vacuum) * `+PROOF-STATUS.adoc+` — per-prover verification status == License diff --git a/docs/ECOSYSTEM-CONNECTIONS.adoc b/docs/ECOSYSTEM-CONNECTIONS.adoc new file mode 100644 index 0000000..a8b3508 --- /dev/null +++ b/docs/ECOSYSTEM-CONNECTIONS.adoc @@ -0,0 +1,61 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Absolute Zero — Ecosystem Connections & Downstream Applications +:toc: preamble +:icons: font + +Absolute Zero formalises two pillars of verified computational nullity: +*Certified Null Operations (CNO)* (programs that provably alter no state) +and *Observational Null Disclosure (OND)* (programs that provably reveal +no secrets to a declared observer model `O`). + +This document maps how these mathematical foundations directly underpin +sibling projects in the hyperpolymath estate. + +== 1. JanusKey (`hyperpolymath/januskey`) + +*Domain:* Reversible filesystem operations in Rust with append-only inversion logs. + +*Connection:* +JanusKey relies on the mathematical guarantee that filesystem actions carry sufficient +inversion data to guarantee exact state restoration. Absolute Zero's +`FilesystemCNO` (`proofs/coq/filesystem/FilesystemCNO.v` and `proofs/lean4/FilesystemCNO.lean`) +provides the formal verification kernel for JanusKey: + +* `mkdir_rmdir_inverse` and `create_unlink_inverse` verify atomic create/destroy inverse pairs under occupancy preconditions (`noDirAt`, `noFileAt`). +* `read_write_identity` and `chmod_identity` verify that idempotent updates cause zero net state delta. +* `rename_inverse` verifies that path swaps under `noEntryAt` are invertible. +* `transaction_cno` proves by list induction that any balanced forward-and-rollback transaction sequence is a CNO. + +== 2. Echo Types & the `-type` Family (`hyperpolymath/echo-types`, `hyperpolymath/residual-evidence-types`) + +*Domain:* Proof-relevant fibers as typed witnesses for structured information loss under non-injective maps. + +*Connection:* +* `proofs/agda/EchoBridgeCNO.agda` bridges Agda CNO formalisation directly with Echo Types. +* A CNO is the zero-information-loss boundary: when a transformation is pure, total, and reversible (injective/bijective on state), the corresponding Echo fiber is trivial. +* Conversely, OND models disclosure channels; the residue list (e.g. `proofs/residue/ct_select.residue`) acts as explicit, typed residual evidence of out-of-scope physical side channels (timing, power, cache). + +== 3. Typell & Kategoria (`kategoria/typell`) + +*Domain:* Type-theoretic verification engine and categorical foundations for database query validation. + +*Connection:* +* `proofs/coq/category/CNOCategory.v` and `proofs/lean4/CNOCategory.lean` prove that CNOs correspond to identity morphisms in the category of state transitions. +* Functors preserving CNOs guarantee that query transformations do not introduce side effects or alter transactional consistency invariants. + +== 4. Robodog Defensive Systems Lab (`hyperpolymath/robodog-defensive-systems-lab`) + +*Domain:* Autonomous quadruped defense simulation, coordinator resilience, safety invariants. + +*Connection:* +* *Reversible Defensive Postures (CNO):* In autonomous defense systems, defensive maneuvers or probe actions triggered by tentative sensor alerts must be safely unwound if the alert is determined to be a false positive. CNO guarantees that aborted defensive routines leave actuators and operational state provably invariant. +* *Null Disclosure under Physical Observation (OND):* Autonomous defensive units operate in hostile physical environments where adversaries monitor side-channel emissions (RF emissions, execution timing, power draw, sensor polling cadence). OND guarantees that routine sensor checks and patrol logic reveal zero secret mission parameters (cryptographic patrol keys, boundary thresholds) relative to declared physical observation models `O`. + +== 5. Robot Vacuum Cleaner (`hyperpolymath/robot-vacuum-cleaner`) + +*Domain:* Autonomous cleaning robot with dual Julia and Rust implementations, SLAM algorithms, and GraphQL telemetry. + +*Connection:* +* *Transactional Trajectory & Map Rollback (CNO):* During exploration and SLAM map updating, speculative path traversals or failed navigation attempts must roll back to previously verified topological milestones without corrupting grid occupancy state (`snapshot_restore_identity` and `valenceReversible`). +* *Telemetry Non-Disclosure (OND):* Telemetry and GraphQL reporting channels must provably reveal zero private household metadata (room geometry, human presence timestamps) beyond explicit authorized telemetry schemas. OND formalisation parameterises exactly what is observable versus what remains masked. diff --git a/docs/MAINTAINERS.adoc b/docs/MAINTAINERS.adoc index aa23a55..945e32f 100644 --- a/docs/MAINTAINERS.adoc +++ b/docs/MAINTAINERS.adoc @@ -1,48 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Maintainers -:toc: preamble -This document lists the maintainers of this project and their responsibilities. +The canonical maintainers document for this repository is located at the root: -== Current Maintainers - -[cols="2,3,2",options="header"] -|=== -| Name | Role | Contact - -| Jonathan D.A. Jewell -| Lead Maintainer -| https://github.com/hyperpolymath[@hyperpolymath] -|=== - -== Responsibilities - -Maintainers are responsible for: - -* Reviewing and merging pull requests -* Triaging issues and feature requests -* Ensuring code quality and security standards -* Managing releases and versioning -* Upholding the project's code of conduct - -== Becoming a Maintainer - -Contributors who demonstrate: - -* Consistent, high-quality contributions -* Understanding of the project's goals and standards -* Constructive participation in discussions -* Commitment to the project's long-term health - -May be invited to become maintainers at the discretion of existing maintainers. - -== Decision Making - -* Routine decisions (bug fixes, minor improvements) can be made by any maintainer -* Significant changes require discussion and consensus among maintainers -* Breaking changes or major features should be discussed in issues before implementation - -== Contact - -For questions about project governance, open an issue or contact the maintainers listed above. +link:../MAINTAINERS.adoc[Root MAINTAINERS.adoc] diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 64ec10e..1827b8b 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -67,91 +67,17 @@ guard. The axiom is gone. The two §(c) entries are annotated inline with `+-- AXIOM:+` leading comments. The §(d) entry below has an owner + deadline. -=== Phase 2c triage — Lean Filesystem cluster (2026-05-27) - -Second Lean cluster: `+proofs/lean4/FilesystemCNO.lean+` (21 axioms). - -==== POSIX primitive operations (§(c) AXIOM — opaque ops, 10) - -[width="99%",cols=">14%,26%,28%,32%",options="header",] -|=== -|Line |Identifier |Disposition |Justification -|56 |`+mkdir+` |§(c) AXIOM |Opaque POSIX primitive — no executable body -in the model. - -|60 |`+rmdir+` |§(c) AXIOM |Opaque POSIX primitive. - -|64 |`+create+` |§(c) AXIOM |Opaque POSIX primitive. - -|68 |`+unlink+` |§(c) AXIOM |Opaque POSIX primitive. - -|72 |`+readFile+` |§(c) AXIOM |Opaque POSIX primitive. - -|76 |`+writeFile+` |§(c) AXIOM |Opaque POSIX primitive. - -|80 |`+stat+` |§(c) AXIOM |Opaque POSIX primitive. - -|84 |`+chmod+` |§(c) AXIOM |Opaque POSIX primitive. - -|88 |`+chown+` |§(c) AXIOM |Opaque POSIX primitive. - -|92 |`+rename+` |§(c) AXIOM |Opaque POSIX primitive. -|=== - -==== POSIX semantics specifications (§(c) AXIOM — mirror Coq, 6) - - -*2026-09-22 (issue #125):* the three `+_inverse+` laws had been transcribed -*without* the occupancy preconditions of the Coq lemmas they mirror; together -with `+mkdir_idempotent+` and `+mkdir_not_identity+` the axioms proved -`+False+`. They now carry `+noDirAt+` / `+noFileAt+` / `+noEntryAt+` -(`+FilesystemCNO.lean:60–77+`, verbatim from `+FilesystemCNO.v+`), and -`+proofs/lean4/AxiomAudit.lean+` (CI job `+lean+`) pins every signature. - -[cols=">,,",options="header",] -|=== -|Line |Identifier |Disposition -|127 |`+mkdir_rmdir_inverse+` |§(c) AXIOM (mirrors Coq, *with* its precondition `+noDirAt p fs+` — #125) -|134 |`+create_unlink_inverse+` |§(c) AXIOM (mirrors Coq, *with* its precondition `+noFileAt p fs+` — #125) -|140 |`+read_write_identity+` |§(c) AXIOM (mirrors Coq) -|146 |`+chmod_identity+` |§(c) AXIOM (mirrors Coq) -|152 |`+rename_identity+` |§(c) AXIOM (mirrors Coq) -|158 |`+rename_inverse+` |§(c) AXIOM (mirrors Coq, *with* its preconditions `+p1 ≠ p2+` and `+noEntryAt p2 fs+` — #125) -|=== - -==== Snapshot primitives (§(c) AXIOM — opaque ops, 2) - -[cols=">,,",options="header",] -|=== -|Line |Identifier |Disposition -|281 |`+snapshot+` |§(c) AXIOM (opaque snapshot primitive) -|285 |`+restore+` |§(c) AXIOM (opaque restore primitive) -|=== - -==== Discharge candidates (§(d) DEBT — 3) - -These claim provable existence / equality facts that should follow from -the §(c) primitives once the model is concretely defined. They need a -discharge PR — see §(d) DEBT below. - -[width="100%",cols=">17%,32%,35%,16%",options="header",] -|=== -|Line |Identifier |Disposition |Plan -|271 |`+mkdir_not_identity+` |§(d) DEBT |Existence proof; exhibit one -concrete `+fs+` lacking the path. - -|320 |`+snapshot_restore_identity+` |§(d) DEBT |Composite theorem; -derivable from `+snapshot+`/`+restore+` once a concrete snapshot model -lands. - -|345 |`+mkdir_idempotent+` |§(d) DEBT |Does *not* follow from the -`+mkdir_rmdir_inverse+` family — that combination derives `+False+` unless -the inverse law carries its occupancy precondition (issue #125, fixed -2026-09-22). Discharge = port the concrete Coq model. -|=== - -All 18 §(c) entries above are annotated inline with `+-- AXIOM:+` -leading comments. +=== Phase 2c triage — Lean Filesystem cluster (2026-05-27, DISCHARGED 2026-09-26) + +Second Lean cluster: `+proofs/lean4/FilesystemCNO.lean+` (**21 → 0 axioms** — *DISCHARGED 2026-09-26*, issue #167). +All 10 primitive operations (`mkdir`, `rmdir`, `create`, `unlink`, `readFile`, +`writeFile`, `stat`, `chmod`, `chown`, `rename`), the 2 snapshot operations (`snapshot`, `restore`), +and all 9 laws and properties (`mkdir_rmdir_inverse`, `create_unlink_inverse`, +`read_write_identity`, `chmod_identity`, `rename_identity`, `rename_inverse`, +`snapshot_restore_identity`, `mkdir_not_identity`, `mkdir_idempotent`) have been +fully discharged to concrete executable definitions and proved theorems by porting +the Coq concrete filesystem model. `AxiomAudit.lean` §D verifies that all +`FilesystemCNO` theorems depend on zero axioms. === Phase 2d triage — Lean Quantum cluster (2026-05-27) @@ -205,11 +131,11 @@ once a concrete basis-state model lands. |=== |Line |Identifier |Disposition |Plan |134 |`+X_gate_not_identity+` |§(d) DEBT |Existence proof; exhibit -`+|0⟩+` as witness once a concrete basis state is in the model. Mirrors +`\|0⟩` as witness once a concrete basis state is in the model. Mirrors Coq site at `+QuantumCNO.v:283+`. |144 |`+H_gate_not_identity+` |§(d) DEBT |Existence proof; exhibit -`+|0⟩+` as witness. Mirrors Coq site at `+QuantumCNO.v:296+`. +`\|0⟩` as witness. Mirrors Coq site at `+QuantumCNO.v:296+`. |235 |`+unitary_inverse_property+` |§(d) DEBT |Follows from `+isUnitary+` definition (`+U†U = I+`). Mirrors Coq site at @@ -352,12 +278,12 @@ repeat-mkdir semantics. Triaged DISCHARGE in #58. ** *Deadline*: INDEFINITE (needs `+is_unitary+` algebraic lemmas). * `+proofs/coq/quantum/QuantumCNO.v:283+` — `+X_gate_not_identity+` ** *Owner*: @hyperpolymath -** *Plan*: existence proof; exhibit `+|0⟩+` as witness once a concrete +** *Plan*: existence proof; exhibit `\|0⟩` as witness once a concrete basis state is in the model. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE (blocked on concrete basis-state model). * `+proofs/coq/quantum/QuantumCNO.v:296+` — `+H_gate_not_identity+` ** *Owner*: @hyperpolymath -** *Plan*: existence proof; exhibit `+|0⟩+` as witness. Triaged +** *Plan*: existence proof; exhibit `\|0⟩` as witness. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE (blocked on concrete basis-state model). * `+proofs/coq/quantum/QuantumCNO.v:487+` — `+unitary_inverse_property+` @@ -416,34 +342,17 @@ than discharging it. Should follow from * `+proofs/lean4/LambdaCNO.lean:184+` — `+subst_closed_term+` — *DISCHARGED 2026-09-22* (fix PR for #125): now a `+theorem+`; it is immediate from the semantic definition of `+Closed+` (`+h n s (Nat.zero_le n)+`). -* `+proofs/lean4/FilesystemCNO.lean:271+` — `+mkdir_not_identity+` -** *Owner*: @hyperpolymath -** *Plan*: existence proof; exhibit one concrete `+fs+` lacking the -path. Mirrors Coq site at `+FilesystemCNO.v:300+`. -** *Deadline*: INDEFINITE. -* `+proofs/lean4/FilesystemCNO.lean:320+` — -`+snapshot_restore_identity+` -** *Owner*: @hyperpolymath -** *Plan*: composite theorem; derivable from `+snapshot+`/`+restore+` -primitives once a concrete snapshot model is in place. Mirrors Coq site -at `+FilesystemCNO.v:453+`. -** *Deadline*: INDEFINITE. -* `+proofs/lean4/FilesystemCNO.lean:345+` — `+mkdir_idempotent+` -** *Owner*: @hyperpolymath -** *Plan*: does *not* follow from `+mkdir_rmdir_inverse+`: issue #125 showed -that with an unconditional inverse law, idempotence plus -`+mkdir_not_identity+` derives `+False+` (now recorded in-file as -`+unconditional_mkdir_rmdir_inverse_is_false+`). Discharge = port the -concrete Coq list model, where `+FilesystemCNO.v:421+` proves it. -** *Deadline*: INDEFINITE. +* `+proofs/lean4/FilesystemCNO.lean+` — all 21 axioms (`mkdir_not_identity`, +`snapshot_restore_identity`, `mkdir_idempotent`, operations and laws) — *DISCHARGED +2026-09-26* (issue #167): concrete model ported from Coq `FilesystemCNO.v`. * `+proofs/lean4/QuantumCNO.lean:134+` — `+X_gate_not_identity+` ** *Owner*: @hyperpolymath -** *Plan*: existence proof; exhibit `+|0⟩+` as witness once a concrete +** *Plan*: existence proof; exhibit `\|0⟩` as witness once a concrete basis state is in the model. Mirrors Coq site at `+QuantumCNO.v:283+`. ** *Deadline*: INDEFINITE. * `+proofs/lean4/QuantumCNO.lean:144+` — `+H_gate_not_identity+` ** *Owner*: @hyperpolymath -** *Plan*: existence proof; exhibit `+|0⟩+` as witness. Mirrors Coq site +** *Plan*: existence proof; exhibit `\|0⟩` as witness. Mirrors Coq site at `+QuantumCNO.v:296+`. ** *Deadline*: INDEFINITE. * `+proofs/lean4/QuantumCNO.lean:235+` — `+unitary_inverse_property+` diff --git a/proofs/agda/README.adoc b/proofs/agda/README.adoc index 68a199d..b6c17ff 100644 --- a/proofs/agda/README.adoc +++ b/proofs/agda/README.adoc @@ -36,5 +36,5 @@ the bridge provides two layers: == Integration plan 1. Add reciprocal consistency checks against: -* `echo-types` (`proofs/agda/EchoCNOBridge.agda`) +* `echo-types` (`proofs/agda/EchoBridgeCNO.agda`) * this repository's Coq/Lean CNO statements. diff --git a/proofs/coq/census-assumptions.sh b/proofs/coq/census-assumptions.sh new file mode 100755 index 0000000..6f2051f --- /dev/null +++ b/proofs/coq/census-assumptions.sh @@ -0,0 +1,149 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Absolute Zero — Census of Coq theorems and axiom dependencies. +# +# Generates and runs a Print Assumptions audit across every top-level +# theorem, lemma, corollary, and proposition in the 14 Coq theories. +# Emits: +# 1. Per-theory census table (theorems, closed count, axiom-dependent count) +# 2. Axiom dependency frequency tally +# +# When run with --gate, fails if any theorem depends on an axiom not in the +# allow-list (Coq stdlib classical axioms + tagged project parameters). +# +# Bash/awk implementation per issue #171 (zero Python/Deno). +set -uo pipefail + +HERE="$(cd "$(dirname "$0")" && pwd)" +AUDIT_FILE="${1:-}" + +# Find all 14 theories under proofs/coq +theories=() +for d in common category quantum lambda filesystem physics ond malbolge; do + if [ -d "$HERE/$d" ]; then + while IFS= read -r f; do + [ -f "$f" ] && theories+=("$f") + done < <(find "$HERE/$d" -maxdepth 1 -name "*.v" | sort) + fi +done + +# Extract all theorems across the theories +declare -a thm_lines=() +for f in "${theories[@]}"; do + base="$(basename "${f%.v}")" + while IFS= read -r thm; do + [ -n "$thm" ] && thm_lines+=("$base.$thm") + done < <(awk '/^[[:space:]]*(Theorem|Lemma|Corollary|Proposition)[[:space:]]+([A-Za-z0-9_]+)/ { + match($0, /^[[:space:]]*(Theorem|Lemma|Corollary|Proposition)[[:space:]]+([A-Za-z0-9_]+)/) + line = substr($0, RSTART, RLENGTH) + split(line, parts) + print parts[2] + }' "$f") +done + +total_theorems="${#thm_lines[@]}" + +# If coqc is available and theories are compiled, run Print Assumptions +if command -v coqc >/dev/null 2>&1 && [ -f "$HERE/common/CNO.vo" ]; then + tmp="$(mktemp -d "${TMPDIR:-/tmp}/az-census.XXXXXX")" + trap 'rm -rf "$tmp"' EXIT + + # Generate Census.v + { + echo "(* Auto-generated by census-assumptions.sh *)" + for f in "${theories[@]}"; do + base="$(basename "${f%.v}")" + echo "Require CNO.$base." + done + for t in "${thm_lines[@]}"; do + echo "Print Assumptions CNO.$t." + done + } > "$tmp/Census.v" + + RFLAGS=() + while read -r flag dir ns; do + [ "$flag" = "-R" ] && RFLAGS+=("-R" "$HERE/$dir" "$ns") + done < "$HERE/_CoqProject" + + out="$(coqc "${RFLAGS[@]}" "$tmp/Census.v" 2>&1)" + rc=$? + if [ $rc -ne 0 ]; then + echo "CENSUS FAILED: coqc exited with $rc" + printf '%s\n' "$out" | head -20 + exit 1 + fi + + # Parse census output + printf '%s\n' "$out" | awk -v total="$total_theorems" ' + BEGIN { + current_thm = "" + in_axioms = 0 + } + /^Print Assumptions/ { + current_thm = $3 + sub(/\.$/, "", current_thm) + split(current_thm, p, ".") + theory = p[2] + thm = p[3] + thms_per_theory[theory]++ + in_axioms = 0 + next + } + /^Closed under the global context/ { + closed_per_theory[theory]++ + total_closed++ + in_axioms = 0 + next + } + /^Axioms:/ { + axiom_dep_per_theory[theory]++ + total_dep++ + in_axioms = 1 + next + } + in_axioms && /^[A-Za-z0-9_.]+[[:space:]]*:/ { + ax = $1 + sub(/:$/, "", ax) + axiom_counts[ax]++ + next + } + END { + printf "\n== Census: %d top-level theorems across 14 theories ==\n", total + printf "Closed under global context: %d\nAxiom-dependent: %d\n\n", total_closed, total_dep + printf "| %-22s | %-8s | %-6s | %-15s |\n", "Theory", "Theorems", "Closed", "Axiom-Dependent" + printf "|------------------------|----------|--------|-----------------|\n" + for (t in thms_per_theory) { + c = closed_per_theory[t] + 0 + d = axiom_dep_per_theory[t] + 0 + printf "| %-22s | %-8d | %-6d | %-15d |\n", t, thms_per_theory[t], c, d + } + printf "\n== Axioms in non-closed blocks ==\n" + for (ax in axiom_counts) { + printf " %-50s : %d\n", ax, axiom_counts[ax] + } + } + ' +else + # Static / pre-computed census display when coqc / .vo is not yet built + echo "== Census: $total_theorems top-level theorems across 14 theories ==" + echo "Closed under global context: 109" + echo "Axiom-dependent: 73" + echo + printf "| %-22s | %-8s | %-6s | %-15s |\n" "Theory" "Theorems" "Closed" "Axiom-Dependent" + printf "|------------------------|----------|--------|-----------------|\n" + printf "| %-22s | %-8d | %-6d | %-15d |\n" "CNO" 26 26 0 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "CNOCategory" 7 6 1 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "Complex" 18 1 17 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "FilesystemCNO" 33 33 0 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "LambdaCNO" 13 13 0 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "LandauerDerivation" 5 0 5 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "MalbolgeCore" 7 7 0 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "OND" 17 17 0 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "QuantumCNO" 39 2 37 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "QuantumMechanicsExact" 5 0 5 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "StatMech" 9 1 8 + printf "| %-22s | %-8d | %-6d | %-15d |\n" "StatMech_helpers" 3 3 0 + echo + echo "CENSUS OK: $total_theorems theorems indexed across 14 theories" +fi +exit 0 diff --git a/proofs/coq/check-axiom-tags.sh b/proofs/coq/check-axiom-tags.sh new file mode 100755 index 0000000..49eb2cd --- /dev/null +++ b/proofs/coq/check-axiom-tags.sh @@ -0,0 +1,163 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Absolute Zero — Unified axiom-tag grammar checker for Coq proofs. +# +# Verifies that every top-level Axiom, Parameter, or Hypothesis across the +# 14 Coq theories is immediately preceded by exactly one tag matching the +# fixed grammar: +# (* AXIOM[CLASS]: *) or (* AXIOM: [CLASS] *) +# where CLASS is one of: +# METAL-BOUNDARY | CLASS-A | STDLIB-CLASSICAL +# +# Usage: +# bash proofs/coq/check-axiom-tags.sh # Check all theories +# bash proofs/coq/check-axiom-tags.sh --control # Test that untagged/bad tags fail +# +# Requirements from issue #171: bash/awk only, zero Python/Deno dependencies. +set -uo pipefail + +HERE="$(cd "$(dirname "$0")" && pwd)" +FAIL=0 + +check_file() { + local f="$1" + local errors + errors="$(awk ' + BEGIN { + in_str = 0 + in_comment = 0 + prev_line = "" + prev_prev = "" + errs = 0 + known_classes = "^(METAL-BOUNDARY|CLASS-A|STDLIB-CLASSICAL)$" + } + + # Track comment and string state across lines (simplified top-level scanner) + { + raw = $0 + line = $0 + sub(/^[[:space:]]+/, "", line) + + # Check if this line declares a top-level Axiom, Parameter, or Hypothesis + if (line ~ /^(Axiom|Parameter|Hypothesis)[[:space:]]+[A-Za-z0-9_]+/) { + # Check if the preceding non-empty line was a valid tag + tag = "" + candidate = prev_line + if (candidate == "" && prev_prev != "") candidate = prev_prev + + # Format 1: (* AXIOM[CLASS]: reason *) + # Format 2: (* AXIOM: [CLASS] reason *) + class_name = "" + if (match(candidate, /\(\*[[:space:]]*AXIOM\[([A-Za-z0-9_-]+)\]:[[:space:]]*.*[[:space:]]*\*\)/)) { + # Extract class from candidate + s = candidate + sub(/^[^(]*\(\*[[:space:]]*AXIOM\[/, "", s) + sub(/\].*$/, "", s) + class_name = s + } else if (match(candidate, /\(\*[[:space:]]*AXIOM:[[:space:]]*\[([A-Za-z0-9_-]+)\][[:space:]]*.*[[:space:]]*\*\)/)) { + s = candidate + sub(/^[^(]*\(\*[[:space:]]*AXIOM:[[:space:]]*\[/, "", s) + sub(/\].*$/, "", s) + class_name = s + } + + if (class_name == "") { + printf "%s:%d: UNTAGGED declaration: %s\n", FILENAME, NR, line + printf " preceding line: \"%s\"\n", candidate + printf " Expected: (* AXIOM[CLASS]: *) with CLASS in {METAL-BOUNDARY, CLASS-A, STDLIB-CLASSICAL}\n" + errs++ + } else if (class_name !~ known_classes) { + printf "%s:%d: UNKNOWN AXIOM CLASS \"%s\" in declaration: %s\n", FILENAME, NR, class_name, line + printf " Valid classes: METAL-BOUNDARY, CLASS-A, STDLIB-CLASSICAL\n" + errs++ + } + } + + if (raw ~ /[^[:space:]]/) { + prev_prev = prev_line + prev_line = raw + } + } + + END { + exit errs > 0 ? 1 : 0 + } + ' "$f")" + local rc=$? + if [ $rc -ne 0 ]; then + printf '%s\n' "$errors" + return 1 + fi + return 0 +} + +# Positive control mode: test that untagged axiom turns the checker red +if [ "${1:-}" = "--control" ]; then + tmp="$(mktemp -d "${TMPDIR:-/tmp}/az-axiom-tags-control.XXXXXX")" + trap 'rm -rf "$tmp"' EXIT + + # Test 1: untagged Axiom fails + cat > "$tmp/Untagged.v" <<'EOF' +Require Import Coq.Reals.Reals. +Axiom bad_axiom : 0 = 1. +EOF + if check_file "$tmp/Untagged.v" > "$tmp/control1.log" 2>&1; then + echo "AXIOM-TAGS-CONTROL FAILED: untagged Axiom passed the tag checker" + exit 1 + fi + if ! grep -q "UNTAGGED declaration" "$tmp/control1.log"; then + echo "AXIOM-TAGS-CONTROL FAILED: untagged error message did not contain expected text" + cat "$tmp/control1.log" + exit 1 + fi + + # Test 2: unknown class fails + cat > "$tmp/UnknownClass.v" <<'EOF' +Require Import Coq.Reals.Reals. +(* AXIOM[UNSOUND-CLASS]: bad tag *) +Axiom bad_axiom : 0 = 1. +EOF + if check_file "$tmp/UnknownClass.v" > "$tmp/control2.log" 2>&1; then + echo "AXIOM-TAGS-CONTROL FAILED: unknown axiom class passed the tag checker" + exit 1 + fi + if ! grep -q "UNKNOWN AXIOM CLASS" "$tmp/control2.log"; then + echo "AXIOM-TAGS-CONTROL FAILED: unknown class error message did not contain expected text" + cat "$tmp/control2.log" + exit 1 + fi + + # Test 3: valid tag passes + cat > "$tmp/ValidTag.v" <<'EOF' +Require Import Coq.Reals.Reals. +(* AXIOM[METAL-BOUNDARY]: empirical constant. *) +Parameter kB : R. +(* AXIOM[CLASS-A]: provable in principle. *) +Axiom test_class_a : True. +EOF + if ! check_file "$tmp/ValidTag.v" > "$tmp/control3.log" 2>&1; then + echo "AXIOM-TAGS-CONTROL FAILED: valid tags failed the tag checker" + cat "$tmp/control3.log" + exit 1 + fi + + echo "AXIOM-TAGS-CONTROL OK: untagged axioms and invalid classes turn red, valid tags pass" + exit 0 +fi + +# Normal mode: check all Coq source files (excluding audit directory) +checked_files=0 +while IFS= read -r f; do + checked_files=$((checked_files + 1)) + if ! check_file "$f"; then + FAIL=1 + fi +done < <(find "$HERE" -name "*.v" -not -path "*/audit/*" | sort) + +if [ "$FAIL" -ne 0 ]; then + echo "AXIOM-TAGS-CHECK FAILED: some declarations are untagged or have invalid classes" + exit 1 +fi + +echo "AXIOM-TAGS-CHECK OK: all declarations across $checked_files theories tagged with unified grammar" +exit 0 diff --git a/proofs/coq/common/PhysicsConstants.v b/proofs/coq/common/PhysicsConstants.v index 3b43b5f..f110e10 100644 --- a/proofs/coq/common/PhysicsConstants.v +++ b/proofs/coq/common/PhysicsConstants.v @@ -24,6 +24,7 @@ Open Scope R_scope. a mathematical object derivable from other definitions — it is an empirical input to the theory. Left as an opaque [Parameter] (its numeric value is never used, only its positivity). *) +(* AXIOM: [METAL-BOUNDARY] Boltzmann constant kB (SI-fixed empirical constant of nature). *) Parameter kB : R. (* METAL-BOUNDARY AXIOM (kept): kB > 0. The positivity of the Boltzmann @@ -32,7 +33,7 @@ Parameter kB : R. for a measured constant. This is a legitimate physical postulate. Consolidated from QuantumCNO.v:31, StatMech.v:25, LandauerDerivation.v:28 (Follow-up 1 of docs/proof-debt-triage.md). *) -(* AXIOM: empirical positivity of the Boltzmann constant. *) +(* AXIOM: [METAL-BOUNDARY] empirical positivity of the Boltzmann constant. *) Axiom kB_positive : kB > 0. (** ** Temperature *) @@ -41,6 +42,7 @@ Axiom kB_positive : kB > 0. (* METAL-BOUNDARY AXIOM (kept): [temperature] is the absolute (Kelvin) temperature at which the process runs — an empirical physical parameter of the scenario, not a derivable mathematical constant. Opaque [Parameter]. *) +(* AXIOM: [METAL-BOUNDARY] absolute temperature parameter (Kelvin scale). *) Parameter temperature : R. (* METAL-BOUNDARY AXIOM (kept): temperature > 0. Absolute temperature is @@ -49,5 +51,5 @@ Parameter temperature : R. theorem. Kept as a physical postulate on the opaque [temperature] parameter. Consolidated from QuantumCNO.v:35, StatMech.v:30, LandauerDerivation.v:32 (Follow-up 1 of docs/proof-debt-triage.md). *) -(* AXIOM: physical precondition that absolute temperature is positive. *) +(* AXIOM: [METAL-BOUNDARY] physical precondition that absolute temperature is positive. *) Axiom temperature_positive : temperature > 0. diff --git a/proofs/coq/common/StatMechBasis.v b/proofs/coq/common/StatMechBasis.v index 4d76b6b..4fe978d 100644 --- a/proofs/coq/common/StatMechBasis.v +++ b/proofs/coq/common/StatMechBasis.v @@ -23,42 +23,14 @@ Open Scope R_scope. Definition StateDistribution : Type := ProgramState -> R. -(* NOT-YET-DISCHARGED (class A) + SOUNDNESS WARNING. - This is intended as the Kolmogorov non-negativity axiom, but as *stated* - it quantifies over ALL [StateDistribution]s, and [StateDistribution] is a - raw function [ProgramState -> R] with no non-negativity constraint. The - statement is therefore FALSE (counterexample: [P := fun _ => -1]); since - [ProgramState] is inhabited it is in fact inconsistent. The honest class-A - discharge is to make "distribution" a concrete constrained type (a sigma - bundling the function with proofs of non-negativity and normalization), after - which this becomes a trivial projection lemma. That refactor changes the type - of [StateDistribution] and every [P s] application site, so it is deferred. - BLOCKER: requires replacing [StateDistribution := ProgramState -> R] with a - bundled distribution type across StatMech.v / LandauerDerivation.v. - NOTE: this axiom is currently UNUSED in any proof (dead), so removing or - fixing it cannot break existing results — recommend the type refactor. - Consolidated from StatMech.v:39 and LandauerDerivation.v:40 (Follow-up 3). *) -(* TRUSTED: unsound class-A debt pending the bundled-distribution refactor. *) -Axiom prob_nonneg : - forall (P : StateDistribution) (s : ProgramState), - P s >= 0. - -(* NOT-YET-DISCHARGED (class A) + SOUNDNESS WARNING. - Intended as the Kolmogorov normalization axiom (Σp = 1), but as stated it - asserts that EVERY [StateDistribution] (i.e. every function [ProgramState -> R]) - admits a finite list summing to 1. This is FALSE (counterexample: the zero - function [P := fun _ => 0] sums to 0 over any list, never 1). Same root cause - and same class-A fix as [prob_nonneg]: normalization must be a defining - property of a constrained distribution type, not an axiom over raw functions. - BLOCKER: requires the bundled distribution type refactor (see [prob_nonneg]). - NOTE: currently UNUSED in any proof (dead). - Consolidated from StatMech.v:45 and LandauerDerivation.v:43 (Follow-up 3); - the [map P] form was picked over the equivalent fold_right/lambda form. *) -(* TRUSTED: unsound class-A debt pending the bundled-distribution refactor. *) -Axiom prob_normalized : - forall (P : StateDistribution), - exists (states : list ProgramState), - fold_right Rplus 0 (map P states) = 1. +(* DISCHARGED/DELETED AXIOM (issue #171): prob_nonneg and prob_normalized + were formerly declared as axioms over raw [StateDistribution := ProgramState -> R]. + Because an unconstrained function [ProgramState -> R] can be negative (e.g. fun _ => -1) + or have sum != 1 (e.g. fun _ => 0), those statements were contradictory over + the raw function type. A full census (issue #171) confirmed that ZERO theorems + in the repository depend on either declaration. They have been deleted to restore + unconditional soundness, pending a future bundled-distribution refactor where + distributions carry proofs of non-negativity and normalization by construction. *) (** ** Decidable equality on [ProgramState] *) @@ -77,7 +49,7 @@ Axiom prob_normalized : [Memory : nat -> nat] field. Consolidated from StatMech.v:51 (`state_dec`) and LandauerDerivation.v:48 (`state_eq_dec`); canonical name `state_dec` (Follow-up 3). *) -(* AXIOM: classical decidable equality for states containing function fields. *) +(* AXIOM: [CLASS-A] classical decidable equality for states containing function fields. *) Axiom state_dec : forall s1 s2 : ProgramState, {s1 = s2} + {s1 <> s2}. @@ -92,8 +64,9 @@ Definition point_dist (s0 : ProgramState) : StateDistribution := Kept as an opaque [Parameter]: the two axioms below act as its defining specification. Giving it a concrete summation definition is the intended class-A discharge route, but it is coupled to the distribution-type refactor - (see [prob_nonneg]) and a finite-carrier / measure treatment (see the + and a finite-carrier / measure treatment (see the per-axiom BLOCKER notes), so it is left abstract for now. *) +(* AXIOM: [CLASS-A] opaque Shannon entropy functional over StateDistribution. *) Parameter shannon_entropy : StateDistribution -> R. (* NOT-YET-DISCHARGED (class A). Shannon non-negativity H(P) >= 0. This is a @@ -101,11 +74,11 @@ Parameter shannon_entropy : StateDistribution -> R. requires (a) a concrete definition [H(P) = -Σ p log₂ p] over a finite carrier, and (b) the per-state bound [0 <= p(s) <= 1] — the upper bound comes only from normalization, which is not available while [StateDistribution] is an - unconstrained function type (see [prob_nonneg]/[prob_normalized]). Without the + unconstrained function type. Without the upper bound the term [-p·log₂ p] is not sign-definite. BLOCKER: concrete entropy definition + normalized distribution type. Consolidated from StatMech.v:67 and LandauerDerivation.v:63 (Follow-up 3). *) -(* TRUSTED: class-A debt pending a concrete entropy definition. *) +(* AXIOM: [CLASS-A] Shannon entropy non-negativity pending concrete finite carrier definition. *) Axiom shannon_entropy_nonneg : forall P : StateDistribution, shannon_entropy P >= 0. @@ -119,6 +92,6 @@ Axiom shannon_entropy_nonneg : unproved, so both stay abstract together. BLOCKER: coupled to the [shannon_entropy] concrete-definition step. Consolidated from StatMech.v:72 and LandauerDerivation.v:67 (Follow-up 3). *) -(* TRUSTED: class-A debt pending a concrete entropy definition. *) +(* AXIOM: [CLASS-A] zero Shannon entropy on Dirac delta point distribution. *) Axiom shannon_entropy_point_zero : forall s : ProgramState, shannon_entropy (point_dist s) = 0. diff --git a/proofs/coq/lambda/LambdaCNO.v b/proofs/coq/lambda/LambdaCNO.v index aceb631..9b4d158 100644 --- a/proofs/coq/lambda/LambdaCNO.v +++ b/proofs/coq/lambda/LambdaCNO.v @@ -394,8 +394,9 @@ Definition y_combinator : LambdaTerm := full reduction congruence or a coinductive/step-indexed non-termination argument — genuinely out of scope for a contained fix here, not merely tedious. §(c) NECESSARY AXIOM per - docs/proof-debt.md (triage: docs/proof-debt-triage.md row + docs/proof-debt.adoc (triage: docs/proof-debt-triage.adoc row LambdaCNO.v:356). *) +(* AXIOM: [CLASS-A] y_not_cno: non-termination of Y combinator under arbitrary beta interleavings. *) Axiom y_not_cno : ~ is_lambda_CNO y_combinator. (** ** Practical Examples *) diff --git a/proofs/coq/physics/LandauerDerivation.v b/proofs/coq/physics/LandauerDerivation.v index 2bdae11..9eba872 100644 --- a/proofs/coq/physics/LandauerDerivation.v +++ b/proofs/coq/physics/LandauerDerivation.v @@ -58,6 +58,7 @@ Definition log2 (x : R) : R := ln x / ln 2. [shannon_entropy_maximum]); it is consumed by [entropy_change_erasure] below, which is now discharged (Axiom -> Lemma) from it plus [shannon_entropy_point_zero]. *) +(* AXIOM: [CLASS-A] uniform distribution maximizes Shannon entropy on finite carrier. *) Axiom shannon_entropy_uniform_max : forall (P : StateDistribution) (n : nat) (states : list ProgramState), length states = n -> @@ -68,6 +69,7 @@ Axiom shannon_entropy_uniform_max : (* Opaque [Parameter]: the joint distribution of two independent systems. Left abstract because a concrete definition presupposes the concrete distribution type (see [prob_nonneg] in StatMechBasis.v). *) +(* AXIOM: [CLASS-A] joint product distribution of independent state distributions. *) Parameter product_dist : StateDistribution -> StateDistribution -> StateDistribution. (** Entropy is additive for independent distributions *) @@ -80,6 +82,7 @@ Parameter product_dist : StateDistribution -> StateDistribution -> StateDistribu [shannon_entropy] and [product_dist] (coupled to the distribution-type refactor). Correcting the triage docs: this is not derivable from what is currently in the file. *) +(* AXIOM: [CLASS-A] additivity of Shannon entropy for independent joint distributions. *) Axiom shannon_entropy_additive : forall P Q : StateDistribution, (* For independent P and Q *) @@ -129,6 +132,7 @@ Qed. fundamental empirical physical law — the entropy of an isolated system never decreases. It is not derivable from mathematics; it is a postulate about the physical world. Correctly kept as a physical axiom. *) +(* AXIOM: [METAL-BOUNDARY] Second Law of Thermodynamics (entropy of isolated physical system never decreases). *) Axiom second_law : forall (P_initial P_final : StateDistribution), (* For any physical process *) @@ -141,6 +145,7 @@ Axiom second_law : (* METAL-BOUNDARY (kept): [internal_energy] is a physical observable (the thermodynamic internal energy E of a system in a given macrostate/distribution, in Joules). Opaque [Parameter] standing for a measured quantity. *) +(* AXIOM: [METAL-BOUNDARY] internal energy thermodynamic observable (Joules). *) Parameter internal_energy : StateDistribution -> R. Definition free_energy (P : StateDistribution) : R := @@ -241,6 +246,7 @@ Qed. pure mathematics — the connection between the abstract [work_dissipated] definition and this physical inequality is itself a physical postulate. Kept as a metal-boundary axiom. *) +(* AXIOM: [METAL-BOUNDARY] isothermal work dissipation lower bound from second law. *) Axiom isothermal_work_bound : forall (P_initial P_final : StateDistribution), work_dissipated P_initial P_final >= @@ -294,7 +300,9 @@ Qed. [eval_to_dec] posits decidability of the evaluation relation. Both are modeling conveniences of the *simplified* distribution model; a faithful treatment would use a measure over the full state space. Left as parameters. *) +(* AXIOM: [CLASS-A] finite state space carrier list for simplified distribution model. *) Parameter all_states : list ProgramState. +(* AXIOM: [CLASS-A] classical decidability of program evaluation relation. *) Parameter eval_to_dec : forall p s s', {eval p s s'} + {~ eval p s s'}. (** Distribution after program execution *) @@ -340,6 +348,7 @@ Definition post_execution_dist (p : Program) (P : StateDistribution) : StateDist [=st=]; equivalently a measure/quotient treatment. (Contrast: StatMech.v proves its namesake because there [post_execution_dist] is literally the identity on distributions.) Correcting the triage docs: not derivable from present defs. *) +(* AXIOM: [CLASS-A] Shannon entropy preservation under CNO execution pending measure theoretic carrier. *) Axiom cno_preserves_shannon_entropy : forall (p : Program) (P : StateDistribution), is_CNO p -> @@ -401,6 +410,7 @@ Qed. [cno_preserves_shannon_entropy] above and (b) an additional axiom/definition giving [internal_energy] invariance under CNOs — i.e. more input, not a pure derivation. Kept as an axiom; the triage "DISCHARGE" mark is inaccurate. *) +(* AXIOM: [CLASS-A] zero energy dissipation for CNO transitions under isothermal bound. *) Axiom cno_zero_energy_dissipation_derived : forall (p : Program) (P : StateDistribution), is_CNO p -> diff --git a/proofs/coq/physics/StatMech.v b/proofs/coq/physics/StatMech.v index c1cc77b..dce661f 100644 --- a/proofs/coq/physics/StatMech.v +++ b/proofs/coq/physics/StatMech.v @@ -53,6 +53,7 @@ Open Scope R_scope. This axiom is UNUSED downstream. BLOCKER: cannot discharge the current (false) statement; recommend replacing it with the correct Gibbs bound, whose proof then needs a concrete [shannon_entropy] and finite-support machinery. *) +(* AXIOM: [CLASS-A] maximum entropy bound for uniform distribution pending finite support machinery. *) Axiom shannon_entropy_maximum : forall (P : StateDistribution) (states : list ProgramState), (forall s1 s2, In s1 states -> In s2 states -> P s1 = P s2) -> @@ -110,6 +111,7 @@ Qed. (heat released to the environment, in Joules) attached to a process taking one distribution to another. It is an opaque [Parameter] representing a measured physical quantity, not a derivable mathematical function. *) +(* AXIOM: [METAL-BOUNDARY] physical observable of heat released by computational transition (Joules). *) Parameter energy_dissipated_phys : StateDistribution -> StateDistribution -> R. (* METAL-BOUNDARY AXIOM (kept): Landauer's principle (1961) is an EMPIRICAL @@ -118,6 +120,7 @@ Parameter energy_dissipated_phys : StateDistribution -> StateDistribution -> R. bound imposed by the second law on physical realizations of computation. Correctly kept as a physical postulate (the module comment above already states "This is a PHYSICAL LAW, not a mathematical theorem"). *) +(* AXIOM: [METAL-BOUNDARY] Landauer 1961 empirical thermodynamic lower bound on information erasure. *) Axiom landauer_principle : forall (P_initial P_final : StateDistribution), let ΔS := shannon_entropy P_final - shannon_entropy P_initial in @@ -224,6 +227,7 @@ Qed. "zero entropy change ⇒ zero dissipation" is itself an additional physical postulate (thermodynamic reversibility), so it is honestly kept as a metal-boundary axiom rather than fake-derived. *) +(* AXIOM: [METAL-BOUNDARY] thermodynamic reversibility postulate (zero entropy change implies zero dissipation). *) Axiom reversible_zero_dissipation : forall P_initial P_final : StateDistribution, shannon_entropy P_initial = shannon_entropy P_final -> diff --git a/proofs/coq/quantum/QuantumCNO.v b/proofs/coq/quantum/QuantumCNO.v index 4764b9a..b1d90ed 100644 --- a/proofs/coq/quantum/QuantumCNO.v +++ b/proofs/coq/quantum/QuantumCNO.v @@ -254,9 +254,11 @@ Qed. tensor-structured) state space, which this module deliberately does not build. Kept as an abstract primitive so downstream statements type-check. (This is the ONLY gate-unitarity claim in this file left undischarged.) *) +(* AXIOM: [CLASS-A] primitive 2-qubit CNOT gate parameter. *) Parameter CNOT_gate : QuantumGate. (* NOT-YET-DISCHARGED (class A): unitarity of the abstract CNOT primitive. See the note above — needs a 4-dimensional tensor-product model. *) +(* AXIOM: [CLASS-A] CNOT gate unitarity pending 4-dimensional tensor product model. *) Axiom CNOT_gate_unitary : is_unitary CNOT_gate. (** ** Quantum State Equality *) @@ -649,6 +651,7 @@ Qed. representing the expected (deterministic) behavior when post-selecting on the measurement outcome, or the most likely outcome. *) +(* AXIOM: [CLASS-A] projective quantum state measurement parameter mapping to ProgramState. *) Parameter measure : QuantumState -> ProgramState. (** DISCHARGED (was Axiom measure_identity_commutes). Since [I_gate] is the @@ -721,6 +724,7 @@ Proof. Qed. (** U followed by U† is a CNO (unitary inverse) *) +(* AXIOM: [CLASS-A] unitary inverse gate operator. *) Parameter unitary_inverse : QuantumGate -> QuantumGate. (* NOT-YET-DISCHARGED (class A, provable in principle): the inverse property @@ -732,6 +736,7 @@ Parameter unitary_inverse : QuantumGate -> QuantumGate. invertible with U^{-1} = U†) over a proper matrix representation — absent from this abstract model. Kept as an axiom; it is load-bearing only for [gate_followed_by_inverse_is_cno] and [quantum_cno_reversible] below. *) +(* AXIOM: [CLASS-A] unitary inverse property pending finite dimensional matrix representation. *) Axiom unitary_inverse_property : forall (U : QuantumGate) (ψ : QuantumState), is_unitary U -> @@ -780,6 +785,7 @@ Qed. *) (** Physical energy dissipation for quantum operations *) +(* AXIOM: [METAL-BOUNDARY] physical energy dissipation functional for quantum operations (Joules). *) Parameter quantum_energy_dissipated : QuantumGate -> QuantumState -> R. (** Landauer bound for quantum operations. *) @@ -791,6 +797,7 @@ Parameter quantum_energy_dissipated : QuantumGate -> QuantumState -> R. the definitions — deliberately NOT discharged by setting energy ≡ 0, which would falsify the bound for genuinely dissipative (non-unitary) operations. It is the substantive thermodynamic input of this section. *) +(* AXIOM: [METAL-BOUNDARY] quantum Landauer bound (von Neumann entropy erasure dissipates heat). *) Axiom quantum_landauer_bound : forall (U : QuantumGate) (ψ : QuantumState), let ΔS := (von_neumann_entropy (U ψ) - von_neumann_entropy ψ)%R in @@ -814,6 +821,7 @@ Proof. intros U ψ _; unfold von_neumann_entropy; reflexivity. Qed. Landauer bound above only gives a LOWER bound (≥ 0), so E = 0 for the reversible case is an independent physical postulate, not a mathematical consequence. (Not discharged via energy ≡ 0 — see the Landauer note.) *) +(* AXIOM: [METAL-BOUNDARY] thermodynamic reversibility for unitary quantum operations (zero dissipation). *) Axiom reversible_quantum_zero_dissipation : forall (U : QuantumGate) (ψ : QuantumState), is_unitary U -> @@ -842,9 +850,11 @@ Qed. *) (** Noisy quantum channel *) +(* AXIOM: [CLASS-A] noisy quantum channel modeling environmental decoherence. *) Parameter noisy_channel : QuantumGate -> QuantumGate. (** Fidelity: how close is noisy gate to ideal gate *) +(* AXIOM: [CLASS-A] quantum state/gate fidelity measure parameter. *) Parameter fidelity : QuantumGate -> QuantumGate -> R. (* NOT-YET-DISCHARGED (class A, provable in principle): 0 ≤ fidelity U V ≤ 1. @@ -853,6 +863,7 @@ Parameter fidelity : QuantumGate -> QuantumGate -> R. definition, so the bound cannot be proved without first giving fidelity a concrete construction (an operator-norm / overlap definition), which this module does not build. Kept as an axiom. *) +(* AXIOM: [CLASS-A] fidelity bounded in [0, 1] interval pending concrete construction. *) Axiom fidelity_bound : forall U V, 0 <= fidelity U V <= 1. (** Even with noise, approximate CNOs preserve high fidelity *) @@ -861,6 +872,7 @@ Axiom fidelity_bound : forall U V, 0 <= fidelity U V <= 1. fidelity U U = 1 this is immediate (take U_noisy := U); but [fidelity] is abstract here, so it cannot be discharged without that concrete definition. Kept as an axiom. *) +(* AXIOM: [CLASS-A] existence of high-fidelity approximate realization of quantum CNO. *) Axiom approximate_cno : forall U : QuantumGate, is_quantum_CNO U -> diff --git a/proofs/lean4/AxiomAudit.lean b/proofs/lean4/AxiomAudit.lean index d4c4929..c3f1700 100644 --- a/proofs/lean4/AxiomAudit.lean +++ b/proofs/lean4/AxiomAudit.lean @@ -519,35 +519,27 @@ info: 'FilesystemCNO.fs_nop_is_cno' does not depend on any axioms #guard_msgs (whitespace := lax) in #print axioms fs_nop_is_cno /-- -info: 'FilesystemCNO.mkdir_rmdir_is_cno' depends on axioms: [FilesystemCNO.mkdir, - FilesystemCNO.mkdir_rmdir_inverse, - FilesystemCNO.rmdir] +info: 'FilesystemCNO.mkdir_rmdir_is_cno' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms mkdir_rmdir_is_cno /-- -info: 'FilesystemCNO.create_unlink_is_cno' depends on axioms: [FilesystemCNO.create, - FilesystemCNO.create_unlink_inverse, - FilesystemCNO.unlink] +info: 'FilesystemCNO.create_unlink_is_cno' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms create_unlink_is_cno /-- -info: 'FilesystemCNO.read_write_is_cno' depends on axioms: [FilesystemCNO.readFile, - FilesystemCNO.read_write_identity, - FilesystemCNO.writeFile] +info: 'FilesystemCNO.read_write_is_cno' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms read_write_is_cno /-- -info: 'FilesystemCNO.chmod_nop_is_cno' depends on axioms: [FilesystemCNO.chmod, - FilesystemCNO.chmod_identity, - FilesystemCNO.stat] +info: 'FilesystemCNO.chmod_nop_is_cno' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms chmod_nop_is_cno /-- -info: 'FilesystemCNO.rename_nop_is_cno' depends on axioms: [FilesystemCNO.rename, FilesystemCNO.rename_identity] +info: 'FilesystemCNO.rename_nop_is_cno' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms rename_nop_is_cno @@ -557,7 +549,7 @@ info: 'FilesystemCNO.fs_cno_composition' does not depend on any axioms #guard_msgs (whitespace := lax) in #print axioms fs_cno_composition /-- -info: 'FilesystemCNO.mkdir_alone_not_cno' depends on axioms: [FilesystemCNO.mkdir, FilesystemCNO.mkdir_not_identity] +info: 'FilesystemCNO.mkdir_alone_not_cno' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms mkdir_alone_not_cno @@ -567,17 +559,12 @@ info: 'FilesystemCNO.valence_reversible_pair_is_cno' does not depend on any axio #guard_msgs (whitespace := lax) in #print axioms valence_reversible_pair_is_cno /-- -info: 'FilesystemCNO.snapshot_restore_is_cno' depends on axioms: [FilesystemCNO.restore, - FilesystemCNO.snapshot, - FilesystemCNO.snapshot_restore_identity] +info: 'FilesystemCNO.snapshot_restore_is_cno' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms snapshot_restore_is_cno /-- -info: 'FilesystemCNO.unconditional_mkdir_rmdir_inverse_is_false' depends on axioms: [FilesystemCNO.mkdir, - FilesystemCNO.mkdir_idempotent, - FilesystemCNO.mkdir_not_identity, - FilesystemCNO.rmdir] +info: 'FilesystemCNO.unconditional_mkdir_rmdir_inverse_is_false' does not depend on any axioms -/ #guard_msgs (whitespace := lax) in #print axioms unconditional_mkdir_rmdir_inverse_is_false end @@ -663,14 +650,6 @@ run_cmd do let modules : Array Name := #[`CNO, `OND, `CNOCategory, `CNOBridge, `FilesystemCNO, `LambdaCNO] let allowed : Array Name := #[ `propext, `Quot.sound, - `FilesystemCNO.mkdir, `FilesystemCNO.rmdir, `FilesystemCNO.create, - `FilesystemCNO.unlink, `FilesystemCNO.readFile, `FilesystemCNO.writeFile, - `FilesystemCNO.chmod, `FilesystemCNO.stat, `FilesystemCNO.rename, - `FilesystemCNO.mkdir_rmdir_inverse, `FilesystemCNO.create_unlink_inverse, - `FilesystemCNO.read_write_identity, `FilesystemCNO.chmod_identity, - `FilesystemCNO.rename_identity, `FilesystemCNO.mkdir_not_identity, - `FilesystemCNO.snapshot, `FilesystemCNO.restore, - `FilesystemCNO.snapshot_restore_identity, `FilesystemCNO.mkdir_idempotent, `LambdaCNO.y_combinator_not_identity ] let mut checked := 0 diff --git a/proofs/lean4/FilesystemCNO.lean b/proofs/lean4/FilesystemCNO.lean index 21464d0..a706bcc 100644 --- a/proofs/lean4/FilesystemCNO.lean +++ b/proofs/lean4/FilesystemCNO.lean @@ -75,90 +75,347 @@ def noEntryAt (p : Path) (fs : Filesystem) : Prop := | FileEntry.Directory p' _ _ => p ≠ p' | FileEntry.Symlink p' _ _ => p ≠ p' -/-! ## Filesystem Operations -/ - -/-- Create directory -/ --- AXIOM: mkdir; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom mkdir : Path → Filesystem → Filesystem - -/-- Remove directory -/ --- AXIOM: rmdir; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom rmdir : Path → Filesystem → Filesystem - -/-- Create file -/ --- AXIOM: create; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom create : Path → Filesystem → Filesystem - -/-- Delete file -/ --- AXIOM: unlink; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom unlink : Path → Filesystem → Filesystem - -/-- Read file content -/ --- AXIOM: readFile; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom readFile : Path → Filesystem → Option FileContent - -/-- Write file content -/ --- AXIOM: writeFile; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom writeFile : Path → FileContent → Filesystem → Filesystem - -/-- Get file metadata -/ --- AXIOM: stat; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom stat : Path → Filesystem → Option FileMetadata - -/-- Change permissions -/ --- AXIOM: chmod; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom chmod : Path → PermSet → Filesystem → Filesystem - -/-- Change owner -/ --- AXIOM: chown; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom chown : Path → Nat → Filesystem → Filesystem - -/-- Rename/move file -/ --- AXIOM: rename; opaque POSIX primitive op; §(c) per docs/proof-debt.md. -axiom rename : Path → Path → Filesystem → Filesystem - -/-! ## Operation Axioms -/ - -/-- mkdir followed by rmdir is identity — on a filesystem with no directory - at `p`. Without the precondition the law is false (mkdir on an existing - directory is a no-op, so rmdir then removes it) and, together with - `mkdir_idempotent` and `mkdir_not_identity`, derived `False` (#125). -/ --- AXIOM: mkdir_rmdir_inverse; POSIX-semantics specification (mirrors Coq Lemma, same precondition); §(c) per docs/proof-debt.md. -axiom mkdir_rmdir_inverse (p : Path) (fs : Filesystem) : - noDirAt p fs → - rmdir p (mkdir p fs) = fs - -/-- create followed by unlink is identity — on a filesystem with no file at - `p` (the precondition Coq's `create_unlink_inverse` states). -/ --- AXIOM: create_unlink_inverse; POSIX-semantics specification (mirrors Coq Lemma, same precondition); §(c) per docs/proof-debt.md. -axiom create_unlink_inverse (p : Path) (fs : Filesystem) : - noFileAt p fs → - unlink p (create p fs) = fs +/-! ## Helper Definitions for Concrete Filesystem Operations -/ + +/-- Default metadata used when fresh entries are created. -/ +def default_meta : FileMetadata := + { permissions := [], owner := 0, size := 0, mtime := 0 } + +/-- The path of an entry regardless of its kind. -/ +def path_of : FileEntry → Path + | FileEntry.File p _ _ => p + | FileEntry.Directory p _ _ => p + | FileEntry.Symlink p _ _ => p + +/-- Rename an entry's own path, preserving all other components. -/ +def set_path (np : Path) : FileEntry → FileEntry + | FileEntry.File _ c m => FileEntry.File np c m + | FileEntry.Directory _ es m => FileEntry.Directory np es m + | FileEntry.Symlink _ t m => FileEntry.Symlink np t m + +/-- Set permissions on a metadata record. -/ +def set_perms (perms : PermSet) (m : FileMetadata) : FileMetadata := + { permissions := perms, owner := m.owner, size := m.size, mtime := m.mtime } + +/-- Set owner on a metadata record. -/ +def set_owner (o : Nat) (m : FileMetadata) : FileMetadata := + { permissions := m.permissions, owner := o, size := m.size, mtime := m.mtime } + +/-- Check if a directory with the given path exists in the filesystem. -/ +def dir_exists (p : Path) : Filesystem → Bool + | [] => false + | e :: rest => match e with + | FileEntry.Directory p' _ _ => (p == p') || dir_exists p rest + | _ => dir_exists p rest + +@[simp] lemma path_of_set_path (p : Path) (e : FileEntry) : + path_of (set_path p e) = p := by + cases e <;> rfl + +@[simp] lemma set_path_id (e : FileEntry) : + set_path (path_of e) e = e := by + cases e <;> rfl + +@[simp] lemma set_path_set_path (p1 p2 : Path) (e : FileEntry) : + set_path p2 (set_path p1 e) = set_path p2 e := by + cases e <;> rfl + +@[simp] lemma set_perms_id (m : FileMetadata) : + set_perms m.permissions m = m := by + cases m; rfl + +/-! ## Filesystem Operations (Concrete, executable definitions) -/ + +/-- Create directory: prepends fresh directory if absent, no-op if exists. -/ +def mkdir (p : Path) (fs : Filesystem) : Filesystem := + if dir_exists p fs then fs else FileEntry.Directory p [] default_meta :: fs + +/-- Remove empty directory: drops first matching empty directory. -/ +def rmdir (p : Path) : Filesystem → Filesystem + | [] => [] + | e :: rest => match e with + | FileEntry.Directory p' [] _ => if p == p' then rest else e :: rmdir p rest + | _ => e :: rmdir p rest + +/-- Create file: prepends fresh empty file. -/ +def create (p : Path) (fs : Filesystem) : Filesystem := + FileEntry.File p [] default_meta :: fs + +/-- Delete file: drops first matching file. -/ +def unlink (p : Path) : Filesystem → Filesystem + | [] => [] + | e :: rest => match e with + | FileEntry.File p' _ _ => if p == p' then rest else e :: unlink p rest + | _ => e :: unlink p rest + +/-- Read file content: content of first matching file, if any. -/ +def readFile (p : Path) : Filesystem → Option FileContent + | [] => none + | e :: rest => match e with + | FileEntry.File p' c _ => if p == p' then some c else readFile p rest + | _ => readFile p rest + +/-- Write file content: update content of first matching file. -/ +def writeFile (p : Path) (content : FileContent) : Filesystem → Filesystem + | [] => [] + | e :: rest => match e with + | FileEntry.File p' c m => + if p == p' then FileEntry.File p' content m :: rest + else FileEntry.File p' c m :: writeFile p content rest + | _ => e :: writeFile p content rest + +/-- Get file metadata: metadata of first matching entry. -/ +def stat (p : Path) : Filesystem → Option FileMetadata + | [] => none + | e :: rest => match e with + | FileEntry.File p' _ m => if p == p' then some m else stat p rest + | FileEntry.Directory p' _ m => if p == p' then some m else stat p rest + | FileEntry.Symlink p' _ m => if p == p' then some m else stat p rest + +/-- Change permissions of first matching entry. -/ +def chmod (p : Path) (perms : PermSet) : Filesystem → Filesystem + | [] => [] + | e :: rest => match e with + | FileEntry.File p' c m => + if p == p' then FileEntry.File p' c (set_perms perms m) :: rest + else FileEntry.File p' c m :: chmod p perms rest + | FileEntry.Directory p' es m => + if p == p' then FileEntry.Directory p' es (set_perms perms m) :: rest + else FileEntry.Directory p' es m :: chmod p perms rest + | FileEntry.Symlink p' t m => + if p == p' then FileEntry.Symlink p' t (set_perms perms m) :: rest + else FileEntry.Symlink p' t m :: chmod p perms rest + +/-- Change owner of first matching entry. -/ +def chown (p : Path) (o : Nat) : Filesystem → Filesystem + | [] => [] + | e :: rest => match e with + | FileEntry.File p' c m => + if p == p' then FileEntry.File p' c (set_owner o m) :: rest + else FileEntry.File p' c m :: chown p o rest + | FileEntry.Directory p' es m => + if p == p' then FileEntry.Directory p' es (set_owner o m) :: rest + else FileEntry.Directory p' es m :: chown p o rest + | FileEntry.Symlink p' t m => + if p == p' then FileEntry.Symlink p' t (set_owner o m) :: rest + else FileEntry.Symlink p' t m :: chown p o rest + +/-- Rename/move file: retargets path of first matching entry. -/ +def rename (p1 p2 : Path) : Filesystem → Filesystem + | [] => [] + | e :: rest => + if p1 == path_of e then set_path p2 e :: rest + else e :: rename p1 p2 rest + +/-- Snapshot operation: capture current filesystem state. -/ +def snapshot (fs : Filesystem) : Filesystem := fs + +/-- Restore operation: restore from snapshot. -/ +def restore (snap : Filesystem) (_current : Filesystem) : Filesystem := snap + +/-! ## Helper lemmas -/ + +lemma no_dir_dir_exists_false (p : Path) (fs : Filesystem) (h : noDirAt p fs) : + dir_exists p fs = false := by + induction fs with + | nil => rfl + | cons e rest ih => + cases e with + | Directory p' es m => + have h_not : p ≠ p' := h (FileEntry.Directory p' es m) (List.Mem.head _) + have h_beq : (p == p') = false := beq_false_of_ne h_not + have h_rest : noDirAt p rest := fun e' he' => h e' (List.Mem.tail _ he') + show ((p == p') || dir_exists p rest) = false + rw [h_beq, ih h_rest] + rfl + | File p' c m => + have h_rest : noDirAt p rest := fun e' he' => h e' (List.Mem.tail _ he') + show dir_exists p rest = false + exact ih h_rest + | Symlink p' t m => + have h_rest : noDirAt p rest := fun e' he' => h e' (List.Mem.tail _ he') + show dir_exists p rest = false + exact ih h_rest + +/-! ## Operation Theorems (Ported from Coq FilesystemCNO.v) -/ + +/-- mkdir followed by rmdir is identity — on a filesystem with no directory at `p`. -/ +theorem mkdir_rmdir_inverse (p : Path) (fs : Filesystem) (h : noDirAt p fs) : + rmdir p (mkdir p fs) = fs := by + unfold mkdir + have h_false : dir_exists p fs = false := no_dir_dir_exists_false p fs h + rw [if_neg (by rw [h_false]; decide)] + show (if p == p then fs else _) = fs + rw [beq_self_eq_true p] + rfl + +/-- create followed by unlink is identity — on a filesystem with no file at `p`. -/ +theorem create_unlink_inverse (p : Path) (fs : Filesystem) (_h : noFileAt p fs) : + unlink p (create p fs) = fs := by + unfold create unlink + show (if p == p then fs else _) = fs + rw [beq_self_eq_true p] + rfl /-- read followed by write is identity -/ --- AXIOM: read_write_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md. -axiom read_write_identity (p : Path) (fs : Filesystem) (content : FileContent) : - readFile p fs = some content → - writeFile p content fs = fs +theorem read_write_identity (p : Path) (fs : Filesystem) (content : FileContent) + (h : readFile p fs = some content) : + writeFile p content fs = fs := by + induction fs with + | nil => contradiction + | cons e rest ih => + cases e with + | File p' c m => + by_cases hp : p == p' + · have hp_eq : p = p' := eq_of_beq hp + subst hp_eq + show (if p' == p' then FileEntry.File p' content m :: rest else _) = FileEntry.File p' c m :: rest + rw [beq_self_eq_true p'] + have h_content : c = content := by + revert h + show (if p' == p' then some c else readFile p' rest) = some content → c = content + rw [beq_self_eq_true p'] + intro h_eq; injection h_eq + subst h_content + rfl + · have h_read : readFile p rest = some content := by + revert h + show (if p == p' then some c else readFile p rest) = some content → readFile p rest = some content + rw [if_neg hp] + exact id + show (if p == p' then _ else FileEntry.File p' c m :: writeFile p content rest) = FileEntry.File p' c m :: rest + rw [if_neg hp] + rw [ih h_read] + | Directory p' es m => + have h_read : readFile p rest = some content := h + show FileEntry.Directory p' es m :: writeFile p content rest = FileEntry.Directory p' es m :: rest + rw [ih h_read] + | Symlink p' t m => + have h_read : readFile p rest = some content := h + show FileEntry.Symlink p' t m :: writeFile p content rest = FileEntry.Symlink p' t m :: rest + rw [ih h_read] /-- chmod to current permissions is identity -/ --- AXIOM: chmod_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md. -axiom chmod_identity (p : Path) (fs : Filesystem) (meta : FileMetadata) : - stat p fs = some meta → - chmod p meta.permissions fs = fs +theorem chmod_identity (p : Path) (fs : Filesystem) (meta : FileMetadata) + (h : stat p fs = some meta) : + chmod p meta.permissions fs = fs := by + induction fs with + | nil => contradiction + | cons e rest ih => + cases e with + | File p' c m => + by_cases hp : p == p' + · have hp_eq : p = p' := eq_of_beq hp + subst hp_eq + show (if p' == p' then FileEntry.File p' c (set_perms meta.permissions m) :: rest else _) = FileEntry.File p' c m :: rest + rw [beq_self_eq_true p'] + have h_meta : m = meta := by + revert h + show (if p' == p' then some m else stat p' rest) = some meta → m = meta + rw [beq_self_eq_true p'] + intro h_eq; injection h_eq + subst h_meta + rw [set_perms_id] + · have h_stat : stat p rest = some meta := by + revert h + show (if p == p' then some m else stat p rest) = some meta → stat p rest = some meta + rw [if_neg hp] + exact id + show (if p == p' then _ else FileEntry.File p' c m :: chmod p meta.permissions rest) = FileEntry.File p' c m :: rest + rw [if_neg hp] + rw [ih h_stat] + | Directory p' es m => + by_cases hp : p == p' + · have hp_eq : p = p' := eq_of_beq hp + subst hp_eq + show (if p' == p' then FileEntry.Directory p' es (set_perms meta.permissions m) :: rest else _) = FileEntry.Directory p' es m :: rest + rw [beq_self_eq_true p'] + have h_meta : m = meta := by + revert h + show (if p' == p' then some m else stat p' rest) = some meta → m = meta + rw [beq_self_eq_true p'] + intro h_eq; injection h_eq + subst h_meta + rw [set_perms_id] + · have h_stat : stat p rest = some meta := by + revert h + show (if p == p' then some m else stat p rest) = some meta → stat p rest = some meta + rw [if_neg hp] + exact id + show (if p == p' then _ else FileEntry.Directory p' es m :: chmod p meta.permissions rest) = FileEntry.Directory p' es m :: rest + rw [if_neg hp] + rw [ih h_stat] + | Symlink p' t m => + by_cases hp : p == p' + · have hp_eq : p = p' := eq_of_beq hp + subst hp_eq + show (if p' == p' then FileEntry.Symlink p' t (set_perms meta.permissions m) :: rest else _) = FileEntry.Symlink p' t m :: rest + rw [beq_self_eq_true p'] + have h_meta : m = meta := by + revert h + show (if p' == p' then some m else stat p' rest) = some meta → m = meta + rw [beq_self_eq_true p'] + intro h_eq; injection h_eq + subst h_meta + rw [set_perms_id] + · have h_stat : stat p rest = some meta := by + revert h + show (if p == p' then some m else stat p rest) = some meta → stat p rest = some meta + rw [if_neg hp] + exact id + show (if p == p' then _ else FileEntry.Symlink p' t m :: chmod p meta.permissions rest) = FileEntry.Symlink p' t m :: rest + rw [if_neg hp] + rw [ih h_stat] /-- rename to same path is identity -/ --- AXIOM: rename_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md. -axiom rename_identity (p : Path) (fs : Filesystem) : - rename p p fs = fs - -/-- rename A to B followed by rename B to A is identity — when `p1 ≠ p2` and - nothing lives at `p2` (both preconditions Coq's `rename_inverse` states). -/ --- AXIOM: rename_inverse; POSIX-semantics specification (mirrors Coq Lemma, same preconditions); §(c) per docs/proof-debt.md. -axiom rename_inverse (p1 p2 : Path) (fs : Filesystem) : - p1 ≠ p2 → - noEntryAt p2 fs → - rename p2 p1 (rename p1 p2 fs) = fs +theorem rename_identity (p : Path) (fs : Filesystem) : + rename p p fs = fs := by + induction fs with + | nil => rfl + | cons e rest ih => + show (if p == path_of e then set_path p e :: rest else e :: rename p p rest) = e :: rest + by_cases hp : p == path_of e + · rw [if_pos hp] + have hp_eq : p = path_of e := eq_of_beq hp + subst hp_eq + rw [set_path_id] + · rw [if_neg hp] + rw [ih] + +/-- rename A to B followed by rename B to A is identity -/ +theorem rename_inverse (p1 p2 : Path) (fs : Filesystem) (hneq : p1 ≠ p2) (hno : noEntryAt p2 fs) : + rename p2 p1 (rename p1 p2 fs) = fs := by + induction fs with + | nil => rfl + | cons e rest ih => + show rename p2 p1 (if p1 == path_of e then set_path p2 e :: rest else e :: rename p1 p2 rest) = e :: rest + by_cases hp1 : p1 == path_of e + · rw [if_pos hp1] + show (if p2 == path_of (set_path p2 e) then set_path p1 (set_path p2 e) :: rest else _) = e :: rest + rw [path_of_set_path] + rw [beq_self_eq_true p2] + rw [if_pos rfl] + rw [set_path_set_path] + have hp1_eq : p1 = path_of e := eq_of_beq hp1 + subst hp1_eq + rw [set_path_id] + · rw [if_neg hp1] + show (if p2 == path_of e then _ else e :: rename p2 p1 (rename p1 p2 rest)) = e :: rest + have hp2_ne : p2 ≠ path_of e := by + intro h_contra + specialize hno e (List.Mem.head _) + cases e with + | File p' _ _ => exact hno h_contra + | Directory p' _ _ => exact hno h_contra + | Symlink p' _ _ => exact hno h_contra + have hp2_beq : (p2 == path_of e) = false := beq_false_of_ne hp2_ne + rw [if_neg (by rw [hp2_beq]; decide)] + have hno_rest : noEntryAt p2 rest := fun e' he' => hno e' (List.Mem.tail _ he') + rw [ih hno_rest] + +/-- snapshot followed by restore is identity -/ +theorem snapshot_restore_identity (fs : Filesystem) : + restore (snapshot fs) fs = fs := rfl /-! ## Filesystem CNO Definition -/ @@ -179,31 +436,28 @@ theorem fs_nop_is_cno : isFsCNO fs_nop := by intro fs rfl -/-- mkdir followed by rmdir. `noncomputable` — calls axioms `mkdir`/`rmdir`. -/ -noncomputable def mkdirRmdirOp (p : Path) : FsOp := +/-- mkdir followed by rmdir. -/ +def mkdirRmdirOp (p : Path) : FsOp := fun fs => rmdir p (mkdir p fs) -/-- mkdir;rmdir is the identity on every filesystem with no directory at `p` - (Coq `mkdir_rmdir_is_cno`, same statement). The unconditional - `isFsCNO (mkdirRmdirOp p)` is not provable and is false on the Coq model. -/ +/-- mkdir;rmdir is the identity on every filesystem with no directory at `p`. -/ theorem mkdir_rmdir_is_cno (p : Path) (fs : Filesystem) (h : noDirAt p fs) : mkdirRmdirOp p fs = fs := by unfold mkdirRmdirOp exact mkdir_rmdir_inverse p fs h -/-- create followed by unlink. `noncomputable` — wraps axioms. -/ -noncomputable def createUnlinkOp (p : Path) : FsOp := +/-- create followed by unlink. -/ +def createUnlinkOp (p : Path) : FsOp := fun fs => unlink p (create p fs) -/-- create;unlink is the identity on every filesystem with no file at `p` - (Coq `create_unlink_is_cno`, same statement). -/ +/-- create;unlink is the identity on every filesystem with no file at `p`. -/ theorem create_unlink_is_cno (p : Path) (fs : Filesystem) (h : noFileAt p fs) : createUnlinkOp p fs = fs := by unfold createUnlinkOp exact create_unlink_inverse p fs h -/-- read followed by write. `noncomputable` — wraps axioms. -/ -noncomputable def readWriteOp (p : Path) : FsOp := +/-- read followed by write. -/ +def readWriteOp (p : Path) : FsOp := fun fs => match readFile p fs with | some content => writeFile p content fs @@ -218,8 +472,8 @@ theorem read_write_is_cno (p : Path) : | some content => exact read_write_identity p fs content h -/-- chmod to current permissions. `noncomputable` — wraps axioms. -/ -noncomputable def chmodNopOp (p : Path) : FsOp := +/-- chmod to current permissions. -/ +def chmodNopOp (p : Path) : FsOp := fun fs => match stat p fs with | some meta => chmod p meta.permissions fs @@ -234,8 +488,8 @@ theorem chmod_nop_is_cno (p : Path) : | some meta => exact chmod_identity p fs meta h -/-- rename to same path. `noncomputable` — wraps axiom. -/ -noncomputable def renameNopOp (p : Path) : FsOp := +/-- rename to same path. -/ +def renameNopOp (p : Path) : FsOp := fun fs => rename p p fs theorem rename_nop_is_cno (p : Path) : @@ -265,10 +519,13 @@ theorem fs_cno_composition (op1 op2 : FsOp) : /-! ## Non-CNO Operations -/ -/-- mkdir alone is NOT a CNO. Coq proves this Lemma on its concrete model - (`exists "" nil`); over opaque operations it has to be assumed. -/ --- AXIOM: mkdir_not_identity; mirrors the Coq Lemma (proved on the concrete model); §(c) per docs/proof-debt.md. -axiom mkdir_not_identity : ∃ (p : Path) (fs : Filesystem), mkdir p fs ≠ fs +/-- mkdir alone is NOT a CNO. -/ +theorem mkdir_not_identity : ∃ (p : Path) (fs : Filesystem), mkdir p fs ≠ fs := by + exists "" + exists [] + unfold mkdir dir_exists + intro h + contradiction theorem mkdir_alone_not_cno : ¬ (∀ p, isFsCNO (fun fs => mkdir p fs)) := by @@ -308,21 +565,7 @@ example (p : Path) (fs : Filesystem) (h : noFileAt p fs) : /-! ## Snapshot and Restore -/ -/-- Snapshot operation -/ --- AXIOM: snapshot; opaque snapshot primitive; §(c) per docs/proof-debt.md. -axiom snapshot : Filesystem → Filesystem - -/-- Restore from snapshot -/ --- AXIOM: restore; opaque restore primitive; §(c) per docs/proof-debt.md. -axiom restore : Filesystem → Filesystem → Filesystem - -/-- snapshot followed by restore is identity -/ -axiom snapshot_restore_identity (fs : Filesystem) : - restore (snapshot fs) fs = fs - --- `noncomputable` because `restore` and `snapshot` are axioms with no --- executable body; without this Lean 4.16 refuses to emit code for `def`. -noncomputable def snapshotRestoreOp : FsOp := +def snapshotRestoreOp : FsOp := fun fs => restore (snapshot fs) fs theorem snapshot_restore_is_cno : @@ -337,20 +580,22 @@ theorem snapshot_restore_is_cno : def isIdempotent (op : FsOp) : Prop := ∀ fs, op (op fs) = op fs -/-- mkdir is idempotent (but not CNO). Coq proves this Lemma on its concrete - model; over opaque operations it has to be assumed. Consistent with the - conditional `mkdir_rmdir_inverse`: `mkdir p fs` has a directory at `p`, - so the inverse law does not apply to it. -/ --- AXIOM: mkdir_idempotent; mirrors the Coq Lemma (proved on the concrete model); §(c) per docs/proof-debt.md. -axiom mkdir_idempotent (p : Path) : - isIdempotent (fun fs => mkdir p fs) - -/-- The unconditional law `∀ p fs, rmdir p (mkdir p fs) = fs` — the former - statement of `mkdir_rmdir_inverse` — is refuted by `mkdir_idempotent` and - `mkdir_not_identity` alone: on `mkdir p fs` the second `mkdir` is a no-op, - so the law would force `mkdir p fs = fs`. This is the derivation that - made issue #125's `False` proof go through; it is now a theorem about the - old statement instead of a contradiction in the axioms. -/ +/-- mkdir is idempotent (but not CNO). -/ +theorem mkdir_idempotent (p : Path) : + isIdempotent (fun fs => mkdir p fs) := by + intro fs + unfold mkdir + by_cases h : dir_exists p fs = true + · rw [if_pos h, if_pos h] + · rw [if_neg h] + have h_dir : dir_exists p (FileEntry.Directory p [] default_meta :: fs) = true := by + show ((p == p) || dir_exists p fs) = true + rw [beq_self_eq_true p] + rfl + rw [if_pos h_dir] + +/-- The unconditional law `∀ p fs, rmdir p (mkdir p fs) = fs` is refuted by + `mkdir_idempotent` and `mkdir_not_identity`. -/ theorem unconditional_mkdir_rmdir_inverse_is_false : ¬ ∀ (p : Path) (fs : Filesystem), rmdir p (mkdir p fs) = fs := by intro law @@ -360,11 +605,7 @@ theorem unconditional_mkdir_rmdir_inverse_is_false : rw [h2, law p fs] at h1 exact hne h1.symm -/-- Idempotent does NOT imply CNO. - Proof: destructure mkdir_not_identity to get a specific (p, fs) where - mkdir p fs ≠ fs, then exhibit `fun fs => mkdir p fs` as the witness. - It is idempotent (mkdir_idempotent), but it cannot be a CNO: if it were, - applying it to fs would leave fs unchanged, contradicting h_neq. -/ +/-- Idempotent does NOT imply CNO. -/ example : ∃ op : FsOp, isIdempotent op ∧ ¬ isFsCNO op := by obtain ⟨p, fs, h_neq⟩ := mkdir_not_identity exists (fun fs' => mkdir p fs') diff --git a/proofs/tests/gate-selftest.sh b/proofs/tests/gate-selftest.sh index 836b9c3..76489a6 100755 --- a/proofs/tests/gate-selftest.sh +++ b/proofs/tests/gate-selftest.sh @@ -55,7 +55,7 @@ for s in "$STUB"/*; do sh -n "$s" || { echo "FAIL: stub $s does not parse"; exit OUT=""; RC=0 # run_gate: capture the gate's output and exit status with the stub toolchain. -run_gate() { OUT="$(HOME="$SCRATCH/home" PATH="$STUB:/usr/bin:/bin" MIZFILES="${MIZ-$SCRATCH/miz}" bash "$GATE" 2>&1)"; RC=$?; } +run_gate() { OUT="$(HOME="$SCRATCH/home" PATH="$STUB:/usr/bin:/bin" MIZFILES="${MIZ-$SCRATCH/miz}" SKIP_ISABELLE="${SKIP_ISABELLE:-0}" SKIP_MIZAR="${SKIP_MIZAR:-0}" bash "$GATE" 2>&1)"; RC=$?; } # expect