From d74e907c25b14b4868d2bb31f817f4099213cacd Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 15:49:56 +0000 Subject: [PATCH 1/3] Archive non-active provers; migrate a2ml to deed and K9; CodeRabbit config - Owner ruling 2026-10-10: active proof stack is Idris 2 and Agda (Z3 as solver). Coq, Lean 4, Isabelle and Mizar moved to archive/proofs/ with the six-prover gate and self-test. New gate: proofs/verify-active-provers.sh. - proofs.yml: agda, z3 and idris jobs. Idris job builds absolute-zero-abi.ipkg on the digest-pinned image used by pages.yml. Not yet run on CI. - Containerfile and .gitlab-ci.yml: Coq/Lean/Isabelle build and verify removed. - A2ML retired: 20 sources archived to archive/a2ml-v1/ (ledger alongside). Added absolute-zero_chora.deed, six K9 contracts under .machine_readable/contractiles//, and coordination.k9. - .coderabbit.yaml: docstring finishing touch disabled (D217). - Justfile copies kept identical (#76). - ULTRAPLAN revision 2 at docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc. Not verified: Nickel L2, deed-validate CI, Hunt contract signatures (K-1), Agda/Z3/Idris2 runs. Commits are unsigned. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .claude/CLAUDE.md | 18 +- .coderabbit.yaml | 19 + .github/workflows/proofs.yml | 88 +- .gitlab-ci.yml | 38 +- .machine_readable/bot_directives/README.adoc | 3 + .machine_readable/contractiles/Justfile | 96 +- .../contractiles/adjust/adjust.k9.ncl | 112 +++ .../contractiles/bust/bust.k9.ncl | 116 +++ .../contractiles/dust/dust.k9.ncl | 102 ++ .../contractiles/intend/intend.k9.ncl | 145 +++ .../contractiles/must/must.k9.ncl | 154 +++ .../contractiles/trust/trust.k9.ncl | 171 ++++ .machine_readable/descriptiles/README.adoc | 3 + .../descriptiles/anchor/README.adoc | 3 + Containerfile | 5 +- Justfile | 96 +- PROOF-STATUS.adoc | 5 + README.adoc | 6 + absolute-zero_chora.deed | 249 +++++ archive/README.adoc | 74 ++ archive/a2ml-v1/MIGRATION-LEDGER.adoc | 190 ++++ .../audits-assail-classifications.a2ml.txt | 0 .../bot_directives-git-private-farm.a2ml.txt | 0 .../bot_directives-gitbot-fleet.a2ml.txt | 0 .../a2ml-v1/bot_directives-hypatia.a2ml.txt | 0 .../a2ml-v1/contractiles-Adjustfile.a2ml.txt | 0 .../a2ml-v1/contractiles-Bustfile.a2ml.txt | 0 .../a2ml-v1/contractiles-Dustfile.a2ml.txt | 0 .../a2ml-v1/contractiles-Intentfile.a2ml.txt | 0 .../a2ml-v1/contractiles-Mustfile.a2ml.txt | 0 .../a2ml-v1/contractiles-Trustfile.a2ml.txt | 0 .../descriptiles-0-AI-MANIFEST.a2ml.txt | 0 .../a2ml-v1/descriptiles-AGENTIC.a2ml.txt | 0 .../a2ml-v1/descriptiles-ECOSYSTEM.a2ml.txt | 0 .../a2ml-v1/descriptiles-META.a2ml.txt | 0 .../a2ml-v1/descriptiles-NEUROSYM.a2ml.txt | 0 .../a2ml-v1/descriptiles-PLAYBOOK.a2ml.txt | 0 .../a2ml-v1/descriptiles-STATE.a2ml.txt | 0 ...descriptiles-anchor-0-AI-MANIFEST.a2ml.txt | 0 .../descriptiles-anchor-ANCHOR.a2ml.txt | 0 .../a2ml-v1/root-0-AI-MANIFEST.a2ml.txt | 0 {proofs => archive/proofs}/coq/_CoqProject | 0 .../proofs}/coq/audit/Assumptions.v | 0 .../proofs}/coq/category/CNOCategory.v | 0 .../proofs}/coq/census-assumptions.sh | 0 .../proofs}/coq/check-assumptions.sh | 0 .../proofs}/coq/check-axiom-tags.sh | 0 {proofs => archive/proofs}/coq/common/CNO.v | 0 .../proofs}/coq/common/Complex.v | 0 .../proofs}/coq/common/PhysicsConstants.v | 0 .../proofs}/coq/common/StatMechBasis.v | 0 .../proofs}/coq/filesystem/FilesystemCNO.v | 0 .../proofs}/coq/lambda/LambdaCNO.v | 0 .../proofs}/coq/malbolge/MalbolgeCore.v | 0 {proofs => archive/proofs}/coq/ond/OND.v | 0 .../proofs}/coq/physics/LandauerDerivation.v | 0 .../proofs}/coq/physics/StatMech.v | 0 .../proofs}/coq/physics/StatMech_helpers.v | 0 .../proofs}/coq/quantum/QuantumCNO.v | 0 .../coq/quantum/QuantumMechanicsExact.v | 0 {proofs => archive/proofs}/isabelle/CNO.thy | 0 {proofs => archive/proofs}/isabelle/OND.thy | 0 {proofs => archive/proofs}/isabelle/ROOT | 0 .../proofs}/lean4/AxiomAudit.lean | 0 {proofs => archive/proofs}/lean4/CNO.lean | 0 .../proofs}/lean4/CNOBridge.lean | 0 .../proofs}/lean4/CNOCategory.lean | 0 .../proofs}/lean4/FilesystemCNO.lean | 0 .../proofs}/lean4/LambdaCNO.lean | 0 {proofs => archive/proofs}/lean4/OND.lean | 0 .../proofs}/lean4/QuantumCNO.lean | 0 .../proofs}/lean4/StatMech.lean | 0 .../proofs}/lean4/check-core.sh | 0 .../proofs}/lean4/lake-manifest.json | 0 .../proofs}/lean4/lakefile.lean | 0 .../proofs}/lean4/lean-toolchain | 0 {proofs => archive/proofs}/mizar/CNO.miz | 0 {proofs => archive/proofs}/mizar/dict/cno.voc | 0 .../proofs/tests/gate-selftest.six-prover.sh | 0 .../proofs/verify-all-provers.six-prover.sh | 0 coordination.k9 | 128 +++ docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc | 927 ++++++++++++++++++ proofs/verify-active-provers.sh | 43 + proofs/z3/verify.sh | 2 +- 84 files changed, 2524 insertions(+), 269 deletions(-) create mode 100644 .coderabbit.yaml create mode 100644 .machine_readable/contractiles/adjust/adjust.k9.ncl create mode 100644 .machine_readable/contractiles/bust/bust.k9.ncl create mode 100644 .machine_readable/contractiles/dust/dust.k9.ncl create mode 100644 .machine_readable/contractiles/intend/intend.k9.ncl create mode 100644 .machine_readable/contractiles/must/must.k9.ncl create mode 100644 .machine_readable/contractiles/trust/trust.k9.ncl create mode 100644 absolute-zero_chora.deed create mode 100644 archive/README.adoc create mode 100644 archive/a2ml-v1/MIGRATION-LEDGER.adoc rename audits/assail-classifications.a2ml => archive/a2ml-v1/audits-assail-classifications.a2ml.txt (100%) rename .machine_readable/bot_directives/git-private-farm.a2ml => archive/a2ml-v1/bot_directives-git-private-farm.a2ml.txt (100%) rename .machine_readable/bot_directives/gitbot-fleet.a2ml => archive/a2ml-v1/bot_directives-gitbot-fleet.a2ml.txt (100%) rename .machine_readable/bot_directives/hypatia.a2ml => archive/a2ml-v1/bot_directives-hypatia.a2ml.txt (100%) rename .machine_readable/contractiles/Adjustfile.a2ml => archive/a2ml-v1/contractiles-Adjustfile.a2ml.txt (100%) rename .machine_readable/contractiles/Bustfile.a2ml => archive/a2ml-v1/contractiles-Bustfile.a2ml.txt (100%) rename .machine_readable/contractiles/Dustfile.a2ml => archive/a2ml-v1/contractiles-Dustfile.a2ml.txt (100%) rename .machine_readable/contractiles/Intentfile.a2ml => archive/a2ml-v1/contractiles-Intentfile.a2ml.txt (100%) rename .machine_readable/contractiles/Mustfile.a2ml => archive/a2ml-v1/contractiles-Mustfile.a2ml.txt (100%) rename .machine_readable/contractiles/Trustfile.a2ml => archive/a2ml-v1/contractiles-Trustfile.a2ml.txt (100%) rename .machine_readable/descriptiles/0-AI-MANIFEST.a2ml => archive/a2ml-v1/descriptiles-0-AI-MANIFEST.a2ml.txt (100%) rename .machine_readable/descriptiles/AGENTIC.a2ml => archive/a2ml-v1/descriptiles-AGENTIC.a2ml.txt (100%) rename .machine_readable/descriptiles/ECOSYSTEM.a2ml => archive/a2ml-v1/descriptiles-ECOSYSTEM.a2ml.txt (100%) rename .machine_readable/descriptiles/META.a2ml => archive/a2ml-v1/descriptiles-META.a2ml.txt (100%) rename .machine_readable/descriptiles/NEUROSYM.a2ml => archive/a2ml-v1/descriptiles-NEUROSYM.a2ml.txt (100%) rename .machine_readable/descriptiles/PLAYBOOK.a2ml => archive/a2ml-v1/descriptiles-PLAYBOOK.a2ml.txt (100%) rename .machine_readable/descriptiles/STATE.a2ml => archive/a2ml-v1/descriptiles-STATE.a2ml.txt (100%) rename .machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml => archive/a2ml-v1/descriptiles-anchor-0-AI-MANIFEST.a2ml.txt (100%) rename .machine_readable/descriptiles/anchor/ANCHOR.a2ml => archive/a2ml-v1/descriptiles-anchor-ANCHOR.a2ml.txt (100%) rename 0-AI-MANIFEST.a2ml => archive/a2ml-v1/root-0-AI-MANIFEST.a2ml.txt (100%) rename {proofs => archive/proofs}/coq/_CoqProject (100%) rename {proofs => archive/proofs}/coq/audit/Assumptions.v (100%) rename {proofs => archive/proofs}/coq/category/CNOCategory.v (100%) rename {proofs => archive/proofs}/coq/census-assumptions.sh (100%) rename {proofs => archive/proofs}/coq/check-assumptions.sh (100%) rename {proofs => archive/proofs}/coq/check-axiom-tags.sh (100%) rename {proofs => archive/proofs}/coq/common/CNO.v (100%) rename {proofs => archive/proofs}/coq/common/Complex.v (100%) rename {proofs => archive/proofs}/coq/common/PhysicsConstants.v (100%) rename {proofs => archive/proofs}/coq/common/StatMechBasis.v (100%) rename {proofs => archive/proofs}/coq/filesystem/FilesystemCNO.v (100%) rename {proofs => archive/proofs}/coq/lambda/LambdaCNO.v (100%) rename {proofs => archive/proofs}/coq/malbolge/MalbolgeCore.v (100%) rename {proofs => archive/proofs}/coq/ond/OND.v (100%) rename {proofs => archive/proofs}/coq/physics/LandauerDerivation.v (100%) rename {proofs => archive/proofs}/coq/physics/StatMech.v (100%) rename {proofs => archive/proofs}/coq/physics/StatMech_helpers.v (100%) rename {proofs => archive/proofs}/coq/quantum/QuantumCNO.v (100%) rename {proofs => archive/proofs}/coq/quantum/QuantumMechanicsExact.v (100%) rename {proofs => archive/proofs}/isabelle/CNO.thy (100%) rename {proofs => archive/proofs}/isabelle/OND.thy (100%) rename {proofs => archive/proofs}/isabelle/ROOT (100%) rename {proofs => archive/proofs}/lean4/AxiomAudit.lean (100%) rename {proofs => archive/proofs}/lean4/CNO.lean (100%) rename {proofs => archive/proofs}/lean4/CNOBridge.lean (100%) rename {proofs => archive/proofs}/lean4/CNOCategory.lean (100%) rename {proofs => archive/proofs}/lean4/FilesystemCNO.lean (100%) rename {proofs => archive/proofs}/lean4/LambdaCNO.lean (100%) rename {proofs => archive/proofs}/lean4/OND.lean (100%) rename {proofs => archive/proofs}/lean4/QuantumCNO.lean (100%) rename {proofs => archive/proofs}/lean4/StatMech.lean (100%) rename {proofs => archive/proofs}/lean4/check-core.sh (100%) rename {proofs => archive/proofs}/lean4/lake-manifest.json (100%) rename {proofs => archive/proofs}/lean4/lakefile.lean (100%) rename {proofs => archive/proofs}/lean4/lean-toolchain (100%) rename {proofs => archive/proofs}/mizar/CNO.miz (100%) rename {proofs => archive/proofs}/mizar/dict/cno.voc (100%) rename proofs/tests/gate-selftest.sh => archive/proofs/tests/gate-selftest.six-prover.sh (100%) rename proofs/verify-all-provers.sh => archive/proofs/verify-all-provers.six-prover.sh (100%) create mode 100644 coordination.k9 create mode 100644 docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc create mode 100755 proofs/verify-active-provers.sh diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index f60d504..fef31e1 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -1,14 +1,14 @@ ## Machine-Readable Artefacts -The following files in `.machine_readable/descriptiles/` contain structured -project metadata (a2ml is TOML-flavoured, not Guile Scheme): +A2ML is retired (standards D99, D269c, D312, D313). The old `.a2ml` sources are +archived under `archive/a2ml-v1/` and must not be recreated or extended. Use: -- `STATE.a2ml` - Current project state and progress -- `META.a2ml` - Architecture decisions and development practices -- `ECOSYSTEM.a2ml` - Position in the ecosystem and related projects -- `AGENTIC.a2ml` - AI agent interaction patterns -- `NEUROSYM.a2ml` - Neurosymbolic integration config -- `PLAYBOOK.a2ml` - Operational runbook +- `absolute-zero_chora.deed` - project metadata (state, ecosystem, agentic and + policy clauses). Deed grammar; validate with the estate deed linter. +- `.machine_readable/contractiles//.k9.ncl` - the six contracts + (must, trust, dust, bust, adjust, intend). The four Hunt contracts are unsigned + and must not run as Hunt until signed (ledger K-1). +- `coordination.k9` - coordination metadata (repo root). --- @@ -29,7 +29,7 @@ project metadata (a2ml is TOML-flavoured, not Guile Scheme): | **Bash/POSIX Shell** | Scripts, automation | Keep minimal | | **JavaScript** | Only where AffineScript cannot, or as per-language reference (examples/) | Avoid for new code unless integrating an external JS API | | **Nickel** | Configuration language | For complex configs | -| **Guile Scheme** | Scripting where needed | (state/meta files are `.machine_readable/descriptiles/*.a2ml`, TOML-flavoured) | +| **Guile Scheme** | Scripting where needed | (metadata is `_chora.deed`; contracts are `*.k9.ncl`; see Machine-Readable Artefacts) | | **Julia** | Batch scripts, data processing | Per RSR | | **OCaml** | AffineScript compiler | Language-specific | | **Ada** | Safety-critical systems | Where required | diff --git a/.coderabbit.yaml b/.coderabbit.yaml new file mode 100644 index 0000000..b5f5dd5 --- /dev/null +++ b/.coderabbit.yaml @@ -0,0 +1,19 @@ +# SPDX-License-Identifier: MPL-2.0 +# CodeRabbit configuration. Schema: https://coderabbit.ai/integrations/schema.v2.json +# +# Ruling D217: CodeRabbit does not push commits to PR branches. Bot commits on a +# PR branch are unsigned and fail the estate signed-commit floor. The docstring +# finishing touch below is the feature that commits to the branch, so it is +# disabled here. The matching app-UI setting must also be off; it lives outside +# this repo and is tracked in the ULTRAPLAN. +# +# The docstring pre-merge check stays advisory (mode: warning), as in +# rsr-template-repo. CodeRabbit is advisory. +reviews: + pre_merge_checks: + docstrings: + mode: warning + threshold: 80 + finishing_touches: + docstrings: + enabled: false diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index a915123..ef776d2 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -1,23 +1,15 @@ # This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 -# This workflow is managed by gh actions-lock. -# This workflow is managed by gh actions-lock. # Copyright (c) Jonathan D.A. Jewell # -# Proof verification CI. Runs the LIGHTWEIGHT provers that are fast and reliable -# on a standard GitHub runner — Coq (both pillars, all 14 theories), Agda (CNO + -# OND), and Z3 (CNO + OND bounded instances). Each is an INDEPENDENT job, so one -# flaking never blocks the others. +# Proof verification CI for the ACTIVE proof stack (owner ruling 2026-10-10): +# * Agda — CNO + OND + EchoBridge (--safe --without-K) +# * Z3 — CNO + OND bounded checks (expect-annotated) +# * Idris 2 — the ABI package (absolute-zero-abi.ipkg) +# Each is an INDEPENDENT job, so one flaking never blocks the others. # -# The Mathlib-free Lean core (CNO, OND, CNOCategory, CNOBridge, FilesystemCNO, -# LambdaCNO) is built here too, with the toolchain pinned in -# proofs/lean4/lean-toolchain, and proofs/lean4/AxiomAudit.lean pins the -# signature of every axiom and the axiom list of every theorem (issue #125). -# -# The heavy provers (Lean + multi-GB Mathlib for QuantumCNO/StatMech, Isabelle -# ~1.2 GB, Mizar i386 + MML, Idris 2 from source) are NOT run here — they are -# covered by the local/container gate `proofs/verify-all-provers.sh` -# (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc. +# Coq, Lean 4, Isabelle/HOL and Mizar are ARCHIVED under archive/proofs/ and are +# not gated here. See archive/README.adoc for the archive and its status. name: Proofs on: @@ -26,11 +18,11 @@ on: pull_request: paths: - 'proofs/**' + - 'src/abi/**' - 'absolute-zero-abi.ipkg' - '.github/workflows/proofs.yml' - 'Justfile' - '*.agda-lib' - - 'lakefile*' permissions: contents: read @@ -41,37 +33,8 @@ concurrency: cancel-in-progress: true jobs: - coq: - name: Coq — CNO + OND (14 theories) - runs-on: ubuntu-24.04 - steps: - - uses: actions/checkout@v7.0.1 - - name: Install Coq - run: sudo apt-get update && sudo apt-get install -y coq - - name: Build all theories via coq_makefile - working-directory: proofs/coq - run: | - coqc --version - coq_makefile -f _CoqProject -o Makefile.all - make -f Makefile.all -j"$(nproc)" - echo "✓ Coq: 14/14 theories compiled (CNO + OND)" - - name: Print Assumptions gate (17 named theorems closed) + control - working-directory: proofs/coq - 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 + name: Agda — CNO + OND + EchoBridge runs-on: ubuntu-24.04 timeout-minutes: 25 steps: @@ -114,25 +77,22 @@ jobs: z3 --version bash proofs/z3/verify.sh echo "✓ Z3: every (check-sat) verdict matched its ; expect annotation" - - name: Gate self-test (stub provers + z3 mutants must turn the gate red) - run: bash proofs/tests/gate-selftest.sh - lean: - name: Lean — core CNO (6 modules + axiom audit) - runs-on: ubuntu-24.04 - timeout-minutes: 20 + idris: + name: Idris 2 — ABI package (absolute-zero-abi.ipkg) + runs-on: ubuntu-latest + timeout-minutes: 30 + container: + # Same pinned idris2-pack image as pages.yml (digest-pinned). + image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff steps: - uses: actions/checkout@v7.0.1 - - name: Install elan v4.2.4 (sha256-verified) and the pinned toolchain - # elan is fetched as a release tarball and checksum-verified rather than - # via a third-party action, so the repo's Actions allow-list is not in - # play. The toolchain itself comes from proofs/lean4/lean-toolchain. + - name: Build the ABI package (type-checks every src/abi module) + run: | + idris2 --version + idris2 --build absolute-zero-abi.ipkg + echo "✓ Idris 2: absolute-zero-abi.ipkg builds" + - name: Advisory — believe_me sites in src/abi (issue #27; not gated) run: | - curl -fsSL --retry 3 -o elan.tgz \ - https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz - echo "42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 elan.tgz" | sha256sum -c - - tar -xzf elan.tgz - ./elan-init -y --no-modify-path --default-toolchain none - echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - - name: Build the six Mathlib-free modules and run the axiom audit - run: bash proofs/lean4/check-core.sh + n=$(grep -rn 'believe_me' src/abi --include='*.idr' | grep -v -- '--' | wc -l) + echo "believe_me code sites in src/abi: $n (tracked in #27; advisory, not a gate)" diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 29dbbba..cc47432 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -46,20 +46,6 @@ build:affinescript: # Verification Stage # ============================================================================ -verify:coq: - stage: verify - image: coqorg/coq:latest - script: - - cd proofs/coq/common - - coqc CNO.v - - cd ../malbolge - - coqc -R ../common CNO MalbolgeCore.v - artifacts: - paths: - - proofs/coq/**/*.vo - expire_in: 1 day - allow_failure: false - verify:z3: stage: verify image: ubuntu:22.04 @@ -70,26 +56,6 @@ verify:z3: - z3 cno_properties.smt2 allow_failure: false -verify:lean4: - stage: verify - image: leanprover/lean4:latest - script: - - cd proofs/lean4 - - lake build - artifacts: - paths: - - proofs/lean4/.lake/ - expire_in: 1 day - allow_failure: true # Lean 4 may not be fully set up - -verify:isabelle: - stage: verify - image: makarius/isabelle:latest - script: - - isabelle build -D proofs/isabelle - allow_failure: true # Isabelle setup may vary - -# ============================================================================ # Test Stage # ============================================================================ @@ -140,10 +106,8 @@ verify:summary: - echo "==========================================" - echo "Multi-Prover Verification Summary" - echo "==========================================" - - echo "Coq: ✓ (if verify:coq passed)" - echo "Z3: ✓ (if verify:z3 passed)" - - echo "Lean 4: ⚠ (if verify:lean4 passed, else optional)" - - echo "Isabelle: ⚠ (if verify:isabelle passed, else optional)" + - echo "Coq, Lean 4, Isabelle: archived under archive/proofs/ (retired 2026-10-10; not gated)" - echo "" - echo "Multi-prover agreement increases confidence!" when: always diff --git a/.machine_readable/bot_directives/README.adoc b/.machine_readable/bot_directives/README.adoc index dc3a91d..8a76cae 100644 --- a/.machine_readable/bot_directives/README.adoc +++ b/.machine_readable/bot_directives/README.adoc @@ -1,6 +1,9 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = bot_directives — per-repo directives for automated agents + +NOTE: Retired 2026-10-10. The A2ML files described below are archived under `archive/a2ml-v1/` (see `archive/a2ml-v1/MIGRATION-LEDGER.adoc`). Repository metadata now lives in `absolute-zero_chora.deed`, and contracts live in `.machine_readable/contractiles//.k9.ncl`. The text below describes the retired set and is kept as history until it is rewritten. + :toc: == Purpose diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index 83d8504..3d86215 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -13,45 +13,19 @@ default: # ============================================================================ # Build Commands # ============================================================================ +# Active proof stack (owner ruling 2026-10-10): Idris 2 (ABI) and Agda (CNO + +# OND), plus Z3 bounded checks. Coq, Lean 4, Isabelle/HOL and Mizar are archived +# under archive/proofs/ and are not built or gated here. -# Build everything (all six prover backends + the Idris ABI) -build-all: build-coq build-lean build-agda build-isabelle build-mizar build-idris +# Build the active provers and the Idris ABI +build-all: build-agda build-idris @echo "✓ All builds complete" -# Build Coq proofs — all 14 theories (CNO + OND pillars) via coq_makefile -build-coq: - @echo "Building Coq proofs (14 theories, both pillars)..." - @if command -v coqc >/dev/null 2>&1; then \ - 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 (CNO libs + OND; needs Mathlib cache) -build-lean: - @echo "Building Lean 4 proofs..." - cd proofs/lean4 && lake build - # Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K) build-agda: @echo "Building Agda proofs..." 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 (CNO + OND session) -build-isabelle: - @echo "Building Isabelle/HOL proofs..." - 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..." @@ -61,24 +35,14 @@ build-idris: # Verification Commands # ============================================================================ -# Verify BOTH pillars across ALL six provers + the Idris ABI (canonical gate). -# Single source of truth; prints ALL-PROVERS-GREEN on success. +# Canonical gate: Agda + Z3 + Idris 2 ABI. Prints ACTIVE-PROVERS-GREEN on success. verify: - @proofs/verify-all-provers.sh + @proofs/verify-active-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 +# Verify all active proofs (per-prover targets; `just verify` is the canonical one-shot) +verify-all: verify-z3 verify-agda verify-idris @echo "✓ All verifications complete" -# Verify Coq proofs: build, then the Print Assumptions gate and its control -verify-coq: build-coq - 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..." @@ -86,32 +50,10 @@ verify-z3: 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" -# Verify Isabelle/HOL proofs -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" @@ -162,16 +104,16 @@ clean: clean-coq clean-lean # Clean Coq artifacts clean-coq: @echo "Cleaning Coq artifacts..." - find proofs/coq -name "*.vo" -delete - find proofs/coq -name "*.vok" -delete - find proofs/coq -name "*.vos" -delete - find proofs/coq -name "*.glob" -delete - find proofs/coq -name ".*.aux" -delete + find archive/proofs/coq -name "*.vo" -delete + find archive/proofs/coq -name "*.vok" -delete + find archive/proofs/coq -name "*.vos" -delete + find archive/proofs/coq -name "*.glob" -delete + find archive/proofs/coq -name ".*.aux" -delete # Clean Lean artifacts clean-lean: @echo "Cleaning Lean artifacts..." - cd proofs/lean4 && lake clean + cd archive/proofs/lean4 && lake clean # ============================================================================ # Development @@ -254,8 +196,8 @@ proof-status: @echo "=== Proof Completion Status ===" @echo "" @echo "Coq proofs:" - @admitted=$$(grep -r "Admitted\." proofs/coq/ 2>/dev/null | wc -l); \ - total=$$(grep -r "Theorem\|Lemma\|Corollary" proofs/coq/ 2>/dev/null | wc -l); \ + @admitted=$$(grep -r "Admitted\." archive/proofs/coq/ 2>/dev/null | wc -l); \ + total=$$(grep -r "Theorem\|Lemma\|Corollary" archive/proofs/coq/ 2>/dev/null | wc -l); \ if [ $$total -gt 0 ]; then \ complete=$$((total - admitted)); \ percent=$$((complete * 100 / total)); \ @@ -268,8 +210,8 @@ proof-status: fi @echo "" @echo "Lean 4 proofs:" - @sorry=$$(grep -r "sorry" proofs/lean4/ 2>/dev/null | wc -l); \ - total=$$(grep -r "theorem\|lemma" proofs/lean4/ 2>/dev/null | wc -l); \ + @sorry=$$(grep -r "sorry" archive/proofs/lean4/ 2>/dev/null | wc -l); \ + total=$$(grep -r "theorem\|lemma" archive/proofs/lean4/ 2>/dev/null | wc -l); \ if [ $$total -gt 0 ]; then \ complete=$$((total - sorry)); \ percent=$$((complete * 100 / total)); \ diff --git a/.machine_readable/contractiles/adjust/adjust.k9.ncl b/.machine_readable/contractiles/adjust/adjust.k9.ncl new file mode 100644 index 0000000..b38ef17 --- /dev/null +++ b/.machine_readable/contractiles/adjust/adjust.k9.ncl @@ -0,0 +1,112 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# adjust.k9.ncl — K9 contractile component: ADJUST (drift tolerance) +# Repo: absolute-zero +# +# Migrated from archive/a2ml-v1/contractiles-Adjustfile.a2ml.txt (2026-10-10, +# a2ml retirement: D99, D269c, D312, D313; envelope per MIGRATION-1058 M1 and +# the K9 contract spec v1.0.0). Cumulative-drift catchment: tolerance bands and +# corrective actions. Advisory only: it warns and trends and does not block. +# +# Leash / authority: 'Yard / advisory (continue-with-warnings). Estate template +# canon for the adjust verb. +# +# Grants: NONE. The source's `adjust fix` deterministic auto-fix would write +# files, which 'Yard does not permit. Under this grant `adjust fix` is NOT +# operative; the corrective actions below are for humans and agents. Ledger row D-1. +# +# Adaptations (ledger rows A-A1, A-A2): the Coq-sourced tolerances are marked +# archived because Coq is archived under archive/proofs/ (2026-10-10). + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "contractile:adjust", + semantics = "drift-tolerance", + + security = { + leash = 'Yard, + trust_level = "advisory (continue-with-warnings)", + signature_required = false, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + capabilities = [], + }, + + metadata = { + name = "absolute-zero-adjust", + version = "1.0.0", + description = "Drift tolerances for absolute-zero's proof-debt figures, language-policy surface, and documentation sync. Advisory only.", + author = "Jonathan D.A. Jewell ", + }, + }, + + declaration = { + abstract = "Drift tolerances for absolute-zero's proof-debt figures, language-policy surface, and documentation sync. Advisory only.", + last_updated = "2026-10-10", + + tolerances = [ + { + id = "coq-axiom-count", + description = "Coq Axiom count must not exceed the Phase-1 triage baseline", + tolerance = "<= 72 Axioms (counting method = docs/proof-debt-triage.md, PR #58, 2026-05-27)", + corrective = "Any NEW axiom requires a triage entry (TRUSTED-BASE / DISCHARGE / PROPERTY-TEST) in docs/proof-debt-triage.md before merge; trend the count DOWN by discharging the 17-item DISCHARGE backlog", + severity = "advisory", + status = "archived", + status_note = "Coq is archived under archive/proofs/coq/ (2026-10-10). Not gated; kept for reference. Note: the cited file docs/proof-debt-triage.md is .adoc in the repo (stale path in the source).", + }, + { + id = "coq-parameter-count", + description = "Coq Parameter count stays at the model-layer baseline", + tolerance = "<= 42 Parameters (baseline of 2026-05-27)", + corrective = "New Parameters need the same triage discipline as Axioms", + severity = "advisory", + status = "archived", + status_note = "Coq is archived under archive/proofs/coq/ (2026-10-10). Not gated; kept for reference.", + }, + { + id = "escape-hatch-total", + description = "Total escape hatches across all proof languages must not increase", + tolerance = "<= 124 (canonical figure per the standards#195 counting method; was 129, reduced to 124 as of the 2026-05-27 STATE entry)", + corrective = "Decrement by discharge; any increment needs a documented rationale in docs/proof-debt-triage.md", + severity = "advisory", + status = "active", + status_note = "The count baseline predates archiving; recount on the active tree plus archive/proofs/ before relying on it.", + }, + { + id = "physics-constant-duplication", + description = "Physics constants should be declared once, not per-file", + tolerance = "Known duplication: kB_positive/temperature_positive declared 3x across QuantumCNO/StatMech/LandauerDerivation (surfaced by the Phase-1 triage)", + corrective = "Deduplicate into a shared constants module (already on the STATE this-week actions; those are now archived)", + severity = "advisory", + status = "archived", + status_note = "The duplicated declarations live in archived Coq sources (archive/proofs/coq/). Not gated.", + }, + { + id = "banned-language-surface", + description = "Banned-language files stay confined to the demonstration surface", + tolerance = "Banned-language files only under examples/ or enumerated in .hypatia-ignore; zero NEW banned-language files elsewhere", + corrective = "Move demonstration files under examples/; anything load-bearing gets rewritten per the language policy (Python to Julia/Rust, etc.)", + severity = "advisory", + status = "active", + }, + { + id = "wiki-sync-drift", + description = "docs/wiki/ (canonical, in-repo) vs the GitHub Wiki copy", + tolerance = "GitHub Wiki may lag docs/wiki/ between manual syncs (sync is a manual cp + push, see docs/wiki/README.md)", + corrective = "Run the sync procedure in docs/wiki/README.md; automation (just wiki-sync + workflow) is a tracked TODO", + severity = "advisory", + status = "active", + }, + { + id = "stale-dated-docs", + description = "Dated snapshots belong in docs/archive/", + tolerance = "0 dated status/roadmap snapshots outside docs/archive/", + corrective = "Move superseded dated documents into docs/archive/ and add them to docs/archive/README.adoc", + severity = "advisory", + status = "active", + }, + ], + }, +} diff --git a/.machine_readable/contractiles/bust/bust.k9.ncl b/.machine_readable/contractiles/bust/bust.k9.ncl new file mode 100644 index 0000000..5c42ec2 --- /dev/null +++ b/.machine_readable/contractiles/bust/bust.k9.ncl @@ -0,0 +1,116 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# bust.k9.ncl — K9 contractile component: BUST (breakage and failure-recovery) +# Repo: absolute-zero +# +# Migrated from archive/a2ml-v1/contractiles-Bustfile.a2ml.txt (2026-10-10, +# a2ml retirement: D99, D269c, D312, D313; envelope per MIGRATION-1058 M1 and +# the K9 contract spec v1.0.0). Source semantics: every declared failure mode +# must have a recovery path that has been exercised. +# +# Leash / authority: 'Hunt / blocking (hard gate). Estate template canon for +# the bust verb. +# +# Runner: NOT ENABLED (runner-semantics.enabled = false in the source). The old +# runner (bust.ncl) was never present in this repo, and D187/#81 rule on whether +# it is dropped. Ledger row B-5. +# +# Signature: NONE. K9-S009 requires a signature block at 'Hunt. No signing +# ceremony has run. Not authorised to run as 'Hunt until the owner signs it +# (ledger row K-1). + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "contractile:bust", + semantics = "recovery-drill", + + security = { + leash = 'Hunt, + trust_level = "blocking (hard gate)", + signature_required = true, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = true, + capabilities = [ "process.spawn" ], + injection_scope = "system-under-test-only", + }, + + metadata = { + name = "absolute-zero-bust", + version = "1.1.0", + description = "Rollback procedures when something breaks: revert-first escalation, secret-leak response, proof-suite breakage recovery.", + author = "Jonathan D.A. Jewell ", + }, + + side_effects = [ + "drill mode would inject declared failures into the system under test; the runner is NOT enabled, so no drill runs today", + "writes nothing; no network access", + ], + }, + + declaration = { + abstract = "Rollback procedures when something breaks: revert-first escalation, secret-leak response, proof-suite breakage recovery.", + last_updated = "2026-10-10", + + runner_semantics = { + enabled = false, + verb = "bust", + gate = "hard gate on any failure mode with missing or broken recovery", + injection_scope = "system-under-test-only", + allow_network = false, + record_recovery_times = true, + }, + + scenarios = [ + { + id = "bad-merge-or-bump", + description = "A bad commit (merge, pointer/pin bump, metadata sweep) lands on main", + recovery = "git revert : reversible, low blast radius; child/upstream repos untouched", + status = "verified", + notes = "Generalised from the ported 'bad-pointer-bump' scenario; exercised routinely via PR reverts.", + }, + { + id = "secret-leaked-to-public-history", + description = "Secret or private content committed to public history", + recovery = "Hard-rotate the leaked secret IMMEDIATELY; then git-filter-repo or BFG on the affected history; public re-publication only after rotation completes", + status = "declared", + notes = "Ported in substance from the nested Bustfile, generalised from submodule to any public history. Rotation before rewrite, always.", + }, + { + id = "proof-suite-breakage", + description = "Proof suite goes red systemically (toolchain or keystone regression)", + recovery = "Revert to last CI-green; for keystone damage use the rescue-branch pattern (re-prove on a branch, land via reviewed PR)", + status = "verified", + notes = "Exercised: Tier-0 rescue 2026-05-18 (docs/archive/PROOF-STATUS-2026-05-18.md); rescue branch rebased and landed 2026-05-20 (PR #24). The active proof stack is now Agda, Z3 and Idris 2; archived provers are under archive/proofs/.", + }, + { + id = "submodule-pointer-points-at-missing-sha", + description = "Submodule pointer references a SHA missing from the child remote", + recovery = "git submodule update --init --checkout ; or revert the stale bump commit", + status = "not-applicable", + reason = "absolute-zero has no git submodules (no .gitmodules). Preserved from the ported meta-repo-flavoured Bustfile so its content is not lost.", + }, + { + id = "submodule-orphan-after-local-only-commit", + description = "Local-only submodule commit stranded after parent reset", + recovery = "git reset to before the stranded commit; fix the remote situation before re-attempting", + status = "not-applicable", + reason = "absolute-zero has no git submodules (no .gitmodules). Preserved from the ported meta-repo-flavoured Bustfile so its content is not lost.", + }, + ], + + escalation_ladder = [ + "1. revert the offending commit (reversible, low blast radius)", + "2. reset the local clone / working tree (affects only local workspace)", + "3. force-push to main: PROHIBITED without explicit user confirmation (violates branch protection)", + "4. registry-level action (delete/archive the GitHub repo): human-only, never by AI", + ], + + backup_points = [ + "GitHub (origin) serves as the durable backup for the full history", + "CI-green commits on origin/main are the durable rollback targets for the proof suite", + "Local backup tags (backup/pre--) retained on risky rewrites", + ], + }, +} diff --git a/.machine_readable/contractiles/dust/dust.k9.ncl b/.machine_readable/contractiles/dust/dust.k9.ncl new file mode 100644 index 0000000..7a79fbe --- /dev/null +++ b/.machine_readable/contractiles/dust/dust.k9.ncl @@ -0,0 +1,102 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# dust.k9.ncl — K9 contractile component: DUST (recovery and rollback semantics) +# Repo: absolute-zero +# +# Migrated from archive/a2ml-v1/contractiles-Dustfile.a2ml.txt (2026-10-10, +# a2ml retirement: D99, D269c, D312, D313; envelope per MIGRATION-1058 M1 and +# the K9 contract spec v1.0.0). Every asset that can degrade declares a +# reversible recovery path. +# +# Leash / authority: 'Yard / advisory (continue-with-warnings). Estate template +# canon for the dust verb. +# +# Grants: NONE. At 'Yard the spec permits no filesystem, network or subprocess +# access. The source's recovery handlers are text for humans and agents, not +# executed by this component. Ledger row D-1. +# +# Adaptations (ledger rows A-D1, A-D2): the proof-suite asset now names the +# active and archived proof trees; the machine-metadata asset names the deed, +# the K9 contracts and coordination.k9 in place of the retired .a2ml set. + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "contractile:dust", + semantics = "recovery-paths", + + security = { + leash = 'Yard, + trust_level = "advisory (continue-with-warnings)", + signature_required = false, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + capabilities = [], + }, + + metadata = { + name = "absolute-zero-dust", + version = "1.0.0", + description = "Reversible recovery paths for absolute-zero: git-revert-first discipline, proof-suite rescue precedent, append-only archives, and pinned-workflow rollback.", + author = "Jonathan D.A. Jewell ", + }, + }, + + declaration = { + abstract = "Reversible recovery paths for absolute-zero: git-revert-first discipline, proof-suite rescue precedent, append-only archives, and pinned-workflow rollback.", + last_updated = "2026-10-10", + + recoveries = [ + { + id = "bad-commit-on-main", + asset = "main branch history", + reversible = true, + handler = "git revert : origin/main on GitHub is the durable history; never force-push main", + notes = "First rung for any regression: revert, do not rewrite.", + }, + { + id = "proof-suite-regression", + asset = "proofs/ (agda, z3, observation-models, residue) + src/abi/; archive/proofs/ (coq, lean4, isabelle, mizar) is reference-only since 2026-10-10 (A-D1)", + reversible = true, + handler = "Revert the offending commit to the last CI-green state; for systemic breakage follow the rescue-branch pattern", + notes = "Exercised precedent: Tier-0 rescue of 2026-05-18 (ledger archived at docs/archive/PROOF-STATUS-2026-05-18.md).", + }, + { + id = "ci-workflow-regression", + asset = ".github/workflows/ (thin wrappers over hyperpolymath/standards reusables)", + reversible = true, + handler = "Revert the pin bump; workflows are SHA-pinned to the standards reusables, so rollback = restoring the previous pinned SHA", + notes = "Exercised precedent: PR #69 repinned orphan reusable SHAs (97df7621/4fdf4314 to live).", + }, + { + id = "stale-machine-metadata", + asset = "machine-readable metadata: absolute-zero_chora.deed, .machine_readable/contractiles/ K9 set, coordination.k9, .machine_readable/bot_directives/ (A-D2)", + reversible = true, + handler = "Regenerate from repo facts (git log since the last deed date + repo docs); prior states are recoverable from git history and from archive/a2ml-v1/", + notes = "Deed updates are additive; never invent facts; omit unknown keys.", + }, + { + id = "dated-doc-supersession", + asset = "docs/archive/", + reversible = true, + handler = "Append-only: supersede by adding a new dated snapshot; consult docs/archive/README.adoc for the live counterpart of each archived file", + notes = "Do not edit archived snapshots in place.", + }, + { + id = "github-wiki-divergence", + asset = "GitHub Wiki (mirror of docs/wiki/)", + reversible = true, + handler = "docs/wiki/ in-repo is canonical; re-run the sync procedure in docs/wiki/README.md to overwrite the wiki copy", + notes = "Wiki divergence is always resolvable in favour of the in-repo source.", + }, + { + id = "template-dust-handlers", + asset = "decision-log replay / policy rollback / gateway deployment undo (from the removed root template)", + reversible = false, + status = "not-applicable", + reason = "Template placeholders from contractiles/dust/Dustfile (generic gateway repo shape: logs/decisions.json, policy/policy.ncl, kubectl rollout undo). absolute-zero has no such gateway, deployment, or decision-log assets; recorded here so the removed template's content is accounted for rather than lost.", + }, + ], + }, +} diff --git a/.machine_readable/contractiles/intend/intend.k9.ncl b/.machine_readable/contractiles/intend/intend.k9.ncl new file mode 100644 index 0000000..1980760 --- /dev/null +++ b/.machine_readable/contractiles/intend/intend.k9.ncl @@ -0,0 +1,145 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# intend.k9.ncl — K9 contractile component: INTEND (north-star intents and wishes) +# Repo: absolute-zero +# +# Migrated from archive/a2ml-v1/contractiles-Intentfile.a2ml.txt (2026-10-10, +# a2ml retirement: D99, D269c, D312, D313; envelope per MIGRATION-1058 M1 and +# the K9 contract spec v1.0.0). Non-gating: this is a report, not a gate. +# +# Leash / authority: 'Hunt / reporting (log drift, never fail). The leash is the +# estate template canon for the intend verb. The source Intentfile has no +# runner and no probes, so this component requests no grants. +# +# Signature: NONE. K9-S009 requires a signature block at 'Hunt. No signing +# ceremony has run. Not authorised to run as 'Hunt until the owner signs it +# (ledger row K-1). Its authority is 'reporting, so an unsigned run can only +# log drift. +# +# Adaptations (ledger rows A-I1..A-I3): the purpose statement now names the +# ACTIVE prover set (Idris 2, Agda, Z3) after the owner's 2026-10-10 ruling. +# Intents and wishes tied to archived provers stay listed, marked parked +# (never silently dropped). + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "contractile:intend", + semantics = "north-star", + + security = { + leash = 'Hunt, + trust_level = "reporting (log drift, never fail)", + signature_required = true, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + capabilities = [], + }, + + metadata = { + name = "absolute-zero-intend", + version = "1.0.0", + description = "North star for absolute-zero: machine-checked proofs that Certified Null Operations do nothing, en route to a publication release.", + author = "Jonathan D.A. Jewell ", + }, + + side_effects = [ + "reads the repository's declarations; writes nothing; no subprocess; no network", + ], + }, + + declaration = { + abstract = "North star for absolute-zero: machine-checked proofs that Certified Null Operations (CNOs) do nothing, en route to a publication release.", + last_updated = "2026-10-10", + + purpose = { + statement = "Formal verification of Certified Null Operations (programs provably having zero net computational effect), with an Idris 2 ABI and Agda and Z3 proof surfaces, and cross-language demonstration examples. Coq, Lean 4, Isabelle/HOL and Mizar are archived under archive/proofs/ (owner ruling 2026-10-10).", + supersedes = "The six-prover statement (Coq, Lean 4, Z3, Agda, Isabelle, Mizar), adaptation A-I1.", + }, + + anti_purpose = { + not = [ + "A production runtime or deployed service (research repo; service-security checks are kept only for estate consistency)", + "A general-purpose proof framework: the subject is CNOs and their thermodynamic/categorical meaning", + "A language-advocacy showcase: banned-language files under examples/ exist to demonstrate cross-language nop semantics, not to endorse those languages", + ], + }, + + if_in_doubt = { + sensitive_areas = [ "proofs/", "src/abi/", ".github/workflows/", ".claude/CLAUDE.md", "LICENSE", "TOPOLOGY.adoc" ], + guidance = "Proof semantics and licensing are maintainer-gated; ask before touching.", + }, + + intents = [ + { + id = "phase-2-triage", + description = "Phase 2 proof-debt triage of the Idris 2 postulates (#27), following the Phase-1 triage discipline (PR #58). The Lean 52-axiom item is parked: Lean is archived (A-I2).", + status = "declared", + }, + { + id = "discharge-coq-backlog", + description = "Discharge the 17 DISCHARGE-class Coq axioms from the Phase-1 triage (lowest-hanging: cno_zero_energy_dissipation_derived, fidelity_bound, unitary_inverse_property, *_not_identity existence pair)", + status = "declared", + parked = "Coq is archived under archive/proofs/coq/ (2026-10-10). Parked, not abandoned; needs an owner ruling (Coq is also in the D204 Coq Module Type CNO interface).", + }, + { + id = "physics-constant-dedup", + description = "Deduplicate kB_positive/temperature_positive (declared 3x across QuantumCNO/StatMech/LandauerDerivation)", + status = "declared", + parked = "The duplicates are in archived Coq sources. Parked.", + }, + { + id = "migrate-python-to-rust", + description = "Migrate Python interpreters to Rust (RSR language-policy blocker recorded in STATE)", + status = "declared", + }, + { + id = "v0-8-compliance-sprint", + description = "v0.8 milestone: compliance sprint (RSR/estate alignment)", + status = "in_progress", + progress = "estate-standardization merged + governance checkpoint 2026-06-12; STATE put route-to-mvp completion at 40 as of 2026-05-27", + }, + { + id = "v0-9-container-verification", + description = "v0.9 milestone: container verification pipeline (active gate: proofs/verify-active-provers.sh; proofs.yml runs Agda, Z3 and Idris 2)", + status = "declared", + }, + { + id = "v1-0-publication-release", + description = "v1.0 milestone: publication release + paper draft. The paper's six-prover story is out of date (A-I3); the Coq, Lean 4, Isabelle and Mizar results are archived.", + status = "declared", + }, + ], + + wishes = [ + { + id = "wiki-sync-automation", + horizon = "near", + description = "Automated docs/wiki to GitHub Wiki sync (just wiki-sync recipe + push workflow), replacing the manual procedure in docs/wiki/README.md", + status = "declared", + }, + { + id = "landauer-measure-theory", + horizon = "mid", + description = "LandauerDerivation.v upgraded with real measure theory (current blocker recorded in STATE)", + status = "declared", + parked = "Coq is archived under archive/proofs/coq/ (2026-10-10). Parked.", + }, + { + id = "mizar-beyond-stub", + horizon = "far", + description = "Mizar track beyond stub (needs installation per STATE components)", + status = "declared", + parked = "Mizar is archived under archive/proofs/mizar/ (2026-10-10). Parked.", + }, + { + id = "y-not-cno-nontermination", + horizon = "far", + description = "y_not_cno non-termination proof (low-priority blocker in STATE)", + status = "declared", + parked = "The open axiom lives in the archived Coq/Lean sources. Parked.", + }, + ], + }, +} diff --git a/.machine_readable/contractiles/must/must.k9.ncl b/.machine_readable/contractiles/must/must.k9.ncl new file mode 100644 index 0000000..844f30d --- /dev/null +++ b/.machine_readable/contractiles/must/must.k9.ncl @@ -0,0 +1,154 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# must.k9.ncl — K9 contractile component: MUST (invariant assertion, release-blocking) +# Repo: absolute-zero +# +# Migrated from archive/a2ml-v1/contractiles-Mustfile.a2ml.txt (2026-10-10, +# a2ml retirement: D99, D269c, D312, D313; envelope per MIGRATION-1058 M1 and +# the K9 contract spec v1.0.0). +# +# Leash / authority: 'Hunt / blocking (hard gate). The leash is the estate +# template canon for the must verb (rsr-template-repo must.k9.ncl). The source +# Mustfile declares no leash itself. +# +# Signature: NONE. K9-S009 requires a signature block at 'Hunt. No signing +# ceremony has run, and this sandbox has no signing key. A block would be a +# claim, not a fact, so none is written. This contract is therefore NOT +# authorised to run as 'Hunt until the owner signs it. Ledger row K-1. +# +# Adaptations to source checks (ledger rows A-M1..A-M7): +# proofs-tree-present -> active proof tree + archive/proofs +# six-a2ml-present -> deed-and-coordination-present +# contractiles-flat-complete -> contractiles-k9-complete +# a2ml-parses-as-toml -> retired; replaced by no-live-a2ml +# anchor-directory -> anchor-clause-present (ANCHOR is a deed clause) +# bot-directives-present -> clause check against the deed +# ai-manifest -> manifest clause in the deed (root 0-AI-MANIFEST retired) + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "contractile:must", + semantics = "invariant", + + security = { + leash = 'Hunt, + trust_level = "blocking (hard gate)", + signature_required = true, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = true, + capabilities = [ "process.spawn" ], + }, + + metadata = { + name = "absolute-zero-must", + version = "1.0.0", + description = "Physical-state invariants for absolute-zero: required governance files, the K9 contractile set, the deed, and the absence of retired a2ml metadata.", + author = "Jonathan D.A. Jewell ", + }, + + side_effects = [ + "runs read-only shell probes (test, grep, find) from the repository root, one subprocess per invariant", + "writes nothing; no network access", + ], + }, + + declaration = { + abstract = "Physical-state invariants for absolute-zero: required governance files, the K9 contractile set, the deed, and the absence of retired a2ml metadata.", + last_updated = "2026-10-10", + + invariants = [ + { + id = "license-present", + description = "LICENSE file must exist (MPL-2.0)", + probe = "test -f LICENSE && grep -q 'Mozilla Public License' LICENSE", + severity = "critical", + }, + { + id = "readme-canonical", + description = "README.adoc (canonical) must exist; README.md is a pointer only", + probe = "test -f README.adoc", + severity = "critical", + }, + { + id = "security-policy", + description = "SECURITY.md must exist", + probe = "test -f SECURITY.md", + severity = "critical", + }, + { + id = "ai-manifest", + description = "AI manifest clause must be present in the repo deed (retired root 0-AI-MANIFEST.a2ml, adaptation A-M6)", + probe = "test -f absolute-zero_chora.deed && grep -q '(manifest' absolute-zero_chora.deed", + severity = "critical", + }, + { + id = "governance-docs", + description = "GOVERNANCE.adoc, MAINTAINERS.adoc, .github/CODEOWNERS must exist (estate wave 2026-06)", + probe = "test -f GOVERNANCE.adoc && test -f MAINTAINERS.adoc && test -f .github/CODEOWNERS", + severity = "critical", + }, + { + id = "contractiles-k9-complete", + description = "All six contractile K9 components exist at .machine_readable/contractiles//.k9.ncl (adaptation A-M3: replaces the flat .a2ml check)", + probe = "test -f .machine_readable/contractiles/must/must.k9.ncl && test -f .machine_readable/contractiles/trust/trust.k9.ncl && test -f .machine_readable/contractiles/dust/dust.k9.ncl && test -f .machine_readable/contractiles/bust/bust.k9.ncl && test -f .machine_readable/contractiles/adjust/adjust.k9.ncl && test -f .machine_readable/contractiles/intend/intend.k9.ncl", + severity = "critical", + }, + { + id = "deed-and-coordination-present", + description = "The repo deed and coordination.k9 exist (adaptation A-M2: replaces the six-a2ml check)", + probe = "test -f absolute-zero_chora.deed && grep -q '(repo-deed' absolute-zero_chora.deed && test -f coordination.k9", + severity = "critical", + }, + { + id = "anchor-clause-present", + description = "The ANCHOR realignment record is present as a deed clause (adaptation A-M4)", + probe = "grep -q '(anchor' absolute-zero_chora.deed", + severity = "warning", + }, + { + id = "bot-directives-present", + description = "bot_directives/ README exists and the deed carries the bot-directives clause (adaptation A-M5)", + probe = "test -f .machine_readable/bot_directives/README.adoc && grep -q '(bot-directives' absolute-zero_chora.deed", + severity = "warning", + }, + { + id = "self-validating-present", + description = "self-validating/ (renamed from svc/k9) exists with the k9 template set", + probe = "test -d .machine_readable/self-validating && test -f .machine_readable/self-validating/template-kennel.k9.ncl", + severity = "warning", + }, + { + id = "no-duplicate-root-scm", + description = "No duplicate root .machine_readable/*.scm set (removed by estate wave 2026-06; the deed is canonical)", + probe = "test -z \"$(ls .machine_readable/*.scm 2>/dev/null)\"", + severity = "critical", + }, + { + id = "no-live-a2ml", + description = "No live .a2ml files outside archive/ (added by the 2026-10-10 migration; replaces the a2ml-parses-as-toml check, adaptation A-M7)", + probe = "test -z \"$(find . -name '*.a2ml' -not -path './archive/*' -not -path './.git/*' 2>/dev/null | head -1)\"", + severity = "critical", + }, + { + id = "proofs-tree-present", + description = "The active proof tree exists (agda, z3, observation-models, residue) and the archived provers are under archive/proofs (adaptation A-M1)", + probe = "test -d proofs/agda && test -d proofs/z3 && test -d proofs/observation-models && test -d proofs/residue && test -d archive/proofs/coq && test -d archive/proofs/lean4 && test -d archive/proofs/isabelle && test -d archive/proofs/mizar", + severity = "critical", + }, + { + id = "root-mustfile-buildgate", + description = "Repo-root Mustfile (build-gate: just lint/test/fmt) and Justfile exist", + probe = "test -f Mustfile && test -f Justfile", + severity = "warning", + }, + { + id = "no-dockerfile", + description = "No Dockerfile (use Containerfile)", + probe = "test ! -f Dockerfile", + severity = "warning", + }, + ], + }, +} diff --git a/.machine_readable/contractiles/trust/trust.k9.ncl b/.machine_readable/contractiles/trust/trust.k9.ncl new file mode 100644 index 0000000..9ee62a4 --- /dev/null +++ b/.machine_readable/contractiles/trust/trust.k9.ncl @@ -0,0 +1,171 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# trust.k9.ncl — K9 contractile component: TRUST (trust boundaries and integrity invariants) +# Repo: absolute-zero +# +# Migrated from archive/a2ml-v1/contractiles-Trustfile.a2ml.txt (2026-10-10, +# a2ml retirement: D99, D269c, D312, D313; envelope per MIGRATION-1058 M1 and +# the K9 contract spec v1.0.0). +# +# Leash / authority: 'Hunt / blocking (hard gate). The leash is the estate +# template canon for the trust verb. The source Trustfile declares no leash. +# +# Runner: DISABLED in the source ([runner] enabled = false). It stays disabled here. +# +# Signature: NONE. K9-S009 requires a signature block at 'Hunt. No signing +# ceremony has run, and this sandbox has no signing key. This contract is NOT +# authorised to run as 'Hunt until the owner signs it. Ledger row K-1. +# +# Probes are the source `run` strings with TOML escapes decoded. No runner +# executes them yet, so they are documentation-grade until a runner is wired. +# +# Adaptations (ledger rows A-T1, A-T2): the Lean and Coq "bounded" checks point +# at archive/proofs/ because those provers are archived (2026-10-10). + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "contractile:trust", + semantics = "invariant", + + security = { + leash = 'Hunt, + trust_level = "maximal", + signature_required = true, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = true, + capabilities = [ "process.spawn" ], + }, + + metadata = { + name = "absolute-zero-trust", + version = "1.0.0", + description = "Trust boundaries for AI agents plus integrity invariants: no committed secrets, traceable provenance, and dangerous proof patterns held at the verified baselines.", + author = "Jonathan D.A. Jewell ", + }, + + side_effects = [ + "runs read-only shell probes (test, grep, find, git log) from the repository root; one subprocess per invariant", + "writes nothing; no network access", + ], + }, + + declaration = { + abstract = "Trust boundaries for AI agents plus integrity invariants: no committed secrets, traceable provenance, and dangerous proof patterns held at the verified baselines.", + last_updated = "2026-10-10", + + runner = { + enabled = false, + command = "just trust-check", + on_push = false, + on_pr = false, + note = "Scaffold only. Do not activate until the maintainer has reviewed.", + }, + + trust = { + level = "maximal", + definition = "Agents may read, build, test, lint and format freely. Destructive or external actions, and edits to the protected paths below, require maintainer approval.", + protected_paths = [ + ".claude/CLAUDE.md", + ".github/workflows/", + "proofs/", + "src/abi/", + "LICENSE", + "TOPOLOGY.adoc", + "coordination.k9", + ], + }, + + invariants = [ + { + id = "no-secrets-committed", + section = "secrets", + description = "No credential files in repo", + probe = "test ! -f .env && test ! -f credentials.json && test ! -f .env.local && test ! -f .env.production", + severity = "critical", + }, + { + id = "no-private-keys", + section = "secrets", + description = "No private key files committed", + probe = "! find . -name '*.pem' -o -name '*.key' -o -name 'id_rsa' -o -name 'id_ed25519' 2>/dev/null | grep -v node_modules | head -1 | grep -q .", + severity = "critical", + }, + { + id = "no-tokens-in-source", + section = "secrets", + description = "No hardcoded API tokens in source files", + probe = "! grep -rE '(api[_-]?key|secret|token|password)[[:space:]]*[:=][[:space:]]*[\\\"'\\\\''][A-Za-z0-9]{16,}' --include='*.js' --include='*.res' --include='*.py' --include='*.rs' . 2>/dev/null | grep -v node_modules | head -1 | grep -q .", + severity = "critical", + }, + { + id = "author-correct", + section = "provenance", + description = "Git author matches expected identity", + probe = "git log -1 --format='%ae' | grep -qE '(hyperpolymath|j\\\\.d\\\\.a\\\\.jewell)'", + severity = "warning", + }, + { + id = "license-content", + section = "provenance", + description = "LICENSE contains the MPL identifier (repo policy: MPL-2.0 only, PMPL banned)", + probe = "grep -q 'Mozilla Public License' LICENSE", + severity = "warning", + }, + { + id = "container-images-pinned", + section = "container-security", + description = "Containerfile uses pinned/Chainguard base images", + probe = "test ! -f Containerfile || grep -q 'cgr.dev\\\\|@sha256:' Containerfile", + severity = "warning", + }, + { + id = "no-dockerfile", + section = "container-security", + description = "No Dockerfile (use Containerfile)", + probe = "test ! -f Dockerfile", + severity = "warning", + }, + { + id = "no-dangerous-proof-patterns", + section = "dangerous-patterns", + description = "No believe_me, assert_total, unsafeCoerce, Obj.magic in non-proof source", + probe = "! grep -rE 'believe_me|assert_total|unsafeCoerce|Obj\\\\.magic' --include='*.idr' --include='*.ml' --include='*.hs' --include='*.rs' . 2>/dev/null | head -1 | grep -q .", + severity = "critical", + }, + { + id = "lean4-sorry-bounded", + section = "dangerous-patterns", + description = "Lean 4 sorry count does not exceed baseline (0). Archived prover; path adapted to archive/proofs/lean4/ (A-T1)", + probe = "count=$(grep -rn 'sorry' archive/proofs/lean4/ 2>/dev/null | grep -v '^[[:space:]]*--' | wc -l); test \"$count\" -le 0", + severity = "high", + baseline = 0, + baseline_note = "Refreshed 2026-06-12 from a verified grep (0 hits). Lean is archived under archive/proofs/lean4/ as of 2026-10-10; the check is retained for reference.", + }, + { + id = "coq-admitted-bounded", + section = "dangerous-patterns", + description = "Coq Admitted count does not exceed baseline (0). Archived prover; path adapted to archive/proofs/coq/ (A-T2)", + probe = "count=$(grep -rn 'Admitted' archive/proofs/coq/ 2>/dev/null | wc -l); test \"$count\" -le 0", + severity = "high", + baseline = 0, + baseline_note = "Refreshed 2026-06-12 from a verified grep (0 hits). Coq is archived under archive/proofs/coq/ as of 2026-10-10; the check is retained for reference.", + }, + { + id = "no-unsafe-rust-without-comment", + section = "dangerous-patterns", + description = "All unsafe blocks in Rust must have SAFETY comments", + probe = "! grep -B1 'unsafe {' --include='*.rs' -r . 2>/dev/null | grep -v SAFETY | grep 'unsafe {' | head -1 | grep -q .", + severity = "warning", + }, + { + id = "localhost-only-bindings", + section = "service-security", + description = "No wildcard service bindings in source (n/a: research repo; kept for estate consistency)", + probe = "! grep -rE 'bind\\\\(\\\"0\\\\.0\\\\.0\\\\.0' --include='*.rs' --include='*.ex' --include='*.res' . 2>/dev/null | head -1 | grep -q .", + severity = "critical", + }, + ], + }, +} diff --git a/.machine_readable/descriptiles/README.adoc b/.machine_readable/descriptiles/README.adoc index 97414db..c9f2f50 100644 --- a/.machine_readable/descriptiles/README.adoc +++ b/.machine_readable/descriptiles/README.adoc @@ -2,6 +2,9 @@ // Copyright (c) Jonathan D.A. Jewell # A2ML descriptiles Directory +NOTE: Retired 2026-10-10. The A2ML files described below are archived under `archive/a2ml-v1/` (see `archive/a2ml-v1/MIGRATION-LEDGER.adoc`). Repository metadata now lives in `absolute-zero_chora.deed`, and contracts live in `.machine_readable/contractiles//.k9.ncl`. The text below describes the retired set and is kept as history until it is rewritten. + + This directory contains the 6 core A2ML machine-readable metadata files for this repository. ## Files diff --git a/.machine_readable/descriptiles/anchor/README.adoc b/.machine_readable/descriptiles/anchor/README.adoc index 13cae63..b693de5 100644 --- a/.machine_readable/descriptiles/anchor/README.adoc +++ b/.machine_readable/descriptiles/anchor/README.adoc @@ -2,6 +2,9 @@ // Copyright (c) Jonathan D.A. Jewell # A2ML Anchor Directory +NOTE: Retired 2026-10-10. The A2ML files described below are archived under `archive/a2ml-v1/` (see `archive/a2ml-v1/MIGRATION-LEDGER.adoc`). Repository metadata now lives in `absolute-zero_chora.deed`, and contracts live in `.machine_readable/contractiles//.k9.ncl`. The text below describes the retired set and is kept as history until it is rewritten. + + This directory contains ANCHOR.a2ml files for project recalibration and scope intervention. ## Files diff --git a/Containerfile b/Containerfile index a88af86..c651e0a 100644 --- a/Containerfile +++ b/Containerfile @@ -122,9 +122,6 @@ COPY . . # Build TypeScript RUN npm run build || echo "TypeScript build not configured" -# Build Coq proofs -RUN cd proofs/coq/common && coqc CNO.v -RUN cd proofs/coq/malbolge && coqc -R ../common CNO MalbolgeCore.v # Make scripts executable RUN chmod +x proofs/z3/verify.sh @@ -215,7 +212,7 @@ CMD ["just", "verify-all"] # podman run --rm -it absolute-zero /bin/bash # # Run specific verification: -# podman run --rm absolute-zero just verify-coq +# podman run --rm absolute-zero just verify-agda # podman run --rm absolute-zero just verify-z3 # # Run interpreter tests: diff --git a/Justfile b/Justfile index 83d8504..3d86215 100644 --- a/Justfile +++ b/Justfile @@ -13,45 +13,19 @@ default: # ============================================================================ # Build Commands # ============================================================================ +# Active proof stack (owner ruling 2026-10-10): Idris 2 (ABI) and Agda (CNO + +# OND), plus Z3 bounded checks. Coq, Lean 4, Isabelle/HOL and Mizar are archived +# under archive/proofs/ and are not built or gated here. -# Build everything (all six prover backends + the Idris ABI) -build-all: build-coq build-lean build-agda build-isabelle build-mizar build-idris +# Build the active provers and the Idris ABI +build-all: build-agda build-idris @echo "✓ All builds complete" -# Build Coq proofs — all 14 theories (CNO + OND pillars) via coq_makefile -build-coq: - @echo "Building Coq proofs (14 theories, both pillars)..." - @if command -v coqc >/dev/null 2>&1; then \ - 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 (CNO libs + OND; needs Mathlib cache) -build-lean: - @echo "Building Lean 4 proofs..." - cd proofs/lean4 && lake build - # Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K) build-agda: @echo "Building Agda proofs..." 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 (CNO + OND session) -build-isabelle: - @echo "Building Isabelle/HOL proofs..." - 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..." @@ -61,24 +35,14 @@ build-idris: # Verification Commands # ============================================================================ -# Verify BOTH pillars across ALL six provers + the Idris ABI (canonical gate). -# Single source of truth; prints ALL-PROVERS-GREEN on success. +# Canonical gate: Agda + Z3 + Idris 2 ABI. Prints ACTIVE-PROVERS-GREEN on success. verify: - @proofs/verify-all-provers.sh + @proofs/verify-active-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 +# Verify all active proofs (per-prover targets; `just verify` is the canonical one-shot) +verify-all: verify-z3 verify-agda verify-idris @echo "✓ All verifications complete" -# Verify Coq proofs: build, then the Print Assumptions gate and its control -verify-coq: build-coq - 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..." @@ -86,32 +50,10 @@ verify-z3: 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" -# Verify Isabelle/HOL proofs -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" @@ -162,16 +104,16 @@ clean: clean-coq clean-lean # Clean Coq artifacts clean-coq: @echo "Cleaning Coq artifacts..." - find proofs/coq -name "*.vo" -delete - find proofs/coq -name "*.vok" -delete - find proofs/coq -name "*.vos" -delete - find proofs/coq -name "*.glob" -delete - find proofs/coq -name ".*.aux" -delete + find archive/proofs/coq -name "*.vo" -delete + find archive/proofs/coq -name "*.vok" -delete + find archive/proofs/coq -name "*.vos" -delete + find archive/proofs/coq -name "*.glob" -delete + find archive/proofs/coq -name ".*.aux" -delete # Clean Lean artifacts clean-lean: @echo "Cleaning Lean artifacts..." - cd proofs/lean4 && lake clean + cd archive/proofs/lean4 && lake clean # ============================================================================ # Development @@ -254,8 +196,8 @@ proof-status: @echo "=== Proof Completion Status ===" @echo "" @echo "Coq proofs:" - @admitted=$$(grep -r "Admitted\." proofs/coq/ 2>/dev/null | wc -l); \ - total=$$(grep -r "Theorem\|Lemma\|Corollary" proofs/coq/ 2>/dev/null | wc -l); \ + @admitted=$$(grep -r "Admitted\." archive/proofs/coq/ 2>/dev/null | wc -l); \ + total=$$(grep -r "Theorem\|Lemma\|Corollary" archive/proofs/coq/ 2>/dev/null | wc -l); \ if [ $$total -gt 0 ]; then \ complete=$$((total - admitted)); \ percent=$$((complete * 100 / total)); \ @@ -268,8 +210,8 @@ proof-status: fi @echo "" @echo "Lean 4 proofs:" - @sorry=$$(grep -r "sorry" proofs/lean4/ 2>/dev/null | wc -l); \ - total=$$(grep -r "theorem\|lemma" proofs/lean4/ 2>/dev/null | wc -l); \ + @sorry=$$(grep -r "sorry" archive/proofs/lean4/ 2>/dev/null | wc -l); \ + total=$$(grep -r "theorem\|lemma" archive/proofs/lean4/ 2>/dev/null | wc -l); \ if [ $$total -gt 0 ]; then \ complete=$$((total - sorry)); \ percent=$$((complete * 100 / total)); \ diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 01269af..12fee53 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -26,6 +26,11 @@ longer say no, turns it red. `proofs/tests/gate-selftest.sh` proves both gates t each absent or failing prover, for each verdict mutant and for both audit mutants (16 cases, run in CI). ==== +[IMPORTANT] +==== +*Archive notice (2026-10-10).* The active proof stack is now Idris 2 (ABI) and Agda (CNO, OND, EchoBridge), with Z3 as a bounded-check solver. Coq, Lean 4, Isabelle/HOL and Mizar are archived under `archive/proofs/` (see `archive/README.adoc`). Text that describes those provers as active is historical until the full rewrite lands. +==== + == Coq — VERIFIED (this environment) * `coqc` **8.18.0**; clean build from scratch (all `.vo`/`.glob` deleted first), diff --git a/README.adoc b/README.adoc index 01e3765..a0eda8e 100644 --- a/README.adoc +++ b/README.adoc @@ -8,6 +8,12 @@ Multi-prover formal verification of programs that provably compute nothing (CNO) and programs that provably reveal nothing (OND). Two co-equal pillars: Certified Null Effect and Certified Null Disclosure. +[IMPORTANT] +==== +*Archive notice (2026-10-10).* The active proof stack is now Idris 2 (ABI) and Agda (CNO, OND, EchoBridge), with Z3 as a bounded-check solver. Coq, Lean 4, Isabelle/HOL and Mizar are archived under `archive/proofs/` (see `archive/README.adoc`). Text that describes those provers as active is historical until the full rewrite lands. +==== + + == Overview Absolute Zero formalises two kinds of computational nothingness: diff --git a/absolute-zero_chora.deed b/absolute-zero_chora.deed new file mode 100644 index 0000000..5c49770 --- /dev/null +++ b/absolute-zero_chora.deed @@ -0,0 +1,249 @@ +;; SPDX-License-Identifier: MPL-2.0 +; +; The repo deed of absolute-zero: the one machine-readable description of this +; repository (standards#837 one-deed-per-repo doctrine; owner ruling 2026-09-19, +; Option A). It replaces the twenty .a2ml descriptiles/contractiles/bot_directives +; files, which are archived verbatim under archive/a2ml-v1/*.a2ml.txt (D99, +; D269c, D312, D313, D222). Contracts live in .machine_readable/contractiles/ +; /.k9.ncl; agent coordination lives in coordination.k9. +; +; Migration ledger, fail-closed items and per-field provenance: +; archive/a2ml-v1/MIGRATION-LEDGER.adoc +; Mapping specs followed: 1-formats/deed/mappings/{meta-ecosystem-to-repo-deed, +; agentic-neurosym-playbook-to-repo-deed, state-v1-decision (option B), +; ai-manifest-decision (option A)}.adoc +; +; Items that did NOT translate (no table row, or no source) are kept as comments +; in the clause they belonged to, and each one has a ledger row. Nothing was +; invented to fill a field: identity, clade, forges, lineage and status have no +; CLADE source in this repo and are NOT emitted (owner input required). +(repo-deed + :schema-version "1.0.0" + :canonical-name "absolute-zero" + :beholding-chora #u5"estate/chora" + :repo-uuid #u5"github.com/hyperpolymath/absolute-zero" + + ; The canon pin: which release of hyperpolymath/standards canon.lock this repo + ; implements. Exactly one pin (deed_canon refuses zero or two). Values copied + ; from standards canon.lock [canon] and [canon.artifacts] (version 2.1.2). + ; :lockstep-since is not emitted: it is a per-repo adoption date that the + ; source does not carry (ledger row C-1). + (canon + :version "2.1.2" + :criteria-sha256 "6a5aa8857bd0d0d58ef48827938ca17c251b6b854dacf59d306388d61694d82a" + :gates-sha256 "e70efd2f53c9445e30da4baf770366f04a4a84ffd844a01426e587e565b53e6a" + :order "spine-adopts-then-canon-releases") + + ; ---- META.a2ml (family 2) ------------------------------------------------ + ; ADR-001..ADR-014 (META [architecture-decisions]). Not emitted as clauses: the + ; ADR entries carry no :date, which the family-2 table requires (ledger M-2). + ; Text kept verbatim here so nothing is lost: + ; ADR-001 accepted: ProofIrrelevance for morphism equality in category theory + ; ADR-002 accepted: Dual Landauer formalization: axiom (StatMech.v) + derivation (LandauerDerivation.v) + ; ADR-003 accepted: Lambda CNO = identity property only, not termination + ; ADR-004 accepted: post_execution_dist specialized for CNOs (identity on distributions) + ; ADR-005 accepted: Fix QuantumCNO.v Cexp: concretised as e^(i Re z) = (cos(Re z), sin(Re z)); removed the false Cconj_Cexp axiom (PR #100) + ; ADR-006 accepted: state_eq excludes state_pc: PC is control-flow bookkeeping, not observable side effect (2026-05-18 rescue) + ; ADR-007 accepted: Discharge eval_deterministic Axiom to Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win + ; ADR-008 accepted: Delete unsound eval_respects_state_eq axioms; weaken logically_reversible to use =st= (observational reversibility); re-prove cno_eval_on_equal_states and cno_logically_reversible + ; ADR-009 accepted: Delete unsound alignmentMatchesPlatformWord Idris2 postulate; consolidate alignedSizeCorrect into shared AbsoluteZero.ABI.Proofs.DivMod module (PR #40, Refs #27) + ; ADR-010 accepted: Phase 1 per-axiom triage of 72 Coq Axioms per standards#203 (2026-05-27, PR #58): 52 TRUSTED-BASE + 17 DISCHARGE backlog + 3 PROPERTY-TEST + ; ADR-011 accepted: OND (disclosure) pillar model (PR #100): operation = (state effect, timing cost); observable execution = (declared output channel, timing); observer does NOT see raw secret input + ; ADR-012 accepted: OND-1..5 proved zero-axiom in Coq/Lean/Agda (+Z3 bounded); OND-3 independence anchored to the real core is_CNO; OND-6 left OPEN as a research capstone (PR #100) + ; ADR-013 accepted: Remove three latent-UNSOUND axioms found during discharge (PR #100): no_cloning, Cconj_Cexp, eta_equivalence + ; ADR-014 accepted: Accept a small, openly-labelled class-A axiom remainder (y_not_cno, CNOT_gate_unitary, unitary_inverse_property, fidelity_bound) + ; [development-practices] code-style, testing, versioning, documentation, branching + ; and [security], [proof-methodology], [design-rationale], [project-info] type/ + ; languages/container-runtime/ci-platform/package-manager: no table row (ledger M-3..M-6). + (meta + :version "1.0.1" + :last-updated "2026-07-07" + :license MPL-2.0 + :author "Jonathan D.A. Jewell (hyperpolymath)" + :build-tool just + :scoping-first #t + :execution-order "axis-1 > axis-2 > axis-3" + :axis-1 "must > intend > like" + :axis-2 "corrective > adaptive > perfective" + :axis-3 "systems > compliance > effects") + + ; STATE v1 option B (state-v1-decision §2): phase is a lifecycle claim owned by + ; the CLADE status clause, which this repo has no source for, so phase is not + ; emitted (ledger S-1). Maturity is its own clause, ruled 2026-10-02. The + ; STATE journal (route-to-mvp, blockers, next actions, session history, + ; components percentages) is archived, not translated (ledger S-2..S-4). + (maturity :level experimental) + + ; ECOSYSTEM.a2ml (family 2). [project], [position-in-ecosystem], + ; [what-this-is], [what-this-is-not] have no table row (ledger E-1..E-3). + ; [related-projects] relationships are outside the closed set (ledger E-4) and + ; are carried in coordination.k9 under its ecosystem section, verbatim. + (ecosystem + :project "absolute-zero" + :ecosystem "hyperpolymath") + + ; ---- AGENTIC.a2ml (family 4) ------------------------------------------- + ; [agent-constraints] and [automation-hooks] are comment-carried in the source. + ; Decision D4-1: they are template canon, so the deed carries the methodology + ; pointer only. Divergence from canon was NOT diffed (no canon block to hash + ; against here), so the text is kept below as comments (ledger A-1). + ; agent-constraints: never use believe_me, assert_total, Admitted, sorry, unsafeCoerce, Obj.magic; + ; never introduce a new axiom or postulate to close a goal (report instead); + ; never commit secrets; never use banned languages (TypeScript, Python except SaltStack, + ; Go, Node.js, Bun, npm); never place checkpoint files outside .machine_readable/; + ; never relicense a file or run an automated licence sweep (LICENCE-POLICY A2); + ; never assume a licence (LICENCE-POLICY rules 1-5). + ; automation-hooks: on-enter read 0-AI-MANIFEST and STATE; on-exit update STATE with session outcomes; + ; on-commit run just validate-rsr if available. + ; [proof-safety] counts (lean4-sorry-count, coq-admitted-count) are derivable + ; facts and are dropped by the derivable-facts doctrine (ledger A-2). [tools] + ; has no table row (ledger A-3). + (agentic + :version "1.0.1" + :last-updated "2026-07-07" + (permissions :source #t :tests #t :docs #t :config #t :create-files #t) + (integrity + :fail-closed #t + :require-evidence-per-step #t + :allow-silent-skip #f + :require-rerun-after-fix #t + :release-claim-requires-hard-pass #t)) + + ; ---- NEUROSYM.a2ml (family 4) ------------------------------------------ + ; report-format "a2ml" is STALE: Hypatia's Logtalk output was removed on + ; 2026-04-12 and its output was JSON then A2ML, which is retired by D312. Kept + ; verbatim as a string, flagged in the ledger (N-1). [symbolic-layer], + ; [neural-layer], [integration] have no table row (ledger N-2..N-4); + ; [symbolic-rules] is commented out in the source and is not emitted. + (neurosym + :version "1.0.1" + :last-updated "2026-07-07" + (hypatia + :scan-enabled #t + :scan-depth deep + :report-format "a2ml")) + + ; ---- PLAYBOOK.a2ml (family 4) ------------------------------------------ + ; The five operational sections are POPULATED in this repo, not empty. The + ; family-4 rule is that populated sections fail closed for table extension, so + ; their text is kept as comments below (ledger P-1..P-4). + ; [deployment]: method "library", target "library" (research repo, no deployed service). + ; [build-procedures]: build "just build", test "just test", release "just release". + ; [proof-procedures]: verify-all "proofs/verify-all-provers.sh" (now archived; the active gate is + ; proofs/verify-active-provers.sh, see Justfile `just verify`), per-prover build recipes. + ; [incident-response]: check STATE, review git log, run just validate, run just security, + ; check proofs// for Admitted/sorry. + ; [release-process]: update version in STATE and META, resolve Admitted/sorry, run just build-all, + ; tag and push to GitHub, update PROOF-COMPLETION-PLAN. + ; [rollback]: revert the commit and re-check proof counts. [maintenance-operations]: TODO recipes. + ; [contacts]: none (TODO if paper co-authors join). + (playbook + :version "1.0.1" + :last-updated "2026-07-07") + + ; ---- 0-AI-MANIFEST.a2ml (root) — ai-manifest-decision option A ---------- + ; The root manifest's keys are [metadata] manifest-version, [scope] purpose, + ; [entry-points], [machine-readable], [language-policy], [echidna-protocol], + ; [delivery]. None of these is in the family table (which is [metadata] + ; version/last-updated, [project] name/purpose, [ai-allocation], [policy], + ; [work-allocation]), so they fail closed (ledger G-1..G-3). Only the + ; last-updated date is emitted. + ; Language policy (verbatim, for reference): allowed AffineScript, Deno, Rust, + ; Tauri, Dioxus, Gleam, Bash, JavaScript (limited), Nickel, Guile Scheme, Julia, + ; OCaml, Ada, Idris2. Banned: TypeScript, Node.js, npm, Bun, pnpm, yarn, Go, + ; Python, Java, Kotlin, Swift, React Native, Flutter, Dart, Ruby, Perl. + ; The root manifest's [delivery] rule "architectural changes recorded in + ; META.scm architecture-decisions" points at a retired file: superseded by the + ; ADR comments above (ledger G-4). + (manifest + :last-updated "2026-05-25") + + ; ---- anchor/ANCHOR.a2ml (realignment record; template anchor precedent) -- + (anchor + :repo "absolute-zero" + :owner "hyperpolymath" + :id "org.hyperpolymath.absolute-zero" + :created "2026-06-12" + :last-updated "2026-06-12" + (realignment + :date "2026-06-12" + :title "Estate standardization + governance checkpoint" + :what-changed ( + "Merged origin/estate-standardization-20260607: flat .machine_readable/contractiles/ layout, svc/k9 to self-validating/ rename, GOVERNANCE.adoc + MAINTAINERS.adoc + .github/CODEOWNERS, Guix manifest.scm, descriptiles 0-AI-MANIFEST.a2ml + README.adoc + anchor/, removal of the duplicate root .machine_readable/*.scm set and the root contractiles/ template dir, SPDX header normalization" + "Conflict resolution: .github/workflows/rust-ci.yml kept at origin/main's version; .claude/CLAUDE.md kept identical to origin/main" + "Governance checkpoint layer: bot_directives/ (README.adoc, hypatia, gitbot-fleet, git-private-farm); flat contractiles fully populated with repo-true content; descriptiles/STATE light-bump to 2026-06-12 with [recent-work]; README.md pointer-ized to canonical README.adoc; docs/archive/ index README; wiki Home.md currency fixes") + :why "Per-repo governance refresh aligning absolute-zero with the estate standard fully landed in echo-types (PR #185 there); checkpoint of 2026-06-12" + :evidence ( + "Merge of origin/estate-standardization-20260607 on branch claude/confident-shannon-xf0Td" + "Upstream PRs since 2026-05-27: #68 (scorecard job-level permissions), #69 (reusable SHA repins), #71 (CodeQL cron monthly), #72 (actions bumps)" + "Proof-track anchor unchanged: Phase-1 axiom triage PR #58 (2026-05-27), docs/proof-debt-triage.md"))) + + ; ---- bot_directives/ (named clause; template bot-directives precedent) -- + ; hypatia.a2ml -> (scanner ...) and (accepted-finding ...) + ; gitbot-fleet.a2ml -> (fleet ...), (branch-policy ...), (per-bot ...) + ; git-private-farm.a2ml -> (propagation ...), (never-propagate ...), (on-token-rotation ...) + ; The git-private-farm propagation surface is DISABLED (no instant-sync workflow; + ; propagation.enabled = #f). The secret NAME is recorded; the secret VALUE is never + ; in the repo. + (bot-directives + (scanner + :ignore-file ".hypatia-ignore" + :ignore-file-present #t + :workflow ".github/workflows/hypatia-scan.yml") + (accepted-finding + :id "banned-language-example-files" + :finding "cicd_rules/banned_language_file hits under examples/ (go, java, kotlin, swift, ...) and legacy AffineScript paths" + :reason "absolute-zero is the canonical cross-language nop-semantics demonstration repo; example files in banned languages are the point, not load-bearing code. Each accepted path is enumerated in .hypatia-ignore. After standards#180 (file_pattern glob support) the per-file entries collapse to a single examples/** pattern." + :status accepted) + (accepted-finding + :id "reusable-caller-timeout-minutes" + :finding "timeout-minutes flagged on jobs that call estate reusable workflows" + :reason "hypatia-scan.yml, mirror.yml and scorecard.yml call hyperpolymath/standards reusable workflows; timeout-minutes is set at the caller job level (10 minutes), which the scanner does not always attribute to the reusable's jobs. False positive." + :status accepted) + (accepted-finding + :id "scorecard-token-permissions" + :finding "token-permissions advisories on .github/workflows/scorecard.yml" + :reason "Deliberate: top-level permissions read-all with job-level security-events write and id-token write added in PR #68 for the reusable scorecard workflow. This is the intended least-privilege split." + :status accepted) + (accepted-finding + :id "stale-hypatia-ignore-affinescript-entries" + :finding ".hypatia-ignore lists AffineScript paths (src/AuditTrail.res, interpreters/affinescript/malbolgeInterpreter.res, examples/SafeDOMExample.res) that no longer exist in the tree" + :reason "Harmless staleness: ignore entries for deleted files have no effect. Cleanup is proposed as a maintainer issue rather than bot-edited, since .hypatia-ignore is security policy." + :status accepted-pending-cleanup) + (fleet + :bots ("rhodibot" "echidnabot" "sustainabot" "glambot" "seambot" "finishbot") + :roles ("rhodibot: git operations" "echidnabot: code quality" "sustainabot: dependency updates" "glambot: documentation" "seambot: integration" "finishbot: task completion")) + (branch-policy + :working-branch-pattern "bot//" + :draft-prs-only #t + :ci-green-before-merge #t + :never-touch (".claude/CLAUDE.md" "proofs/" "src/abi/" ".github/workflows/" "LICENSE")) + (per-bot + (echidnabot + :deny ("proofs/" "src/abi/") + :note "Quality findings on proof code go to an issue, never an automated edit; proof-debt disposition is canonical in docs/proof-debt-triage.md.") + (sustainabot + :allow ("Cargo.toml" "Cargo.lock" "deno.json" "elm.json") + :deny (".github/workflows/") + :note "Workflow action pins are repinned by maintainer-reviewed PRs (cf. PR #69); dependency bumps for the actions group arrive via the existing dependabot grouping (cf. PR #72).") + (glambot + :allow ("docs/" "docs/wiki/" "README.adoc") + :deny ("docs/archive/") + :note "docs/archive/ is append-only historical snapshots (see docs/archive/README.adoc); do not refresh archived files.")) + (propagation + :enabled #f + :workflow-present #f + :target "hyperpolymath/.git-private-farm" + :event-type "propagate" + :secret-name "FARM_DISPATCH_TOKEN" + :presence-gated #f) + (never-propagate :items ("secrets" "unmerged branches" "work-in-progress")) + (on-token-rotation + :secret-name "FARM_DISPATCH_TOKEN" + :note "Name only; paste the new value interactively, never commit it.")) + + ; ---- .machine_readable/ scope-check ------------------------------------ + ; Contracts: .machine_readable/contractiles/{must,trust,dust,bust,adjust,intend}/.k9.ncl + ; Agent coordination: coordination.k9 (repo root) + ; Archived source: archive/a2ml-v1/ +) diff --git a/archive/README.adoc b/archive/README.adoc new file mode 100644 index 0000000..032877f --- /dev/null +++ b/archive/README.adoc @@ -0,0 +1,74 @@ +// SPDX-License-Identifier: MPL-2.0 += Archive +:toc: + +This directory holds material that has been retired from the live tree but +kept for reference. Nothing here is gated by CI, and nothing here is deleted. + +== proofs/ — retired provers (2026-10-10) + +Owner ruling, 2026-10-10: the *active* proof stack is **Idris 2** (the ABI +package) and **Agda** (CNO, OND and EchoBridge). The following provers were +moved here with `git mv`, so their history is preserved: + +[cols="2,3,3",options="header"] +|=== +| Archived path | What it was | Status +| `archive/proofs/coq/` | Coq theories: CNO and OND pillars, 14 theories, `coq_makefile` build, Print Assumptions and axiom-tag gates | Not built or gated. Kept for reference. +| `archive/proofs/lean4/` | Lean 4 CNO and OND libraries, `lake` build, `check-core.sh` axiom audit | Not built or gated. +| `archive/proofs/isabelle/` | Isabelle/HOL session `AbsoluteZero-CNO` and `OND.thy` | Not built or gated. +| `archive/proofs/mizar/` | Mizar CNO article and `dict/cno.voc` | Not built or gated. +| `archive/proofs/verify-all-provers.six-prover.sh` | The six-prover gate (Coq, Agda, Lean, Z3, Isabelle, Mizar, Idris 2) | Superseded by `proofs/verify-active-provers.sh`. +| `archive/proofs/tests/gate-selftest.six-prover.sh` | Self-test for the six-prover gate (stubbed toolchains, z3 mutants) | Superseded. Kept for reference only. +|=== + +=== Why + +* Owner ruling, 2026-10-10: use Idris 2 and Agda as the active proof stack, and + file the other provers in this archive. The owner's rationale is not restated + here; add it if it should be on record. +* Archiving is reversible. A prover returns to the active tree by moving its + directory back and restoring its gate. + +=== What was NOT archived + +* `proofs/agda/` (active; CNO, OND, EchoBridge) +* `proofs/z3/` (active as a *solver* of bounded, expect-annotated checks, not as a + proof assistant; see the flag below) +* `proofs/observation-models/` and `proofs/residue/` (not prover trees) +* `src/abi/` and `absolute-zero-abi.ipkg` (Idris 2 ABI) + +== Flags for the owner (open) + +. *Coq and D204.* D204 (2026-09-30) defines the CNO interface as a Coq Module + Type that `valence-shell` imports. Archiving Coq conflicts with that decision. + The ruling needed is whether the Module Type moves to Agda, or whether Coq is + restored for that interface alone. +. *Agda and LANGUAGE-POLICY.* `CLAUDE.md` allows Agda. The language policy names + Idris 2 as the sole formal-verification option. The active stack uses both, so + the policy needs a standards ruling. +. *Z3.* Kept active as a solver of bounded checks, not as a proof assistant. Flagged + so the choice is visible. +. *TIERS.* TIERS names Coq and Isabelle at the Rhodium tier. Neither is in the + allowed-provers table. Unresolved. + +== Live references + +The archived provers still appear in the narrative documents (README, +PROOF-STATUS, docs/*, the wiki). Those documents get an archive banner now +and a full rewrite later as a separate follow-up. The machine-readable +references (Justfile, `proofs.yml`, Containerfile, `.gitlab-ci.yml`, the K9 +contracts) were updated in the same change. + +== proofs-archive history + +Before the 2026-10-10 change, `proofs.yml` ran separate coq, lean4, agda and z3 +jobs. The six-prover gate history is in git for `proofs/verify-all-provers.sh`. + +== a2ml-v1/ — retired metadata (2026-10-10) + +`archive/a2ml-v1/` holds the twenty `.a2ml` files that were the repo's +machine-readable metadata before the migration to the repo deed and the K9 +contracts. Each was moved with `git mv` and renamed to `-.a2ml.txt`. +See `archive/a2ml-v1/MIGRATION-LEDGER.adoc` for where every field went and +what did not translate. diff --git a/archive/a2ml-v1/MIGRATION-LEDGER.adoc b/archive/a2ml-v1/MIGRATION-LEDGER.adoc new file mode 100644 index 0000000..79d47bd --- /dev/null +++ b/archive/a2ml-v1/MIGRATION-LEDGER.adoc @@ -0,0 +1,190 @@ +// SPDX-License-Identifier: MPL-2.0 += Migration ledger: a2ml v1 to deed + K9 (absolute-zero, 2026-10-10) +:toc: + +Every field that moved, did not move, or was adapted in the 2026-10-10 migration. +Row IDs match the comments in `absolute-zero_chora.deed`, the K9 contracts and +`coordination.k9`. + +Rules followed: D99, D269c, D312, D313 (a2ml retired); D222 (the 27-file +precedent); standards `1-formats/deed/mappings/*` (proposals, binding for this +work); `1-formats/k9/spec/K9-CONTRACT-SPEC.adoc`; MIGRATION-1058 M1; the +coordination grammar in `2-protocols/k9-coordination`. + +== Archive map + +The twenty `.a2ml` files were moved with `git mv` into this directory, so the +history is kept. None remain in the live tree. + +[cols="3,3",options="header"] +|=== +| Source (before) | Archived as +| `.machine_readable/descriptiles/STATE.a2ml` | `descriptiles-STATE.a2ml.txt` +| `.machine_readable/descriptiles/META.a2ml` | `descriptiles-META.a2ml.txt` +| `.machine_readable/descriptiles/ECOSYSTEM.a2ml` | `descriptiles-ECOSYSTEM.a2ml.txt` +| `.machine_readable/descriptiles/AGENTIC.a2ml` | `descriptiles-AGENTIC.a2ml.txt` +| `.machine_readable/descriptiles/NEUROSYM.a2ml` | `descriptiles-NEUROSYM.a2ml.txt` +| `.machine_readable/descriptiles/PLAYBOOK.a2ml` | `descriptiles-PLAYBOOK.a2ml.txt` +| `.machine_readable/descriptiles/0-AI-MANIFEST.a2ml` | `descriptiles-0-AI-MANIFEST.a2ml.txt` +| `.machine_readable/descriptiles/anchor/ANCHOR.a2ml` | `descriptiles-anchor-ANCHOR.a2ml.txt` +| `.machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml` | `descriptiles-anchor-0-AI-MANIFEST.a2ml.txt` +| `.machine_readable/bot_directives/hypatia.a2ml` | `bot_directives-hypatia.a2ml.txt` +| `.machine_readable/bot_directives/gitbot-fleet.a2ml` | `bot_directives-gitbot-fleet.a2ml.txt` +| `.machine_readable/bot_directives/git-private-farm.a2ml` | `bot_directives-git-private-farm.a2ml.txt` +| `.machine_readable/contractiles/{Mustfile,Trustfile,Dustfile,Bustfile,Adjustfile,Intentfile}.a2ml` | `contractiles-.a2ml.txt` (six) +| `0-AI-MANIFEST.a2ml` (root) | `root-0-AI-MANIFEST.a2ml.txt` +| `audits/assail-classifications.a2ml` | `audits-assail-classifications.a2ml.txt` +|=== + +== Where each file went + +[cols="2,4",options="header"] +|=== +| Source | Destination +| STATE v1 | Option B (ruled in the standards decision spec). Maturity goes to the deed as `(maturity :level experimental)`. Phase is not emitted (S-1). Journal sections are archived here (S-2..S-4). +| META | `(meta …)` and `(adr …)`-equivalent comments in the deed +| ECOSYSTEM | `(ecosystem :project :ecosystem)` in the deed; the rest in `coordination.k9` +| AGENTIC | `(agentic …)` in the deed; comment-carried canon (D4-1) as comments +| NEUROSYM | `(neurosym (hypatia …))` in the deed +| PLAYBOOK | `(playbook :version :last-updated)` in the deed; populated sections as comments +| root 0-AI-MANIFEST | `(manifest :last-updated)` in the deed (option A); rest fails closed +| ANCHOR | `(anchor …)` clause in the deed (template anchor precedent) +| bot_directives | `(bot-directives …)` clause in the deed (template precedent) +| contractiles (six) | `.machine_readable/contractiles//.k9.ncl` +| agent coordination (AGENTIC constraints, bot never-touch, ECOSYSTEM related) | `coordination.k9` at the repo root +| descriptiles/0-AI-MANIFEST, anchor/0-AI-MANIFEST | archived only; they describe a directory layout that no longer exists (G-5) +| audits/assail-classifications | archived only; it is a suppression list for `examples/haskell/Nop.hs` (ledger X-1) +|=== + +== Ledger rows + +=== Deed: canon, identity, status + +[cols="1,3,4",options="header"] +|=== +| ID | Item | Disposition +| C-1 | `[canon]` `lockstep-since` (template value 2026-09-17) | Not emitted. It is a per-repo adoption date that the source does not carry. The pin version 2.1.2 and the criteria/gates hashes were verified against standards `canon.lock`. +| I-1 | CLADE family 1: identity, clade, forges, lineage, status | Not emitted. There is no `CLADE.a2ml` source in this repo. Owner input is required and nothing was invented. +| S-2 | STATE `[recent-work]`, `[route-to-mvp]`, `[blockers-and-issues]`, `[critical-next-actions]`, `[session-history]`, `[components]`, `[working-features]`, `[migration-notes]` | Journal and derivable state. Archived here, not translated (v2 thin-journal doctrine). Open blockers and next actions are carried by the ultraplan and the issue list. +| S-3 | STATE `[maintenance-status]` | Archived. The last-run fact is not current state. +| S-4 | STATE `completion-percentage` and `[components]` percentages | Derivable from the milestone rows, so dropped (state-v1-decision §3). +| S-1 | STATE `[position] phase` | Not emitted. Phase belongs in the `(status …)` clause, and that needs CLADE (I-1). Owner input is required. +|=== + +=== Deed: META and ECOSYSTEM + +[cols="1,3,4",options="header"] +|=== +| ID | Item | Disposition +| M-1 | `[metadata]` version, last-updated; `[project-info]` license, author; `[development-practices] build-tool`; `[maintenance-axes]` | Emitted, per the table. +| M-2 | `[architecture-decisions]` ADR-001..ADR-014 | Text kept as comments. The ADR entries have no `:date`, which the table requires. Owner or the ADR history must supply dates. +| M-3 | `[development-practices]` code-style, testing, versioning, documentation, branching | Fail closed. No table row. Kept in the archive. +| M-4 | `[security]` principle | Fail closed. No table row. +| M-5 | `[proof-methodology]` rules | Fail closed. No table row. +| M-6 | `[design-rationale]` | Fail closed. No table row. +| M-7 | `[project-info]` type, languages, container-runtime, ci-platform, package-manager | Absent from the source. Not emitted; not invented. +| E-1 | ECOSYSTEM `[project]` name, type, role, purpose | Fail closed. No table row. Kept in the archive. The name is covered by `:project`. +| E-2 | ECOSYSTEM `[position-in-ecosystem]` category, subcategory, unique-value | Fail closed. No table row. +| E-3 | ECOSYSTEM `[what-this-is]` and `[what-this-is-not]` | Fail closed. No table row. +| E-4 | ECOSYSTEM `[related-projects]` | Relationships are outside the closed set. Carried verbatim in `coordination.k9` `ecosystem:`, with the relationship label kept in each role. +|=== + +=== Deed: AGENTIC, NEUROSYM, PLAYBOOK, root manifest + +[cols="1,3,4",options="header"] +|=== +| ID | Item | Disposition +| A-1 | `[agent-constraints]` and `[automation-hooks]` (comment-carried) | D4-1: template canon. Kept as deed comments because the divergence diff against canon was not run. Also summarised in `coordination.k9` invariants. +| A-2 | `[proof-safety]` counts (lean4-sorry-count, coq-admitted-count) | Dropped as derivable facts (the derivable-facts doctrine). The checks live in the K9 trust contract. +| A-3 | `[tools]` | Fail closed. No table row. +| N-1 | `[hypatia-config] report-format = "a2ml"` | Stale: Hypatia's Logtalk output was removed 2026-04-12, and the output format is retired. Kept verbatim, flagged. +| N-2 | `[symbolic-layer]` | Fail closed. No table row. +| N-3 | `[neural-layer]` | Fail closed. No table row. +| N-4 | `[integration]` (echidna planned, verisimdb TODO) | Fail closed. No table row. +| P-1 | `[deployment]`, `[build-procedures]`, `[proof-procedures]`, `[incident-response]`, `[release-process]`, `[rollback]`, `[maintenance-operations]`, `[contacts]` | Populated, so family-4 fails closed. Kept as deed comments. +| P-2 | `[proof-procedures]` verify-all `proofs/verify-all-provers.sh` | Stale. The gate is archived. The active gate is `proofs/verify-active-provers.sh`, run by `just verify`. +| P-3 | `[release-process]` update STATE and META | Stale. Both files are archived; the deed is the replacement. +| P-4 | `[maintenance-operations]` TODO recipes (`maint-audit`, `maint-hard-pass`) | Not present in the Justfile. Left as TODO. +| G-1 | Root manifest `manifest-version`, `[scope] purpose`, `[entry-points]`, `[machine-readable]` | Fail closed. Keys do not match the family table. +| G-2 | `[language-policy]` allowed and banned lists | Fail closed. Kept as deed comments and in `coordination.k9` (banned-language invariant). +| G-3 | `[echidna-protocol]` (ECHIDNA only through the BoJ MCP cartridge) | Fail closed. No table row. Kept in the archive. +| G-4 | `[delivery]` "architectural changes recorded in META.scm" | Stale: points at a retired file. Superseded by the ADR comments. +| G-5 | descriptiles/0-AI-MANIFEST and anchor/0-AI-MANIFEST (directory manifests) | Archived only. They describe a six-file layout that no longer exists. +|=== + +=== Deed: bot_directives and anchor + +[cols="1,3,4",options="header"] +|=== +| ID | Item | Disposition +| B-1 | hypatia `[[accepted-findings]]` (4 entries) | Emitted as `(accepted-finding …)` clauses. Reasons copied in full. +| B-2 | gitbot-fleet `[fleet]`, `[branch-policy]`, `[per-bot.*]` | Emitted as `(fleet …)`, `(branch-policy …)`, `(per-bot …)`. +| B-3 | git-private-farm `[propagation]` (disabled), `[never-propagate]`, `[on-token-rotation]` | Emitted. The secret NAME is recorded. The value is never in the repo. +| B-4 | ANCHOR realignment 2026-06-12 | Emitted as `(anchor …)` with `(realignment …)`. +|=== + +=== K9 contracts + +[cols="1,3,4",options="header"] +|=== +| ID | Item | Disposition +| K-1 | 'Hunt contracts (must, trust, bust, intend) have no signature block | K9-S009 fails by design. No signing ceremony has run and the sandbox has no signing key, so no signature was fabricated. These contracts are not authorised to run as 'Hunt until the owner signs them. The 'Yard contracts (dust, adjust) do not need one. +| K-2 | Nickel L2 typecheck (K9-N001, K9-N002) | Not run. The Nickel release binary is hosted on `release-assets.githubusercontent.com`, which is not on this sandbox's allowlist, and no Nickel build is available on the allowed registries. Run `k9-validate.sh --strict` where Nickel is installed. +| K-3 | Leash source | The source Mustfile/Trustfile/Dustfile/Bustfile/Adjustfile/Intentfile declare no leash. Leashes come from the estate template canon for each verb: must, trust, bust, intend = 'Hunt; dust, adjust = 'Yard. +| K-4 | Grants | 'Hunt contracts request `process.spawn` only, because their probes shell out. 'Yard contracts request nothing. +| A-M1 | must: `proofs-tree-present` | Adapted. Checks the active tree (agda, z3, observation-models, residue) and archive/proofs/*. +| A-M2 | must: `six-a2ml-present` | Adapted to `deed-and-coordination-present`. +| A-M3 | must: `contractiles-flat-complete` | Adapted to `contractiles-k9-complete`. The flat layout was the a2ml layout. +| A-M4 | must: `anchor-directory` | Adapted to `anchor-clause-present` (ANCHOR is a deed clause). +| A-M5 | must: `bot-directives-present` | Adapted to a deed clause check. +| A-M6 | must: `ai-manifest` | Adapted to a deed `(manifest` clause check. +| A-M7 | must: `a2ml-parses-as-toml` | Retired. Replaced by the new check `no-live-a2ml`, which states the migration ruling. +| A-T1 | trust: `lean4-sorry-bounded` | Path adapted to `archive/proofs/lean4/`. +| A-T2 | trust: `coq-admitted-bounded` | Path adapted to `archive/proofs/coq/`. +| A-T3 | trust: protected-paths | Added `TOPOLOGY.adoc` (standing rule: never edit) and `coordination.k9`. Both are additions to the source list. +| B-5 | bust: runner | Not enabled (the source says so). The old bust.ncl runner is absent. D187 and #81 rule on dropping it. +| D-1 | dust, adjust: `adjust fix` auto-fix and file writes | Not operative under 'Yard. The corrective actions are for humans and agents. +| D-A1 | dust: `proof-suite-regression` asset | Updated to name the active and archived proof trees. +| D-A2 | dust: `stale-machine-metadata` asset | Updated to name the deed, the K9 set, coordination.k9 and bot_directives. +| A-A1 | adjust: `coq-axiom-count`, `coq-parameter-count` | Marked archived, not gated. +| A-A2 | adjust: `physics-constant-duplication` | Marked archived (the duplicates are in archived Coq). +| A-I1 | intend: purpose statement | Updated to the active stack (owner ruling 2026-10-10). The old six-prover statement is kept in `supersedes`. +| A-I2 | intend: `phase-2-triage` | Narrowed to the Idris 2 postulates. The Lean item is parked. +| A-I3 | intend: `v1-0-publication-release` | Paper scope is out of date. Parked for the owner. +| X-1 | `injection_scope` in bust `security`; `audits/assail-classifications` | `injection_scope` is an extension field, which the spec permits. The audit suppression is archived only. +|=== + +=== coordination.k9 + +[cols="1,3,4",options="header"] +|=== +| ID | Item | Disposition +| CO-1 | `coordination.k9` name and grammar | Verified: standards CLAUDE.md names `coordination.k9` at the repo root, and the grammar is `2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.1.abnf`. +| CO-2 | Grammar conformance | Checked by hand against the grammar (indentation levels, section order, symbol and string rules). The standards generator was NOT run: it imports from `jsr:` and this repo's toolchain does not run that loader. +|=== + +== Validation status (2026-10-10) + +[cols="3,2,5",options="header"] +|=== +| Check | Result | Notes +| Deed: `deed_lint` (normative grammar + filename dispatch) | PASS | Run under Node. The lint script is Bun-only, so it was copied to a `.mjs` file with its `import.meta.main` guard removed. The lint was not changed otherwise. Control: the template deed passes too. +| K9 L0 (envelope) and L1 (structure), six contracts | PASS for dust and adjust; 4 fail only K9-S009 | See K-1. +| K9 L2 (Nickel typecheck) | NOT RUN | See K-2. +| coordination.k9 generator | NOT RUN | See CO-2. +| Proof gate `proofs/verify-active-provers.sh` | NOT RUN here | Agda, Z3 and Idris 2 are not installed in this sandbox. The gate fails closed (a missing tool is a failure). +|=== + +== Open items (owner) + +. Sign the four 'Hunt contracts, or set their leash, so that K9-S009 passes (K-1). +. CLADE input for identity, clade, forges, lineage and status (I-1, S-1). +. Dates for the ADR entries (M-2). +. Ruling on the 'reporting authority for intend, and on whether the root manifest keys are kept (G-1). +. The four proof-stack flags in `archive/README.adoc`. +. Narrative docs still describe six provers. Archive banners are the first step; a full rewrite is a follow-up. +. CI gap: the z3 job in `proofs.yml` no longer runs the archived six-prover self-test. A self-test for `proofs/verify-active-provers.sh` (stubbed tools must turn it red) has not been written yet. +. Containerfile line 29 still installs `coq` in the apt layer. The `coqc` build lines were removed; the package line was left for the owner to decide. +. `.gitlab-ci.yml`: `verify:coq`, `verify:lean4` and `verify:isabelle` were removed, and the summary now says those provers are archived. No Agda job was added to GitLab. +. Retired notes added to `.machine_readable/bot_directives/README.adoc`, `.machine_readable/descriptiles/README.adoc` and `.machine_readable/descriptiles/anchor/README.adoc`. Their bodies still describe the retired A2ML set. +. `.claude/CLAUDE.md`: the Machine-Readable Artefacts section and the language-table row now name the deed and K9 files. The rest of that file is not reviewed. diff --git a/audits/assail-classifications.a2ml b/archive/a2ml-v1/audits-assail-classifications.a2ml.txt similarity index 100% rename from audits/assail-classifications.a2ml rename to archive/a2ml-v1/audits-assail-classifications.a2ml.txt diff --git a/.machine_readable/bot_directives/git-private-farm.a2ml b/archive/a2ml-v1/bot_directives-git-private-farm.a2ml.txt similarity index 100% rename from .machine_readable/bot_directives/git-private-farm.a2ml rename to archive/a2ml-v1/bot_directives-git-private-farm.a2ml.txt diff --git a/.machine_readable/bot_directives/gitbot-fleet.a2ml b/archive/a2ml-v1/bot_directives-gitbot-fleet.a2ml.txt similarity index 100% rename from .machine_readable/bot_directives/gitbot-fleet.a2ml rename to archive/a2ml-v1/bot_directives-gitbot-fleet.a2ml.txt diff --git a/.machine_readable/bot_directives/hypatia.a2ml b/archive/a2ml-v1/bot_directives-hypatia.a2ml.txt similarity index 100% rename from .machine_readable/bot_directives/hypatia.a2ml rename to archive/a2ml-v1/bot_directives-hypatia.a2ml.txt diff --git a/.machine_readable/contractiles/Adjustfile.a2ml b/archive/a2ml-v1/contractiles-Adjustfile.a2ml.txt similarity index 100% rename from .machine_readable/contractiles/Adjustfile.a2ml rename to archive/a2ml-v1/contractiles-Adjustfile.a2ml.txt diff --git a/.machine_readable/contractiles/Bustfile.a2ml b/archive/a2ml-v1/contractiles-Bustfile.a2ml.txt similarity index 100% rename from .machine_readable/contractiles/Bustfile.a2ml rename to archive/a2ml-v1/contractiles-Bustfile.a2ml.txt diff --git a/.machine_readable/contractiles/Dustfile.a2ml b/archive/a2ml-v1/contractiles-Dustfile.a2ml.txt similarity index 100% rename from .machine_readable/contractiles/Dustfile.a2ml rename to archive/a2ml-v1/contractiles-Dustfile.a2ml.txt diff --git a/.machine_readable/contractiles/Intentfile.a2ml b/archive/a2ml-v1/contractiles-Intentfile.a2ml.txt similarity index 100% rename from .machine_readable/contractiles/Intentfile.a2ml rename to archive/a2ml-v1/contractiles-Intentfile.a2ml.txt diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/archive/a2ml-v1/contractiles-Mustfile.a2ml.txt similarity index 100% rename from .machine_readable/contractiles/Mustfile.a2ml rename to archive/a2ml-v1/contractiles-Mustfile.a2ml.txt diff --git a/.machine_readable/contractiles/Trustfile.a2ml b/archive/a2ml-v1/contractiles-Trustfile.a2ml.txt similarity index 100% rename from .machine_readable/contractiles/Trustfile.a2ml rename to archive/a2ml-v1/contractiles-Trustfile.a2ml.txt diff --git a/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml b/archive/a2ml-v1/descriptiles-0-AI-MANIFEST.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/0-AI-MANIFEST.a2ml rename to archive/a2ml-v1/descriptiles-0-AI-MANIFEST.a2ml.txt diff --git a/.machine_readable/descriptiles/AGENTIC.a2ml b/archive/a2ml-v1/descriptiles-AGENTIC.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/AGENTIC.a2ml rename to archive/a2ml-v1/descriptiles-AGENTIC.a2ml.txt diff --git a/.machine_readable/descriptiles/ECOSYSTEM.a2ml b/archive/a2ml-v1/descriptiles-ECOSYSTEM.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/ECOSYSTEM.a2ml rename to archive/a2ml-v1/descriptiles-ECOSYSTEM.a2ml.txt diff --git a/.machine_readable/descriptiles/META.a2ml b/archive/a2ml-v1/descriptiles-META.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/META.a2ml rename to archive/a2ml-v1/descriptiles-META.a2ml.txt diff --git a/.machine_readable/descriptiles/NEUROSYM.a2ml b/archive/a2ml-v1/descriptiles-NEUROSYM.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/NEUROSYM.a2ml rename to archive/a2ml-v1/descriptiles-NEUROSYM.a2ml.txt diff --git a/.machine_readable/descriptiles/PLAYBOOK.a2ml b/archive/a2ml-v1/descriptiles-PLAYBOOK.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/PLAYBOOK.a2ml rename to archive/a2ml-v1/descriptiles-PLAYBOOK.a2ml.txt diff --git a/.machine_readable/descriptiles/STATE.a2ml b/archive/a2ml-v1/descriptiles-STATE.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/STATE.a2ml rename to archive/a2ml-v1/descriptiles-STATE.a2ml.txt diff --git a/.machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml b/archive/a2ml-v1/descriptiles-anchor-0-AI-MANIFEST.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml rename to archive/a2ml-v1/descriptiles-anchor-0-AI-MANIFEST.a2ml.txt diff --git a/.machine_readable/descriptiles/anchor/ANCHOR.a2ml b/archive/a2ml-v1/descriptiles-anchor-ANCHOR.a2ml.txt similarity index 100% rename from .machine_readable/descriptiles/anchor/ANCHOR.a2ml rename to archive/a2ml-v1/descriptiles-anchor-ANCHOR.a2ml.txt diff --git a/0-AI-MANIFEST.a2ml b/archive/a2ml-v1/root-0-AI-MANIFEST.a2ml.txt similarity index 100% rename from 0-AI-MANIFEST.a2ml rename to archive/a2ml-v1/root-0-AI-MANIFEST.a2ml.txt diff --git a/proofs/coq/_CoqProject b/archive/proofs/coq/_CoqProject similarity index 100% rename from proofs/coq/_CoqProject rename to archive/proofs/coq/_CoqProject diff --git a/proofs/coq/audit/Assumptions.v b/archive/proofs/coq/audit/Assumptions.v similarity index 100% rename from proofs/coq/audit/Assumptions.v rename to archive/proofs/coq/audit/Assumptions.v diff --git a/proofs/coq/category/CNOCategory.v b/archive/proofs/coq/category/CNOCategory.v similarity index 100% rename from proofs/coq/category/CNOCategory.v rename to archive/proofs/coq/category/CNOCategory.v diff --git a/proofs/coq/census-assumptions.sh b/archive/proofs/coq/census-assumptions.sh similarity index 100% rename from proofs/coq/census-assumptions.sh rename to archive/proofs/coq/census-assumptions.sh diff --git a/proofs/coq/check-assumptions.sh b/archive/proofs/coq/check-assumptions.sh similarity index 100% rename from proofs/coq/check-assumptions.sh rename to archive/proofs/coq/check-assumptions.sh diff --git a/proofs/coq/check-axiom-tags.sh b/archive/proofs/coq/check-axiom-tags.sh similarity index 100% rename from proofs/coq/check-axiom-tags.sh rename to archive/proofs/coq/check-axiom-tags.sh diff --git a/proofs/coq/common/CNO.v b/archive/proofs/coq/common/CNO.v similarity index 100% rename from proofs/coq/common/CNO.v rename to archive/proofs/coq/common/CNO.v diff --git a/proofs/coq/common/Complex.v b/archive/proofs/coq/common/Complex.v similarity index 100% rename from proofs/coq/common/Complex.v rename to archive/proofs/coq/common/Complex.v diff --git a/proofs/coq/common/PhysicsConstants.v b/archive/proofs/coq/common/PhysicsConstants.v similarity index 100% rename from proofs/coq/common/PhysicsConstants.v rename to archive/proofs/coq/common/PhysicsConstants.v diff --git a/proofs/coq/common/StatMechBasis.v b/archive/proofs/coq/common/StatMechBasis.v similarity index 100% rename from proofs/coq/common/StatMechBasis.v rename to archive/proofs/coq/common/StatMechBasis.v diff --git a/proofs/coq/filesystem/FilesystemCNO.v b/archive/proofs/coq/filesystem/FilesystemCNO.v similarity index 100% rename from proofs/coq/filesystem/FilesystemCNO.v rename to archive/proofs/coq/filesystem/FilesystemCNO.v diff --git a/proofs/coq/lambda/LambdaCNO.v b/archive/proofs/coq/lambda/LambdaCNO.v similarity index 100% rename from proofs/coq/lambda/LambdaCNO.v rename to archive/proofs/coq/lambda/LambdaCNO.v diff --git a/proofs/coq/malbolge/MalbolgeCore.v b/archive/proofs/coq/malbolge/MalbolgeCore.v similarity index 100% rename from proofs/coq/malbolge/MalbolgeCore.v rename to archive/proofs/coq/malbolge/MalbolgeCore.v diff --git a/proofs/coq/ond/OND.v b/archive/proofs/coq/ond/OND.v similarity index 100% rename from proofs/coq/ond/OND.v rename to archive/proofs/coq/ond/OND.v diff --git a/proofs/coq/physics/LandauerDerivation.v b/archive/proofs/coq/physics/LandauerDerivation.v similarity index 100% rename from proofs/coq/physics/LandauerDerivation.v rename to archive/proofs/coq/physics/LandauerDerivation.v diff --git a/proofs/coq/physics/StatMech.v b/archive/proofs/coq/physics/StatMech.v similarity index 100% rename from proofs/coq/physics/StatMech.v rename to archive/proofs/coq/physics/StatMech.v diff --git a/proofs/coq/physics/StatMech_helpers.v b/archive/proofs/coq/physics/StatMech_helpers.v similarity index 100% rename from proofs/coq/physics/StatMech_helpers.v rename to archive/proofs/coq/physics/StatMech_helpers.v diff --git a/proofs/coq/quantum/QuantumCNO.v b/archive/proofs/coq/quantum/QuantumCNO.v similarity index 100% rename from proofs/coq/quantum/QuantumCNO.v rename to archive/proofs/coq/quantum/QuantumCNO.v diff --git a/proofs/coq/quantum/QuantumMechanicsExact.v b/archive/proofs/coq/quantum/QuantumMechanicsExact.v similarity index 100% rename from proofs/coq/quantum/QuantumMechanicsExact.v rename to archive/proofs/coq/quantum/QuantumMechanicsExact.v diff --git a/proofs/isabelle/CNO.thy b/archive/proofs/isabelle/CNO.thy similarity index 100% rename from proofs/isabelle/CNO.thy rename to archive/proofs/isabelle/CNO.thy diff --git a/proofs/isabelle/OND.thy b/archive/proofs/isabelle/OND.thy similarity index 100% rename from proofs/isabelle/OND.thy rename to archive/proofs/isabelle/OND.thy diff --git a/proofs/isabelle/ROOT b/archive/proofs/isabelle/ROOT similarity index 100% rename from proofs/isabelle/ROOT rename to archive/proofs/isabelle/ROOT diff --git a/proofs/lean4/AxiomAudit.lean b/archive/proofs/lean4/AxiomAudit.lean similarity index 100% rename from proofs/lean4/AxiomAudit.lean rename to archive/proofs/lean4/AxiomAudit.lean diff --git a/proofs/lean4/CNO.lean b/archive/proofs/lean4/CNO.lean similarity index 100% rename from proofs/lean4/CNO.lean rename to archive/proofs/lean4/CNO.lean diff --git a/proofs/lean4/CNOBridge.lean b/archive/proofs/lean4/CNOBridge.lean similarity index 100% rename from proofs/lean4/CNOBridge.lean rename to archive/proofs/lean4/CNOBridge.lean diff --git a/proofs/lean4/CNOCategory.lean b/archive/proofs/lean4/CNOCategory.lean similarity index 100% rename from proofs/lean4/CNOCategory.lean rename to archive/proofs/lean4/CNOCategory.lean diff --git a/proofs/lean4/FilesystemCNO.lean b/archive/proofs/lean4/FilesystemCNO.lean similarity index 100% rename from proofs/lean4/FilesystemCNO.lean rename to archive/proofs/lean4/FilesystemCNO.lean diff --git a/proofs/lean4/LambdaCNO.lean b/archive/proofs/lean4/LambdaCNO.lean similarity index 100% rename from proofs/lean4/LambdaCNO.lean rename to archive/proofs/lean4/LambdaCNO.lean diff --git a/proofs/lean4/OND.lean b/archive/proofs/lean4/OND.lean similarity index 100% rename from proofs/lean4/OND.lean rename to archive/proofs/lean4/OND.lean diff --git a/proofs/lean4/QuantumCNO.lean b/archive/proofs/lean4/QuantumCNO.lean similarity index 100% rename from proofs/lean4/QuantumCNO.lean rename to archive/proofs/lean4/QuantumCNO.lean diff --git a/proofs/lean4/StatMech.lean b/archive/proofs/lean4/StatMech.lean similarity index 100% rename from proofs/lean4/StatMech.lean rename to archive/proofs/lean4/StatMech.lean diff --git a/proofs/lean4/check-core.sh b/archive/proofs/lean4/check-core.sh similarity index 100% rename from proofs/lean4/check-core.sh rename to archive/proofs/lean4/check-core.sh diff --git a/proofs/lean4/lake-manifest.json b/archive/proofs/lean4/lake-manifest.json similarity index 100% rename from proofs/lean4/lake-manifest.json rename to archive/proofs/lean4/lake-manifest.json diff --git a/proofs/lean4/lakefile.lean b/archive/proofs/lean4/lakefile.lean similarity index 100% rename from proofs/lean4/lakefile.lean rename to archive/proofs/lean4/lakefile.lean diff --git a/proofs/lean4/lean-toolchain b/archive/proofs/lean4/lean-toolchain similarity index 100% rename from proofs/lean4/lean-toolchain rename to archive/proofs/lean4/lean-toolchain diff --git a/proofs/mizar/CNO.miz b/archive/proofs/mizar/CNO.miz similarity index 100% rename from proofs/mizar/CNO.miz rename to archive/proofs/mizar/CNO.miz diff --git a/proofs/mizar/dict/cno.voc b/archive/proofs/mizar/dict/cno.voc similarity index 100% rename from proofs/mizar/dict/cno.voc rename to archive/proofs/mizar/dict/cno.voc diff --git a/proofs/tests/gate-selftest.sh b/archive/proofs/tests/gate-selftest.six-prover.sh similarity index 100% rename from proofs/tests/gate-selftest.sh rename to archive/proofs/tests/gate-selftest.six-prover.sh diff --git a/proofs/verify-all-provers.sh b/archive/proofs/verify-all-provers.six-prover.sh similarity index 100% rename from proofs/verify-all-provers.sh rename to archive/proofs/verify-all-provers.six-prover.sh diff --git a/coordination.k9 b/coordination.k9 new file mode 100644 index 0000000..766d0b9 --- /dev/null +++ b/coordination.k9 @@ -0,0 +1,128 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# coordination.k9 — agent coordination for absolute-zero (K9 coordination protocol v1.1.1) +# +# Migrated 2026-10-10 from the a2ml descriptiles and bot_directives (archive/a2ml-v1/). +# Grammar: 2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.1.abnf +# (standards). Full provenance: archive/a2ml-v1/MIGRATION-LEDGER.adoc. +# +# Invariant rules come from AGENTIC.a2ml constraints and maintenance integrity, +# the 0-AI-MANIFEST language policy, Intentfile if-in-doubt, and bot-directives +# never-touch lists. Ecosystem entries come from ECOSYSTEM.a2ml related-projects, +# with the source relationship kept verbatim in each role. + +metadata: + schema: k9-coordination + schema_version: 1.1.1 + generated_by: "hand-migrated from a2ml-v1 (2026-10-10); not generator output" + last_updated: 2026-10-10 + +project: + name: "Absolute Zero" + description: "Formal verification of Certified Null Operations (CNOs): programs proven to compute nothing, with the OND disclosure pillar. Active proof stack: Idris 2 (ABI), Agda and Z3. Coq, Lean 4, Isabelle and Mizar are archived." + license: MPL-2.0 + repo: hyperpolymath/absolute-zero + deed_ref: absolute-zero_chora.deed + languages: + - Idris2 + - Agda + - Z3 + - Rust + build_system: just + +invariants: + - id: no-dangerous-proof-patterns + rule: "Never use believe_me, assert_total, Admitted, sorry, unsafeCoerce or Obj.magic in load-bearing proofs or source" + reason: "Escape hatches defeat the proofs. AGENTIC.a2ml constraints; Trustfile dangerous-patterns section" + severity: critical + - id: no-new-axioms-to-close-goals + rule: "Never introduce a new axiom or postulate to close a goal. If a proof cannot be completed, leave it open and report it" + reason: "A silent axiom is unverified trust. The open remainder is tracked openly (ADR-014)" + severity: critical + - id: no-silent-skip + rule: "A check that could not run is a failure, never a pass or a skip" + reason: "allow-silent-skip = false in AGENTIC maintenance-integrity; the gate-that-could-never-fire defect" + severity: critical + - id: no-secrets + rule: "Never commit secrets or credentials" + reason: "Trustfile secrets section. Public history cannot be un-published" + severity: critical + - id: no-typescript-or-banned-runtimes + rule: "Do not introduce banned-language code (TypeScript, Node.js, npm, Bun, pnpm, yarn, Go, Python, Java, Kotlin, Swift, Dart, Ruby, Perl and the rest of the 0-AI-MANIFEST banned list) outside the enumerated carve-outs" + reason: "Estate language policy (0-AI-MANIFEST); carve-outs are examples/ and the .hypatia-ignore list" + severity: high + - id: no-dockerfile + rule: "Use Containerfile, not Dockerfile" + reason: "Podman is the container runtime (Mustfile no-dockerfile)" + severity: high + - id: no-licence-sweep + rule: "Never relicense an existing file, never run an automated licence sweep, never assume a licence" + reason: "LICENCE-POLICY A2 and rules 1-5. New files get correct SPDX from birth" + severity: high + - id: no-new-a2ml + rule: "Do not create new .a2ml files. Metadata lives in _chora.deed and contracts in *.k9.ncl" + reason: "a2ml is retired (D99, D269c, D312, D313)" + severity: high + - id: maintainer-gated-areas + rule: "Proof semantics, the Idris 2 ABI, CI workflows and LICENSE are maintainer-gated: ask before touching" + reason: "Intentfile if-in-doubt; bot-directives never-touch lists" + severity: high + - id: topology-never-edited + rule: "Never edit TOPOLOGY.adoc" + reason: "Estate rule (standards constraint)" + severity: critical + - id: checkpoints-under-machine-readable + rule: "Place agent checkpoint files only under .machine_readable/" + reason: "AGENTIC.a2ml constraints" + severity: moderate + +protected: + - path: .machine_readable/contractiles/ + reason: "K9 contract set. The signature ceremony gates 'Hunt" + - path: proofs/ + reason: "Active proof surface; semantics are maintainer-gated" + - path: src/abi/ + reason: "Idris 2 ABI proof surface" + - path: .github/workflows/ + reason: "CI gates, pinned to standards reusables" + - path: LICENSE + reason: "Licence is maintainer-gated" + - path: TOPOLOGY.adoc + reason: "Never edited by agents" + - path: coordination.k9 + reason: "Source of truth for AI coordination" + +do_not_create: + - pattern: Dockerfile + reason: "Use Containerfile (Podman)" + - pattern: .machine_readable/**/*.a2ml + reason: "a2ml is retired; the deed and K9 files replace it" + +ecosystem: + depends_on: + - name: rsr-template-repo + role: "infrastructure: repository standards template" + consumed_by: + - name: januskey + role: "downstream-consumer: reversible file operations CLI formally verified by FilesystemCNO" + - name: typell + role: "theory-consumer: category-theoretic query verification via CNOCategory" + related: + - name: echidna + role: "sibling-standard: security scanning; potential CNO verifier integration" + - name: echidnabot + role: "potential-consumer: GitHub bot; could automate CNO checks in PRs" + - name: valence-shell + role: "integration-target: filesystem ops library proven in FilesystemCNO.v" + - name: echo-types + role: "bridge-target: EchoBridgeCNO.agda connects the CNO zero-loss boundary with proof-relevant fibers" + - name: robodog-defensive-systems-lab + role: "application-domain: reversible defensive maneuvers (CNO) and side-channel non-disclosure (OND)" + - name: robot-vacuum-cleaner + role: "application-domain: transactional SLAM map rollback (CNO) and privacy telemetry boundaries (OND)" + +coordination: + available: + - "#27: Idris 2 believe_me sites (src/abi/AbsoluteZero/ABI/Proofs/DivMod.idr and Layout.idr)" + - "Archive banners on the six-prover narrative docs (README, PROOF-STATUS, docs/*); full rewrite is a separate follow-up" + - "#182: CodeRabbit UI setting (commit-pushing off per D217); the repo-side .coderabbit.yaml is in place" diff --git a/docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc b/docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc new file mode 100644 index 0000000..dadba1e --- /dev/null +++ b/docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc @@ -0,0 +1,927 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += ULTRAPLAN: Absolute Zero open issues (2026-10-10, revision 2) +:toc: left +:toclevels: 2 +:sectnums: + +[NOTE] +==== +*Status: PLAN, with uncommitted working-tree changes.* Nothing has been filed, +edited or closed on GitHub. No PR, ruleset or workflow was changed on GitHub. +Locally, branch `arena/6c682e29-absolute-zero` carries the changes listed in +<>. They are not committed, not signed, not pushed and not reviewed. Every +GitHub action below waits on the owner decisions in <>, and each +PR goes through the estate's normal review and signing path. + +*Basis:* `main` @ `6010145` (PR #186) for the recon; the ten open issues of +`hyperpolymath/absolute-zero`; `hyperpolymath/standards` (shallow clone at +`3108c1b`, decision sheet `standards#787`); `hyperpolymath/rsr-template-repo` +(shallow clone at `df09a6c`). + +*Claim labels* follow `0-canon/constitution/ASSURANCE-CONSTITUTION.adoc`. +*Measured* means read from the repo, the GitHub API or the canon during this +work. *Designed* means a proposal. *Assumed* means taken from a source that was +not checked here. Nothing here is *proven*. No prover was run in this session: +Agda, Z3 and Idris 2 are not installed in the sandbox, and the archived provers +were not run. Prover status comes from CI on `main`, which is not proof. +==== + +== Summary + +* *Ten issues are open:* #182, #175, #171, #170, #167, #161, #81, #76, #70, + #27. Seventeen are closed. I checked the closed ones only where they touch + open work. +* *`main` is red on three workflows:* CodeQL (startup failure), Governance + (`Actions lockfile verify`) and Scorecards (`Reconcile native action pins`). + They share one likely cause: `actions.lock` drift after Dependabot bumps #185 + and #186. No open issue covers it. It is still the first thing to fix (<>). + This revision does not touch it. +* *The owner ruled on the proof stack (2026-10-10).* The active stack is Idris 2 + (ABI) and Agda (CNO, OND, EchoBridge), with Z3 as a bounded-check solver. Coq, + Lean 4, Isabelle/HOL and Mizar are archived under `archive/proofs/`. That + removes the subject of #171, the `coqchk` part of #161, and most of #70. It + creates a new conflict for #167 (<>). +* *The A2ML-to-deed migration is done in the working tree (<>).* No tracked + `.a2ml` files remain. Six K9 contracts, a `_chora.deed` and `coordination.k9` + are in place. Still open: Nickel L2 validation, owner signing of the four Hunt + contracts, and an unverified author email. +* *#27's postulate was deleted.* Its five `believe_me` sites remain, and a CI + build of the ABI is now in the working tree (<>), but it has not been run. +* *Three issues have owner rulings that change their scope:* #167 (D204 rescope, + now also conflicting with the archive), #81 (D187 "drop the runner"), and #175 + (D188 "rename", with no replacement term chosen). +* *Two issues are blocked on a decision:* #76 (a template-level ruling) and #70 + (its 2026-05-30 comment recommends deferral). +* *One contradiction cannot be resolved locally:* the proof-assistant policy + (<>). The owner ruling narrows it. It does not remove it. + +[[wt]] +== Working-tree changes since the recon + +Recorded so that the plan matches the tree. Nothing is committed. The sandbox +commits would be unsigned, so the PR path is a signed cherry-pick (<>). + +[cols="1,3,3",options="header"] +|=== +| Area | What changed | Check status + +| Proof stack +| 39 renames: `proofs/{coq,lean4,isabelle,mizar}` and the six-prover gate and + self-test moved to `archive/proofs/`. New active gate + `proofs/verify-active-provers.sh` runs Agda, Z3 and Idris 2. +| *Measured:* run here. All three tools are missing, so the gate fails closed + with exit 1 and no skip. Its paths exist. Not run with the tools present. + +| `proofs.yml` +| Rewritten. Jobs: `agda`, `z3`, `idris`. The `coq` and `lean` jobs are removed. + The z3 job no longer runs the archived self-test (no replacement yet, <>). + The `idris` job builds `absolute-zero-abi.ipkg` on the same digest-pinned image + as `pages.yml`. The `uses:` set is unchanged (`actions/checkout@v7.0.1`). +| *Measured:* parses as YAML (js-yaml). Not run on CI. The `idris` job is + *designed*, not tested. + +| Justfile +| Prover sections rewritten to the active stack. `contractiles/Justfile` was + synced, so the two copies are byte-identical again (#76 state). +| *Measured:* `cmp` equal. `just` is not installed, so not run. + +| Containerfile, `.gitlab-ci.yml` +| `coqc` RUN lines removed. `verify:coq`, `verify:lean4` and `verify:isabelle` + removed from GitLab CI. The apt `coq` package line is still there (<>). +| *Measured:* GitLab YAML parses. + +| `.coderabbit.yaml` +| New. Docstring pre-merge check at `mode: warning`, threshold 80, as in the + template. Docstring finishing touch disabled (D217). +| *Measured:* parses. The template uses the same `reviews:` keys. The schema's + first chunk confirms `reviews`. The `finishing_touches` key was not verified + against the schema's later chunks. The app-UI setting is untouched (Q9). + +| A2ML and deed +| 20 `.a2ml` sources moved to `archive/a2ml-v1/-.a2ml.txt` (`git mv`). + `absolute-zero_chora.deed` added. Ledger: `archive/a2ml-v1/MIGRATION-LEDGER.adoc`. + `.claude/CLAUDE.md` artefact section now names the deed and the K9 files. + Retired notes on the three `.machine_readable` READMEs that described A2ML. +| *Measured:* 0 tracked `*.a2ml`. Deed linter (a copy of the template's + `deed_lint.js`, run with node) passes. Template CI not run. + +| K9 and coordination +| Six contracts under `.machine_readable/contractiles//.k9.ncl`, all + unsigned (K-1). `coordination.k9` at the repo root. +| *Measured:* `dust` and `adjust` pass the K9 validator. `must`, `trust`, `bust` + and `intend` fail `K9-S009` only. *Not run:* Nickel L2 (no Nickel binary; the + release download and the npm packages are blocked). The standards generator + was not run because it imports from `jsr:`. + +| Docs +| `archive/README.adoc`. Archive notices in `README.adoc` and `PROOF-STATUS.adoc` + (placed after the title block, before the first section). +| Full rewrites of README, PROOF-STATUS and `docs/*` are a separate follow-up. + +| Git +| 59 renames staged. Modified and new files are unstaged or untracked. No commit. +| *Outcome unknown until committed.* +|=== + +== Ground rules: the binding canon applied + +[cols="1,2,3",options="header"] +|=== +| Authority | Source | What it binds for this plan + +| Constitution +| `standards/0-canon/constitution/` (ESTATE, ASSURANCE, EXCEPTIONS-AND-ANCHORS, + KNOWN-TENSIONS, CHANGE-PROCEDURE) +| Claims carry a label. An exception needs a full record: rule, scope, reason, + authority, containment, expiry, exit. A contradiction goes in the tension + register and is not silently resolved. Evidence does not override policy. + +| Owner rulings +| `standards#787` ledger: D85–D89, D124, D187, D188, D204, D215–D218, D220, + D222, D239, and the 2026-10-10 proof-stack ruling +| Binding decisions. An issue body is subordinate to a later ruling. A ruling + closes on the surface it governs. + +| Agent canon +| `standards/AGENTS.adoc`, `standards/.claude/CLAUDE.md` +| A2ML is retired. Do not create or extend `.a2ml`. Repo metadata goes in + `_chora.deed`, contracts in `*.k9.ncl`. No TypeScript, no Deno, no + Python outside enumerated carve-outs. Do not sweep licence headers. + +| Signing +| `standards/docs/SIGNING-POLICY.adoc` (D215–D218) +| Every commit on a PR branch is signed. Bots do not push commits to PR + branches. The remedy is a signed cherry-pick into a new PR, not a force-push + and not an admin merge. Squash-merge only. + +| Language +| `standards/0-canon/rsr/LANGUAGE-POLICY.adoc` v1.6.0 +| Bun is tier 1 and Deno is banned (ruling 2026-09-22). All Python is banned + (the SaltStack exception was removed 2026-01-03). The policy says Idris 2 is the + only formal-verification language. The owner's 2026-10-10 ruling makes Idris 2 + and Agda the active stack (<>). + +| RSR criteria +| `standards/0-canon/rsr/RSR-SPEC-v2.adoc`, `rsr-criteria-v2.a2ml` (2.1.0-draft) +| *DRAFT. Do not cite as ratified.* Used as a checklist only, and labelled as + draft. Some gates still name A2ML (<>). + +| Template +| `rsr-template-repo`: `.github/workflows/`, `.github/rulesets/`, + `.coderabbit.yaml`, `scripts/check-lock-sync.sh` +| The worked model. It ships `lock-sync-gate.yml`, `estate-rules.yml`, + `runtime-policy.yml`, `deed-validate.yml`, and `rsr-template-repo_chora.deed` + with no `.a2ml` files. Its own `.coderabbit.yaml` enables a docstring + finishing touch (<>). + +| Local policy +| `absolute-zero/.claude/CLAUDE.md`, `RSR_COMPLIANCE.adoc` +| `CLAUDE.md` artefact section updated in the working tree. `RSR_COMPLIANCE.adoc` + is still stale. Local policy cannot override estate canon (<>). +|=== + +== Recon: the ten open issues against the current repo + +The "Measured state" column is the recon at `main` @ `6010145`. The "Verdict" +column is revised for the working tree. + +[cols="1,2,3,3",options="header"] +|=== +| Issue | Title (short) | Measured state (recon, `main` @ `6010145`) | Verdict (revision 2) + +| #182 +| CodeRabbit pushes unsigned bot commits +| No `.coderabbit.yaml` in this repo. D217 rules CodeRabbit commit-pushing off. + The app-level setting is not visible from the repo. +| *Repo half in the working tree; app half open (Q9).* Not verified applied. + +| #175 +| "residue list" collides with the glossary +| The phrase appears in 17 files outside `archive/`, including this plan: + `CITATION.cff`, `EXPLAINME.adoc`, `EXPLAINME.-new.adoc`, `GLOSSARY.adoc`, + `README.adoc`, `ROADMAP.adoc`, four `docs/` files, `proofs/agda/OND.agda`, + `proofs/observation-models/*`, `proofs/residue/*`. D188 rules "rename" and + approves the two map rows. No replacement term was chosen. +| *Ruled, awaiting a term (Q1).* The Coq, Lean and Isabelle copies are archived + and no longer need changing, apart from historical notes. + +| #171 +| Coq tag grammar and census +| `proofs.yml` ran the Coq assumption gates, the axiom-tag gate and the census. +| *Subject archived.* The Coq gates and the census moved to `archive/proofs/` + with Coq. Close with a receipt that cites the last green `main` run, unless + the owner keeps Coq active (Q10). + +| #170 +| Scorecard: five high alerts +| Job-level token permissions for `publish-container.yml` and `hypatia-scan.yml`. + Alert 508 is the reusable-workflow call. Branch-Floor (`23869372`) has + `non_fast_forward` with no bypass. No owner row for Code-Review (alert 25). + Scorecard fails at its reconcile step on `main`. The code-scanning alert API + returns HTTP 403 to my token, so counts are unverified. +| *Partly landed, blocked on <>.* Owner row needed for alert 25 (<>). + +| #167 +| Lean port of the Coq filesystem model +| `FilesystemCNO.lean` was restored by #177. D124 says "#167 keeps the port". + D204 (2026-09-30, later) says `FilesystemCNO.v` "retires or becomes a toy + instance" and that #167 becomes an abstract CNO interface. D204 asks for a Coq + `Module Type`. +| *Superseded by D204, and now in conflict with the archive (<>, Q2, Q10).* + +| #161 +| `Proofs` is not a gate +| `push` has no `paths:` filter; `pull_request` does. The Z3 step has no `|| true`. + The Coq assumption gates ran with controls. No `coqchk` step existed. +| *Mostly landed; Coq part moot.* Remainder: the always-run change on the active + jobs (D85), and a gate for the Agda and Idris jobs (<>). + +| #81 +| Bustfile runner decision +| `Bustfile.a2ml` was present, with no runner file. `Mustfile.a2ml` required it. + D187 says "drop the Bustfile runner". +| *Changed.* The migration created `contractiles/bust/bust.k9.ncl`, disabled, as + the K9 form of the Bustfile. `must.k9.ncl` probes for it. The old `Mustfile` + check is archived (<>, Q3). + +| #76 +| `contractiles/Justfile` duplicates `Justfile` +| Byte-identical at the recon. +| *Identical again after the sync (working tree).* The duplication is still a + template-level ruling (Q4). + +| #70 +| Proof-debt triage +| The 2026-05-30 comment assessed four quick-win candidates as not tractable, and + recommends deferral. It cites `docs/proof-debt-triage.md`, which is + `docs/proof-debt-triage.adoc` on disk. Five `believe_me` sites in `src/abi`. +| *Premise stale. Most candidates are Coq, and Coq is archived.* Defer, or close + as moot (Q5). + +| #27 +| Idris 2 postulates in `Layout.idr` +| The unsound postulate `alignmentMatchesPlatformWord` is deleted. Five + `believe_me` sites remain. No CI job built the ABI. +| *Premise changed.* A CI build exists in the working tree (`idris` job, not + run). The live issue is the `believe_me` sites and the advisory-only count + (<>). +|=== + +== Tensions and contradictions + +Record these in the estate tension register (`KNOWN-TENSIONS.adoc`) or in the +owner's decision list. None is fixed by a local edit. + +[[t1]] +=== T1 — Proof-assistant policy (contradiction, narrowed) + +* `LANGUAGE-POLICY.adoc` v1.6.0: "Idris2 is the only formal-verification + language. ATS2 is rejected." +* `.claude/CLAUDE.md` (standards) lists Agda as a formal-verification tool, used + by echo-types. +* `0-canon/rsr/TIERS.adoc` names "Formal verification (SPARK, Coq, Isabelle)" in + its Rhodium list. +* *Owner ruling 2026-10-10:* absolute-zero's active stack is Idris 2 and Agda, + with Z3 as a bounded-check solver (not a proof assistant). Coq, Lean 4, + Isabelle/HOL and Mizar are archived. + +*Still open:* Agda is not in LANGUAGE-POLICY's list, and TIERS still names Coq and +Isabelle. *Why it matters:* the constitution requires a full exception record, or +a policy change through the change procedure. *Action:* standards ruling (<>). + +[[t2]] +=== T2 — A2ML retirement vs. the criteria file (contradiction, estate-level) + +`rsr-criteria-v2.a2ml` (2.1.0-draft) still names `.a2ml` descriptiles in its +gates. `AGENTS.adoc` and `CLAUDE.md` retired A2ML. *Action:* standards +maintainers, not this repo. + +[[t3]] +=== T3 — Template `.coderabbit.yaml` vs. D217 (architectural tension) + +The template enables `finishing_touches.docstrings` under `reviews:`. D217 says +CodeRabbit commit-pushing is off. The repo's `.coderabbit.yaml` now disables it, +using the same key placement as the template. Whether the key placement is +fully valid is still open: the schema's first chunk confirms `reviews` only. +*Action:* check the rest of CodeRabbit's live schema before the template is +changed. The template fix belongs upstream. + +[[t4]] +=== T4 — D124 vs. D204 for #167 (superseded ruling) + +D124 and D204 are both dated 2026-09-30. D204 is the later ruling, and it +rescopes #167. The 1:1 Lean port is what D124 kept. *Action:* the owner confirms +which governs (<>). The later ruling should govern unless the owner says +otherwise. T7 now adds the archive. + +[[t5]] +=== T5 — "Drop the Bustfile runner" vs. the canonical six-set (changed) + +D187 can mean "delete the Bustfile declaration" or "stop the runner and keep the +declaration disabled". The working tree now has `contractiles/bust/bust.k9.ncl`, +which the must contract's `contractiles-k9-complete` probe requires. Deleting it +breaks that probe, and the old flat-file check is archived with the Mustfile. +*Action:* <>. + +[[t6]] +=== T6 — Scorecard is a required code-scanning tool with no analysis on `main` (live risk) + +D85(b) keeps Scorecard in the `code_scanning` rule of ruleset `18110203` until +#168's analyses are restored. The Scorecard job on `main` fails at its reconcile +step. A rule that waits for a tool's results cannot be satisfied if the tool +produces none. I have not confirmed a blocked PR. *Action:* check the first PR +after the fix. Treat any block as a symptom of <>. + +[[t7]] +=== T7 — Archived Coq vs. D204's Coq CNO interface (contradiction, new) + +D204 asks absolute-zero to factor out an abstract CNO interface as a Coq +`Module Type`, so that valence-shell can import it. The owner's 2026-10-10 ruling +archives Coq. The two cannot both hold as written. Options are in <>. +*Action:* owner ruling. Do not write the interface until it is made. + +== Per-issue plans + +[[i182]] +=== #182 — CodeRabbit unsigned bot commits + +*Problem.* A bot commit on a PR branch is unsigned, and the signed-commit floor +(D215, D216) rejects it. + +*Plan.* + +. *Owner, app-level:* in CodeRabbit's organisation settings for this repo, turn + off autofix, committable suggestions, "Commit to this branch", Autopilot, and + any docstring generation that commits to the branch. This implements D217. + Confirm first (<>). +. *Repo (done in working tree):* `.coderabbit.yaml` with the docstring finishing + touch disabled. Its comment does not cite a signing-policy file that does not + exist in this repo. It names the estate floor and D217 only. +. *Positive control:* open a throwaway PR where CodeRabbit makes a suggestion. + Confirm no bot commit appears in `pulls/N/commits`, and that every commit + reports `verification.verified == true`. +. *Do not* add CodeRabbit to a required check. + +*Acceptance (revised).* + +* AC1: no bot commit on any PR branch of this repo, shown by the positive control. +* AC2: CodeRabbit accepts the `.coderabbit.yaml` with no config-error comment. +* AC3: every commit on every PR head is signed. +* AC4: no PR is blocked on signatures by a bot commit for 30 days. + +*Size:* S. + +[[i175]] +=== #175 — "residue list" terminology + +*Problem.* "Residue" already has a sense in the estate glossary and in numerical +work (residual). OND's "residue list" is a third sense: out-of-scope observables. + +*Plan.* After <> is answered: + +. One mechanical PR renames the phrase in prose, comments and asciidoc, in the + 17 active files. It also renames `proofs/residue/` and `*.residue` to match, + with a link check. Archived files keep their wording as history. +. Add a one-line fence to `GLOSSARY.adoc` for the new term, stating the sense it + does not have. +. Do not touch proof logic. Re-run the Agda and Idris jobs, since comments change. +. Register the approved map rows with `nextgen-typing` (cross-repo; D188 + approved them). + +*Acceptance (revised).* + +* AC1: grep for the old phrase finds nothing outside history and `archive/`. +* AC2: the new term has a glossary fence in the same PR. +* AC3: the proof workflow is green after the change. + +*Size:* S, mechanical. + +[[i171]] +=== #171 — Coq axiom tags and census + +*Plan.* The Coq gates and census are archived with Coq. Close with a receipt that +cites the last green `main` run that included them, and a pointer to +`archive/proofs/`. The 73-theorem triage is Coq work, so it is moot while Coq is +archived. If the owner reopens Coq (Q10), the advisory-to-gate step and the triage +return with it, and both must be re-scoped. + +*Acceptance (revised).* Closed with a receipt, or re-scoped under Q10. + +*Size:* S to close. + +[[i170]] +=== #170 — Scorecard high alerts + +*Plan.* + +. Land <> first, so Scorecard runs on `main` and refreshes its alerts. +. Alerts 510 and 509: already fixed in the tree. Confirm they close on the next + analysis. +. Alert 508: dismiss as "won't fix", with a comment that points at the callee's + SARIF upload (`hyperpolymath/standards/.github/workflows/scorecard-reusable.yml` + at `0f13f51`). Keep `security-events: write` at job level, because the callee + needs it. Removing it brings back the startup failure fixed in #169. +. Alert 25 (Code-Review): an owner row on `standards#787` is required. The sole + maintainer cannot approve their own PRs on GitHub, so the honest options are + "waive with reason" or "gate on something else" (<>). +. Alert 1 (Branch-Protection): confirm that Branch-Floor (`23869372`) clears the + force-push finding on the next analysis. + +*Acceptance (revised).* Zero open `high` alerts, or each remaining one is +dismissed with a stated reason. The Scorecard analysis on `refs/heads/main` is +newer than the fix. My token cannot read code-scanning alerts (HTTP 403), so an +owner or CI must confirm the counts. + +*Size:* S, once <> lands. + +[[i167]] +=== #167 — Abstract CNO interface (rescope blocked by T7) + +*Problem.* The issue as written asks for a 1:1 Lean port of the concrete Coq +filesystem model, so that the model's axioms become theorems. D204 (2026-09-30) +says the concrete model "retires or becomes a toy instance". It asks for an +abstract CNO interface, and valence-shell would import it and prove `is_CNO` over +its own model. A 1:1 port would be spent on a model D204 says will retire. + +The owner's archive ruling removes Coq, and D204's interface is a Coq Module Type. +So the rescope has no home until Q10 is answered. + +*Plan (conditional on <> and <>).* + +. If the owner rescopes to an Idris 2 or Agda interface (recommended), rewrite + #167 around that interface. Its deliverable is a module that type-checks in the + active stack, with a witness instance. The cross-repo acceptance (valence-shell + imports it and proves `is_CNO`) goes in valence-shell's issue, not here. +. `FilesystemCNO.lean` is archived with Lean. Its axioms remain audited only in + the archive. Add no new work to it. +. If the owner keeps Coq for this interface (a bounded exception), record it as + an exception under T1, and un-archive only the interface file. + +*Acceptance (rescoped).* The interface type-checks in CI. The retire-or-toy +decision is recorded for `FilesystemCNO`. The cross-repo items are filed in +valence-shell. + +*Size:* M. Cross-repo. + +[[i161]] +=== #161 — Proofs is not a gate + +*Plan.* + +. Make the active Proofs jobs run on `pull_request` and `push`, with an internal + change check that reports success cheaply on PRs touching no proof file. This + is the always-run-with-internal-skip pattern that D85 prescribes. +. Give the Agda and Idris jobs a positive control: a mutant with a type error must + turn them red (<>). +. Only after step 1 is green on a PR that touches no proof file does the owner add + the prover contexts to the ruleset. +. `coqchk` is dropped from this plan. Coq is archived (Q10 can reinstate it). + +*Acceptance (revised).* Proofs runs on every PR and reports success on proof-free +PRs. The Agda and Idris jobs have controls. + +*Size:* M. + +[[i81]] +=== #81 — Bustfile runner + +*Plan.* Depends on <>. + +* *Keep (recommended):* `contractiles/bust/bust.k9.ncl` stays, disabled and + documented, as it is now. The issue closes as "no runner in this repo". Nothing + else changes. +* *Delete:* remove `bust.k9.ncl`, and update `must.k9.ncl`'s + `contractiles-k9-complete` probe from six files to five, in the same PR. This + diverges from the canonical INDEX. + +*Acceptance.* The chosen state, with a green `k9-validate` run on the contracts. + +*Size:* S. + +[[i76]] +=== #76 — `contractiles/Justfile` duplicates `Justfile` + +*Plan.* No further local change until the template ruling (<>). The two copies +were re-synced in the working tree, so they stay identical. If the owner says "by +design", close as by-design. If the template pointerises or removes its copy, +follow it here at the next template sync. Any edit to one copy must edit both. + +*Size:* S, blocked. + +[[i70]] +=== #70 — Proof-debt triage + +*Plan.* Recommended: defer, or close as moot. The 2026-05-30 comment already +recommends deferral. Most candidates were Coq DISCHARGE items, and Coq is archived. +Fold the five `believe_me` sites into #27. Correct the body's path (`.md` to `.adoc`) +and its site count (five code sites in `src/abi`), if the issue stays open. + +*Size:* S, to close or defer. + +[[i27]] +=== #27 — Idris 2 `believe_me` in the ABI proofs + +*Problem.* The unsound postulate is gone. Five `believe_me` sites remain in +`src/abi`. RSR's draft criterion 5.2.2 forbids `believe_me` in load-bearing proofs. +The count is printed by the `idris` job, but only as an advisory. Nothing stops a +sixth. + +*Plan.* + +. <> first: run the `idris` job on `main` and confirm it is green. Its + image is the one `pages.yml` already pins by digest. +. A discharge spike for `programStateAlignmentValid`. The 2026-05-30 comment on + #70 says it is blocked by Idris 2 0.8.0's non-reduction of `mod`. Test that claim + before relying on it, for example by a case-split on `Platform`. +. The `DivMod.idr` lemmas: discharge them if the spike works. If Idris 2 cannot + reduce them, record the sites in the known-limitations register, labelled + *assumed*, with the reason and an exit (an Idris upgrade). Do not describe them + as proven. +. Turn the `believe_me` count into a gate with a positive control (<>). + +*Acceptance (revised).* The ABI builds in CI. A grep gate on `believe_me` in +`src/abi` (excluding comments) has a positive control. The count is zero, or each +residual site is in the known-limitations register with the required fields. + +*Owner input:* <>, <>. *Size:* M to L, depending on the spike. + +== New issues to file (proposed, not filed) + +[[n1]] +=== N1 (P0) — `actions.lock` drift turns `main` red + +*Evidence (measured, recon).* + +[cols="1,2,2",options="header"] +|=== +| Entry | Workflow `uses:` | `actions.lock` records + +| `hyperpolymath/smtp-notify-action` +| `@c1c9fa0` (v0.5.0), bumped by #186, merged 2026-10-09 +| `@22e7bdb` (v0.3.0) + +| `github/codeql-action` +| `init` and `analyze` at `@v4.38.2`, bumped by #185, merged 2026-10-02 +| `@v4.38.1` +|=== + +The three `main` reds all involve the lock. Governance fails its `Verify +actions.lock` job. Scorecard fails `Fail if reconciliation did not succeed` after +`Reconcile native action pins`. CodeQL fails with a startup failure. The job-log +download returns EOF, so this is a strong inference from step names and the +comparison, not a log-confirmed cause. + +*Plan (per D220).* Regenerate the lock in a fresh clone with +`standards/scripts/update-actions-lock.sh`, which D220 names. Land the regenerated +lock. Regenerate lock entries for Dependabot bumps with `regen-dependabot-locks.sh`. +Add the estate's lock-sync gate to CI (`lock-sync-gate.yml` in the template). It +needs `gawk`, which the runner must install. The local `scripts/check-lock-sync.sh` +exits "FATAL: needs gawk" here, so I could not run it. + +*Acceptance.* Governance, Scorecard and CodeQL are green on `main`. The lock matches +the `uses:` set. The next Dependabot bump either regenerates the lock or is blocked +by the gate. + +*Size:* S. *Owner input:* none. D220 already rules this arm. + +[[n2]] +=== N2 (P1) — A2ML to deed and K9 migration (mostly done, uncommitted) + +*Evidence (measured).* Recon: 20 `.a2ml` files and zero `.deed`. Working tree: +0 tracked `.a2ml`; 20 sources in `archive/a2ml-v1/`; `absolute-zero_chora.deed`; +six K9 contracts; `coordination.k9`; `.claude/CLAUDE.md` artefact section updated. + +*Done (working tree).* Migration per D99, D269c, D312 and D313. Contracts follow +the standard's leash and authority per verb. Every unmapped field is recorded in +the ledger. The ledger lists IDs (C-1 to CO-2) that the K9 headers cite. + +*Still open.* + +* Nickel L2 validation of the six K9 files has not run (no binary; blocked). +* `must`, `trust`, `bust` and `intend` fail `K9-S009` only. The unsigned pedigree + (K-1) is the expected cause, not re-verified. These are Hunt contracts, which + need owner signing before they can run. +* The K9 `author` email is unverified against the template. +* ADR entries have no dates (ledger M-2). Owner or ADR history must supply them. +* The `coordination.k9` generator was not run, because it imports from `jsr:`. +* The README in `archive/` and the three `.machine_readable` READMEs are + notice-only. Full rewrites are a follow-up. + +*Acceptance.* Zero tracked `.a2ml`. A `_chora.deed` that passes the template's +`deed-validate.yml` (not yet run). Coordination in `coordination.k9`. `.claude/CLAUDE.md` +no longer names A2ML (done). + +*Owner input:* <>, <>. *Size:* remaining S, plus signing. + +[[n3]] +=== N3 (P2) — Record the proof-assistant contradiction (T1, narrowed) + +Add a `KNOWN-TENSIONS` entry in standards for Agda and for the TIERS naming, and an +exception record or policy change for absolute-zero, after <>. This is an +estate-level change, so the constitutional change procedure applies. + +*Size:* S to record; L to resolve. + +[[n4]] +=== N4 (P2) — The ABI is never built in CI (addressed in working tree, not run) + +The working tree adds the `idris` job to `proofs.yml`. It builds +`absolute-zero-abi.ipkg` on the pinned image and prints the `believe_me` count. It +has no positive control, and it has not run. `src/abi` was type-checked only by the +local gate before this. + +*Acceptance.* The job is green on `main`, and the control is red on a mutant. + +*Size:* S for the control. + +[[n5]] +=== N5 (P2) — Container base and dead interpreter references + +*Evidence (measured).* `Containerfile` line 12: `FROM registry.fedoraproject.org/fedora:39`. +Lines 131–132 run `chmod +x interpreters/...`, and the comments around line 222 run +`python3 interpreters/brainfuck/brainfuck.py`. `interpreters/` does not exist. The +`coqc` build lines were removed in the working tree. + +*Plan.* Move to a Wolfi-style base. Remove the Python and `interpreters/` +references. Confirm the `publish-container` build still produces its attestation. + +*Size:* M. + +[[n6]] +=== N6 (P3) — `language-policy.yml` enforces a stale policy + +*Evidence (measured).* The workflow still exempts "salt". The SaltStack exception +was removed on 2026-01-03 (LANGUAGE-POLICY v1.6.0). It checks only added files +(`--diff-filter=A HEAD~1`), so an existing banned file is never seen. + +*Plan.* Replace it with the estate's reusable gate. The template ships +`estate-rules.yml` and `runtime-policy.yml`. + +*Size:* S. + +[[n7]] +=== N7 (P3) — Refresh local policy docs + +`RSR_COMPLIANCE.adoc` (dated 2026-05-25) predates the A2ML, signing and +proof-assistant rulings. `.claude/CLAUDE.md` artefact section is updated; the rest +of that file is not reviewed. Refresh both from the canon, and cite the canon as +the source. + +*Size:* S. + +[[n8]] +=== N8 (P3) — RSR shape gaps (guidance, against a draft) + +* No `guix.scm`. `manifest.scm` is present. The canon's criterion 8.1.4 (draft) + rejects a scaffold-stub `guix.scm`, so the approach needs an owner decision, + not a stub. +* No `.tool-versions`. `mise.toml` is present. +* Actions are pinned by tag (23 `uses:` references) and held by the lock file, not + by SHA in the `uses:` line. Criterion 4.1.3 (draft) says SHA-pinned. Decide with + the estate which form counts. + +*Size:* M. Mostly guidance. Treat the criteria as draft. + +[[n9]] +=== N9 (P3) — Ruleset 18110203 allows merge and rebase methods + +*Evidence (measured).* Ruleset `18110203` lists `allowed_merge_methods`: `squash`, +`rebase`, `merge`. The repo settings have merge commits and rebase merges off. +D89 and D216 require squash only where signatures are required. + +*Plan.* Align the ruleset to squash-only, after confirming the owner's intent. + +*Size:* S. + +[[n10]] +=== N10 (P1) — Migration verification gaps (new) + +Things the migration claims that have not been checked: + +* Nickel L2 for the six K9 files. Not run. +* The template's `deed-validate.yml` against `absolute-zero_chora.deed`. Not run; + only the local copy of the linter was run. +* The four Hunt contracts. Signing is an owner act. +* `.coderabbit.yaml` against CodeRabbit's full schema. + +*Plan.* Run each check where the tools exist (CI, or the owner's machine), and +record the result in the ledger. Do not mark the migration verified until they pass. + +*Size:* S. + +[[n11]] +=== N11 (P2) — Proof gates for the active stack (new) + +* `proofs/verify-active-provers.sh` has no self-test. The archived six-prover + self-test was removed from the z3 job with no replacement. A replacement must + stub the tools and show the gate turn red. +* The Agda and Idris jobs have no positive control. +* The `believe_me` count is advisory (<>). + +*Plan.* Write a self-test for the active gate, with stubs for `agda`, `z3` and +`idris2`. Add a mutant control for each. Make the `believe_me` count a gate once +#27's sites are discharged or recorded. + +*Size:* S for the self-test; M for the controls. + +[[n12]] +=== N12 (P3) — Containerfile apt `coq` package (new) + +The apt layer still installs `coq`, although the `coqc` build lines were removed. +Remove the package with the rest of the Coq toolchain, once the owner has ruled +(Q10). Otherwise the image keeps a dead dependency. + +*Size:* S. + +== Owner decisions {#owner-decisions} + +Each has a recommended default. Nothing is taken without an answer. + +[[q1]] +*Q1 (#175) — replacement term for "residue list".* Options: `exclusion list` (the +issue's first suggestion), `boundary list`, `out-of-scope list`. *Recommended: +`exclusion list`.* I did not check the estate glossary (in `nextgen-typing`) for +collisions with the chosen term. Check before the rename. + +[[q2]] +*Q2 (#167) — which ruling governs?* (a) D204: rescope to an abstract CNO +interface, and stop the 1:1 Lean port. *Recommended,* in an Idris 2 or Agda form +(see Q10). (b) D124: keep the port (archived; would need Q10 first). + +[[q3]] +*Q3 (#81) — what does "drop the Bustfile runner" mean?* (a) Keep +`bust.k9.ncl` disabled; close as "no runner in this repo". *Recommended; it matches +the canonical six-set.* (b) Delete `bust.k9.ncl` and update the `must` probe. + +[[q4]] +*Q4 (#76) — the template duplicate.* (a) By design: keep the copy in both, and close +#76. (b) The template pointerises, and absolute-zero follows. (c) Remove the copy +from both. *Recommended: (a) now, with (b) as a later template task.* + +[[q5]] +*Q5 (#70 / #27) — the Idris and Coq debt.* (a) Defer or close #70 as moot; re-scope +#27 to the five `believe_me` sites, with the `idris` job green first. *Recommended.* +(b) Approve a multi-hour spike on the Idris side now. + +[[q6]] +*Q6 (#170 alert 25) — Code-Review.* (a) Waive with a recorded reason on +`standards#787`. `required_approving_review_count` is 0 on `18110203`, and the sole +maintainer cannot approve their own PRs. *Recommended.* (b) Gate the metric with a +second reviewer, which cannot be satisfied today. + +[[q7]] +*Q7 (T1) — proof assistants, after the 2026-10-10 ruling.* The ruling settles the +active stack. Still open: whether Agda is added to LANGUAGE-POLICY, and whether +TIERS is corrected. (a) Amend LANGUAGE-POLICY to list Agda, with a dated +rationale. *Recommended.* (b) Keep LANGUAGE-POLICY as Idris 2 only, and record +Agda as an exception for absolute-zero, with containment and expiry. (c) Ask the +constitutional authority to settle the policy text first. + +[[q8]] +*Q8 (N2) — how to land the migration.* (a) One squash PR, after <> passes. +*Recommended.* (b) Three PRs: archive, deed, K9. Each would need its own signed +cherry-pick. + +[[q9]] +*Q9 (#182) — the CodeRabbit app setting.* Confirm that D217's setting is applied to +this repo in the CodeRabbit app. I cannot see it from here. If it is not applied, +apply it before any repo change is merged. + +[[q10]] +*Q10 (T7, #167, #171, #70, N12) — Coq after the archive. Owner choice 2026-10-10: (b).* (a) Keep Coq archived. +D204's interface is rescoped to Idris 2 or Agda (Q2a). Retire the Coq apt package. +*Recommended.* (b) *Chosen.* Un-archive only the abstract CNO interface as a bounded Coq +exception, with containment and expiry. Not yet done: no interface file exists +yet, and the exception record is still to be written under T1. (c) Ask standards +to amend D204. + +[[q11]] +*Q11 (N2, N10) — signing the Hunt contracts.* The four Hunt contracts (must, trust, +bust, intend) need an owner signature before they can run as Hunt (K-1). Options: +(a) the owner signs them locally, and the signed commit goes in the migration PR. +*Recommended.* (b) Keep them as declarations until a later PR signs them. In that +case they stay disabled. + +== Sequencing + +[cols="1,3,3,2",options="header"] +|=== +| Wave | Work | Exit criteria | Gate + +| 0 — restore `main` +| N1 +| Governance, Scorecard and CodeQL green on `main`. Lock matches the `uses:` set. +| Owner merge. Squash only. + +| 1 — decide +| Q1–Q11 +| Each answer recorded as a row on `standards#787`, naming the surface it governs. +| Owner + +| 2 — land what is in the tree +| The proof-stack archive and the active gate (one PR, after N11's self-test); + the migration (Q8); `.coderabbit.yaml` (after Q9) +| Each PR: signed commits, rule-suite `pass`, positive control where the issue + asks for one. +| Squash auto-merge when every rule passes (D87). No bypass. + +| 3 — small PRs +| #182 (S); #175 (S, after Q1); #81 and #76 (after Q3/Q4); #161 always-run (M); + #170 dismissals (after N1); #171 close; #70 close or defer; N9 (S); N12 (S, after + Q10) +| As above. +| As above. + +| 4 — proofs and ABI +| N4 (run the `idris` job on `main`), then the #27 spike, then #167 rescoped to + the interface (after Q10) +| ABI green in CI. Zero `believe_me` in `src/abi`, or known limitations recorded. + Abstract interface type-checks. +| Owner, for the Idris version and the T1 and T7 decisions + +| 5 — hygiene +| N5 (container), N6 (language gate), N7 (docs), N8 (criteria), N10 (migration + checks) +| Container on a Wolfi-style base. Stale gate retired. Docs match canon. +| Owner for N10 and N5 timing + +| 6 — estate (not this repo) +| T2; T3 (template `.coderabbit.yaml`); the template `Justfile` (Q4); the N3 tension + record +| Entries in standards and in the template. +| Standards and template maintainers +|=== + +== Verification protocol + +For every PR in this plan: + +. Run the local gate that exists for the area. For the active stack: + `proofs/verify-active-provers.sh` (needs `agda`, `z3` and `idris2` on the path). + `proofs/z3/verify.sh` runs alone. The archived gates are in `archive/proofs/` and + are not run. +. For the migration: `k9-validate.sh --strict` (standards) on each K9 file, the + template's `deed-validate.yml` on the deed, and a Nickel L2 run when a binary is + available. +. For YAML: parse each changed workflow and `.gitlab-ci.yml` (the sandbox used + js-yaml from npm). +. For the Justfile copies: `cmp Justfile .machine_readable/contractiles/Justfile`. +. After merge, check `gh run list --branch main` for the fix commit, and confirm + each workflow the PR touched has `jobs > 0`. +. Check signatures: `gh api repos/.../pulls/N/commits`, and each commit's + `verification.verified`. +. Check that the ruleset rule-suite entry reads `pass`. Do not use a bypass merge. +. Check the grep counts named in the acceptance criteria (`believe_me`, the old + residue phrase, `.a2ml`). + +== Limits of this recon + +* *Code-scanning alerts:* HTTP 403 with this token. Alert counts are unverified. +* *Job logs:* the download returns EOF. Root causes are inferred from step names and + from comparing `actions.lock` with the workflow `uses:` lines. +* *Provers:* Agda, Z3, Idris 2 and the archived provers are not installed here. The + active gate fails closed in this sandbox. CI status on `main` is the evidence for + prover claims, and CI status is not proof. +* *Nickel:* no binary. The release download and npm packages are blocked. L2 is not run. +* *CodeRabbit:* app settings are not visible. Key placement is partly checked (T3). +* *Standards:* shallow clones. RSR criteria are draft (2.1.0-draft, 2026-09-19). + `/tmp` is not persistent across sessions. +* *Issue bodies* in some cases describe an older tree. Where a comment contradicts a + body, I followed the comment and the code. + +[[do-not]] +== Do-not list + +* Do not force-push a PR branch to fix a signature. Use a signed cherry-pick into a + new PR. +* Do not bypass-merge. Use squash auto-merge, and read the rule-suite entry (D87). +* Do not create or extend an `.a2ml` file. Do not add TypeScript, Deno or Python. +* Do not add CodeRabbit to a required check (D86). +* Do not sweep licence headers in bulk. Do not change a licence file without owner + approval. +* Do not describe a `believe_me`, an axiom, a draft criterion or a passing CI run as + "proven". +* Do not un-archive Coq, Lean, Isabelle or Mizar without Q10 (or the owner's + equivalent ruling). +* Do not run the standards generator for `coordination.k9`. It imports from `jsr:`. +* Do not file, close or edit issues or rulesets from this plan without the owner's + go-ahead. + +== Evidence commands + +The recon used read-only commands. Reproduce with: + +[source,bash] +---- +gh issue list --repo hyperpolymath/absolute-zero --state all --limit 100 +gh issue view --repo hyperpolymath/absolute-zero --json title,body,labels,comments +gh api repos/hyperpolymath/absolute-zero/rulesets/18110203 +gh api repos/hyperpolymath/absolute-zero/rulesets/23869372 +gh run list --repo hyperpolymath/absolute-zero --branch main --limit 12 +gh api repos/hyperpolymath/standards/issues/787/comments --paginate +grep -rn 'believe_me' src --include=*.idr +grep -rli 'residue list' --exclude-dir=.git --exclude-dir=archive . +grep -rhoE 'uses: *[^ #]+' .github/workflows/*.yml +cmp Justfile .machine_readable/contractiles/Justfile +bash proofs/verify-active-provers.sh +---- diff --git a/proofs/verify-active-provers.sh b/proofs/verify-active-provers.sh new file mode 100755 index 0000000..e554a87 --- /dev/null +++ b/proofs/verify-active-provers.sh @@ -0,0 +1,43 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Absolute Zero — reproduce the ACTIVE machine-checked verification. +# +# Owner ruling 2026-10-10: the active proof stack is Idris 2 (ABI) and Agda +# (CNO + OND). Z3 remains as bounded, expect-annotated checks. Coq, Lean 4, +# Isabelle/HOL and Mizar are retired from the active gate; their trees and their +# six-prover gate are archived under archive/proofs/ (see archive/README.adoc). +# +# Every active prover is REQUIRED: an absent toolchain is a failure, never a skip. +# Needs on PATH: agda, z3, idris2. The Agda standard library is registered via +# ~/.agda/libraries (see .github/workflows/proofs.yml for the pinned setup). +set -uo pipefail +export PATH="$HOME/.local/bin:$HOME/.elan/bin:$PATH" +HERE="$(cd "$(dirname "$0")" && pwd)" +fail=0 +say() { printf '\n\033[1m== %s ==\033[0m\n' "$1"; } + +# ---- Agda (CNO + OND + EchoBridge) ---------------------------------------- +say "Agda — CNO + OND + EchoBridge" +if command -v agda >/dev/null; then + ( cd "$HERE/agda" && for m in CNO OND EchoBridgeScaffold EchoBridgeCNO; do + [ -f "$m.agda" ] || { echo "$m.agda MISSING"; exit 1; } + echo "checking $m"; agda --safe --without-K "$m.agda" || exit 1 + done ) || { echo "AGDA FAILED"; fail=1; } +else echo "agda missing"; fail=1; fi + +# ---- Z3 (bounded instances, expect-checked) -------------------------------- +say "Z3 — expect-checked bounded instances (proofs/z3/verify.sh)" +if command -v z3 >/dev/null; then + bash "$HERE/z3/verify.sh" || { echo "Z3 FAILED"; fail=1; } +else echo "z3 missing"; fail=1; fi + +# ---- Idris 2 (ABI boundary) ------------------------------------------------ +say "Idris 2 — ABI" +if command -v idris2 >/dev/null; then + ( cd "$HERE/.." && idris2 --build absolute-zero-abi.ipkg ) \ + || { echo "IDRIS FAILED"; fail=1; } +else echo "idris2 missing"; fail=1; fi + +echo +if [ "$fail" -eq 0 ]; then echo "ACTIVE-PROVERS-GREEN"; else echo "SOME ACTIVE PROVERS FAILED"; fi +exit "$fail" diff --git a/proofs/z3/verify.sh b/proofs/z3/verify.sh index 02bd2a0..5e47d68 100755 --- a/proofs/z3/verify.sh +++ b/proofs/z3/verify.sh @@ -14,7 +14,7 @@ # Before 2026-09-23 this script ran `z3 cno_properties.smt2` (a file that did # not exist), CI wrapped it in `|| true`, and the only other check was z3's # exit code — which is 0 for sat AND unsat, so a broken theorem never failed. -# Self-test (mutants that must turn this red): proofs/tests/gate-selftest.sh. +# Self-test: the archived six-prover self-test (archive/proofs/tests/) no longer covers this gate; a replacement is open (ULTRAPLAN N11). set -uo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" ROOT="${1:-$HERE}" From 1ffc68a84e47ded4e2cb2235e8cff32dd87c507a Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Sat, 10 Oct 2026 20:17:54 +0000 Subject: [PATCH 2/3] test(proofs): add active prover gate self-tests and Z3 checker integration coverage --- proofs/tests/gate-selftest.sh | 235 ++++++++++++++++++++++++++++++++++ 1 file changed, 235 insertions(+) create mode 100644 proofs/tests/gate-selftest.sh diff --git a/proofs/tests/gate-selftest.sh b/proofs/tests/gate-selftest.sh new file mode 100644 index 0000000..2b207b5 --- /dev/null +++ b/proofs/tests/gate-selftest.sh @@ -0,0 +1,235 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Unit tests for verify-active-provers.sh, plus its Z3 checker integration. +# Run: bash proofs/tests/gate-selftest.sh (no real provers or network needed). +# All mutations are confined to a disposable fixture; archived proofs are unused. +set -euo pipefail + +HERE="$(cd "$(dirname "$0")" && pwd)" +PROOFS="$(cd "$HERE/.." && pwd)" +BASH_BIN="$(command -v bash)" +ENV_BIN="$(command -v env)" +SCRATCH="$(mktemp -d "${TMPDIR:-/tmp}/az-active-gate-selftest.XXXXXX")" +trap 'rm -rf "$SCRATCH"' EXIT +# Spaces exercise quoting in the gate's path resolution and subprocess calls. +FIXTURE="$SCRATCH/repo with spaces" +STUB="$SCRATCH/bin" +TRACE="$SCRATCH/trace" +mkdir -p "$STUB" "$SCRATCH/home" "$SCRATCH/unrelated cwd" "$FIXTURE/proofs" +cp "$PROOFS/verify-active-provers.sh" "$FIXTURE/proofs/" + +# No system PATH fallback: missing-prover cases must stay missing even on a +# developer's machine with all provers installed. Only checker utilities escape. +for utility in bash dirname find sort awk grep diff sed tail tr; do + ln -s "$(command -v "$utility")" "$STUB/$utility" +done + +cat > "$STUB/agda" <<'AGDA' +#!/bin/sh +printf 'agda|%s|%s\n' "$PWD" "$*" >> "$TRACE" +[ "$#" -eq 3 ] && [ "$1" = --safe ] && [ "$2" = --without-K ] || exit 90 +[ -f "$3" ] || exit 91 +[ "$3" != "$AGDA_FAIL" ] || exit 7 +AGDA +cat > "$STUB/idris2" <<'IDRIS' +#!/bin/sh +printf 'idris2|%s|%s\n' "$PWD" "$*" >> "$TRACE" +[ "$#" -eq 2 ] && [ "$1" = --build ] && [ "$2" = absolute-zero-abi.ipkg ] || exit 90 +[ -f "$2" ] || exit 91 +exit "$IDRIS_RC" +IDRIS +cat > "$STUB/z3" <<'Z3' +#!/bin/sh +printf 'z3|%s|%s\n' "$PWD" "$*" >> "$TRACE" +[ "$#" -eq 1 ] || exit 90 +if [ "$1" = --version ]; then + echo 'Z3 version stub' + exit 0 +fi +[ -f "$1" ] || exit 91 +printf '%s\n' "$Z3_OUTPUT" +exit "$Z3_RC" +Z3 +# Retirement is a behavior: even available archived tools must never be called. +for retired in coqc coq_makefile make lake lean isabelle accom verifier; do + cat > "$STUB/$retired" <<'RETIRED' +#!/bin/sh +printf 'ARCHIVED TOOL CALLED: %s\n' "$0" >> "$TRACE" +exit 99 +RETIRED +done +chmod +x "$STUB/"{agda,idris2,z3,coqc,coq_makefile,make,lake,lean,isabelle,accom,verifier} + +MODULES=(CNO OND EchoBridgeScaffold EchoBridgeCNO) +cases=0 +fails=0 + +reset_fixture() { + local module + rm -rf "$FIXTURE/proofs/agda" "$FIXTURE/proofs/z3" + mkdir -p "$FIXTURE/proofs/agda" "$FIXTURE/proofs/z3/ond" + for module in "${MODULES[@]}"; do + cp "$PROOFS/agda/$module.agda" "$FIXTURE/proofs/agda/" + done + cp "$PROOFS/z3/verify.sh" "$FIXTURE/proofs/z3/" + cp "$PROOFS/../absolute-zero-abi.ipkg" "$FIXTURE/" + # The solver is stubbed, so a small annotated fixture is sufficient to test + # the gate/checker boundary without coupling it to theorem contents. + printf '(check-sat) ; expect sat\n(check-sat) ; expect unsat\n(check-sat) ; expect sat\n' \ + > "$FIXTURE/proofs/z3/ond/checks.smt2" + AGDA_FAIL='' + IDRIS_RC=0 + Z3_RC=0 + Z3_OUTPUT=$'sat\nunsat\nsat' + EXPECTED='' +} + +expect_agda() { + local module + for module in "$@"; do + EXPECTED+="agda|$FIXTURE/proofs/agda|--safe --without-K $module.agda"$'\n' + done +} +expect_z3() { + EXPECTED+="z3|$SCRATCH/unrelated cwd|--version"$'\n' + EXPECTED+="z3|$SCRATCH/unrelated cwd|$FIXTURE/proofs/z3/ond/checks.smt2"$'\n' +} +expect_idris() { + EXPECTED+="idris2|$FIXTURE|--build absolute-zero-abi.ipkg"$'\n' +} +expect_all() { expect_agda "${MODULES[@]}"; expect_z3; expect_idris; } + +run_gate() { + : > "$TRACE" + RC=0 + # A clean child environment also removes exported shell functions, BASH_ENV, + # user-local toolchains, and legacy skip flags from the host test environment. + OUT="$(cd "$SCRATCH/unrelated cwd" && "$ENV_BIN" -i \ + HOME="$SCRATCH/home" PATH="$STUB" LC_ALL=C TRACE="$TRACE" \ + AGDA_FAIL="$AGDA_FAIL" IDRIS_RC="$IDRIS_RC" Z3_RC="$Z3_RC" Z3_OUTPUT="$Z3_OUTPUT" \ + "$BASH_BIN" "$FIXTURE/proofs/verify-active-provers.sh" 2>&1)" || RC=$? +} + +# Require the specific failure diagnostic AND final status AND exact tool +# invocations: an unrelated shell error must never satisfy a negative case. +expect() { + local label=$1 want=$2 reason problem='' actual + shift 2 + cases=$((cases + 1)) + [ "$RC" -eq "$want" ] || problem+="exit $RC, wanted $want; " + for reason in "$@"; do + [[ "$OUT" == *"$reason"* ]] || problem+="missing '$reason'; " + done + if [ "$want" -eq 0 ]; then + [[ "$OUT" == *ACTIVE-PROVERS-GREEN ]] || problem+='missing green summary; ' + [[ "$OUT" != *'SOME ACTIVE PROVERS FAILED'* ]] || problem+='failure on success; ' + else + [[ "$OUT" == *'SOME ACTIVE PROVERS FAILED' ]] || problem+='missing failure summary; ' + [[ "$OUT" != *ACTIVE-PROVERS-GREEN* ]] || problem+='false green; ' + fi + actual="$(cat "$TRACE")" + [[ "$actual" == "${EXPECTED%$'\n'}" ]] || problem+='tool calls differ; ' + if [ -z "$problem" ]; then + printf 'PASS: %s\n' "$label" + else + fails=$((fails + 1)) + printf 'FAIL: %s — %s\n%s\nExpected calls:\n%sActual calls:\n%s\n' \ + "$label" "$problem" "$OUT" "$EXPECTED" "$actual" + fi +} + +reset_fixture; expect_all; run_gate +expect 'all active provers pass; archived tools unused; cwd and flags correct' 0 'Z3-CHECK OK' + +for tool in agda z3 idris2; do + reset_fixture + mv "$STUB/$tool" "$SCRATCH/$tool.off" + if [ "$tool" != agda ]; then expect_agda "${MODULES[@]}"; fi + if [ "$tool" != z3 ]; then expect_z3; fi + if [ "$tool" != idris2 ]; then expect_idris; fi + run_gate + expect "$tool missing fails while other provers still run" 1 "$tool missing" + mv "$SCRATCH/$tool.off" "$STUB/$tool" +done + +reset_fixture +for tool in agda z3 idris2; do mv "$STUB/$tool" "$SCRATCH/$tool.off"; done +run_gate +expect 'all missing provers are reported together' 1 'agda missing' 'z3 missing' 'idris2 missing' +for tool in agda z3 idris2; do mv "$SCRATCH/$tool.off" "$STUB/$tool"; done + +for index in "${!MODULES[@]}"; do + module=${MODULES[$index]} + reset_fixture + AGDA_FAIL="$module.agda" + expect_agda "${MODULES[@]:0:index+1}"; expect_z3; expect_idris + run_gate + expect "$module rejects: stop Agda at that module, continue other provers" 1 'AGDA FAILED' + + reset_fixture + rm "$FIXTURE/proofs/agda/$module.agda" + expect_agda "${MODULES[@]:0:index}"; expect_z3; expect_idris + run_gate + expect "$module missing: never invoke Agda on a missing module" 1 "$module.agda MISSING" +done + +reset_fixture +rm -rf "$FIXTURE/proofs/agda" +expect_z3; expect_idris; run_gate +expect 'missing Agda directory fails without checking from the wrong cwd' 1 'AGDA FAILED' + +reset_fixture +IDRIS_RC=3 +expect_all; run_gate +expect 'Idris build failure normalizes to gate exit 1' 1 'IDRIS FAILED' + +reset_fixture +rm "$FIXTURE/absolute-zero-abi.ipkg" +expect_all; run_gate +expect 'missing ABI package propagates the build failure' 1 'IDRIS FAILED' + +# These are integration cases for the new gate's delegation to the existing +# expect-checker; a solver exiting zero alone must never make the gate green. +for mode in mismatch unknown error nonzero empty truncated extra; do + reset_fixture + reason='verdicts differ from annotations' + case "$mode" in + mismatch) Z3_OUTPUT=$'sat\nsat\nsat';; + unknown) Z3_OUTPUT=$'sat\nunknown\nsat';; + error) Z3_OUTPUT=$'sat\n(error "boom")\nunsat\nsat'; reason='z3 reported an error';; + nonzero) Z3_RC=4; reason='z3 exit 4';; + empty) Z3_OUTPUT='';; + truncated) Z3_OUTPUT=$'sat\nunsat';; + extra) Z3_OUTPUT=$'sat\nunsat\nsat\nsat';; + esac + expect_all; run_gate + expect "Z3 $mode fails the active gate and still runs Idris" 1 "$reason" 'Z3 FAILED' +done + +reset_fixture +rm "$FIXTURE/proofs/z3/ond/checks.smt2" +expect_agda "${MODULES[@]}" +EXPECTED+="z3|$SCRATCH/unrelated cwd|--version"$'\n' +expect_idris; run_gate +expect 'empty solver fixture cannot pass vacuously' 1 'no .smt2 files' + +reset_fixture +rm "$FIXTURE/proofs/z3/verify.sh" +expect_agda "${MODULES[@]}"; expect_idris; run_gate +expect 'missing delegated checker fails even with z3 available' 1 'Z3 FAILED' + +reset_fixture +AGDA_FAIL=CNO.agda; Z3_RC=4; IDRIS_RC=3 +expect_agda CNO; expect_z3; expect_idris; run_gate +expect 'multiple failures preserve a failing result after every prover runs' 1 \ + 'AGDA FAILED' 'Z3 FAILED' 'IDRIS FAILED' + +reset_fixture; expect_all; run_gate +expect 'positive control after negative cases: no fixture state leaks' 0 'Z3-CHECK OK' + +if [ "$fails" -eq 0 ]; then + printf 'GATE-SELFTEST OK: %s/%s cases\n' "$cases" "$cases" + exit 0 +fi +printf 'GATE-SELFTEST FAILED: %s failures in %s cases\n' "$fails" "$cases" +exit 1 From 27f0bd0996f1ba552064b8130ca5b5c5dbde50e3 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Sat, 10 Oct 2026 20:48:31 +0000 Subject: [PATCH 3/3] fix(ci): enforce proof escape-hatch limits, disable CodeRabbit commit actions, and expand retired a2ml guards --- .coderabbit.yaml | 12 ++-- .github/workflows/proofs.yml | 17 ++++-- .../contractiles/trust/trust.k9.ncl | 11 ++-- coordination.k9 | 6 +- docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc | 35 +++++++----- scripts/check-proof-patterns.sh | 40 ++++++++++++++ tests/check-proof-patterns.sh | 55 +++++++++++++++++++ 7 files changed, 148 insertions(+), 28 deletions(-) create mode 100644 scripts/check-proof-patterns.sh create mode 100644 tests/check-proof-patterns.sh diff --git a/.coderabbit.yaml b/.coderabbit.yaml index b5f5dd5..32ae7f7 100644 --- a/.coderabbit.yaml +++ b/.coderabbit.yaml @@ -2,10 +2,10 @@ # CodeRabbit configuration. Schema: https://coderabbit.ai/integrations/schema.v2.json # # Ruling D217: CodeRabbit does not push commits to PR branches. Bot commits on a -# PR branch are unsigned and fail the estate signed-commit floor. The docstring -# finishing touch below is the feature that commits to the branch, so it is -# disabled here. The matching app-UI setting must also be off; it lives outside -# this repo and is tracked in the ULTRAPLAN. +# PR branch are unsigned and fail the estate signed-commit floor. Docstrings, +# fix_ci and resolve_merge_conflict finishing touches are disabled here. +# The matching app-UI settings must also be off; they live outside +# this repo and are tracked in the ULTRAPLAN. # # The docstring pre-merge check stays advisory (mode: warning), as in # rsr-template-repo. CodeRabbit is advisory. @@ -17,3 +17,7 @@ reviews: finishing_touches: docstrings: enabled: false + fix_ci: + enabled: false + resolve_merge_conflict: + enabled: false diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index ef776d2..a808750 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -18,7 +18,10 @@ on: pull_request: paths: - 'proofs/**' - - 'src/abi/**' + - 'src/**' + - 'scripts/check-proof-patterns.sh' + - 'tests/check-proof-patterns.sh' + - '.machine_readable/contractiles/trust/trust.k9.ncl' - 'absolute-zero-abi.ipkg' - '.github/workflows/proofs.yml' - 'Justfile' @@ -33,6 +36,14 @@ concurrency: cancel-in-progress: true jobs: + proof-patterns: + name: Proof escape-hatch baseline + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v7.0.1 + - run: bash scripts/check-proof-patterns.sh + - run: bash tests/check-proof-patterns.sh + agda: name: Agda — CNO + OND + EchoBridge runs-on: ubuntu-24.04 @@ -92,7 +103,3 @@ jobs: idris2 --version idris2 --build absolute-zero-abi.ipkg echo "✓ Idris 2: absolute-zero-abi.ipkg builds" - - name: Advisory — believe_me sites in src/abi (issue #27; not gated) - run: | - n=$(grep -rn 'believe_me' src/abi --include='*.idr' | grep -v -- '--' | wc -l) - echo "believe_me code sites in src/abi: $n (tracked in #27; advisory, not a gate)" diff --git a/.machine_readable/contractiles/trust/trust.k9.ncl b/.machine_readable/contractiles/trust/trust.k9.ncl index 9ee62a4..26fc3d1 100644 --- a/.machine_readable/contractiles/trust/trust.k9.ncl +++ b/.machine_readable/contractiles/trust/trust.k9.ncl @@ -16,8 +16,9 @@ K9! # ceremony has run, and this sandbox has no signing key. This contract is NOT # authorised to run as 'Hunt until the owner signs it. Ledger row K-1. # -# Probes are the source `run` strings with TOML escapes decoded. No runner -# executes them yet, so they are documentation-grade until a runner is wired. +# Probes are the source `run` strings with TOML escapes decoded, except for the +# dangerous-patterns probe below. Its shared script is enforced separately in +# proofs.yml, independently of this disabled contract runner. # # Adaptations (ledger rows A-T1, A-T2): the Lean and Coq "bounded" checks point # at archive/proofs/ because those provers are archived (2026-10-10). @@ -130,8 +131,10 @@ K9! { id = "no-dangerous-proof-patterns", section = "dangerous-patterns", - description = "No believe_me, assert_total, unsafeCoerce, Obj.magic in non-proof source", - probe = "! grep -rE 'believe_me|assert_total|unsafeCoerce|Obj\\\\.magic' --include='*.idr' --include='*.ml' --include='*.hs' --include='*.rs' . 2>/dev/null | head -1 | grep -q .", + description = "At most five believe_me code occurrences in src/abi Idris files; none elsewhere in src. No assert_total, unsafeCoerce or Obj.magic in src", + probe = "bash scripts/check-proof-patterns.sh", + baseline = 5, + baseline_note = "Issue #27: four sites in Proofs/DivMod.idr and one in Layout.idr. Enforced by the shared script in CI even while this runner is disabled.", severity = "critical", }, { diff --git a/coordination.k9 b/coordination.k9 index 766d0b9..aa0cfce 100644 --- a/coordination.k9 +++ b/coordination.k9 @@ -95,8 +95,12 @@ protected: do_not_create: - pattern: Dockerfile reason: "Use Containerfile (Podman)" - - pattern: .machine_readable/**/*.a2ml + - pattern: "*.a2ml" + reason: "a2ml is retired; the deed and K9 files replace it" + - pattern: "**/*.a2ml" reason: "a2ml is retired; the deed and K9 files replace it" + - pattern: .machine_readable/**/*.a2ml + reason: "Keep hidden metadata covered when glob matching excludes dot directories" ecosystem: depends_on: diff --git a/docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc b/docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc index dadba1e..059acd3 100644 --- a/docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc +++ b/docs/ULTRAPLAN-OPEN-ISSUES-2026-10-10.adoc @@ -6,12 +6,12 @@ [NOTE] ==== -*Status: PLAN, with uncommitted working-tree changes.* Nothing has been filed, -edited or closed on GitHub. No PR, ruleset or workflow was changed on GitHub. -Locally, branch `arena/6c682e29-absolute-zero` carries the changes listed in -<>. They are not committed, not signed, not pushed and not reviewed. Every -GitHub action below waits on the owner decisions in <>, and each -PR goes through the estate's normal review and signing path. +*Status (2026-10-10): PLAN, with changes published in draft +https://github.com/hyperpolymath/absolute-zero/pull/187[PR #187].* +The changes listed in <> were committed as `d74e907`, which is unsigned. +They still require a signed cherry-pick into a new PR branch (<>). +Remaining GitHub actions follow the owner decisions in <> +and the estate's normal review and signing path. *Basis:* `main` @ `6010145` (PR #186) for the recon; the ten open issues of `hyperpolymath/absolute-zero`; `hyperpolymath/standards` (shallow clone at @@ -56,10 +56,11 @@ were not run. Prover status comes from CI on `main`, which is not proof. (<>). The owner ruling narrows it. It does not remove it. [[wt]] -== Working-tree changes since the recon +== Working-tree changes since the recon (history: 2026-10-10, before PR #187) -Recorded so that the plan matches the tree. Nothing is committed. The sandbox -commits would be unsigned, so the PR path is a signed cherry-pick (<>). +The table records the earlier, uncommitted working-tree state and its checks +on 2026-10-10. Those changes are now in draft PR #187 at unsigned commit +`d74e907`; the signed cherry-pick remains outstanding (<>). [cols="1,3,3",options="header"] |=== @@ -352,10 +353,14 @@ archives Coq. The two cannot both hold as written. Options are in <>. . *Owner, app-level:* in CodeRabbit's organisation settings for this repo, turn off autofix, committable suggestions, "Commit to this branch", Autopilot, and - any docstring generation that commits to the branch. This implements D217. + any docstring generation that commits to the branch. Disable *Fix failing CI* + (`fix_ci`, including direct-commit requests) and *Resolve merge conflict* + (`resolve_merge_conflict`) so neither action can commit to a PR branch. + This implements D217. Confirm first (<>). -. *Repo (done in working tree):* `.coderabbit.yaml` with the docstring finishing - touch disabled. Its comment does not cite a signing-policy file that does not +. *Repo:* `.coderabbit.yaml` disables the docstring, `fix_ci` and + `resolve_merge_conflict` finishing touches. The docstring setting is unchanged. + Its comment does not cite a signing-policy file that does not exist in this repo. It names the estate floor and D217 only. . *Positive control:* open a throwaway PR where CodeRabbit makes a suggestion. Confirm no bot commit appears in `pulls/N/commits`, and that every commit @@ -784,8 +789,10 @@ cherry-pick. [[q9]] *Q9 (#182) — the CodeRabbit app setting.* Confirm that D217's setting is applied to -this repo in the CodeRabbit app. I cannot see it from here. If it is not applied, -apply it before any repo change is merged. +this repo in the CodeRabbit app, including disabling `fix_ci` and +`resolve_merge_conflict`. App-side settings remain unverified: this checkout +contains no app implementation and no app-settings connection is available. +Apply and verify these settings before any repo change is merged. [[q10]] *Q10 (T7, #167, #171, #70, N12) — Coq after the archive. Owner choice 2026-10-10: (b).* (a) Keep Coq archived. diff --git a/scripts/check-proof-patterns.sh b/scripts/check-proof-patterns.sh new file mode 100644 index 0000000..48cc6ab --- /dev/null +++ b/scripts/check-proof-patterns.sh @@ -0,0 +1,40 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Text gate for active source. Issue #27 approves at most five ABI believe_me +# occurrences, not a general allowance for escape hatches elsewhere. +set -euo pipefail +cd "$(dirname "$0")/.." +test -d src/abi +shopt -s globstar nullglob dotglob +sources=(src/**/*.idr src/**/*.ml src/**/*.hs src/**/*.rs) +if ((${#sources[@]} == 0)); then + echo "No source files found" >&2 + exit 1 +fi + +awk ' + { + code = $0 + # Ignore Idris documentation and line comments, retaining code before --. + if (FILENAME ~ /[.]idr$/) { + if (code ~ /^[[:space:]]*\|\|\|/) next + sub(/--.*/, "", code) + } + if (code ~ /assert_total|unsafeCoerce|Obj[.]magic/) { + print FILENAME ":" FNR ": forbidden proof escape hatch" + failed = 1 + } + while (match(code, /believe_me/)) { + if (FILENAME ~ /^src\/abi\/.*[.]idr$/) count++ + else { + print FILENAME ":" FNR ": believe_me outside the approved ABI scope" + failed = 1 + } + code = substr(code, RSTART + RLENGTH) + } + } + END { + printf "ABI believe_me occurrences: %d (maximum 5; issue #27)\n", count + exit (failed || count > 5) + } +' "${sources[@]}" diff --git a/tests/check-proof-patterns.sh b/tests/check-proof-patterns.sh new file mode 100644 index 0000000..3d4353d --- /dev/null +++ b/tests/check-proof-patterns.sh @@ -0,0 +1,55 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Exercise the gate with synthetic mutations, without changing actual proofs. +set -euo pipefail +repo_root="$(cd "$(dirname "$0")/.." && pwd)" +fixture=$(mktemp -d) +trap 'rm -rf "$fixture"' EXIT +mkdir -p "$fixture/scripts" "$fixture/src/abi" +cp "$repo_root/scripts/check-proof-patterns.sh" "$fixture/scripts/" + +expect() { + local expected=$1 label=$2 status + if bash "$fixture/scripts/check-proof-patterns.sh" > "$fixture/result" 2>&1; then + status=0 + else + status=$? + fi + if [[ "$status" != "$expected" ]]; then + cat "$fixture/result" + echo "FAIL: $label (expected $expected, got $status)" >&2 + exit 1 + fi + echo "PASS: $label" +} + +printf 'proof = believe_me ()\n%.0s' {1..5} > "$fixture/src/abi/Baseline.idr" +cat >> "$fixture/src/abi/Baseline.idr" <<'EOF' +-- believe_me in a comment +||| believe_me in documentation +EOF +expect 0 'five approved sites plus comments' +printf 'sixth = believe_me () -- inline comment\n' > "$fixture/src/abi/Extra.idr" +expect 1 'sixth site with inline comment' +rm "$fixture/src/abi/Extra.idr" +printf 'pair = (believe_me (), believe_me ())\n%.0s' {1..3} > "$fixture/src/abi/Baseline.idr" +expect 1 'multiple occurrences on one line' +: > "$fixture/src/abi/Baseline.idr" +expect 0 'baseline can decrease to zero' +printf 'escape = believe_me ()\n' > "$fixture/src/Outside.idr" +expect 1 'believe_me outside ABI even below baseline' +rm "$fixture/src/Outside.idr" +for pattern in assert_total unsafeCoerce Obj.magic; do + printf 'escape = %s\n' "$pattern" > "$fixture/src/abi/Extra.idr" + expect 1 "$pattern is never allowed in ABI" + rm "$fixture/src/abi/Extra.idr" +done +for extension in rs ml hs; do + printf 'Obj.magic\n' > "$fixture/src/Outside.$extension" + expect 1 "forbidden pattern in $extension source" + rm "$fixture/src/Outside.$extension" +done +rm "$fixture/src/abi/Baseline.idr" +expect 1 'empty source fails closed' +rmdir "$fixture/src/abi" +expect 1 'missing ABI directory fails closed'