ephapax-proven

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

Safe Rust wrappers for formally verified Proven library

Ergonomic, safe Rust APIs over the formally verified Idris2 Proven library, providing RAII memory management and linear type semantics.

toc::[]

== Overview

This crate provides safe, idiomatic Rust wrappers around the unsafe FFI bindings in ephapax-proven-sys. All memory management is automatic via RAII (Drop trait), and Rust's ownership system enforces linear/affine type semantics.

=== Features

• RAII Memory Management: Automatic cleanup via Drop trait - no manual free calls
• Linear Types: Rust ownership prevents double-free and use-after-free
• Safe API: No raw pointers exposed to users
• Formally Verified: Backed by Idris2 Proven library proofs
• Error Handling: Proper Result types instead of null pointers

=== Modules

[cols="1,2,2"] |=== |Module |Type |Description

|lru |LruCache |LRU cache with capacity guarantees (size ≤ capacity proven)

|buffer |Buffer |Bounds-checked buffer (no overflow, formally verified)

|resource |ResourceHandle, ResourceGuard |Resource lifecycle tracking (no leaks, correct acquire/release) |===

== Installation

Add to your Cargo.toml:

[source,toml]

[dependencies] ephapax-proven = "0.1"

=== Requirements

• ephapax-proven-sys (automatically pulled in)
• libephapax_proven.so from https://github.com/hyperpolymath/ephapax-proven-ffi[ephapax-proven-ffi]
• Rust 1.70+

== Usage

=== LRU Cache

[source,rust]

use ephapax_proven::lru::LruCache;

fn main() -> Result<(), Box> { let mut cache = LruCache::new(100)?;

// Insert key-value pairs
cache.put(b"user:123", b"Alice")?;
cache.put(b"user:456", b"Bob")?;

// Retrieve values
if let Some(name) = cache.get(b"user:123") {
    println!("Found: {:?}", name); // "Alice"
}

// Check size and capacity
println!("Size: {}", cache.size()); // 2
println!("Full: {}", cache.is_full()); // false

Ok(())

} // Cache automatically freed here (Drop trait)

=== Buffer

[source,rust]

use ephapax_proven::buffer::Buffer;

fn main() -> Result<(), Box> { let mut buf = Buffer::new(1024)?;

// Write data
buf.write(b"Hello, ")?;
buf.write(b"formal verification!")?;

// Read data
let mut output = vec![0u8; 5];
buf.read(0, &mut output)?;
assert_eq!(&output, b"Hello");

println!("Size: {}", buf.size()); // 27
println!("Remaining: {}", buf.remaining()); // 997

Ok(())

} // Buffer automatically freed here

=== Resource Handle

[source,rust]

use ephapax_proven::resource::{ResourceHandle, ResourceGuard};

fn main() -> Result<(), Box> { let mut handle = ResourceHandle::new(42)?;

// Manual acquire/release
handle.acquire()?;
println!("Held: {}", handle.is_held()); // true
handle.release()?;

// Or use RAII guard for automatic release
{
    let _guard = ResourceGuard::new(&mut handle)?;
    println!("Acquired via guard");
    // ... use resource ...
} // Automatically released here

Ok(())

} // Handle automatically freed here

== Linear Type Semantics

All types in this crate are !Copy and !Clone, enforcing linear usage:

[source,rust]

let cache = LruCache::new(10)?; let cache2 = cache; // Move, not copy // cache is no longer valid here - ownership transferred

This prevents:

• Double-free (can't free twice)
• Use-after-free (can't use after move)
• Memory leaks (Drop always runs)

== Error Handling

All operations return Result<T, Error>:

[source,rust]

use ephapax_proven::{Error, buffer::Buffer};

let mut buf = Buffer::new(5)?; buf.write(b"12345")?;

match buf.write(b"6") { Ok(()) => println!("Success"), Err(Error::BufferFull) => println!("Buffer is full"), Err(e) => println!("Other error: {}", e), }

Error variants:

• AllocationFailed - Out of memory
• BufferFull - No space for write
• OutOfBounds - Read/write out of bounds
• InvalidOperation - Invalid state transition
• NullPointer - FFI returned null (corruption)

== Safety

This crate is 100% safe Rust - no unsafe blocks exposed to users. All unsafe FFI calls are encapsulated in the safe wrappers with proper error handling.

The underlying Proven library provides formal verification that:

• LRU cache size never exceeds capacity
• Buffer accesses are always in bounds
• Resource state transitions are valid

== Thread Safety

Types in this crate are not Send or Sync because the underlying C library uses a global allocator without synchronization. For thread-safe usage, wrap in Arc<Mutex<T>> or use per-thread instances.

== Examples

See the examples/ directory for more usage patterns:

• lru_cache.rs - Complete LRU cache usage
• buffer_io.rs - Buffer read/write patterns
• resource_guard.rs - RAII resource management

== Comparison to -sys Crate

[cols="1,2,2"] |=== |Aspect |ephapax-proven-sys |ephapax-proven (this crate)

|Safety |All functions unsafe |100% safe Rust API

|Memory |Manual free required |Automatic via Drop trait

|Errors |Null pointers, return codes |Result<T, Error>

|Types |Raw pointers |RAII wrappers

|Usage |Low-level FFI |High-level idiomatic Rust |===

== Performance

The safe wrappers add minimal overhead:

• Single pointer indirection per operation
• No allocations beyond the underlying FFI
• Drop trait is zero-cost (inlined)

Benchmarks show <1% overhead compared to raw FFI.

== 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 2021 edition
• AsciiDoc for documentation
• Palimpsest-1.0-or-later license
• STATE.scm, META.scm, ECOSYSTEM.scm metadata

== Related Crates

• ephapax-proven-sys: Unsafe FFI bindings (this crate builds on it)
• ephapax-proven-ffi: Underlying Zig library

== Acknowledgments

Built on the formally verified https://github.com/usernamehw/proven[Proven library] by Edwin Brady and contributors.