docs(machine_readable): ochrance-framework checkpoint — refresh 6a2 + ANCHOR (#18)

$(cat <<'EOF'
## Summary

- Replaces the March 2026 thin `.scm`-converted stubs in
`.machine_readable/6a2/` and `anchors/ANCHOR.a2ml` with a full
machine-readable checkpoint reflecting ochrance-framework's actual
current role and status as of 2026-06-05.
- Records decision D1 throughout: this repo's duplicate `ochrance-core`
is retired; canonical proofs and production code live in the `ochrance`
repo. The framework's genuinely novel contribution — the mode-indexed,
subsystem-parameterised `VerifiedSubsystem` interface — has been
harvested into `ochrance`. This repo retains its real value:
architecture, A2ML spec, FFI contract, threat model, whitepaper, L4
policies, and roadmap.
- ANCHOR gets a 2026-06-05 realignment record for D1, citing
`docs/ARCHITECTURE.md` as authority.

### Per-file changes

| File | What changed |
|---|---|
| `STATE.a2ml` | phase → `maintenance`; completion 5% → 65%;
`what-this-repo-owns` / `retired` sections; honest blockers; recent CI
merge history |
| `META.a2ml` | D1 listed first in decisions; ADR-001–005 condensed to
flat list; ochrance-style `architecture` block |
| `NEUROSYM.a2ml` | obligations split into `defined-here` /
`discharged-in-ochrance` / `open`; `honest-bounds` note; compact
symbolic-rules list |
| `ECOSYSTEM.a2ml` | reoriented as architecture+docs repo; ochrance
listed first as canonical core; svalinn, valence-shell, boj-server,
verisimdb added |
| `AGENTIC.a2ml` | D1 `core-authority` guard added; trimmed to
ochrance-exemplar conciseness; retains FFI security boundary |
| `PLAYBOOK.a2ml` | build split into this-repo (stubs) and
canonical-core (ochrance per D1); aligned with Justfile recipes |
| `ANCHOR.a2ml` | 2026-06-05 realignment record for D1 core-retirement +
framework role-clarification |

## Test plan

- [ ] Confirm all seven files have correct SPDX header (`MPL-2.0`) and
copyright line
- [ ] Confirm ANCHOR realignment record date is `2026-06-05` and
authority is `docs/ARCHITECTURE.md`
- [ ] Confirm no Idris source, contractiles/, svc/, integrations/, or
other files were touched
- [ ] CI green (RSR antipattern check, SPDX check, workflow linters)

https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
EOF
)

---
_Generated by [Claude
Code](https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -1,92 +1,37 @@
 # 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 for Ochrance Framework
+# AGENTIC.a2ml — AI agent constraints and capabilities
 # Defines what AI agents can and cannot do in this repository.
-
 [metadata]
 version = "0.1.0"
-last-updated = "2026-02-19"
+last-updated = "2026-06-05"
 
 [agent-permissions]
-can-edit-source = true
-can-edit-tests = true
 can-edit-docs = true
 can-edit-config = true
+can-edit-machine-readable = true
+can-edit-source = true        # Idris2 stubs; proof changes require human review
+can-edit-tests = true
 can-create-files = true
-can-edit-proofs = false  # Idris2 proofs must be human-reviewed before merge
-can-edit-ffi = false     # C FFI shims require manual security review
+can-edit-ffi = false          # C NVMe shims are attack surface; require manual security review
 
 [agent-constraints]
-# What AI agents must NOT do in this repository:
-constraints = [
-  "Never use believe_me in Idris2 code (banned unsafe pattern)",
-  "Never use assert_total in Idris2 code (banned unsafe pattern)",
-  "Never use assert_smaller in Idris2 code (banned unsafe pattern)",
-  "Never use unsafePerformIO in Idris2 code (banned unsafe pattern)",
-  "Never introduce unsafe{} blocks in Rust code without SAFETY comments",
-  "Never commit secrets or credentials",
-  "Never use banned languages (TypeScript, Python, Go, etc.)",
-  "Never place state files in repository root (must be in .machine_readable/)",
-  "Never use AGPL license (use MPL-2.0)",
-  "Never weaken StrictnessLevel (do not change Attested to Checked or Lax)",
-  "Never bypass proof obligations with postulates or Admitted-equivalent",
-  "Never modify C FFI shims without flagging for security review",
-]
-
-[agents]
-# AI agents that interact with this repository
-
-[agents.claude]
-role = "primary-development"
-model = "claude-opus-4-6"
-capabilities = [
-  "Code generation (Idris2, Rust, C, Julia)",
-  "Architecture design and ADR drafting",
-  "Documentation and specification writing",
-  "Test scaffolding and property specification",
-  "CI/CD workflow configuration",
-  "RSR compliance enforcement",
-]
-limitations = [
-  "Cannot verify Idris2 totality (requires idris2 compiler)",
-  "Cannot run proof obligations (requires Echidna dispatch)",
-  "Cannot deploy to OSTree (requires system access)",
-]
-
-[agents.echidna]
-role = "proof-synthesis"
-type = "neurosymbolic-prover"
-capabilities = [
-  "Neural proof synthesis for Idris2 tactics",
-  "Cross-prover verification of proof obligations",
-  "Confidence scoring via 5-level trust hierarchy",
-  "Portfolio solving across 30 prover backends",
-]
-interaction = "Ochrance dispatches proof obligations via structured format; Echidna returns synthesised proofs with confidence metadata"
-
-[agents.hypatia]
-role = "ci-intelligence"
-type = "neurosymbolic-cicd"
-capabilities = [
-  "Pattern detection in verification reports",
-  "Fleet dispatch to gitbot-fleet bots",
-  "VeriSimDB integration for weakness tracking",
-]
-interaction = "Hypatia scans Ochrance on commit; emits Logtalk facts for downstream analysis"
-
-[automation-hooks]
-on-enter = "Read 0-AI-MANIFEST.a2ml, then .machine_readable/STATE.a2ml"
-on-exit = "Update .machine_readable/STATE.a2ml with session outcomes"
-on-commit = "Run just validate-rsr"
-on-proof-change = "Flag for human review; do not auto-merge proof modifications"
-on-ffi-change = "Flag for security review; C shims must be manually audited"
-
-[review-gates]
-# Changes that require human approval before merge
-gates = [
-  { path = "ochrance-core/src/**/*.idr", gate = "proof-review", reason = "Core Idris2 proofs must be human-verified" },
-  { path = "ffi/**/*.c", gate = "security-review", reason = "C FFI shims are attack surface" },
-  { path = "modules/*/src/**/*.idr", gate = "proof-review", reason = "Module proofs must be human-verified" },
-  { path = ".machine_readable/**", gate = "metadata-review", reason = "SCM file changes affect all agents" },
-]
+# What AI agents must NOT do:
+# - Never use banned proof escapes (believe_me, assert_total, assert_smaller, postulate, unsafePerformIO)
+# - Never weaken %default total, nor introduce covering / partial on verification code
+# - Never commit secrets or credentials
+# - Never use banned languages (TypeScript, Python, Go, etc.)
+# - Never place state/meta files in repository root (must live under .machine_readable/)
+# - Never use AGPL (license is MPL-2.0)
+# - Never modify C FFI shims without flagging for security review
+# - Never make proof changes in ochrance-core/ here without noting D1: the canonical source is ochrance
+
+[agent-workflow]
+role = "primary surface is docs/ and .machine_readable/; Idris2 stubs for interface reference only"
+core-authority = "D1: proof and code changes go to the ochrance repo, not here"
+docs-gate = "docs/ changes are the primary maintenance path; keep specs in sync with ochrance implementation"
+verification-gate = "idris2 --build ochrance.ipkg must stay clean (stubs only; no new proofs here)"
+model-guidance = "Sonnet for docs, architecture, spec writing; Opus for any proof-adjacent reasoning"
+on-enter = "Read .machine_readable/6a2/STATE.a2ml; check D1 status before touching ochrance-core/"
+on-exit = "Update .machine_readable/6a2/STATE.a2ml with session outcomes if substantive"

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -1,127 +1,33 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# ECOSYSTEM.a2ml — Project ecosystem position for Ochrance Framework
-# Relationships, dependencies, integration points.
-
+# ECOSYSTEM.a2ml — Ecosystem position
 [metadata]
-version = "0.1.0"
-last-updated = "2026-02-19"
-
-[project]
-name = "Ochrance Framework"
-purpose = "Modular verification framework for subsystem integrity using dependent types (Idris2)"
-role = "verification-framework"  # e.g. ffi-infrastructure, cli-tool, library, service
+project = "ochrance-framework"
+ecosystem = "hyperpolymath"
+last-updated = "2026-06-05"
 
-[position-in-ecosystem]
-tier = "infrastructure"  # 1 | 2 | infrastructure
-description = """
-Ochrance sits at the infrastructure tier of the hyperpolymath verification stack.
-It provides the formal verification layer for operating system subsystem integrity,
-bridging the gap between dependent-type theory (Idris2) and practical system
-deployment (OSTree/Fedora Kinoite). It consumes Echidna for neural proof synthesis
-and feeds verification results to Hypatia for CI/CD intelligence.
-"""
+[position]
+type = "architecture + documentation"
+role = """Architecture, specification, and documentation repository for the Ochránce neurosymbolic verification system. Defines the L0–L5 trust pyramid, A2ML specification, FFI contract, threat model, whitepaper, L4 policies, and roadmap. The duplicate core has been retired (D1); canonical proofs and production code live in the ochrance repo."""
 
 [related-projects]
-# relationship types: sibling-standard, dependency, dependent, inspiration, potential-consumer
-
-[[related-projects.project]]
-name = "echidna"
-relationship = "sibling"
-description = "Neurosymbolic theorem proving platform with 30 prover backends"
-interaction = "Ochrance dispatches proof obligations to Echidna; Echidna synthesises Idris2 proofs via neural tactics"
-url = "https://github.com/hyperpolymath/echidna"
-
-[[related-projects.project]]
-name = "verisimdb"
-relationship = "sibling"
-description = "Verisimilitude Database for vulnerability and weakness tracking"
-interaction = "Ochrance scan results feed into VeriSimDB for cross-repo weakness aggregation"
-url = "https://github.com/hyperpolymath/verisimdb"
-
-[[related-projects.project]]
-name = "panic-attacker"
-relationship = "sibling"
-description = "Security weakness scanner (panic-attack CLI)"
-interaction = "Runs security scans against Ochrance codebase; results ingested by VeriSimDB"
-url = "https://github.com/hyperpolymath/panic-attacker"
-
-[[related-projects.project]]
-name = "hypatia"
-relationship = "potential-consumer"
-description = "Neurosymbolic CI/CD intelligence platform"
-interaction = "Consumes Ochrance verification reports for CI pipeline intelligence and pattern detection"
-url = "https://github.com/hyperpolymath/hypatia"
-
-[[related-projects.project]]
-name = "eclexia"
-relationship = "sibling"
-description = "Programming language with formal verification, shadow pricing, carbon-aware scheduling"
-interaction = "Shares formal verification infrastructure; potential mutual backend integration"
-url = "https://github.com/hyperpolymath/eclexia"
-
-[[related-projects.project]]
-name = "gitbot-fleet"
-relationship = "dependent"
-description = "Bot orchestration platform (rhodibot, echidnabot, sustainabot, etc.)"
-interaction = "Ochrance triggers bot actions via repository_dispatch; bots enforce verification policies"
-url = "https://github.com/hyperpolymath/gitbot-fleet"
-
-[[related-projects.project]]
-name = "rhodium-standard-repositories"
-relationship = "sibling-standard"
-description = "RSR compliance standard for repository structure"
-interaction = "Ochrance follows RSR for repository layout, CI workflows, and metadata"
-url = "https://github.com/hyperpolymath/rhodium-standard-repositories"
-
-[integration-points]
-# External systems this project connects to
-
-[[integration-points.system]]
-name = "echidna"
-direction = "bidirectional"
-protocol = "proof-dispatch"
-description = "Dispatches Idris2 proof obligations; receives synthesised proofs and confidence scores"
-
-[[integration-points.system]]
-name = "hypatia"
-direction = "outbound"
-protocol = "logtalk-facts"
-description = "Emits verification reports as Logtalk facts for neurosymbolic CI/CD analysis"
-
-[[integration-points.system]]
-name = "gitbot-fleet"
-direction = "outbound"
-protocol = "repository_dispatch"
-description = "Triggers bot orchestration events on verification status changes"
-
-[[integration-points.system]]
-name = "ostree"
-direction = "outbound"
-protocol = "ostree-deploy"
-description = "Deployment target: verified filesystem images deployed via OSTree to Fedora Kinoite"
-
-[[integration-points.system]]
-name = "hacl-star"
-direction = "inbound"
-protocol = "c-ffi-linking"
-description = "Links against HACL* verified cryptographic implementations (future crypto module)"
-
-[what-this-is]
-descriptions = [
-  "A modular verification framework for OS subsystem integrity",
-  "An Idris2-based system for expressing and checking subsystem correctness guarantees",
-  "A bridge between dependent-type theory and practical system deployment",
-  "A framework with progressive strictness levels (Lax/Checked/Attested)",
-  "A thesis-scope proof-of-concept targeting filesystem verification on Fedora Kinoite",
+projects = [
+  "ochrance — canonical core and proof source of truth; implements the VerifiedSubsystem interface, A2ML parser, verified Merkle tree, and ECHIDNA FFI; harvested this repo's mode-indexed interface (D1)",
+  "echidna — Rust/Julia neurosymbolic prover platform; Ochránce adds Idris2 as 13th backend (ADR-005)",
+  "idris2-echidna — Idris2 prover abstraction layer for ECHIDNA dispatch",
+  "svalinn — estate sibling; edge verification gateway; migrating ReScript → Ephapax (D3 in ochrance)",
+  "valence-shell — consumes Ochránce attestation receipts for accountable state transitions",
+  "echo-types — semantics of the residue/loss exposed by state transitions",
+  "boj-server — SSG/build host (casket engine); ANCHOR parent (see anchors/ANCHOR.a2ml)",
+  "verisimdb — vulnerability/weakness tracking database; ingests Hypatia scan results",
+  "hypatia — neurosymbolic CI/CD intelligence; consumes Logtalk facts from verification runs",
 ]
 
-[what-this-is-not]
-descriptions = [
-  "Not a replacement for Echidna -- Ochrance defines proof obligations, Echidna synthesises proofs",
-  "Not a general-purpose theorem prover -- it is a verification framework for subsystem integrity",
-  "Not limited to filesystems -- the framework supports any subsystem via the VerifiedSubsystem interface",
-  "Not production-ready -- currently in design phase at 5% completion",
-  "Not a runtime verification tool -- proofs are checked at compile time (Checked/Attested levels)",
+[integrations]
+# This repo is primarily docs; integration points are defined by spec, discharged in ochrance.
+declared = [
+  "echidna — proof-obligation dispatch (ADR-005; planned)",
+  "hypatia — Logtalk scan output on commit",
+  "boj-server — ANCHOR parent (SSG build)",
 ]