lean_bindings.zig

// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
//! Lean 4 FFI Bindings for Zig
//!
//! This module provides Zig bindings to Lean 4 compiled verification code.
//! It bridges formally verified Lean 4 theorems to Zig via C FFI.
//!
//! Architecture:
//!   Lean 4 Proofs → C Code (Lean compiler) → Zig FFI (this file) → Zig App
//!
//! TRUST CHAIN:
//!   ✓ Lean 4 proofs (HIGH TRUST - formally verified)
//!   ✓ Lean → C compiler (MEDIUM TRUST - standard Lean compiler)
//!   ✓ C → Zig FFI (MEDIUM TRUST - type-safe bindings)
//!   ⚠ POSIX operations (LOW TRUST - OS dependent)

const std = @import("std");

// ============================================================================
// C Types from Lean Runtime
// ============================================================================

/// Opaque Lean object pointer (reference-counted)
pub const LeanObject = opaque {};

/// Lean filesystem handle (abstract state)
pub const LeanFilesystem = opaque {};

/// Error codes matching Lean CErrorCode type
pub const LeanError = enum(c_int) {
    no_error = 0,
    eexist = 17, // File exists
    enoent = 2, // No such file or directory
    eacces = 13, // Permission denied
    enotdir = 20, // Not a directory
    eisdir = 21, // Is a directory
    enotempty = 39, // Directory not empty

    pub fn toPosixError(self: LeanError) @import("lib.zig").PosixError {
        return switch (self) {
            .no_error => .success,
            .eexist => .eexist,
            .enoent => .enoent,
            .eacces => .eacces,
            .enotdir => .enotdir,
            .eisdir => .eisdir,
            .enotempty => .enotempty,
        };
    }
};

/// Result type from Lean operations
pub const LeanResult = extern struct {
    success: bool,
    error_code: LeanError,
};

// ============================================================================
// C Function Declarations (from lean_wrapper.c)
// ============================================================================

extern "c" fn vsh_filesystem_create(root: [*:0]const u8) ?*LeanFilesystem;
extern "c" fn vsh_filesystem_destroy(fs: *LeanFilesystem) void;

extern "c" fn vsh_safe_mkdir(fs: *LeanFilesystem, path: [*:0]const u8) LeanResult;
extern "c" fn vsh_safe_rmdir(fs: *LeanFilesystem, path: [*:0]const u8) LeanResult;
extern "c" fn vsh_safe_create_file(fs: *LeanFilesystem, path: [*:0]const u8) LeanResult;
extern "c" fn vsh_safe_delete_file(fs: *LeanFilesystem, path: [*:0]const u8) LeanResult;

extern "c" fn vsh_get_version() [*:0]const u8;

// ============================================================================
// Zig-Friendly Wrappers
// ============================================================================

/// Lean-verified filesystem handle
pub const VerifiedFilesystem = struct {
    handle: *LeanFilesystem,
    allocator: std.mem.Allocator,

    /// Create a new verified filesystem handle
    ///
    /// Returns null if creation fails (e.g., invalid root path)
    pub fn init(allocator: std.mem.Allocator, root: []const u8) !VerifiedFilesystem {
        // Ensure null-terminated for C
        const root_z = try allocator.dupeZ(u8, root);
        defer allocator.free(root_z);

        const handle = vsh_filesystem_create(root_z) orelse return error.InitFailed;

        return VerifiedFilesystem{
            .handle = handle,
            .allocator = allocator,
        };
    }

    /// Destroy the filesystem handle
    pub fn deinit(self: *VerifiedFilesystem) void {
        vsh_filesystem_destroy(self.handle);
    }

    /// Check mkdir preconditions using Lean-verified code
    ///
    /// This calls into formally verified Lean 4 logic that checks:
    /// 1. Path does not exist
    /// 2. Parent directory exists
    /// 3. Parent is a directory
    /// 4. Parent is writable
    ///
    /// Returns Ok(void) if preconditions are satisfied, Error otherwise.
    pub fn checkMkdirPreconditions(self: *VerifiedFilesystem, path: []const u8) !void {
        const path_z = try self.allocator.dupeZ(u8, path);
        defer self.allocator.free(path_z);

        const result = vsh_safe_mkdir(self.handle, path_z);

        if (!result.success) {
            return result.error_code.toPosixError().toError();
        }
    }

    /// Check rmdir preconditions using Lean-verified code
    ///
    /// Verifies:
    /// 1. Path exists and is a directory
    /// 2. Directory is empty
    /// 3. Not removing root directory
    pub fn checkRmdirPreconditions(self: *VerifiedFilesystem, path: []const u8) !void {
        const path_z = try self.allocator.dupeZ(u8, path);
        defer self.allocator.free(path_z);

        const result = vsh_safe_rmdir(self.handle, path_z);

        if (!result.success) {
            return result.error_code.toPosixError().toError();
        }
    }

    /// Check file creation preconditions using Lean-verified code
    ///
    /// Verifies:
    /// 1. Path does not exist
    /// 2. Parent directory exists
    pub fn checkCreateFilePreconditions(self: *VerifiedFilesystem, path: []const u8) !void {
        const path_z = try self.allocator.dupeZ(u8, path);
        defer self.allocator.free(path_z);

        const result = vsh_safe_create_file(self.handle, path_z);

        if (!result.success) {
            return result.error_code.toPosixError().toError();
        }
    }

    /// Check file deletion preconditions using Lean-verified code
    ///
    /// Verifies:
    /// 1. Path exists
    /// 2. Path is a file (not a directory)
    pub fn checkDeleteFilePreconditions(self: *VerifiedFilesystem, path: []const u8) !void {
        const path_z = try self.allocator.dupeZ(u8, path);
        defer self.allocator.free(path_z);

        const result = vsh_safe_delete_file(self.handle, path_z);

        if (!result.success) {
            return result.error_code.toPosixError().toError();
        }
    }
};

/// Get Lean FFI library version
pub fn getVersion() []const u8 {
    const c_str = vsh_get_version();
    return std.mem.span(c_str);
}

// Helper to convert PosixError to Zig error
fn posixErrorToZigError(err: @import("lib.zig").PosixError) anyerror {
    return switch (err) {
        .success => unreachable,
        .eexist => error.PathAlreadyExists,
        .enoent => error.FileNotFound,
        .eacces => error.AccessDenied,
        .enotdir => error.NotDir,
        .eisdir => error.IsDir,
        .enotempty => error.DirNotEmpty,
        else => error.Unexpected,
    };
}

// Extension method for PosixError
const PosixError = @import("lib.zig").PosixError;
fn posixErrorToError(self: PosixError) anyerror {
    return switch (self) {
        .success => unreachable,
        .eexist => error.PathAlreadyExists,
        .enoent => error.FileNotFound,
        .eacces => error.AccessDenied,
        .enotdir => error.NotDir,
        .eisdir => error.IsDir,
        .enotempty => error.DirNotEmpty,
        .einval => error.InvalidArgument,
        .enomem => error.OutOfMemory,
        .eio => error.InputOutput,
        .eloop => error.SymLinkLoop,
        .enametoolong => error.NameTooLong,
    };
}

// ============================================================================
// Integration Example
// ============================================================================

/// Example: Verified mkdir operation
///
/// This combines:
/// 1. Lean-verified precondition checking (from this module)
/// 2. Real POSIX mkdir operation (from std.fs)
///
/// Result: Mathematical guarantee on preconditions, real execution
pub fn verifiedMkdir(fs: *VerifiedFilesystem, path: []const u8) !void {
    // Step 1: Check preconditions using Lean-verified code
    try fs.checkMkdirPreconditions(path);

    // Step 2: Preconditions satisfied, execute real operation
    try std.fs.cwd().makeDir(path);

    // Success! The operation was:
    // - Verified safe by formal proofs (Lean 4)
    // - Actually executed (POSIX)
}

// ============================================================================
// Tests
// ============================================================================

test "lean bindings basic" {
    const testing = std.testing;
    const allocator = testing.allocator;

    // Create verified filesystem
    var vfs = try VerifiedFilesystem.init(allocator, "/tmp/vsh_test");
    defer vfs.deinit();

    // Test 1: Version string
    const version = getVersion();
    try testing.expect(version.len > 0);

    // Test 2: Valid mkdir should pass precondition check
    // (assuming /tmp/vsh_test exists and /tmp/vsh_test/new_dir does not)
    // This is a smoke test - real tests need controlled environment
}

test "verified mkdir integration" {
    const testing = std.testing;
    const allocator = testing.allocator;

    // Set up test directory
    const test_root = "/tmp/vsh_zig_test";
    std.fs.cwd().makeDir(test_root) catch |err| switch (err) {
        error.PathAlreadyExists => {}, // OK if already exists
        else => return err,
    };
    defer std.fs.cwd().deleteTree(test_root) catch {};

    // Create verified filesystem
    var vfs = try VerifiedFilesystem.init(allocator, test_root);
    defer vfs.deinit();

    // Test verified mkdir
    const test_path = "/tmp/vsh_zig_test/verified_dir";

    // Should succeed (path doesn't exist, parent exists)
    try verifiedMkdir(&vfs, test_path);

    // Verify directory was created
    var dir = try std.fs.cwd().openDir(test_path, .{});
    dir.close();

    // Clean up
    try std.fs.cwd().deleteDir(test_path);
}

// ============================================================================
// Documentation
// ============================================================================

/// USAGE GUIDE
/// ============
///
/// Basic Usage:
/// ```zig
/// const lean = @import("lean_bindings.zig");
///
/// // Initialize verified filesystem
/// var vfs = try lean.VerifiedFilesystem.init(allocator, "/tmp/vsh");
/// defer vfs.deinit();
///
/// // Check preconditions before operation
/// try vfs.checkMkdirPreconditions("/tmp/vsh/new_dir");
///
/// // Execute operation (preconditions guaranteed satisfied)
/// try std.fs.cwd().makeDir("/tmp/vsh/new_dir");
/// ```
///
/// Integration with Existing Code:
/// ```zig
/// // In lib.zig, replace manual precondition checks:
///
/// // OLD (manual checking):
/// if (!preconditions.checkMkdirPreconditions(path)) {
///     return .{ .err = .eexist };
/// }
///
/// // NEW (Lean-verified checking):
/// vfs.checkMkdirPreconditions(path) catch |err| {
///     return .{ .err = PosixError.fromError(err) };
/// };
/// ```
///
/// TRUST CHAIN
/// ===========
///
/// This module establishes the following trust chain:
///
/// 1. Lean 4 Proofs (HIGH TRUST)
///    - ~256 theorems proven across 6 systems
///    - Formal guarantees on reversibility, composition
///    - Independently verified by different proof assistants
///
/// 2. Lean → C Compiler (MEDIUM TRUST)
///    - Standard Lean 4 compiler
///    - Well-tested, widely used
///    - Extraction preserves semantics
///
/// 3. C → Zig FFI (MEDIUM TRUST)
///    - Type-safe bindings (this file)
///    - Explicit error handling
///    - Memory-safe (no raw pointers exposed)
///
/// 4. POSIX Operations (LOW TRUST)
///    - OS-dependent behavior
///    - Kernel guarantees only
///    - Not formally verified
///
/// RESULT: Mathematical guarantees on preconditions + Real execution
///
/// BUILDING
/// ========
///
/// See docs/ZIG_LEAN_EXTRACTION.md for complete build instructions.
///
/// Quick start:
/// ```bash
/// # 1. Build Lean proofs
/// cd proofs/lean4 && lake build Extraction
///
/// # 2. Build C wrapper
/// cd ../../impl/ocaml && make lean_wrapper
///
/// # 3. Build Zig with Lean integration
/// cd ../zig && zig build -Dlean-verified=true
/// ```