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..32ae7f7 --- /dev/null +++ b/.coderabbit.yaml @@ -0,0 +1,23 @@ +# 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. 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. +reviews: + pre_merge_checks: + docstrings: + mode: warning + threshold: 80 + 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 a915123..a808750 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,14 @@ on: pull_request: paths: - 'proofs/**' + - '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' - '*.agda-lib' - - 'lakefile*' permissions: contents: read @@ -41,37 +36,16 @@ concurrency: cancel-in-progress: true jobs: - coq: - name: Coq — CNO + OND (14 theories) + proof-patterns: + name: Proof escape-hatch baseline 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 + - run: bash scripts/check-proof-patterns.sh + - run: bash tests/check-proof-patterns.sh agda: - name: Agda — CNO + OND + name: Agda — CNO + OND + EchoBridge runs-on: ubuntu-24.04 timeout-minutes: 25 steps: @@ -114,25 +88,18 @@ 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: | - 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 + idris2 --version + idris2 --build absolute-zero-abi.ipkg + echo "✓ Idris 2: absolute-zero-abi.ipkg builds" 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..26fc3d1 --- /dev/null +++ b/.machine_readable/contractiles/trust/trust.k9.ncl @@ -0,0 +1,174 @@ +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, 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). + +{ + 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 = "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", + }, + { + 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/archive/proofs/tests/gate-selftest.six-prover.sh b/archive/proofs/tests/gate-selftest.six-prover.sh new file mode 100755 index 0000000..76489a6 --- /dev/null +++ b/archive/proofs/tests/gate-selftest.six-prover.sh @@ -0,0 +1,130 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Absolute Zero — self-test for the prover gate. +# +# Proves that proofs/verify-all-provers.sh and proofs/z3/verify.sh turn RED when +# they should, using a stub toolchain on a private PATH (no real prover needed), +# plus two mutants under a REAL z3 (required on PATH). Every negative case must +# fail with the expected reason string, not merely a non-zero exit — a parse +# error would otherwise pass as a kill. +# HOME is overridden because the gate prepends $HOME/.local/bin:$HOME/.elan/bin. +set -uo pipefail +HERE="$(cd "$(dirname "$0")" && pwd)" +PROOFS="$(cd "$HERE/.." && pwd)" +GATE="$PROOFS/verify-all-provers.sh" +Z3CHECK="$PROOFS/z3/verify.sh" +REAL_SMT2="$PROOFS/z3/ond/OND_checks.smt2" +SCRATCH="$(mktemp -d "${TMPDIR:-/tmp}/az-gate-selftest.XXXXXX")" +trap 'rm -rf "$SCRATCH"' EXIT +STUB="$SCRATCH/bin"; mkdir -p "$STUB" "$SCRATCH/home" +cases=0; fails=0 +# pass