feat(abi): binary ABI + Zig↔Idris layout cross-check

.claude/CLAUDE.md

@@ -41,7 +41,7 @@ panic-attack assail .
 ```
 Gossamer GUI (Ephapax .eph)        -- src/core/, src/gui/panels/
     |  IPC (gossamer:// protocol)
-Zig FFI (libgsa.so + gsa CLI)     -- src/interface/ffi/src/ (9 modules)
+Zig FFI (libgsa.so + gsa CLI)     -- src/interface/ffi/src/ (11 modules)
     |  C ABI (13 result codes)
 Idris2 ABI (Types/Foreign/Layout)  -- src/interface/abi/
     |  REST (port 8090)
@@ -60,8 +60,13 @@ VeriSimDB (8-modality octads)      -- container/verisimdb/
 | `server_actions.zig` | Start/stop/restart/logs via Podman/Docker/systemd |
 | `game_profiles.zig` | A2ML profile registry + parser |
 | `groove_client.zig` | .well-known Groove voice alerting |
+| `abi_layout.zig` | Canonical C-ABI `extern struct`s + comptime Zig↔Idris layout cross-check |
+| `abi_serde.zig` | Binary ABI emitters + offset readers (`read_int`/`read_ptr`/…) — makes `Layout.idr` offsets a live contract |
 | `cli.zig` | Standalone CLI executable (status, probe, profiles, version) |
 
+`abi_layout_expected.zig` is generated from `Layout.idr` by
+`scripts/gen_abi_expected.py` (regenerate when `Layout.idr` changes).
+
 ## Key Conventions
 
 - **All exported FFI functions** are prefixed `gossamer_gsa_` and use `pub export fn ... callconv(.c)`
@@ -78,13 +83,15 @@ VeriSimDB (8-modality octads)      -- container/verisimdb/
 
 - **Completion**: 93% (15 phases built; v1.0.0 gates still open — see Remaining)
 - **Zig version**: 0.15.2 (see `.tool-versions`)
-- **Exported FFI symbols**: 27 (comptime linker hints in main.zig)
-- **Tests**: 111 Zig tests across 3 suites (unit: 67, integration: 39, smoke: 5). All passing.
+- **Exported FFI symbols**: 38 (comptime linker hints in main.zig)
+- **Tests**: 124 Zig tests across 3 suites (unit: 80, integration: 39, smoke: 5). All passing.
   - Security tests for command injection in server_actions
   - Config parser edge cases for all 8 formats
   - A2ML round-trip, diff, and secret redaction tests
   - Groove target registry overflow and buffer truncation tests
+  - ABI layout cross-check + binary ABI round-trip (read at proven `Layout.idr` offsets)
 - **Idris2 ABI**: Alignment postulate replaced with constructive proof (`alignUpCeil` + `alignUpCeilIsMultiple`)
+- **Cross-language ABI**: `abi_layout.zig` asserts (at compile time + `zig build test`) that the 8 `extern struct`s match the proven `Layout.idr` offsets/sizes; `abi_serde.zig` implements the offset readers/emitters so those offsets are a live runtime contract (was the open HIGH proof item)
 - **VeriSimDB**: Main on 8090 (built, running), backup on 8091 (game saves)
 - **Container**: Containerfile wired with real Zig build, entrypoint.sh execs gsa
 - **Nix/Guix**: Both flake.nix and guix.scm have real build/install phases

PROOF-NEEDS.md

@@ -1,9 +1,11 @@
 # Proof Requirements
 
-## Current State (2026-06-21 — verified with Idris2 0.7.0)
+## Current State (2026-06-21 — verified with Idris2 0.7.0 + Zig 0.15.2)
 
 The ABI package typechecks end-to-end (all modules `%default total`, no
-`postulate` / `believe_me` / `assert_total`):
+`postulate` / `believe_me` / `assert_total`), and the hand-written Idris layout
+constants are now cross-checked against the real C layout the Zig compiler emits
+(see *Cross-language ABI* below):
 
 ```bash
 cd src/interface/abi && idris2 --typecheck gsa-abi.ipkg
@@ -54,13 +56,36 @@ Decidable `portInRange`, `nonEmptyId`, `configFieldCountPositive`,
 `allPortsValid`, the `Valid*` smart constructors, and the linear
 `ServerHandle` with its erased non-null witness.
 
+### Cross-language ABI (`abi_layout.zig` / `abi_serde.zig`)
+The Idris proofs above show the *model* is internally consistent; the Zig side
+now checks that model against reality and makes it a live runtime contract.
+
+- **Layout cross-check (was the open HIGH item).** Each of the 8 structs is
+  declared as a Zig `extern struct` (`abi_layout.zig`). A comptime block asserts
+  `@offsetOf` / `@sizeOf` / `@alignOf` of every field equals the proven Idris
+  constant — lifted verbatim from `Layout.idr` into `abi_layout_expected.zig` by
+  `scripts/gen_abi_expected.py`. Any divergence is a **compile error**, so the
+  library cannot build against a layout the proofs do not describe. A negative
+  test (perturbing one offset) confirms the guard bites; the check also runs
+  under `zig build test`.
+- **Live offset contract.** The previously-unimplemented FFI readers that
+  `GSA.ABI.Foreign` binds are now real (`abi_serde.zig`): `read_int` /
+  `read_double` / `read_ptr` decode fields at a byte offset; `read_string`,
+  `array_len`, `array_get_string`, `is_null`, `free` handle strings/arrays;
+  `apply_config` / `close_handle` round out the surface. Emitters
+  (`serializeDriftReport` / `serializeFingerprint` / `serializeStringArray`)
+  write the wire structs, and `gossamer_gsa_drift_struct` exports one. Round-trip
+  tests read each field back at its **proven** `Layout.idr` offset, standing in
+  for the Idris reader — so agreement is an end-to-end cross-language guarantee.
+- **Idris consumer.** `Foreign.getDrift` now decodes a `DriftReport` at offsets
+  taken from `offsetOf … driftReportLayout` (not the previous, wrong hand-tuned
+  `0/4/12/20/28`), via `prim__driftStruct` + `prim__readPtr`/`readInt`/`readDouble`.
+
+> Regenerate the expected table whenever `Layout.idr` changes:
+> `python3 scripts/gen_abi_expected.py` (then the Zig cross-check re-validates).
+
 ## What still needs proving
 
-- **Zig ↔ Idris layout cross-check (HIGH).** `Layout.idr` proves the Idris
-  model is internally consistent, but nothing yet checks the hand-written
-  field offsets/sizes against Zig's `@sizeOf`/`@offsetOf`. A generated test
-  emitting Zig's numbers and comparing them to the `Layout` constants would
-  close the actual cross-language ABI guarantee.
 - **Server probe safety (MEDIUM).** Prove probes cause no side effects on
   targets. Needs a specification first.
 - **Configuration drift-detection completeness (LOW).** Needs a richer spec.

scripts/gen_abi_expected.py

@@ -0,0 +1,123 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: AGPL-3.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# gen_abi_expected.py — extract the canonical C-ABI layout numbers from the
+# machine-checked Idris2 model (src/interface/abi/Layout.idr) and emit a Zig
+# source file (src/interface/ffi/src/abi_layout_expected.zig) consumed by the
+# Zig-side cross-check (abi_layout.zig).
+#
+# Layout.idr is the single source of truth: it carries the proofs (NoOverlap,
+# AllFieldsAligned, SizeAligned, SizeCoversFields). This script lifts the same
+# `MkFieldDesc name offset size align` / `MkStructLayout [...] total align`
+# constants into Zig so the compiler can assert `@offsetOf`/`@sizeOf`/`@alignOf`
+# of the canonical extern structs agree with the proven model.
+#
+# Run from the repository root:
+#   python3 scripts/gen_abi_expected.py
+# The build/CI re-runs this and `git diff --exit-code`s the result to guarantee
+# the Zig expectations never drift from the Idris proofs.
+
+import re
+import sys
+import pathlib
+
+# Idris layout variable (lowerCamel, without the "Layout" suffix) -> Zig struct
+# type name. Drives both extraction and the emitted const names.
+STRUCTS = {
+    "serverHandle": "ServerHandle",
+    "probeResult": "ProbeResult",
+    "configField": "ConfigField",
+    "a2mlConfig": "A2MLConfig",
+    "gameProfile": "GameProfile",
+    "serverOctad": "ServerOctad",
+    "fingerprint": "Fingerprint",
+    "driftReport": "DriftReport",
+}
+
+FIELD_RE = re.compile(
+    r'MkFieldDesc\s+"(?P<name>\w+)"\s+(?P<offset>\d+)\s+(?P<size>\d+)\s+(?P<align>\d+)'
+)
+
+
+def parse_layout(text, var):
+    """Return (fields, total_size, struct_align) for `<var>Layout`."""
+    # Match:  <var>Layout = MkStructLayout [ ...fields... ] <total> <align>
+    block_re = re.compile(
+        r'\b' + re.escape(var) + r'Layout\s*=\s*MkStructLayout\s*\[(?P<body>.*?)\]\s*'
+        r'(?P<total>\d+)\s+(?P<align>\d+)',
+        re.DOTALL,
+    )
+    m = block_re.search(text)
+    if not m:
+        raise SystemExit(f"error: could not find {var}Layout in Layout.idr")
+    fields = []
+    for fm in FIELD_RE.finditer(m.group("body")):
+        name = fm.group("name")
+        if name.startswith("padding"):
+            continue  # implicit C padding; not a real extern-struct field
+        fields.append(
+            (name, int(fm.group("offset")), int(fm.group("size")), int(fm.group("align")))
+        )
+    return fields, int(m.group("total")), int(m.group("align"))
+
+
+def main():
+    root = pathlib.Path(__file__).resolve().parent.parent
+    layout_idr = root / "src" / "interface" / "abi" / "Layout.idr"
+    out_zig = root / "src" / "interface" / "ffi" / "src" / "abi_layout_expected.zig"
+
+    text = layout_idr.read_text(encoding="utf-8")
+
+    out = []
+    out.append("// SPDX-License-Identifier: AGPL-3.0-or-later")
+    out.append("// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>")
+    out.append("//")
+    out.append("// @generated by scripts/gen_abi_expected.py from src/interface/abi/Layout.idr")
+    out.append("// DO NOT EDIT. Regenerate with: python3 scripts/gen_abi_expected.py")
+    out.append("//")
+    out.append("// Canonical C-ABI layout numbers lifted from the machine-checked Idris2 model")
+    out.append("// (GSA.ABI.Layout). Consumed by abi_layout.zig to assert that the Zig extern")
+    out.append("// structs agree, byte-for-byte, with the proven Idris layout.")
+    out.append("")
+    out.append("pub const Field = struct {")
+    out.append("    name: []const u8,")
+    out.append("    offset: u32,")
+    out.append("    size: u32,")
+    out.append("    alignment: u32,")
+    out.append("};")
+    out.append("")
+    out.append("pub const StructExpect = struct {")
+    out.append("    name: []const u8,")
+    out.append("    total_size: u32,")
+    out.append("    struct_align: u32,")
+    out.append("    fields: []const Field,")
+    out.append("};")
+    out.append("")
+
+    names = []
+    for var, zig_name in STRUCTS.items():
+        fields, total, align = parse_layout(text, var)
+        names.append(zig_name)
+        out.append(f"pub const {zig_name} = StructExpect{{")
+        out.append(f'    .name = "{zig_name}",')
+        out.append(f"    .total_size = {total},")
+        out.append(f"    .struct_align = {align},")
+        out.append("    .fields = &.{")
+        for (fn, off, sz, al) in fields:
+            out.append(
+                f'        .{{ .name = "{fn}", .offset = {off}, .size = {sz}, .alignment = {al} }},'
+            )
+        out.append("    },")
+        out.append("};")
+        out.append("")
+
+    out.append("pub const all = [_]StructExpect{ " + ", ".join(names) + " };")
+    out.append("")
+
+    out_zig.write_text("\n".join(out), encoding="utf-8")
+    print(f"wrote {out_zig.relative_to(root)} ({len(names)} structs)")
+
+
+if __name__ == "__main__":
+    sys.exit(main())

src/interface/abi/Foreign.idr

@@ -192,6 +192,23 @@ export
 %foreign "C:gossamer_gsa_array_get_string, libgossamer_gsa"
 prim__arrayGetString : AnyPtr -> Int -> PrimIO String
 
+||| Read a pointer field at a byte offset from a serialised struct. Combined
+||| with prim__readString this decodes char* fields at their proven offsets:
+||| readString (readPtr struct (offsetOf "serverId" layout)).
+|||
+||| C signature: void* gossamer_gsa_read_ptr(void* ptr, int32_t offset)
+export
+%foreign "C:gossamer_gsa_read_ptr, libgossamer_gsa"
+prim__readPtr : AnyPtr -> Int -> PrimIO AnyPtr
+
+||| Emit a binary DriftReport wire struct (canonical Layout.idr layout) for a
+||| tracked server. The returned pointer must be released with prim__free.
+|||
+||| C signature: void* gossamer_gsa_drift_struct(const char* server_id)
+export
+%foreign "C:gossamer_gsa_drift_struct, libgossamer_gsa"
+prim__driftStruct : String -> PrimIO AnyPtr
+
 --------------------------------------------------------------------------------
 -- Internal Helpers
 -- Utility functions used by the safe wrappers to convert between C
@@ -457,30 +474,40 @@ checkHealth = do
            Just status => pure (Right status)
            Nothing     => pure (Left Error)
 
-||| Get a drift report for a specific server.
-||| Compares the server's current VeriSimDB octad against its historical
-||| baseline across all modalities (config, semantic, temporal).
+||| Get a drift report for a specific server, decoded from the binary
+||| DriftReport wire struct emitted by gossamer_gsa_drift_struct.
+|||
+||| Every field is read at the offset *proven* in GSA.ABI.Layout
+||| (driftReportLayout): the char* field serverId via prim__readPtr, the scalars
+||| via prim__readInt / prim__readDouble. These are the same offsets the Zig
+||| layer is compile-time-checked against (abi_layout.zig), so this is the live
+||| cross-language ABI contract rather than hand-tuned constants.
+|||
+||| status reflects the tracked liveness; the configDrift / semanticDrift /
+||| temporalConsistency / overallScore metrics are 0.0 until VeriSimDB scoring
+||| is wired into the emitter.
 |||
 ||| @param serverId The server identifier to check
 ||| @return Left Result on failure, Right DriftReport on success
 export
 covering
 getDrift : String -> IO (Either Result DriftReport)
 getDrift serverId = do
-  ptr <- primIO (prim__verisimdbDrift serverId)
+  ptr <- primIO (prim__driftStruct serverId)
   case prim__isNull ptr /= 0 of
-    True => pure (Left VeriSimDBUnavailable)
+    True => pure (Left Error)
     False => do
-      -- Deserialise the DriftReport from the returned pointer.
-      -- Field offsets match the Zig struct layout (see Layout.idr).
-      statusCode    <- primIO (prim__readInt ptr 0)
-      configDrift   <- primIO (prim__readDouble ptr 4)
-      semanticDrift <- primIO (prim__readDouble ptr 12)
-      temporalCons  <- primIO (prim__readDouble ptr 20)
-      overallScore  <- primIO (prim__readDouble ptr 28)
+      let o = \name => the Int (cast (fromMaybe 0 (Layout.offsetOf name Layout.driftReportLayout)))
+      sidPtr        <- primIO (prim__readPtr ptr (o "serverId"))
+      sid           <- primIO (prim__readString sidPtr)
+      statusCode    <- primIO (prim__readInt ptr (o "status"))
+      configDrift   <- primIO (prim__readDouble ptr (o "configDrift"))
+      semanticDrift <- primIO (prim__readDouble ptr (o "semanticDrift"))
+      temporalCons  <- primIO (prim__readDouble ptr (o "temporalConsistency"))
+      overallScore  <- primIO (prim__readDouble ptr (o "overallScore"))
       primIO (prim__free ptr)
       let status = fromMaybe Warning (healthStatusFromInt statusCode)
-      pure (Right (MkDriftReport serverId status configDrift semanticDrift temporalCons overallScore))
+      pure (Right (MkDriftReport sid status configDrift semanticDrift temporalCons overallScore))
 
 --------------------------------------------------------------------------------
 -- Safe Wrappers: Profile Management