chore: estate-wide metadata and submodule sync (2026-04-20)

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -1,10 +1,10 @@
 # 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
+# AGENTIC.a2ml — AI agent constraints and capabilities for julia-the-viper
 [metadata]
-version = "0.1.0"
-last-updated = "2026-04-11"
+version = "0.2.0"
+last-updated = "2026-04-19"
 
 [agent-permissions]
 can-edit-source = true
@@ -15,20 +15,83 @@ 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)
+banned-patterns = [
+  "believe_me (Idris2)",
+  "assert_total (Idris2)",
+  "Admitted (Coq)",
+  "sorry (Lean)",
+  "unsafeCoerce (Haskell)",
+  "Obj.magic (OCaml)",
+  ".unwrap() → .expect('TODO') anti-pattern (Rust)"
+]
+banned-languages = [
+  "TypeScript (use ReScript)",
+  "Python (no SaltStack here)",
+  "Go (use Rust)",
+  "V-lang (banned 2026-04-10 → migrate to Zig)"
+]
+structural-rules = [
+  "no SCM files — use A2ML",
+  "no state files in repo root — must be in .machine_readable/",
+  "no .git in subdirs (exception: declared submodules)",
+  "no AGPL (JtV is PMPL)"
+]
+thesis-protection = [
+  "Harvard separation: Data MUST NOT contain Control constructs",
+  "Addition-only: no explicit subtract token in user Data syntax (v2 reverse blocks auto-generate -= — still no new syntax)",
+  "Totality: @pure MUST NOT call impure; @total MUST provably terminate",
+  "Post-pivot 2026-04-19: extern coproc MUST NOT embed predicate syntax — references PataCL gate by name only"
+]
 
 [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
+no-stubbing = true
+
+[memory-discipline]
+# Per user global memory feedback_ask_before_memory_creation.md (2026-04-19):
+# agents MUST ASK user before creating new memory files.
+# Explicit requests ("remember this", "save this") bypass confirmation.
+ask-before-memory-creation = true
+spot-fix-immediately = true  # per feedback_spot_fix_memorize_immediately.md (updated 2026-04-19 — no longer requires autonomous memory write)
 
 [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
+on-enter = """
+1. Read 0-AI-MANIFEST.a2ml
+2. Read .machine_readable/6a2/STATE.a2ml for current phase
+3. Read docs/design-decisions/0001-0006-*.adoc if working on coproc support
+4. Acknowledge in first response
+"""
+on-exit = """
+1. Update STATE.a2ml with session outcomes
+2. Ask user before creating any new memory (per feedback_ask_before_memory_creation.md)
+3. End-of-session marker: 'SAFE TO CLOSE'
+"""
+on-commit = """
+1. Run panic-attack assail (pre-commit)
+2. Verify SPDX headers on modified files
+3. Verify no banned-pattern introductions
+4. Verify Harvard thesis not violated (grep for subtract tokens in data_expr grammar rules)
+"""
+
+[cross-repo-coordination]
+# JtV depends on PataCL for compile-time decisions (post-pivot).
+# Agents must respect the coordination points:
+coordination-points = [
+  "PataCL grammar/semantics change → update JtV ADR-0005 call-site contract if needed",
+  "JtV coproc use-case expansion → may unblock deferred PataCL features (ordering, list-valued facts) — file a PataCL ADR",
+  "PataCL version releases → update META.a2ml dependency line"
+]
+
+[trust-level]
+level = "maximal"
+destructive-ops-require-auth = true  # git push, branch deletion, memory deletion
+
+[delegation-policy]
+# Per estate standing rule feedback_opus_supervise_haiku_first.md:
+phase-0-docs-default = "haiku"
+phase-1-impl-default = "sonnet (code) / haiku (docs)"
+escalation = "opus only as fallback"

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -3,18 +3,84 @@
 #
 # ECOSYSTEM.a2ml — Julia The Viper ecosystem position
 [metadata]
-version = "1.0"
-last-updated = "2026-04-11"
+version = "1.1"
+last-updated = "2026-04-19"
 
 [project]
 name = "Julia The Viper"
-purpose = ""
-role = ""
+purpose = "Harvard-architecture programming language with grammatical Control/Data separation; universal extender for injection-resistant retrofits"
+role = "Programming language — user-facing runtime substrate"
 
 [position-in-ecosystem]
-category = ""
+category = "language"
+tier = "user-facing-runtime"
+top-level-repo = true
 
 [related-projects]
 projects = [
-  # No related projects recorded
+  { name = "patacl",
+    relationship = "dependency (post-pivot 2026-04-19)",
+    role = "compile-time decision substrate for extern coproc blocks",
+    path = "/var/mnt/eclipse/repos/patacl/",
+    status = "co-designed 2026-04-19; integration lands in JtV Phase 2 (blocked on PataCL Phase 1)",
+    integration-shape = "extern coproc <gate-name> { item* } references PataCL gates by name; PataCL evaluates predicates and returns liveness + family string",
+    adr-reference = "docs/design-decisions/0006-patacl-pivot.adoc" },
+
+  { name = "oblibeny",
+    relationship = "sibling-in-family (MPR inspiration for PataCL, not direct dependency)",
+    path = "developer-ecosystem/nextgen-languages/oblibeny/",
+    contribution = "Maximum Principle Reduction, dual-form, reversibility discipline — inherited by PataCL (JtV consumes PataCL)",
+    status = "reference only" },
+
+  { name = "idris2",
+    relationship = "potential-dependency (Phase 2+)",
+    role = "formal ABI layer for coprocessor preconditions (Phase 4 in coproc trajectory)",
+    status = "planned" },
+
+  { name = "zig",
+    relationship = "potential-dependency (Phase 2+)",
+    role = "native emission for extern coproc decls (@Vector / asm volatile / extern)",
+    status = "planned" },
+
+  { name = "spark-ada",
+    relationship = "potential-dependency (optional, Phase 5+)",
+    role = "safety-critical coprocessor contracts — optional path for safety-tier work",
+    status = "deferred" },
+
+  { name = "hypatia",
+    relationship = "consumer (existing)",
+    role = "neurosymbolic scan of JtV repo; consumes A2ML findings",
+    status = "integrated via .github/workflows/hypatia-scan.yml" }
+]
+
+[ecosystem-role]
+what-jtv-provides = [
+  "Harvard-architecture runtime language (Control + Data)",
+  "v2 reversibility for quantum-simulation / Landauer-efficient computation",
+  "Extern-coproc surface for ISA-extension accelerators (via PataCL, post-pivot)",
+  "Teaching platform for grammar-enforced injection-impossibility"
 ]
+what-jtv-consumes = [
+  "PataCL (compile-time decisions)",
+  "Rust toolchain (implementation)",
+  "pest (parser generator)",
+  "Idris2 / Zig / SPARK (deferred; for native coproc emission)"
+]
+
+[supply-chain]
+upstream-deps = [
+  "pest / pest_derive (Rust parsing)",
+  "tower-lsp (LSP implementation)",
+  "wasm-pack (WASM backend)"
+]
+downstream-consumers = [
+  "(none yet; JtV is a pilot/research language. Future: security-research, legacy-retrofit tooling.)"
+]
+
+[governance]
+maintainer = "Jonathan D.A. Jewell (single author)"
+license = "PMPL-1.0-or-later"
+
+[visibility]
+public = true
+mirror-targets = "GitHub only (origin); downstream mirroring via hub-and-spoke per hyperpolymath policy"

.machine_readable/6a2/META.a2ml

@@ -3,25 +3,68 @@
 #
 # META.a2ml — Julia The Viper meta-level information
 [metadata]
-version = "0.1.0"
-last-updated = "2026-04-11"
+version = "0.2.0"
+last-updated = "2026-04-19"
 
 [project-info]
 license = "PMPL-1.0-or-later"
+license-fallback = "MPL-2.0 (automatic legal fallback until PMPL formally recognised)"
 author = "Jonathan D.A. Jewell (hyperpolymath)"
+author-email = "j.d.a.jewell@open.ac.uk"
+git-author-email = "6759885+hyperpolymath@users.noreply.github.com"
 
 [architecture-decisions]
 decisions = [
-  # No ADRs recorded
+  { id = "v2-reversibility", title = "v2 reversibility via reverse blocks (5 decisions closed)", status = "design-complete",
+    path = "docs/language/DESIGN-JTV-V2-REVERSIBILITY.md",
+    date = "2026-04-12" },
+  { id = "coproc-0001", title = "Coprocessor support via pata pathway (Trajectory E)", status = "closed",
+    path = "docs/design-decisions/0001-coprocessor-pata-pathway.adoc",
+    date = "2026-04-19" },
+  { id = "coproc-0002", title = "Decision sublanguage (SUPERSEDED by Delta pivot)", status = "superseded",
+    superseded-by = "coproc-0006",
+    path = "docs/design-decisions/0002-decision-sublanguage.adoc" },
+  { id = "coproc-0003", title = "Compile-time fact vocabulary", status = "closed",
+    path = "docs/design-decisions/0003-compile-time-fact-vocabulary.adoc" },
+  { id = "coproc-0004", title = "Pata-eval failure semantics", status = "closed",
+    path = "docs/design-decisions/0004-pata-eval-failure-semantics.adoc" },
+  { id = "coproc-0005", title = "Extern coproc call semantics", status = "closed",
+    path = "docs/design-decisions/0005-extern-coproc-call-semantics.adoc" },
+  { id = "coproc-0006", title = "Delta pivot — PataCL as separate DSL", status = "closed",
+    path = "docs/design-decisions/0006-patacl-pivot.adoc",
+    date = "2026-04-19",
+    supersedes = ["coproc-0002"] }
 ]
 
+[design-rationale]
+# Load-bearing choices for JtV:
+# 1. Harvard separation is the whole thesis; do not dilute with embedded sublanguages.
+# 2. Addition-only Data: provable totality + injection impossibility.
+# 3. Reverse blocks (v2): snapshot-based, linear ReversalToken typing, no new subtract syntax.
+# 4. Coprocessor support delegated to PataCL (2026-04-19 Delta pivot) — JtV grammar stays focused on runtime semantics.
+# 5. First pilot target: RISC-V — X-ext exercises Idris2/Zig/SPARK stack end-to-end.
+
 [development-practices]
 versioning = "SemVer"
-documentation = "AsciiDoc"
+documentation = "AsciiDoc (human-primary) + A2ML (bot-primary)"
 build-tool = "just"
+package-manager = "Guix (primary) / Nix (fallback)"
+implementation-language = "Rust; SPARK admissible for safety-critical via Idris2-ABI + Zig-FFI"
 
 [maintenance-axes]
 scoping-first = true
 axis-1 = "must > intend > like"
 axis-2 = "corrective > adaptive > perfective"
 axis-3 = "systems > compliance > effects"
+
+[language-sublanguages-post-pivot]
+# After the 2026-04-19 Delta pivot, JtV Harvard remains BINARY (Control + Data).
+# The Decision sublanguage that ADR-0002 introduced as a third lane is extracted
+# to PataCL, which is a sibling language, not a sublanguage of JtV.
+control = "Turing-complete, runtime, effectful"
+data = "total, addition-only, runtime, pure"
+patacl-relationship = "sibling language consulted at compile time; not a JtV sublanguage post-pivot"
+
+[cross-repo-dependencies]
+patacl = "/var/mnt/eclipse/repos/patacl/ — compile-time decision substrate (post-pivot)"
+oblibeny = "developer-ecosystem/nextgen-languages/oblibeny/ — source of MPR discipline that PataCL inherits"

.machine_readable/6a2/NEUROSYM.a2ml

@@ -1,21 +1,76 @@
 # 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
+# NEUROSYM.a2ml — Neurosymbolic integration metadata for julia-the-viper
 [metadata]
-version = "0.1.0"
-last-updated = "2026-04-11"
+version = "0.2.0"
+last-updated = "2026-04-19"
 
 [hypatia-config]
 scan-enabled = true
 scan-depth = "standard"  # quick | standard | deep
-report-format = "logtalk"
+report-format = "a2ml"   # Logtalk removed 2026-04-12 — see memory: hypatia-logtalk-removed
+# JtV is scanned on every CI run; findings go into .github/hypatia-findings/
 
 [symbolic-rules]
-# Custom symbolic rules for this project
-# - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
+# Project-specific symbolic rules for Hypatia's logic engine.
+rules = [
+  # Harvard thesis protection
+  { name = "jtv-no-control-in-data-expr",
+    pattern = "data_expr.*if|data_expr.*while|data_expr.*for|data_expr.*assignment",
+    severity = "blocker",
+    rationale = "Data expressions MUST NOT contain Control constructs — injection-impossibility depends on this",
+    fix-hint = "Remove Control construct from Data expression; refactor into Control context" },
+
+  { name = "jtv-no-subtract-in-data-grammar",
+    pattern = "additive_expr.*\"-\"",
+    severity = "blocker",
+    rationale = "Data Language is addition-only. v2 reverse blocks auto-generate -= semantics but do NOT introduce user-visible subtract syntax",
+    fix-hint = "Revert; discuss in ADR if real need" },
+
+  # Post-pivot coproc rules
+  { name = "jtv-no-embedded-predicate-in-extern-coproc",
+    pattern = "extern_coproc_block.*target\\s*\\(|extern_coproc_block.*requires\\s+[a-z]|extern_coproc_block.*encoding\\s+[a-z]",
+    severity = "blocker",
+    rationale = "ADR-0006 Delta pivot: extern coproc MUST reference PataCL gate by identifier, not embed predicates",
+    fix-hint = "Extract predicate into a .pata file; reference gate by name from JtV" },
+
+  # v2 reversibility
+  { name = "jtv-reversible-block-requires-snapshot",
+    pattern = "reversible\\s*\\{[^}]*\\}(?!\\s*(reverse|abandon|->))",
+    severity = "warning",
+    rationale = "reversible block should produce a ReversalToken (v2 Decision 4 — linear-use-once typing)",
+    fix-hint = "Use reverse { ... } sugar OR capture token with -> tok" },
+
+  # Dangerous patterns (reinforces estate rules)
+  { name = "jtv-no-unwrap-to-expect-antipattern",
+    pattern = "\\.expect\\s*\\(\\s*\"TODO\"",
+    severity = "warning",
+    rationale = "per feedback_unwrap_to_expect_antipattern — identical panic with fake debt marker",
+    fix-hint = "Handle the error properly or revert to .unwrap() with comment explaining why" }
+]
 
 [neural-config]
-# Neural pattern detection settings
-# confidence-threshold = 0.85
-# model = "hypatia-v2"
+# Neural pattern detection (Phase 2+)
+enabled = true
+confidence-threshold = 0.85
+model = "hypatia-v2"
+rationale = "subtle thesis violations (e.g., sneaking arithmetic into Data via trick operators) benefit from neural detection beyond regex"
+
+[proof-integration]
+# JtV has formal verification hooks for v2 reversibility and (planned) coproc ABI
+proof-obligations = [
+  "Data Language totality — structural induction on additive_expr (trivial)",
+  "v2 reverse block semantics — forward-then-reverse = identity (Lean/Coq)",
+  "Snapshot capture completeness — all locals captured on reversible { } entry",
+  "Post-pivot: extern coproc gate result faithfulness — JtV's liveness decision matches PataCL's evaluation"
+]
+preferred-proof-system = "Idris2 (per feedback_idris_over_ephapax)"
+alternative-proof-systems = ["Lean4", "Agda", "Coq"]
+
+[dangerous-pattern-exclusion]
+banned = [
+  "believe_me", "unsafeCoerce", "assert_total",
+  "Admitted", "sorry", "Obj.magic",
+  ".unwrap() → .expect('TODO') anti-pattern"
+]