fix: repair the justfile's broken local gates + toolchain hygiene

.gitignore

@@ -46,3 +46,6 @@ dist/
 # Zig (FFI) build artifacts
 .zig-cache/
 zig-out/
+
+# Cross-compiled package binaries (just pkg-build-hello)
+examples/packages/hello.zpkg/binaries/

.tool-versions

@@ -1,3 +1,4 @@
 # SPDX-License-Identifier: MPL-2.0
 # asdf version manager configuration
 ocaml 5.1.1
+zig 0.13.0

docs/TOOLCHAIN.adoc

@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.8
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= Local toolchain setup
+
+Everything the CI gate runs (`.github/workflows/ci.yml`) can be reproduced
+locally with `just ci` plus `just proofs`. The pins live in `.tool-versions`.
+
+== Idris2 (>= 0.7.0) — the ABI proof layer
+
+Not packaged on most distros; bootstrap from source with Chez Scheme:
+
+[source,bash]
+----
+sudo apt-get install -y chezscheme libgmp-dev
+git clone --depth 1 -b v0.7.0 https://github.com/idris-lang/Idris2
+cd Idris2 && make bootstrap SCHEME=chezscheme && sudo make install
+----
+
+== OCaml (>= 4.14, pinned 5.1.1) with dune + menhir
+
+Via apt:
+
+[source,bash]
+----
+sudo apt-get install -y ocaml ocaml-dune menhir libmenhir-ocaml-dev \
+  libyojson-ocaml-dev libsedlex-ocaml-dev libppx-deriving-ocaml-dev \
+  libppx-deriving-yojson-ocaml-dev libalcotest-ocaml-dev ocaml-findlib
+----
+
+...or via opam:
+
+[source,bash]
+----
+opam install dune menhir sedlex yojson ppx_deriving ppx_deriving_yojson alcotest
+----
+
+== Zig (0.13 verified) — the FFI layer
+
+`just zig-ffi-check` compile-checks every FFI source without linking.
+A full `zig build` link requires system liboqs + libsodium
+(see `ffi/zig/build.zig` and `Containerfile.liboqs`).
+
+== The gate itself
+
+* `just proofs` — `idris2 --build src/abi/oblibeny-abi.ipkg`
+* `just ci` — dune lint + conformance suite + Zig FFI compile-check +
+  escape-hatch guard (no `believe_me` / `postulate` / `assert_total` /
+  `partial` / `idris_crash` / holes in the ABI proofs)

justfile

@@ -46,13 +46,22 @@ proofs:
 zig-ffi-check:
     @if command -v zig >/dev/null 2>&1; then \
         for f in ffi/zig/src/*.zig ffi/zig/src/packages/*.zig; do \
-            [ -f "$$f" ] && echo "ast-check $$f" && zig ast-check "$$f"; \
+            [ -f "$f" ] && echo "ast-check $f" && zig ast-check "$f"; \
         done; \
         echo "✓ Zig FFI sources compile-checked"; \
     else \
         echo "zig not installed — skipping (see ffi/zig/build.zig; Zig 0.13 verified in PR #56)"; \
     fi
 
+# Fail if any soundness escape hatch appears in the ABI proofs — same gate as ci.yml
+guard-escape-hatches:
+    @if grep -rnE 'believe_me|assert_total|\bpostulate\b|\bpartial\b|idris_crash|\?[A-Za-z_][A-Za-z0-9_]*' \
+         src/abi/Crypto.idr src/abi/Packages; then \
+        echo "ERROR: soundness escape hatch found in ABI proofs"; \
+        exit 1; \
+    fi
+    @echo "no escape hatches"
+
 # ============================================================================
 # RUN
 # ============================================================================
@@ -105,8 +114,8 @@ doc:
 # RELEASE
 # ============================================================================
 
-# Run all checks (lint + test)
-ci: lint test
+# Run all checks (lint + test + FFI compile-check + escape-hatch guard)
+ci: lint test zig-ffi-check guard-escape-hatches
     @echo "All checks passed."
 
 # Prepare a release
@@ -125,8 +134,8 @@ release VERSION:
 validate-spec:
     @echo "Validating specification files..."
     @for f in ANCHOR*.scm SPEC*.scm AUTHORITY*.scm; do \
-        if [ -f "$$f" ]; then \
-            echo "  ✓ $$f exists"; \
+        if [ -f "$f" ]; then \
+            echo "  ✓ $f exists"; \
         fi; \
     done
 
@@ -139,31 +148,35 @@ golden-path:
 # DISTRIBUTION PROOF-OF-CONCEPT
 # ============================================================================
 
-# Verify Idris2 ABI proofs for hello package
+# Verify Idris2 ABI proofs for hello package (ipkg-level; per-file --check is a fake gate)
 abi-check-hello:
-    @echo "Checking Idris2 ABI proofs..."
-    idris2 --check src/abi/packages/hello/Interface.idr
+    @echo "Checking Idris2 ABI proofs (via oblibeny-abi.ipkg)..."
+    cd src/abi && idris2 --build oblibeny-abi.ipkg
 
-# Generate C headers from Idris2 ABI
+# Generate C code from the Idris2 ABI interface (module root = src/abi)
 abi-gen-hello:
-    @echo "Generating C headers from Idris2..."
+    @echo "Generating C from Idris2..."
     mkdir -p generated/abi/hello
-    idris2 --codegen c src/abi/packages/hello/Interface.idr
-    @echo "Headers generated in generated/abi/"
+    cd src/abi && idris2 --codegen c Packages/Hello/Interface.idr
+    @echo "Generated under src/abi/build/ (C backend)"
 
 # Build Zig FFI library for hello package
 ffi-build-hello:
     @echo "Building Zig FFI for hello package..."
+    mkdir -p dist/ffi
     cd ffi/zig && zig build-lib src/packages/hello.zig \
         -dynamic \
         -target x86_64-linux-musl \
         -O ReleaseSafe \
-        -femit-bin=../../lib/libhello.so
-    @echo "Built: lib/libhello.so"
+        -femit-bin=../../dist/ffi/libhello.so
+    @echo "Built: dist/ffi/libhello.so"
 
 # Build hello package for all architectures
 pkg-build-hello:
     @echo "Cross-compiling hello for all architectures..."
+    @mkdir -p examples/packages/hello.zpkg/binaries/x86_64 \
+        examples/packages/hello.zpkg/binaries/aarch64 \
+        examples/packages/hello.zpkg/binaries/riscv64
     @echo "  x86_64..."
     @cd examples/packages/hello.zpkg && \
         echo 'const std = @import("std"); pub fn main() !void { std.debug.print("Hello, Oblibeny Distribution!\\n", .{}); }' > hello.zig && \
@@ -177,7 +190,7 @@ pkg-build-hello:
     @cd examples/packages/hello.zpkg && \
         zig build-exe hello.zig -target riscv64-linux-musl -O ReleaseSafe && \
         mv hello binaries/riscv64/ && \
-        rm hello.zig hello.o || true
+        rm -f hello.zig hello.o
     @echo "✓ Cross-compilation complete"
 
 # Package hello.zpkg archive