chore(rsr): machine-readable artefacts, Justfile, community-health

.machine_readable/6a2/AGENTIC.a2ml

@@ -0,0 +1,39 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# AGENTIC.a2ml — AI agent constraints and capabilities
+
+[metadata]
+version = "0.1.0"
+last-updated = "2026-06-18"
+
+[agent-permissions]
+can-edit-source = true
+can-edit-tests = true
+can-edit-docs = true
+can-edit-config = true
+can-create-files = true
+
+[agent-constraints]
+# What AI agents must NOT do:
+# - arghda never proves: do not embed a prover or claim a result Agda did not return.
+# - Never commit secrets or credentials.
+# - Never bulk-sweep SPDX headers (estate licence guardrail); new files may carry MPL-2.0 from birth.
+# - Never place state files in repository root (must be in .machine_readable/).
+# - Never use the AGPL license (use MPL-2.0).
+# - Keep `just check` (fmt + clippy -D warnings + build + test) green on every change.
+
+[maintenance-integrity]
+fail-closed = true
+require-evidence-per-step = true
+allow-silent-skip = false
+require-rerun-after-fix = true
+release-claim-requires-hard-pass = true
+
+[methodology]
+default-mode = "hybrid"
+
+[automation-hooks]
+# on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml
+# on-exit:  Update STATE.a2ml with session outcomes
+# on-commit: Run `just check`

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -0,0 +1,28 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# ECOSYSTEM.a2ml — Position in the hyperpolymath ecosystem
+
+[metadata]
+project = "arghda-core"
+ecosystem = "hyperpolymath"
+
+[position]
+type = "engine"
+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."
+
+[pipeline]
+position = "proof-organisation layer (rides alongside the research-to-production pipeline)"
+chain = "standards -> rsr-template-repo -> arghda-core"
+coordination = "standards"
+
+[related-projects]
+projects = [
+  { 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." },
+  { name = "arghda-panll", relationship = "downstream-consumer", notes = "Planned PanLL panel embedding, discovered via the Groove protocol." },
+  { name = "echo-types", relationship = "dogfood-workspace", notes = "Constructive Agda corpus; arghda's first real workspace. Not a build dependency." },
+  { name = "absolute-zero", relationship = "dogfood-workspace", notes = "Sister Agda corpus under the same --safe --without-K discipline." },
+  { name = "echidna", relationship = "verification-backend", notes = "Multi-prover orchestrator (Unified Zig API service #3, port 8090); arghda dispatches goals to it." },
+  { name = "standards", relationship = "standard-source", notes = "Estate language / licence / RSR policy." },
+  { name = "rsr-template-repo", relationship = "scaffold-source", notes = "RSR compliance template this repo is being aligned to." },
+]

.machine_readable/6a2/META.a2ml

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

.machine_readable/6a2/NEUROSYM.a2ml

@@ -0,0 +1,24 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# NEUROSYM.a2ml — Hypatia / symbolic-scan configuration
+
+[metadata]
+version = "0.1.0"
+last-updated = "2026-06-18"
+
+[hypatia-config]
+scan-enabled = true
+scan-depth = "standard"  # quick | standard | deep
+report-format = "logtalk"
+
+[symbolic-rules]
+# Repo-local symbolic checks (severity = critical | warn | info):
+# - { name = "no-unsafe-rust", pattern = "unsafe ", severity = "warn" }
+# - { name = "no-panic-on-io", pattern = "\\.unwrap\\(\\)", severity = "info" }
+# Note: arghda's own lint rules (missing-safe-pragma, orphan-module,
+# unjustified-postulate, escape-hatch, tab-mix) are the symbolic layer it
+# applies to *Agda* workspaces; this section is for scanning *this* repo.
+
+[neural-config]
+# confidence-threshold = 0.85

.machine_readable/6a2/PLAYBOOK.a2ml

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

.machine_readable/6a2/STATE.a2ml

@@ -0,0 +1,57 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# STATE.a2ml — Project state checkpoint
+
+[metadata]
+project = "arghda-core"
+version = "0.1.0"
+last-updated = "2026-06-18"
+status = "active"  # active | paused | archived
+
+[project-context]
+name = "arghda-core"
+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."
+completion-percentage = 55
+
+[position]
+phase = "implementation"   # design | implementation | testing | maintenance | archived
+maturity = "alpha"         # experimental | alpha | beta | production | lts
+
+[route-to-mvp]
+milestones = [
+  { name = "Workspace scaffold + filesystem watcher", completion = 100 },
+  { name = "Lint pack (missing-safe-pragma, orphan-module, unjustified-postulate, escape-hatch, tab-mix)", completion = 100 },
+  { name = "First-class import graph + `dag` JSON command", completion = 100 },
+  { name = "State machine (claim/promote/reject/requeue/invalidate) + events.jsonl", completion = 100 },
+  { name = "`check` command (Agda typecheck + lint verdict)", completion = 100 },
+  { name = "Multi-root reachability (union of discovered CI roots)", completion = 100 },
+  { name = "Remaining lint rules (unpinned-headline, unused-import)", completion = 0 },
+  { name = "Content-hash invalidation of proven", completion = 0 },
+  { name = "Groove service manifest (/.well-known/groove)", completion = 0 },
+  { name = "RSR retrofit (.machine_readable, Justfile, .well-known)", completion = 60 },
+]
+
+[blockers-and-issues]
+# No active blockers. `unpinned-headline` needs Smoke.agda parsing + a
+# configurable headline regex; `unused-import` shells out to `agda-unused`.
+
+[critical-next-actions]
+actions = [
+  "Add unpinned-headline + unused-import lint rules",
+  "Content-hash proven files (SHA-256 of file + imports) for auto-invalidation",
+  "Serve /.well-known/groove for PanLL discovery",
+  "Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)",
+]
+
+[maintenance-status]
+last-run-utc = "never"
+last-result = "unknown"  # unknown | pass | warn | fail
+open-warnings = 0
+open-failures = 0
+
+[ecosystem]
+part-of = ["arghda"]
+depends-on = []
+# Downstream consumers: arghda-studio (planned), arghda-panll (planned).
+# Dogfood workspaces: echo-types, absolute-zero.

.well-known/ai.txt

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

.well-known/humans.txt

@@ -0,0 +1,11 @@
+# SPDX-License-Identifier: MPL-2.0
+/* TEAM */
+  Author: Jonathan D.A. Jewell (hyperpolymath)
+  Contact: j.d.a.jewell [at] open.ac.uk
+
+/* PROJECT */
+  Name: arghda-core
+  Purpose: proof-workspace manager for Agda (engine)
+  Standard: Rhodium Standard Repository (RSR)
+  Components: Rust
+  License: MPL-2.0

.well-known/security.txt

@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# RFC 9116 security contact for arghda-core.
+Contact: mailto:j.d.a.jewell@open.ac.uk
+Expires: 2027-06-18T00:00:00Z
+Preferred-Languages: en
+Canonical: https://github.com/hyperpolymath/arghda-core/blob/main/.well-known/security.txt

0-AI-MANIFEST.a2ml

@@ -0,0 +1,37 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# 0-AI-MANIFEST.a2ml — AI agent entry point (read first)
+
+[metadata]
+version = "0.1.0"
+last-updated = "2026-06-18"
+
+[project]
+name = "arghda-core"
+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."
+
+[entry]
+read-order = [
+  ".machine_readable/6a2/STATE.a2ml",
+  ".machine_readable/6a2/META.a2ml",
+  "README.md",
+  "docs/arghda-spec.adoc",
+  "docs/arghda-vision.adoc",
+]
+
+[ai-allocation]
+agents = [
+  { name = "CLAUDE", role = "Rust engine, lint rules, Agda integration, CI/CD, formal-tooling glue" },
+  { name = "CHATGPT", role = "prose, spec/vision docs, outreach drafts" },
+  { name = "GEMINI", role = "cross-repo audits, dogfood triage, pattern detection" },
+  { name = "VIBE", role = "arghda-studio UI / PanLL panel (AffineScript)" },
+]
+
+[policy]
+rules = [
+  "arghda organises and communicates proofs; Agda proves. Never embed a prover or claim an unverified result.",
+  "Do not bulk-sweep SPDX headers; new files may carry MPL-2.0 from birth.",
+  "Update STATE.a2ml during sessions; do not create per-repo TODO files.",
+  "Keep `just check` green on every change.",
+]

CHANGELOG.md

@@ -0,0 +1,39 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+# Changelog
+
+All notable changes to arghda-core are documented here. The format follows
+[Keep a Changelog](https://keepachangelog.com/), and this project adheres to
+[Semantic Versioning](https://semver.org/).
+
+## [Unreleased]
+
+### Added
+
+- `dag` command emitting the dependency-DAG JSON contract (nodes with
+  lint-derived status, import edges, and a `blocked` list covering
+  self-blocks and prerequisite-blocks).
+- `check` command: Agda typecheck fused with the lint report
+  (`proven-eligible` / `rejected` / `agda-unavailable`); degrades gracefully
+  when `agda` is absent.
+- Workspace state machine — `claim` / `promote` / `reject` / `requeue` /
+  `invalidate` as validated file moves, each logged to
+  `.arghda/events.jsonl`; plus `events` to replay the log.
+- First-class import graph (`graph` module) with multi-root reachability:
+  orphan detection is the union of auto-discovered `All.agda` / `Smoke.agda`
+  CI roots (or `--entry`, repeatable).
+- Lint rules: `unjustified-postulate` (hard-block), `escape-hatch` (warn:
+  `TERMINATING`-family pragmas + `believe_me` / `primTrustMe`), `tab-mix`
+  (warn).
+- RSR scaffolding: `.machine_readable/6a2/` artefacts, `0-AI-MANIFEST.a2ml`,
+  `Justfile`, `.well-known/`, and community-health files.
+
+### Notes
+
+- Verified against Agda 2.6.3 and dogfooded on the echo-types corpus
+  (193 modules, 903 import edges; the known `VarianceGate.agda` orphan and
+  the out-of-cone files are surfaced correctly).
+
+## [0.1.0] — 2026-05-30
+
+- Initial extraction from echo-types: workspace scaffold, filesystem
+  watcher, `missing-safe-pragma` + `orphan-module` lints, and the `scan` CLI.

CONTRIBUTING.md

@@ -0,0 +1,33 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+# Contributing to arghda-core
+
+arghda-core is the Rust engine for the arghda proof-workspace tool.
+
+## Ground rules
+
+- **arghda never proves.** Agda (directly, or via echidna) proves; arghda
+  organises, lints, and emits the DAG / event JSON. Don't add a prover or
+  claim a result Agda didn't return.
+- **Licence:** MPL-2.0. New files carry an SPDX header from birth. Don't
+  bulk-rewrite existing headers.
+- **Green gate.** Every change keeps `just check`
+  (`cargo fmt --check` + `clippy -D warnings` + `build` + `test`) green,
+  and adds tests for new behaviour.
+
+## Workflow
+
+1. Branch from `main`.
+2. Make the change; `just check` must pass.
+3. Open a PR. CI runs build / test / clippy / fmt.
+
+## Layout
+
+- `src/` — the library plus the thin `arghda` CLI (`src/main.rs`).
+- `src/lint/` — one module per lint rule (`LintRule` trait is the
+  extension point).
+- `src/graph.rs` — the first-class Agda import graph.
+- `tests/` — integration tests; `tests/fixtures/` — tiny Agda fixtures.
+- `docs/` — `.adoc` spec (`arghda-spec.adoc`) and vision/roadmap
+  (`arghda-vision.adoc`).
+- `.machine_readable/6a2/` — RSR machine-readable state; update
+  `STATE.a2ml` as work lands.