refactor: migrate Markdown to AsciiDoc

.machine_readable/6a2/META.a2ml

@@ -28,7 +28,7 @@ author = "Jonathan D.A. Jewell (hyperpolymath)"
 build-tool = "just"
 container-runtime = "podman"
 ci-platform = "github-actions"
-package-manager = "cargo"  # Rust crate; guix/nix dev-shells are a future addition.
+package-manager = "cargo"  # Rust crate; guix/guix dev-shells are a future addition.
 
 [maintenance-axes]
 scoping-first = true
@@ -52,7 +52,7 @@ 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)"
+drift-risk-example = "single exception broadening into policy violation (e.g. AffineScript->TypeScript spread)"
 effects-evidence = "benchmark execution/results and maintainer status dialogue/review"
 
 [design-rationale]

.machine_readable/rsr-profile.a2ml

@@ -19,6 +19,6 @@ remove = []   # preset capabilities this repo does NOT have
 no-abi = "language-agnostic engine; no C-ABI/FFI seam, no Idris2 ABI proofs (no abi.ipkg / src/interface/)"
 no-formal-proofs = "consumes Agda — shells out to agda / agda-unused — but contains no in-tree proofs (no verification/proofs/)"
 no-container = "ships a CLI binary, not a container image"
-no-reproducible-build = "cargo build only for now; guix.scm / flake.nix are a future addition, not present"
+no-reproducible-build = "cargo build only for now; guix.scm / flake.guix are a future addition, not present"
 no-affinescript = "pure Rust; the planned AffineScript visual layer is a separate repo (arghda-studio)"
 no-governance-tier = "leaf tool; declines the full AUDIT / AFFIRMATION / GOVERNANCE / MAINTAINERS trio"

ARCHITECTURE.adoc

@@ -0,0 +1,48 @@
+== Architecture
+
+=== Overview
+
+This repository follows a modular, maintainable architecture designed
+for clarity, scalability, and long-term sustainability.
+
+=== Directory Structure
+
+....
+.
+├── src/           # Source code
+├── tests/        # Test suites
+├── docs/         # Documentation
+├── scripts/      # Utility scripts
+├── config/       # Configuration files
+├── LICENSE       # License file
+├── LICENSES/     # Full license texts
+└── README.adoc   # Project documentation
+....
+
+=== Design Principles
+
+* *Separation of Concerns*: Each module has a single responsibility
+* *Testability*: Code is written to be easily testable
+* *Documentation*: All public APIs are documented
+* *Configuration*: Environment-specific settings are externalized
+
+=== Dependencies
+
+* External dependencies are minimized and clearly declared
+* Version pinning is used for reproducibility
+
+=== Security Considerations
+
+* Sensitive data is never committed to the repository
+* Secrets are managed through environment variables or secure vaults
+* Regular dependency audits are performed
+
+=== Maintainability
+
+* Code follows consistent style guidelines
+* Pull requests require review and CI checks
+* Issues and discussions are tracked transparently
+
+'''''
+
+_Last updated: 2026-07-18_

CHANGELOG.adoc

@@ -0,0 +1,92 @@
+== Changelog
+
+All notable changes to arghda-core are documented here. The format
+follows https://keepachangelog.com/[Keep a Changelog], and this project
+adheres to https://semver.org/[Semantic Versioning].
+
+=== [Unreleased]
+
+==== Changed
+
+* Standards / RSR alignment and root cleanup: `+README.md+` →
+`+README.adoc+` (adoc-first; refreshed to the feature-complete v0.1
+status), no duplicate doc formats. Added `+EXPLAINME.adoc+` (orientation
+pointer), `+LICENSE+` (full MPL-2.0 text), and `+CODE_OF_CONDUCT.md+`
+(Contributor Covenant 2.1). Prose docs carry `+CC-BY-SA-4.0+`;
+code/config/state stay `+MPL-2.0+` (per the estate licence policy).
+Refreshed `+.machine_readable/6a2/STATE.a2ml+` + `+META.a2ml+` and the
+`+0-AI-MANIFEST.a2ml+` read-order; removed local `+dist-newstyle/+`
+build cruft.
+* Formal SPDX licence invariant (owner-directed): every tracked file
+carries the correct header — `+MPL-2.0+` for code/config/scripts/state,
+`+CC-BY-SA-4.0+` for prose — applied per file (incl. all `+src/*.rs+`)
+and enforced by `+scripts/check-spdx.sh+`, wired into `+just check+` and
+Rust CI. Third-party, generated (`+Cargo.lock+`), and test-data
+(`+tests/fixtures/+`) files are explicitly excluded and never
+relicensed; `+docs/*.adoc+` normalised from `+CC-BY-4.0+` to
+`+CC-BY-SA-4.0+`. Declared in
+`+.machine_readable/licensing-policy.toml+`.
+
+==== 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).
+* `+unpinned-headline+` (warn): flags a top-level theorem whose name
+matches the headline pattern but is not pinned in any `+Smoke.agda+` via
+a `+using ( … )+` clause. The pattern is operator-configurable via
+`+--headline-pattern <regex>+` on `+scan+` / `+dag+` (default
+`+^[a-z][A-Za-z0-9-]*$+`, per the spec). Detects top-level (column-0)
+signatures only, which gives the export-only filter for free; tolerant
+of multi-line `+using+` lists; self-skips when no `+Smoke.agda+` is in
+scope.
+* `+unused-import+` (warn): re-emits the findings of the external
+`+agda-unused+` tool (spec §Linter rules). Opt-in behind
+`+scan --unused+`; runs `+agda-unused+` per file in local mode with
+`+LC_ALL=C.UTF-8+`, parses its `+--json+` output, and re-emits each
+finding as an `+unused-import+` warning attributed to the file. Degrades
+gracefully (with a note) when `+agda-unused+` is not on `+PATH+`,
+mirroring how `+check+` tolerates a missing `+agda+`.
+* `+.arghda/config.toml+` operator configuration (the spec’s
+open-question surface): `+scan+` / `+dag+` read a
+`+[lint] headline_pattern+` override from `+<PATH>/.arghda/config.toml+`
+(or an explicit `+--config <file>+`). Precedence is built-in default <
+`+config.toml+` < CLI `+--headline-pattern+`. Missing file ⇒ defaults;
+unknown keys are rejected so typos surface.
+* DAG `+headlines+` field: each `+dag+` node now carries the sorted,
+deduped list of top-level headline theorem names it declares (the spec’s
+per-node `+headlines+` array), extracted with the same logic as
+`+unpinned-headline+` and honouring the configured headline pattern.
+Completes the v0 DAG schema.
+* RSR scaffolding: `+.machine_readable/6a2/+` artefacts,
+`+0-AI-MANIFEST.a2ml+`, `+Justfile+`, `+.well-known/+`, and
+community-health files.
+* Content-hash invalidation of `+proven+`: promotion records a SHA-256
+of the file in `+.arghda/hashes.json+`; the `+stale+` command reports
+proven files edited since promotion, and `+stale --invalidate+` moves
+them back to inbox (the `+proven -> inbox+` invalidation).
+Dependency-free SHA-256, pinned against the NIST test vectors.
+
+==== 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.

CODE_OF_CONDUCT.adoc

@@ -0,0 +1,8 @@
+== Code of Conduct
+
+This project follows the
+https://www.contributor-covenant.org/version/2/1/code_of_conduct/[Contributor
+Covenant 2.1].
+
+Reports go to `+j.d.a.jewell@open.ac.uk+`. Reports are confidential by
+default.

CONTRIBUTING.adoc

@@ -0,0 +1,34 @@
+== 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
+
+[arabic]
+. Branch from `+main+`.
+. Make the change; `+just check+` must pass.
+. 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.