ci: make CI genuinely green — rust-ci toolchain pin + canonical Julia ABI-FFI gate (#77)

* feat(abi): prove Conformant scaffold property (Layer 2 Semantics)

Add Iseriser.ABI.Semantics proving the headline domain property: a
generated -iser scaffold is Conformant exactly when all five required
components (Manifest, Idris2 ABI, Zig FFI, Codegen, Rust CLI) are
present. Conformant is built from genuine Data.List.Elem membership
obligations with no catch-all constructor, so a scaffold missing any
component has no witness.

Includes a sound+complete decConformant : (s) -> Dec (Conformant s),
a soundness fact certifyConformantSound, a positive control
(completeIsConformant via explicit Elem positions), and a negative
control (ffiMissingNotConformant : Not (Conformant ffiMissing)).
Non-vacuity confirmed: a deliberately-false Has Ffi witness for the
FFI-missing scaffold is rejected by idris2.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* abi: add Layer-3 Invariants (generation soundness + conformance closure)

Add Iseriser.ABI.Invariants over the existing Layer-2 Semantics model
(Component/Scaffold/Has/Conformant). Two new, deeper, distinct theorems:

  1. Generation soundness (correct-by-construction): genScaffold provably
     emits (s ** Conformant s) for any LanguageModel, with a corollary
     tying it back to the Layer-2 certifier (conformantCertifies).
  2. Upward-closure / monotonicity: conformantStable proves Conformance is
     preserved under extension, via a genuine Elem-weakening lemma
     (elemAppendRight) — an algebraic closure law, not the Layer-2 decision.

Includes a sound+complete Dec (decExtendConformant), a positive control
(extendedGeneratedConformant) and a non-vacuity negative control
(extendedBrokenNotConformant : Not ...). Builds clean with zero warnings;
adversarial false proof rejected. No believe_me/postulate/assert_total.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* abi: seal ABI<->FFI seam with Layer-4 soundness proof (FfiSeam)

Add Iseriser.ABI.FfiSeam proving the resultToInt encoding is sound:
- intToResult decoder + resultRoundTrip (lossless/faithful encoding)
- resultToIntInjective derived from round-trip (distinct outcomes never
  collide on the wire)
- positive controls (concrete decodes by Refl) and a machine-checked
  non-vacuity control (resultToInt Ok /= resultToInt Error)

Genuine total proof: no believe_me/postulate/assert_total/etc. Registered
in iseriser-abi.ipkg; package builds clean with zero warnings.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* abi(iseriser): add Layer-5 capstone ABI soundness certificate

Assemble the existing Layer-2/3/4 ABI proofs into one inhabited value,
Iseriser.ABI.Capstone.abiContractDischarged : ABISound, with fields:
  - flagship     : Conformant Semantics.completeScaffold
                   (reuses Semantics.completeIsConformant)
  - invariant    : Conformant (extend [Manifest] generatedScaffold)
                   (reuses Invariants.extendedGeneratedConformant)
  - ffiInjective : resultToInt injectivity
                   (reuses FfiSeam.resultToIntInjective)

Pure composition of already-exported witnesses: if any prior layer were
unsound the capstone would not typecheck. Adversarial check confirms a
wrong-type witness in the flagship slot is rejected. %default total, SPDX,
zero warnings. ipkg updated (Capstone listed last).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* ci: make CI green — bump rust-ci to standards@8dc2bf0 (toolchain: stable fix); port ABI-FFI gate Python->Bash (Python is estate-banned)

Resolves the standing baseline CI reds (rust-ci toolchain error, governance
Language/anti-pattern, governance workflow-lint) without altering the proven
ABI. The Bash gate reproduces the former Python gate's verdict verbatim
(validated across all -iser repos) and catches the same drift classes.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* ci: adopt canonical Julia ABI-FFI gate (estate standard, matches verisimiser) in place of the interim Bash port

---------

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

Author: hyperpolymath

.github/workflows/abi-ffi-gate.yml

@@ -21,8 +21,15 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
+      - name: Install Julia 1.11.5
+        run: |
+          curl -fsSL https://julialang-s3.julialang.org/bin/linux/x64/1.11/julia-1.11.5-linux-x86_64.tar.gz -o /tmp/julia.tar.gz
+          tar -xf /tmp/julia.tar.gz -C /tmp
+          echo "/tmp/julia-1.11.5/bin" >> "$GITHUB_PATH"
       - name: Run ABI-FFI gate
-        run: python3 scripts/abi-ffi-gate.py
+        run: |
+          julia --version   # confirms the pinned 1.11.5 is on PATH, not the runner default
+          julia scripts/abi-ffi-gate.jl
 
   zig-build:
     name: Zig FFI builds + tests (Zig 0.14.0)

.github/workflows/rust-ci.yml

@@ -14,4 +14,4 @@ permissions:
 
 jobs:
   rust-ci:
-    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236
+    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@8dc2bf039d1ff0372d650895c46bea7fbaec68ff

scripts/abi-ffi-gate.jl

@@ -0,0 +1,116 @@
+#!/usr/bin/env julia
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# abi-ffi-gate.jl — 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 compile toolchain
+# needed (pure base-Julia text analysis):
+#
+#   1. the Zig FFI carries no unrendered `{{...}}` template tokens;
+#   2. every `%foreign "C:<name>"` symbol declared anywhere in the ABI .idr
+#      sources is exported by the Zig FFI (`export fn <name>`);
+#   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: julia scripts/abi-ffi-gate.jl [repo_root]   (defaults to cwd)
+#
+# Julia port of the former scripts/abi-ffi-gate.py (Python is banned estate-wide,
+# RSR-H4); behaviour is identical.
+
+"camelCase / PascalCase → snake_case (insert `_` before each non-initial capital)."
+camel_to_snake(s) = lowercase(replace(s, r"(?<!^)(?=[A-Z])" => "_"))
+
+"Canonical result-code key: lowercased, with `err`/`error` unified to `error`."
+function canon_rc(name)
+    n = lowercase(name)
+    (n == "err" || n == "error") ? "error" : n
+end
+
+"Return {variant => value} for the C-ABI `Result` enum (the `enum(c_int)` block whose `ok = 0`), or empty."
+function find_result_enum(zig::AbstractString)
+    best = Dict{String,Int}()
+    for m in eachmatch(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}"s, zig)
+        body = m.captures[1]
+        variants = Dict{String,Int}()
+        for vm in eachmatch(r"@?\"?([A-Za-z_][A-Za-z0-9_]*)\"?\s*=\s*(\d+)", body)
+            variants[canon_rc(vm.captures[1])] = parse(Int, vm.captures[2])
+        end
+        # The Result enum is the one starting at ok = 0.
+        if get(variants, "ok", nothing) == 0 && length(variants) > length(best)
+            best = variants
+        end
+    end
+    return best
+end
+
+"Collect every `*.idr` under `abi_dir`, skipping any `build/` output directory."
+function idr_sources(abi_dir::AbstractString)
+    files = String[]
+    isdir(abi_dir) || return files
+    for (root, _dirs, fs) in walkdir(abi_dir)
+        occursin("/build/", root * "/") && continue
+        for f in fs
+            endswith(f, ".idr") && push!(files, joinpath(root, f))
+        end
+    end
+    return files
+end
+
+function main(root::AbstractString)::Int
+    name = basename(rstrip(abspath(root), '/'))
+    abi_dir = joinpath(root, "src/interface/abi")
+    zig_path = joinpath(root, "src/interface/ffi/src/main.zig")
+    errs = String[]
+
+    idr_files = idr_sources(abi_dir)
+    if isempty(idr_files)
+        println("ABI-FFI GATE: SKIP ($name) — no Idris2 ABI .idr files under $abi_dir")
+        return 0
+    end
+    if !isfile(zig_path)
+        println("ABI-FFI GATE: FAIL ($name) — no Zig FFI at $zig_path")
+        return 1
+    end
+
+    idr = join((read(p, String) for p in idr_files), "\n")
+    zig = read(zig_path, String)
+
+    # 1. unrendered template tokens
+    toks = sort(unique(String(m.match) for m in eachmatch(r"\{\{[A-Za-z0-9_]+\}\}", zig)))
+    isempty(toks) || push!(errs, "Zig FFI has unrendered template tokens: $(toks)")
+
+    # 2. foreign C symbols must be exported
+    csyms = sort(unique(String(m.captures[1]) for m in eachmatch(r"C:([A-Za-z0-9_]+)", idr)))
+    exports = Set(String(m.captures[1]) for m in eachmatch(r"export fn ([A-Za-z0-9_]+)", zig))
+    missing_syms = [s for s in csyms if !(s in exports)]
+    isempty(missing_syms) ||
+        push!(errs, "$(length(missing_syms)) ABI function(s) not exported by the Zig FFI: $(missing_syms)")
+
+    # 3. result-code map (names + values) must agree
+    idr_rc = Dict{String,Int}()
+    for m in eachmatch(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr)
+        idr_rc[canon_rc(camel_to_snake(m.captures[1]))] = parse(Int, m.captures[2])
+    end
+    zig_rc = find_result_enum(zig)
+    if !isempty(idr_rc) && isempty(zig_rc)
+        push!(errs, "no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes")
+    elseif !isempty(idr_rc) && !isempty(zig_rc) && idr_rc != zig_rc
+        push!(errs, "Result-code map differs (name or value):\n" *
+                    "      Idris resultToInt: $(sort(collect(idr_rc)))\n" *
+                    "      Zig   Result enum: $(sort(collect(zig_rc)))")
+    end
+
+    if !isempty(errs)
+        println("ABI-FFI GATE: FAIL ($name)")
+        for e in errs
+            println("  - " * e)
+        end
+        return 1
+    end
+    println("ABI-FFI GATE: OK ($name) — $(length(csyms)) ABI functions exported, " *
+            "$(length(idr_rc)) result codes match")
+    return 0
+end
+
+root = length(ARGS) >= 1 ? ARGS[1] : "."
+exit(main(root))