Commit b792eac
committed
feat(verify): provable CI for the type-checker + render the Zig FFI
Slice 3 — propagate the chapeliser "provably-real + honest" pattern to
typedqliser (the #1 -iser priority).
Provable — add .github/workflows/provable.yml:
- golden-check: the SQL type-checker ACCEPTS valid queries and REJECTS
invalid ones (blog-api example; verified locally — good pass, bad fail
at L1/L2/L3). The headline value, machine-checked.
- zig-ffi: `zig build test` the C-ABI FFI (Zig 0.14, SHA-pinned action).
Make the Zig FFI real — it shipped as an UNRENDERED RSR template:
- render {{project}}/{{PROJECT}} -> typedqliser across build.zig,
src/main.zig, test/integration_test.zig.
- build.zig: drop `lib.version` (versioned .so panics in Zig 0.14's
InstallArtifact) and add linkLibC() (main.zig uses std.heap.c_allocator)
— the same fixes proven on chapeliser.
Honest docs — the README sold an "Idris2 type kernel" as "the core", but
there are zero .idr files (src/abi/ is 54 lines of Rust):
- reframe the level model as proof OBLIGATIONS enforced in Rust today,
with the Idris2 kernel specified-but-unimplemented.
- fix the Zig FFI path and the Status paragraph.
Rust layer unchanged (116 tests). The golden type-checker is verified
locally; the Zig build is CI-gated (no zig mirror reachable in the sandbox).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ1 parent 7232886 commit b792eac
6 files changed
Lines changed: 504 additions & 86 deletions
File tree
- .github/workflows
- src/interface/ffi
- src
- test
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
0 commit comments