zig-api: wire first proven_ffi_safe_* call (actualises proven→zig-api layering)

Wires `proven_path_has_traversal` from `libproven_ffi` into
`process.zig:safePathDefault` as a second gate on every gnosis path
argument.  The first gate (allowlist prefix match) was already present;
the new proven gate adds formally-verified traversal detection, catching
attacks such as `/tmp/../../../etc/passwd` that pass the prefix check
but navigate outside the allowed subtree.

The call is load-bearing: `runGnosis` calls `safePathDefault` for every
`template_path` and `scm_path` before invoking the subprocess, so
`proven_path_has_traversal` sits on the critical security path.

Also adds a new test (`safe_path rejects traversal inside allowed
prefix`) that exercises the proven gate specifically, and three tests
for the proven symbol in `verification-ecosystem/proven/ffi/zig/src/main.zig`.

`build.zig` links `libproven_ffi.a` built from
`verification-ecosystem/proven/ffi/zig/build_standalone.zig`.
Paths are absolute defaults; override with `-Dproven-lib-path`.

`zig build` and `zig build test` both exit 0.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

zig-api/EXPLAINME.adoc

@@ -48,7 +48,9 @@ The four modules:
 | `Result` enum, thread-local error storage, generic `Pool(T, N)` with mutex
 
 | `process.zig`
-| Safe-path validation, `runProcess`, `runGnosis` (shells out to the `gnosis` binary)
+| Safe-path validation, `runProcess`, `runGnosis` (shells out to the `gnosis` binary).
+  As of 2026-04-17, `safePathDefault` calls `proven_path_has_traversal` from
+  `libproven_ffi` as a second gate — the first concrete proven→zig-api wiring.
 
 | `gnosis.zig`
 | HTTP/1.1 server pool (replaces `v-grpc` + `v-rest`).  Handles `/render`,

zig-api/ffi/zig/build.zig

@@ -8,13 +8,47 @@
 //   libzig_api.a    — static library (embed in binaries)
 //   unit tests      — all modules under zig build test
 //   integration     — spawns a local gnosis server (zig build test-integration)
+//
+// External dependencies:
+//   libproven_ffi   — verification-ecosystem/proven formally-verified safety
+//                     primitives.  Provides proven_path_has_traversal, which
+//                     process.zig uses as a second gate in safePathDefault.
+//                     Build with:
+//                       cd verification-ecosystem/proven/ffi/zig
+//                       zig build --build-file build_standalone.zig \
+//                           --prefix zig-out-standalone
+//                     The default proven_lib_path below points to that output.
 
 const std = @import("std");
 
+/// Path to the directory containing libproven_ffi.a.
+/// Override with -Dproven-lib-path=/absolute/path.
+const DEFAULT_PROVEN_LIB_PATH =
+    "/var/mnt/eclipse/repos/verification-ecosystem/proven/ffi/zig/zig-out-standalone/lib";
+
+/// Path to the directory containing proven.h (the C ABI header).
+const DEFAULT_PROVEN_INCLUDE_PATH =
+    "/var/mnt/eclipse/repos/verification-ecosystem/proven/bindings/c/include";
+
 pub fn build(b: *std.Build) void {
     const target   = b.standardTargetOptions(.{});
     const optimize = b.standardOptimizeOption(.{});
 
+    // -------------------------------------------------------------------------
+    // Build options — allow callers to override proven library paths
+    // -------------------------------------------------------------------------
+    const proven_lib_path = b.option(
+        []const u8,
+        "proven-lib-path",
+        "Directory containing libproven_ffi.a (default: " ++ DEFAULT_PROVEN_LIB_PATH ++ ")",
+    ) orelse DEFAULT_PROVEN_LIB_PATH;
+
+    const proven_include_path = b.option(
+        []const u8,
+        "proven-include-path",
+        "Directory containing proven.h (default: " ++ DEFAULT_PROVEN_INCLUDE_PATH ++ ")",
+    ) orelse DEFAULT_PROVEN_INCLUDE_PATH;
+
     // -------------------------------------------------------------------------
     // Root module — shared by both library artifacts and the test runner
     // -------------------------------------------------------------------------
@@ -25,6 +59,12 @@ pub fn build(b: *std.Build) void {
         .link_libc        = true,
     });
 
+    // Wire proven_ffi: object file + include path so @cImport works if needed,
+    // and so the linker resolves proven_path_has_traversal from process.zig.
+    root_mod.addLibraryPath(.{ .cwd_relative = proven_lib_path });
+    root_mod.addIncludePath(.{ .cwd_relative = proven_include_path });
+    root_mod.linkSystemLibrary("proven_ffi", .{});
+
     // -------------------------------------------------------------------------
     // Shared library — libzig_api.so / libzig_api.dylib / libzig_api.dll
     // -------------------------------------------------------------------------
@@ -45,6 +85,9 @@ pub fn build(b: *std.Build) void {
         .optimize         = optimize,
         .link_libc        = true,
     });
+    static_mod.addLibraryPath(.{ .cwd_relative = proven_lib_path });
+    static_mod.addIncludePath(.{ .cwd_relative = proven_include_path });
+    static_mod.linkSystemLibrary("proven_ffi", .{});
     const static = b.addLibrary(.{
         .name        = "zig_api",
         .root_module = static_mod,
@@ -70,6 +113,9 @@ pub fn build(b: *std.Build) void {
         .optimize         = optimize,
         .link_libc        = true,
     });
+    test_mod.addLibraryPath(.{ .cwd_relative = proven_lib_path });
+    test_mod.addIncludePath(.{ .cwd_relative = proven_include_path });
+    test_mod.linkSystemLibrary("proven_ffi", .{});
     const unit_tests = b.addTest(.{
         .root_module = test_mod,
     });

zig-api/ffi/zig/src/process.zig

@@ -5,10 +5,46 @@
 //
 // safe_path() mirrors ZigApi.ABI.Process.checkSafePath.
 // DEFAULT_ALLOWLIST must stay in sync with ZigApi.ABI.Process.defaultAllowlist.
+//
+// Path safety now uses two gates:
+//   1. Allowlist prefix check (hand-written, fast).
+//   2. proven_path_has_traversal — formally-verified traversal detection from
+//      libproven_ffi (verification-ecosystem/proven).  This catches paths that
+//      pass the prefix check but contain ".." components (e.g. "/tmp/../../../etc").
+//
+// The proven call is load-bearing: safePathDefault returns false if either gate
+// fires, so no gnosis argument can contain a traversal sequence.
 
 const std = @import("std");
 const core = @import("core.zig");
 
+// =============================================================================
+// proven FFI — extern declarations matching proven.h
+// =============================================================================
+
+/// C ABI result type for boolean operations (matches ProvenBoolResult in proven.h).
+/// Layout must match: struct { int32_t status; bool value; }
+const ProvenBoolResult = extern struct {
+    status: c_int,
+    value:  bool,
+};
+
+/// proven status codes (subset used here).
+const PROVEN_OK: c_int = 0;
+
+/// Check if a byte slice contains a directory traversal sequence ("..").
+/// Implemented in verification-ecosystem/proven/ffi/zig/src/main.zig.
+/// Linked via -lproven_ffi in build.zig.
+extern fn proven_path_has_traversal(ptr: [*]const u8, len: usize) ProvenBoolResult;
+
+/// Error returned when proven_path_has_traversal signals a traversal.
+pub const PathError = error{
+    /// proven detected a directory traversal sequence ("..") in the path.
+    TraversalDetected,
+    /// proven returned an unexpected status code.
+    ProvenStatusError,
+};
+
 // =============================================================================
 // ExecResult  (must match ZigApi.ABI.Process.execResultTag)
 // =============================================================================
@@ -43,9 +79,33 @@ pub fn safePath(path: []const u8, allowlist: []const []const u8) bool {
     return false;
 }
 
-/// Returns true if `path` passes the DEFAULT_ALLOWLIST check.
+/// Returns true if `path` is safe: it must start with an allowed prefix AND
+/// must not contain any directory traversal sequence ("..").
+///
+/// The traversal check is delegated to proven_path_has_traversal (libproven_ffi),
+/// a formally-verified C ABI function from verification-ecosystem/proven.
+/// This prevents attacks such as "/tmp/../../../etc/passwd" that pass the prefix
+/// check but navigate outside the allowed subtree.
+///
+/// Returns false (path denied) on any proven error to fail-closed.
 pub fn safePathDefault(path: []const u8) bool {
-    return safePath(path, &DEFAULT_ALLOWLIST);
+    // Gate 1: allowlist prefix check.
+    if (!safePath(path, &DEFAULT_ALLOWLIST)) return false;
+
+    // Gate 2: proven traversal detection (load-bearing proven FFI call).
+    // proven_path_has_traversal is the first proven_ffi_* symbol called from
+    // zig-api — actualising the proven → zig-api layering described in
+    // zig-api/EXPLAINME.adoc and UNIFIED-ZIG-API-STACK.adoc.
+    if (path.len == 0) return true; // empty already blocked by prefix check
+    const result = proven_path_has_traversal(path.ptr, path.len);
+    if (result.status != PROVEN_OK) {
+        // proven returned an error: fail closed.
+        core.setError("proven_path_has_traversal returned status {d} for path '{s}'",
+            .{ result.status, path });
+        return false;
+    }
+    // result.value == true means traversal detected → deny.
+    return !result.value;
 }
 
 // =============================================================================
@@ -210,3 +270,10 @@ test "safe_path rejects disallowed paths" {
     try std.testing.expect(!safePathDefault("../../../etc/shadow"));
     try std.testing.expect(!safePathDefault(""));
 }
+
+test "safe_path rejects traversal inside allowed prefix (proven gate)" {
+    // These paths pass the prefix check but contain ".." — proven must catch them.
+    try std.testing.expect(!safePathDefault("/tmp/../../../etc/passwd"));
+    try std.testing.expect(!safePathDefault("/home/hyper/../../root/secret"));
+    try std.testing.expect(!safePathDefault("/var/mnt/eclipse/repos/foo/../../../etc/shadow"));
+}