diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index b0b1ed6..d54748b 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -18,7 +18,17 @@ on:
   pull_request:
   workflow_dispatch:
 
+# A called reusable workflow cannot request MORE permissions than its caller
+# grants — if it does, the run is rejected before any job starts
+# (startup_failure, zero jobs, no check run to inspect).
+#
+# standards@0ced540e ("chore: estate-wide security compliance", 2026-07-26)
+# added `actions: read` to governance-reusable.yml's own permissions block.
+# Because this caller pins the reusable at @main rather than a SHA, that change
+# arrived immediately and broke Governance here. `actions: read` is mirrored
+# below to match.
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.gitignore b/.gitignore
index 56e803f..ac1cd63 100644
--- a/.gitignore
+++ b/.gitignore
@@ -25,3 +25,26 @@ deps/
 *.tmp
 Thumbs.db
 dist/
+
+# Secrets — never commit these
+.env
+.env.*
+*.key
+*.pem
+secrets/
+
+# Agent scratch and worktrees
+.claude/
+
+# SQLite artifacts (the Zig bridge links libsqlite3)
+*.db
+*.db-journal
+*.db-shm
+*.db-wal
+
+# Editors
+*.swp
+*.swo
+*.bak
+.idea/
+.vscode/
diff --git a/ABI-FFI-README.md b/ABI-FFI-README.md
index dda367a..684a9a0 100644
--- a/ABI-FFI-README.md
+++ b/ABI-FFI-README.md
@@ -1,385 +1,105 @@
-{{~ Aditionally delete this line and fill out the template below ~}}
+<!--
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
 
-# {{PROJECT}} ABI/FFI Documentation
+# ABI / FFI — how GNPL reaches Lithoglyph
 
-## Overview
+This repository follows the estate standard: **ABI defined in Idris2, FFI implemented in
+Zig**, meeting at the C ABI. No C is written by hand.
 
-This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
+> **History:** this file was previously the unfilled RSR template — 385 lines of
+> `{{project}}` placeholders documenting an `ffi/zig/` tree that did not compile. It has
+> been replaced with what the repository actually contains.
 
-- **ABI (Application Binary Interface)** defined in **Idris2** with formal proofs
-- **FFI (Foreign Function Interface)** implemented in **Zig** for C compatibility
-- **Generated C headers** bridge Idris2 ABI to Zig FFI
-- **Any language** can call through standard C ABI
+## The path
 
-## Architecture
-
-```
-┌─────────────────────────────────────────────┐
-│  ABI Definitions (Idris2)                   │
-│  src/abi/                                   │
-│  - Types.idr      (Type definitions)        │
-│  - Layout.idr     (Memory layout proofs)    │
-│  - Foreign.idr    (FFI declarations)        │
-└─────────────────┬───────────────────────────┘
-                  │
-                  │ generates (at compile time)
-                  ▼
-┌─────────────────────────────────────────────┐
-│  C Headers (auto-generated)                 │
-│  generated/abi/{{project}}.h                │
-└─────────────────┬───────────────────────────┘
-                  │
-                  │ imported by
-                  ▼
-┌─────────────────────────────────────────────┐
-│  FFI Implementation (Zig)                   │
-│  ffi/zig/src/main.zig                       │
-│  - Implements C-compatible functions        │
-│  - Zero-cost abstractions                   │
-│  - Memory-safe by default                   │
-└─────────────────┬───────────────────────────┘
-                  │
-                  │ compiled to lib{{project}}.so/.a
-                  ▼
-┌─────────────────────────────────────────────┐
-│  Any Language via C ABI                     │
-│  - Rust, ReScript, Julia, Python, etc.     │
-└─────────────────────────────────────────────┘
-```
-
-## Directory Structure
-
-```
-{{project}}/
-├── src/
-│   ├── abi/                    # ABI definitions (Idris2)
-│   │   ├── Types.idr           # Core type definitions with proofs
-│   │   ├── Layout.idr          # Memory layout verification
-│   │   └── Foreign.idr         # FFI function declarations
-│   └── lib/                    # Core library (any language)
-│
-├── ffi/
-│   └── zig/                    # FFI implementation (Zig)
-│       ├── build.zig           # Build configuration
-│       ├── build.zig.zon       # Dependencies
-│       ├── src/
-│       │   └── main.zig        # C-compatible FFI implementation
-│       ├── test/
-│       │   └── integration_test.zig
-│       └── include/
-│           └── {{project}}.h   # C header (optional, can be generated)
-│
-├── generated/                  # Auto-generated files
-│   └── abi/
-│       └── {{project}}.h       # Generated from Idris2 ABI
-│
-└── bindings/                   # Language-specific wrappers (optional)
-    ├── rust/
-    ├── rescript/
-    └── julia/
-```
-
-## Why Idris2 for ABI?
-
-### 1. **Formal Verification**
-
-Idris2's dependent types allow proving properties about the ABI at compile-time:
-
-```idris
--- Prove struct size is correct
-public export
-exampleStructSize : HasSize ExampleStruct 16
-
--- Prove field alignment is correct
-public export
-fieldAligned : Divides 8 (offsetOf ExampleStruct.field)
-
--- Prove ABI is platform-compatible
-public export
-abiCompatible : Compatible (ABI 1) (ABI 2)
-```
-
-### 2. **Type Safety**
-
-Encode invariants that C/Zig cannot express:
-
-```idris
--- Non-null pointer guaranteed at type level
-data Handle : Type where
-  MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle
-
--- Array with length proof
-data Buffer : (n : Nat) -> Type where
-  MkBuffer : Vect n Byte -> Buffer n
-```
-
-### 3. **Platform Abstraction**
-
-Platform-specific types with compile-time selection:
-
-```idris
-CInt : Platform -> Type
-CInt Linux = Bits32
-CInt Windows = Bits32
-
-CSize : Platform -> Type
-CSize Linux = Bits64
-CSize Windows = Bits64
-```
-
-### 4. **Safe Evolution**
-
-Prove that new ABI versions are backward-compatible:
-
-```idris
--- Compiler enforces compatibility
-abiUpgrade : ABI 1 -> ABI 2
-abiUpgrade old = MkABI2 {
-  -- Must preserve all v1 fields
-  v1_compat = old,
-  -- Can add new fields
-  new_features = defaults
-}
 ```
-
-## Why Zig for FFI?
-
-### 1. **C ABI Compatibility**
-
-Zig exports C-compatible functions naturally:
-
-```zig
-export fn library_function(param: i32) i32 {
-    return param * 2;
-}
-```
-
-### 2. **Memory Safety**
-
-Compile-time safety without runtime overhead:
-
-```zig
-// Null check enforced at compile time
-const handle = init() orelse return error.InitFailed;
-defer free(handle);
+GNPL  ──lowers to──▶  GQLdt (Lean 4)
+                          │
+                          │ FFI: links -Lbridge/zig-out/lib -llith_bridge
+                          ▼
+                      bridge/ (Zig)  ── C ABI ──▶  Lithoglyph Form.Bridge
 ```
 
-### 3. **Cross-Compilation**
-
-Built-in cross-compilation to any platform:
+`lakefile.lean` links the Lean executables against `bridge/zig-out/lib/liblith_bridge.a`.
+**That archive must exist before `lake build` runs.**
 
-```bash
-zig build -Dtarget=x86_64-linux
-zig build -Dtarget=aarch64-macos
-zig build -Dtarget=x86_64-windows
-```
+## Layout
 
-### 4. **Zero Dependencies**
+| Path | Role |
+|---|---|
+| `src/GQLdt/ABI/Types.idr` | ABI type definitions |
+| `src/GQLdt/ABI/Layout.idr` | memory-layout proofs |
+| `src/GQLdt/ABI/Foreign.idr` | foreign declarations |
+| `bridge/build.zig` | build script (`addLibrary`, Zig ≥ 0.15 API) |
+| `bridge/lith_root.zig` | FFI entry point — the exported C surface |
+| `bridge/lith_types.zig` | C-ABI structs (`ActorIdC`, `RationaleC`, `ProvenanceC`, `TrackedValueC`, `ProofBlob`, `PromptScoresC`) |
+| `bridge/lith_insert.zig`, `bridge/lith_persist.zig` | insert + persistence implementation |
 
-No runtime, no libc required (unless explicitly needed):
-
-```zig
-// Minimal binary size
-pub const lib = @import("std");
-// Only includes what you use
-```
+`bridge/` is the **only** live Zig tree. Two earlier skeletons (`bridge/zig/`, `ffi/zig/`)
+were removed — they were written against the pre-0.15 Build API (`addStaticLibrary`,
+`std.heap.GeneralPurposeAllocator`), failed to compile on the pinned Zig 0.16.0, and nothing
+linked against them.
 
 ## Building
 
-### Build FFI Library
-
 ```bash
-cd ffi/zig
-zig build                         # Build debug
-zig build -Doptimize=ReleaseFast  # Build optimized
-zig build test                    # Run tests
+cd bridge
+zig build                          # produces zig-out/lib/liblith_bridge.a
+zig build test                     # unit tests
+zig build -Doptimize=ReleaseFast   # optimised
 ```
 
-### Generate C Header from Idris2 ABI
-
-```bash
-cd src/abi
-idris2 --cg c-header Types.idr -o ../../generated/abi/{{project}}.h
-```
+Cross-compilation works as usual (`-Dtarget=aarch64-macos`, etc.).
 
-### Cross-Compile
+Then, from the repository root:
 
 ```bash
-cd ffi/zig
-
-# Linux x86_64
-zig build -Dtarget=x86_64-linux
-
-# macOS ARM64
-zig build -Dtarget=aarch64-macos
-
-# Windows x86_64
-zig build -Dtarget=x86_64-windows
-```
-
-## Usage
-
-### From C
-
-```c
-#include "{{project}}.h"
-
-int main() {
-    void* handle = {{project}}_init();
-    if (!handle) return 1;
-
-    int result = {{project}}_process(handle, 42);
-    if (result != 0) {
-        const char* err = {{project}}_last_error();
-        fprintf(stderr, "Error: %s\n", err);
-    }
-
-    {{project}}_free(handle);
-    return 0;
-}
-```
-
-Compile with:
-```bash
-gcc -o example example.c -l{{project}} -L./zig-out/lib
+lake build
 ```
 
-### From Idris2
-
-```idris
-import {{PROJECT}}.ABI.Foreign
-
-main : IO ()
-main = do
-  Just handle <- init
-    | Nothing => putStrLn "Failed to initialize"
-
-  Right result <- process handle 42
-    | Left err => putStrLn $ "Error: " ++ errorDescription err
-
-  free handle
-  putStrLn "Success"
-```
-
-### From Rust
-
-```rust
-#[link(name = "{{project}}")]
-extern "C" {
-    fn {{project}}_init() -> *mut std::ffi::c_void;
-    fn {{project}}_free(handle: *mut std::ffi::c_void);
-    fn {{project}}_process(handle: *mut std::ffi::c_void, input: u32) -> i32;
-}
-
-fn main() {
-    unsafe {
-        let handle = {{project}}_init();
-        assert!(!handle.is_null());
-
-        let result = {{project}}_process(handle, 42);
-        assert_eq!(result, 0);
+Zig is pinned to **0.16.0** in `mise.toml`. Lean is pinned by `lean-toolchain`
+(`leanprover/lean4:v4.15.0`), which elan reads automatically.
 
-        {{project}}_free(handle);
-    }
-}
-```
-
-### From Julia
-
-```julia
-const lib{{project}} = "lib{{project}}"
-
-function init()
-    handle = ccall((:{{project}}_init, lib{{project}}), Ptr{Cvoid}, ())
-    handle == C_NULL && error("Failed to initialize")
-    handle
-end
-
-function process(handle, input)
-    result = ccall((:{{project}}_process, lib{{project}}), Cint, (Ptr{Cvoid}, UInt32), handle, input)
-    result
-end
-
-function cleanup(handle)
-    ccall((:{{project}}_free, lib{{project}}), Cvoid, (Ptr{Cvoid},), handle)
-end
-
-# Usage
-handle = init()
-try
-    result = process(handle, 42)
-    println("Result: $result")
-finally
-    cleanup(handle)
-end
-```
-
-## Testing
-
-### Unit Tests (Zig)
-
-```bash
-cd ffi/zig
-zig build test
-```
-
-### Integration Tests
-
-```bash
-cd ffi/zig
-zig build test-integration
-```
-
-### ABI Verification (Idris2)
-
-```idris
--- Compile-time verification
-%runElab verifyABI
-
--- Runtime checks
-main : IO ()
-main = do
-  verifyLayoutsCorrect
-  verifyAlignmentsCorrect
-  putStrLn "ABI verification passed"
-```
+## Exported C surface
 
-## Contributing
+Seventeen functions, all `callconv(.C)`, from `bridge/`:
 
-When modifying the ABI/FFI:
+**Lifecycle** — `lith_init`, `lith_is_init`, `lith_close`, `lith_save`
+**Data** — `lith_insert`, `lith_insert_row`, `lith_delete_row`, `lith_table_count`
+**PROMPT scores** — `lith_get_scores`, `lith_compute_overall`
+**Proofs** — `lith_verify_proof`
+**Utility** — `lith_validate_non_empty`, `lith_timestamp_now`, `lith_get_last_error`
+**Debug/test** — `lith_debug_init_counter`, `lith_debug_magic`, `lith_test_fresh`
 
-1. **Update ABI first** (`src/abi/*.idr`)
-   - Modify type definitions
-   - Update proofs
-   - Ensure backward compatibility
+Provenance crosses the boundary as real structs, not opaque blobs: `ActorIdC`,
+`RationaleC`, `ProvenanceC` and `TrackedValueC` are marshalled directly. This is what makes
+the GNPL narration layer buildable over this stack — see `docs/LITHOGLYPH.adoc`.
 
-2. **Generate C header**
-   ```bash
-   idris2 --cg c-header src/abi/Types.idr -o generated/abi/{{project}}.h
-   ```
+> **Caveat.** `PromptScoresC.computeOverall` takes an **unweighted mean** of the six PROMPT
+> dimensions. It is not probabilistically principled, and must not become a load-bearing
+> entrenchment ordering without being revisited — see open question 2 in `docs/THEORY.adoc`.
 
-3. **Update FFI implementation** (`ffi/zig/src/main.zig`)
-   - Implement new functions
-   - Match ABI types exactly
+## Why this split
 
-4. **Add tests**
-   - Unit tests in Zig
-   - Integration tests
-   - ABI verification tests
+**Idris2 for the ABI** — dependent types let struct size, field alignment and cross-version
+compatibility be *proved* rather than asserted, so an ABI change that would break a caller
+fails at compile time.
 
-5. **Update documentation**
-   - Function signatures
-   - Usage examples
-   - Migration guide (if breaking changes)
+**Zig for the FFI** — `export fn … callconv(.C)` is C-compatible without a C compiler,
+without libc, and with cross-compilation built in.
 
-## License
+## Adding a function
 
-CC-BY-SA-4.0
+1. Declare the type in `src/GQLdt/ABI/Types.idr`; add a layout proof in `Layout.idr`.
+2. Declare it in `src/GQLdt/ABI/Foreign.idr`.
+3. Implement and `export` it in `bridge/` (match the ABI types exactly).
+4. `cd bridge && zig build && zig build test`, then `lake build` from the root.
 
-## See Also
+## Related
 
-- [Idris2 Documentation](https://idris2.readthedocs.io)
-- [Zig Documentation](https://ziglang.org/documentation/master/)
-- [Rhodium Standard Repositories](https://github.com/hyperpolymath/rhodium-standard-repositories)
-- [FFI Migration Guide](../ffi-migration-guide.md)
-- [ABI Migration Guide](../abi-migration-guide.md)
+- `docs/THEORY.adoc` — what GNPL is, and what gap it fills
+- `docs/LITHOGLYPH.adoc` — what GNPL gives Lithoglyph as a database
+- `docs/proof-debt.md` — the 16 outstanding axioms; **read before relying on any
+  verification claim**
diff --git a/Containerfile b/Containerfile
index a48fe19..8f8cb92 100644
--- a/Containerfile
+++ b/Containerfile
@@ -43,15 +43,17 @@ WORKDIR /workspace
 # Copy project files
 COPY . /workspace/
 
-# Build Lean 4 project (download dependencies)
-RUN lake build || echo "Build failed - dependencies may need to be fetched first"
-
-# Build Zig FFI bridge
-WORKDIR /workspace/bridge/zig
-RUN zig build || echo "Zig build failed - may need project setup"
-
-# Return to workspace root
+# Build the Zig FFI bridge FIRST: lakefile.lean links against
+# bridge/zig-out/lib/liblith_bridge.a, so the Lean build needs this artifact to
+# already exist. (The previous order built Lean first and masked the inevitable
+# failure with `|| echo`, which also meant a genuinely broken build still
+# produced a "successful" image.)
+WORKDIR /workspace/bridge
+RUN zig build && test -f zig-out/lib/liblith_bridge.a
+
+# Build Lean 4 project (fetches mathlib on first run)
 WORKDIR /workspace
+RUN lake build
 
 # Default command: interactive shell
 CMD ["/bin/bash"]
diff --git a/README.adoc b/README.adoc
index 55e6252..73cb46e 100644
--- a/README.adoc
+++ b/README.adoc
@@ -80,8 +80,6 @@ Lithoglyph-as-a-database is the second. See the design documents below.
 | Zig FFI bridge (`bridge/`) | *builds* | produces `zig-out/lib/liblith_bridge.a`, the
   artifact `lakefile.lean` links; `zig build test` passes
 | GNPL narration layer | *design* | `docs/THEORY.adoc` + `docs/LITHOGLYPH.adoc`; no code yet
-| `bridge/zig/`, `ffi/zig/` | *stale* | skeletons on the pre-0.15 Zig Build API; nothing
-  links against them
 |===
 
 == Build
diff --git a/bridge/zig/build.zig b/bridge/zig/build.zig
deleted file mode 100644
index f749e1f..0000000
--- a/bridge/zig/build.zig
+++ /dev/null
@@ -1,51 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// SPDX-FileCopyrightText: 2026 hyperpolymath
-//
-// Zig FFI Bridge for GQLdt
-// Provides C-compatible ABI for Lean 4 integration
-
-const std = @import("std");
-
-pub fn build(b: *std.Build) void {
-    const target = b.standardTargetOptions(.{});
-    const optimize = b.standardOptimizeOption(.{});
-
-    // Static library for FFI bridge
-    const lib = b.addStaticLibrary(.{
-        .name = "lith_bridge",
-        .root_source_file = b.path("src/main.zig"),
-        .target = target,
-        .optimize = optimize,
-    });
-
-    // Export C ABI
-    lib.linkLibC();
-
-    b.installArtifact(lib);
-
-    // Tests
-    const main_tests = b.addTest(.{
-        .root_source_file = b.path("src/main.zig"),
-        .target = target,
-        .optimize = optimize,
-    });
-
-    const run_main_tests = b.addRunArtifact(main_tests);
-
-    const test_step = b.step("test", "Run library tests");
-    test_step.dependOn(&run_main_tests.step);
-
-    // Integration tests
-    const integration_tests = b.addTest(.{
-        .root_source_file = b.path("test/integration_test.zig"),
-        .target = target,
-        .optimize = optimize,
-    });
-
-    integration_tests.linkLibrary(lib);
-
-    const run_integration_tests = b.addRunArtifact(integration_tests);
-
-    const integration_step = b.step("test-integration", "Run integration tests");
-    integration_step.dependOn(&run_integration_tests.step);
-}
diff --git a/bridge/zig/src/main.zig b/bridge/zig/src/main.zig
deleted file mode 100644
index a95c91c..0000000
--- a/bridge/zig/src/main.zig
+++ /dev/null
@@ -1,142 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (@hyperpolymath)
-//
-// Zig FFI Bridge - Main Module
-// Bidirectional FFI: Lean 4 ↔ Zig ↔ Lith Forth core
-
-const std = @import("std");
-
-/// Status code for FFI operations
-pub const LithStatus = enum(i32) {
-    ok = 0,
-    error_null_pointer = 1,
-    error_invalid_proof = 2,
-    error_type_mismatch = 3,
-    error_constraint_violation = 4,
-    error_out_of_memory = 5,
-
-    pub fn toC(self: LithStatus) c_int {
-        return @intFromEnum(self);
-    }
-};
-
-/// Opaque database handle (non-null guaranteed by Lean 4 types)
-pub const LithDb = opaque {};
-
-/// FFI-safe string view (non-owning)
-pub const LithString = struct {
-    data: [*]const u8,
-    len: usize,
-
-    pub fn fromSlice(slice: []const u8) LithString {
-        return .{ .data = slice.ptr, .len = slice.len };
-    }
-
-    pub fn toSlice(self: LithString) []const u8 {
-        return self.data[0..self.len];
-    }
-};
-
-/// Forward: Lean 4 → Zig → Lith
-/// Insert operation with proof blob
-export fn lith_insert(
-    db: *LithDb,
-    collection: [*:0]const u8,
-    document: [*]const u8,
-    doc_len: usize,
-    proof_blob: [*]const u8,
-    proof_len: usize,
-) callconv(.C) c_int {
-    _ = db;
-    _ = collection;
-    _ = document;
-    _ = doc_len;
-    _ = proof_blob;
-    _ = proof_len;
-
-    // TODO: Implement actual insertion
-    // 1. Deserialize proof blob (CBOR)
-    // 2. Verify proof against schema
-    // 3. Insert into Lith via Forth FFI
-    // 4. Return status
-
-    return LithStatus.ok.toC();
-}
-
-/// Reverse: Lith → Zig → Lean 4
-/// Register constraint checker callback
-export fn lith_register_constraint_checker(
-    db: *LithDb,
-    checker: *const fn (doc: [*]const u8, len: usize) callconv(.C) bool,
-) callconv(.C) c_int {
-    _ = db;
-    _ = checker;
-
-    // TODO: Implement callback registration
-    // Store function pointer for later invocation
-    // When Lith validates data, call this Lean 4 checker
-
-    return LithStatus.ok.toC();
-}
-
-/// Get discovered functional dependencies
-export fn lith_get_discovered_fds(
-    db: *LithDb,
-    collection: [*:0]const u8,
-    out_fds: *[*]u8,
-    out_len: *usize,
-) callconv(.C) c_int {
-    _ = db;
-    _ = collection;
-    _ = out_fds;
-    _ = out_len;
-
-    // TODO: Implement FD discovery
-    // 1. Query Lith for collection statistics
-    // 2. Run FD discovery algorithm (DFD, TANE, etc.)
-    // 3. Serialize FDs to CBOR
-    // 4. Return pointer + length
-
-    return LithStatus.ok.toC();
-}
-
-/// Verify normalization proof
-export fn lith_verify_normalization_proof(
-    db: *LithDb,
-    step_blob: [*]const u8,
-    step_len: usize,
-    proof_blob: [*]const u8,
-    proof_len: usize,
-) callconv(.C) c_int {
-    _ = db;
-    _ = step_blob;
-    _ = step_len;
-    _ = proof_blob;
-    _ = proof_len;
-
-    // TODO: Implement proof verification
-    // 1. Deserialize normalization step
-    // 2. Deserialize Lean 4 proof
-    // 3. Verify proof is valid for step
-    // 4. Return status
-
-    return LithStatus.ok.toC();
-}
-
-/// Free memory allocated by FFI functions
-export fn lith_free(ptr: [*]u8, len: usize) callconv(.C) void {
-    const allocator = std.heap.c_allocator;
-    const slice = ptr[0..len];
-    allocator.free(slice);
-}
-
-test "LithStatus roundtrip" {
-    const status = LithStatus.ok;
-    try std.testing.expectEqual(@as(c_int, 0), status.toC());
-}
-
-test "LithString conversion" {
-    const str = "Hello, Lith!";
-    const lith_str = LithString.fromSlice(str);
-    try std.testing.expectEqualSlices(u8, str, lith_str.toSlice());
-}
diff --git a/bridge/zig/test/integration_test.zig b/bridge/zig/test/integration_test.zig
deleted file mode 100644
index 9a8f36b..0000000
--- a/bridge/zig/test/integration_test.zig
+++ /dev/null
@@ -1,45 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// SPDX-FileCopyrightText: 2026 hyperpolymath
-//
-// Integration tests for Zig FFI bridge
-
-const std = @import("std");
-const main = @import("main");
-
-test "lith_insert stub returns ok" {
-    // Mock database handle (in production, would be created by Lith)
-    var db: main.LithDb = undefined;
-    const db_ptr = @as(*main.LithDb, @ptrCast(&db));
-
-    const collection = "test_collection";
-    const document = "{\"id\": 1, \"value\": 42}";
-    const proof = "{}"; // Empty proof for stub
-
-    const status = main.lith_insert(
-        db_ptr,
-        collection,
-        document.ptr,
-        document.len,
-        proof.ptr,
-        proof.len,
-    );
-
-    try std.testing.expectEqual(@as(c_int, 0), status);
-}
-
-test "lith_register_constraint_checker stub" {
-    var db: main.LithDb = undefined;
-    const db_ptr = @as(*main.LithDb, @ptrCast(&db));
-
-    const checker = struct {
-        fn check(doc: [*]const u8, len: usize) callconv(.C) bool {
-            _ = doc;
-            _ = len;
-            return true;
-        }
-    }.check;
-
-    const status = main.lith_register_constraint_checker(db_ptr, checker);
-
-    try std.testing.expectEqual(@as(c_int, 0), status);
-}
diff --git a/ffi/zig/build.zig b/ffi/zig/build.zig
deleted file mode 100644
index 0961651..0000000
--- a/ffi/zig/build.zig
+++ /dev/null
@@ -1,51 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (@hyperpolymath)
-//
-// build.zig - GQL-DT FFI Build Configuration (Zig 0.15.2+)
-//
-// Builds the libgqldt shared library (C ABI) and unit tests.
-
-const std = @import("std");
-
-pub fn build(b: *std.Build) void {
-    const target = b.standardTargetOptions(.{});
-    const optimize = b.standardOptimizeOption(.{});
-
-    // Static library (libgqldt.a)
-    const static_lib = b.addLibrary(.{
-        .name = "gqldt",
-        .root_module = b.createModule(.{
-            .root_source_file = b.path("src/main.zig"),
-            .target = target,
-            .optimize = optimize,
-        }),
-        .linkage = .static,
-    });
-    b.installArtifact(static_lib);
-
-    // Shared library (libgqldt.so / libgqldt.dylib)
-    const shared_lib = b.addLibrary(.{
-        .name = "gqldt",
-        .root_module = b.createModule(.{
-            .root_source_file = b.path("src/main.zig"),
-            .target = target,
-            .optimize = optimize,
-        }),
-        .linkage = .dynamic,
-    });
-    b.installArtifact(shared_lib);
-
-    // Unit tests (from main.zig internal tests)
-    const unit_tests = b.addTest(.{
-        .name = "gqldt-tests",
-        .root_module = b.createModule(.{
-            .root_source_file = b.path("src/main.zig"),
-            .target = target,
-            .optimize = optimize,
-        }),
-    });
-
-    const run_unit_tests = b.addRunArtifact(unit_tests);
-    const test_step = b.step("test", "Run unit tests");
-    test_step.dependOn(&run_unit_tests.step);
-}
diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig
deleted file mode 100644
index e3ee8af..0000000
--- a/ffi/zig/src/main.zig
+++ /dev/null
@@ -1,861 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (@hyperpolymath)
-//
-// main.zig - Zig FFI implementation for GQL-DT ABI
-//
-// Pure ABI bridge — all safety logic in Idris2.
-// Delegates database operations to the Lith bridge layer (lith_persist/lith_insert).
-// Manages opaque handle lifecycle and query parsing at the FFI boundary.
-
-const std = @import("std");
-const testing = std.testing;
-
-// ---------------------------------------------------------------------------
-// Status codes (matches Idris2 GqldtStatus in GQLdt.ABI.Types)
-// ---------------------------------------------------------------------------
-
-/// Result status codes for GQL-DT FFI operations.
-/// Integer values match the Idris2 statusToInt mapping exactly.
-pub const Status = enum(i32) {
-    ok = 0,
-    invalid_arg = 1,
-    type_mismatch = 2,
-    proof_failed = 3,
-    permission_denied = 4,
-    out_of_memory = 5,
-    internal_error = 6,
-};
-
-// ---------------------------------------------------------------------------
-// Handle backing structures
-// ---------------------------------------------------------------------------
-
-/// Internal database state backing the opaque GqldtDb handle.
-/// Stores the path used to open the database and tracks open state.
-const DbState = struct {
-    path_buf: [4096]u8 = undefined,
-    path_len: usize = 0,
-    opened: bool = false,
-};
-
-/// Internal query state backing the opaque GqldtQuery handle.
-/// Stores the raw query text and whether it has been type-checked.
-const QueryState = struct {
-    text_buf: [1_000_000]u8 = undefined,
-    text_len: usize = 0,
-    type_checked: bool = false,
-    inferred: bool = false,
-};
-
-/// Internal schema state backing the opaque GqldtSchema handle.
-/// Stores the collection name the schema was retrieved for.
-const SchemaState = struct {
-    collection_buf: [256]u8 = undefined,
-    collection_len: usize = 0,
-};
-
-/// Internal result-set state backing the opaque GqldtResult handle.
-/// Stores serialised query output after execution.
-const ResultState = struct {
-    data_buf: [1_000_000]u8 = undefined,
-    data_len: usize = 0,
-};
-
-// ---------------------------------------------------------------------------
-// Opaque handle types (matches Idris2 handle types)
-// ---------------------------------------------------------------------------
-
-pub const GqldtDb = opaque {};
-pub const GqldtQuery = opaque {};
-pub const GqldtSchema = opaque {};
-pub const GqldtType = opaque {};
-pub const GqldtResult = opaque {};
-
-// ---------------------------------------------------------------------------
-// Global library state
-// ---------------------------------------------------------------------------
-
-/// Whether gqldt_init() has been called successfully.
-var initialized: bool = false;
-
-/// General-purpose allocator for handle allocations.
-var gpa = std.heap.GeneralPurposeAllocator(.{}){};
-
-// ---------------------------------------------------------------------------
-// Library Lifecycle
-// ---------------------------------------------------------------------------
-
-/// Initialise the GQL-DT library.
-/// Idempotent — repeated calls return ok without side-effects.
-export fn gqldt_init() callconv(.c) i32 {
-    if (initialized) return @intFromEnum(Status.ok);
-    initialized = true;
-    return @intFromEnum(Status.ok);
-}
-
-/// Tear down the GQL-DT library and release the backing allocator.
-export fn gqldt_cleanup() callconv(.c) void {
-    if (!initialized) return;
-    _ = gpa.deinit();
-    gpa = std.heap.GeneralPurposeAllocator(.{}){};
-    initialized = false;
-}
-
-// ---------------------------------------------------------------------------
-// Database Operations
-// ---------------------------------------------------------------------------
-
-/// Open a database at the given path and write an opaque handle into *db_out.
-///
-/// Path validation is expected to happen on the Idris2 side via Proven.SafePath
-/// before this function is called.  The FFI layer performs basic sanity checks
-/// (non-null, bounded length) and allocates a DbState on the heap.
-export fn gqldt_db_open(
-    path: [*:0]const u8,
-    path_len: u64,
-    db_out: *?*GqldtDb,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-    if (path_len == 0) return @intFromEnum(Status.invalid_arg);
-    if (path_len > 4096) return @intFromEnum(Status.invalid_arg);
-
-    const len: usize = @intCast(path_len);
-
-    // Validate that the path is a reasonable C string.
-    if (!validate_c_string(path, len)) return @intFromEnum(Status.invalid_arg);
-
-    const allocator = gpa.allocator();
-    const state = allocator.create(DbState) catch {
-        return @intFromEnum(Status.out_of_memory);
-    };
-
-    @memcpy(state.path_buf[0..len], path[0..len]);
-    state.path_len = len;
-    state.opened = true;
-
-    // SAFETY: DbState is a heap-allocated struct; casting its pointer to the
-    // opaque GqldtDb handle is the standard pattern for Zig FFI bridges.
-    db_out.* = @ptrCast(state);
-    return @intFromEnum(Status.ok);
-}
-
-/// Close a previously-opened database handle and free its backing memory.
-export fn gqldt_db_close(db: *GqldtDb) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-
-    // SAFETY: The caller must pass a handle originally obtained from
-    // gqldt_db_open.  We cast back to the concrete DbState to free it.
-    const state: *DbState = @ptrCast(@alignCast(db));
-    state.opened = false;
-
-    const allocator = gpa.allocator();
-    allocator.destroy(state);
-    return @intFromEnum(Status.ok);
-}
-
-// ---------------------------------------------------------------------------
-// Query Parsing and Type Checking
-// ---------------------------------------------------------------------------
-
-/// Parse a GQL-DT query string (explicit dependent types).
-///
-/// String validation is expected to happen on the Idris2 side via
-/// Proven.SafeString before this function is called.  The FFI layer stores
-/// the raw query text in a heap-allocated QueryState.
-export fn gqldt_parse(
-    query_str: [*:0]const u8,
-    query_len: u64,
-    query_out: *?*GqldtQuery,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-    if (query_len == 0) return @intFromEnum(Status.invalid_arg);
-    if (query_len > 1_000_000) return @intFromEnum(Status.invalid_arg);
-
-    const len: usize = @intCast(query_len);
-
-    if (!validate_c_string(query_str, len)) return @intFromEnum(Status.invalid_arg);
-
-    const allocator = gpa.allocator();
-    const state = allocator.create(QueryState) catch {
-        return @intFromEnum(Status.out_of_memory);
-    };
-
-    @memcpy(state.text_buf[0..len], query_str[0..len]);
-    state.text_len = len;
-    state.type_checked = false;
-    state.inferred = false;
-
-    // SAFETY: Heap-allocated QueryState cast to opaque handle.
-    query_out.* = @ptrCast(state);
-    return @intFromEnum(Status.ok);
-}
-
-/// Parse a GQL query string with type inference against a schema.
-///
-/// Type inference is delegated to the Idris2 layer; at the FFI level we
-/// record that this query was parsed with inference enabled.
-export fn gqldt_parse_inferred(
-    query_str: [*:0]const u8,
-    query_len: u64,
-    schema: *GqldtSchema,
-    query_out: *?*GqldtQuery,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-    if (query_len == 0) return @intFromEnum(Status.invalid_arg);
-    if (query_len > 1_000_000) return @intFromEnum(Status.invalid_arg);
-
-    const len: usize = @intCast(query_len);
-
-    if (!validate_c_string(query_str, len)) return @intFromEnum(Status.invalid_arg);
-
-    // Validate the schema handle is non-null (opaque pointer check).
-    _ = schema;
-
-    const allocator = gpa.allocator();
-    const state = allocator.create(QueryState) catch {
-        return @intFromEnum(Status.out_of_memory);
-    };
-
-    @memcpy(state.text_buf[0..len], query_str[0..len]);
-    state.text_len = len;
-    state.type_checked = false;
-    state.inferred = true;
-
-    // SAFETY: Heap-allocated QueryState cast to opaque handle.
-    query_out.* = @ptrCast(state);
-    return @intFromEnum(Status.ok);
-}
-
-/// Type-check a parsed query against a schema.
-///
-/// Full dependent-type checking happens in Idris2.  The FFI layer marks the
-/// query as type-checked so that gqldt_execute can verify the precondition.
-export fn gqldt_typecheck(
-    query: *GqldtQuery,
-    schema: *GqldtSchema,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-
-    _ = schema;
-
-    // SAFETY: Caller must pass a handle from gqldt_parse / gqldt_parse_inferred.
-    const state: *QueryState = @ptrCast(@alignCast(query));
-    if (state.text_len == 0) return @intFromEnum(Status.invalid_arg);
-
-    state.type_checked = true;
-    return @intFromEnum(Status.ok);
-}
-
-// ---------------------------------------------------------------------------
-// Query Execution
-// ---------------------------------------------------------------------------
-
-/// Execute a type-checked query against an open database.
-///
-/// Execution with provenance tracking is handled by the Idris2 layer.  The
-/// FFI layer allocates a ResultState to hold the output and verifies that the
-/// query has been type-checked beforehand.
-export fn gqldt_execute(
-    db: *GqldtDb,
-    query: *GqldtQuery,
-    result_out: *?*GqldtResult,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-
-    // SAFETY: Handles must originate from their respective open/parse calls.
-    const db_state: *DbState = @ptrCast(@alignCast(db));
-    const q_state: *QueryState = @ptrCast(@alignCast(query));
-
-    if (!db_state.opened) return @intFromEnum(Status.internal_error);
-    if (q_state.text_len == 0) return @intFromEnum(Status.invalid_arg);
-    if (!q_state.type_checked) return @intFromEnum(Status.type_mismatch);
-
-    const allocator = gpa.allocator();
-    const r_state = allocator.create(ResultState) catch {
-        return @intFromEnum(Status.out_of_memory);
-    };
-
-    // Placeholder result — in production the Idris2 execute function fills
-    // this with CBOR-encoded result rows.
-    r_state.data_len = 0;
-
-    // SAFETY: Heap-allocated ResultState cast to opaque handle.
-    result_out.* = @ptrCast(r_state);
-    return @intFromEnum(Status.ok);
-}
-
-// ---------------------------------------------------------------------------
-// Serialization
-// ---------------------------------------------------------------------------
-
-/// Serialise a parsed query to CBOR (RFC 8949).
-///
-/// Semantic-tag encoding is performed in Idris2 via the CborTag definitions.
-/// The FFI layer writes a minimal CBOR text-string encoding of the raw query
-/// into the caller-provided buffer.
-export fn gqldt_serialize_cbor(
-    query: *GqldtQuery,
-    buffer: [*]u8,
-    buffer_len: u64,
-    written_out: *u64,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-    if (buffer_len == 0) return @intFromEnum(Status.invalid_arg);
-
-    // SAFETY: Handle from gqldt_parse.
-    const state: *QueryState = @ptrCast(@alignCast(query));
-    if (state.text_len == 0) return @intFromEnum(Status.invalid_arg);
-
-    const buf_len: usize = @intCast(buffer_len);
-
-    // Encode as CBOR text string: major type 3 + length prefix + UTF-8 bytes.
-    // This is a minimal encoding; full semantic tagging is handled by Idris2.
-    const header_size = cbor_text_header_size(state.text_len);
-    const total = header_size + state.text_len;
-
-    if (total > buf_len) return @intFromEnum(Status.invalid_arg);
-
-    var pos: usize = 0;
-    write_cbor_text_header(buffer, &pos, state.text_len);
-    @memcpy(buffer[pos .. pos + state.text_len], state.text_buf[0..state.text_len]);
-    pos += state.text_len;
-
-    written_out.* = @intCast(pos);
-    return @intFromEnum(Status.ok);
-}
-
-/// Serialise a parsed query to JSON.
-///
-/// Produces a JSON object wrapping the raw query text.
-export fn gqldt_serialize_json(
-    query: *GqldtQuery,
-    buffer: [*]u8,
-    buffer_len: u64,
-    written_out: *u64,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-    if (buffer_len == 0) return @intFromEnum(Status.invalid_arg);
-
-    // SAFETY: Handle from gqldt_parse.
-    const state: *QueryState = @ptrCast(@alignCast(query));
-    if (state.text_len == 0) return @intFromEnum(Status.invalid_arg);
-
-    const buf_len: usize = @intCast(buffer_len);
-
-    // Produce: {"query":"<text>"}
-    const prefix = "{\"query\":\"";
-    const suffix = "\"}";
-    const total = prefix.len + state.text_len + suffix.len;
-
-    if (total > buf_len) return @intFromEnum(Status.invalid_arg);
-
-    var pos: usize = 0;
-    @memcpy(buffer[pos .. pos + prefix.len], prefix);
-    pos += prefix.len;
-    @memcpy(buffer[pos .. pos + state.text_len], state.text_buf[0..state.text_len]);
-    pos += state.text_len;
-    @memcpy(buffer[pos .. pos + suffix.len], suffix);
-    pos += suffix.len;
-
-    written_out.* = @intCast(pos);
-    return @intFromEnum(Status.ok);
-}
-
-/// Deserialise a query from CBOR.
-///
-/// Expects a CBOR text-string encoding (major type 3).  Full semantic-tag
-/// validation is handled in Idris2.
-export fn gqldt_deserialize_cbor(
-    buffer: [*]const u8,
-    buffer_len: u64,
-    query_out: *?*GqldtQuery,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-    if (buffer_len == 0) return @intFromEnum(Status.invalid_arg);
-    if (buffer_len > 10_000_000) return @intFromEnum(Status.invalid_arg);
-
-    const buf_len: usize = @intCast(buffer_len);
-
-    // Decode CBOR text string header (major type 3).
-    var pos: usize = 0;
-    const text_len = read_cbor_text_header(buffer, buf_len, &pos) orelse {
-        return @intFromEnum(Status.invalid_arg);
-    };
-
-    if (pos + text_len > buf_len) return @intFromEnum(Status.invalid_arg);
-    if (text_len == 0) return @intFromEnum(Status.invalid_arg);
-    if (text_len > 1_000_000) return @intFromEnum(Status.invalid_arg);
-
-    const allocator = gpa.allocator();
-    const state = allocator.create(QueryState) catch {
-        return @intFromEnum(Status.out_of_memory);
-    };
-
-    @memcpy(state.text_buf[0..text_len], buffer[pos .. pos + text_len]);
-    state.text_len = text_len;
-    state.type_checked = false;
-    state.inferred = false;
-
-    // SAFETY: Heap-allocated QueryState cast to opaque handle.
-    query_out.* = @ptrCast(state);
-    return @intFromEnum(Status.ok);
-}
-
-// ---------------------------------------------------------------------------
-// Schema Operations
-// ---------------------------------------------------------------------------
-
-/// Retrieve the schema for a named collection from an open database.
-///
-/// Schema extraction and validation are performed in Idris2.  The FFI layer
-/// allocates a SchemaState that records the collection name.
-export fn gqldt_get_schema(
-    db: *GqldtDb,
-    collection_name: [*:0]const u8,
-    schema_out: *?*GqldtSchema,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-
-    // SAFETY: Handle from gqldt_db_open.
-    const db_state: *DbState = @ptrCast(@alignCast(db));
-    if (!db_state.opened) return @intFromEnum(Status.internal_error);
-
-    // Measure collection name length (null-terminated).
-    var name_len: usize = 0;
-    while (collection_name[name_len] != 0) : (name_len += 1) {
-        if (name_len >= 256) return @intFromEnum(Status.invalid_arg);
-    }
-    if (name_len == 0) return @intFromEnum(Status.invalid_arg);
-
-    const allocator = gpa.allocator();
-    const state = allocator.create(SchemaState) catch {
-        return @intFromEnum(Status.out_of_memory);
-    };
-
-    @memcpy(state.collection_buf[0..name_len], collection_name[0..name_len]);
-    state.collection_len = name_len;
-
-    // SAFETY: Heap-allocated SchemaState cast to opaque handle.
-    schema_out.* = @ptrCast(state);
-    return @intFromEnum(Status.ok);
-}
-
-// ---------------------------------------------------------------------------
-// Permission Validation
-// ---------------------------------------------------------------------------
-
-/// Validate query permissions using the two-tier TypeWhitelist system.
-///
-/// Permission checking with TypeWhitelist is performed in Idris2.  The FFI
-/// layer delegates the decision and returns the result.  Currently returns
-/// ok for all queries — real enforcement is in the Idris2 layer.
-export fn gqldt_validate_permissions(
-    query: *GqldtQuery,
-    user_id: [*:0]const u8,
-    permissions: *const anyopaque,
-) callconv(.c) i32 {
-    if (!initialized) return @intFromEnum(Status.internal_error);
-
-    // SAFETY: Handle from gqldt_parse.
-    const q_state: *QueryState = @ptrCast(@alignCast(query));
-    if (q_state.text_len == 0) return @intFromEnum(Status.invalid_arg);
-
-    // Validate user_id is non-empty.
-    if (user_id[0] == 0) return @intFromEnum(Status.invalid_arg);
-
-    // Permissions opaque pointer must be non-null (checked by C ABI contract).
-    _ = permissions;
-
-    // Permission enforcement happens in Idris2 — FFI layer grants by default.
-    return @intFromEnum(Status.ok);
-}
-
-// ---------------------------------------------------------------------------
-// Resource Cleanup
-// ---------------------------------------------------------------------------
-
-/// Free a query handle previously returned by gqldt_parse,
-/// gqldt_parse_inferred, or gqldt_deserialize_cbor.
-export fn gqldt_query_free(query: *GqldtQuery) callconv(.c) void {
-    if (!initialized) return;
-
-    // SAFETY: Handle from gqldt_parse / gqldt_parse_inferred / gqldt_deserialize_cbor.
-    const state: *QueryState = @ptrCast(@alignCast(query));
-    const allocator = gpa.allocator();
-    allocator.destroy(state);
-}
-
-/// Free a schema handle previously returned by gqldt_get_schema.
-export fn gqldt_schema_free(schema: *GqldtSchema) callconv(.c) void {
-    if (!initialized) return;
-
-    // SAFETY: Handle from gqldt_get_schema.
-    const state: *SchemaState = @ptrCast(@alignCast(schema));
-    const allocator = gpa.allocator();
-    allocator.destroy(state);
-}
-
-/// Free a result handle previously returned by gqldt_execute.
-export fn gqldt_result_free(result: *GqldtResult) callconv(.c) void {
-    if (!initialized) return;
-
-    // SAFETY: Handle from gqldt_execute.
-    const state: *ResultState = @ptrCast(@alignCast(result));
-    const allocator = gpa.allocator();
-    allocator.destroy(state);
-}
-
-// ---------------------------------------------------------------------------
-// Version Information
-// ---------------------------------------------------------------------------
-
-/// Return the GQL-DT FFI library version as a null-terminated C string.
-export fn gqldt_version() callconv(.c) [*:0]const u8 {
-    return "0.1.0";
-}
-
-// ---------------------------------------------------------------------------
-// Slot Allocation Helpers (for Idris2 prim__allocSlot / prim__readSlot)
-// ---------------------------------------------------------------------------
-
-/// Allocate a pointer-sized output slot on the heap.
-/// Used by Idris2 to receive opaque handle pointers from FFI calls.
-export fn gqldt_alloc_slot() callconv(.c) ?*anyopaque {
-    const allocator = gpa.allocator();
-    const slot = allocator.create(usize) catch return null;
-    slot.* = 0;
-    // SAFETY: usize* cast to opaque — Idris2 treats it as AnyPtr.
-    return @ptrCast(slot);
-}
-
-/// Read a pointer value from an output slot as u64 (Bits64 in Idris2).
-export fn gqldt_read_slot(slot: *anyopaque) callconv(.c) u64 {
-    // SAFETY: Slot must have been allocated by gqldt_alloc_slot.
-    const typed: *usize = @ptrCast(@alignCast(slot));
-    return @intCast(typed.*);
-}
-
-/// Free an output slot allocated by gqldt_alloc_slot.
-export fn gqldt_free_slot(slot: *anyopaque) callconv(.c) void {
-    // SAFETY: Slot must have been allocated by gqldt_alloc_slot.
-    const typed: *usize = @ptrCast(@alignCast(slot));
-    const allocator = gpa.allocator();
-    allocator.destroy(typed);
-}
-
-/// Cast a Bits64 value to an opaque pointer.
-/// Used by Idris2 to convert handle values back to pointers for FFI calls.
-export fn gqldt_bits64_to_ptr(value: u64) callconv(.c) ?*anyopaque {
-    if (value == 0) return null;
-    // SAFETY: The caller guarantees that value was originally obtained from
-    // a valid pointer via gqldt_read_slot.
-    return @ptrFromInt(@as(usize, @intCast(value)));
-}
-
-// ---------------------------------------------------------------------------
-// Helper Functions (ABI Bridge Only)
-// ---------------------------------------------------------------------------
-
-/// Validate a null-terminated C string has non-zero length and fits within
-/// max_len bytes.
-///
-/// NOTE: Full validation happens in Idris2 via Proven.SafeString.
-fn validate_c_string(ptr: [*:0]const u8, max_len: usize) bool {
-    var len: usize = 0;
-    while (ptr[len] != 0) : (len += 1) {
-        if (len >= max_len) return false;
-    }
-    return len > 0;
-}
-
-/// Compute the number of header bytes needed for a CBOR text string of the
-/// given length (major type 3).
-fn cbor_text_header_size(text_len: usize) usize {
-    if (text_len < 24) return 1;
-    if (text_len <= 0xFF) return 2;
-    if (text_len <= 0xFFFF) return 3;
-    if (text_len <= 0xFFFFFFFF) return 5;
-    return 9;
-}
-
-/// Write a CBOR text string header (major type 3) into buffer at *pos.
-fn write_cbor_text_header(buffer: [*]u8, pos: *usize, text_len: usize) void {
-    const major: u8 = 3 << 5; // major type 3
-    if (text_len < 24) {
-        buffer[pos.*] = major | @as(u8, @truncate(text_len));
-        pos.* += 1;
-    } else if (text_len <= 0xFF) {
-        buffer[pos.*] = major | 24;
-        pos.* += 1;
-        buffer[pos.*] = @truncate(text_len);
-        pos.* += 1;
-    } else if (text_len <= 0xFFFF) {
-        buffer[pos.*] = major | 25;
-        pos.* += 1;
-        const be = std.mem.nativeToBig(u16, @truncate(text_len));
-        const bytes = std.mem.toBytes(be);
-        @memcpy(buffer[pos.* .. pos.* + 2], &bytes);
-        pos.* += 2;
-    } else if (text_len <= 0xFFFFFFFF) {
-        buffer[pos.*] = major | 26;
-        pos.* += 1;
-        const be = std.mem.nativeToBig(u32, @truncate(text_len));
-        const bytes = std.mem.toBytes(be);
-        @memcpy(buffer[pos.* .. pos.* + 4], &bytes);
-        pos.* += 4;
-    } else {
-        buffer[pos.*] = major | 27;
-        pos.* += 1;
-        const be = std.mem.nativeToBig(u64, @as(u64, text_len));
-        const bytes = std.mem.toBytes(be);
-        @memcpy(buffer[pos.* .. pos.* + 8], &bytes);
-        pos.* += 8;
-    }
-}
-
-/// Read a CBOR text string header (major type 3) from buffer, advancing *pos.
-/// Returns null if the header is invalid or not a text string.
-fn read_cbor_text_header(buffer: [*]const u8, buf_len: usize, pos: *usize) ?usize {
-    if (pos.* >= buf_len) return null;
-
-    const initial = buffer[pos.*];
-    const major = initial >> 5;
-    if (major != 3) return null; // Not a text string.
-
-    const additional = initial & 0x1F;
-    pos.* += 1;
-
-    if (additional < 24) {
-        return @as(usize, additional);
-    } else if (additional == 24) {
-        if (pos.* >= buf_len) return null;
-        const len: usize = buffer[pos.*];
-        pos.* += 1;
-        return len;
-    } else if (additional == 25) {
-        if (pos.* + 2 > buf_len) return null;
-        var bytes: [2]u8 = undefined;
-        @memcpy(&bytes, buffer[pos.* .. pos.* + 2]);
-        pos.* += 2;
-        return @as(usize, std.mem.bigToNative(u16, @bitCast(bytes)));
-    } else if (additional == 26) {
-        if (pos.* + 4 > buf_len) return null;
-        var bytes: [4]u8 = undefined;
-        @memcpy(&bytes, buffer[pos.* .. pos.* + 4]);
-        pos.* += 4;
-        return @as(usize, std.mem.bigToNative(u32, @bitCast(bytes)));
-    } else if (additional == 27) {
-        if (pos.* + 8 > buf_len) return null;
-        var bytes: [8]u8 = undefined;
-        @memcpy(&bytes, buffer[pos.* .. pos.* + 8]);
-        pos.* += 8;
-        return @as(usize, std.mem.bigToNative(u64, @bitCast(bytes)));
-    }
-
-    return null;
-}
-
-// ---------------------------------------------------------------------------
-// Tests
-// ---------------------------------------------------------------------------
-
-test "status codes match Idris2 ABI" {
-    try testing.expectEqual(@as(i32, 0), @intFromEnum(Status.ok));
-    try testing.expectEqual(@as(i32, 1), @intFromEnum(Status.invalid_arg));
-    try testing.expectEqual(@as(i32, 2), @intFromEnum(Status.type_mismatch));
-    try testing.expectEqual(@as(i32, 3), @intFromEnum(Status.proof_failed));
-    try testing.expectEqual(@as(i32, 4), @intFromEnum(Status.permission_denied));
-    try testing.expectEqual(@as(i32, 5), @intFromEnum(Status.out_of_memory));
-    try testing.expectEqual(@as(i32, 6), @intFromEnum(Status.internal_error));
-}
-
-test "library initialization" {
-    const status = gqldt_init();
-    try testing.expectEqual(@intFromEnum(Status.ok), status);
-    gqldt_cleanup();
-}
-
-test "library double-init is idempotent" {
-    _ = gqldt_init();
-    const status = gqldt_init();
-    try testing.expectEqual(@intFromEnum(Status.ok), status);
-    gqldt_cleanup();
-}
-
-test "validate_c_string rejects empty strings" {
-    const empty_str: [*:0]const u8 = "";
-    try testing.expect(!validate_c_string(empty_str, 100));
-}
-
-test "validate_c_string accepts valid strings" {
-    const valid_str: [*:0]const u8 = "SELECT * FROM users";
-    try testing.expect(validate_c_string(valid_str, 1000));
-}
-
-test "validate_c_string rejects oversized strings" {
-    var buf: [200]u8 = undefined;
-    @memset(&buf, 'A');
-    buf[199] = 0;
-    const long_str: [*:0]const u8 = @ptrCast(&buf);
-    try testing.expect(!validate_c_string(long_str, 100));
-}
-
-test "db_open and db_close round-trip" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*GqldtDb = null;
-    const open_status = gqldt_db_open("test.db", 7, &db);
-    try testing.expectEqual(@intFromEnum(Status.ok), open_status);
-    try testing.expect(db != null);
-
-    const close_status = gqldt_db_close(db.?);
-    try testing.expectEqual(@intFromEnum(Status.ok), close_status);
-}
-
-test "db_open rejects empty path" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*GqldtDb = null;
-    const status = gqldt_db_open("", 0, &db);
-    try testing.expectEqual(@intFromEnum(Status.invalid_arg), status);
-}
-
-test "parse and query_free round-trip" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var query: ?*GqldtQuery = null;
-    const query_text: [*:0]const u8 = "MATCH (n:Person) RETURN n";
-    const status = gqldt_parse(query_text, 25, &query);
-    try testing.expectEqual(@intFromEnum(Status.ok), status);
-    try testing.expect(query != null);
-
-    gqldt_query_free(query.?);
-}
-
-test "parse rejects empty query" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var query: ?*GqldtQuery = null;
-    const status = gqldt_parse("", 0, &query);
-    try testing.expectEqual(@intFromEnum(Status.invalid_arg), status);
-}
-
-test "typecheck marks query as checked" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    // Create a schema handle.
-    var db: ?*GqldtDb = null;
-    _ = gqldt_db_open("test.db", 7, &db);
-    defer _ = gqldt_db_close(db.?);
-
-    var schema: ?*GqldtSchema = null;
-    _ = gqldt_get_schema(db.?, "users", &schema);
-    defer gqldt_schema_free(schema.?);
-
-    // Parse a query.
-    var query: ?*GqldtQuery = null;
-    _ = gqldt_parse("MATCH (n) RETURN n", 18, &query);
-    defer gqldt_query_free(query.?);
-
-    // Type-check.
-    const tc_status = gqldt_typecheck(query.?, schema.?);
-    try testing.expectEqual(@intFromEnum(Status.ok), tc_status);
-}
-
-test "execute requires type-checked query" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*GqldtDb = null;
-    _ = gqldt_db_open("test.db", 7, &db);
-    defer _ = gqldt_db_close(db.?);
-
-    var query: ?*GqldtQuery = null;
-    _ = gqldt_parse("MATCH (n) RETURN n", 18, &query);
-    defer gqldt_query_free(query.?);
-
-    // Attempt execution without type-checking — should fail.
-    var result: ?*GqldtResult = null;
-    const status = gqldt_execute(db.?, query.?, &result);
-    try testing.expectEqual(@intFromEnum(Status.type_mismatch), status);
-}
-
-test "execute succeeds after typecheck" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*GqldtDb = null;
-    _ = gqldt_db_open("test.db", 7, &db);
-    defer _ = gqldt_db_close(db.?);
-
-    var schema: ?*GqldtSchema = null;
-    _ = gqldt_get_schema(db.?, "users", &schema);
-    defer gqldt_schema_free(schema.?);
-
-    var query: ?*GqldtQuery = null;
-    _ = gqldt_parse("MATCH (n) RETURN n", 18, &query);
-    defer gqldt_query_free(query.?);
-
-    _ = gqldt_typecheck(query.?, schema.?);
-
-    var result: ?*GqldtResult = null;
-    const exec_status = gqldt_execute(db.?, query.?, &result);
-    try testing.expectEqual(@intFromEnum(Status.ok), exec_status);
-    try testing.expect(result != null);
-
-    gqldt_result_free(result.?);
-}
-
-test "serialize_cbor and deserialize_cbor round-trip" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    const query_text: [*:0]const u8 = "MATCH (n) RETURN n";
-    var query: ?*GqldtQuery = null;
-    _ = gqldt_parse(query_text, 18, &query);
-    defer gqldt_query_free(query.?);
-
-    // Serialise to CBOR.
-    var cbor_buf: [1024]u8 = undefined;
-    var written: u64 = 0;
-    const ser_status = gqldt_serialize_cbor(query.?, &cbor_buf, 1024, &written);
-    try testing.expectEqual(@intFromEnum(Status.ok), ser_status);
-    try testing.expect(written > 0);
-
-    // Deserialise from CBOR.
-    var query2: ?*GqldtQuery = null;
-    const deser_status = gqldt_deserialize_cbor(&cbor_buf, written, &query2);
-    try testing.expectEqual(@intFromEnum(Status.ok), deser_status);
-    try testing.expect(query2 != null);
-
-    gqldt_query_free(query2.?);
-}
-
-test "serialize_json produces valid wrapper" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var query: ?*GqldtQuery = null;
-    _ = gqldt_parse("RETURN 1", 8, &query);
-    defer gqldt_query_free(query.?);
-
-    var json_buf: [1024]u8 = undefined;
-    var written: u64 = 0;
-    const status = gqldt_serialize_json(query.?, &json_buf, 1024, &written);
-    try testing.expectEqual(@intFromEnum(Status.ok), status);
-
-    const json_str = json_buf[0..@intCast(written)];
-    try testing.expectEqualStrings("{\"query\":\"RETURN 1\"}", json_str);
-}
-
-test "version returns semantic version" {
-    const ver = gqldt_version();
-    const ver_str = std.mem.span(ver);
-    try testing.expect(ver_str.len > 0);
-    try testing.expect(std.mem.count(u8, ver_str, ".") >= 1);
-}
diff --git a/ffi/zig/test/integration_test.zig b/ffi/zig/test/integration_test.zig
deleted file mode 100644
index 8fc1d46..0000000
--- a/ffi/zig/test/integration_test.zig
+++ /dev/null
@@ -1,233 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (@hyperpolymath)
-//
-// GQL-DT Integration Tests
-//
-// These tests verify that the Zig FFI correctly implements the Idris2 ABI.
-// They exercise the exported C-ABI functions end-to-end.
-
-const std = @import("std");
-const testing = std.testing;
-
-// Import FFI functions
-extern fn gqldt_init() callconv(.c) i32;
-extern fn gqldt_cleanup() callconv(.c) void;
-extern fn gqldt_db_open(path: [*:0]const u8, path_len: u64, db_out: *?*anyopaque) callconv(.c) i32;
-extern fn gqldt_db_close(db: *anyopaque) callconv(.c) i32;
-extern fn gqldt_parse(query_str: [*:0]const u8, query_len: u64, query_out: *?*anyopaque) callconv(.c) i32;
-extern fn gqldt_parse_inferred(query_str: [*:0]const u8, query_len: u64, schema: *anyopaque, query_out: *?*anyopaque) callconv(.c) i32;
-extern fn gqldt_typecheck(query: *anyopaque, schema: *anyopaque) callconv(.c) i32;
-extern fn gqldt_execute(db: *anyopaque, query: *anyopaque, result_out: *?*anyopaque) callconv(.c) i32;
-extern fn gqldt_get_schema(db: *anyopaque, collection_name: [*:0]const u8, schema_out: *?*anyopaque) callconv(.c) i32;
-extern fn gqldt_query_free(query: *anyopaque) callconv(.c) void;
-extern fn gqldt_schema_free(schema: *anyopaque) callconv(.c) void;
-extern fn gqldt_result_free(result: *anyopaque) callconv(.c) void;
-extern fn gqldt_serialize_cbor(query: *anyopaque, buffer: [*]u8, buffer_len: u64, written_out: *u64) callconv(.c) i32;
-extern fn gqldt_serialize_json(query: *anyopaque, buffer: [*]u8, buffer_len: u64, written_out: *u64) callconv(.c) i32;
-extern fn gqldt_deserialize_cbor(buffer: [*]const u8, buffer_len: u64, query_out: *?*anyopaque) callconv(.c) i32;
-extern fn gqldt_validate_permissions(query: *anyopaque, user_id: [*:0]const u8, permissions: *const anyopaque) callconv(.c) i32;
-extern fn gqldt_version() callconv(.c) [*:0]const u8;
-extern fn gqldt_alloc_slot() callconv(.c) ?*anyopaque;
-extern fn gqldt_read_slot(slot: *anyopaque) callconv(.c) u64;
-extern fn gqldt_free_slot(slot: *anyopaque) callconv(.c) void;
-extern fn gqldt_bits64_to_ptr(value: u64) callconv(.c) ?*anyopaque;
-
-//==============================================================================
-// Lifecycle Tests
-//==============================================================================
-
-test "init and cleanup" {
-    const status = gqldt_init();
-    try testing.expectEqual(@as(i32, 0), status);
-    gqldt_cleanup();
-}
-
-test "double init is idempotent" {
-    _ = gqldt_init();
-    const status = gqldt_init();
-    try testing.expectEqual(@as(i32, 0), status);
-    gqldt_cleanup();
-}
-
-//==============================================================================
-// Database Operations
-//==============================================================================
-
-test "db_open and db_close" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*anyopaque = null;
-    const open_status = gqldt_db_open("test.db", 7, &db);
-    try testing.expectEqual(@as(i32, 0), open_status);
-    try testing.expect(db != null);
-
-    const close_status = gqldt_db_close(db.?);
-    try testing.expectEqual(@as(i32, 0), close_status);
-}
-
-test "db_open rejects empty path" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*anyopaque = null;
-    const status = gqldt_db_open("", 0, &db);
-    try testing.expectEqual(@as(i32, 1), status); // invalid_arg
-}
-
-test "db_open rejects oversized path" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*anyopaque = null;
-    const status = gqldt_db_open("x", 5000, &db);
-    try testing.expectEqual(@as(i32, 1), status); // invalid_arg
-}
-
-//==============================================================================
-// Query Parsing
-//==============================================================================
-
-test "parse valid query" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var query: ?*anyopaque = null;
-    const status = gqldt_parse("MATCH (n:Person) RETURN n", 25, &query);
-    try testing.expectEqual(@as(i32, 0), status);
-    try testing.expect(query != null);
-
-    gqldt_query_free(query.?);
-}
-
-test "parse rejects empty query" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var query: ?*anyopaque = null;
-    const status = gqldt_parse("", 0, &query);
-    try testing.expectEqual(@as(i32, 1), status); // invalid_arg
-}
-
-//==============================================================================
-// Type Checking and Execution
-//==============================================================================
-
-test "full pipeline: open -> schema -> parse -> typecheck -> execute" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    // Open database.
-    var db: ?*anyopaque = null;
-    _ = gqldt_db_open("pipeline.db", 11, &db);
-    defer gqldt_db_close(db.?);
-
-    // Get schema.
-    var schema: ?*anyopaque = null;
-    _ = gqldt_get_schema(db.?, "nodes", &schema);
-    defer gqldt_schema_free(schema.?);
-
-    // Parse query.
-    var query: ?*anyopaque = null;
-    _ = gqldt_parse("MATCH (n) RETURN n", 18, &query);
-    defer gqldt_query_free(query.?);
-
-    // Type-check.
-    const tc_status = gqldt_typecheck(query.?, schema.?);
-    try testing.expectEqual(@as(i32, 0), tc_status);
-
-    // Execute.
-    var result: ?*anyopaque = null;
-    const exec_status = gqldt_execute(db.?, query.?, &result);
-    try testing.expectEqual(@as(i32, 0), exec_status);
-    try testing.expect(result != null);
-
-    gqldt_result_free(result.?);
-}
-
-test "execute without typecheck fails" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var db: ?*anyopaque = null;
-    _ = gqldt_db_open("test.db", 7, &db);
-    defer gqldt_db_close(db.?);
-
-    var query: ?*anyopaque = null;
-    _ = gqldt_parse("MATCH (n) RETURN n", 18, &query);
-    defer gqldt_query_free(query.?);
-
-    var result: ?*anyopaque = null;
-    const status = gqldt_execute(db.?, query.?, &result);
-    try testing.expectEqual(@as(i32, 2), status); // type_mismatch
-}
-
-//==============================================================================
-// Serialization
-//==============================================================================
-
-test "serialize to CBOR and back" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var query: ?*anyopaque = null;
-    _ = gqldt_parse("RETURN 42", 9, &query);
-    defer gqldt_query_free(query.?);
-
-    var cbor_buf: [1024]u8 = undefined;
-    var written: u64 = 0;
-    const ser_status = gqldt_serialize_cbor(query.?, &cbor_buf, 1024, &written);
-    try testing.expectEqual(@as(i32, 0), ser_status);
-    try testing.expect(written > 0);
-
-    var query2: ?*anyopaque = null;
-    const deser_status = gqldt_deserialize_cbor(&cbor_buf, written, &query2);
-    try testing.expectEqual(@as(i32, 0), deser_status);
-    try testing.expect(query2 != null);
-
-    gqldt_query_free(query2.?);
-}
-
-test "serialize to JSON" {
-    _ = gqldt_init();
-    defer gqldt_cleanup();
-
-    var query: ?*anyopaque = null;
-    _ = gqldt_parse("RETURN 1", 8, &query);
-    defer gqldt_query_free(query.?);
-
-    var json_buf: [1024]u8 = undefined;
-    var written: u64 = 0;
-    const status = gqldt_serialize_json(query.?, &json_buf, 1024, &written);
-    try testing.expectEqual(@as(i32, 0), status);
-
-    const json_str = json_buf[0..@intCast(written)];
-    try testing.expectEqualStrings("{\"query\":\"RETURN 1\"}", json_str);
-}
-
-//==============================================================================
-// Slot Allocation Helpers
-//==============================================================================
-
-test "alloc_slot and free_slot" {
-    const slot = gqldt_alloc_slot() orelse return error.SlotAllocFailed;
-    const value = gqldt_read_slot(slot);
-    try testing.expectEqual(@as(u64, 0), value); // initially zero
-    gqldt_free_slot(slot);
-}
-
-test "bits64_to_ptr null returns null" {
-    const ptr = gqldt_bits64_to_ptr(0);
-    try testing.expect(ptr == null);
-}
-
-//==============================================================================
-// Version
-//==============================================================================
-
-test "version string is semantic version" {
-    const ver = gqldt_version();
-    const ver_str = std.mem.span(ver);
-    try testing.expect(ver_str.len > 0);
-    try testing.expect(std.mem.count(u8, ver_str, ".") >= 1);
-}
diff --git a/mise.toml b/mise.toml
index e02f506..01ef2cb 100644
--- a/mise.toml
+++ b/mise.toml
@@ -18,8 +18,8 @@
 # Zig — builds the FFI bridge in bridge/ that Lean links against
 # (`lakefile.lean`: -Lbridge/zig-out/lib -llith_bridge).
 # 0.16.0 verified: `bridge/` builds clean and `zig build test` passes.
-# NB the stale skeletons in bridge/zig/ and ffi/zig/ use the pre-0.15 Build API
-# and do NOT compile under this version — see issue notes in the PR.
+# `bridge/` is the only Zig tree; the pre-0.15-API skeletons that used to sit in
+# bridge/zig/ and ffi/zig/ were removed (they could not compile under 0.16).
 zig = "0.16.0"
 
 # Idris2 — the ABI layer, src/GQLdt/ABI/{Types,Layout,Foreign}.idr,
diff --git a/selur-compose.yml b/selur-compose.yml
index f8cf987..50d704c 100644
--- a/selur-compose.yml
+++ b/selur-compose.yml
@@ -15,7 +15,7 @@ services:
     volumes:
       - .:/workspace
       - lean-cache:/root/.elan
-      - zig-cache:/workspace/bridge/zig/.zig-cache
+      - zig-cache:/workspace/bridge/.zig-cache
     working_dir: /workspace
     stdin_open: true
     tty: true