proof(abi): machine-check layout properties for all 8 ABI structs (Idris2 0.7.0) (#37)

The Idris2 ABI had never compiled (no .ipkg; modules declared `module
Types/Layout/Foreign` but cross-imported as `GSA.ABI.*`). This makes the
package build and proves the previously-declared-but-unpopulated layout
predicates. Verified end-to-end with Idris2 0.7.0:

    cd src/interface/abi && idris2 --typecheck gsa-abi.ipkg

Build fixes (package compiles for the first time):
- Add gsa-abi.ipkg; fix imports GSA.ABI.* -> flat module names.
- Types.idr: %hide Data.List.NonEmpty (name clash); nonEmptyId via `with`
  (case on `unpack s` did not refine the dependent goal); rename a
  shadowing pattern variable.
- Layout.idr: alignUpCeilIsMultiple did NOT typecheck as written; rewritten
  via an in-module total `ceilDiv` so the multiple-witness is a direct Refl.
- Foreign.idr: `total` is a reserved word (renamed param); fix linear
  ServerHandle misuse in extractConfig/applyConfig/serverAction/getLogs/
  closeHandle (consume the handle by pattern match, rebuild for the
  borrow-return).

Proofs (32 = 8 structs x 4 properties), all machine-checked:
- NoOverlap, AllFieldsAligned, SizeAligned, SizeCoversFields for
  ServerHandle, ProbeResult, ConfigField, A2MLConfig, GameProfile,
  ServerOctad, Fingerprint, DriftReport.
- Discharged by decision procedures extracted via getYes; each proof
  typechecks only because its Dec reduces to Yes for that concrete layout.

PROOF-NEEDS.md updated to the verified state (corrects the stale
alignUpEquiv claim; records the Zig<->Idris cross-check as the main
remaining obligation).

No postulates / believe_me / assert_total; all modules %default total.


Claude-Session: https://claude.ai/code/session_01LvsZgNxFbeqfRmrVFNhJ8G

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -1,46 +1,72 @@
 # Proof Requirements
 
-## Current State (2026-04-03 blitz)
+## Current State (2026-06-21 — verified with Idris2 0.7.0)
 
-- ABI exists in `src/interface/abi/Layout.idr`
-- **RESOLVED**: `postulate alignUpProducesAligned` replaced with constructive proof
-- Remaining: one weaker equivalence postulate (`alignUpEquiv`)
+The ABI package typechecks end-to-end (all modules `%default total`, no
+`postulate` / `believe_me` / `assert_total`):
 
-## What Was Done
+```bash
+cd src/interface/abi && idris2 --typecheck gsa-abi.ipkg
+# 1/3: Building Types (Types.idr)
+# 2/3: Building Layout (Layout.idr)
+# 3/3: Building Foreign (Foreign.idr)
+```
 
-### Alignment Proof (CLOSED)
+Toolchain: Idris2 0.7.0, Chez backend (`.tool-versions` pins `idris2 0.7.0`).
 
-The original `postulate alignUpProducesAligned` asserted that `alignUp` produces
-aligned results but could not be proven because Idris2 0.7.x's `modNatNZ` lacks
-composition lemmas.
+## What is proven (machine-checked)
 
-**Solution**: Introduced `alignUpCeil` — an alternative alignment function that
-computes the next multiple via ceiling division. The result is `k * alignment`
-by construction, so the alignment property is trivially witnessed:
+### Memory layout (`Layout.idr`)
+For every one of the 8 ABI structs — ServerHandle, ProbeResult, ConfigField,
+A2MLConfig, GameProfile, ServerOctad, Fingerprint, DriftReport — all four
+layout properties are proven:
 
-- `alignUpCeil` : computes next multiple via `ceilDiv(n, a) * a`
-- `alignUpCeilIsMultiple` : constructive proof returning `MkMultiple k Refl`
+| Property | Meaning |
+|----------|---------|
+| `NoOverlap` | no two fields' `[offset, offset+size)` ranges overlap |
+| `AllFieldsAligned` | every field offset is a multiple of its alignment |
+| `SizeAligned` | total struct size is a multiple of the struct alignment |
+| `SizeCoversFields` | total size ≥ sum of field sizes (padding accounted) |
 
-No postulates, no `believe_me`. Both cases (`remainder = 0` and `remainder > 0`)
-return a direct `Refl` witness.
+Discharged by decision procedures (`decNoOverlap`, `decAllAligned`,
+`decSizeAligned`, `decSizeCovers`) extracted via `getYes`; each proof
+typechecks only because its `Dec` reduces to `Yes` for that concrete layout —
+i.e. a malformed layout would fail to compile.
 
-**Remaining postulate**: `alignUpEquiv` asserts that `alignUp` and `alignUpCeil`
-produce the same result. This is mathematically trivial but opaque `modNatNZ`
-prevents structural proof. Strictly weaker than the original postulate.
+Also still proven: the per-type size/alignment `Refl` proofs, the
+`SizeOf`↔layout agreement (`LayoutMatchesSizeOf`), and cross-platform
+x86_64 ≡ aarch64 equivalence.
 
-## What Still Needs Proving
+### Alignment (`Layout.idr`)
+- `alignUpCeil offset a = ceilDiv offset a * a` (via an in-module total
+  `ceilDiv`).
+- `alignUpCeilIsMultiple` — constructive `Refl` proof that the result is
+  `k * a`.
 
-- **Server probe safety**: Prove that probes do not cause side effects on targets
-- **Configuration drift detection**: Prove drift dashboard identifies all deviations
-- **Access control for admin panels**: Prove panel-level authorization
+> Correction to the prior version of this file: the earlier
+> `alignUpCeilIsMultiple` did **not** typecheck (the `case` form left the
+> goal stuck). It was rewritten via `ceilDiv` so the witness is a direct
+> `Refl`. There is no remaining `alignUpEquiv` postulate — the proven path
+> uses `alignUpCeil`/`ceilDiv` directly, so that obligation is moot.
 
-## When alignUpEquiv Can Be Closed
+### Domain validators (`Types.idr`)
+Decidable `portInRange`, `nonEmptyId`, `configFieldCountPositive`,
+`allPortsValid`, the `Valid*` smart constructors, and the linear
+`ServerHandle` with its erased non-null witness.
 
-When Idris2 stdlib gains either:
-- `modNatNZ_zero : modNatNZ (k * d) d ok = 0`
-- `modNatNZ_spec : n = divNatNZ n d ok * d + modNatNZ n d ok`
+## What still needs proving
 
-## Priority
-- **DONE** — Alignment proof is constructive
-- **MEDIUM** — Server probe safety (production concern)
-- **LOW** — Drift detection, access control (need richer specifications)
+- **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.
+- **Access control for admin panels (LOW).** Needs a specification.
+
+## Notes
+- `Foreign.idr`'s linear `ServerHandle` wrappers now typecheck: each handle is
+  consumed by a pattern match and rebuilt for the borrow-return, so linearity
+  is respected (previously they used the handle twice and did not compile).

src/interface/abi/Foreign.idr

@@ -23,8 +23,8 @@
 
 module Foreign
 
-import GSA.ABI.Types
-import GSA.ABI.Layout
+import Types
+import Layout
 
 import Data.List
 import Data.Maybe
@@ -233,12 +233,12 @@ readStringArray ptr = do
   where
     covering
     go : Int -> Int -> List String -> IO (List String)
-    go idx total acc =
-      if idx >= total
+    go idx tot acc =
+      if idx >= tot
         then pure (reverse acc)
         else do
           s <- primIO (prim__arrayGetString ptr idx)
-          go (idx + 1) total (s :: acc)
+          go (idx + 1) tot (s :: acc)
 
 --------------------------------------------------------------------------------
 -- Safe Wrappers: Server Lifecycle
@@ -302,10 +302,10 @@ fingerprint host ports = do
 export
 covering
 extractConfig : (1 handle : ServerHandle) -> GameProfile -> IO (Either Result A2MLConfig, ServerHandle)
-extractConfig handle profile = do
-  ptr <- primIO (prim__extractConfig handle.rawPtr profile.id)
+extractConfig (MkServerHandle p sid v) profile = do
+  ptr <- primIO (prim__extractConfig p profile.id)
   case prim__isNull ptr /= 0 of
-    True => pure (Left NullPointer, handle)
+    True => pure (Left NullPointer, MkServerHandle p sid v)
     False => do
       -- Deserialise the A2MLConfig from the returned pointer
       serverId <- primIO (prim__readString ptr)
@@ -314,7 +314,7 @@ extractConfig handle profile = do
       configPath <- primIO (prim__arrayGetString ptr 3)
       primIO (prim__free ptr)
       let format = fromMaybe KeyValue (parseConfigFormat formatCode)
-      pure (Right (MkA2MLConfig serverId gameId format configPath []), handle)
+      pure (Right (MkA2MLConfig serverId gameId format configPath []), MkServerHandle p sid v)
   where
     parseConfigFormat : Int -> Maybe ConfigFormat
     parseConfigFormat 0 = Just XML
@@ -337,15 +337,15 @@ extractConfig handle profile = do
 export
 covering
 applyConfig : (1 handle : ServerHandle) -> A2MLConfig -> IO (Either Result (), ServerHandle)
-applyConfig handle config = do
+applyConfig (MkServerHandle p sid v) config = do
   -- The Zig layer accepts a serialised config struct.
   -- For now we pass the config path and let the Zig layer handle serialisation.
   -- A proper implementation would use prim__applyConfig with a packed struct.
-  result <- primIO (prim__serverAction handle.rawPtr ("apply:" ++ config.configPath))
+  result <- primIO (prim__serverAction p ("apply:" ++ config.configPath))
   let parsed = if result == 0
                  then Right ()
                  else Left (fromMaybe Error (resultFromInt (negate result)))
-  pure (parsed, handle)
+  pure (parsed, MkServerHandle p sid v)
 
 ||| Send a named action to the server (start, stop, restart, status, etc.),
 ||| BORROWING the handle. The action string must match one of the actions
@@ -357,11 +357,11 @@ applyConfig handle config = do
 export
 covering
 serverAction : (1 handle : ServerHandle) -> String -> IO (Either Result String, ServerHandle)
-serverAction handle action = do
-  result <- primIO (prim__serverAction handle.rawPtr action)
+serverAction (MkServerHandle p sid v) action = do
+  result <- primIO (prim__serverAction p action)
   if result >= 0
-    then pure (Right ("Action '" ++ action ++ "' completed (code " ++ show result ++ ")"), handle)
-    else pure (Left (fromMaybe Error (resultFromInt (negate result))), handle)
+    then pure (Right ("Action '" ++ action ++ "' completed (code " ++ show result ++ ")"), MkServerHandle p sid v)
+    else pure (Left (fromMaybe Error (resultFromInt (negate result))), MkServerHandle p sid v)
 
 ||| Retrieve the last N lines of server log output, BORROWING the handle.
 ||| Log lines are returned in chronological order (oldest first).
@@ -372,14 +372,14 @@ serverAction handle action = do
 export
 covering
 getLogs : (1 handle : ServerHandle) -> Nat -> IO (Either Result (List String), ServerHandle)
-getLogs handle lineCount = do
-  ptr <- primIO (prim__getLogs handle.rawPtr (cast lineCount))
+getLogs (MkServerHandle p sid v) lineCount = do
+  ptr <- primIO (prim__getLogs p (cast lineCount))
   case prim__isNull ptr /= 0 of
-    True => pure (Left NullPointer, handle)
+    True => pure (Left NullPointer, MkServerHandle p sid v)
     False => do
       lines <- readStringArray ptr
       primIO (prim__free ptr)
-      pure (Right lines, handle)
+      pure (Right lines, MkServerHandle p sid v)
 
 ||| Close and release a server handle, CONSUMING it.
 ||| After this call, the handle is no longer valid. The linear type system
@@ -391,8 +391,8 @@ getLogs handle lineCount = do
 export
 covering
 closeHandle : (1 handle : ServerHandle) -> IO Result
-closeHandle handle = do
-  result <- primIO (prim__closeHandle handle.rawPtr)
+closeHandle (MkServerHandle p _ _) = do
+  result <- primIO (prim__closeHandle p)
   pure (fromMaybe Error (resultFromInt result))
 
 --------------------------------------------------------------------------------