merge: bring claude/admiring-babbage-4l40ko up to main (#37 proofs + CI #34-36)

claude · claude · commit fde37c488148 · 2026-06-21T06:46:39.000Z
diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml
@@ -14,6 +14,7 @@ on:
 jobs:
   trigger-boj:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     if: ${{ vars.BOJ_SERVER_URL != '' || secrets.BOJ_SERVER_URL != '' }}
     steps:
       - name: Checkout
diff --git a/.github/workflows/casket-pages.yml b/.github/workflows/casket-pages.yml
@@ -18,6 +18,7 @@ concurrency:
 jobs:
   build:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     steps:
       - name: Checkout
         uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
@@ -109,6 +110,7 @@ jobs:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     needs: build
     steps:
       - name: Deploy to GitHub Pages
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
@@ -23,6 +23,7 @@ permissions:
 jobs:
   analyze:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     permissions:
       contents: read
       security-events: write
diff --git a/.github/workflows/cross-platform.yml b/.github/workflows/cross-platform.yml
@@ -1,7 +1,8 @@
-# Cross-platform CI for Game Server Admin
-# Builds and tests on Linux, macOS, and Windows
-#
 # SPDX-License-Identifier: MPL-2.0
+# CI for Game Server Admin — Linux only for now.
+# macOS and Windows are deferred to the dedicated cross-platform effort:
+# the FFI is currently POSIX-only (fcntl sockets, posix.getenv) and does
+# not compile on Windows. Re-add the matrix legs there.
 
 name: Cross-Platform Build & Test
 
@@ -20,25 +21,22 @@ jobs:
       fail-fast: false
       matrix:
         include:
+          # Linux only for now; macOS/Windows deferred to the cross-platform
+          # effort. Kept as a matrix so re-adding os/name there is trivial.
           - os: ubuntu-latest
             name: Linux
             run-integration: true
-          - os: macos-latest
-            name: macOS
-            run-integration: false
-          - os: windows-latest
-            name: Windows
-            run-integration: false
 
     name: ${{ matrix.name }}
     runs-on: ${{ matrix.os }}
+    timeout-minutes: 30
 
     steps:
       - name: Checkout
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
 
       - name: Install Zig 0.15.2
-        uses: goto-bus-stop/setup-zig@7ab2955eb728f5440978d7e4148f16f0e36aa02f # v2.2.1
+        uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
         with:
           version: 0.15.2
 
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
@@ -22,6 +22,7 @@ jobs:
   a2ml-validate:
     name: Validate A2ML manifests
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -66,6 +67,7 @@ jobs:
   k9-validate:
     name: Validate K9 contracts
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -115,6 +117,7 @@ jobs:
   empty-lint:
     name: Empty-linter (invisible characters)
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -179,6 +182,7 @@ jobs:
   groove-check:
     name: Groove manifest check
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -237,6 +241,7 @@ jobs:
   eclexiaiser-validate:
     name: Validate eclexiaiser manifest
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -300,6 +305,7 @@ print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))')
   dogfood-summary:
     name: Dogfooding compliance summary
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate]
     if: always()
 
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
@@ -43,6 +43,7 @@ jobs:
   scan:
     name: Hypatia Neurosymbolic Analysis
     runs-on: ubuntu-latest
+    timeout-minutes: 30
 
     steps:
       - name: Checkout repository
diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml
@@ -14,6 +14,7 @@ permissions:
 jobs:
   dispatch:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - name: Trigger Propagation
         uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -18,6 +18,7 @@ jobs:
   build:
     name: Build Artifacts
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     permissions:
       contents: read
     steps:
@@ -44,6 +45,7 @@ jobs:
   changelog:
     name: Generate Changelog
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     permissions:
       contents: read
     outputs:
@@ -90,6 +92,7 @@ jobs:
     name: Create GitHub Release
     needs: [build, changelog]
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     permissions:
       contents: write
     steps:
diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml
@@ -27,6 +27,7 @@ permissions:
 jobs:
   rhodibot:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Checkout
         uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
diff --git a/.github/workflows/scorecard-enforcer.yml b/.github/workflows/scorecard-enforcer.yml
@@ -23,6 +23,7 @@ permissions:
 jobs:
   scorecard:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       security-events: write
       id-token: write  # For OIDC
@@ -61,6 +62,7 @@ jobs:
   # Check specific high-priority items
   check-critical:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml
@@ -19,6 +19,7 @@ jobs:
   panic-attack-assail:
     name: panic-attack assail
     runs-on: ubuntu-latest
+    timeout-minutes: 30
 
     steps:
       - name: Checkout repository
@@ -123,6 +124,7 @@ jobs:
   hypatia-scan:
     name: Hypatia neurosymbolic scan
     runs-on: ubuntu-latest
+    timeout-minutes: 30
 
     steps:
       - name: Checkout repository
@@ -235,6 +237,7 @@ jobs:
   patch-bridge-triage:
     name: Patch Bridge CVE triage
     runs-on: ubuntu-latest
+    timeout-minutes: 30
 
     steps:
       - name: Checkout repository
@@ -324,6 +327,7 @@ jobs:
   deposit-findings:
     name: Deposit findings for gitbot-fleet
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     needs: [panic-attack-assail, hypatia-scan, patch-bridge-triage]
     if: always()
 
diff --git a/PROOF-NEEDS.md b/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).
diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Foreign.idr
diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Layout.idr
diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Types.idr
diff --git a/src/interface/abi/gsa-abi.ipkg b/src/interface/abi/gsa-abi.ipkg
diff --git a/src/interface/ffi/src/probe.zig b/src/interface/ffi/src/probe.zig
