chore(6a2): commit pre-existing 6a2 sweep for echidnabot, HOL-o-extension, echidna-playground

Files were converted from SCM format and filled in by a prior session
but never staged/committed. Covers AGENTIC, ECOSYSTEM, META, NEUROSYM,
PLAYBOOK, STATE for each sub-project.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

HOL-o-extension/.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -1,60 +1,20 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-;; ECOSYSTEM.scm — HOL-o-extension ecosystem position
-
-(ecosystem
-  ((metadata
-     ((version . "0.1.0")
-      (name . "HOL-o-extension")
-      (type . "o-extension")
-      (purpose . "Optional overlay extending HOL4 with custom theories and tactics for ECHIDNA integration")))
-
-   (overlay-protocol
-     ((base . "../HOL")
-      (upstream . "https://github.com/HOL-Theorem-Prover/HOL")
-      (peer-type . "o-extension")
-      (activation . "source activate.sh")
-      (deactivation . "unset HOL_OEXT_ACTIVE; unset HOL_OEXT_DIR")
-      (switchable . #t)
-      (modifies-base . #f)
-      (description . "Optional-extension pattern: never touches base code, purely additive overlay that can be toggled on/off per-run. When active, extends HOL's load path with custom theories and tactics. When inactive, HOL behaves as virgin upstream.")))
-
-   (position-in-ecosystem
-     "HOL-o-extension is a peer-level sibling to the upstream HOL4 theorem prover within the ECHIDNA monorepo. It provides custom theories and tactics needed for ECHIDNA's neurosymbolic proof search without forking or modifying HOL itself. This follows the Overlay Protocol, where overlays declare their relationship to a base project and maintain strict non-modification invariants.")
-
-   (related-projects
-     ((base-project
-        ((hol4
-           ((relationship . "base")
-            (description . "HOL4 higher-order logic theorem prover (upstream)")
-            (path . "../HOL")
-            (upstream . "https://github.com/HOL-Theorem-Prover/HOL")
-            (interaction . "Load path extension, never modification")))))
-
-      (parent-project
-        ((echidna
-           ((relationship . "parent-monorepo")
-            (description . "ECHIDNA neurosymbolic theorem prover")
-            (path . "..")
-            (interaction . "HOL4 backend uses o-extension theories when activated")))))
-
-      (overlay-protocol-peers
-        ;; Other projects using the Overlay Protocol pattern
-        ((proven-aggregate-lib
-           ((relationship . "protocol-peer")
-            (peer-type . "aggregate-library")
-            (description . "Curated subset of proven bindings — same Overlay Protocol, different peer-type")
-            (status . "active")
-            (notes . "aggregate-library selects/re-exports; o-extension adds new capabilities. Both verified conformant.")))))))
-
-   (what-this-is
-     (("An optional overlay for HOL4 within ECHIDNA"
-       "Custom theories for neurosymbolic proof search"
-       "Additional tactics for ECHIDNA-specific proof strategies"
-       "Switchable per-run — activate.sh to enable, unset to disable"
-       "Part of the Overlay Protocol (peer-type: o-extension)")))
-
-   (what-this-is-not
-     (("Not a fork of HOL — upstream is rebased, never patched"
-       "Not a dependency — HOL works fine without it"
-       "Not an aggregate-library — it adds new things, not curates existing ones"
-       "Not permanent — can be toggled off for vanilla HOL behaviour")))))
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# ECOSYSTEM.a2ml — HOL O Extension ecosystem position
+[metadata]
+version = "0.1.0"
+last-updated = "2026-04-11"
+
+[project]
+name = "HOL O Extension"
+purpose = "Optional overlay extending HOL4 with custom theories and tactics for ECHIDNA integration"
+role = "o-extension"
+
+[position-in-ecosystem]
+category = ""
+
+[related-projects]
+projects = [
+  { name = "HOL-o-extension", relationship = "base" },
+]

HOL-o-extension/.machine_readable/6a2/META.a2ml

@@ -1,40 +1,27 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-;; META.scm — HOL-o-extension meta-level information
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# META.a2ml — HOL O Extension meta-level information
+[metadata]
+version = "0.1.0"
+last-updated = "2026-04-11"
 
-(meta
-  ((metadata
-     ((version . "0.1.0")
-      (media-type . "application/meta+scheme")))
+[project-info]
+license = "PMPL-1.0-or-later"
+author = "Jonathan D.A. Jewell (hyperpolymath)"
 
-   (architecture-decisions
-     ((adr-001
-        ((title . "Use o-extension pattern instead of forking HOL")
-         (status . "accepted")
-         (date . "2026-03-07")
-         (context . "ECHIDNA needs custom theories and tactics for HOL4 integration. Options: fork HOL, patch HOL, or overlay alongside HOL.")
-         (decision . "Use the o-extension (optional-extension) pattern: a peer-level directory that overlays HOL via environment variables without modifying any upstream files.")
-         (rationale . "Forking creates maintenance burden tracking upstream. Patching breaks on rebase. The o-extension pattern keeps HOL pristine, allows clean rebasing, and can be toggled on/off per-run.")
-         (consequences . ("HOL upstream can be rebased freely"
-                          "No merge conflicts with upstream"
-                          "Slightly more complex activation (must source activate.sh)"
-                          "Custom theories must be self-contained"))))
+[architecture-decisions]
+decisions = [
+  # No ADRs recorded
+]
 
-      (adr-002
-        ((title . "Overlay Protocol as shared pattern with aggregate-library")
-         (status . "accepted")
-         (date . "2026-03-07")
-         (context . "Both o-extension and aggregate-library share core invariants: never modify base, switchable, declared relationship.")
-         (decision . "Formalize both as instances of the Overlay Protocol, differentiated by peer-type (o-extension vs aggregate-library) and activation-method (flag vs dependency).")
-         (rationale . "Unifying under one protocol makes the patterns discoverable, composable, and consistently documented across the ecosystem.")
-         (consequences . ("ECOSYSTEM.scm gains overlay-protocol section"
-                          "Both patterns can reference each other as protocol-peers"
-                          "Future overlay types can extend the protocol"))))))
+[development-practices]
+versioning = "SemVer"
+documentation = "AsciiDoc"
+build-tool = "just"
 
-   (development-practices
-     ((sml-conventions
-        ((description . "HOL4 uses Standard ML (SML). All theories and tactics in this o-extension are written in SML.")
-         (style . "Follow HOL4 naming conventions for theories and tactics")))
-
-      (testing
-        ((description . "Test by loading theories with and without o-extension active")
-         (approach . "Activation/deactivation cycle must be idempotent")))))))
+[maintenance-axes]
+scoping-first = true
+axis-1 = "must > intend > like"
+axis-2 = "corrective > adaptive > perfective"
+axis-3 = "systems > compliance > effects"

HOL-o-extension/.machine_readable/6a2/STATE.a2ml

@@ -1,45 +1,40 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-;; STATE.scm — HOL-o-extension project state
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# STATE.a2ml — HOL O Extension project state
+[metadata]
+project = "HOL-o-extension"
+version = "0.1.0"
+last-updated = "2026-03-07"
+status = "active"
+session = "converted from scheme — 2026-04-11"
 
-(state
-  ((metadata
-     ((version . "0.1.0")
-      (last-updated . "2026-03-07")
-      (author . "Jonathan D.A. Jewell")))
+[project-context]
+name = "HOL O Extension"
+purpose = """activate.sh sets environment for HOL load path extension"""
+completion-percentage = 0
 
-   (project-context
-     ((name . "HOL-o-extension")
-      (type . "o-extension")
-      (base . "HOL4 Theorem Prover")
-      (parent . "ECHIDNA")))
+[position]
+phase = "scaffolding"   # design | implementation | testing | maintenance | archived
+maturity = "experimental"  # experimental | alpha | beta | production | lts
 
-   (current-position
-     ((phase . "scaffolding")
-      (completion . 5)
-      (status . "Directory structure and overlay protocol declared. Theories and tactics not yet populated.")))
+[route-to-mvp]
+milestones = [
+  { name = "HOL-o-extension", completion = 5 },
+]
 
-   (route-to-mvp
-     ((milestone-1
-        ((name . "Activation mechanism")
-         (status . "complete")
-         (description . "activate.sh sets environment for HOL load path extension")))
-      (milestone-2
-        ((name . "First custom theory")
-         (status . "pending")
-         (description . "Create an ECHIDNA-specific HOL4 theory (e.g., trust levels, confidence types)")))
-      (milestone-3
-        ((name . "First custom tactic")
-         (status . "pending")
-         (description . "Create an ECHIDNA-specific HOL4 tactic (e.g., neurosymbolic_suggest)")))
-      (milestone-4
-        ((name . "ECHIDNA HOL4 backend integration")
-         (status . "pending")
-         (description . "Wire o-extension into ECHIDNA's HOL4 prover backend")))))
+[blockers-and-issues]
+issues = [
+  # No blockers recorded
+]
 
-   (blockers-and-issues
-     ((none-currently . #t)))
+[critical-next-actions]
+actions = [
+  "Define first custom HOL4 theory for ECHIDNA trust types",
+  "Create neurosymbolic tactic stubs",
+  "Test activate/deactivate cycle end-to-end",
+]
 
-   (critical-next-actions
-     (("Define first custom HOL4 theory for ECHIDNA trust types"
-       "Create neurosymbolic tactic stubs"
-       "Test activate/deactivate cycle end-to-end")))))
+[maintenance-status]
+last-run-utc = "2026-03-07T00:00:00Z"
+last-result = "unknown"  # unknown | pass | warn | fail

echidna-playground/.machine_readable/6a2/AGENTIC.a2ml

@@ -1,2 +1,34 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-;; Reserved for future use.
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# 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-04-11"
+
+[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:
+# - Never use banned language patterns (believe_me, unsafeCoerce, etc.)
+# - 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 PMPL-1.0-or-later)
+
+[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
+
+[automation-hooks]
+# on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml
+# on-exit: Update STATE.a2ml with session outcomes
+# on-commit: Run just validate-rsr

echidna-playground/.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -1,3 +1,20 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-(ecosystem (metadata (version "0.1.0") (last-updated "2026-02-08"))
-  (project (name "language-bridges") (purpose "FFI bridges between languages via Zig") (role ffi-infrastructure)))
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# ECOSYSTEM.a2ml — Echidna Playground ecosystem position
+[metadata]
+version = "0.1.0"
+last-updated = "2026-02-08"
+
+[project]
+name = "Echidna Playground"
+purpose = "FFI bridges between languages via Zig"
+role = ""
+
+[position-in-ecosystem]
+category = ""
+
+[related-projects]
+projects = [
+  # No related projects recorded
+]

echidna-playground/.machine_readable/6a2/META.a2ml

@@ -1,3 +1,27 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-(meta (metadata (version "0.1.0") (last-updated "2026-02-08"))
-  (project-info (type monorepo) (languages (zig ada gleam idris2 julia ocaml rescript rust swift)) (license "PMPL-1.0-or-later")))
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# META.a2ml — Echidna Playground meta-level information
+[metadata]
+version = "0.1.0"
+last-updated = "2026-02-08"
+
+[project-info]
+license = "PMPL-1.0-or-later"
+author = "Jonathan D.A. Jewell (hyperpolymath)"
+
+[architecture-decisions]
+decisions = [
+  # No ADRs recorded
+]
+
+[development-practices]
+versioning = "SemVer"
+documentation = "AsciiDoc"
+build-tool = "just"
+
+[maintenance-axes]
+scoping-first = true
+axis-1 = "must > intend > like"
+axis-2 = "corrective > adaptive > perfective"
+axis-3 = "systems > compliance > effects"

echidna-playground/.machine_readable/6a2/NEUROSYM.a2ml

@@ -1,2 +1,21 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-;; Reserved for future use.
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# NEUROSYM.a2ml — Neurosymbolic integration metadata
+[metadata]
+version = "0.1.0"
+last-updated = "2026-04-11"
+
+[hypatia-config]
+scan-enabled = true
+scan-depth = "standard"  # quick | standard | deep
+report-format = "logtalk"
+
+[symbolic-rules]
+# Custom symbolic rules for this project
+# - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
+
+[neural-config]
+# Neural pattern detection settings
+# confidence-threshold = 0.85
+# model = "hypatia-v2"

echidna-playground/.machine_readable/6a2/PLAYBOOK.a2ml

@@ -1,2 +1,26 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-;; Reserved for future use.
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# PLAYBOOK.a2ml — Operational playbook
+[metadata]
+version = "0.1.0"
+last-updated = "2026-04-11"
+
+[deployment]
+# method = "gitops"  # gitops | manual | ci-triggered
+# target = "container"  # container | binary | library | wasm
+
+[incident-response]
+# 1. Check .machine_readable/STATE.a2ml for current status
+# 2. Review recent commits and CI results
+# 3. Run `just validate` to check compliance
+# 4. Run `just security` to audit for vulnerabilities
+
+[release-process]
+# 1. Update version in STATE.a2ml, META.a2ml
+# 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass)
+# 3. Tag and push
+
+[maintenance-operations]
+# Baseline audit: just maint-audit
+# Hard release gate: just maint-hard-pass