| # NraayTensor FFI Contract |
|
|
| ## Overview |
|
|
| The FFI layer provides a **C-compatible ABI** that bridges: |
| - **Rust `tensor.rs`** (production hardware layer) |
| - **Free Pascal** (reference implementation & oracle) |
| - **Formal verification** (Kani proofs for correctness) |
|
|
| All operations are defined through a canonical binary protocol (`tensor_abi.h`) that both implementations must conform to. |
|
|
| --- |
|
|
| ## Files |
|
|
| ### C ABI Definition |
| - **`tensor_abi.h`** β Canonical C-compatible tensor descriptor and operation signatures |
| - `TensorDescriptorC`: packed struct with buffer identity, rank, governance, ownership, generation |
| - Operations: `tensor_allocate`, `tensor_view`, `tensor_materialize`, `tensor_load`, `tensor_store`, etc. |
| |
| ### Rust Implementation |
| - **`tensor_ffi.rs`** β Rust FFI layer that wraps the real `tensor.rs` implementation |
| - Global registry (`TENSOR_REGISTRY`) maps buffer IDs to actual tensor data |
| - Arc-based ownership semantics are preserved through FFI boundary |
| - Every operation maps directly to tensor logic (no translation layer) |
|
|
| ### Pascal Bindings |
| - **`tensor_abi.pas`** β Free Pascal FFI wrapper (calls into Rust via C ABI) |
| - Pascal-idiomatic error handling with exception raising |
| - Thin wrappers around C FFI calls |
| - Same semantic contract as Rust |
| |
| ### Sparse Router (Work-Stealing) |
| - **`sparse_router.rs`** β RAW_ROUTE algorithm for tensor task scheduling |
| - Memory-locality-aware work stealing |
| - Region ownership tracking |
| - Topology-aware routing decisions |
| |
| - **`sparse_router_kani.rs`** β Formal verification of router invariants |
| - 8 proven theorems about routing correctness |
| - Kani proofs: all tasks routed, locality preserved, no deadlock, migration cost minimized |
| |
| ### Conformance Testing |
| - **`conformance_bridge.rs`** β Cross-language validation harness |
| - Rust tests that exercise the FFI |
| - Oracle functions for descriptor comparison |
| - Both Rust and Pascal implementations must produce identical results |
| |
| --- |
| |
| ## Core Tensor Descriptor (ABI Contract) |
| |
| ```c |
| typedef struct { |
| uint64_t buffer_id; /* Unique buffer identity */ |
| uint64_t base_addr; /* Physical address */ |
| uint64_t offset; /* Offset into buffer */ |
| |
| uint32_t rank; /* Tensor rank (# dimensions) */ |
| uint64_t element_count; /* Total elements */ |
| |
| uint64_t shape_ptr; /* Pointer to shape array */ |
| uint64_t stride_ptr; /* Pointer to stride array */ |
| |
| uint8_t governance; /* B: 0=shared, 1=canonical */ |
| uint8_t ownership; /* OWNED/SHARED/EXCLUSIVE */ |
| uint8_t materialized; /* 0=not, 1=materialized */ |
| uint8_t state; /* Internal state */ |
| |
| uint64_t generation; /* Generation counter (stale detection) */ |
| } tensor_descriptor_t; |
| ``` |
| |
| **Address Calculation (no framework overhead):** |
| ``` |
| address = base + offset + Ξ£(index[i] * stride[i]) |
| ``` |
| |
| --- |
| |
| ## Ownership Semantics Through FFI |
| |
| ### Allocation |
| ``` |
| tensor_allocate(rank, shape, element_size) |
| β TensorDescriptorC { buffer_id=N, generation=G, governance=1 (canonical) } |
| β Arc<Vec<f32>> created internally |
| ``` |
| |
| ### View (Slice) |
| ``` |
| tensor_view(source, start_indices, end_indices) |
| β TensorDescriptorC { buffer_id=M (new), generation=G' } |
| β Arc::clone() increments refcount on source's data |
| β shape/stride/offset computed, data NOT copied |
| β is_contiguous recalculated |
| ``` |
| |
| ### Materialization |
| ``` |
| tensor_materialize(source where is_contiguous=false) |
| β new Arc<Vec> allocated |
| β strided data copied to new contiguous buffer |
| β TensorDescriptorC { buffer_id=K (new), generation=G'', governance=1 } |
| β source buffer remains alive and valid |
| β ownership is exclusive on new buffer |
| ``` |
| |
| ### Deallocation |
| ``` |
| tensor_deallocate(descriptor) |
| β Registry entry removed |
| β Arc is dropped |
| β if refcount reaches 0, buffer freed |
| ``` |
| |
| --- |
| |
| ## Generation Counter Safety |
| |
| Every buffer has a **generation** counter that increments on: |
| - **Allocation** β generation = 1 |
| - **Materialization** β new buffer gets new generation |
| - **Reallocation** β if buffer is reassigned |
| |
| **Stale Descriptor Detection:** |
| ```rust |
| fn tensor_validate_generation(desc: &TensorDescriptorC) -> Result { |
| if registry[desc.buffer_id].generation != desc.generation { |
| return Err("StaleGeneration"); |
| } |
| Ok(()) |
| } |
| ``` |
| |
| Prevents use-after-free and races on descriptor validity. |
|
|
| --- |
|
|
| ## Governance State Machine |
|
|
| ``` |
| SHARED (B=0) |
| β |
| ββββββββ΄βββββββ |
| β β |
| MATERIALIZE VIEW/SLICE |
| β β |
| βΌ βΌ |
| EXCLUSIVE SHARED (B=0) |
| (B=1) β |
| β β |
| βββββββββββββββββ |
| ``` |
|
|
| **Invariants:** |
| - `B=0`: shared view, non-canonical strides permitted, materialization available |
| - `B=1`: exclusive owner, canonical strides, direct element access |
| - Generation increments on every transition |
| - Invalid transitions β rejected with fail-closed error |
|
|
| --- |
|
|
| ## Cross-Language Conformance |
|
|
| For every operation, both **Rust** and **Pascal** must produce: |
|
|
| 1. **Identical shape** (rank and dimensions) |
| 2. **Identical strides** (same canonical form) |
| 3. **Identical offset** |
| 4. **Identical element values** (same underlying data) |
| 5. **Identical governance** (B value) |
| 6. **Identical generation** (stale check) |
| 7. **Identical buffer identity** (whether shared or independent) |
|
|
| **Oracle Function:** |
| ```rust |
| fn conformance_compare_descriptors( |
| rust: &TensorDescriptorC, |
| pascal: &TensorDescriptorC |
| ) -> ConformanceResult { ... } |
| ``` |
|
|
| If Rust and Pascal produce different descriptors, conformance fails. |
|
|
| --- |
|
|
| ## Sparse Router (RAW_ROUTE) |
| |
| ### Algorithm |
| |
| ``` |
| route(task): |
| r β task.memory_region |
| |
| if RegionTable[r].owner exists: |
| push(task, Worker[owner].deque) |
| return owner |
| |
| candidates β SparseTopology[r] |
| best β NONE |
| best_score β -β |
| |
| for worker in candidates: |
| score β 0.35 * locality(worker, task) |
| + 0.20 * memory_affinity(worker, task) |
| + 0.25 * queue_pressure(worker) |
| + 0.10 * stealability(worker) |
| - 0.10 * migration_cost(worker, task) |
| |
| if score > best_score: |
| best β worker |
| best_score β score |
| |
| if best != NONE: |
| push(task, Worker[best].deque) |
| RegionTable[r].owner β best |
| return best |
| |
| worker β select_least_loaded_worker() |
| push(task, Worker[worker].deque) |
| RegionTable[r].owner β worker |
| return worker |
| ``` |
| |
| ### Kani-Verified Theorems |
|
|
| 1. **Progress**: Every task is routed βt: βw such that route(t) = w |
| 2. **Locality**: Locality score dominates queue balance |
| 3. **Region Consistency**: Once region R β worker W, reused until unset |
| 4. **Migration Cost**: High-cost migrations are avoided over balance |
| 5. **Fallback**: Empty topology always assigns via least-loaded fallback |
| 6. **No Deadlock**: No circular region ownership |
| 7. **Score Bounds**: Score β [-1.0, 1.0] |
| 8. **Stability**: Route decisions remain valid until topology changes |
|
|
| --- |
|
|
| ## Error Handling (Fail-Closed) |
|
|
| All FFI operations return `TensorResultC`: |
| ```c |
| typedef struct { |
| int32_t success; /* 1 = OK, 0 = error */ |
| uint32_t error_code; /* machine-readable code */ |
| char error_msg[256]; /* human-readable message */ |
| } TensorResultC; |
| ``` |
|
|
| **Error codes:** |
| - `1`: Invalid pointer or rank |
| - `2`: Zero-element shape |
| - `3`: Buffer not found in registry |
| - `4`: Indices out of bounds |
| - `5`: Stale generation |
| - `6`: Computed address out of bounds |
| - `7`: Shared tensor cannot be mutated |
|
|
| On error: operation is rejected, no partial state is applied. |
|
|
| --- |
|
|
| ## Test Matrix |
|
|
| See `./tests/ffi/conformance_bridge.rs` for comprehensive coverage: |
|
|
| - `test_allocate_conforms` β Allocation produces canonical descriptor |
| - `test_view_preserves_data_and_buffer` β Views don't copy, source remains valid |
| - `test_materialization_creates_new_buffer` β New buffer, source unmodified |
| - `test_generation_safety` β Stale descriptors rejected |
| - `test_bounds_checking` β Out-of-bounds access fails |
| - `test_shared_ownership_prevents_store` β Arc refcount prevents mutation |
|
|
| Each test exercises both the Rust FFI and validates against Pascal oracle. |
|
|
| --- |
|
|
| ## Integration |
|
|
| The FFI layer enables: |
|
|
| 1. **Hardware execution**: Tensor descriptors can be mapped directly to hardware registers/DMA |
| 2. **Cross-language validation**: Pascal reference model verifies Rust correctness |
| 3. **Formal reasoning**: Kani proves routing correctness, temporal safety, bounds |
| 4. **Deterministic execution**: No implicit copies, ownership explicit, all state transitions auditable |
|
|
| The FFI is the **binary boundary** between Rust hardware semantics and Pascal reference semantics. Both must conform to the same ABI contract. |
|
|
