Skip to content

ABI-FFI-README.md

Latest commit

 

History

History
385 lines (295 loc) · 9.38 KB

ABI-FFI-README.md

File metadata and controls

385 lines (295 loc) · 9.38 KB

{{~ Aditionally delete this line and fill out the template below ~}}

{{PROJECT}} ABI/FFI Documentation

Overview

This library follows the Hyperpolymath RSR Standard for ABI and FFI design:

  • 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

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:

-- 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:

-- 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:

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:

-- 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:

export fn library_function(param: i32) i32 {
    return param * 2;
}

2. Memory Safety

Compile-time safety without runtime overhead:

// Null check enforced at compile time
const handle = init() orelse return error.InitFailed;
defer free(handle);

3. Cross-Compilation

Built-in cross-compilation to any platform:

zig build -Dtarget=x86_64-linux
zig build -Dtarget=aarch64-macos
zig build -Dtarget=x86_64-windows

4. Zero Dependencies

No runtime, no libc required (unless explicitly needed):

// Minimal binary size
pub const lib = @import("std");
// Only includes what you use

Building

Build FFI Library

cd ffi/zig
zig build                         # Build debug
zig build -Doptimize=ReleaseFast  # Build optimized
zig build test                    # Run tests

Generate C Header from Idris2 ABI

cd src/abi
idris2 --cg c-header Types.idr -o ../../generated/abi/{{project}}.h

Cross-Compile

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

#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:

gcc -o example example.c -l{{project}} -L./zig-out/lib

From Idris2

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

#[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);

        {{project}}_free(handle);
    }
}

From 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)

cd ffi/zig
zig build test

Integration Tests

cd ffi/zig
zig build test-integration

ABI Verification (Idris2)

-- Compile-time verification
%runElab verifyABI

-- Runtime checks
main : IO ()
main = do
  verifyLayoutsCorrect
  verifyAlignmentsCorrect
  putStrLn "ABI verification passed"

Contributing

When modifying the ABI/FFI:

  1. Update ABI first (src/abi/*.idr)

    • Modify type definitions
    • Update proofs
    • Ensure backward compatibility

  2. Generate C header

    idris2 --cg c-header src/abi/Types.idr -o generated/abi/{{project}}.h

  3. Update FFI implementation (ffi/zig/src/main.zig)

    • Implement new functions
    • Match ABI types exactly

  4. Add tests

    • Unit tests in Zig
    • Integration tests
    • ABI verification tests

  5. Update documentation

    • Function signatures
    • Usage examples
    • Migration guide (if breaking changes)

License

PMPL-1.0-or-later

See Also