Skip to content

Commit 5d770f7

Browse files
claudeclaude
committed
chore(rsr): align to RSR taxonomy — 0-AI-MANIFEST, AUDIT, RSR_COMPLIANCE, .well-known, tests/, tools/, verification/
Per Hypatia governance scan + RSR-template-repo conventions: * 0-AI-MANIFEST.a2ml created (was the missing root-hygiene file Hypatia flagged). Consolidates the deleted stray AI.a2ml + AI.djot; customised for absolute-zero (was previously rsr-template-repo boilerplate copy-paste). Includes echidna-llm-mcp BoJ protocol table, language policy summary, machine-readable artefact map. * AUDIT.adoc created — estate audit trail. Records the absolute-zero#27 discharge (unsound alignmentMatchesPlatformWord) plus the pre-existing Types.idr and cflite_pr.yml findings as open items. * RSR_COMPLIANCE.adoc created (proper one; the existing RSR_OUTLINE.adoc is the RSR template's own README, now at docs/RSR_OUTLINE.adoc). Tracks per-category compliance status. * .well-known/ created with security.txt (RFC-9116), ai.txt, humans.txt. * tests/ + tools/ + verification/ directories created per RSR taxonomy. verify-proofs.sh, run-local-verification.sh, and setup-and-verify.sh moved from root into verification/. * Deleted AI.a2ml + AI.djot (superseded; the former was literally boilerplate from rsr-template-repo, never customised). Resolves Hypatia high-severity findings: - root_hygiene: stray AI.a2ml + AI.djot - honest_completion: no_tests (placeholder + cross-reference to where real tests live)
1 parent 3394259 commit 5d770f7

14 files changed

Lines changed: 340 additions & 139 deletions

‎.well-known/ai.txt‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# AI agent discovery file for absolute-zero
3+
# See: https://github.com/hyperpolymath/absolute-zero/blob/main/0-AI-MANIFEST.a2ml
4+
5+
User-Agent: *
6+
Manifest: /0-AI-MANIFEST.a2ml
7+
EntryPoint: /docs/CLAUDE.adoc
8+
State: /.machine_readable/6a2/STATE.a2ml
9+
Roadmap: /ROADMAP.adoc
10+
Allow: training-with-attribution
11+
Allow: documentation-summarisation
12+
Disallow: closed-source-redistribution
13+
License: PMPL-1.0-or-later
14+
Contact: developer@joshuajewell.dev

‎.well-known/humans.txt‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# humanstxt.org
3+
4+
/* TEAM */
5+
Maintainer: Jonathan D. A. Jewell
6+
Contact: developer @ joshuajewell.dev
7+
Site: https://github.com/hyperpolymath/absolute-zero
8+
9+
/* THANKS */
10+
Contributors: see git log + docs/MAINTAINERS.adoc
11+
12+
/* SITE */
13+
Last update: 2026-05-25
14+
Standards: PMPL-1.0-or-later, RSR (Rhodium Standard Repository) compliant
15+
Components: Coq, Lean 4, Z3, Agda, Isabelle, Mizar, Idris2, ReScript, Rust

‎.well-known/security.txt‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
Contact: https://github.com/hyperpolymath/absolute-zero/security/advisories/new
3+
Expires: 2027-05-25T00:00:00Z
4+
Preferred-Languages: en
5+
Canonical: https://github.com/hyperpolymath/absolute-zero/.well-known/security.txt
6+
Policy: https://github.com/hyperpolymath/absolute-zero/blob/main/SECURITY.md

‎0-AI-MANIFEST.a2ml‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# 0-AI-MANIFEST.a2ml — Absolute Zero AI assistant manifest
3+
# Schema: a2ml v1.0
4+
# Supersedes legacy AI.a2ml + AI.djot (deleted in repo tidy 2026-05-25)
5+
6+
[metadata]
7+
project = "absolute-zero"
8+
repo = "github.com/hyperpolymath/absolute-zero"
9+
manifest-version = "1.0"
10+
last-updated = "2026-05-25"
11+
12+
[scope]
13+
purpose = """
14+
Formal verification of Certified Null Operations (CNOs) across multiple
15+
proof systems (Coq, Lean 4, Z3, Agda, Isabelle, Mizar) plus an Idris2
16+
ABI surface for FFI.
17+
"""
18+
19+
[entry-points]
20+
# Where an AI agent should look first.
21+
root-context = "docs/CLAUDE.adoc"
22+
project-state = ".machine_readable/6a2/STATE.a2ml"
23+
roadmap = "ROADMAP.adoc"
24+
contributing = "CONTRIBUTING.adoc"
25+
audit-trail = "AUDIT.adoc"
26+
rsr-status = "RSR_COMPLIANCE.adoc"
27+
28+
[machine-readable]
29+
# Authoritative metadata artefacts; .a2ml format under 6a2/ supersedes
30+
# the older Guile-Scheme .scm format. Both kept side-by-side during the
31+
# migration window for legacy tooling compatibility.
32+
state = ".machine_readable/6a2/STATE.a2ml"
33+
meta = ".machine_readable/6a2/META.a2ml"
34+
ecosystem = ".machine_readable/6a2/ECOSYSTEM.a2ml"
35+
agentic = ".machine_readable/6a2/AGENTIC.a2ml"
36+
neurosym = ".machine_readable/6a2/NEUROSYM.a2ml"
37+
playbook = ".machine_readable/6a2/PLAYBOOK.a2ml"
38+
39+
legacy-scm-meta = ".machine_readable/META.scm"
40+
legacy-scm-ecosystem = ".machine_readable/ECOSYSTEM.scm"
41+
legacy-scm-agentic = ".machine_readable/AGENTIC.scm"
42+
legacy-scm-neurosym = ".machine_readable/NEUROSYM.scm"
43+
legacy-scm-playbook = ".machine_readable/PLAYBOOK.scm"
44+
45+
[language-policy]
46+
# Single source of truth lives in docs/CLAUDE.adoc + .github/workflows/language-policy.yml.
47+
# Summary:
48+
allowed = ["ReScript", "Deno", "Rust", "Tauri", "Dioxus", "Gleam", "Bash", "JavaScript (limited)", "Nickel", "Guile Scheme", "Julia", "OCaml", "Ada", "Idris2"]
49+
banned = ["TypeScript", "Node.js", "npm", "Bun", "pnpm", "yarn", "Go", "Python", "Java", "Kotlin", "Swift", "React Native", "Flutter", "Dart", "Ruby", "Perl"]
50+
reference = "docs/CLAUDE.adoc#language-policy"
51+
52+
[echidna-protocol]
53+
# All ECHIDNA invocations route through the echidna-llm-mcp BoJ cartridge.
54+
# Never call ECHIDNA directly.
55+
gateway = "boj-server/cartridges/echidna-llm-mcp"
56+
docs = "docs/archive/ECHIDNA-2025-11-22.adoc"
57+
tools = [
58+
"echidna_list_provers",
59+
"echidna_prove",
60+
"echidna_verify",
61+
"echidna_verify_raw",
62+
"echidna_suggest",
63+
"echidna_suggest_tactics",
64+
"echidna_search",
65+
"echidna_session_create",
66+
]
67+
68+
[delivery]
69+
commit-policy = "conventional commits; never amend published commits"
70+
state-update = "update .machine_readable/6a2/STATE.a2ml whenever phase/progress changes"
71+
adr-tracking = "architectural changes recorded in .machine_readable/META.scm `architecture-decisions`"

‎AI.a2ml‎

Lines changed: 0 additions & 39 deletions
This file was deleted.

‎AI.djot‎

Lines changed: 0 additions & 100 deletions
This file was deleted.

‎AUDIT.adoc‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= Absolute Zero — Audit Trail
3+
Jonathan D. A. Jewell <developer@joshuajewell.dev>
4+
:toc:
5+
:sectnums:
6+
7+
== Purpose
8+
9+
Estate-wide audit log for absolute-zero. Records all axiom/postulate
10+
discharges, unsoundness findings, deletions of dead code, license
11+
audits, and other trust-boundary events.
12+
13+
For architectural decisions (which are forward-looking design choices
14+
rather than backward-looking audit events), see
15+
`.machine_readable/META.scm` `architecture-decisions`.
16+
17+
== Open Audit Items
18+
19+
|===
20+
|ID |Date filed |Severity |Description |Issue
21+
22+
|AUDIT-2026-05-20-A
23+
|2026-05-20
24+
|Medium
25+
|`src/abi/Types.idr` has 5 pre-existing errors blocking Idris2 0.8.0
26+
typecheck (missing `Decidable.Equality` import; `%runElab` without
27+
`ElabReflection`; `MkStateHandle ptr` doesn't supply the `nonNull`
28+
auto-proof; `No absurd` lacks `Uninhabited` instances).
29+
|TBD (separate from #27)
30+
31+
|AUDIT-2026-05-20-B
32+
|2026-05-20
33+
|Low
34+
|`.github/workflows/cflite_pr.yml` has no `actions/checkout` step
35+
before invoking `build_fuzzers`; the fuzzer job has been silently
36+
failing on every PR.
37+
|TBD
38+
|===
39+
40+
== Resolved Audit Items
41+
42+
|===
43+
|ID |Date resolved |Description |Resolution commit
44+
45+
|AUDIT-2026-05-20-#27
46+
|2026-05-25
47+
|Unsound `alignmentMatchesPlatformWord` postulate (Idris2). The
48+
universal-quantification claim could derive `So (1 mod 8 == 0)` from
49+
the file's own `CNOResultLayout.alignment` since `HasAlignment t n`
50+
carries no evidence about `n`. Companion `alignedSizeCorrect`
51+
postulate isolated into shared `Proofs/DivMod.idr` for
52+
cross-estate incremental discharge.
53+
|aac48b7, f0f9b8f, d2853ca (PR #41 / merged via #40)
54+
55+
|AUDIT-2026-05-20-#24
56+
|2026-05-20
57+
|`eval_deterministic` discharged from Axiom → Theorem via
58+
`step_deterministic_strong` helper. First post-T0 axiom audit win.
59+
|PR #24 (see META.scm ADR-007)
60+
61+
|AUDIT-2026-05-20-#32
62+
|2026-05-20
63+
|Deleted unsound `eval_respects_state_eq_{left,right}` axioms;
64+
weakened `logically_reversible` to observational reversibility
65+
(`=st=`); re-proved `cno_eval_on_equal_states` +
66+
`cno_logically_reversible` via `cno_terminates` +
67+
`cno_preserves_state`.
68+
|PR #32 (see META.scm ADR-008)
69+
70+
|AUDIT-2026-02-05
71+
|2026-02-05
72+
|License canonicalisation across the estate to PMPL-1.0-or-later
73+
(79 files updated). Pre-existing AGPL references reconciled.
74+
|see docs/archive/LICENSE-AUDIT-2026-02-05.adoc
75+
|===
76+
77+
== Audit categorisation
78+
79+
Audit IDs follow `AUDIT-<YYYY-MM-DD>-<seq-or-PR>`:
80+
81+
* PR-numbered IDs map directly to GitHub PRs that close the item.
82+
* Seq-numbered IDs (A, B, C…) are pre-PR findings that still need a
83+
tracking issue or PR.
84+
85+
== See also
86+
87+
* `.machine_readable/META.scm` — forward-looking architecture decisions (ADR-001…N)
88+
* `docs/archive/` — historical session / audit artefacts (dated)
89+
* `RSR_COMPLIANCE.adoc` — Rhodium Standard Repository compliance status

0 commit comments

Comments
 (0)