P3: prove octad-model invariants as real bijections + sidecar isolation

.github/workflows/abi-ffi-gate.yml

@@ -0,0 +1,38 @@
+# SPDX-License-Identifier: MPL-2.0
+# abi-ffi-gate.yml — enforce that the Zig FFI conforms to the Idris2 ABI.
+#
+# The Idris2 ABI (src/interface/abi) is the source of truth. This gate fails if
+# the Zig FFI (src/interface/ffi) drifts from it: a declared C function with no
+# export, a mismatched result-code map, or an unrendered template token. A
+# second job builds + tests the Zig FFI under the pinned Zig 0.14.0.
+name: ABI-FFI Gate
+
+on:
+  pull_request:
+  push:
+    branches: [main, master]
+
+permissions:
+  contents: read
+
+jobs:
+  conformance:
+    name: ABI ↔ FFI structural conformance
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Run ABI-FFI gate
+        run: python3 scripts/abi-ffi-gate.py
+
+  zig-build:
+    name: Zig FFI builds + tests (Zig 0.14.0)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install Zig 0.14.0
+        run: |
+          curl -fsSL https://ziglang.org/download/0.14.0/zig-linux-x86_64-0.14.0.tar.xz -o /tmp/zig.tar.xz
+          tar -xf /tmp/zig.tar.xz -C /tmp
+          echo "/tmp/zig-linux-x86_64-0.14.0" >> "$GITHUB_PATH"
+      - name: zig test FFI
+        run: zig test src/interface/ffi/src/main.zig -lc

scripts/abi-ffi-gate.py

@@ -0,0 +1,103 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# abi-ffi-gate.py — fail (exit 1) if the Zig FFI does not conform to the Idris2
+# ABI. The Idris2 ABI is the source of truth. Checks, with no toolchain needed:
+#
+#   1. the Zig FFI carries no unrendered `{{...}}` template tokens;
+#   2. every `%foreign "C:<name>"` symbol declared anywhere in the ABI .idr
+#      sources is exported by the Zig FFI (`export fn <name>`);
+#   3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH
+#      names and integer values (the `Error`/`err` spelling is treated as one).
+#
+# Usage: python3 scripts/abi-ffi-gate.py [repo_root]   (defaults to cwd)
+
+import os
+import re
+import sys
+import glob
+
+
+def camel_to_snake(s):
+    return re.sub(r"(?<!^)(?=[A-Z])", "_", s).lower()
+
+
+def canon_rc(name):
+    n = name.lower()
+    return "error" if n in ("err", "error") else n
+
+
+def find_result_enum(zig):
+    """Return {variant: value} for the C-ABI Result enum, or {}."""
+    best = {}
+    for m in re.finditer(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}", zig, re.S):
+        body = m.group(1)
+        variants = {}
+        for vm in re.finditer(r'@?"?([A-Za-z_][A-Za-z0-9_]*)"?\s*=\s*(\d+)', body):
+            variants[canon_rc(vm.group(1))] = int(vm.group(2))
+        # The Result enum is the one starting at ok = 0.
+        if variants.get("ok") == 0 and len(variants) > len(best):
+            best = variants
+    return best
+
+
+def main():
+    root = sys.argv[1] if len(sys.argv) > 1 else "."
+    name = os.path.basename(os.path.abspath(root))
+    abi_dir = os.path.join(root, "src/interface/abi")
+    zig_path = os.path.join(root, "src/interface/ffi/src/main.zig")
+    errs = []
+
+    idr_files = [
+        p for p in glob.glob(os.path.join(abi_dir, "**", "*.idr"), recursive=True)
+        if os.sep + "build" + os.sep not in p
+    ]
+    if not idr_files:
+        print(f"ABI-FFI GATE: SKIP ({name}) — no Idris2 ABI .idr files under {abi_dir}")
+        return 0
+    if not os.path.exists(zig_path):
+        print(f"ABI-FFI GATE: FAIL ({name}) — no Zig FFI at {zig_path}")
+        return 1
+
+    idr = "\n".join(open(p, encoding="utf-8").read() for p in idr_files)
+    zig = open(zig_path, encoding="utf-8").read()
+
+    # 1. unrendered template tokens
+    toks = sorted(set(re.findall(r"\{\{[A-Za-z0-9_]+\}\}", zig)))
+    if toks:
+        errs.append(f"Zig FFI has unrendered template tokens: {toks}")
+
+    # 2. foreign C symbols must be exported
+    csyms = sorted(set(re.findall(r"C:([A-Za-z0-9_]+)", idr)))
+    exports = set(re.findall(r"export fn ([A-Za-z0-9_]+)", zig))
+    missing = [s for s in csyms if s not in exports]
+    if missing:
+        errs.append(f"{len(missing)} ABI function(s) not exported by the Zig FFI: {missing}")
+
+    # 3. result-code map (names + values) must agree
+    idr_rc = {}
+    for m in re.finditer(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr):
+        idr_rc[canon_rc(camel_to_snake(m.group(1)))] = int(m.group(2))
+    zig_rc = find_result_enum(zig)
+    if idr_rc and not zig_rc:
+        errs.append("no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes")
+    elif idr_rc and zig_rc and idr_rc != zig_rc:
+        errs.append(
+            "Result-code map differs (name or value):\n"
+            f"      Idris resultToInt: {dict(sorted(idr_rc.items()))}\n"
+            f"      Zig   Result enum: {dict(sorted(zig_rc.items()))}"
+        )
+
+    if errs:
+        print(f"ABI-FFI GATE: FAIL ({name})")
+        for e in errs:
+            print("  - " + e)
+        return 1
+    print(f"ABI-FFI GATE: OK ({name}) — {len(csyms)} ABI functions exported, "
+          f"{len(idr_rc)} result codes match")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

src/interface/abi/Verisimiser/ABI/Octad.idr

@@ -0,0 +1,195 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Semantic octad-model invariants for VeriSimiser.
+|||
+||| `Proofs.idr` checks the octad only shallowly (`length allDimensions = 8`,
+||| a couple of tag values). This module proves the *defining* invariants of the
+||| VeriSimDB octad model as genuine theorems:
+|||
+|||   1. Octad ≅ Fin 8 — the eight dimensions are exactly eight, all distinct and
+|||      with no gaps: a full bijection (both round-trips), not just a count.
+|||   2. DriftCategory ≅ OctadDimension — the asserted "drift categories biject
+|||      onto octad dimensions" proven as a real bijection.
+|||   3. Sidecar isolation — the per-dimension write model agrees with the tier
+|||      classification: every Tier-1 (piggyback) dimension provably never writes
+|||      to the target database, and every Tier-2 (overlay) dimension does.
+
+module Verisimiser.ABI.Octad
+
+import Verisimiser.ABI.Types
+import Data.Fin
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- 1. Octad ≅ Fin 8  (exactly eight distinct dimensions, no gaps)
+--------------------------------------------------------------------------------
+
+||| Ordinal position of each octad dimension (matches `octadToInt`).
+public export
+octadToFin : OctadDimension -> Fin 8
+octadToFin Data          = 0
+octadToFin Metadata      = 1
+octadToFin Provenance    = 2
+octadToFin Lineage       = 3
+octadToFin Constraints   = 4
+octadToFin AccessControl = 5
+octadToFin Temporal      = 6
+octadToFin Simulation    = 7
+
+||| Inverse: recover the dimension from its ordinal.
+public export
+octadFromFin : Fin 8 -> OctadDimension
+octadFromFin FZ                                    = Data
+octadFromFin (FS FZ)                               = Metadata
+octadFromFin (FS (FS FZ))                          = Provenance
+octadFromFin (FS (FS (FS FZ)))                     = Lineage
+octadFromFin (FS (FS (FS (FS FZ))))                = Constraints
+octadFromFin (FS (FS (FS (FS (FS FZ)))))           = AccessControl
+octadFromFin (FS (FS (FS (FS (FS (FS FZ))))))      = Temporal
+octadFromFin (FS (FS (FS (FS (FS (FS (FS FZ))))))) = Simulation
+
+||| Round-trip 1: every dimension survives ordinal encode/decode (injective).
+export
+octadFinInverseL : (d : OctadDimension) -> octadFromFin (octadToFin d) = d
+octadFinInverseL Data          = Refl
+octadFinInverseL Metadata      = Refl
+octadFinInverseL Provenance    = Refl
+octadFinInverseL Lineage       = Refl
+octadFinInverseL Constraints   = Refl
+octadFinInverseL AccessControl = Refl
+octadFinInverseL Temporal      = Refl
+octadFinInverseL Simulation    = Refl
+
+||| Round-trip 2: every ordinal in [0,8) names a dimension (surjective, no gaps).
+export
+octadFinInverseR : (i : Fin 8) -> octadToFin (octadFromFin i) = i
+octadFinInverseR FZ                                    = Refl
+octadFinInverseR (FS FZ)                               = Refl
+octadFinInverseR (FS (FS FZ))                          = Refl
+octadFinInverseR (FS (FS (FS FZ)))                     = Refl
+octadFinInverseR (FS (FS (FS (FS FZ))))                = Refl
+octadFinInverseR (FS (FS (FS (FS (FS FZ)))))           = Refl
+octadFinInverseR (FS (FS (FS (FS (FS (FS FZ))))))      = Refl
+octadFinInverseR (FS (FS (FS (FS (FS (FS (FS FZ))))))) = Refl
+
+--------------------------------------------------------------------------------
+-- 2. DriftCategory ≅ OctadDimension  (the asserted bijection, made real)
+--------------------------------------------------------------------------------
+
+||| Each drift category detects inconsistency in exactly one octad dimension,
+||| paired by ordinal.
+public export
+driftToDim : DriftCategory -> OctadDimension
+driftToDim Structural      = Data
+driftToDim SemanticDrift   = Metadata
+driftToDim TemporalDrift   = Provenance
+driftToDim Statistical     = Lineage
+driftToDim Referential     = Constraints
+driftToDim ProvenanceDrift = AccessControl
+driftToDim SpatialDrift    = Temporal
+driftToDim EmbeddingDrift  = Simulation
+
+||| Inverse pairing.
+public export
+dimToDrift : OctadDimension -> DriftCategory
+dimToDrift Data          = Structural
+dimToDrift Metadata      = SemanticDrift
+dimToDrift Provenance    = TemporalDrift
+dimToDrift Lineage       = Statistical
+dimToDrift Constraints   = Referential
+dimToDrift AccessControl = ProvenanceDrift
+dimToDrift Temporal      = SpatialDrift
+dimToDrift Simulation    = EmbeddingDrift
+
+||| The drift↔octad correspondence is a genuine bijection (round-trip 1).
+export
+driftDimInverseL : (c : DriftCategory) -> dimToDrift (driftToDim c) = c
+driftDimInverseL Structural      = Refl
+driftDimInverseL SemanticDrift   = Refl
+driftDimInverseL TemporalDrift   = Refl
+driftDimInverseL Statistical     = Refl
+driftDimInverseL Referential     = Refl
+driftDimInverseL ProvenanceDrift = Refl
+driftDimInverseL SpatialDrift    = Refl
+driftDimInverseL EmbeddingDrift  = Refl
+
+||| …and round-trip 2.
+export
+driftDimInverseR : (d : OctadDimension) -> driftToDim (dimToDrift d) = d
+driftDimInverseR Data          = Refl
+driftDimInverseR Metadata      = Refl
+driftDimInverseR Provenance    = Refl
+driftDimInverseR Lineage       = Refl
+driftDimInverseR Constraints   = Refl
+driftDimInverseR AccessControl = Refl
+driftDimInverseR Temporal      = Refl
+driftDimInverseR Simulation    = Refl
+
+--------------------------------------------------------------------------------
+-- 3. Sidecar isolation: the write model agrees with the tier classification
+--------------------------------------------------------------------------------
+
+||| Whether augmenting a given octad dimension writes to the *target* database.
+||| Defined per-dimension (independently of `dimensionTier`): the three
+||| read-path/sidecar dimensions never touch the target; the overlay dimensions
+||| add storage alongside it.
+public export
+writesTarget : OctadDimension -> Bool
+writesTarget Provenance  = False  -- piggyback: append-only provenance sidecar
+writesTarget Temporal    = False  -- piggyback: read-path temporal snapshots
+writesTarget Constraints = False  -- piggyback: read-path drift observation
+writesTarget Data          = True
+writesTarget Metadata      = True
+writesTarget Lineage       = True
+writesTarget AccessControl = True
+writesTarget Simulation    = True
+
+||| SIDECAR ISOLATION (the core safety guarantee): every Tier-1 (piggyback)
+||| dimension provably never writes to the target database. This proves the
+||| independently-defined write model is *consistent* with the tier model — a
+||| real cross-check, not a tautology.
+export
+tier1NeverWritesTarget : (d : OctadDimension) ->
+                         dimensionTier d = Tier1 -> writesTarget d = False
+tier1NeverWritesTarget Provenance    _ = Refl
+tier1NeverWritesTarget Temporal      _ = Refl
+tier1NeverWritesTarget Constraints   _ = Refl
+tier1NeverWritesTarget Data          Refl impossible
+tier1NeverWritesTarget Metadata      Refl impossible
+tier1NeverWritesTarget Lineage       Refl impossible
+tier1NeverWritesTarget AccessControl Refl impossible
+tier1NeverWritesTarget Simulation    Refl impossible
+
+||| Dual: every Tier-2 (overlay) dimension does write to the target — so the
+||| isolation above is not vacuous (the two tiers genuinely partition by write
+||| behaviour).
+export
+tier2WritesTarget : (d : OctadDimension) ->
+                    dimensionTier d = Tier2 -> writesTarget d = True
+tier2WritesTarget Data          _ = Refl
+tier2WritesTarget Metadata      _ = Refl
+tier2WritesTarget Lineage       _ = Refl
+tier2WritesTarget AccessControl _ = Refl
+tier2WritesTarget Simulation    _ = Refl
+tier2WritesTarget Provenance    Refl impossible
+tier2WritesTarget Temporal      Refl impossible
+tier2WritesTarget Constraints   Refl impossible
+
+--------------------------------------------------------------------------------
+-- Negative controls (the invariants are non-vacuous)
+--------------------------------------------------------------------------------
+
+||| Distinct dimensions are genuinely distinct — the ordinal tagging cannot
+||| collide two dimensions onto one slot.
+export
+dataNotMetadata : Not (Data = Metadata)
+dataNotMetadata Refl impossible
+
+||| Sidecar isolation has real content: at least one dimension *does* write to
+||| the target, so `writesTarget` is not constantly `False`.
+export
+dataDoesWrite : writesTarget Data = True
+dataDoesWrite = Refl

src/interface/abi/verisimiser-abi.ipkg

@@ -9,3 +9,4 @@ modules = Verisimiser.ABI.Types
         , Verisimiser.ABI.Layout
         , Verisimiser.ABI.Foreign
         , Verisimiser.ABI.Proofs
+        , Verisimiser.ABI.Octad