From 62e0fe967e5e9b157a4483f4c79d1c7146f4a362 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 15:14:12 +0000 Subject: [PATCH] chore(rsr): retrofit machine-readable artefacts, Justfile, community-health MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The repo had none of the estate's RSR scaffolding (no .machine_readable/, no Justfile). This adds the mandated, safe core — deliberately NOT the estate CI-workflow battery, which pulls reusable workflows that are red and would jeopardise the currently-green build (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. - `0-AI-MANIFEST.a2ml` — root AI entry point (read-order + allocation + 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` (community-health). Discipline - New files carry MPL-2.0 SPDX from birth; existing `.rs` files are NOT swept (estate licence guardrail). No source/logic changed. 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 (openssf-compliance, estate-rules, wellknown-enforcement, etc.), guix.scm/flake.nix dev-shells, the contractiles, and the optional .adoc authority docs (EXPLAINME/GOVERNANCE/MAINTAINERS/AUDIT/AFFIRMATION). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- .machine_readable/6a2/AGENTIC.a2ml | 39 +++++++++++++++++ .machine_readable/6a2/ECOSYSTEM.a2ml | 28 +++++++++++++ .machine_readable/6a2/META.a2ml | 59 ++++++++++++++++++++++++++ .machine_readable/6a2/NEUROSYM.a2ml | 24 +++++++++++ .machine_readable/6a2/PLAYBOOK.a2ml | 34 +++++++++++++++ .machine_readable/6a2/STATE.a2ml | 57 +++++++++++++++++++++++++ .well-known/ai.txt | 6 +++ .well-known/humans.txt | 11 +++++ .well-known/security.txt | 6 +++ 0-AI-MANIFEST.a2ml | 37 ++++++++++++++++ CHANGELOG.md | 39 +++++++++++++++++ CONTRIBUTING.md | 33 +++++++++++++++ Justfile | 63 ++++++++++++++++++++++++++++ SECURITY.md | 32 ++++++++++++++ 14 files changed, 468 insertions(+) create mode 100644 .machine_readable/6a2/AGENTIC.a2ml create mode 100644 .machine_readable/6a2/ECOSYSTEM.a2ml create mode 100644 .machine_readable/6a2/META.a2ml create mode 100644 .machine_readable/6a2/NEUROSYM.a2ml create mode 100644 .machine_readable/6a2/PLAYBOOK.a2ml create mode 100644 .machine_readable/6a2/STATE.a2ml create mode 100644 .well-known/ai.txt create mode 100644 .well-known/humans.txt create mode 100644 .well-known/security.txt create mode 100644 0-AI-MANIFEST.a2ml create mode 100644 CHANGELOG.md create mode 100644 CONTRIBUTING.md create mode 100644 Justfile create mode 100644 SECURITY.md diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/6a2/AGENTIC.a2ml new file mode 100644 index 0000000..01d7901 --- /dev/null +++ b/.machine_readable/6a2/AGENTIC.a2ml @@ -0,0 +1,39 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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` diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml new file mode 100644 index 0000000..8b22a83 --- /dev/null +++ b/.machine_readable/6a2/ECOSYSTEM.a2ml @@ -0,0 +1,28 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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." }, +] diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml new file mode 100644 index 0000000..347bb70 --- /dev/null +++ b/.machine_readable/6a2/META.a2ml @@ -0,0 +1,59 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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. diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/6a2/NEUROSYM.a2ml new file mode 100644 index 0000000..d76275c --- /dev/null +++ b/.machine_readable/6a2/NEUROSYM.a2ml @@ -0,0 +1,24 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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 diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/6a2/PLAYBOOK.a2ml new file mode 100644 index 0000000..a0f553c --- /dev/null +++ b/.machine_readable/6a2/PLAYBOOK.a2ml @@ -0,0 +1,34 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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 (arghda scan ) +# Emit the DAG (JSON): just dag (arghda dag ) +# Typecheck one file: arghda check (needs `agda` on PATH; degrades gracefully) +# Triage workspace: arghda init +# arghda claim|promote|reject|requeue|invalidate +# arghda events + +[release-process] +# 1. Update CHANGELOG.md; bump version in Cargo.toml + the 6a2 files. +# 2. `just check` must pass. +# 3. Tag v; push. + +[maintenance-operations] +# Run `just validate` (validate-rsr + check) before claiming release-ready. +# Re-dogfood `just dag /proofs/agda` after any engine change and +# confirm the node/edge/blocked counts move as expected. diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml new file mode 100644 index 0000000..3a5106c --- /dev/null +++ b/.machine_readable/6a2/STATE.a2ml @@ -0,0 +1,57 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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. diff --git a/.well-known/ai.txt b/.well-known/ai.txt new file mode 100644 index 0000000..a4c6b71 --- /dev/null +++ b/.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 diff --git a/.well-known/humans.txt b/.well-known/humans.txt new file mode 100644 index 0000000..c180102 --- /dev/null +++ b/.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 diff --git a/.well-known/security.txt b/.well-known/security.txt new file mode 100644 index 0000000..cd5cf7b --- /dev/null +++ b/.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 diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml new file mode 100644 index 0000000..e4fa9bf --- /dev/null +++ b/0-AI-MANIFEST.a2ml @@ -0,0 +1,37 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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.", +] diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..5698912 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,39 @@ + +# 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. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..0fa2722 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,33 @@ + +# 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. diff --git a/Justfile b/Justfile new file mode 100644 index 0000000..7a71331 --- /dev/null +++ b/Justfile @@ -0,0 +1,63 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Task runner for arghda-core. See https://just.systems +set shell := ["bash", "-uc"] + +# List recipes. +default: + @just --list --unsorted + +# Build everything (lib + bin + tests). +build: + cargo build --all-targets + +# Release CLI binary (target/release/arghda). +build-release: + cargo build --release + +# Unit + integration tests. +test: + cargo test + +# Format in place. +fmt: + cargo fmt + +# Format check (CI gate). +fmt-check: + cargo fmt --check + +# Clippy with warnings as errors (CI gate). +lint: + cargo clippy --all-targets -- -D warnings + +# The full CI gate, exactly what .github/workflows/rust-ci.yml runs. +check: fmt-check lint build test + +# Alias for CI. +ci: check + +# Lint an Agda source tree (auto-discovers All.agda/Smoke.agda roots). +scan path: + cargo run -- scan "{{path}}" + +# Emit the dependency-DAG JSON for an Agda source tree. +dag path: + cargo run -- dag "{{path}}" + +# Typecheck one file with Agda + lint it (needs `agda` on PATH). +agda-check file: + cargo run -- check "{{file}}" + +# RSR: the mandated machine-readable artefacts are present and well-formed. +validate-rsr: + @for f in STATE META ECOSYSTEM AGENTIC NEUROSYM PLAYBOOK; do \ + test -f ".machine_readable/6a2/$f.a2ml" || { echo "missing .machine_readable/6a2/$f.a2ml"; exit 1; }; \ + done + @grep -q 'scoping-first = true' .machine_readable/6a2/META.a2ml || { echo "META.a2ml missing maintenance axes"; exit 1; } + @test -f 0-AI-MANIFEST.a2ml || { echo "missing 0-AI-MANIFEST.a2ml"; exit 1; } + @echo "RSR artefacts present and well-formed" + +# Full local gate: RSR artefacts + the CI gate. +validate: validate-rsr check diff --git a/SECURITY.md b/SECURITY.md new file mode 100644 index 0000000..758453f --- /dev/null +++ b/SECURITY.md @@ -0,0 +1,32 @@ + +# Security Policy + +## Supported versions + +arghda-core is alpha (0.1.x). Only the latest `main` is supported. + +## Reporting a vulnerability + +Please report suspected security issues **privately** to +**j.d.a.jewell@open.ac.uk**. Do not open a public issue for a suspected +vulnerability. + +Where possible, include: + +- a description of the issue and its impact; +- steps or a proof-of-concept to reproduce; +- the commit or version affected. + +## Response + +We aim to acknowledge a report within 7 days and to agree a disclosure +timeline with the reporter. + +## Scope + +This policy covers the arghda-core engine. arghda reads `.agda` files as +text and shells out to the configured `agda` (and, in future, +`agda-unused`) binary on files you point it at; it never executes proof +code itself. Reports about untrusted-input handling — path traversal, +command construction, denial of service on malformed input — are +especially welcome.