ephapax-proven-sys

= ephapax-proven-sys :toc: :toc-placement!:

Raw Rust FFI bindings to ephapax-proven-ffi

Unsafe Rust bindings to the Zig-based FFI library bridging Ephapax (linear types) with Proven (dependent types).

toc::[]

== Overview

This is a -sys crate providing raw, unsafe FFI bindings to libephapax_proven.so. For safe, idiomatic Rust wrappers, see the ephapax-proven crate.

=== Features

• Raw C-compatible bindings to all FFI functions
• Zero-cost abstractions over Zig implementation
• Opaque types for FFI safety
• Comprehensive safety documentation

=== Supported Modules

[cols="1,2"] |=== |Module |Functions

|LRU Cache |7 functions: new, put, get, contains, size, is_full, free

|Buffer |8 functions: new, write, read, capacity, size, is_full, remaining, free

|Resource Handle |6 functions: new_handle, mark_acquired, mark_released, is_held, get_state, free_handle |===

== Installation

Add to your Cargo.toml:

[source,toml]

[dependencies] ephapax-proven-sys = "0.1"

=== Requirements

• libephapax_proven.so from https://github.com/hyperpolymath/ephapax-proven-ffi[ephapax-proven-ffi]
• Rust 1.70+ (for better FFI support)

=== Linking

By default, the build script looks for the library in ../ephapax-proven-ffi. Override with:

[source,bash]

export EPHAPAX_PROVEN_LIB=/path/to/ephapax-proven-ffi cargo build

== Usage

All functions are unsafe. You must ensure:

• Pointers are non-null and valid
• Memory is not freed while in use
• No data races (these are !Send and !Sync)

=== Example: LRU Cache

[source,rust]

use ephapax_proven_sys::*;

unsafe { let cache = idris_proven_lru_new(100); assert!(!cache.is_null());

let key = b"test_key";
let val = b"test_value";
let cache = idris_proven_lru_put(
    cache,
    key.as_ptr(), key.len() as u64,
    val.as_ptr(), val.len() as u64
);

assert_eq!(idris_proven_lru_size(cache), 1);

idris_proven_lru_free(cache);

}

=== Example: Buffer

[source,rust]

use ephapax_proven_sys::*;

unsafe { let buf = idris_proven_buffer_new(1024); assert!(!buf.is_null());

let data = b"Hello, formal verification!";
let result = idris_proven_buffer_write(
    buf,
    data.as_ptr(),
    data.len() as u64
);
assert_eq!(result, 0); // 0 = success

assert_eq!(idris_proven_buffer_size(buf), data.len() as u64);

idris_proven_buffer_free(buf);

}

=== Example: Resource Handle

[source,rust]

use ephapax_proven_sys::*; use std::time::{SystemTime, UNIX_EPOCH};

unsafe { let handle = idris_proven_resource_new_handle(42); assert!(!handle.is_null());

let timestamp = SystemTime::now()
    .duration_since(UNIX_EPOCH)
    .unwrap()
    .as_secs();

let handle = idris_proven_resource_mark_acquired(handle, timestamp);
assert!(idris_proven_resource_is_held(handle));

let state = idris_proven_resource_get_state(handle);
assert_eq!(state, ResourceState::Acquired as u32);

idris_proven_resource_free_handle(handle);

}

== Safety

This crate is unsafe by design. Every function has detailed safety documentation. Common pitfalls:

• Double-free: Calling *_free twice on the same pointer
• Use-after-free: Using a pointer after calling *_free
• Null dereference: Not checking if returned pointers are null
• Data races: Sharing mutable pointers across threads (types are not Send/Sync)

For safe wrappers with RAII and linear types, use ephapax-proven.

== API Reference

See https://docs.rs/ephapax-proven-sys[docs.rs] for full API documentation.

== Testing

Run tests with the library in the default location:

[source,bash]

cargo test

Or specify a custom location:

[source,bash]

export EPHAPAX_PROVEN_LIB=/path/to/lib cargo test

== Related Crates

• ephapax-proven: Safe Rust wrappers (recommended for most users)
• ephapax-proven-ffi: Underlying Zig library

== License

SPDX-License-Identifier: Palimpsest-1.0-or-later

Built on Mozilla Public License 2.0-or-later (MPL-2.0-or-later).

See https://github.com/hyperpolymath/palimpsest-license[Palimpsest License] for full text.

== Contributing

See link:CONTRIBUTING.adoc[] for guidelines.

This crate follows Hyperpolymath standards:

• Rust for systems integration
• AsciiDoc for documentation
• Palimpsest-1.0-or-later license
• STATE.scm, META.scm, ECOSYSTEM.scm metadata