ci: add Idris2 proof gate; make Idris test suites fail-capable

.github/workflows/e2e.yml

@@ -1,4 +1,9 @@
 # SPDX-License-Identifier: MPL-2.0
+# The former "Integration tests" job here was a structural no-op: it ran
+# `cargo test` in a repo with no Cargo.toml and looped over
+# tests/integration/*.sh which never existed — always green, gating nothing.
+# Real integration coverage now lives in idris2.yml (Idris suites + the
+# Idris->Zig FFI runtime test) and zig-ffi.yml (C-ABI link + Zig tests).
 name: E2E and Integration Tests
 on:
   push: {branches: [main]}
@@ -14,19 +19,3 @@ jobs:
       - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
       - name: Run E2E tests
         run: bash tests/e2e_test.sh
-  integration:
-    name: Integration tests
-    runs-on: ubuntu-latest
-    timeout-minutes: 15
-    steps:
-      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
-      - name: Install Rust
-        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
-      - name: Run integration tests
-        run: |
-          if [ -f "Cargo.toml" ]; then
-            cargo test --test '*' 2>/dev/null || echo "No integration tests"
-          fi
-          if ls tests/integration/*.sh 2>/dev/null | head -1 | grep -q .; then
-            for f in tests/integration/*.sh; do bash "$f"; done
-          fi

.github/workflows/idris2.yml

@@ -0,0 +1,59 @@
+# SPDX-License-Identifier: MPL-2.0
+# Idris2 proof + test gate.
+#
+# This is the job that makes the proof ledger (docs/PROOFS.adoc) CI-enforced:
+# `idris2 --build ochrance.ipkg` type-checks all core modules under
+# `%default total` (opts = "--total" in the ipkg), so every theorem in
+# ochrance-core either machine-checks here or the build goes red. It then
+# runs the three Idris test suites and the Idris->Zig runtime FFI test
+# (tests/ffi/run_ffi_test.sh), which proves the production Merkle path
+# computes real BLAKE3 across the %foreign boundary.
+#
+# Toolchain: ghcr.io/stefan-hoeck/idris2-pack ships Idris 2 v0.8.0 (the
+# exact version this repo requires) + chezscheme/gcc/make. Digest-pinned;
+# bump deliberately, not via :latest drift.
+name: Idris2
+
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  idris2:
+    name: Idris2 proofs + tests
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    container:
+      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:7116e4fc2c68ff6345139a55d908e9dd1c7acabaf197c32e709deae3448dd7d7 # :latest @ 2026-07-01, Idris 2 v0.8.0
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+      - name: Set up Zig 0.15.2 (for the FFI runtime test)
+        uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
+        with:
+          version: 0.15.2
+      - name: Build core (type-checks all modules under --total)
+        run: idris2 --build ochrance.ipkg
+      - name: Install package (needed by the test ipkgs)
+        run: idris2 --install ochrance.ipkg
+      - name: A2ML parser tests
+        run: |
+          idris2 --build tests/A2ML/tests.ipkg
+          ./tests/A2ML/build/exec/a2ml-tests
+      - name: Property tests
+        run: |
+          idris2 --build tests/property/tests.ipkg
+          ./tests/property/build/exec/property-tests
+      - name: Integration tests
+        run: |
+          idris2 --build tests/integration/tests.ipkg
+          ./tests/integration/build/exec/integration-tests
+      - name: Idris -> Zig FFI runtime test (real BLAKE3 across %foreign)
+        run: bash tests/ffi/run_ffi_test.sh

tests/A2ML/ParserTests.idr

@@ -12,24 +12,32 @@ import Ochrance.A2ML.Lexer
 import Ochrance.A2ML.Parser
 import Ochrance.A2ML.Serializer
 import Ochrance.A2ML.Types
+import System
 
 %default total
 
 --------------------------------------------------------------------------------
 -- Test Helpers
 --------------------------------------------------------------------------------
 
+||| Report a failure and exit nonzero, so CI actually gates on this suite
+||| (fail-fast: the first failure ends the run with exit code 1).
+failWith : String -> IO ()
+failWith msg = do
+  putStrLn msg
+  exitFailure
+
 ||| Assert that a value is Right
 assertRight : Show e => Either e a -> IO ()
-assertRight (Left err) = putStrLn ("FAIL: " ++ show err)
+assertRight (Left err) = failWith ("FAIL: " ++ show err)
 assertRight (Right _) = pure ()
 
 ||| Assert two values are equal
 assertEqual : (Eq a, Show a) => a -> a -> IO ()
 assertEqual expected actual =
   if expected == actual
      then pure ()
-     else putStrLn ("FAIL: Expected " ++ show expected ++ ", got " ++ show actual)
+     else failWith ("FAIL: Expected " ++ show expected ++ ", got " ++ show actual)
 
 ||| Test case wrapper
 testCase : String -> IO () -> IO ()
@@ -107,27 +115,27 @@ lexerTests = do
   testCase "Lex empty string" $ do
     case lex "" of
       Right tokens => assertEqual [EOF] tokens
-      Left err => putStrLn ("FAIL: " ++ show err)
+      Left err => failWith ("FAIL: " ++ show err)
 
   testCase "Lex minimal manifest" $ do
     case lex minimalManifest of
       Right tokens => pure ()  -- Success if no error
-      Left err => putStrLn ("FAIL: " ++ show err)
+      Left err => failWith ("FAIL: " ++ show err)
 
   testCase "Lex with attestation" $ do
     case lex attestedManifest of
       Right tokens => pure ()
-      Left err => putStrLn ("FAIL: " ++ show err)
+      Left err => failWith ("FAIL: " ++ show err)
 
   testCase "Lex with policy" $ do
     case lex policyManifest of
       Right tokens => pure ()
-      Left err => putStrLn ("FAIL: " ++ show err)
+      Left err => failWith ("FAIL: " ++ show err)
 
   testCase "Lex rejects invalid characters" $ do
     case lex "@manifest { version = \x00 }" of
       Left _ => pure ()  -- Should fail
-      Right _ => putStrLn "FAIL: Should reject null bytes"
+      Right _ => failWith "FAIL: Should reject null bytes"
 
 --------------------------------------------------------------------------------
 -- Parser Tests
@@ -145,44 +153,44 @@ parserTests = do
           Right manifest => do
             assertEqual "0.1.0" manifest.manifestData.version
             assertEqual "test" manifest.manifestData.subsystem
-          Left err => putStrLn ("FAIL: " ++ show err)
-      Left err => putStrLn ("FAIL lex: " ++ show err)
+          Left err => failWith ("FAIL: " ++ show err)
+      Left err => failWith ("FAIL lex: " ++ show err)
 
   testCase "Parse attested manifest" $ do
     case lex attestedManifest of
       Right tokens =>
         case parse tokens of
           Right manifest => do
             case manifest.attestation of
-              Nothing => putStrLn "FAIL: Expected attestation"
+              Nothing => failWith "FAIL: Expected attestation"
               Just att => do
                 assertEqual "test-witness" att.witness
                 assertEqual "sig123" att.signature
-          Left err => putStrLn ("FAIL: " ++ show err)
-      Left err => putStrLn ("FAIL lex: " ++ show err)
+          Left err => failWith ("FAIL: " ++ show err)
+      Left err => failWith ("FAIL lex: " ++ show err)
 
   testCase "Parse policy manifest" $ do
     case lex policyManifest of
       Right tokens =>
         case parse tokens of
           Right manifest => do
             case manifest.policy of
-              Nothing => putStrLn "FAIL: Expected policy"
+              Nothing => failWith "FAIL: Expected policy"
               Just pol => do
                 assertEqual Checked pol.mode
                 case pol.maxAge of
-                  Nothing => putStrLn "FAIL: Expected max_age"
+                  Nothing => failWith "FAIL: Expected max_age"
                   Just age => assertEqual 3600 age
-          Left err => putStrLn ("FAIL: " ++ show err)
-      Left err => putStrLn ("FAIL lex: " ++ show err)
+          Left err => failWith ("FAIL: " ++ show err)
+      Left err => failWith ("FAIL lex: " ++ show err)
 
   testCase "Parse rejects duplicate sections" $ do
     let duplicateManifest = minimalManifest ++ "\n@manifest { version = \"0.2.0\" }\n"
     case lex duplicateManifest of
       Right tokens =>
         case parse tokens of
           Left _ => pure ()  -- Should fail
-          Right _ => putStrLn "FAIL: Should reject duplicate sections"
+          Right _ => failWith "FAIL: Should reject duplicate sections"
       Left _ => pure ()  -- Lex error also acceptable
 
 --------------------------------------------------------------------------------
@@ -206,10 +214,10 @@ roundtripTests = do
                   Right manifest2 => do
                     assertEqual manifest1.manifestData.version manifest2.manifestData.version
                     assertEqual manifest1.manifestData.subsystem manifest2.manifestData.subsystem
-                  Left err => putStrLn ("FAIL parse2: " ++ show err)
-              Left err => putStrLn ("FAIL lex2: " ++ show err)
-          Left err => putStrLn ("FAIL parse1: " ++ show err)
-      Left err => putStrLn ("FAIL lex1: " ++ show err)
+                  Left err => failWith ("FAIL parse2: " ++ show err)
+              Left err => failWith ("FAIL lex2: " ++ show err)
+          Left err => failWith ("FAIL parse1: " ++ show err)
+      Left err => failWith ("FAIL lex1: " ++ show err)
 
 --------------------------------------------------------------------------------
 -- Error Handling Tests
@@ -226,7 +234,7 @@ errorHandlingTests = do
       Right tokens =>
         case parse tokens of
           Left _ => pure ()  -- Should fail
-          Right _ => putStrLn "FAIL: Should require version field"
+          Right _ => failWith "FAIL: Should require version field"
       Left _ => pure ()  -- Lex error also acceptable
 
   testCase "Invalid hash format" $ do
@@ -235,14 +243,14 @@ errorHandlingTests = do
       Right tokens =>
         case parse tokens of
           Left _ => pure ()  -- Should fail
-          Right _ => putStrLn "FAIL: Should reject invalid hash format"
+          Right _ => failWith "FAIL: Should reject invalid hash format"
       Left _ => pure ()  -- Lex error also acceptable
 
   testCase "Unterminated string" $ do
     let invalid = "@manifest { version = \"unterminated }"
     case lex invalid of
       Left _ => pure ()  -- Should fail at lex stage
-      Right _ => putStrLn "FAIL: Should reject unterminated string"
+      Right _ => failWith "FAIL: Should reject unterminated string"
 
 --------------------------------------------------------------------------------
 -- Main Test Runner

tests/e2e_test.sh

@@ -90,7 +90,7 @@ assert "build.zig configures library" \
 assert "build.zig emits libochrance.so (no stale 'ochrance-shared' name)" \
     "$(! grep -q "ochrance-shared" "$BASE/ffi/zig/build.zig" && echo 0 || echo 1)"
 assert "build.zig builds a shared library" \
-    "$(grep -q "addSharedLibrary" "$BASE/ffi/zig/build.zig" && echo 0 || echo 1)"
+    "$(grep -q 'linkage = .dynamic' "$BASE/ffi/zig/build.zig" && echo 0 || echo 1)"
 
 # ================================================================
 # E2E: Test coverage completeness

tests/integration/IntegrationTests.idr

@@ -9,6 +9,7 @@
 
 module IntegrationTests
 
+import System
 import Data.Vect
 import Ochrance.A2ML.Types
 import Ochrance.A2ML.Lexer
@@ -35,12 +36,16 @@ Show TestResult where
   show Pass = "PASS"
   show (Fail msg) = "FAIL: " ++ msg
 
-||| Test case wrapper
+||| Test case wrapper. Fail-fast: a failing case ends the run with exit
+||| code 1, so CI actually gates on this suite instead of always going green.
 testCase : String -> IO TestResult -> IO ()
 testCase name test = do
   putStr (name ++ " ... ")
   result <- test
   putStrLn (show result)
+  case result of
+    Fail _ => exitFailure
+    Pass   => pure ()
 
 ||| Create a test filesystem state
 createTestFS : Nat -> FSState

tests/property/PropertyTests.idr

@@ -14,6 +14,7 @@
 
 module PropertyTests
 
+import System
 import Data.Vect
 import Data.List
 import Data.Bits
@@ -520,3 +521,6 @@ main = do
          ++ show totalCount ++ " passed, "
          ++ show totalFailed ++ " failed")
   putStrLn "==========================================="
+
+  -- Gate: nonzero exit on any failure, so CI actually enforces this suite
+  when (totalFailed > 0) exitFailure