diff --git a/.github/workflows/abi-ffi-gate.yml b/.github/workflows/abi-ffi-gate.yml new file mode 100644 index 0000000..269464d --- /dev/null +++ b/.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 diff --git a/scripts/abi-ffi-gate.py b/scripts/abi-ffi-gate.py new file mode 100755 index 0000000..9ee96db --- /dev/null +++ b/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) +# +# 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:"` symbol declared anywhere in the ABI .idr +# sources is exported by the Zig FFI (`export fn `); +# 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"(? 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()) diff --git a/src/interface/abi/Verisimiser/ABI/Octad.idr b/src/interface/abi/Verisimiser/ABI/Octad.idr new file mode 100644 index 0000000..9f42fc9 --- /dev/null +++ b/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) +-- +||| 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 diff --git a/src/interface/abi/verisimiser-abi.ipkg b/src/interface/abi/verisimiser-abi.ipkg index 868e348..8533052 100644 --- a/src/interface/abi/verisimiser-abi.ipkg +++ b/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