Skip to content

Commit cec15c5

Browse files
hyperpolymathhyperpolymath
authored
chore(rsr): machine-readable artefacts, Justfile, community-health (#4)
## RSR retrofit — machine-readable artefacts, Justfile, community-health arghda-core had none of the estate's RSR scaffolding (no `.machine_readable/`, no `Justfile`). This adds the mandated, **safe** core. **Deliberately *not* in this PR:** the estate CI-workflow battery (`openssf-compliance`, `estate-rules`, `wellknown-enforcement`, …). Those pull reusable workflows from `standards` that are currently red, and wiring them in would jeopardise this repo's currently-green inlined `rust-ci.yml`. That's a careful, separate step. ### Added - **`.machine_readable/6a2/`** — the six mandated A2ML artefacts (`STATE`, `META`, `ECOSYSTEM`, `AGENTIC`, `NEUROSYM`, `PLAYBOOK`), authored to reflect **arghda-core specifically** (not template residue). `META.a2ml` carries the verbatim maintenance-axis strings the RSR validator greps (`scoping-first = true`, `axis-1 = "must > intend > like"`, `idris-unsound-scan = "believe_me/assert_total"`, …). - **`0-AI-MANIFEST.a2ml`** — root AI entry point (read-order, allocation, and the "arghda never proves" policy). - **`Justfile`** — real recipes wrapping the cargo gates: `build`, `test`, `fmt`/`fmt-check`, `lint`, `check` (= the exact CI gate), `scan`/`dag`/`agda-check`, and `validate-rsr`/`validate`. - **`.well-known/`** — `security.txt` (RFC 9116), `ai.txt`, `humans.txt`. - **`SECURITY.md`, `CONTRIBUTING.md`, `CHANGELOG.md`**. ### Discipline - New files carry MPL-2.0 SPDX from birth; existing `.rs` files are **not** swept (estate licence guardrail). **No source/logic changed** — purely additive. ### Verification - `just check` (fmt-check + clippy `-D warnings` + build + test) green **via the new recipes**; `just validate-rsr` passes. 28 tests unchanged. ### Deferred (follow-ups) The CI-gate workflows, `guix.scm`/`flake.nix` dev-shells, the contractiles, and the optional `.adoc` authority docs (`EXPLAINME`/`GOVERNANCE`/`MAINTAINERS`/`AUDIT`/`AFFIRMATION`). Draft for review. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- _Generated by [Claude Code](https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs)_
2 parents 4802018 + 62e0fe9 commit cec15c5

14 files changed

Lines changed: 468 additions & 0 deletions

File tree

‎.machine_readable/6a2/AGENTIC.a2ml‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# AGENTIC.a2ml — AI agent constraints and capabilities
5+
6+
[metadata]
7+
version = "0.1.0"
8+
last-updated = "2026-06-18"
9+
10+
[agent-permissions]
11+
can-edit-source = true
12+
can-edit-tests = true
13+
can-edit-docs = true
14+
can-edit-config = true
15+
can-create-files = true
16+
17+
[agent-constraints]
18+
# What AI agents must NOT do:
19+
# - arghda never proves: do not embed a prover or claim a result Agda did not return.
20+
# - Never commit secrets or credentials.
21+
# - Never bulk-sweep SPDX headers (estate licence guardrail); new files may carry MPL-2.0 from birth.
22+
# - Never place state files in repository root (must be in .machine_readable/).
23+
# - Never use the AGPL license (use MPL-2.0).
24+
# - Keep `just check` (fmt + clippy -D warnings + build + test) green on every change.
25+
26+
[maintenance-integrity]
27+
fail-closed = true
28+
require-evidence-per-step = true
29+
allow-silent-skip = false
30+
require-rerun-after-fix = true
31+
release-claim-requires-hard-pass = true
32+
33+
[methodology]
34+
default-mode = "hybrid"
35+
36+
[automation-hooks]
37+
# on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml
38+
# on-exit: Update STATE.a2ml with session outcomes
39+
# on-commit: Run `just check`

‎.machine_readable/6a2/ECOSYSTEM.a2ml‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# ECOSYSTEM.a2ml — Position in the hyperpolymath ecosystem
5+
6+
[metadata]
7+
project = "arghda-core"
8+
ecosystem = "hyperpolymath"
9+
10+
[position]
11+
type = "engine"
12+
purpose = "The language-agnostic proof-workspace engine for the arghda visual proof-wiring tool. Targets Agda first; the LintRule trait is the extension point for further provers."
13+
14+
[pipeline]
15+
position = "proof-organisation layer (rides alongside the research-to-production pipeline)"
16+
chain = "standards -> rsr-template-repo -> arghda-core"
17+
coordination = "standards"
18+
19+
[related-projects]
20+
projects = [
21+
{ name = "arghda-studio", relationship = "downstream-consumer", notes = "Planned AffineScript -> typed-wasm visual layer; consumes the dag JSON + events.jsonl contract; v1 renders static SVG/HTML." },
22+
{ name = "arghda-panll", relationship = "downstream-consumer", notes = "Planned PanLL panel embedding, discovered via the Groove protocol." },
23+
{ name = "echo-types", relationship = "dogfood-workspace", notes = "Constructive Agda corpus; arghda's first real workspace. Not a build dependency." },
24+
{ name = "absolute-zero", relationship = "dogfood-workspace", notes = "Sister Agda corpus under the same --safe --without-K discipline." },
25+
{ name = "echidna", relationship = "verification-backend", notes = "Multi-prover orchestrator (Unified Zig API service #3, port 8090); arghda dispatches goals to it." },
26+
{ name = "standards", relationship = "standard-source", notes = "Estate language / licence / RSR policy." },
27+
{ name = "rsr-template-repo", relationship = "scaffold-source", notes = "RSR compliance template this repo is being aligned to." },
28+
]

‎.machine_readable/6a2/META.a2ml‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# META.a2ml — Project meta-level information
5+
# Architecture decisions, design rationale, governance.
6+
7+
[metadata]
8+
version = "0.1.0"
9+
last-updated = "2026-06-18"
10+
11+
[project-info]
12+
type = "library" # library | binary | monorepo | service | website
13+
languages = ["rust"]
14+
license = "MPL-2.0"
15+
author = "Jonathan D.A. Jewell (hyperpolymath)"
16+
17+
[architecture-decisions]
18+
# status = proposed | accepted | deprecated | superseded | rejected
19+
# - { id = "ADR-001", title = "Rust for the language-agnostic engine", status = "accepted", date = "2026-05-30" }
20+
# - { id = "ADR-002", title = "Triage transitions are file moves; ground truth is the filesystem", status = "accepted", date = "2026-05-30" }
21+
# - { id = "ADR-003", title = "Dependency-free RFC 3339 timestamps (hermetic build, no chrono)", status = "accepted", date = "2026-06-18" }
22+
# - { id = "ADR-004", title = "Orphan reachability is the union of discovered CI roots (All.agda/Smoke.agda)", status = "accepted", date = "2026-06-18" }
23+
24+
[development-practices]
25+
build-tool = "just"
26+
container-runtime = "podman"
27+
ci-platform = "github-actions"
28+
package-manager = "cargo" # Rust crate; guix/nix dev-shells are a future addition.
29+
30+
[maintenance-axes]
31+
scoping-first = true
32+
execution-order = "axis-1 > axis-2 > axis-3"
33+
axis-1 = "must > intend > like"
34+
axis-2 = "corrective > adaptive > perfective"
35+
axis-3 = "systems > compliance > effects"
36+
37+
[scoping]
38+
sources = "README, roadmap, status docs, maintenance checklist, CI/security docs"
39+
marker-scan = "TODO/FIXME/XXX/HACK/STUB/PARTIAL"
40+
idris-unsound-scan = "believe_me/assert_total"
41+
42+
[axis-2-maintenance-rules]
43+
corrective-first = true
44+
adaptive-second = true
45+
adaptive-focus = "scope-change reconciliation, stale-reference removal, obsolete-work culling"
46+
perfective-third = true
47+
perfective-source = "axis-1 honest state after corrective/adaptive updates"
48+
49+
[axis-3-audit-rules]
50+
audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"
51+
compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"
52+
drift-risk-example = "single exception broadening into policy violation (e.g. ReScript->TypeScript spread)"
53+
effects-evidence = "benchmark execution/results and maintainer status dialogue/review"
54+
55+
[design-rationale]
56+
# arghda-core is the engine half of the arghda split (engine in Rust;
57+
# arghda-studio presentation in AffineScript -> typed-wasm). It organises,
58+
# lints, and emits the DAG / events.jsonl JSON contract a visual layer
59+
# consumes. It never proves: Agda (directly, or via echidna) proves.

‎.machine_readable/6a2/NEUROSYM.a2ml‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# NEUROSYM.a2ml — Hypatia / symbolic-scan configuration
5+
6+
[metadata]
7+
version = "0.1.0"
8+
last-updated = "2026-06-18"
9+
10+
[hypatia-config]
11+
scan-enabled = true
12+
scan-depth = "standard" # quick | standard | deep
13+
report-format = "logtalk"
14+
15+
[symbolic-rules]
16+
# Repo-local symbolic checks (severity = critical | warn | info):
17+
# - { name = "no-unsafe-rust", pattern = "unsafe ", severity = "warn" }
18+
# - { name = "no-panic-on-io", pattern = "\\.unwrap\\(\\)", severity = "info" }
19+
# Note: arghda's own lint rules (missing-safe-pragma, orphan-module,
20+
# unjustified-postulate, escape-hatch, tab-mix) are the symbolic layer it
21+
# applies to *Agda* workspaces; this section is for scanning *this* repo.
22+
23+
[neural-config]
24+
# confidence-threshold = 0.85

‎.machine_readable/6a2/PLAYBOOK.a2ml‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# PLAYBOOK.a2ml — Operational runbook
5+
6+
[metadata]
7+
version = "0.1.0"
8+
last-updated = "2026-06-18"
9+
10+
[build]
11+
# Debug: just build (cargo build --all-targets)
12+
# Release: just build-release (binary: target/release/arghda)
13+
14+
[test]
15+
# just test — cargo test (unit + integration: dag, transitions, smoke)
16+
# just check — the full CI gate: fmt-check + clippy -D warnings + build + test
17+
18+
[usage]
19+
# Lint a tree: just scan <path> (arghda scan <path>)
20+
# Emit the DAG (JSON): just dag <path> (arghda dag <path>)
21+
# Typecheck one file: arghda check <file> (needs `agda` on PATH; degrades gracefully)
22+
# Triage workspace: arghda init <ws>
23+
# arghda claim|promote|reject|requeue|invalidate <ws> <file>
24+
# arghda events <ws>
25+
26+
[release-process]
27+
# 1. Update CHANGELOG.md; bump version in Cargo.toml + the 6a2 files.
28+
# 2. `just check` must pass.
29+
# 3. Tag v<x.y.z>; push.
30+
31+
[maintenance-operations]
32+
# Run `just validate` (validate-rsr + check) before claiming release-ready.
33+
# Re-dogfood `just dag <echo-types>/proofs/agda` after any engine change and
34+
# confirm the node/edge/blocked counts move as expected.

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# STATE.a2ml — Project state checkpoint
5+
6+
[metadata]
7+
project = "arghda-core"
8+
version = "0.1.0"
9+
last-updated = "2026-06-18"
10+
status = "active" # active | paused | archived
11+
12+
[project-context]
13+
name = "arghda-core"
14+
purpose = "Lightweight proof-workspace manager for Agda — the language-agnostic engine half of arghda. A four-state triage workspace (inbox/working/proven/rejected) as file moves, a lint pack targeting the silent-failure class, a first-class import-graph DAG, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. It never proves anything; Agda does."
15+
completion-percentage = 55
16+
17+
[position]
18+
phase = "implementation" # design | implementation | testing | maintenance | archived
19+
maturity = "alpha" # experimental | alpha | beta | production | lts
20+
21+
[route-to-mvp]
22+
milestones = [
23+
{ name = "Workspace scaffold + filesystem watcher", completion = 100 },
24+
{ name = "Lint pack (missing-safe-pragma, orphan-module, unjustified-postulate, escape-hatch, tab-mix)", completion = 100 },
25+
{ name = "First-class import graph + `dag` JSON command", completion = 100 },
26+
{ name = "State machine (claim/promote/reject/requeue/invalidate) + events.jsonl", completion = 100 },
27+
{ name = "`check` command (Agda typecheck + lint verdict)", completion = 100 },
28+
{ name = "Multi-root reachability (union of discovered CI roots)", completion = 100 },
29+
{ name = "Remaining lint rules (unpinned-headline, unused-import)", completion = 0 },
30+
{ name = "Content-hash invalidation of proven", completion = 0 },
31+
{ name = "Groove service manifest (/.well-known/groove)", completion = 0 },
32+
{ name = "RSR retrofit (.machine_readable, Justfile, .well-known)", completion = 60 },
33+
]
34+
35+
[blockers-and-issues]
36+
# No active blockers. `unpinned-headline` needs Smoke.agda parsing + a
37+
# configurable headline regex; `unused-import` shells out to `agda-unused`.
38+
39+
[critical-next-actions]
40+
actions = [
41+
"Add unpinned-headline + unused-import lint rules",
42+
"Content-hash proven files (SHA-256 of file + imports) for auto-invalidation",
43+
"Serve /.well-known/groove for PanLL discovery",
44+
"Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)",
45+
]
46+
47+
[maintenance-status]
48+
last-run-utc = "never"
49+
last-result = "unknown" # unknown | pass | warn | fail
50+
open-warnings = 0
51+
open-failures = 0
52+
53+
[ecosystem]
54+
part-of = ["arghda"]
55+
depends-on = []
56+
# Downstream consumers: arghda-studio (planned), arghda-panll (planned).
57+
# Dogfood workspaces: echo-types, absolute-zero.

‎.well-known/ai.txt‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# ai.txt — AI interaction policy for arghda-core.
3+
User-Agent: *
4+
Allow: /
5+
Purpose: Lightweight proof-workspace manager for Agda (the language-agnostic engine). Source is MPL-2.0; reuse is welcome under that licence.
6+
Contact: mailto:j.d.a.jewell@open.ac.uk

‎.well-known/humans.txt‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
/* TEAM */
3+
Author: Jonathan D.A. Jewell (hyperpolymath)
4+
Contact: j.d.a.jewell [at] open.ac.uk
5+
6+
/* PROJECT */
7+
Name: arghda-core
8+
Purpose: proof-workspace manager for Agda (engine)
9+
Standard: Rhodium Standard Repository (RSR)
10+
Components: Rust
11+
License: MPL-2.0

‎.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: MPL-2.0
2+
# RFC 9116 security contact for arghda-core.
3+
Contact: mailto:j.d.a.jewell@open.ac.uk
4+
Expires: 2027-06-18T00:00:00Z
5+
Preferred-Languages: en
6+
Canonical: https://github.com/hyperpolymath/arghda-core/blob/main/.well-known/security.txt

‎0-AI-MANIFEST.a2ml‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# 0-AI-MANIFEST.a2ml — AI agent entry point (read first)
5+
6+
[metadata]
7+
version = "0.1.0"
8+
last-updated = "2026-06-18"
9+
10+
[project]
11+
name = "arghda-core"
12+
purpose = "Language-agnostic proof-workspace engine for the arghda visual proof-wiring tool (Agda first). Emits the DAG / events.jsonl JSON contract a visual layer consumes; never proves anything itself."
13+
14+
[entry]
15+
read-order = [
16+
".machine_readable/6a2/STATE.a2ml",
17+
".machine_readable/6a2/META.a2ml",
18+
"README.md",
19+
"docs/arghda-spec.adoc",
20+
"docs/arghda-vision.adoc",
21+
]
22+
23+
[ai-allocation]
24+
agents = [
25+
{ name = "CLAUDE", role = "Rust engine, lint rules, Agda integration, CI/CD, formal-tooling glue" },
26+
{ name = "CHATGPT", role = "prose, spec/vision docs, outreach drafts" },
27+
{ name = "GEMINI", role = "cross-repo audits, dogfood triage, pattern detection" },
28+
{ name = "VIBE", role = "arghda-studio UI / PanLL panel (AffineScript)" },
29+
]
30+
31+
[policy]
32+
rules = [
33+
"arghda organises and communicates proofs; Agda proves. Never embed a prover or claim an unverified result.",
34+
"Do not bulk-sweep SPDX headers; new files may carry MPL-2.0 from birth.",
35+
"Update STATE.a2ml during sessions; do not create per-repo TODO files.",
36+
"Keep `just check` green on every change.",
37+
]

0 commit comments

Comments
 (0)