diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index b46b83d..3539cd2 100644 --- a/.github/workflows/e2e.yml +++ b/.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 diff --git a/.github/workflows/idris2.yml b/.github/workflows/idris2.yml new file mode 100644 index 0000000..07ad893 --- /dev/null +++ b/.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 diff --git a/tests/A2ML/ParserTests.idr b/tests/A2ML/ParserTests.idr index e799e72..476957c 100644 --- a/tests/A2ML/ParserTests.idr +++ b/tests/A2ML/ParserTests.idr @@ -12,6 +12,7 @@ import Ochrance.A2ML.Lexer import Ochrance.A2ML.Parser import Ochrance.A2ML.Serializer import Ochrance.A2ML.Types +import System %default total @@ -19,9 +20,16 @@ import Ochrance.A2ML.Types -- 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 @@ -29,7 +37,7 @@ 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,8 +153,8 @@ 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 @@ -154,12 +162,12 @@ parserTests = do 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 @@ -167,14 +175,14 @@ parserTests = do 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" @@ -182,7 +190,7 @@ parserTests = do 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 diff --git a/tests/e2e_test.sh b/tests/e2e_test.sh index 1ade37e..8838a70 100644 --- a/tests/e2e_test.sh +++ b/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 diff --git a/tests/integration/IntegrationTests.idr b/tests/integration/IntegrationTests.idr index 52817d1..8782442 100644 --- a/tests/integration/IntegrationTests.idr +++ b/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 diff --git a/tests/property/PropertyTests.idr b/tests/property/PropertyTests.idr index 1127808..96ea245 100644 --- a/tests/property/PropertyTests.idr +++ b/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