Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
41 lines (30 loc) · 1.07 KB

EXPLAINME.adoc

File metadata and controls

41 lines (30 loc) · 1.07 KB

ffmpeg-ffi — EXPLAINME

Zig FFI Bindings for FFmpeg with Formally Verified ABI Definitions in Idris2

Zig FFI bindings for FFmpeg multimedia libraries (libavformat, libavcodec, libavutil, swresample, swscale), with formally verified ABI definitions in Idris2.

— README.adoc

The repo follows the hyperpolymath ABI/FFI Universal Standard: Idris2 defines the ABI with dependent-type proofs for memory layout and alignment, Zig provides the C-compatible FFI, and a thin Rust shim handles FFmpeg opaque struct field access. See src/abi/Layout.idr for the memory layout proofs.

Evidence

Path Proves

src/abi/Types.idr

Idris2 ABI type definitions exist

src/abi/Layout.idr

Memory layout proofs are present

src/abi/Foreign.idr

FFI function declarations are formally specified

src/main.zig

Core Zig FFmpeg bindings with C FFI exports

ffi/zig/

Generic Zig FFI template implementation

shim/src/lib.rs

Rust shim for opaque struct field access