Skip to content

ABI-FFI-README.adoc

Latest commit

 

History

History
387 lines (297 loc) · 9.53 KB

ABI-FFI-README.adoc

File metadata and controls

387 lines (297 loc) · 9.53 KB
Raw

ABI/FFI Standards

NEXTGEN_TYPING 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/interface/Abi/                         │
│  - Types.idr      (Type definitions)        │
│  - Layout.idr     (Memory layout proofs)    │
│  - Foreign.idr    (FFI declarations)        │
└─────────────────┬───────────────────────────┘
                  │
                  │ generates (at compile time)
                  ▼
┌─────────────────────────────────────────────┐
│  C Headers (auto-generated)                 │
│  generated/abi/nextgen_typing.h                │
└─────────────────┬───────────────────────────┘
                  │
                  │ imported by
                  ▼
┌─────────────────────────────────────────────┐
│  FFI Implementation (Zig)                   │
│  ffi/zig/src/main.zig                       │
│  - Implements C-compatible functions        │
│  - Zero-cost abstractions                   │
│  - Memory-safe by default                   │
└─────────────────┬───────────────────────────┘
                  │
                  │ compiled to libnextgen_typing.so/.a
                  ▼
┌─────────────────────────────────────────────┐
│  Any Language via C ABI                     │
│  - Rust, ReScript, Julia, Python, etc.     │
└─────────────────────────────────────────────┘

Directory Structure

nextgen_typing/
├── src/
│   └── interface/
│       └── 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/
│           └── nextgen_typing.h   # C header (optional, can be generated)
│
├── generated/                  # Auto-generated files
│   └── abi/
│       └── nextgen_typing.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/interface/Abi
idris2 --cg c-header Types.idr -o ../../../generated/abi/nextgen_typing.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 "nextgen_typing.h"

int main() {
    void* handle = nextgen_typing_init();
    if (!handle) return 1;

    int result = nextgen_typing_process(handle, 42);
    if (result != 0) {
        const char* err = nextgen_typing_last_error();
        fprintf(stderr, "Error: %s\n", err);
    }

    nextgen_typing_free(handle);
    return 0;
}

Compile with:

gcc -o example example.c -lnextgen_typing -L./zig-out/lib

From Idris2

import NEXTGEN_TYPING.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 = "nextgen_typing")]
extern "C" {
    fn nextgen_typing_init() -> *mut std::ffi::c_void;
    fn nextgen_typing_free(handle: *mut std::ffi::c_void);
    fn nextgen_typing_process(handle: *mut std::ffi::c_void, input: u32) -> i32;
}

fn main() {
    unsafe {
        let handle = nextgen_typing_init();
        assert!(!handle.is_null());

        let result = nextgen_typing_process(handle, 42);
        assert_eq!(result, 0);

        nextgen_typing_free(handle);
    }
}

From Julia

const libnextgen_typing = "libnextgen_typing"

function init()
    handle = ccall((:nextgen_typing_init, libnextgen_typing), Ptr{Cvoid}, ())
    handle == C_NULL && error("Failed to initialize")
    handle
end

function process(handle, input)
    result = ccall((:nextgen_typing_process, libnextgen_typing), Cint, (Ptr{Cvoid}, UInt32), handle, input)
    result
end

function cleanup(handle)
    ccall((:nextgen_typing_free, libnextgen_typing), 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/interface/Abi/*.idr)

    • Modify type definitions

    • Update proofs

    • Ensure backward compatibility

  2. Generate C header bash idris2 --cg c-header src/interface/Abi/Types.idr -o generated/abi/nextgen_typing.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

{{LICENSE}}

See Also