verisimiser: make ABI/FFI/codegen provably-real + honest docs

.github/workflows/provable.yml

@@ -0,0 +1,112 @@
+# SPDX-License-Identifier: MPL-2.0
+# Provable — machine-checks the claims VeriSimiser makes outside the Rust layer.
+#
+# The Rust CLI/codegen is covered by rust-ci.yml (fmt + clippy + test). This
+# workflow verifies the four things that are otherwise only asserted in prose:
+#   1. idris2-proofs  — the Idris2 ABI proofs actually type-check (`idris2 --check`).
+#   2. zig-ffi        — the Zig FFI reference impl builds and its tests pass.
+#   3. codegen-drift  — the committed golden sample matches fresh codegen output.
+#   4. sql-golden     — the generated overlay SQL actually applies to a real
+#                       SQLite database and every table/view builds and queries.
+#
+# Until every job here is green, the proofs / FFI / generated SQL are "written"
+# but NOT "verified" — ROADMAP.adoc and README.adoc are worded accordingly.
+name: Provable
+
+on:
+  push:
+    branches: [main, master, "claude/**"]
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  idris2-proofs:
+    name: Idris2 — machine-check ABI proofs
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    container: ghcr.io/stefan-hoeck/idris2-pack:latest
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - name: idris2 build the ABI package (Types, Layout, Proofs, Foreign)
+        working-directory: src/interface/abi
+        # Modules are namespaced Verisimiser.ABI.* under Verisimiser/ABI/.
+        # Building the .ipkg type-checks every module in the package — including
+        # Proofs.idr, which carries the machine-checked C-ABI / layout theorems —
+        # in one invocation, which is also the canonical command in the .ipkg.
+        run: |
+          idris2 --version
+          idris2 --build verisimiser-abi.ipkg
+
+  zig-ffi:
+    name: Zig — build + test FFI reference impl
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - uses: mlugg/setup-zig@53fc45b17fe98b52f92ee5ea08ff48a85a3e7eb7 # v1.2.2
+        with:
+          version: 0.14.0
+      - name: zig build + test
+        working-directory: src/interface/ffi
+        # `zig build test` runs the 8 in-module unit tests AND the 35 C-ABI
+        # integration tests (which link the compiled libverisimiser.so).
+        run: |
+          zig version
+          zig build test
+          zig build
+
+  codegen-drift:
+    name: Codegen — golden sample is up to date
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - name: Regenerate golden artifacts and diff against committed tree
+        run: |
+          # retry: fresh runners occasionally flake fetching crates from crates.io
+          built=0
+          for i in 1 2 3; do
+            cargo build --quiet && { built=1; break; }
+            echo "build attempt $i failed; retrying after backoff…"; sleep $((i * 5))
+          done
+          [ "$built" = 1 ] || { echo "cargo build failed after retries"; exit 1; }
+          ( cd examples/golden && ../../target/debug/verisimiser generate -m verisimiser.toml -o /tmp/golden )
+          diff -ru examples/golden/generated /tmp/golden
+
+  sql-golden:
+    name: SQLite — generated overlay applies and views build
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - name: Ensure sqlite3 is available
+        run: sudo apt-get update && sudo apt-get install -y sqlite3
+      - name: Apply schema + generated overlay + interceptors into a fresh SQLite DB
+        run: |
+          sqlite3 --version
+          DB="$(mktemp -d)/golden.db"
+          sqlite3 "$DB" < examples/golden/schema.sql
+          sqlite3 "$DB" < examples/golden/generated/sidecar_schema.sql
+          sqlite3 "$DB" < examples/golden/generated/interceptors.sql
+
+          # Every enabled octad dimension must have produced its sidecar table.
+          for t in verisimdb_metadata verisimdb_provenance_log \
+                   verisimdb_lineage_graph verisimdb_temporal_versions \
+                   verisimdb_access_policies; do
+            sqlite3 "$DB" "SELECT name FROM sqlite_master WHERE type='table' AND name='$t';" \
+              | grep -qx "$t" || { echo "missing sidecar table: $t"; exit 1; }
+          done
+
+          # Every target table must have provenance + temporal enrichment views,
+          # and each view must be queryable (catches invalid SQL in view bodies).
+          for v in verisimdb_users_with_provenance verisimdb_users_with_temporal \
+                   verisimdb_posts_with_provenance verisimdb_posts_with_temporal; do
+            sqlite3 "$DB" "SELECT name FROM sqlite_master WHERE type='view' AND name='$v';" \
+              | grep -qx "$v" || { echo "missing enrichment view: $v"; exit 1; }
+            sqlite3 "$DB" "SELECT count(*) FROM $v;" >/dev/null \
+              || { echo "view not queryable: $v"; exit 1; }
+          done
+
+          echo "Generated overlay applied cleanly; all sidecar tables + views present and queryable."

examples/golden/README.adoc

@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: MPL-2.0
+= VeriSimiser Codegen Golden Sample
+:toc: macro
+:source-highlighter: rouge
+
+This directory is the *frozen golden sample* that the `codegen-drift` and
+`sql-golden` jobs of `.github/workflows/provable.yml` check on every push and
+pull request. It exists to turn "the generator produces correct SQL" from a
+prose claim into a machine-checked fact.
+
+toc::[]
+
+== What's here
+
+[cols="1,3"]
+|===
+| File | Role
+
+| `verisimiser.toml`
+| Frozen input manifest (SQLite backend, 7 of 8 octad dimensions enabled).
+
+| `schema.sql`
+| Frozen input schema — two tables (`users`, `posts`) with a typical author
+  relationship and a spread of column types.
+
+| `generated/sidecar_schema.sql`
+| Committed expected output: the octad sidecar overlay DDL.
+
+| `generated/interceptors.sql`
+| Committed expected output: the per-table provenance/temporal enrichment
+  views and lineage/access-control query templates.
+|===
+
+== What the CI checks
+
+`codegen-drift`:: regenerates `generated/` from `verisimiser.toml` + `schema.sql`
+into a temp directory and `diff`s it against the committed tree. The generator
+is deterministic, so any difference fails the job — this catches *unintended*
+changes to codegen output.
+
+`sql-golden`:: applies `schema.sql`, then the two generated files, into a fresh
+SQLite database and asserts every sidecar table and enrichment view is created
+and queryable. This is the SQL analogue of "the generated code compiles and
+runs": it proves the emitted DDL is valid and applies cleanly against the
+target schema (the views use `ROW_NUMBER() OVER (…)`, so SQLite >= 3.25).
+
+== Regenerating after an intentional codegen change
+
+If you change the generator and the new output is correct, refresh the golden
+in the *same* PR as the code change:
+
+[source,sh]
+----
+cargo build
+( cd examples/golden && ../../target/debug/verisimiser generate -m verisimiser.toml -o generated )
+git add examples/golden/generated
+----
+
+Then review the diff carefully — it is the human-readable record of how your
+change affected every consumer's generated overlay.

examples/golden/generated/interceptors.sql

@@ -0,0 +1,145 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- VeriSimiser query interceptors (auto-generated)
+
+-- ==========================================================
+-- Table: users
+-- ==========================================================
+
+-- Provenance-enriched view for 'users'
+-- Joins each row with its latest provenance entry from the sidecar.
+CREATE VIEW IF NOT EXISTS verisimdb_users_with_provenance AS
+SELECT
+    users.id,
+    users.username,
+    users.email,
+    users.created_at,
+    prov.operation   AS _verisimdb_last_operation,
+    prov.actor       AS _verisimdb_last_actor,
+    prov.timestamp   AS _verisimdb_last_modified,
+    prov.hash        AS _verisimdb_provenance_hash
+FROM users
+LEFT JOIN (
+    SELECT entity_id, operation, actor, timestamp, hash
+    FROM (
+        SELECT entity_id, operation, actor, timestamp, hash,
+               ROW_NUMBER() OVER (PARTITION BY entity_id ORDER BY timestamp DESC) AS _rn
+        FROM verisimdb_provenance_log
+        WHERE table_name = 'users'
+    ) ranked
+    WHERE _rn = 1
+) prov ON prov.entity_id = (CAST(users.id AS TEXT));
+
+-- Temporal-enriched view for 'users'
+-- Joins each row with its current version metadata.
+CREATE VIEW IF NOT EXISTS verisimdb_users_with_temporal AS
+SELECT
+    users.id,
+    users.username,
+    users.email,
+    users.created_at,
+    tv.version    AS _verisimdb_version,
+    tv.valid_from AS _verisimdb_valid_from,
+    tv.operation  AS _verisimdb_version_operation
+FROM users
+LEFT JOIN verisimdb_temporal_versions tv
+    ON tv.entity_id = (CAST(users.id AS TEXT))
+    AND tv.table_name = 'users'
+    AND tv.valid_to IS NULL;
+
+-- Lineage queries for 'users'
+
+-- Upstream: what data was this entity derived from?
+-- SELECT * FROM verisimdb_lineage_graph
+-- WHERE target_entity = :entity_id AND target_table = 'users';
+
+-- Downstream: what entities depend on this entity?
+-- SELECT * FROM verisimdb_lineage_graph
+-- WHERE source_entity = :entity_id AND source_table = 'users';
+
+-- Access control filter for 'users'
+-- Apply this as a WHERE clause addition to enforce row-level security.
+--
+-- Example usage (parameterised):
+-- SELECT * FROM users
+-- WHERE ... AND EXISTS (
+--     SELECT 1 FROM verisimdb_access_policies
+--     WHERE target_table = 'users'
+--     AND principal = :current_principal
+--     AND access_level IN ('read', 'admin')
+--     AND active = 1
+--     AND (condition IS NULL OR :row_matches_condition)
+-- );
+
+-- ==========================================================
+-- Table: posts
+-- ==========================================================
+
+-- Provenance-enriched view for 'posts'
+-- Joins each row with its latest provenance entry from the sidecar.
+CREATE VIEW IF NOT EXISTS verisimdb_posts_with_provenance AS
+SELECT
+    posts.id,
+    posts.author_id,
+    posts.title,
+    posts.body,
+    posts.published,
+    posts.created_at,
+    prov.operation   AS _verisimdb_last_operation,
+    prov.actor       AS _verisimdb_last_actor,
+    prov.timestamp   AS _verisimdb_last_modified,
+    prov.hash        AS _verisimdb_provenance_hash
+FROM posts
+LEFT JOIN (
+    SELECT entity_id, operation, actor, timestamp, hash
+    FROM (
+        SELECT entity_id, operation, actor, timestamp, hash,
+               ROW_NUMBER() OVER (PARTITION BY entity_id ORDER BY timestamp DESC) AS _rn
+        FROM verisimdb_provenance_log
+        WHERE table_name = 'posts'
+    ) ranked
+    WHERE _rn = 1
+) prov ON prov.entity_id = (CAST(posts.id AS TEXT));
+
+-- Temporal-enriched view for 'posts'
+-- Joins each row with its current version metadata.
+CREATE VIEW IF NOT EXISTS verisimdb_posts_with_temporal AS
+SELECT
+    posts.id,
+    posts.author_id,
+    posts.title,
+    posts.body,
+    posts.published,
+    posts.created_at,
+    tv.version    AS _verisimdb_version,
+    tv.valid_from AS _verisimdb_valid_from,
+    tv.operation  AS _verisimdb_version_operation
+FROM posts
+LEFT JOIN verisimdb_temporal_versions tv
+    ON tv.entity_id = (CAST(posts.id AS TEXT))
+    AND tv.table_name = 'posts'
+    AND tv.valid_to IS NULL;
+
+-- Lineage queries for 'posts'
+
+-- Upstream: what data was this entity derived from?
+-- SELECT * FROM verisimdb_lineage_graph
+-- WHERE target_entity = :entity_id AND target_table = 'posts';
+
+-- Downstream: what entities depend on this entity?
+-- SELECT * FROM verisimdb_lineage_graph
+-- WHERE source_entity = :entity_id AND source_table = 'posts';
+
+-- Access control filter for 'posts'
+-- Apply this as a WHERE clause addition to enforce row-level security.
+--
+-- Example usage (parameterised):
+-- SELECT * FROM posts
+-- WHERE ... AND EXISTS (
+--     SELECT 1 FROM verisimdb_access_policies
+--     WHERE target_table = 'posts'
+--     AND principal = :current_principal
+--     AND access_level IN ('read', 'admin')
+--     AND active = 1
+--     AND (condition IS NULL OR :row_matches_condition)
+-- );
+