docs(oblibeniser): replace template placeholders with bespoke reversible computing content

All Idris2 ABI files now define ReversibleOperation, InverseProof,
AuditEntry, StateSnapshot, and UndoStack types with layout proofs.
Zig FFI implements operation recording, inverse computation,
hash-chained audit trail, and bounded undo stack. README, ROADMAP,
TOPOLOGY, and all machine-readable metadata updated for reversible
computing domain.

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

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -1,12 +1,12 @@
 # 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 oblibeniser
 # Defines what AI agents can and cannot do in this repository.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [agent-permissions]
 can-edit-source = true
@@ -22,6 +22,9 @@ can-create-files = true
 # - 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 break the reversibility invariant: every ReversibleOperation must have an inverse
+# - Never break audit chain integrity: prevHash must always link correctly
+# - Never use unbounded data structures for undo (UndoStack must have maxDepth)
 
 [maintenance-integrity]
 fail-closed = true

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -6,13 +6,15 @@
   (version "0.1.0")
   (name "oblibeniser")
   (type "tool")
-  (purpose "Make operations reversible and auditable via Oblíbený")
+  (purpose "Make operations reversible and auditable via Oblibeny — every mutation has a provable inverse")
+  (domain "reversible-computing")
 
   (position-in-ecosystem
     (family "-iser acceleration frameworks")
     (meta-framework "iseriser")
     (relationship "sibling")
-    (top-3 ("typedqliser" "chapeliser" "verisimiser")))
+    (top-3 ("typedqliser" "chapeliser" "verisimiser"))
+    (unique-value "Only -iser focused on operation reversibility, undo, and audit trails"))
 
   (related-projects
     (project "iseriser"
@@ -27,12 +29,18 @@
     (project "verisimiser"
       (relationship "sibling-priority-3")
       (description "VeriSimDB octad database augmentation"))
+    (project "oblibeny"
+      (relationship "target-language")
+      (description "Nextgen reversible computing language — source of reversibility semantics"))
     (project "squeakwell"
       (relationship "sibling")
-      (description "Database recovery via constraint propagation"))
+      (description "Database recovery via constraint propagation — complementary to reversible operations"))
     (project "proven"
       (relationship "dependency")
       (description "Shared Idris2 verified library"))
     (project "typell"
       (relationship "dependency")
-      (description "Type theory engine"))))
+      (description "Type theory engine"))
+    (project "verisimdb"
+      (relationship "potential-consumer")
+      (description "Could use oblibeniser for reversible database operations and audit trails"))))

.machine_readable/6a2/META.a2ml

@@ -4,38 +4,61 @@
 
 (meta
   (version "0.1.0")
-  (last-updated "2026-03-20")
+  (last-updated "2026-03-21")
 
   (architecture-decisions
     (adr "001-iser-pattern"
       (status "accepted")
-      (context "Need to make powerful languages accessible without steep learning curves")
-      (decision "Use manifest-driven code generation: user describes WHAT, tool generates HOW")
-      (consequences "Users write zero target language code; all complexity in the -iser"))
+      (context "Need to make reversible computing accessible without users learning Oblibeny")
+      (decision "Use manifest-driven code generation: user describes WHAT operations to make reversible, tool generates HOW")
+      (consequences "Users write zero Oblibeny code; all reversibility logic generated by oblibeniser"))
 
     (adr "002-abi-ffi-standard"
       (status "accepted")
-      (context "Need verified interop between Rust CLI, target language, and user code")
-      (decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge")
+      (context "Need verified interop between Rust CLI, Oblibeny codegen, and user code")
+      (decision "Idris2 ABI for formal proofs (InverseProof, AuditEntry layout), Zig FFI for C-ABI bridge")
       (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs"))
 
     (adr "003-rsr-template"
       (status "accepted")
       (context "Need consistent project structure across 29+ -iser repos")
       (decision "All repos cloned from rsr-template-repo with full CI/CD and governance")
-      (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one")))
+      (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one"))
+
+    (adr "004-reversible-computing-core"
+      (status "accepted")
+      (context "Every mutation in the system must be undoable with formal guarantees")
+      (decision "ReversibleOperation type pairs forward+inverse; InverseProof proves inverse(forward(x))=x")
+      (consequences "All operations auditable and undoable; enables time-travel debugging"))
+
+    (adr "005-hash-chained-audit"
+      (status "accepted")
+      (context "Audit trail must be tamper-evident for compliance and security")
+      (decision "AuditEntry records are hash-chained; each entry's prevHash links to the previous entryHash")
+      (consequences "Any tampering breaks the chain; integrity verifiable in O(n) time"))
+
+    (adr "006-bounded-undo-stack"
+      (status "accepted")
+      (context "Unbounded undo history would consume unbounded memory")
+      (decision "UndoStack has a configurable maxDepth; oldest entries evicted when full")
+      (consequences "Predictable memory usage; time-travel limited to maxDepth operations")))
 
   (development-practices
-    (language "Rust" (purpose "CLI and orchestration"))
-    (language "Idris2" (purpose "ABI formal proofs"))
-    (language "Zig" (purpose "FFI C-ABI bridge"))
+    (language "Rust" (purpose "CLI orchestration, manifest parsing, build coordination"))
+    (language "Idris2" (purpose "ABI formal proofs — ReversibleOperation, InverseProof, AuditEntry layout"))
+    (language "Zig" (purpose "FFI C-ABI bridge — operation recording, inverse computation, audit, undo"))
+    (language "Oblibeny" (purpose "Target language for generated reversible wrappers (future)"))
     (build-tool "cargo")
     (ci "GitHub Actions (17 workflows)"))
 
   (design-rationale
+    (principle "Every operation is reversible"
+      (explanation "The core guarantee: for any forward(x), there exists inverse such that inverse(forward(x)) = x"))
+    (principle "Every state change is auditable"
+      (explanation "Hash-chained audit entries record actor, authorisation, timestamp, and operation for compliance"))
     (principle "Manifest-driven"
       (explanation "User intent captured in TOML; all generation is deterministic and reproducible"))
     (principle "Formally verified bridges"
-      (explanation "Idris2 dependent types prove interface correctness at compile time"))
+      (explanation "Idris2 dependent types prove interface correctness — InverseProof, struct layouts"))
     (principle "Zero target language exposure"
-      (explanation "Users never write Chapel/Julia/Futhark/etc. — the -iser handles everything"))))
+      (explanation "Users never write Oblibeny directly — the -iser handles everything"))))

.machine_readable/6a2/NEUROSYM.a2ml

@@ -1,21 +1,23 @@
 # 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 oblibeniser
 # Configuration for Hypatia scanning and symbolic reasoning.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [hypatia-config]
 scan-enabled = true
 scan-depth = "standard"  # quick | standard | deep
 report-format = "logtalk"
 
 [symbolic-rules]
-# Custom symbolic rules for this project
+# Custom symbolic rules for oblibeniser
 # - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
+# - { name = "inverse-proof-required", pattern = "ReversibleOperation.*inverse_verified.*false", severity = "warning" }
+# - { name = "audit-chain-integrity", pattern = "prev_hash.*=.*0.*sequence_no.*>.*1", severity = "critical" }
 
 [neural-config]
 # Neural pattern detection settings

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -1,25 +1,26 @@
 # 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
+# PLAYBOOK.a2ml — Operational playbook for oblibeniser
 # Runbooks, incident response, deployment procedures.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [deployment]
-# method = "gitops"  # gitops | manual | ci-triggered
-# target = "container"  # container | binary | library | wasm
+method = "ci-triggered"
+target = "binary"  # Rust CLI binary + Zig shared library
 
 [incident-response]
-# 1. Check .machine_readable/STATE.a2ml for current status
+# 1. Check .machine_readable/6a2/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
+# 5. Verify audit chain integrity: `oblibeniser verify-audit`
 
 [release-process]
-# 1. Update version in STATE.a2ml, META.a2ml, Justfile
+# 1. Update version in STATE.a2ml, META.a2ml, Cargo.toml, Justfile
 # 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass)
 # 3. Optional local permission hardening: `just perms-snapshot && just perms-lock`
 # 4. Tag and push

.machine_readable/6a2/STATE.a2ml

@@ -5,31 +5,34 @@
 (state
   (metadata
     (version "0.1.0")
-    (last-updated "2026-03-20")
+    (last-updated "2026-03-21")
     (author "Jonathan D.A. Jewell"))
 
   (project-context
     (name "oblibeniser")
-    (description "Make operations reversible and auditable via Oblíbený")
-    (status "scaffold")
+    (description "Make operations reversible and auditable via Oblibeny")
+    (domain "reversible-computing")
+    (status "scaffold-documented")
     (priority "—")
     (ecosystem "-iser family (https://github.com/hyperpolymath/iseriser)"))
 
   (current-position
-    (phase "initial-scaffold")
-    (completion-percentage 5)
-    (milestone "Architecture defined, CLI scaffolded, RSR template complete"))
+    (phase "scaffold-with-bespoke-abi")
+    (completion-percentage 15)
+    (milestone "Bespoke Idris2 ABI types (ReversibleOperation, InverseProof, AuditEntry, StateSnapshot, UndoStack), Zig FFI with operation recording/inverse/audit/undo, integration tests, documentation"))
 
   (route-to-mvp
-    (step 1 "Replace codegen stubs with target-language-specific generation")
-    (step 2 "Implement Idris2 ABI proofs for core invariants")
-    (step 3 "Build Zig FFI bridge")
-    (step 4 "Integration tests with real-world examples")
-    (step 5 "Documentation and examples"))
+    (step 1 "Wire Rust CLI codegen to emit Oblibeny reversible wrappers")
+    (step 2 "Implement domain-specific inverse computation (file, SQL, config)")
+    (step 3 "Cryptographic audit trail (hash-chain with post-quantum signing)")
+    (step 4 "Time-travel debugging (replay/reverse from snapshots)")
+    (step 5 "Integration tests with real-world use cases (DB migration, config rollback)")
+    (step 6 "PanLL panel and BoJ-server cartridge"))
 
   (blockers-and-issues
     (none "Project is in scaffold phase — no blockers yet"))
 
   (critical-next-actions
-    (action "Implement codegen for primary use case")
-    (action "Write first working example end-to-end")))
+    (action "Implement codegen for reversible wrappers (Phase 1)")
+    (action "Write first end-to-end example: file mutation with undo")
+    (action "Connect Rust manifest parser to Zig FFI via generated C headers")))

.machine_readable/ai/AI.a2ml

@@ -1,14 +1,30 @@
-
-# AI Assistant Instructions
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# AI Assistant Instructions for oblibeniser
 
 ## Repository Focus
-- `rsr-template-repo` is treated as a Rhodium Standard Repository; obey the Rhodium policies and keep `.machine_readable/` authoritative.
-- All machine-readable content lives under `.machine_readable/` — state files (a2ml), bot directives, and contractiles.
-- Prefer to keep generated files out of source control, and regenerate them with the documented commands before committing.
+- `oblibeniser` makes operations reversible and auditable via Oblibeny
+- Core abstraction: ReversibleOperation (forward + inverse + proof)
+- Domain types: InverseProof, AuditEntry, StateSnapshot, UndoStack
+- Follows the -iser pattern: manifest -> Idris2 ABI -> Zig FFI -> codegen
+- All machine-readable content lives under `.machine_readable/` — state files (a2ml), bot directives, and contractiles
+
+## Key Invariants
+- Every ReversibleOperation MUST have a provable inverse
+- Audit trail entries MUST be hash-chained (prevHash links to prior entryHash)
+- UndoStack MUST be bounded (maxDepth prevents unbounded memory growth)
+- InverseProof MUST verify: inverse(forward(x)) = x
+
+## Architecture
+- Rust CLI (src/main.rs) — orchestrates manifest parsing and codegen
+- Idris2 ABI (src/interface/abi/) — formal proofs of reversibility and layout
+- Zig FFI (src/interface/ffi/) — C-ABI bridge with operation recording, audit, undo
+- Codegen (src/codegen/) — generates Oblibeny reversible wrappers
 
 ## Workflow
-1. Inspect `.machine_readable/STATE.a2ml` for blockers and next actions.
-2. Respect any constraints listed inside `.machine_readable/AGENTIC.a2ml` when tooling changes are requested.
+1. Inspect `.machine_readable/6a2/STATE.a2ml` for blockers and next actions.
+2. Respect any constraints listed inside `.machine_readable/6a2/AGENTIC.a2ml`.
 3. After finishing edits, update STATE with your outcomes and commit with a concise, imperative message.
 
 ## Delivery Promises

0-AI-MANIFEST.a2ml

@@ -1,19 +1,24 @@
-# ⚠️ STOP - CRITICAL READING REQUIRED
-
-**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# STOP - CRITICAL READING REQUIRED
+#
+# THIS FILE MUST BE READ FIRST BY ALL AI AGENTS
 
 ## WHAT IS THIS?
 
-This is the AI manifest for **[YOUR-REPO-NAME]**. It declares:
-- Canonical file locations (where things MUST be, and nowhere else)
-- Critical invariants (rules that must NEVER be violated)
-- Repository structure and organization
+This is the AI manifest for **oblibeniser** — a tool that makes operations
+reversible and auditable via Oblibeny (Czech: "favourite"), a nextgen language
+for reversible computing.
+
+Core concept: every forward operation has a provable inverse, enabling undo,
+audit trails, and time-travel debugging.
 
 ## CANONICAL LOCATIONS (UNIVERSAL RULE)
 
 ### Machine-Readable Metadata: `.machine_readable/` ONLY
 
-These 6 a2ml files MUST exist in `.machine_readable/` directory ONLY:
+These 6 a2ml files MUST exist in `.machine_readable/6a2/` directory ONLY:
 1. **STATE.a2ml** - Project state, progress, blockers
 2. **META.a2ml** - Architecture decisions, governance
 3. **ECOSYSTEM.a2ml** - Position in ecosystem, relationships
@@ -55,7 +60,7 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
 ### AI Configuration & Guides: `.machine_readable/ai/` ONLY
 
 - `AI.a2ml` - Language-specific or LLM-specific patterns
-- `PLACEHOLDERS.md` - Bootstrap guide
+- `PLACEHOLDERS.adoc` - Bootstrap guide
 
 ### Community & Forge Metadata: `.github/` ONLY
 
@@ -80,41 +85,61 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
 6. **Container images** - MUST use Chainguard base (`cgr.dev/chainguard/wolfi-base:latest` or `cgr.dev/chainguard/static:latest`)
 7. **Container runtime** - Podman, never Docker. Files are `Containerfile`, never `Dockerfile`
 8. **Container orchestration** - `selur-compose`, never `docker-compose`
+9. **Reversibility invariant** - Every ReversibleOperation MUST have a provable inverse
+10. **Audit chain integrity** - Audit entries MUST be hash-chained; breaks are critical errors
 
 ## REPOSITORY STRUCTURE
 
 This repo follows the **Dual-Track** architecture:
 
 ```
-[YOUR-REPO-NAME]/
+oblibeniser/
 ├── 0-AI-MANIFEST.a2ml         # THIS FILE (start here)
 ├── README.adoc                 # High-level orientation (Rich Human)
 ├── ROADMAP.adoc                # Future direction
 ├── CONTRIBUTING.adoc           # Human contribution guide
-├── GOVERNANCE.adoc             # Decision-making model
+├── Cargo.toml                  # Rust CLI project
 ├── Justfile                    # Task runner
 ├── Containerfile               # OCI build
-├── LICENSE                     # Primary license
+├── LICENSE                     # Primary license (PMPL-1.0-or-later)
 ├── src/                        # Source code
+│   ├── main.rs                 # CLI entrypoint
+│   ├── lib.rs                  # Library root
+│   ├── manifest/               # oblibeniser.toml parser
+│   ├── codegen/                # Oblibeny reversible wrapper codegen
 │   └── interface/              # Verified Interface Seams
-│       ├── abi/                # Idris2 ABI (The Spec)
+│       ├── abi/                # Idris2 ABI (Types, Layout, Foreign)
+│       │   ├── Types.idr       # ReversibleOperation, InverseProof, AuditEntry, etc.
+│       │   ├── Layout.idr      # C-ABI struct layouts with proofs
+│       │   └── Foreign.idr     # FFI declarations for all operations
 │       ├── ffi/                # Zig FFI (The Bridge)
+│       │   ├── build.zig
+│       │   ├── src/main.zig    # FFI implementation
+│       │   └── test/           # Integration tests
 │       └── generated/          # C Headers (The Result)
 ├── container/                  # Stapeln container ecosystem
 ├── docs/                       # Technical depths
-│   ├── attribution/            # Citations, owners, maintainers (adoc)
+│   ├── attribution/            # Citations, owners, maintainers
 │   ├── architecture/           # Topology, diagrams
-│   ├── theory/                 # Domain theory
+│   ├── theory/                 # Domain theory (reversible computing)
 │   └── practice/               # Manuals
-├── docs/legal/                  # Legal exhibits and full texts
 └── .machine_readable/          # ALL machine-readable metadata
+    └── 6a2/                    # STATE, META, ECOSYSTEM, etc.
 ```
 
+## DOMAIN CONCEPTS
+
+- **ReversibleOperation**: A forward operation paired with its inverse
+- **InverseProof**: Dependent-type proof that `inverse(forward(x)) = x`
+- **AuditEntry**: Hash-chained record of who did what, when
+- **StateSnapshot**: Serialised system state before/after an operation
+- **UndoStack**: Bounded LIFO stack of operations for time-travel
+
 ## SESSION STARTUP CHECKLIST
 
-✅ Read THIS file (0-AI-MANIFEST.a2ml) first
-✅ Understand canonical location: `.machine_readable/`
-✅ State understanding of canonical locations
+Read THIS file (0-AI-MANIFEST.a2ml) first
+Understand canonical location: `.machine_readable/`
+State understanding of canonical locations
 
 ## ATTESTATION PROOF