From 8fbde55d89701a23163732a39aa579664a83f0de Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 7 Jul 2026 06:28:21 +0100 Subject: [PATCH] =?UTF-8?q?chore(naming)+ci:=20migrate=206a2=20=E2=86=92?= =?UTF-8?q?=20descriptiles;=20harden=20proofs=20CI?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Naming mandate (estate 2026-06-30): the machine-readable metadata family is `descriptiles`, and `6a2` is fully deprecated. Rename the directory .machine_readable/6a2/ → .machine_readable/descriptiles/ and migrate every `6a2` path/prose reference across the repo (21 files: docs, wiki, AUDIT, GOVERNANCE, RSR_COMPLIANCE, contractile Mustfile invariants, .well-known/ai.txt, the metadata files' own cross-references). Zero residual `6a2`. CI (.github/workflows/proofs.yml): - Three INDEPENDENT jobs — Coq (14 theories, both pillars), Agda (CNO + OND), Z3 (CNO + OND bounded) — so one flaking never reds the others. - Pinned to ubuntu-24.04 (ships Coq 8.18, exactly what the proofs need) to stop apt version drift; concurrency-cancel; SHA-pinned checkout; contents: read. - Heavy provers (Lean+Mathlib, Isabelle, Mizar, Idris) stay on the local gate proofs/verify-all-provers.sh, as documented in-file. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/proofs.yml | 50 ++++++++++++++++--- .machine_readable/contractiles/Dustfile.a2ml | 2 +- .../contractiles/Intentfile.a2ml | 2 +- .machine_readable/contractiles/Mustfile.a2ml | 16 +++--- .../{6a2 => descriptiles}/0-AI-MANIFEST.a2ml | 4 +- .../{6a2 => descriptiles}/AGENTIC.a2ml | 4 +- .../{6a2 => descriptiles}/ECOSYSTEM.a2ml | 0 .../{6a2 => descriptiles}/META.a2ml | 0 .../{6a2 => descriptiles}/NEUROSYM.a2ml | 0 .../{6a2 => descriptiles}/PLAYBOOK.a2ml | 4 +- .../{6a2 => descriptiles}/README.adoc | 2 +- .../{6a2 => descriptiles}/STATE.a2ml | 0 .../anchor/0-AI-MANIFEST.a2ml | 0 .../{6a2 => descriptiles}/anchor/ANCHOR.a2ml | 4 +- .../{6a2 => descriptiles}/anchor/README.adoc | 0 .well-known/ai.txt | 2 +- 0-AI-MANIFEST.a2ml | 18 +++---- AUDIT.adoc | 8 +-- GOVERNANCE.adoc | 2 +- RSR_COMPLIANCE.adoc | 4 +- docs/archive/README.adoc | 6 +-- docs/wiki/Contributing.md | 2 +- docs/wiki/FAQ.md | 2 +- docs/wiki/Glossary.md | 6 +-- docs/wiki/Home.md | 2 +- docs/wiki/Roadmap.md | 4 +- docs/wiki/Verification.md | 2 +- docs/wiki/_Sidebar.md | 2 +- 28 files changed, 91 insertions(+), 57 deletions(-) rename .machine_readable/{6a2 => descriptiles}/0-AI-MANIFEST.a2ml (81%) rename .machine_readable/{6a2 => descriptiles}/AGENTIC.a2ml (93%) rename .machine_readable/{6a2 => descriptiles}/ECOSYSTEM.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/META.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/NEUROSYM.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/PLAYBOOK.a2ml (92%) rename .machine_readable/{6a2 => descriptiles}/README.adoc (97%) rename .machine_readable/{6a2 => descriptiles}/STATE.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/anchor/0-AI-MANIFEST.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/anchor/ANCHOR.a2ml (79%) rename .machine_readable/{6a2 => descriptiles}/anchor/README.adoc (100%) diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 82b3c21..49463c6 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -1,11 +1,14 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) Jonathan D.A. Jewell # -# Proof verification CI. Runs the LIGHTWEIGHT provers that are feasible on a -# standard GitHub runner — Coq (both pillars, all 14 theories) and Z3 (CNO + -# OND bounded instances). The full six-prover gate (adds Lean+Mathlib, Agda, -# Isabelle, Mizar, Idris) is heavy and runs locally / in a container via -# `proofs/verify-all-provers.sh`; see PROOF-STATUS.adoc. +# 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. +# +# The heavy provers (Lean + multi-GB Mathlib, 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. name: Proofs on: @@ -24,10 +27,15 @@ on: permissions: contents: read +# Cancel superseded runs on the same ref (don't pile up on force-pushes). +concurrency: + group: proofs-${{ github.ref }} + cancel-in-progress: true + jobs: coq: name: Coq — CNO + OND (14 theories) - runs-on: ubuntu-latest + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 - name: Install Coq @@ -40,9 +48,35 @@ jobs: make -f Makefile.all -j"$(nproc)" echo "✓ Coq: 14/14 theories compiled (CNO + OND)" + agda: + name: Agda — CNO + OND + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 + - name: Install Agda + stdlib + run: sudo apt-get update && sudo apt-get install -y agda agda-stdlib + - name: Register the standard library + run: | + mkdir -p "$HOME/.agda" + LIB="$(dpkg -L agda-stdlib | grep -m1 'standard-library.*\.agda-lib' || true)" + if [ -n "$LIB" ]; then + echo "$LIB" > "$HOME/.agda/libraries" + echo "standard-library" > "$HOME/.agda/defaults" + echo "registered: $LIB" + else + echo "agda-stdlib .agda-lib not found via dpkg -L" >&2; exit 1 + fi + - name: Type-check CNO + OND (--safe --without-K) + working-directory: proofs/agda + run: | + agda --version + agda --safe --without-K CNO.agda + agda --safe --without-K OND.agda + echo "✓ Agda: CNO + OND type-check" + z3: - name: Z3 — OND bounded checks - runs-on: ubuntu-latest + name: Z3 — CNO + OND bounded checks + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 - name: Install Z3 diff --git a/.machine_readable/contractiles/Dustfile.a2ml b/.machine_readable/contractiles/Dustfile.a2ml index 2c1e448..e87ee2c 100644 --- a/.machine_readable/contractiles/Dustfile.a2ml +++ b/.machine_readable/contractiles/Dustfile.a2ml @@ -43,7 +43,7 @@ notes = "Exercised precedent: PR #69 repinned orphan reusable SHAs (97df7621/4fd [[recovery]] id = "stale-machine-metadata" -asset = ".machine_readable/ (6a2, contractiles, bot_directives)" +asset = ".machine_readable/ (descriptiles, contractiles, bot_directives)" reversible = true handler = "Regenerate from repo facts: git log since the last STATE date + repo docs, per the governance-checkpoint discipline; prior states recoverable from git history" notes = "STATE refreshes are additive light-bumps; never invent facts — omit unknown keys." diff --git a/.machine_readable/contractiles/Intentfile.a2ml b/.machine_readable/contractiles/Intentfile.a2ml index 492942b..4816184 100644 --- a/.machine_readable/contractiles/Intentfile.a2ml +++ b/.machine_readable/contractiles/Intentfile.a2ml @@ -12,7 +12,7 @@ # # Populated 2026-06-12 (governance checkpoint): replaces the # rsr-template-repo stub. Sources: README.adoc, ROADMAP.adoc, -# 6a2/STATE.a2ml ([route-to-mvp], [critical-next-actions], [blockers-and-issues]). +# descriptiles/STATE.a2ml ([route-to-mvp], [critical-next-actions], [blockers-and-issues]). # A2ML here is TOML-flavoured. [metadata] diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml index afda9d7..965f8d9 100644 --- a/.machine_readable/contractiles/Mustfile.a2ml +++ b/.machine_readable/contractiles/Mustfile.a2ml @@ -17,7 +17,7 @@ repo = "absolute-zero" contractile-verb = "must" last-updated = "2026-06-12" -abstract = "Physical-state invariants for absolute-zero: required governance files, the flat contractile set, the 6a2 metadata set, and the absence of superseded duplicate metadata." +abstract = "Physical-state invariants for absolute-zero: required governance files, the flat contractile set, the descriptiles metadata set, and the absence of superseded duplicate metadata." [[checks]] id = "license-present" @@ -57,14 +57,14 @@ severity = "critical" [[checks]] id = "six-a2ml-present" -description = "6a2 directory has all six A2ML files plus manifest and README" -run = "test -f .machine_readable/6a2/STATE.a2ml && test -f .machine_readable/6a2/META.a2ml && test -f .machine_readable/6a2/ECOSYSTEM.a2ml && test -f .machine_readable/6a2/AGENTIC.a2ml && test -f .machine_readable/6a2/NEUROSYM.a2ml && test -f .machine_readable/6a2/PLAYBOOK.a2ml && test -f .machine_readable/6a2/0-AI-MANIFEST.a2ml" +description = "descriptiles directory has all six A2ML files plus manifest and README" +run = "test -f .machine_readable/descriptiles/STATE.a2ml && test -f .machine_readable/descriptiles/META.a2ml && test -f .machine_readable/descriptiles/ECOSYSTEM.a2ml && test -f .machine_readable/descriptiles/AGENTIC.a2ml && test -f .machine_readable/descriptiles/NEUROSYM.a2ml && test -f .machine_readable/descriptiles/PLAYBOOK.a2ml && test -f .machine_readable/descriptiles/0-AI-MANIFEST.a2ml" severity = "critical" [[checks]] id = "anchor-directory" -description = "6a2/anchor/ exists with ANCHOR.a2ml (realignment record)" -run = "test -d .machine_readable/6a2/anchor && test -f .machine_readable/6a2/anchor/ANCHOR.a2ml" +description = "descriptiles/anchor/ exists with ANCHOR.a2ml (realignment record)" +run = "test -d .machine_readable/descriptiles/anchor && test -f .machine_readable/descriptiles/anchor/ANCHOR.a2ml" severity = "warning" [[checks]] @@ -81,14 +81,14 @@ severity = "warning" [[checks]] id = "no-duplicate-root-scm" -description = "No duplicate root .machine_readable/*.scm set (removed by estate wave 2026-06; 6a2/*.a2ml is canonical)" +description = "No duplicate root .machine_readable/*.scm set (removed by estate wave 2026-06; descriptiles/*.a2ml is canonical)" run = "test -z \"$(ls .machine_readable/*.scm 2>/dev/null)\"" severity = "critical" [[checks]] id = "a2ml-parses-as-toml" -description = "Every 6a2 A2ML file parses as TOML" -run = "for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml .machine_readable/6a2/AGENTIC.a2ml .machine_readable/6a2/NEUROSYM.a2ml .machine_readable/6a2/PLAYBOOK.a2ml; do python3 -c \"import tomllib;tomllib.load(open('$f','rb'))\" || exit 1; done" +description = "Every descriptiles A2ML file parses as TOML" +run = "for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml .machine_readable/descriptiles/AGENTIC.a2ml .machine_readable/descriptiles/NEUROSYM.a2ml .machine_readable/descriptiles/PLAYBOOK.a2ml; do python3 -c \"import tomllib;tomllib.load(open('$f','rb'))\" || exit 1; done" severity = "critical" [[checks]] diff --git a/.machine_readable/6a2/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml similarity index 81% rename from .machine_readable/6a2/0-AI-MANIFEST.a2ml rename to .machine_readable/descriptiles/0-AI-MANIFEST.a2ml index 6bf1f8c..83c1803 100644 --- a/.machine_readable/6a2/0-AI-MANIFEST.a2ml +++ b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml @@ -1,8 +1,8 @@ -# AI Manifest for 6a2 Directory +# AI Manifest for descriptiles Directory ## Purpose -This manifest declares the AI-assistant context for the 6a2 machine-readable metadata directory. +This manifest declares the AI-assistant context for the descriptiles machine-readable metadata directory. ## Canonical Locations diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml similarity index 93% rename from .machine_readable/6a2/AGENTIC.a2ml rename to .machine_readable/descriptiles/AGENTIC.a2ml index 0580baf..8c3facd 100644 --- a/.machine_readable/6a2/AGENTIC.a2ml +++ b/.machine_readable/descriptiles/AGENTIC.a2ml @@ -51,6 +51,6 @@ recommended = ["read", "edit", "bash", "grep", "glob"] permissions = "read-all" [automation-hooks] -# on-enter: Read AI.a2ml, then .machine_readable/6a2/STATE.a2ml -# on-exit: Update .machine_readable/6a2/STATE.a2ml with session outcomes +# on-enter: Read AI.a2ml, then .machine_readable/descriptiles/STATE.a2ml +# on-exit: Update .machine_readable/descriptiles/STATE.a2ml with session outcomes # on-commit: Run just validate-rsr (if available) diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml similarity index 100% rename from .machine_readable/6a2/ECOSYSTEM.a2ml rename to .machine_readable/descriptiles/ECOSYSTEM.a2ml diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/descriptiles/META.a2ml similarity index 100% rename from .machine_readable/6a2/META.a2ml rename to .machine_readable/descriptiles/META.a2ml diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/descriptiles/NEUROSYM.a2ml similarity index 100% rename from .machine_readable/6a2/NEUROSYM.a2ml rename to .machine_readable/descriptiles/NEUROSYM.a2ml diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/descriptiles/PLAYBOOK.a2ml similarity index 92% rename from .machine_readable/6a2/PLAYBOOK.a2ml rename to .machine_readable/descriptiles/PLAYBOOK.a2ml index 6b565f2..7807bbe 100644 --- a/.machine_readable/6a2/PLAYBOOK.a2ml +++ b/.machine_readable/descriptiles/PLAYBOOK.a2ml @@ -31,14 +31,14 @@ build-mizar = "just build-mizar" build-idris = "just build-idris" [incident-response] -# 1. Check .machine_readable/6a2/STATE.a2ml for current status +# 1. Check .machine_readable/descriptiles/STATE.a2ml for current status # 2. Review recent commits: git log --oneline -10 # 3. Run `just validate` if available # 4. Run `just security` for vulnerability audit # 5. For proof failures: check proofs// for unsaved Admitted/sorry [release-process] -# 1. Update version in .machine_readable/6a2/STATE.a2ml and META.a2ml +# 1. Update version in .machine_readable/descriptiles/STATE.a2ml and META.a2ml # 2. Resolve all Admitted/sorry entries to target count # 3. Run `just build-all` to confirm no regressions # 4. Tag and push to origin (GitHub only) diff --git a/.machine_readable/6a2/README.adoc b/.machine_readable/descriptiles/README.adoc similarity index 97% rename from .machine_readable/6a2/README.adoc rename to .machine_readable/descriptiles/README.adoc index 916a702..97414db 100644 --- a/.machine_readable/6a2/README.adoc +++ b/.machine_readable/descriptiles/README.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -# A2ML 6a2 Directory +# A2ML descriptiles Directory This directory contains the 6 core A2ML machine-readable metadata files for this repository. diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml similarity index 100% rename from .machine_readable/6a2/STATE.a2ml rename to .machine_readable/descriptiles/STATE.a2ml diff --git a/.machine_readable/6a2/anchor/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml similarity index 100% rename from .machine_readable/6a2/anchor/0-AI-MANIFEST.a2ml rename to .machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml diff --git a/.machine_readable/6a2/anchor/ANCHOR.a2ml b/.machine_readable/descriptiles/anchor/ANCHOR.a2ml similarity index 79% rename from .machine_readable/6a2/anchor/ANCHOR.a2ml rename to .machine_readable/descriptiles/anchor/ANCHOR.a2ml index 4d6f39b..6d20627 100644 --- a/.machine_readable/6a2/anchor/ANCHOR.a2ml +++ b/.machine_readable/descriptiles/anchor/ANCHOR.a2ml @@ -16,9 +16,9 @@ last-updated = "2026-06-12" date = "2026-06-12" title = "Estate standardization + governance checkpoint" what-changed = [ - "Merged origin/estate-standardization-20260607: flat .machine_readable/contractiles/ layout, svc/k9 → self-validating/ rename, GOVERNANCE.adoc + MAINTAINERS.adoc + .github/CODEOWNERS, Guix manifest.scm, 6a2 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", + "Merged origin/estate-standardization-20260607: flat .machine_readable/contractiles/ layout, svc/k9 → 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.a2ml, gitbot-fleet.a2ml, git-private-farm.a2ml); flat contractiles fully populated with repo-true content (template stubs replaced; old nested bust/trust content ported; new Dustfile.a2ml + Bustfile.a2ml); 6a2/STATE.a2ml 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 (license MPL-2.0, axiom count 72, status note)", + "Governance checkpoint layer: bot_directives/ (README.adoc, hypatia.a2ml, gitbot-fleet.a2ml, git-private-farm.a2ml); flat contractiles fully populated with repo-true content (template stubs replaced; old nested bust/trust content ported; new Dustfile.a2ml + Bustfile.a2ml); descriptiles/STATE.a2ml 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 (license MPL-2.0, axiom count 72, status note)", ] 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 = [ diff --git a/.machine_readable/6a2/anchor/README.adoc b/.machine_readable/descriptiles/anchor/README.adoc similarity index 100% rename from .machine_readable/6a2/anchor/README.adoc rename to .machine_readable/descriptiles/anchor/README.adoc diff --git a/.well-known/ai.txt b/.well-known/ai.txt index 557c42a..a3a481f 100644 --- a/.well-known/ai.txt +++ b/.well-known/ai.txt @@ -5,7 +5,7 @@ User-Agent: * Manifest: /0-AI-MANIFEST.a2ml EntryPoint: /docs/CLAUDE.adoc -State: /.machine_readable/6a2/STATE.a2ml +State: /.machine_readable/descriptiles/STATE.a2ml Roadmap: /ROADMAP.adoc Allow: training-with-attribution Allow: documentation-summarisation diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 4a9ece9..9413e0d 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -19,22 +19,22 @@ purpose = """ [entry-points] # Where an AI agent should look first. root-context = "docs/CLAUDE.adoc" -project-state = ".machine_readable/6a2/STATE.a2ml" +project-state = ".machine_readable/descriptiles/STATE.a2ml" roadmap = "ROADMAP.adoc" contributing = "CONTRIBUTING.adoc" audit-trail = "AUDIT.adoc" rsr-status = "RSR_COMPLIANCE.adoc" [machine-readable] -# Authoritative metadata artefacts; .a2ml format under 6a2/ supersedes +# Authoritative metadata artefacts; .a2ml format under descriptiles/ supersedes # the older Guile-Scheme .scm format. Both kept side-by-side during the # migration window for legacy tooling compatibility. -state = ".machine_readable/6a2/STATE.a2ml" -meta = ".machine_readable/6a2/META.a2ml" -ecosystem = ".machine_readable/6a2/ECOSYSTEM.a2ml" -agentic = ".machine_readable/6a2/AGENTIC.a2ml" -neurosym = ".machine_readable/6a2/NEUROSYM.a2ml" -playbook = ".machine_readable/6a2/PLAYBOOK.a2ml" +state = ".machine_readable/descriptiles/STATE.a2ml" +meta = ".machine_readable/descriptiles/META.a2ml" +ecosystem = ".machine_readable/descriptiles/ECOSYSTEM.a2ml" +agentic = ".machine_readable/descriptiles/AGENTIC.a2ml" +neurosym = ".machine_readable/descriptiles/NEUROSYM.a2ml" +playbook = ".machine_readable/descriptiles/PLAYBOOK.a2ml" legacy-scm-meta = ".machine_readable/META.scm" legacy-scm-ecosystem = ".machine_readable/ECOSYSTEM.scm" @@ -67,5 +67,5 @@ tools = [ [delivery] commit-policy = "conventional commits; never amend published commits" -state-update = "update .machine_readable/6a2/STATE.a2ml whenever phase/progress changes" +state-update = "update .machine_readable/descriptiles/STATE.a2ml whenever phase/progress changes" adr-tracking = "architectural changes recorded in .machine_readable/META.scm `architecture-decisions`" diff --git a/AUDIT.adoc b/AUDIT.adoc index 0de86d8..61f0668 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -13,7 +13,7 @@ audits, and other trust-boundary events. For architectural decisions (which are forward-looking design choices rather than backward-looking audit events), see -`.machine_readable/6a2/META.a2ml` `architecture-decisions`. +`.machine_readable/descriptiles/META.a2ml` `architecture-decisions`. == Open Audit Items @@ -74,7 +74,7 @@ PR #100 — see Resolved Audit Items below._ |2026-05-20 |`eval_deterministic` discharged from Axiom → Theorem via `step_deterministic_strong` helper. First post-T0 axiom audit win. -|PR #24 (see 6a2/META.a2ml ADR-007) +|PR #24 (see descriptiles/META.a2ml ADR-007) |AUDIT-2026-05-20-#32 |2026-05-20 @@ -83,7 +83,7 @@ PR #100 — see Resolved Audit Items below._ (`=st=`); re-proved `cno_eval_on_equal_states` + `cno_logically_reversible` via `cno_terminates` + `cno_preserves_state`. -|PR #32 (see 6a2/META.a2ml ADR-008) +|PR #32 (see descriptiles/META.a2ml ADR-008) |AUDIT-2026-02-05 |2026-02-05 @@ -102,6 +102,6 @@ Audit IDs follow `AUDIT--`: == See also -* `.machine_readable/6a2/META.a2ml` — forward-looking architecture decisions (ADR-001…N) +* `.machine_readable/descriptiles/META.a2ml` — forward-looking architecture decisions (ADR-001…N) * `docs/archive/` — historical session / audit artefacts (dated) * `RSR_COMPLIANCE.adoc` — Rhodium Standard Repository compliance status diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index e41020d..f893c5c 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -128,7 +128,7 @@ This repository adheres to hyperpolymath estate-wide policies: | **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ +| **Machine Readable** | META.a2ml in .machine_readable/descriptiles/ | **CI/CD** | GitHub Actions workflows in .github/workflows/ diff --git a/RSR_COMPLIANCE.adoc b/RSR_COMPLIANCE.adoc index c3b313c..7cde875 100644 --- a/RSR_COMPLIANCE.adoc +++ b/RSR_COMPLIANCE.adoc @@ -37,7 +37,7 @@ For the RSR taxonomy itself (what the template prescribes), see |Machine-readable artefacts |✅ Passing -|`.machine_readable/6a2/{STATE,META,ECOSYSTEM,AGENTIC,NEUROSYM,PLAYBOOK}.a2ml` +|`.machine_readable/descriptiles/{STATE,META,ECOSYSTEM,AGENTIC,NEUROSYM,PLAYBOOK}.a2ml` + legacy `.scm` siblings during migration window. |`0-AI-MANIFEST.a2ml` @@ -98,4 +98,4 @@ For the RSR taxonomy itself (what the template prescribes), see * `docs/RSR_OUTLINE.adoc` — the RSR template's own README (what the standard prescribes) * `AUDIT.adoc` — audit trail for unsoundness/dead-code findings * `0-AI-MANIFEST.a2ml` — AI-agent entry-point manifest -* `.machine_readable/6a2/STATE.a2ml` — live project state +* `.machine_readable/descriptiles/STATE.a2ml` — live project state diff --git a/docs/archive/README.adoc b/docs/archive/README.adoc index 076736a..02ef76d 100644 --- a/docs/archive/README.adoc +++ b/docs/archive/README.adoc @@ -10,7 +10,7 @@ snapshots or by updating the live documents listed below. Authoritative live sources: -* Project state — `.machine_readable/6a2/STATE.a2ml` +* Project state — `.machine_readable/descriptiles/STATE.a2ml` * Roadmap — `ROADMAP.adoc` (repo root) * Proof-debt disposition — `docs/proof-debt-triage.md` and `docs/proof-debt.md` * Audit findings — `AUDIT.adoc` (repo root) @@ -21,9 +21,9 @@ Authoritative live sources: |=== | File | Date | What it was | Superseded by -| `CURRENT-STATUS-2026-02-05.md` | 2026-02-05 | Point-in-time project status | `.machine_readable/6a2/STATE.a2ml` +| `CURRENT-STATUS-2026-02-05.md` | 2026-02-05 | Point-in-time project status | `.machine_readable/descriptiles/STATE.a2ml` | `ECHIDNA-2025-11-22.adoc` | 2025-11-22 | Early ECHIDNA integration notes | `ECHIDNA.adoc` -| `INTEGRATION-STATUS-2026-02-05.adoc` | 2026-02-05 | Integration status snapshot | `.machine_readable/6a2/STATE.a2ml` +| `INTEGRATION-STATUS-2026-02-05.adoc` | 2026-02-05 | Integration status snapshot | `.machine_readable/descriptiles/STATE.a2ml` | `LICENSE-AUDIT-2026-02-05.adoc` | 2026-02-05 | License audit snapshot | `LICENSE` (MPL-2.0) | `PROOF-COMPLETION-2026-02-06.md` | 2026-02-06 | Proof-completion plan snapshot | `docs/PROOF-COMPLETION-PLAN.adoc` | `PROOF-STATUS-2026-05-18.md` | 2026-05-18 | Tier-0 rescue proof-status ledger | `docs/proof-debt-triage.md`, `AUDIT.adoc` diff --git a/docs/wiki/Contributing.md b/docs/wiki/Contributing.md index e4f9f07..1df7539 100644 --- a/docs/wiki/Contributing.md +++ b/docs/wiki/Contributing.md @@ -44,7 +44,7 @@ just fmt ## ADR / Audit trail * If your change is an **architectural decision** going forward, add an ADR - entry to [`.machine_readable/6a2/META.a2ml`](../../.machine_readable/6a2/META.a2ml) + entry to [`.machine_readable/descriptiles/META.a2ml`](../../.machine_readable/descriptiles/META.a2ml) (next ADR-NNN). * If your change **discharges a postulate / deletes unsound code**, add an AUDIT entry to [`AUDIT.adoc`](../../AUDIT.adoc). diff --git a/docs/wiki/FAQ.md b/docs/wiki/FAQ.md index 9af25b3..0846cc3 100644 --- a/docs/wiki/FAQ.md +++ b/docs/wiki/FAQ.md @@ -66,7 +66,7 @@ external world, not gaps in the verification of the computational claim. ### Where's the live state? -`.machine_readable/6a2/STATE.a2ml`. Updated on every meaningful change. +`.machine_readable/descriptiles/STATE.a2ml`. Updated on every meaningful change. ### Why "Absolute Zero"? diff --git a/docs/wiki/Glossary.md b/docs/wiki/Glossary.md index 62696b7..c02eae1 100644 --- a/docs/wiki/Glossary.md +++ b/docs/wiki/Glossary.md @@ -10,14 +10,14 @@ Copyright (c) Jonathan D.A. Jewell | **Identity morphism** | In category theory, the morphism `id_X : X → X` that leaves `X` unchanged. CNOs are identity morphisms in the category of computational states (ADR-001). | | **Observational reversibility (`=st=`)** | The weakened reversibility property used after ADR-008. State equality modulo program-counter bookkeeping; PC is not observable, so two states with different PC but same observable content are `=st=`. | | **Landauer bound** | Lower thermodynamic cost of erasing one bit (`kT ln 2`). CNOs erase nothing, so any logically-reversible CNO can in principle be thermodynamically reversible too. Formalised in `StatMech.v` (axiom) + derived in `LandauerDerivation.v` (ADR-002). | -| **Postulate / Axiom** | Asserted, unproven proposition. In Coq: `Axiom`. In Lean: `axiom`. In Idris2 0.8.0: `name = believe_me ()` (the `postulate` keyword was removed). Every estate-wide axiom is tracked in [`AUDIT.adoc`](../../AUDIT.adoc) or [`6a2/META.a2ml`](../../.machine_readable/6a2/META.a2ml). | +| **Postulate / Axiom** | Asserted, unproven proposition. In Coq: `Axiom`. In Lean: `axiom`. In Idris2 0.8.0: `name = believe_me ()` (the `postulate` keyword was removed). Every estate-wide axiom is tracked in [`AUDIT.adoc`](../../AUDIT.adoc) or [`descriptiles/META.a2ml`](../../.machine_readable/descriptiles/META.a2ml). | | **HasAlignment t n** | Idris2 type asserting that type `t` has byte alignment `n`. The constructor `AlignProof` is information-free — the obligation sits on the producer to construct it only for the genuinely-correct `n`. | | **alignedSize** | `(size, align) ↦` smallest multiple of `align` that is ≥ `size`. Core ABI primitive; correctness proved (via `believe_me`, pending discharge) in `Proofs.DivMod`. | | **BoJ** | Brain of Jonathan — the estate's cross-repo automation cartridge layer. ECHIDNA invocations route through `echidna-llm-mcp` BoJ. | | **ECHIDNA** | Estate-wide neurosymbolic prover gateway. 105 prover backends, 66,674-proof corpus, ML tactic suggestion. Lives in a separate repo; called via BoJ. | | **PMPL-1.0** | Palimpsest-MPL 1.0. *Former* project licence (see the archived [licence audit](../archive/LICENSE-AUDIT-2026-02-05.adoc)); the project licence is **MPL-2.0** — see [`LICENSE`](../../LICENSE). | | **RSR** | Rhodium Standard Repository — the estate-wide taxonomy convention defined by [`hyperpolymath/rsr-template-repo`](https://github.com/hyperpolymath/rsr-template-repo). Conformance tracked in [`RSR_COMPLIANCE.adoc`](../../RSR_COMPLIANCE.adoc). | -| **ADR** | Architectural Decision Record. Forward-looking design choice. Recorded in [`6a2/META.a2ml`](../../.machine_readable/6a2/META.a2ml). | +| **ADR** | Architectural Decision Record. Forward-looking design choice. Recorded in [`descriptiles/META.a2ml`](../../.machine_readable/descriptiles/META.a2ml). | | **AUDIT-ID** | Backward-looking trust event (discharged axiom, deleted unsound code, license correction). Format `AUDIT-YYYY-MM-DD-`. Recorded in [`AUDIT.adoc`](../../AUDIT.adoc). | -| **6a2** | The `.a2ml` machine-readable format under `.machine_readable/6a2/`. Successor to the older `.scm` (Guile Scheme) format; the side-by-side `.scm` set was removed by the estate standardization (2026-06). | +| **descriptiles** | The `.a2ml` machine-readable format under `.machine_readable/descriptiles/`. Successor to the older `.scm` (Guile Scheme) format; the side-by-side `.scm` set was removed by the estate standardization (2026-06). | | **Trust escape** | An axiom or `believe_me` use that lets you bypass the type system. Hunted by the estate-wide cross-trust-escape sweep. | diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md index eb856c6..9554620 100644 --- a/docs/wiki/Home.md +++ b/docs/wiki/Home.md @@ -43,7 +43,7 @@ of 23+ languages. * **Lean 4**: `lake build` green (Mathlib) incl. the new `OND` lib; 0 `sorry`. * **Agda / Z3 / Isabelle / Mizar**: CNO + OND verified (Agda `OND.agda`; Z3 `ond/OND_checks.smt2`; Isabelle `AbsoluteZero-CNO` session; Mizar `CNO.miz` → empty `.err`). * **Idris2 ABI**: `absolute-zero-abi.ipkg` builds clean under 0.8.0. -* For the authoritative live state, read [`.machine_readable/6a2/STATE.a2ml`](../../.machine_readable/6a2/STATE.a2ml) +* For the authoritative live state, read [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descriptiles/STATE.a2ml) **Status note (2026-07-06)** — PR #100 (MERGED) completed both pillars across six provers + the Idris ABI: the OND (disclosure) pillar was authored from scratch diff --git a/docs/wiki/Roadmap.md b/docs/wiki/Roadmap.md index 06dcc11..e9ad2a4 100644 --- a/docs/wiki/Roadmap.md +++ b/docs/wiki/Roadmap.md @@ -27,7 +27,7 @@ standardisation. Detailed phase decomposition in [`ROADMAP.adoc`](../../ROADMAP. ## How decisions are recorded * Forward-looking architectural choices → ADRs in - [`.machine_readable/6a2/META.a2ml`](../../.machine_readable/6a2/META.a2ml) + [`.machine_readable/descriptiles/META.a2ml`](../../.machine_readable/descriptiles/META.a2ml) `architecture-decisions` section * Backward-looking audit events → [`AUDIT.adoc`](../../AUDIT.adoc) -* Live phase / progress → [`.machine_readable/6a2/STATE.a2ml`](../../.machine_readable/6a2/STATE.a2ml) +* Live phase / progress → [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descriptiles/STATE.a2ml) diff --git a/docs/wiki/Verification.md b/docs/wiki/Verification.md index 4bfb55e..604b352 100644 --- a/docs/wiki/Verification.md +++ b/docs/wiki/Verification.md @@ -93,7 +93,7 @@ podman run --rm absolute-zero:verify just verify ## Status as of 2026-07-06 (PR #100) -See [`.machine_readable/6a2/STATE.a2ml`](../../.machine_readable/6a2/STATE.a2ml) +See [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descriptiles/STATE.a2ml) and [`PROOF-STATUS.adoc`](../../PROOF-STATUS.adoc) for live status. Summary: both pillars verified across **six provers + Idris** — Coq 14/14, Lean+Mathlib green, Agda (CNO+OND), Z3, Isabelle (`AbsoluteZero-CNO`), Mizar (`CNO.miz` empty `.err`), diff --git a/docs/wiki/_Sidebar.md b/docs/wiki/_Sidebar.md index 462759b..dab6fc2 100644 --- a/docs/wiki/_Sidebar.md +++ b/docs/wiki/_Sidebar.md @@ -22,7 +22,7 @@ Copyright (c) Jonathan D.A. Jewell --- **Live state** -[`STATE.a2ml`](https://github.com/hyperpolymath/absolute-zero/blob/main/.machine_readable/6a2/STATE.a2ml) +[`STATE.a2ml`](https://github.com/hyperpolymath/absolute-zero/blob/main/.machine_readable/descriptiles/STATE.a2ml) **AI manifest** [`0-AI-MANIFEST.a2ml`](https://github.com/hyperpolymath/absolute-zero/blob/main/0-AI-MANIFEST.a2ml)