|
| 1 | +# SPDX-License-Identifier: MPL-2.0 |
| 2 | +# Provable — machine-checks the claims VeriSimiser makes outside the Rust layer. |
| 3 | +# |
| 4 | +# The Rust CLI/codegen is covered by rust-ci.yml (fmt + clippy + test). This |
| 5 | +# workflow verifies the four things that are otherwise only asserted in prose: |
| 6 | +# 1. idris2-proofs — the Idris2 ABI proofs actually type-check (`idris2 --check`). |
| 7 | +# 2. zig-ffi — the Zig FFI reference impl builds and its tests pass. |
| 8 | +# 3. codegen-drift — the committed golden sample matches fresh codegen output. |
| 9 | +# 4. sql-golden — the generated overlay SQL actually applies to a real |
| 10 | +# SQLite database and every table/view builds and queries. |
| 11 | +# |
| 12 | +# Until every job here is green, the proofs / FFI / generated SQL are "written" |
| 13 | +# but NOT "verified" — ROADMAP.adoc and README.adoc are worded accordingly. |
| 14 | +name: Provable |
| 15 | + |
| 16 | +on: |
| 17 | + push: |
| 18 | + branches: [main, master, "claude/**"] |
| 19 | + pull_request: |
| 20 | + |
| 21 | +permissions: |
| 22 | + contents: read |
| 23 | + |
| 24 | +jobs: |
| 25 | + idris2-proofs: |
| 26 | + name: Idris2 — machine-check ABI proofs |
| 27 | + runs-on: ubuntu-latest |
| 28 | + timeout-minutes: 20 |
| 29 | + container: ghcr.io/stefan-hoeck/idris2-pack:latest |
| 30 | + steps: |
| 31 | + - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 |
| 32 | + - name: idris2 --check the ABI modules |
| 33 | + working-directory: src/interface/abi |
| 34 | + # Modules are namespaced Verisimiser.ABI.*, so they live under |
| 35 | + # Verisimiser/ABI/ (idris2 requires the file path to match the module |
| 36 | + # name). Foreign imports Types + Layout, so checking it checks the lot; |
| 37 | + # we check each explicitly for clearer failure attribution. |
| 38 | + run: | |
| 39 | + idris2 --version |
| 40 | + idris2 --check Verisimiser/ABI/Types.idr |
| 41 | + idris2 --check Verisimiser/ABI/Layout.idr |
| 42 | + idris2 --check Verisimiser/ABI/Foreign.idr |
| 43 | +
|
| 44 | + zig-ffi: |
| 45 | + name: Zig — build + test FFI reference impl |
| 46 | + runs-on: ubuntu-latest |
| 47 | + timeout-minutes: 15 |
| 48 | + steps: |
| 49 | + - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 |
| 50 | + - uses: mlugg/setup-zig@53fc45b17fe98b52f92ee5ea08ff48a85a3e7eb7 # v1.2.2 |
| 51 | + with: |
| 52 | + version: 0.14.0 |
| 53 | + - name: zig build + test |
| 54 | + working-directory: src/interface/ffi |
| 55 | + # `zig build test` runs the 8 in-module unit tests AND the 35 C-ABI |
| 56 | + # integration tests (which link the compiled libverisimiser.so). |
| 57 | + run: | |
| 58 | + zig version |
| 59 | + zig build test |
| 60 | + zig build |
| 61 | +
|
| 62 | + codegen-drift: |
| 63 | + name: Codegen — golden sample is up to date |
| 64 | + runs-on: ubuntu-latest |
| 65 | + timeout-minutes: 15 |
| 66 | + steps: |
| 67 | + - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 |
| 68 | + - name: Regenerate golden artifacts and diff against committed tree |
| 69 | + run: | |
| 70 | + # retry: fresh runners occasionally flake fetching crates from crates.io |
| 71 | + built=0 |
| 72 | + for i in 1 2 3; do |
| 73 | + cargo build --quiet && { built=1; break; } |
| 74 | + echo "build attempt $i failed; retrying after backoff…"; sleep $((i * 5)) |
| 75 | + done |
| 76 | + [ "$built" = 1 ] || { echo "cargo build failed after retries"; exit 1; } |
| 77 | + ( cd examples/golden && ../../target/debug/verisimiser generate -m verisimiser.toml -o /tmp/golden ) |
| 78 | + diff -ru examples/golden/generated /tmp/golden |
| 79 | +
|
| 80 | + sql-golden: |
| 81 | + name: SQLite — generated overlay applies and views build |
| 82 | + runs-on: ubuntu-latest |
| 83 | + timeout-minutes: 10 |
| 84 | + steps: |
| 85 | + - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 |
| 86 | + - name: Ensure sqlite3 is available |
| 87 | + run: sudo apt-get update && sudo apt-get install -y sqlite3 |
| 88 | + - name: Apply schema + generated overlay + interceptors into a fresh SQLite DB |
| 89 | + run: | |
| 90 | + sqlite3 --version |
| 91 | + DB="$(mktemp -d)/golden.db" |
| 92 | + sqlite3 "$DB" < examples/golden/schema.sql |
| 93 | + sqlite3 "$DB" < examples/golden/generated/sidecar_schema.sql |
| 94 | + sqlite3 "$DB" < examples/golden/generated/interceptors.sql |
| 95 | +
|
| 96 | + # Every enabled octad dimension must have produced its sidecar table. |
| 97 | + for t in verisimdb_metadata verisimdb_provenance_log \ |
| 98 | + verisimdb_lineage_graph verisimdb_temporal_versions \ |
| 99 | + verisimdb_access_policies; do |
| 100 | + sqlite3 "$DB" "SELECT name FROM sqlite_master WHERE type='table' AND name='$t';" \ |
| 101 | + | grep -qx "$t" || { echo "missing sidecar table: $t"; exit 1; } |
| 102 | + done |
| 103 | +
|
| 104 | + # Every target table must have provenance + temporal enrichment views, |
| 105 | + # and each view must be queryable (catches invalid SQL in view bodies). |
| 106 | + for v in verisimdb_users_with_provenance verisimdb_users_with_temporal \ |
| 107 | + verisimdb_posts_with_provenance verisimdb_posts_with_temporal; do |
| 108 | + sqlite3 "$DB" "SELECT name FROM sqlite_master WHERE type='view' AND name='$v';" \ |
| 109 | + | grep -qx "$v" || { echo "missing enrichment view: $v"; exit 1; } |
| 110 | + sqlite3 "$DB" "SELECT count(*) FROM $v;" >/dev/null \ |
| 111 | + || { echo "view not queryable: $v"; exit 1; } |
| 112 | + done |
| 113 | +
|
| 114 | + echo "Generated overlay applied cleanly; all sidecar tables + views present and queryable." |
0 commit comments