feat: restructure to Idris2 ABI / SPARK core / Zig FFI architecture

Architecture now follows the standard 5-layer verified design:
- Idris2 ABI (src/interface/abi/): State, Events, Widgets with
  dependent type proofs (bounded dimensions, valid transitions,
  monotonic versions, depth-indexed widget trees)
- Pure Zig FFI (src/interface/ffi/): zero-logic pass-through bridge
- SPARK core (src/spark/): formally verified state, events, widgets,
  and C ABI exports with Pre/Post/Contract_Cases on every subprogram
- Ada presentation (src/ada/): terminal renderer using SPARK directly
- Rust consumer (src/rust/): ecosystem integration via Zig bridge

Also: comprehensive .machine_readable/ updates (STATE, META, ECOSYSTEM,
AGENTIC with TSDM categories), real RSR Trustfile, CLAUDE.md session
handoff notes, README.adoc and ROADMAP.adoc rewrites, TOPOLOGY.md.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.claude/CLAUDE.md

@@ -1,84 +1,71 @@
-## Machine-Readable Artefacts
-
-The following files in `.machine_readable/` contain structured project metadata:
-
-- `STATE.scm` - Current project state and progress
-- `META.scm` - Architecture decisions and development practices
-- `ECOSYSTEM.scm` - Position in the ecosystem and related projects
-- `AGENTIC.scm` - AI agent interaction patterns
-- `NEUROSYM.scm` - Neurosymbolic integration config
-- `PLAYBOOK.scm` - Operational runbook
-
----
-
-# CLAUDE.md - AI Assistant Instructions
-
-## Language Policy (Hyperpolymath Standard)
-
-### ALLOWED Languages & Tools
-
-| Language/Tool | Use Case | Notes |
-|---------------|----------|-------|
-| **ReScript** | Primary application code | Compiles to JS, type-safe |
-| **Deno** | Runtime & package management | Replaces Node/npm/bun |
-| **Rust** | Performance-critical, systems, WASM | Preferred for CLI tools |
-| **Tauri 2.0+** | Mobile apps (iOS/Android) | Rust backend + web UI |
-| **Dioxus** | Mobile apps (native UI) | Pure Rust, React-like |
-| **Gleam** | Backend services | Runs on BEAM or compiles to JS |
-| **Bash/POSIX Shell** | Scripts, automation | Keep minimal |
-| **JavaScript** | Only where ReScript cannot | MCP protocol glue, Deno APIs |
-| **Python** | SaltStack only | No other Python permitted |
-| **Nickel** | Configuration language | For complex configs |
-| **Guile Scheme** | State/meta files | STATE.scm, META.scm, ECOSYSTEM.scm |
-| **Julia** | Batch scripts, data processing | Per RSR |
-| **OCaml** | AffineScript compiler | Language-specific |
-| **Ada** | Safety-critical systems | Where required |
-
-### BANNED - Do Not Use
-
-| Banned | Replacement |
-|--------|-------------|
-| TypeScript | ReScript |
-| Node.js | Deno |
-| npm | Deno |
-| Bun | Deno |
-| pnpm/yarn | Deno |
-| Go | Rust |
-| Python (general) | ReScript/Rust |
-| Java/Kotlin | Rust/Tauri/Dioxus |
-| Swift | Tauri/Dioxus |
-| React Native | Tauri/Dioxus |
-| Flutter/Dart | Tauri/Dioxus |
-
-### Mobile Development
-
-**No exceptions for Kotlin/Swift** - use Rust-first approach:
-
-1. **Tauri 2.0+** - Web UI (ReScript) + Rust backend, MIT/Apache-2.0
-2. **Dioxus** - Pure Rust native UI, MIT/Apache-2.0
-
-Both are FOSS with independent governance (no Big Tech).
-
-### Enforcement Rules
-
-1. **No new TypeScript files** - Convert existing TS to ReScript
-2. **No package.json for runtime deps** - Use deno.json imports
-3. **No node_modules in production** - Deno caches deps automatically
-4. **No Go code** - Use Rust instead
-5. **Python only for SaltStack** - All other Python must be rewritten
-6. **No Kotlin/Swift for mobile** - Use Tauri 2.0+ or Dioxus
-
-### Package Management
-
-- **Primary**: Guix (guix.scm)
-- **Fallback**: Nix (flake.nix)
-- **JS deps**: Deno (deno.json imports)
-
-### Security Requirements
-
-- No MD5/SHA1 for security (use SHA256+)
-- HTTPS only (no HTTP URLs)
-- No hardcoded secrets
-- SHA-pinned dependencies
-- SPDX license headers on all files
-
+# CLAUDE.md — RAZE-TUI Project Instructions
+
+## READ FIRST
+
+1. Read `0-AI-MANIFEST.a2ml` — canonical file locations
+2. Read `.machine_readable/STATE.a2ml` — current position, TSDM categories, what's done/next
+3. Follow TSDM: **must** items first, then should, then could
+
+## Architecture (5-layer, 5-language)
+
+```
+Idris2 ABI (src/interface/abi/)     — proves interface correctness
+    ↓ generates C headers
+Zig FFI (src/interface/ffi/)        — PURE pass-through, ZERO logic
+    ↓ C ABI
+SPARK core (src/spark/)             — proves implementation correctness
+    ├── Ada (src/ada/)              — direct `with` (SPARK is Ada)
+    └── Rust (src/rust/)            — extern "C" via Zig bridge
+```
+
+## Critical Rules for This Repo
+
+- **Zig bridge = ZERO logic.** No state, no allocation, no conditionals. Only `extern fn` forwarding.
+- **Rust = `#![forbid(unsafe_code)]`**. Never add unsafe blocks.
+- **SPARK = `with SPARK_Mode`** on all packages. Pre/Post on every subprogram.
+- **Idris2 = `%default total`**. No `believe_me`, `assert_total`, `sorry`.
+- **SPDX headers** on every file, every language.
+- **Run `panic-attack assail`** before every commit.
+- **Check proven repo** for formally verified alternatives before writing new code.
+
+## Build Commands
+
+```bash
+just build          # Build Zig FFI + link SPARK + Rust
+just check-abi      # Type-check Idris2 ABI
+just prove          # Run GNATprove on SPARK packages
+just test           # Run all tests (Zig + Rust + Ada)
+just run            # Run the TUI demo
+```
+
+## Language Roles
+
+| Language | Role | Location | Editable? |
+|----------|------|----------|-----------|
+| Idris2 | ABI proofs | `src/interface/abi/` | Yes |
+| Zig | Pure FFI bridge | `src/interface/ffi/` | Bridge only |
+| SPARK | Verified core | `src/spark/` | Yes |
+| Ada | Presentation | `src/ada/` | Yes |
+| Rust | Consumer | `src/rust/` | Yes |
+
+## Next Session TODO (STANDING)
+
+1. **RSR compliance audit** — run `just validate-rsr`, fix any gaps
+2. **panic-attack assail** — run and address findings
+3. **proven swap-outs** — check if proven repo has verified alternatives for any SPARK packages
+4. **SPARK proofs** — discharge GNATprove obligations on all SPARK packages
+5. **Terminal backend** — implement ANSI rendering and raw mode in SPARK
+6. **Contractiles** — fill in must/trust/dust/intend files with real checks
+7. **Update STATE.a2ml** — adjust completion percentage after work
+
+## Banned Patterns
+
+| Pattern | Language | Why |
+|---------|----------|-----|
+| `believe_me` | Idris2 | Unsound — bypasses type checker |
+| `assert_total` | Idris2 | Unsound — hides non-termination |
+| `sorry` | Idris2/Lean | Unsound — admits unproven goals |
+| `unsafe` | Rust | Forbidden by `#![forbid(unsafe_code)]` |
+| `unsafeCoerce` | Haskell | Unsound — bypasses types |
+| `Obj.magic` | OCaml | Unsound — bypasses types |
+| `pragma Suppress` | Ada | Disables runtime checks — defeats SPARK |

.machine_readable/AGENTIC.a2ml

@@ -2,10 +2,10 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # AGENTIC.a2ml — AI agent constraints and capabilities
-# Defines what AI agents can and cannot do in this repository.
+# Updated: 2026-03-16
 
 [metadata]
-version = "0.1.0"
+version = "0.2.0"
 last-updated = "2026-03-16"
 
 [agent-permissions]
@@ -17,8 +17,34 @@ can-create-files = true
 
 [agent-constraints]
 # What AI agents must NOT do:
-# - Never use banned language patterns (believe_me, unsafeCoerce, etc.)
+# - Never use banned patterns (believe_me, assert_total, sorry, unsafeCoerce, Obj.magic, unsafe)
 # - 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)
+# - Never add logic to the Zig FFI bridge (must remain pure pass-through)
+# - Never use unsafe in Rust (crate uses #![forbid(unsafe_code)])
+
+[session-start]
+actions = [
+    "Read 0-AI-MANIFEST.a2ml FIRST",
+    "Read .machine_readable/STATE.a2ml for current position and TSDM categories",
+    "Check TSDM scoping: must items FIRST, then should, then could",
+    "Check proven repo for formally verified alternatives before writing new code",
+    "Offer to continue Phase 1 work (SPARK proofs, terminal backend)"
+]
+
+[pre-commit]
+actions = [
+    "Run panic-attack assail",
+    "Verify SPDX headers on all changed files",
+    "Verify no banned patterns in any language",
+    "Update .machine_readable/STATE.a2ml if completion changed"
+]
+
+[language-roles]
+idris2 = { role = "ABI specification", location = "src/interface/abi/", editable = true }
+spark = { role = "Verified implementation", location = "src/spark/", editable = true }
+ada = { role = "Presentation layer", location = "src/ada/", editable = true }
+zig = { role = "Pure FFI bridge ONLY", location = "src/interface/ffi/", editable = "bridge-only" }
+rust = { role = "Consumer/ecosystem", location = "src/rust/", editable = true }

.machine_readable/ECOSYSTEM.a2ml

@@ -1,10 +1,50 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
-# ECOSYSTEM.a2ml — Ecosystem position
-# Converted from ECOSYSTEM.scm on 2026-03-15
+# ECOSYSTEM.a2ml — Ecosystem position and relationships
+# Updated: 2026-03-16
 
 [metadata]
 project = "raze-tui"
 ecosystem = "hyperpolymath"
 
 [position]
-type = "component"
+type = "library"
+purpose = "Polyglot TUI framework with formally verified core"
+domain = "terminal-user-interface"
+
+[related-projects]
+
+[related-projects.panll]
+relationship = "consumer"
+description = "PanLL can render panels as TUI widgets via raze-tui"
+integration = "raze-tui implements PanLL panel renderer for terminal contexts"
+
+[related-projects.proven]
+relationship = "dependency"
+description = "Shared formally verified Idris2 library"
+integration = "raze-tui ABI may import proven primitives (state machines, bounded types)"
+
+[related-projects.proven-servers]
+relationship = "sibling"
+description = "Formally verified protocol implementations"
+integration = "raze-tui could use proven-servers FSM for event loop state machine"
+
+[related-projects.typell]
+relationship = "substrate"
+description = "PanLL's type-theory engine"
+integration = "TypeLL type constraints could validate raze-tui widget layouts"
+
+[related-projects.session-sentinel]
+relationship = "consumer"
+description = "Session Sentinel could use raze-tui for its TUI diagnostic mode"
+integration = "session-sentinel --tui would render health dashboard via raze-tui widgets"
+
+[related-projects.idaptik]
+relationship = "potential-consumer"
+description = "IDApTIK's level architect could use raze-tui for terminal-based level editing"
+
+[languages]
+idris2 = "ABI specifications with dependent type proofs"
+spark = "Formally verified core implementation"
+ada = "Terminal presentation layer"
+zig = "Pure FFI bridge (zero logic)"
+rust = "Ecosystem integration and async support"

.machine_readable/META.a2ml

@@ -1,9 +1,60 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
-# META.a2ml — Project meta-information
-# Converted from META.scm on 2026-03-15
+# META.a2ml — Architecture decisions and development practices
+# Updated: 2026-03-16
 
 [metadata]
 project = "raze-tui"
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
 license = "PMPL-1.0-or-later"
 standard = "RSR 2026"
+
+[architecture-decisions]
+
+[architecture-decisions.adr-001]
+title = "Idris2 ABI + SPARK implementation + Zig FFI architecture"
+status = "accepted"
+date = "2026-03-16"
+rationale = """
+Idris2 dependent types prove interface correctness (bounded values, valid enums,
+monotonic state versions). SPARK Pre/Post contracts prove implementation
+correctness (no runtime errors, contract fulfillment). Zig provides zero-overhead
+C ABI bridging. These are complementary proof techniques covering different
+correctness properties.
+"""
+
+[architecture-decisions.adr-002]
+title = "SPARK as shared verified core between Ada and Rust"
+status = "accepted"
+date = "2026-03-16"
+rationale = """
+Ada consumes SPARK packages directly (SPARK IS Ada). Rust consumes SPARK via
+pragma Export + Zig FFI bridge. Both get the same verified implementation.
+Single source of truth for state management and event handling.
+"""
+
+[architecture-decisions.adr-003]
+title = "Pure Zig FFI bridge with zero logic"
+status = "accepted"
+date = "2026-03-16"
+rationale = """
+The Zig bridge must be a dumb pass-through: no state, no allocation, no logic.
+This ensures the bridge itself cannot introduce bugs. All logic lives in SPARK
+(verified) or Rust (type-safe). The bridge is thin enough to audit by inspection.
+"""
+
+[development-practices]
+axis-1 = "must > intend > like"
+axis-2 = "corrective > adaptive > perfective"
+axis-3 = "systems > compliance > effects"
+scoping-first = true
+idris-unsound-scan = "believe_me/assert_total"
+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"
+effects-evidence = "benchmark execution/results and maintainer status dialogue/review"
+compliance-tooling = "panic-attack"
+effects-tooling = "ecological checking with sustainabot guidance"
+
+[design-rationale]
+why-not-single-language = "No single language provides dependent type proofs (Idris2), runtime contract verification (SPARK), zero-overhead FFI (Zig), and ecosystem breadth (Rust) simultaneously"
+why-spark-not-rust-core = "SPARK's Pre/Post/Contract_Cases are provable by GNATprove; Rust's type system cannot express equivalent runtime contracts without macros or external tools"
+why-idris2-not-spark-for-abi = "Idris2 dependent types can prove things SPARK cannot: type-level bounded naturals, indexed widget trees, protocol state machines with Nat indices"