From 1bef5e4d569c57d12a4a8e75527ac35d3446da01 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:24:18 +0100 Subject: [PATCH 1/2] chore: delete the two dead Zig trees; fix the configs that pointed at them MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `bridge/` is the only live Zig tree — it builds and emits `zig-out/lib/liblith_bridge.a`, exactly what `lakefile.lean` links (`-Lbridge/zig-out/lib -llith_bridge`). The other two are removed. Both were measured against the pinned Zig 0.16.0 and neither compiles: bridge/zig/ build.zig:14 error: no field or member function named 'addStaticLibrary' in 'Build' ffi/zig/ src/main.zig:82 error: root source file struct 'heap' has no member named 'GeneralPurposeAllocator' Nothing linked against either. 1,383 lines of code that could not build. Two LIVE configs were still pointing at them — this is the same fault already fixed in CI, which had been building bridge/zig/ rather than bridge/: * `Containerfile` — `WORKDIR /workspace/bridge/zig`, i.e. the container built the tree that cannot compile. Also had the build order inverted: `lake build` ran BEFORE the Zig bridge, but the Lean link needs liblith_bridge.a to exist already. Both steps were `|| echo "..."`, so a wholly broken build still produced a "successful" image — the same swallow-the-failure shape as the gates removed in #6. Now: bridge first, asserting the archive exists, then `lake build`, neither masked. * `selur-compose.yml` — mounted the zig-cache volume at `/workspace/bridge/zig/.zig-cache`, a path that no longer exists. `ABI-FFI-README.md` was still the unfilled RSR template: 385 lines, 27 `{{project}}`/`{{PROJECT}}` placeholders, opening with "delete this line and fill out the template below", and documenting `ffi/zig/src/main.zig` as the FFI implementation — a file that did not compile. `README.adoc` linked to it as though it were real documentation. Replaced with an accurate description of what exists: the three Idris2 ABI files, the bridge layout, the build order and the 17 exported C functions, plus the unweighted-mean caveat on `computeOverall` carried over from docs/THEORY.adoc. `.gitignore` gains secret hygiene (`.env`, `.env.*`, `*.key`, `*.pem`, `secrets/`), `.claude/`, sqlite artifacts and editor droppings. These were sitting uncommitted in the working tree; the generic multi-language entries alongside them (Chapel, Elixir, Haskell, Julia) were dropped as irrelevant here. Verified after the deletions: `cd bridge && zig build && zig build test` passes and still emits liblith_bridge.a; the proof gate passes; `selur-compose.yml` and `mise.toml` both still parse. Remaining `ffi/zig` mentions in GQL-DT-COMPLETION-2026-02-07.md and docs/M6-PARSER-STATUS.md are left alone: they are dated historical snapshots, accurate as records of what was true when written. Co-Authored-By: Claude Opus 5 --- .gitignore | 23 + ABI-FFI-README.md | 422 +++---------- Containerfile | 18 +- README.adoc | 2 - bridge/zig/build.zig | 51 -- bridge/zig/src/main.zig | 142 ----- bridge/zig/test/integration_test.zig | 45 -- ffi/zig/build.zig | 51 -- ffi/zig/src/main.zig | 861 --------------------------- ffi/zig/test/integration_test.zig | 233 -------- mise.toml | 4 +- selur-compose.yml | 2 +- 12 files changed, 107 insertions(+), 1747 deletions(-) delete mode 100644 bridge/zig/build.zig delete mode 100644 bridge/zig/src/main.zig delete mode 100644 bridge/zig/test/integration_test.zig delete mode 100644 ffi/zig/build.zig delete mode 100644 ffi/zig/src/main.zig delete mode 100644 ffi/zig/test/integration_test.zig diff --git a/.gitignore b/.gitignore index 56e803f..ac1cd63 100644 --- a/.gitignore +++ b/.gitignore @@ -25,3 +25,26 @@ deps/ *.tmp Thumbs.db dist/ + +# Secrets — never commit these +.env +.env.* +*.key +*.pem +secrets/ + +# Agent scratch and worktrees +.claude/ + +# SQLite artifacts (the Zig bridge links libsqlite3) +*.db +*.db-journal +*.db-shm +*.db-wal + +# Editors +*.swp +*.swo +*.bak +.idea/ +.vscode/ diff --git a/ABI-FFI-README.md b/ABI-FFI-README.md index dda367a..684a9a0 100644 --- a/ABI-FFI-README.md +++ b/ABI-FFI-README.md @@ -1,385 +1,105 @@ -{{~ Aditionally delete this line and fill out the template below ~}} + -# {{PROJECT}} ABI/FFI Documentation +# ABI / FFI — how GNPL reaches Lithoglyph -## Overview +This repository follows the estate standard: **ABI defined in Idris2, FFI implemented in +Zig**, meeting at the C ABI. No C is written by hand. -This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: +> **History:** this file was previously the unfilled RSR template — 385 lines of +> `{{project}}` placeholders documenting an `ffi/zig/` tree that did not compile. It has +> been replaced with what the repository actually contains. -- **ABI (Application Binary Interface)** defined in **Idris2** with formal proofs -- **FFI (Foreign Function Interface)** implemented in **Zig** for C compatibility -- **Generated C headers** bridge Idris2 ABI to Zig FFI -- **Any language** can call through standard C ABI +## The path -## Architecture - -``` -┌─────────────────────────────────────────────┐ -│ ABI Definitions (Idris2) │ -│ src/abi/ │ -│ - Types.idr (Type definitions) │ -│ - Layout.idr (Memory layout proofs) │ -│ - Foreign.idr (FFI declarations) │ -└─────────────────┬───────────────────────────┘ - │ - │ generates (at compile time) - ▼ -┌─────────────────────────────────────────────┐ -│ C Headers (auto-generated) │ -│ generated/abi/{{project}}.h │ -└─────────────────┬───────────────────────────┘ - │ - │ imported by - ▼ -┌─────────────────────────────────────────────┐ -│ FFI Implementation (Zig) │ -│ ffi/zig/src/main.zig │ -│ - Implements C-compatible functions │ -│ - Zero-cost abstractions │ -│ - Memory-safe by default │ -└─────────────────┬───────────────────────────┘ - │ - │ compiled to lib{{project}}.so/.a - ▼ -┌─────────────────────────────────────────────┐ -│ Any Language via C ABI │ -│ - Rust, ReScript, Julia, Python, etc. │ -└─────────────────────────────────────────────┘ -``` - -## Directory Structure - -``` -{{project}}/ -├── src/ -│ ├── abi/ # ABI definitions (Idris2) -│ │ ├── Types.idr # Core type definitions with proofs -│ │ ├── Layout.idr # Memory layout verification -│ │ └── Foreign.idr # FFI function declarations -│ └── lib/ # Core library (any language) -│ -├── ffi/ -│ └── zig/ # FFI implementation (Zig) -│ ├── build.zig # Build configuration -│ ├── build.zig.zon # Dependencies -│ ├── src/ -│ │ └── main.zig # C-compatible FFI implementation -│ ├── test/ -│ │ └── integration_test.zig -│ └── include/ -│ └── {{project}}.h # C header (optional, can be generated) -│ -├── generated/ # Auto-generated files -│ └── abi/ -│ └── {{project}}.h # Generated from Idris2 ABI -│ -└── bindings/ # Language-specific wrappers (optional) - ├── rust/ - ├── rescript/ - └── julia/ -``` - -## Why Idris2 for ABI? - -### 1. **Formal Verification** - -Idris2's dependent types allow proving properties about the ABI at compile-time: - -```idris --- Prove struct size is correct -public export -exampleStructSize : HasSize ExampleStruct 16 - --- Prove field alignment is correct -public export -fieldAligned : Divides 8 (offsetOf ExampleStruct.field) - --- Prove ABI is platform-compatible -public export -abiCompatible : Compatible (ABI 1) (ABI 2) -``` - -### 2. **Type Safety** - -Encode invariants that C/Zig cannot express: - -```idris --- Non-null pointer guaranteed at type level -data Handle : Type where - MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle - --- Array with length proof -data Buffer : (n : Nat) -> Type where - MkBuffer : Vect n Byte -> Buffer n -``` - -### 3. **Platform Abstraction** - -Platform-specific types with compile-time selection: - -```idris -CInt : Platform -> Type -CInt Linux = Bits32 -CInt Windows = Bits32 - -CSize : Platform -> Type -CSize Linux = Bits64 -CSize Windows = Bits64 -``` - -### 4. **Safe Evolution** - -Prove that new ABI versions are backward-compatible: - -```idris --- Compiler enforces compatibility -abiUpgrade : ABI 1 -> ABI 2 -abiUpgrade old = MkABI2 { - -- Must preserve all v1 fields - v1_compat = old, - -- Can add new fields - new_features = defaults -} ``` - -## Why Zig for FFI? - -### 1. **C ABI Compatibility** - -Zig exports C-compatible functions naturally: - -```zig -export fn library_function(param: i32) i32 { - return param * 2; -} -``` - -### 2. **Memory Safety** - -Compile-time safety without runtime overhead: - -```zig -// Null check enforced at compile time -const handle = init() orelse return error.InitFailed; -defer free(handle); +GNPL ──lowers to──▶ GQLdt (Lean 4) + │ + │ FFI: links -Lbridge/zig-out/lib -llith_bridge + ▼ + bridge/ (Zig) ── C ABI ──▶ Lithoglyph Form.Bridge ``` -### 3. **Cross-Compilation** - -Built-in cross-compilation to any platform: +`lakefile.lean` links the Lean executables against `bridge/zig-out/lib/liblith_bridge.a`. +**That archive must exist before `lake build` runs.** -```bash -zig build -Dtarget=x86_64-linux -zig build -Dtarget=aarch64-macos -zig build -Dtarget=x86_64-windows -``` +## Layout -### 4. **Zero Dependencies** +| Path | Role | +|---|---| +| `src/GQLdt/ABI/Types.idr` | ABI type definitions | +| `src/GQLdt/ABI/Layout.idr` | memory-layout proofs | +| `src/GQLdt/ABI/Foreign.idr` | foreign declarations | +| `bridge/build.zig` | build script (`addLibrary`, Zig ≥ 0.15 API) | +| `bridge/lith_root.zig` | FFI entry point — the exported C surface | +| `bridge/lith_types.zig` | C-ABI structs (`ActorIdC`, `RationaleC`, `ProvenanceC`, `TrackedValueC`, `ProofBlob`, `PromptScoresC`) | +| `bridge/lith_insert.zig`, `bridge/lith_persist.zig` | insert + persistence implementation | -No runtime, no libc required (unless explicitly needed): - -```zig -// Minimal binary size -pub const lib = @import("std"); -// Only includes what you use -``` +`bridge/` is the **only** live Zig tree. Two earlier skeletons (`bridge/zig/`, `ffi/zig/`) +were removed — they were written against the pre-0.15 Build API (`addStaticLibrary`, +`std.heap.GeneralPurposeAllocator`), failed to compile on the pinned Zig 0.16.0, and nothing +linked against them. ## Building -### Build FFI Library - ```bash -cd ffi/zig -zig build # Build debug -zig build -Doptimize=ReleaseFast # Build optimized -zig build test # Run tests +cd bridge +zig build # produces zig-out/lib/liblith_bridge.a +zig build test # unit tests +zig build -Doptimize=ReleaseFast # optimised ``` -### Generate C Header from Idris2 ABI - -```bash -cd src/abi -idris2 --cg c-header Types.idr -o ../../generated/abi/{{project}}.h -``` +Cross-compilation works as usual (`-Dtarget=aarch64-macos`, etc.). -### Cross-Compile +Then, from the repository root: ```bash -cd ffi/zig - -# Linux x86_64 -zig build -Dtarget=x86_64-linux - -# macOS ARM64 -zig build -Dtarget=aarch64-macos - -# Windows x86_64 -zig build -Dtarget=x86_64-windows -``` - -## Usage - -### From C - -```c -#include "{{project}}.h" - -int main() { - void* handle = {{project}}_init(); - if (!handle) return 1; - - int result = {{project}}_process(handle, 42); - if (result != 0) { - const char* err = {{project}}_last_error(); - fprintf(stderr, "Error: %s\n", err); - } - - {{project}}_free(handle); - return 0; -} -``` - -Compile with: -```bash -gcc -o example example.c -l{{project}} -L./zig-out/lib +lake build ``` -### From Idris2 - -```idris -import {{PROJECT}}.ABI.Foreign - -main : IO () -main = do - Just handle <- init - | Nothing => putStrLn "Failed to initialize" - - Right result <- process handle 42 - | Left err => putStrLn $ "Error: " ++ errorDescription err - - free handle - putStrLn "Success" -``` - -### From Rust - -```rust -#[link(name = "{{project}}")] -extern "C" { - fn {{project}}_init() -> *mut std::ffi::c_void; - fn {{project}}_free(handle: *mut std::ffi::c_void); - fn {{project}}_process(handle: *mut std::ffi::c_void, input: u32) -> i32; -} - -fn main() { - unsafe { - let handle = {{project}}_init(); - assert!(!handle.is_null()); - - let result = {{project}}_process(handle, 42); - assert_eq!(result, 0); +Zig is pinned to **0.16.0** in `mise.toml`. Lean is pinned by `lean-toolchain` +(`leanprover/lean4:v4.15.0`), which elan reads automatically. - {{project}}_free(handle); - } -} -``` - -### From Julia - -```julia -const lib{{project}} = "lib{{project}}" - -function init() - handle = ccall((:{{project}}_init, lib{{project}}), Ptr{Cvoid}, ()) - handle == C_NULL && error("Failed to initialize") - handle -end - -function process(handle, input) - result = ccall((:{{project}}_process, lib{{project}}), Cint, (Ptr{Cvoid}, UInt32), handle, input) - result -end - -function cleanup(handle) - ccall((:{{project}}_free, lib{{project}}), Cvoid, (Ptr{Cvoid},), handle) -end - -# Usage -handle = init() -try - result = process(handle, 42) - println("Result: $result") -finally - cleanup(handle) -end -``` - -## Testing - -### Unit Tests (Zig) - -```bash -cd ffi/zig -zig build test -``` - -### Integration Tests - -```bash -cd ffi/zig -zig build test-integration -``` - -### ABI Verification (Idris2) - -```idris --- Compile-time verification -%runElab verifyABI - --- Runtime checks -main : IO () -main = do - verifyLayoutsCorrect - verifyAlignmentsCorrect - putStrLn "ABI verification passed" -``` +## Exported C surface -## Contributing +Seventeen functions, all `callconv(.C)`, from `bridge/`: -When modifying the ABI/FFI: +**Lifecycle** — `lith_init`, `lith_is_init`, `lith_close`, `lith_save` +**Data** — `lith_insert`, `lith_insert_row`, `lith_delete_row`, `lith_table_count` +**PROMPT scores** — `lith_get_scores`, `lith_compute_overall` +**Proofs** — `lith_verify_proof` +**Utility** — `lith_validate_non_empty`, `lith_timestamp_now`, `lith_get_last_error` +**Debug/test** — `lith_debug_init_counter`, `lith_debug_magic`, `lith_test_fresh` -1. **Update ABI first** (`src/abi/*.idr`) - - Modify type definitions - - Update proofs - - Ensure backward compatibility +Provenance crosses the boundary as real structs, not opaque blobs: `ActorIdC`, +`RationaleC`, `ProvenanceC` and `TrackedValueC` are marshalled directly. This is what makes +the GNPL narration layer buildable over this stack — see `docs/LITHOGLYPH.adoc`. -2. **Generate C header** - ```bash - idris2 --cg c-header src/abi/Types.idr -o generated/abi/{{project}}.h - ``` +> **Caveat.** `PromptScoresC.computeOverall` takes an **unweighted mean** of the six PROMPT +> dimensions. It is not probabilistically principled, and must not become a load-bearing +> entrenchment ordering without being revisited — see open question 2 in `docs/THEORY.adoc`. -3. **Update FFI implementation** (`ffi/zig/src/main.zig`) - - Implement new functions - - Match ABI types exactly +## Why this split -4. **Add tests** - - Unit tests in Zig - - Integration tests - - ABI verification tests +**Idris2 for the ABI** — dependent types let struct size, field alignment and cross-version +compatibility be *proved* rather than asserted, so an ABI change that would break a caller +fails at compile time. -5. **Update documentation** - - Function signatures - - Usage examples - - Migration guide (if breaking changes) +**Zig for the FFI** — `export fn … callconv(.C)` is C-compatible without a C compiler, +without libc, and with cross-compilation built in. -## License +## Adding a function -CC-BY-SA-4.0 +1. Declare the type in `src/GQLdt/ABI/Types.idr`; add a layout proof in `Layout.idr`. +2. Declare it in `src/GQLdt/ABI/Foreign.idr`. +3. Implement and `export` it in `bridge/` (match the ABI types exactly). +4. `cd bridge && zig build && zig build test`, then `lake build` from the root. -## See Also +## Related -- [Idris2 Documentation](https://idris2.readthedocs.io) -- [Zig Documentation](https://ziglang.org/documentation/master/) -- [Rhodium Standard Repositories](https://github.com/hyperpolymath/rhodium-standard-repositories) -- [FFI Migration Guide](../ffi-migration-guide.md) -- [ABI Migration Guide](../abi-migration-guide.md) +- `docs/THEORY.adoc` — what GNPL is, and what gap it fills +- `docs/LITHOGLYPH.adoc` — what GNPL gives Lithoglyph as a database +- `docs/proof-debt.md` — the 16 outstanding axioms; **read before relying on any + verification claim** diff --git a/Containerfile b/Containerfile index a48fe19..8f8cb92 100644 --- a/Containerfile +++ b/Containerfile @@ -43,15 +43,17 @@ WORKDIR /workspace # Copy project files COPY . /workspace/ -# Build Lean 4 project (download dependencies) -RUN lake build || echo "Build failed - dependencies may need to be fetched first" - -# Build Zig FFI bridge -WORKDIR /workspace/bridge/zig -RUN zig build || echo "Zig build failed - may need project setup" - -# Return to workspace root +# Build the Zig FFI bridge FIRST: lakefile.lean links against +# bridge/zig-out/lib/liblith_bridge.a, so the Lean build needs this artifact to +# already exist. (The previous order built Lean first and masked the inevitable +# failure with `|| echo`, which also meant a genuinely broken build still +# produced a "successful" image.) +WORKDIR /workspace/bridge +RUN zig build && test -f zig-out/lib/liblith_bridge.a + +# Build Lean 4 project (fetches mathlib on first run) WORKDIR /workspace +RUN lake build # Default command: interactive shell CMD ["/bin/bash"] diff --git a/README.adoc b/README.adoc index 55e6252..73cb46e 100644 --- a/README.adoc +++ b/README.adoc @@ -80,8 +80,6 @@ Lithoglyph-as-a-database is the second. See the design documents below. | Zig FFI bridge (`bridge/`) | *builds* | produces `zig-out/lib/liblith_bridge.a`, the artifact `lakefile.lean` links; `zig build test` passes | GNPL narration layer | *design* | `docs/THEORY.adoc` + `docs/LITHOGLYPH.adoc`; no code yet -| `bridge/zig/`, `ffi/zig/` | *stale* | skeletons on the pre-0.15 Zig Build API; nothing - links against them |=== == Build diff --git a/bridge/zig/build.zig b/bridge/zig/build.zig deleted file mode 100644 index f749e1f..0000000 --- a/bridge/zig/build.zig +++ /dev/null @@ -1,51 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2026 hyperpolymath -// -// Zig FFI Bridge for GQLdt -// Provides C-compatible ABI for Lean 4 integration - -const std = @import("std"); - -pub fn build(b: *std.Build) void { - const target = b.standardTargetOptions(.{}); - const optimize = b.standardOptimizeOption(.{}); - - // Static library for FFI bridge - const lib = b.addStaticLibrary(.{ - .name = "lith_bridge", - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }); - - // Export C ABI - lib.linkLibC(); - - b.installArtifact(lib); - - // Tests - const main_tests = b.addTest(.{ - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }); - - const run_main_tests = b.addRunArtifact(main_tests); - - const test_step = b.step("test", "Run library tests"); - test_step.dependOn(&run_main_tests.step); - - // Integration tests - const integration_tests = b.addTest(.{ - .root_source_file = b.path("test/integration_test.zig"), - .target = target, - .optimize = optimize, - }); - - integration_tests.linkLibrary(lib); - - const run_integration_tests = b.addRunArtifact(integration_tests); - - const integration_step = b.step("test-integration", "Run integration tests"); - integration_step.dependOn(&run_integration_tests.step); -} diff --git a/bridge/zig/src/main.zig b/bridge/zig/src/main.zig deleted file mode 100644 index a95c91c..0000000 --- a/bridge/zig/src/main.zig +++ /dev/null @@ -1,142 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (@hyperpolymath) -// -// Zig FFI Bridge - Main Module -// Bidirectional FFI: Lean 4 ↔ Zig ↔ Lith Forth core - -const std = @import("std"); - -/// Status code for FFI operations -pub const LithStatus = enum(i32) { - ok = 0, - error_null_pointer = 1, - error_invalid_proof = 2, - error_type_mismatch = 3, - error_constraint_violation = 4, - error_out_of_memory = 5, - - pub fn toC(self: LithStatus) c_int { - return @intFromEnum(self); - } -}; - -/// Opaque database handle (non-null guaranteed by Lean 4 types) -pub const LithDb = opaque {}; - -/// FFI-safe string view (non-owning) -pub const LithString = struct { - data: [*]const u8, - len: usize, - - pub fn fromSlice(slice: []const u8) LithString { - return .{ .data = slice.ptr, .len = slice.len }; - } - - pub fn toSlice(self: LithString) []const u8 { - return self.data[0..self.len]; - } -}; - -/// Forward: Lean 4 → Zig → Lith -/// Insert operation with proof blob -export fn lith_insert( - db: *LithDb, - collection: [*:0]const u8, - document: [*]const u8, - doc_len: usize, - proof_blob: [*]const u8, - proof_len: usize, -) callconv(.C) c_int { - _ = db; - _ = collection; - _ = document; - _ = doc_len; - _ = proof_blob; - _ = proof_len; - - // TODO: Implement actual insertion - // 1. Deserialize proof blob (CBOR) - // 2. Verify proof against schema - // 3. Insert into Lith via Forth FFI - // 4. Return status - - return LithStatus.ok.toC(); -} - -/// Reverse: Lith → Zig → Lean 4 -/// Register constraint checker callback -export fn lith_register_constraint_checker( - db: *LithDb, - checker: *const fn (doc: [*]const u8, len: usize) callconv(.C) bool, -) callconv(.C) c_int { - _ = db; - _ = checker; - - // TODO: Implement callback registration - // Store function pointer for later invocation - // When Lith validates data, call this Lean 4 checker - - return LithStatus.ok.toC(); -} - -/// Get discovered functional dependencies -export fn lith_get_discovered_fds( - db: *LithDb, - collection: [*:0]const u8, - out_fds: *[*]u8, - out_len: *usize, -) callconv(.C) c_int { - _ = db; - _ = collection; - _ = out_fds; - _ = out_len; - - // TODO: Implement FD discovery - // 1. Query Lith for collection statistics - // 2. Run FD discovery algorithm (DFD, TANE, etc.) - // 3. Serialize FDs to CBOR - // 4. Return pointer + length - - return LithStatus.ok.toC(); -} - -/// Verify normalization proof -export fn lith_verify_normalization_proof( - db: *LithDb, - step_blob: [*]const u8, - step_len: usize, - proof_blob: [*]const u8, - proof_len: usize, -) callconv(.C) c_int { - _ = db; - _ = step_blob; - _ = step_len; - _ = proof_blob; - _ = proof_len; - - // TODO: Implement proof verification - // 1. Deserialize normalization step - // 2. Deserialize Lean 4 proof - // 3. Verify proof is valid for step - // 4. Return status - - return LithStatus.ok.toC(); -} - -/// Free memory allocated by FFI functions -export fn lith_free(ptr: [*]u8, len: usize) callconv(.C) void { - const allocator = std.heap.c_allocator; - const slice = ptr[0..len]; - allocator.free(slice); -} - -test "LithStatus roundtrip" { - const status = LithStatus.ok; - try std.testing.expectEqual(@as(c_int, 0), status.toC()); -} - -test "LithString conversion" { - const str = "Hello, Lith!"; - const lith_str = LithString.fromSlice(str); - try std.testing.expectEqualSlices(u8, str, lith_str.toSlice()); -} diff --git a/bridge/zig/test/integration_test.zig b/bridge/zig/test/integration_test.zig deleted file mode 100644 index 9a8f36b..0000000 --- a/bridge/zig/test/integration_test.zig +++ /dev/null @@ -1,45 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2026 hyperpolymath -// -// Integration tests for Zig FFI bridge - -const std = @import("std"); -const main = @import("main"); - -test "lith_insert stub returns ok" { - // Mock database handle (in production, would be created by Lith) - var db: main.LithDb = undefined; - const db_ptr = @as(*main.LithDb, @ptrCast(&db)); - - const collection = "test_collection"; - const document = "{\"id\": 1, \"value\": 42}"; - const proof = "{}"; // Empty proof for stub - - const status = main.lith_insert( - db_ptr, - collection, - document.ptr, - document.len, - proof.ptr, - proof.len, - ); - - try std.testing.expectEqual(@as(c_int, 0), status); -} - -test "lith_register_constraint_checker stub" { - var db: main.LithDb = undefined; - const db_ptr = @as(*main.LithDb, @ptrCast(&db)); - - const checker = struct { - fn check(doc: [*]const u8, len: usize) callconv(.C) bool { - _ = doc; - _ = len; - return true; - } - }.check; - - const status = main.lith_register_constraint_checker(db_ptr, checker); - - try std.testing.expectEqual(@as(c_int, 0), status); -} diff --git a/ffi/zig/build.zig b/ffi/zig/build.zig deleted file mode 100644 index 0961651..0000000 --- a/ffi/zig/build.zig +++ /dev/null @@ -1,51 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (@hyperpolymath) -// -// build.zig - GQL-DT FFI Build Configuration (Zig 0.15.2+) -// -// Builds the libgqldt shared library (C ABI) and unit tests. - -const std = @import("std"); - -pub fn build(b: *std.Build) void { - const target = b.standardTargetOptions(.{}); - const optimize = b.standardOptimizeOption(.{}); - - // Static library (libgqldt.a) - const static_lib = b.addLibrary(.{ - .name = "gqldt", - .root_module = b.createModule(.{ - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }), - .linkage = .static, - }); - b.installArtifact(static_lib); - - // Shared library (libgqldt.so / libgqldt.dylib) - const shared_lib = b.addLibrary(.{ - .name = "gqldt", - .root_module = b.createModule(.{ - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }), - .linkage = .dynamic, - }); - b.installArtifact(shared_lib); - - // Unit tests (from main.zig internal tests) - const unit_tests = b.addTest(.{ - .name = "gqldt-tests", - .root_module = b.createModule(.{ - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }), - }); - - const run_unit_tests = b.addRunArtifact(unit_tests); - const test_step = b.step("test", "Run unit tests"); - test_step.dependOn(&run_unit_tests.step); -} diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig deleted file mode 100644 index e3ee8af..0000000 --- a/ffi/zig/src/main.zig +++ /dev/null @@ -1,861 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (@hyperpolymath) -// -// main.zig - Zig FFI implementation for GQL-DT ABI -// -// Pure ABI bridge — all safety logic in Idris2. -// Delegates database operations to the Lith bridge layer (lith_persist/lith_insert). -// Manages opaque handle lifecycle and query parsing at the FFI boundary. - -const std = @import("std"); -const testing = std.testing; - -// --------------------------------------------------------------------------- -// Status codes (matches Idris2 GqldtStatus in GQLdt.ABI.Types) -// --------------------------------------------------------------------------- - -/// Result status codes for GQL-DT FFI operations. -/// Integer values match the Idris2 statusToInt mapping exactly. -pub const Status = enum(i32) { - ok = 0, - invalid_arg = 1, - type_mismatch = 2, - proof_failed = 3, - permission_denied = 4, - out_of_memory = 5, - internal_error = 6, -}; - -// --------------------------------------------------------------------------- -// Handle backing structures -// --------------------------------------------------------------------------- - -/// Internal database state backing the opaque GqldtDb handle. -/// Stores the path used to open the database and tracks open state. -const DbState = struct { - path_buf: [4096]u8 = undefined, - path_len: usize = 0, - opened: bool = false, -}; - -/// Internal query state backing the opaque GqldtQuery handle. -/// Stores the raw query text and whether it has been type-checked. -const QueryState = struct { - text_buf: [1_000_000]u8 = undefined, - text_len: usize = 0, - type_checked: bool = false, - inferred: bool = false, -}; - -/// Internal schema state backing the opaque GqldtSchema handle. -/// Stores the collection name the schema was retrieved for. -const SchemaState = struct { - collection_buf: [256]u8 = undefined, - collection_len: usize = 0, -}; - -/// Internal result-set state backing the opaque GqldtResult handle. -/// Stores serialised query output after execution. -const ResultState = struct { - data_buf: [1_000_000]u8 = undefined, - data_len: usize = 0, -}; - -// --------------------------------------------------------------------------- -// Opaque handle types (matches Idris2 handle types) -// --------------------------------------------------------------------------- - -pub const GqldtDb = opaque {}; -pub const GqldtQuery = opaque {}; -pub const GqldtSchema = opaque {}; -pub const GqldtType = opaque {}; -pub const GqldtResult = opaque {}; - -// --------------------------------------------------------------------------- -// Global library state -// --------------------------------------------------------------------------- - -/// Whether gqldt_init() has been called successfully. -var initialized: bool = false; - -/// General-purpose allocator for handle allocations. -var gpa = std.heap.GeneralPurposeAllocator(.{}){}; - -// --------------------------------------------------------------------------- -// Library Lifecycle -// --------------------------------------------------------------------------- - -/// Initialise the GQL-DT library. -/// Idempotent — repeated calls return ok without side-effects. -export fn gqldt_init() callconv(.c) i32 { - if (initialized) return @intFromEnum(Status.ok); - initialized = true; - return @intFromEnum(Status.ok); -} - -/// Tear down the GQL-DT library and release the backing allocator. -export fn gqldt_cleanup() callconv(.c) void { - if (!initialized) return; - _ = gpa.deinit(); - gpa = std.heap.GeneralPurposeAllocator(.{}){}; - initialized = false; -} - -// --------------------------------------------------------------------------- -// Database Operations -// --------------------------------------------------------------------------- - -/// Open a database at the given path and write an opaque handle into *db_out. -/// -/// Path validation is expected to happen on the Idris2 side via Proven.SafePath -/// before this function is called. The FFI layer performs basic sanity checks -/// (non-null, bounded length) and allocates a DbState on the heap. -export fn gqldt_db_open( - path: [*:0]const u8, - path_len: u64, - db_out: *?*GqldtDb, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - if (path_len == 0) return @intFromEnum(Status.invalid_arg); - if (path_len > 4096) return @intFromEnum(Status.invalid_arg); - - const len: usize = @intCast(path_len); - - // Validate that the path is a reasonable C string. - if (!validate_c_string(path, len)) return @intFromEnum(Status.invalid_arg); - - const allocator = gpa.allocator(); - const state = allocator.create(DbState) catch { - return @intFromEnum(Status.out_of_memory); - }; - - @memcpy(state.path_buf[0..len], path[0..len]); - state.path_len = len; - state.opened = true; - - // SAFETY: DbState is a heap-allocated struct; casting its pointer to the - // opaque GqldtDb handle is the standard pattern for Zig FFI bridges. - db_out.* = @ptrCast(state); - return @intFromEnum(Status.ok); -} - -/// Close a previously-opened database handle and free its backing memory. -export fn gqldt_db_close(db: *GqldtDb) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - - // SAFETY: The caller must pass a handle originally obtained from - // gqldt_db_open. We cast back to the concrete DbState to free it. - const state: *DbState = @ptrCast(@alignCast(db)); - state.opened = false; - - const allocator = gpa.allocator(); - allocator.destroy(state); - return @intFromEnum(Status.ok); -} - -// --------------------------------------------------------------------------- -// Query Parsing and Type Checking -// --------------------------------------------------------------------------- - -/// Parse a GQL-DT query string (explicit dependent types). -/// -/// String validation is expected to happen on the Idris2 side via -/// Proven.SafeString before this function is called. The FFI layer stores -/// the raw query text in a heap-allocated QueryState. -export fn gqldt_parse( - query_str: [*:0]const u8, - query_len: u64, - query_out: *?*GqldtQuery, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - if (query_len == 0) return @intFromEnum(Status.invalid_arg); - if (query_len > 1_000_000) return @intFromEnum(Status.invalid_arg); - - const len: usize = @intCast(query_len); - - if (!validate_c_string(query_str, len)) return @intFromEnum(Status.invalid_arg); - - const allocator = gpa.allocator(); - const state = allocator.create(QueryState) catch { - return @intFromEnum(Status.out_of_memory); - }; - - @memcpy(state.text_buf[0..len], query_str[0..len]); - state.text_len = len; - state.type_checked = false; - state.inferred = false; - - // SAFETY: Heap-allocated QueryState cast to opaque handle. - query_out.* = @ptrCast(state); - return @intFromEnum(Status.ok); -} - -/// Parse a GQL query string with type inference against a schema. -/// -/// Type inference is delegated to the Idris2 layer; at the FFI level we -/// record that this query was parsed with inference enabled. -export fn gqldt_parse_inferred( - query_str: [*:0]const u8, - query_len: u64, - schema: *GqldtSchema, - query_out: *?*GqldtQuery, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - if (query_len == 0) return @intFromEnum(Status.invalid_arg); - if (query_len > 1_000_000) return @intFromEnum(Status.invalid_arg); - - const len: usize = @intCast(query_len); - - if (!validate_c_string(query_str, len)) return @intFromEnum(Status.invalid_arg); - - // Validate the schema handle is non-null (opaque pointer check). - _ = schema; - - const allocator = gpa.allocator(); - const state = allocator.create(QueryState) catch { - return @intFromEnum(Status.out_of_memory); - }; - - @memcpy(state.text_buf[0..len], query_str[0..len]); - state.text_len = len; - state.type_checked = false; - state.inferred = true; - - // SAFETY: Heap-allocated QueryState cast to opaque handle. - query_out.* = @ptrCast(state); - return @intFromEnum(Status.ok); -} - -/// Type-check a parsed query against a schema. -/// -/// Full dependent-type checking happens in Idris2. The FFI layer marks the -/// query as type-checked so that gqldt_execute can verify the precondition. -export fn gqldt_typecheck( - query: *GqldtQuery, - schema: *GqldtSchema, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - - _ = schema; - - // SAFETY: Caller must pass a handle from gqldt_parse / gqldt_parse_inferred. - const state: *QueryState = @ptrCast(@alignCast(query)); - if (state.text_len == 0) return @intFromEnum(Status.invalid_arg); - - state.type_checked = true; - return @intFromEnum(Status.ok); -} - -// --------------------------------------------------------------------------- -// Query Execution -// --------------------------------------------------------------------------- - -/// Execute a type-checked query against an open database. -/// -/// Execution with provenance tracking is handled by the Idris2 layer. The -/// FFI layer allocates a ResultState to hold the output and verifies that the -/// query has been type-checked beforehand. -export fn gqldt_execute( - db: *GqldtDb, - query: *GqldtQuery, - result_out: *?*GqldtResult, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - - // SAFETY: Handles must originate from their respective open/parse calls. - const db_state: *DbState = @ptrCast(@alignCast(db)); - const q_state: *QueryState = @ptrCast(@alignCast(query)); - - if (!db_state.opened) return @intFromEnum(Status.internal_error); - if (q_state.text_len == 0) return @intFromEnum(Status.invalid_arg); - if (!q_state.type_checked) return @intFromEnum(Status.type_mismatch); - - const allocator = gpa.allocator(); - const r_state = allocator.create(ResultState) catch { - return @intFromEnum(Status.out_of_memory); - }; - - // Placeholder result — in production the Idris2 execute function fills - // this with CBOR-encoded result rows. - r_state.data_len = 0; - - // SAFETY: Heap-allocated ResultState cast to opaque handle. - result_out.* = @ptrCast(r_state); - return @intFromEnum(Status.ok); -} - -// --------------------------------------------------------------------------- -// Serialization -// --------------------------------------------------------------------------- - -/// Serialise a parsed query to CBOR (RFC 8949). -/// -/// Semantic-tag encoding is performed in Idris2 via the CborTag definitions. -/// The FFI layer writes a minimal CBOR text-string encoding of the raw query -/// into the caller-provided buffer. -export fn gqldt_serialize_cbor( - query: *GqldtQuery, - buffer: [*]u8, - buffer_len: u64, - written_out: *u64, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - if (buffer_len == 0) return @intFromEnum(Status.invalid_arg); - - // SAFETY: Handle from gqldt_parse. - const state: *QueryState = @ptrCast(@alignCast(query)); - if (state.text_len == 0) return @intFromEnum(Status.invalid_arg); - - const buf_len: usize = @intCast(buffer_len); - - // Encode as CBOR text string: major type 3 + length prefix + UTF-8 bytes. - // This is a minimal encoding; full semantic tagging is handled by Idris2. - const header_size = cbor_text_header_size(state.text_len); - const total = header_size + state.text_len; - - if (total > buf_len) return @intFromEnum(Status.invalid_arg); - - var pos: usize = 0; - write_cbor_text_header(buffer, &pos, state.text_len); - @memcpy(buffer[pos .. pos + state.text_len], state.text_buf[0..state.text_len]); - pos += state.text_len; - - written_out.* = @intCast(pos); - return @intFromEnum(Status.ok); -} - -/// Serialise a parsed query to JSON. -/// -/// Produces a JSON object wrapping the raw query text. -export fn gqldt_serialize_json( - query: *GqldtQuery, - buffer: [*]u8, - buffer_len: u64, - written_out: *u64, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - if (buffer_len == 0) return @intFromEnum(Status.invalid_arg); - - // SAFETY: Handle from gqldt_parse. - const state: *QueryState = @ptrCast(@alignCast(query)); - if (state.text_len == 0) return @intFromEnum(Status.invalid_arg); - - const buf_len: usize = @intCast(buffer_len); - - // Produce: {"query":""} - const prefix = "{\"query\":\""; - const suffix = "\"}"; - const total = prefix.len + state.text_len + suffix.len; - - if (total > buf_len) return @intFromEnum(Status.invalid_arg); - - var pos: usize = 0; - @memcpy(buffer[pos .. pos + prefix.len], prefix); - pos += prefix.len; - @memcpy(buffer[pos .. pos + state.text_len], state.text_buf[0..state.text_len]); - pos += state.text_len; - @memcpy(buffer[pos .. pos + suffix.len], suffix); - pos += suffix.len; - - written_out.* = @intCast(pos); - return @intFromEnum(Status.ok); -} - -/// Deserialise a query from CBOR. -/// -/// Expects a CBOR text-string encoding (major type 3). Full semantic-tag -/// validation is handled in Idris2. -export fn gqldt_deserialize_cbor( - buffer: [*]const u8, - buffer_len: u64, - query_out: *?*GqldtQuery, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - if (buffer_len == 0) return @intFromEnum(Status.invalid_arg); - if (buffer_len > 10_000_000) return @intFromEnum(Status.invalid_arg); - - const buf_len: usize = @intCast(buffer_len); - - // Decode CBOR text string header (major type 3). - var pos: usize = 0; - const text_len = read_cbor_text_header(buffer, buf_len, &pos) orelse { - return @intFromEnum(Status.invalid_arg); - }; - - if (pos + text_len > buf_len) return @intFromEnum(Status.invalid_arg); - if (text_len == 0) return @intFromEnum(Status.invalid_arg); - if (text_len > 1_000_000) return @intFromEnum(Status.invalid_arg); - - const allocator = gpa.allocator(); - const state = allocator.create(QueryState) catch { - return @intFromEnum(Status.out_of_memory); - }; - - @memcpy(state.text_buf[0..text_len], buffer[pos .. pos + text_len]); - state.text_len = text_len; - state.type_checked = false; - state.inferred = false; - - // SAFETY: Heap-allocated QueryState cast to opaque handle. - query_out.* = @ptrCast(state); - return @intFromEnum(Status.ok); -} - -// --------------------------------------------------------------------------- -// Schema Operations -// --------------------------------------------------------------------------- - -/// Retrieve the schema for a named collection from an open database. -/// -/// Schema extraction and validation are performed in Idris2. The FFI layer -/// allocates a SchemaState that records the collection name. -export fn gqldt_get_schema( - db: *GqldtDb, - collection_name: [*:0]const u8, - schema_out: *?*GqldtSchema, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - - // SAFETY: Handle from gqldt_db_open. - const db_state: *DbState = @ptrCast(@alignCast(db)); - if (!db_state.opened) return @intFromEnum(Status.internal_error); - - // Measure collection name length (null-terminated). - var name_len: usize = 0; - while (collection_name[name_len] != 0) : (name_len += 1) { - if (name_len >= 256) return @intFromEnum(Status.invalid_arg); - } - if (name_len == 0) return @intFromEnum(Status.invalid_arg); - - const allocator = gpa.allocator(); - const state = allocator.create(SchemaState) catch { - return @intFromEnum(Status.out_of_memory); - }; - - @memcpy(state.collection_buf[0..name_len], collection_name[0..name_len]); - state.collection_len = name_len; - - // SAFETY: Heap-allocated SchemaState cast to opaque handle. - schema_out.* = @ptrCast(state); - return @intFromEnum(Status.ok); -} - -// --------------------------------------------------------------------------- -// Permission Validation -// --------------------------------------------------------------------------- - -/// Validate query permissions using the two-tier TypeWhitelist system. -/// -/// Permission checking with TypeWhitelist is performed in Idris2. The FFI -/// layer delegates the decision and returns the result. Currently returns -/// ok for all queries — real enforcement is in the Idris2 layer. -export fn gqldt_validate_permissions( - query: *GqldtQuery, - user_id: [*:0]const u8, - permissions: *const anyopaque, -) callconv(.c) i32 { - if (!initialized) return @intFromEnum(Status.internal_error); - - // SAFETY: Handle from gqldt_parse. - const q_state: *QueryState = @ptrCast(@alignCast(query)); - if (q_state.text_len == 0) return @intFromEnum(Status.invalid_arg); - - // Validate user_id is non-empty. - if (user_id[0] == 0) return @intFromEnum(Status.invalid_arg); - - // Permissions opaque pointer must be non-null (checked by C ABI contract). - _ = permissions; - - // Permission enforcement happens in Idris2 — FFI layer grants by default. - return @intFromEnum(Status.ok); -} - -// --------------------------------------------------------------------------- -// Resource Cleanup -// --------------------------------------------------------------------------- - -/// Free a query handle previously returned by gqldt_parse, -/// gqldt_parse_inferred, or gqldt_deserialize_cbor. -export fn gqldt_query_free(query: *GqldtQuery) callconv(.c) void { - if (!initialized) return; - - // SAFETY: Handle from gqldt_parse / gqldt_parse_inferred / gqldt_deserialize_cbor. - const state: *QueryState = @ptrCast(@alignCast(query)); - const allocator = gpa.allocator(); - allocator.destroy(state); -} - -/// Free a schema handle previously returned by gqldt_get_schema. -export fn gqldt_schema_free(schema: *GqldtSchema) callconv(.c) void { - if (!initialized) return; - - // SAFETY: Handle from gqldt_get_schema. - const state: *SchemaState = @ptrCast(@alignCast(schema)); - const allocator = gpa.allocator(); - allocator.destroy(state); -} - -/// Free a result handle previously returned by gqldt_execute. -export fn gqldt_result_free(result: *GqldtResult) callconv(.c) void { - if (!initialized) return; - - // SAFETY: Handle from gqldt_execute. - const state: *ResultState = @ptrCast(@alignCast(result)); - const allocator = gpa.allocator(); - allocator.destroy(state); -} - -// --------------------------------------------------------------------------- -// Version Information -// --------------------------------------------------------------------------- - -/// Return the GQL-DT FFI library version as a null-terminated C string. -export fn gqldt_version() callconv(.c) [*:0]const u8 { - return "0.1.0"; -} - -// --------------------------------------------------------------------------- -// Slot Allocation Helpers (for Idris2 prim__allocSlot / prim__readSlot) -// --------------------------------------------------------------------------- - -/// Allocate a pointer-sized output slot on the heap. -/// Used by Idris2 to receive opaque handle pointers from FFI calls. -export fn gqldt_alloc_slot() callconv(.c) ?*anyopaque { - const allocator = gpa.allocator(); - const slot = allocator.create(usize) catch return null; - slot.* = 0; - // SAFETY: usize* cast to opaque — Idris2 treats it as AnyPtr. - return @ptrCast(slot); -} - -/// Read a pointer value from an output slot as u64 (Bits64 in Idris2). -export fn gqldt_read_slot(slot: *anyopaque) callconv(.c) u64 { - // SAFETY: Slot must have been allocated by gqldt_alloc_slot. - const typed: *usize = @ptrCast(@alignCast(slot)); - return @intCast(typed.*); -} - -/// Free an output slot allocated by gqldt_alloc_slot. -export fn gqldt_free_slot(slot: *anyopaque) callconv(.c) void { - // SAFETY: Slot must have been allocated by gqldt_alloc_slot. - const typed: *usize = @ptrCast(@alignCast(slot)); - const allocator = gpa.allocator(); - allocator.destroy(typed); -} - -/// Cast a Bits64 value to an opaque pointer. -/// Used by Idris2 to convert handle values back to pointers for FFI calls. -export fn gqldt_bits64_to_ptr(value: u64) callconv(.c) ?*anyopaque { - if (value == 0) return null; - // SAFETY: The caller guarantees that value was originally obtained from - // a valid pointer via gqldt_read_slot. - return @ptrFromInt(@as(usize, @intCast(value))); -} - -// --------------------------------------------------------------------------- -// Helper Functions (ABI Bridge Only) -// --------------------------------------------------------------------------- - -/// Validate a null-terminated C string has non-zero length and fits within -/// max_len bytes. -/// -/// NOTE: Full validation happens in Idris2 via Proven.SafeString. -fn validate_c_string(ptr: [*:0]const u8, max_len: usize) bool { - var len: usize = 0; - while (ptr[len] != 0) : (len += 1) { - if (len >= max_len) return false; - } - return len > 0; -} - -/// Compute the number of header bytes needed for a CBOR text string of the -/// given length (major type 3). -fn cbor_text_header_size(text_len: usize) usize { - if (text_len < 24) return 1; - if (text_len <= 0xFF) return 2; - if (text_len <= 0xFFFF) return 3; - if (text_len <= 0xFFFFFFFF) return 5; - return 9; -} - -/// Write a CBOR text string header (major type 3) into buffer at *pos. -fn write_cbor_text_header(buffer: [*]u8, pos: *usize, text_len: usize) void { - const major: u8 = 3 << 5; // major type 3 - if (text_len < 24) { - buffer[pos.*] = major | @as(u8, @truncate(text_len)); - pos.* += 1; - } else if (text_len <= 0xFF) { - buffer[pos.*] = major | 24; - pos.* += 1; - buffer[pos.*] = @truncate(text_len); - pos.* += 1; - } else if (text_len <= 0xFFFF) { - buffer[pos.*] = major | 25; - pos.* += 1; - const be = std.mem.nativeToBig(u16, @truncate(text_len)); - const bytes = std.mem.toBytes(be); - @memcpy(buffer[pos.* .. pos.* + 2], &bytes); - pos.* += 2; - } else if (text_len <= 0xFFFFFFFF) { - buffer[pos.*] = major | 26; - pos.* += 1; - const be = std.mem.nativeToBig(u32, @truncate(text_len)); - const bytes = std.mem.toBytes(be); - @memcpy(buffer[pos.* .. pos.* + 4], &bytes); - pos.* += 4; - } else { - buffer[pos.*] = major | 27; - pos.* += 1; - const be = std.mem.nativeToBig(u64, @as(u64, text_len)); - const bytes = std.mem.toBytes(be); - @memcpy(buffer[pos.* .. pos.* + 8], &bytes); - pos.* += 8; - } -} - -/// Read a CBOR text string header (major type 3) from buffer, advancing *pos. -/// Returns null if the header is invalid or not a text string. -fn read_cbor_text_header(buffer: [*]const u8, buf_len: usize, pos: *usize) ?usize { - if (pos.* >= buf_len) return null; - - const initial = buffer[pos.*]; - const major = initial >> 5; - if (major != 3) return null; // Not a text string. - - const additional = initial & 0x1F; - pos.* += 1; - - if (additional < 24) { - return @as(usize, additional); - } else if (additional == 24) { - if (pos.* >= buf_len) return null; - const len: usize = buffer[pos.*]; - pos.* += 1; - return len; - } else if (additional == 25) { - if (pos.* + 2 > buf_len) return null; - var bytes: [2]u8 = undefined; - @memcpy(&bytes, buffer[pos.* .. pos.* + 2]); - pos.* += 2; - return @as(usize, std.mem.bigToNative(u16, @bitCast(bytes))); - } else if (additional == 26) { - if (pos.* + 4 > buf_len) return null; - var bytes: [4]u8 = undefined; - @memcpy(&bytes, buffer[pos.* .. pos.* + 4]); - pos.* += 4; - return @as(usize, std.mem.bigToNative(u32, @bitCast(bytes))); - } else if (additional == 27) { - if (pos.* + 8 > buf_len) return null; - var bytes: [8]u8 = undefined; - @memcpy(&bytes, buffer[pos.* .. pos.* + 8]); - pos.* += 8; - return @as(usize, std.mem.bigToNative(u64, @bitCast(bytes))); - } - - return null; -} - -// --------------------------------------------------------------------------- -// Tests -// --------------------------------------------------------------------------- - -test "status codes match Idris2 ABI" { - try testing.expectEqual(@as(i32, 0), @intFromEnum(Status.ok)); - try testing.expectEqual(@as(i32, 1), @intFromEnum(Status.invalid_arg)); - try testing.expectEqual(@as(i32, 2), @intFromEnum(Status.type_mismatch)); - try testing.expectEqual(@as(i32, 3), @intFromEnum(Status.proof_failed)); - try testing.expectEqual(@as(i32, 4), @intFromEnum(Status.permission_denied)); - try testing.expectEqual(@as(i32, 5), @intFromEnum(Status.out_of_memory)); - try testing.expectEqual(@as(i32, 6), @intFromEnum(Status.internal_error)); -} - -test "library initialization" { - const status = gqldt_init(); - try testing.expectEqual(@intFromEnum(Status.ok), status); - gqldt_cleanup(); -} - -test "library double-init is idempotent" { - _ = gqldt_init(); - const status = gqldt_init(); - try testing.expectEqual(@intFromEnum(Status.ok), status); - gqldt_cleanup(); -} - -test "validate_c_string rejects empty strings" { - const empty_str: [*:0]const u8 = ""; - try testing.expect(!validate_c_string(empty_str, 100)); -} - -test "validate_c_string accepts valid strings" { - const valid_str: [*:0]const u8 = "SELECT * FROM users"; - try testing.expect(validate_c_string(valid_str, 1000)); -} - -test "validate_c_string rejects oversized strings" { - var buf: [200]u8 = undefined; - @memset(&buf, 'A'); - buf[199] = 0; - const long_str: [*:0]const u8 = @ptrCast(&buf); - try testing.expect(!validate_c_string(long_str, 100)); -} - -test "db_open and db_close round-trip" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*GqldtDb = null; - const open_status = gqldt_db_open("test.db", 7, &db); - try testing.expectEqual(@intFromEnum(Status.ok), open_status); - try testing.expect(db != null); - - const close_status = gqldt_db_close(db.?); - try testing.expectEqual(@intFromEnum(Status.ok), close_status); -} - -test "db_open rejects empty path" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*GqldtDb = null; - const status = gqldt_db_open("", 0, &db); - try testing.expectEqual(@intFromEnum(Status.invalid_arg), status); -} - -test "parse and query_free round-trip" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var query: ?*GqldtQuery = null; - const query_text: [*:0]const u8 = "MATCH (n:Person) RETURN n"; - const status = gqldt_parse(query_text, 25, &query); - try testing.expectEqual(@intFromEnum(Status.ok), status); - try testing.expect(query != null); - - gqldt_query_free(query.?); -} - -test "parse rejects empty query" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var query: ?*GqldtQuery = null; - const status = gqldt_parse("", 0, &query); - try testing.expectEqual(@intFromEnum(Status.invalid_arg), status); -} - -test "typecheck marks query as checked" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - // Create a schema handle. - var db: ?*GqldtDb = null; - _ = gqldt_db_open("test.db", 7, &db); - defer _ = gqldt_db_close(db.?); - - var schema: ?*GqldtSchema = null; - _ = gqldt_get_schema(db.?, "users", &schema); - defer gqldt_schema_free(schema.?); - - // Parse a query. - var query: ?*GqldtQuery = null; - _ = gqldt_parse("MATCH (n) RETURN n", 18, &query); - defer gqldt_query_free(query.?); - - // Type-check. - const tc_status = gqldt_typecheck(query.?, schema.?); - try testing.expectEqual(@intFromEnum(Status.ok), tc_status); -} - -test "execute requires type-checked query" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*GqldtDb = null; - _ = gqldt_db_open("test.db", 7, &db); - defer _ = gqldt_db_close(db.?); - - var query: ?*GqldtQuery = null; - _ = gqldt_parse("MATCH (n) RETURN n", 18, &query); - defer gqldt_query_free(query.?); - - // Attempt execution without type-checking — should fail. - var result: ?*GqldtResult = null; - const status = gqldt_execute(db.?, query.?, &result); - try testing.expectEqual(@intFromEnum(Status.type_mismatch), status); -} - -test "execute succeeds after typecheck" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*GqldtDb = null; - _ = gqldt_db_open("test.db", 7, &db); - defer _ = gqldt_db_close(db.?); - - var schema: ?*GqldtSchema = null; - _ = gqldt_get_schema(db.?, "users", &schema); - defer gqldt_schema_free(schema.?); - - var query: ?*GqldtQuery = null; - _ = gqldt_parse("MATCH (n) RETURN n", 18, &query); - defer gqldt_query_free(query.?); - - _ = gqldt_typecheck(query.?, schema.?); - - var result: ?*GqldtResult = null; - const exec_status = gqldt_execute(db.?, query.?, &result); - try testing.expectEqual(@intFromEnum(Status.ok), exec_status); - try testing.expect(result != null); - - gqldt_result_free(result.?); -} - -test "serialize_cbor and deserialize_cbor round-trip" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - const query_text: [*:0]const u8 = "MATCH (n) RETURN n"; - var query: ?*GqldtQuery = null; - _ = gqldt_parse(query_text, 18, &query); - defer gqldt_query_free(query.?); - - // Serialise to CBOR. - var cbor_buf: [1024]u8 = undefined; - var written: u64 = 0; - const ser_status = gqldt_serialize_cbor(query.?, &cbor_buf, 1024, &written); - try testing.expectEqual(@intFromEnum(Status.ok), ser_status); - try testing.expect(written > 0); - - // Deserialise from CBOR. - var query2: ?*GqldtQuery = null; - const deser_status = gqldt_deserialize_cbor(&cbor_buf, written, &query2); - try testing.expectEqual(@intFromEnum(Status.ok), deser_status); - try testing.expect(query2 != null); - - gqldt_query_free(query2.?); -} - -test "serialize_json produces valid wrapper" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var query: ?*GqldtQuery = null; - _ = gqldt_parse("RETURN 1", 8, &query); - defer gqldt_query_free(query.?); - - var json_buf: [1024]u8 = undefined; - var written: u64 = 0; - const status = gqldt_serialize_json(query.?, &json_buf, 1024, &written); - try testing.expectEqual(@intFromEnum(Status.ok), status); - - const json_str = json_buf[0..@intCast(written)]; - try testing.expectEqualStrings("{\"query\":\"RETURN 1\"}", json_str); -} - -test "version returns semantic version" { - const ver = gqldt_version(); - const ver_str = std.mem.span(ver); - try testing.expect(ver_str.len > 0); - try testing.expect(std.mem.count(u8, ver_str, ".") >= 1); -} diff --git a/ffi/zig/test/integration_test.zig b/ffi/zig/test/integration_test.zig deleted file mode 100644 index 8fc1d46..0000000 --- a/ffi/zig/test/integration_test.zig +++ /dev/null @@ -1,233 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (@hyperpolymath) -// -// GQL-DT Integration Tests -// -// These tests verify that the Zig FFI correctly implements the Idris2 ABI. -// They exercise the exported C-ABI functions end-to-end. - -const std = @import("std"); -const testing = std.testing; - -// Import FFI functions -extern fn gqldt_init() callconv(.c) i32; -extern fn gqldt_cleanup() callconv(.c) void; -extern fn gqldt_db_open(path: [*:0]const u8, path_len: u64, db_out: *?*anyopaque) callconv(.c) i32; -extern fn gqldt_db_close(db: *anyopaque) callconv(.c) i32; -extern fn gqldt_parse(query_str: [*:0]const u8, query_len: u64, query_out: *?*anyopaque) callconv(.c) i32; -extern fn gqldt_parse_inferred(query_str: [*:0]const u8, query_len: u64, schema: *anyopaque, query_out: *?*anyopaque) callconv(.c) i32; -extern fn gqldt_typecheck(query: *anyopaque, schema: *anyopaque) callconv(.c) i32; -extern fn gqldt_execute(db: *anyopaque, query: *anyopaque, result_out: *?*anyopaque) callconv(.c) i32; -extern fn gqldt_get_schema(db: *anyopaque, collection_name: [*:0]const u8, schema_out: *?*anyopaque) callconv(.c) i32; -extern fn gqldt_query_free(query: *anyopaque) callconv(.c) void; -extern fn gqldt_schema_free(schema: *anyopaque) callconv(.c) void; -extern fn gqldt_result_free(result: *anyopaque) callconv(.c) void; -extern fn gqldt_serialize_cbor(query: *anyopaque, buffer: [*]u8, buffer_len: u64, written_out: *u64) callconv(.c) i32; -extern fn gqldt_serialize_json(query: *anyopaque, buffer: [*]u8, buffer_len: u64, written_out: *u64) callconv(.c) i32; -extern fn gqldt_deserialize_cbor(buffer: [*]const u8, buffer_len: u64, query_out: *?*anyopaque) callconv(.c) i32; -extern fn gqldt_validate_permissions(query: *anyopaque, user_id: [*:0]const u8, permissions: *const anyopaque) callconv(.c) i32; -extern fn gqldt_version() callconv(.c) [*:0]const u8; -extern fn gqldt_alloc_slot() callconv(.c) ?*anyopaque; -extern fn gqldt_read_slot(slot: *anyopaque) callconv(.c) u64; -extern fn gqldt_free_slot(slot: *anyopaque) callconv(.c) void; -extern fn gqldt_bits64_to_ptr(value: u64) callconv(.c) ?*anyopaque; - -//============================================================================== -// Lifecycle Tests -//============================================================================== - -test "init and cleanup" { - const status = gqldt_init(); - try testing.expectEqual(@as(i32, 0), status); - gqldt_cleanup(); -} - -test "double init is idempotent" { - _ = gqldt_init(); - const status = gqldt_init(); - try testing.expectEqual(@as(i32, 0), status); - gqldt_cleanup(); -} - -//============================================================================== -// Database Operations -//============================================================================== - -test "db_open and db_close" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*anyopaque = null; - const open_status = gqldt_db_open("test.db", 7, &db); - try testing.expectEqual(@as(i32, 0), open_status); - try testing.expect(db != null); - - const close_status = gqldt_db_close(db.?); - try testing.expectEqual(@as(i32, 0), close_status); -} - -test "db_open rejects empty path" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*anyopaque = null; - const status = gqldt_db_open("", 0, &db); - try testing.expectEqual(@as(i32, 1), status); // invalid_arg -} - -test "db_open rejects oversized path" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*anyopaque = null; - const status = gqldt_db_open("x", 5000, &db); - try testing.expectEqual(@as(i32, 1), status); // invalid_arg -} - -//============================================================================== -// Query Parsing -//============================================================================== - -test "parse valid query" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var query: ?*anyopaque = null; - const status = gqldt_parse("MATCH (n:Person) RETURN n", 25, &query); - try testing.expectEqual(@as(i32, 0), status); - try testing.expect(query != null); - - gqldt_query_free(query.?); -} - -test "parse rejects empty query" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var query: ?*anyopaque = null; - const status = gqldt_parse("", 0, &query); - try testing.expectEqual(@as(i32, 1), status); // invalid_arg -} - -//============================================================================== -// Type Checking and Execution -//============================================================================== - -test "full pipeline: open -> schema -> parse -> typecheck -> execute" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - // Open database. - var db: ?*anyopaque = null; - _ = gqldt_db_open("pipeline.db", 11, &db); - defer gqldt_db_close(db.?); - - // Get schema. - var schema: ?*anyopaque = null; - _ = gqldt_get_schema(db.?, "nodes", &schema); - defer gqldt_schema_free(schema.?); - - // Parse query. - var query: ?*anyopaque = null; - _ = gqldt_parse("MATCH (n) RETURN n", 18, &query); - defer gqldt_query_free(query.?); - - // Type-check. - const tc_status = gqldt_typecheck(query.?, schema.?); - try testing.expectEqual(@as(i32, 0), tc_status); - - // Execute. - var result: ?*anyopaque = null; - const exec_status = gqldt_execute(db.?, query.?, &result); - try testing.expectEqual(@as(i32, 0), exec_status); - try testing.expect(result != null); - - gqldt_result_free(result.?); -} - -test "execute without typecheck fails" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var db: ?*anyopaque = null; - _ = gqldt_db_open("test.db", 7, &db); - defer gqldt_db_close(db.?); - - var query: ?*anyopaque = null; - _ = gqldt_parse("MATCH (n) RETURN n", 18, &query); - defer gqldt_query_free(query.?); - - var result: ?*anyopaque = null; - const status = gqldt_execute(db.?, query.?, &result); - try testing.expectEqual(@as(i32, 2), status); // type_mismatch -} - -//============================================================================== -// Serialization -//============================================================================== - -test "serialize to CBOR and back" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var query: ?*anyopaque = null; - _ = gqldt_parse("RETURN 42", 9, &query); - defer gqldt_query_free(query.?); - - var cbor_buf: [1024]u8 = undefined; - var written: u64 = 0; - const ser_status = gqldt_serialize_cbor(query.?, &cbor_buf, 1024, &written); - try testing.expectEqual(@as(i32, 0), ser_status); - try testing.expect(written > 0); - - var query2: ?*anyopaque = null; - const deser_status = gqldt_deserialize_cbor(&cbor_buf, written, &query2); - try testing.expectEqual(@as(i32, 0), deser_status); - try testing.expect(query2 != null); - - gqldt_query_free(query2.?); -} - -test "serialize to JSON" { - _ = gqldt_init(); - defer gqldt_cleanup(); - - var query: ?*anyopaque = null; - _ = gqldt_parse("RETURN 1", 8, &query); - defer gqldt_query_free(query.?); - - var json_buf: [1024]u8 = undefined; - var written: u64 = 0; - const status = gqldt_serialize_json(query.?, &json_buf, 1024, &written); - try testing.expectEqual(@as(i32, 0), status); - - const json_str = json_buf[0..@intCast(written)]; - try testing.expectEqualStrings("{\"query\":\"RETURN 1\"}", json_str); -} - -//============================================================================== -// Slot Allocation Helpers -//============================================================================== - -test "alloc_slot and free_slot" { - const slot = gqldt_alloc_slot() orelse return error.SlotAllocFailed; - const value = gqldt_read_slot(slot); - try testing.expectEqual(@as(u64, 0), value); // initially zero - gqldt_free_slot(slot); -} - -test "bits64_to_ptr null returns null" { - const ptr = gqldt_bits64_to_ptr(0); - try testing.expect(ptr == null); -} - -//============================================================================== -// Version -//============================================================================== - -test "version string is semantic version" { - const ver = gqldt_version(); - const ver_str = std.mem.span(ver); - try testing.expect(ver_str.len > 0); - try testing.expect(std.mem.count(u8, ver_str, ".") >= 1); -} diff --git a/mise.toml b/mise.toml index e02f506..01ef2cb 100644 --- a/mise.toml +++ b/mise.toml @@ -18,8 +18,8 @@ # Zig — builds the FFI bridge in bridge/ that Lean links against # (`lakefile.lean`: -Lbridge/zig-out/lib -llith_bridge). # 0.16.0 verified: `bridge/` builds clean and `zig build test` passes. -# NB the stale skeletons in bridge/zig/ and ffi/zig/ use the pre-0.15 Build API -# and do NOT compile under this version — see issue notes in the PR. +# `bridge/` is the only Zig tree; the pre-0.15-API skeletons that used to sit in +# bridge/zig/ and ffi/zig/ were removed (they could not compile under 0.16). zig = "0.16.0" # Idris2 — the ABI layer, src/GQLdt/ABI/{Types,Layout,Foreign}.idr, diff --git a/selur-compose.yml b/selur-compose.yml index f8cf987..50d704c 100644 --- a/selur-compose.yml +++ b/selur-compose.yml @@ -15,7 +15,7 @@ services: volumes: - .:/workspace - lean-cache:/root/.elan - - zig-cache:/workspace/bridge/zig/.zig-cache + - zig-cache:/workspace/bridge/.zig-cache working_dir: /workspace stdin_open: true tty: true From c5d78f7d012e00efc3e50cd5786eccd2822d4127 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:27:46 +0100 Subject: [PATCH 2/2] fix(ci): grant `actions: read` so the governance reusable can start MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Governance began returning `startup_failure` with ZERO jobs on this branch, despite `.github/` being byte-identical to main. Not caused by the Zig cleanup. Root cause, measured: standards@0ced540e "chore: estate-wide security compliance" (2026-07-26) added `actions: read` to governance-reusable.yml's own `permissions:` block. A called reusable workflow cannot request MORE permissions than its caller grants. This caller granted only `contents: read`, so GitHub rejected the run before any job started — which is why there are zero jobs and no check run to click into. This caller pins the reusable at `@main`, not a SHA, so the upstream change arrived the moment it landed. Timeline: gnpl Governance was green 2026-07-21, the reusable changed 2026-07-26T13:53Z, and the next gnpl run (today) failed. hyperpolymath/standards' own main is red for the same reason, so this is estate-wide rather than local — filed upstream. Fix is to mirror the permission. Unrelated to the rest of this PR, but it blocks every PR in the repo, so it is folded in here rather than queued. Co-Authored-By: Claude Opus 5 --- .github/workflows/governance.yml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index b0b1ed6..d54748b 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -18,7 +18,17 @@ on: pull_request: workflow_dispatch: +# A called reusable workflow cannot request MORE permissions than its caller +# grants — if it does, the run is rejected before any job starts +# (startup_failure, zero jobs, no check run to inspect). +# +# standards@0ced540e ("chore: estate-wide security compliance", 2026-07-26) +# added `actions: read` to governance-reusable.yml's own permissions block. +# Because this caller pins the reusable at @main rather than a SHA, that change +# arrived immediately and broke Governance here. `actions: read` is mirrored +# below to match. permissions: + actions: read contents: read jobs: