| # TENSOR_CONTRACT.md |
| ## Normative Operation Signatures for NraayTensor |
| |
| ### 1. Overview |
| |
| The NraayTensor Contract defines the complete interface for all tensor operations. Each operation specifies: |
| - **Input State**: Pre-conditions on tensor governance flags (B_layout, B_own), shape, and ownership |
| - **Output State**: Post-conditions on governance flags and memory configuration |
| - **Ownership Effects**: Changes to Arc refcount and exclusive-access semantics |
| - **Memory Effects**: Effects on physical buffer π«, offset O, strides Ξ£ |
| - **Failure Conditions**: Explicit rejection criteria (bounds, dimension mismatch, invalid state) |
| |
| All operations are **fail-closed**: when preconditions fail, the tensor remains unchanged and an error is returned. |
| |
| --- |
| |
| ### 2. Data Structures |
| |
| #### TensorDescriptor (C-Compatible Layout) |
| |
| ```rust |
| pub struct NraayTensor { |
| // Ownership token (temporal safety via Arc<Vec<f32>>) |
| data: Arc<Vec<f32>>, |
| |
| // Semantic view metadata |
| shape: Vec<usize>, // S = (s_0, ..., s_{d-1}) |
| strides: Vec<usize>, // Ξ£ = (Ο_0, ..., Ο_{d-1}) |
| offset: usize, // O (memory offset) |
| |
| // Binary governance flags |
| is_contiguous: bool, // B_layout = 1 βΊ canonical strides |
| owns_storage: bool, // B_own = 1 βΊ refcount = 1 |
| } |
| ``` |
| |
| **Invariant**: The physical buffer π« has length β₯ max accessed address in any view. |
| |
| --- |
| |
| ### 3. Operation Specifications |
| |
| #### OP-1: ALLOC (Constructor) |
| |
| **Signature**: |
| ``` |
| ALLOC(shape: Vec<usize>) -> Result<NraayTensor> |
| ``` |
| |
| **Precondition**: |
| - shape is non-empty |
| - β s_i β shape: s_i > 0 |
| - β s_i is finite and allocatable |
|
|
| **Input State**: |
| - N/A (construction) |
|
|
| **Output State**: |
| ``` |
| shape' = shape |
| strides' = canonical_strides(shape) |
| offset' = 0 |
| B_layout' = 1 (newly allocated buffer is contiguous) |
| B_own' = 1 (exclusive ownership, refcount = 1) |
| buffer' = Arc::new(vec![0.0; size]) |
| ``` |
|
|
| **Ownership Effect**: |
| - refcount = 1 (constructor holds sole Arc) |
|
|
| **Memory Effect**: |
| - Allocates new 1D buffer in heap |
| - Physical storage π« = [0.0; β s_i] |
| |
| **Failure Conditions**: |
| ``` |
| shape.is_empty() β EmptyTensor |
| any s_i = 0 β EmptyTensor |
| β s_i causes overflow β OutOfMemory |
| allocation fails β OutOfMemory |
| ``` |
| |
| **Oracle Behavior** (Rust & Pascal must match): |
| ``` |
| let t = ALLOC([2, 3]) |
| assert(t.shape = [2, 3]) |
| assert(t.strides = [3, 1]) |
| assert(t.offset = 0) |
| assert(t.B_layout = true) |
| assert(t.B_own = true) |
| assert(t.refcount() = 1) |
| ``` |
| |
| --- |
| |
| #### OP-2: FREE (Destructor) |
| |
| **Signature**: |
| ``` |
| FREE(tensor: &mut NraayTensor) |
| ``` |
| |
| **Precondition**: |
| - tensor is valid (within scope) |
| |
| **Input State**: |
| - Any governance configuration allowed |
| |
| **Output State**: |
| - Tensor deallocated |
| - If refcount reaches 0, buffer π« deallocated |
| - Otherwise, Arc refcount decremented by 1 |
| |
| **Ownership Effect**: |
| - Arc::drop() called on self.data |
| - refcount decrements by 1 |
| - When refcount = 0, Vec<f32> deallocated by Rust allocator |
| |
| **Memory Effect**: |
| - Heap memory freed only if this was the last owner (refcount was 1) |
| |
| **Failure Conditions**: None |
| |
| **Oracle Behavior**: |
| ``` |
| let t = ALLOC([2, 3]) // refcount = 1 |
| let s = SLICE(t, ...) // refcount = 2 |
| DROP(s) // refcount = 1 |
| DROP(t) // refcount = 0 β heap freed |
| ``` |
| |
| --- |
| |
| #### OP-3: VIEW (Slicing) |
| |
| **Signature**: |
| ``` |
| VIEW(self: &NraayTensor, ranges: &[(start, end, step)]) |
| -> Result<NraayTensor> |
| ``` |
| |
| **Precondition**: |
| - ranges.len() = self.shape.len() |
| - β i: 0 β€ start_i < end_i β€ shape_i |
| - β i: step_i > 0 |
| |
| **Input State**: |
| ``` |
| self.B_layout β {0, 1} (any contiguity) |
| self.B_own β {0, 1} (any ownership) |
| ``` |
| |
| **Output State**: |
| ``` |
| shape'_i = β(end_i - start_i) / step_iβ |
| strides'_i = strides_i * step_i |
| offset' = offset + Ξ£_i (start_i * strides_i) |
| B_layout' = recompute_canonical(shape', strides') |
| B_own' = 0 (always shared after slicing) |
| data' = Arc::clone(&self.data) |
| ``` |
| |
| **Ownership Effect**: |
| - refcount increments by 1 (Arc clone) |
| - New tensor acquires non-exclusive view (owns_storage = false) |
|
|
| **Memory Effect**: |
| - Zero-copy: no data is copied |
| - Offset computation may skip leading elements |
| - Stride multiplication may create non-canonical access patterns |
|
|
| **Failure Conditions**: |
| ``` |
| ranges.len() β shape.len() β DimensionMismatch |
| start_i β₯ end_i β InvalidSliceRange |
| step_i = 0 β InvalidSliceRange |
| start_i >= shape_i β InvalidSliceRange |
| end_i > shape_i β InvalidSliceRange |
| ``` |
|
|
| **Oracle Behavior**: |
| ``` |
| let t = ALLOC([4, 4]) |
| t.set([0,0], 1.0); t.set([0,1], 2.0); ... t.set([3,3], 16.0) |
| let v = VIEW(t, [(0,2,1), (1,4,1)]) |
| assert(v.shape = [2, 3]) |
| assert(v.offset = 1) |
| assert(v.strides = [4, 1]) |
| assert(v.B_own = false) |
| assert(v.refcount() = 2) |
| ``` |
|
|
| --- |
|
|
| #### OP-4: TRANSPOSE (Logical Shift) |
|
|
| **Signature**: |
| ``` |
| TRANSPOSE(self: &mut NraayTensor, perm: &[usize]) -> Result<()> |
| ``` |
|
|
| **Precondition**: |
| - perm is a valid permutation of (0..self.shape.len()) |
| - perm.len() = self.shape.len() |
|
|
| **Input State**: |
| ``` |
| self.B_layout β {0, 1} |
| self.B_own β {0, 1} |
| ``` |
|
|
| **Output State**: |
| ``` |
| shape'_i = shape[perm[i]] |
| strides'_i = strides[perm[i]] |
| offset' = offset (unchanged) |
| B_layout' = recompute_canonical(shape', strides') |
| B_own' = owns_storage (unchanged) |
| data' = data (unchanged, no copy) |
| ``` |
|
|
| **Ownership Effect**: None (metadata-only operation) |
|
|
| **Memory Effect**: |
| - Pure logical transformation of view metadata |
| - No data movement |
| - Physical buffer π« untouched |
|
|
| **Failure Conditions**: |
| ``` |
| perm.len() β shape.len() β InvalidPermutation |
| perm contains duplicates β InvalidPermutation |
| β p β perm: p >= shape.len() β InvalidPermutation |
| perm is not a permutation β InvalidPermutation |
| ``` |
|
|
| **Oracle Behavior**: |
| ``` |
| let mut t = ALLOC([2, 3]) |
| assert(t.B_layout = true) |
| TRANSPOSE(&mut t, [1, 0]) |
| assert(t.shape = [3, 2]) |
| assert(t.B_layout = false) // Non-canonical now |
| ``` |
|
|
| --- |
|
|
| #### OP-5: RESHAPE (Safe Shape Change) |
|
|
| **Signature**: |
| ``` |
| RESHAPE(self: &mut NraayTensor, new_shape: Vec<usize>) |
| -> Result<()> |
| ``` |
|
|
| **Precondition**: |
| - new_shape is non-empty |
| - β new_shape = β self.shape (size preserved) |
| - B_layout = 1 AND B_own = 1 (only on contiguous exclusive tensors) |
|
|
| **Input State**: |
| ``` |
| B_layout = 1 |
| B_own = 1 |
| β shape = β new_shape |
| ``` |
|
|
| **Output State**: |
| ``` |
| shape' = new_shape |
| strides' = canonical_strides(new_shape) |
| offset' = 0 |
| B_layout' = 1 |
| B_own' = 1 |
| data' = data (unchanged) |
| ``` |
|
|
| **Ownership Effect**: None |
|
|
| **Memory Effect**: |
| - No allocation or copying |
| - Reinterprets physical buffer under new shape |
| - Offset reset to 0 (reshape only on contiguous exclusive) |
|
|
| **Failure Conditions**: |
| ``` |
| β new_shape β β shape β ShapeMismatch |
| new_shape.is_empty() β EmptyTensor |
| B_layout β 1 β NotContiguous |
| B_own β 1 β NotExclusive |
| ``` |
|
|
| **Oracle Behavior**: |
| ``` |
| let mut t = ALLOC([2, 6]) |
| assert(t.len() = 12) |
| RESHAPE(&mut t, [3, 4])? |
| assert(t.shape = [3, 4]) |
| assert(t.len() = 12) |
| ``` |
|
|
| --- |
|
|
| #### OP-6: MATERIALIZE (Restore Contiguity + Exclusive Ownership) |
|
|
| **Signature**: |
| ``` |
| MATERIALIZE(self: &mut NraayTensor) -> Result<()> |
| ``` |
|
|
| **Precondition**: None (always safe) |
|
|
| **Input State**: |
| ``` |
| B_layout β {0, 1} |
| B_own β {0, 1} |
| Any shape/stride/offset valid |
| ``` |
|
|
| **Output State**: |
| ``` |
| IF B_layout = 1 AND B_own = 1: |
| // No-op (already canonical and exclusive) |
| output = input unchanged |
| |
| IF B_layout = 0 OR B_own = 0: |
| // Allocate, copy, and restore canonical state |
| new_buffer = Arc::new(vec![0.0; len]) |
| copy_viewed_elements(self, new_buffer) |
| |
| shape' = shape (unchanged) |
| strides' = canonical_strides(shape) |
| offset' = 0 |
| B_layout' = 1 |
| B_own' = 1 |
| data' = Arc::new(new_buffer) |
| ``` |
|
|
| **Ownership Effect**: |
| - Decrements refcount on old data Arc by 1 |
| - Creates new Arc with refcount = 1 |
| - Old Arc unchanged for other views |
|
|
| **Memory Effect**: |
| - If precondition true: COW semantics apply |
| - New contiguous buffer allocated with element count = β shape |
| - Elements copied in row-major logical order from source view |
| - Original buffer remains valid for other views |
|
|
| **Failure Conditions**: |
| ``` |
| copy_viewed_elements overflow β IndexOutOfBounds |
| new allocation fails β OutOfMemory |
| ``` |
|
|
| **Oracle Behavior**: |
| ``` |
| let mut t = ALLOC([2, 3]) |
| TRANSPOSE(&mut t, [1, 0]) |
| assert(t.B_layout = false) |
| MATERIALIZE(&mut t)? |
| assert(t.B_layout = true) |
| assert(t.B_own = true) |
| assert(t.strides = [2, 1]) |
| assert(t.offset = 0) |
| ``` |
|
|
| --- |
|
|
| #### OP-7: GET (Element Access - Read) |
|
|
| **Signature**: |
| ``` |
| GET(self: &NraayTensor, coord: &[usize]) -> Result<f32> |
| ``` |
|
|
| **Precondition**: |
| - coord.len() = self.shape.len() |
| - β i: 0 β€ coord_i < shape_i |
|
|
| **Input State**: |
| - Any governance state (read-only) |
|
|
| **Output State**: |
| - Unchanged |
|
|
| **Ownership Effect**: None |
|
|
| **Memory Effect**: |
| - Reads single element from buffer π« |
| - Computes physical index: idx = offset + Ξ£ (coord_i * strides_i) |
| - Bounds check: idx < |π«| |
|
|
| **Failure Conditions**: |
| ``` |
| coord.len() β shape.len() β DimensionMismatch |
| coord_i >= shape_i β IndexOutOfBounds |
| computed_idx >= buffer.len() β IndexOutOfBounds |
| ``` |
|
|
| **Oracle Behavior**: |
| ``` |
| let mut t = ALLOC([2, 3]) |
| SET(t, [0,1], 42.0) |
| assert(GET(t, [0,1]) = 42.0) |
| ``` |
|
|
| --- |
|
|
| #### OP-8: SET (Element Access - Write) |
|
|
| **Signature**: |
| ``` |
| SET(self: &mut NraayTensor, coord: &[usize], value: f32) |
| -> Result<()> |
| ``` |
|
|
| **Precondition**: |
| - coord.len() = self.shape.len() |
| - β i: 0 β€ coord_i < shape_i |
|
|
| **Input State**: |
| ``` |
| B_own β {0, 1} |
| ``` |
|
|
| **Output State**: |
| ``` |
| IF refcount(data) = 1: |
| // Exclusive; direct mutation |
| B_own' = true |
| B_layout' unchanged |
| element_at(offset + Ξ£ coord_i * strides_i) = value |
| |
| IF refcount(data) > 1: |
| // Shared; COW |
| data' = Arc::new(clone(data)) |
| B_own' = true |
| B_layout' unchanged |
| element_at(0 + Ξ£ coord_i * strides_i) = value |
| ``` |
|
|
| **Ownership Effect**: |
| - If refcount > 1: Arc refcount decrements by 1 on old buffer, new Arc created with refcount = 1 |
| - If refcount = 1: no Arc change, in-place mutation via Arc::get_mut |
| |
| **Memory Effect**: |
| - Single element written to buffer |
| - If COW triggered, full copy of data to new allocation before write |
| - Old buffer remains accessible to other views |
| |
| **Failure Conditions**: |
| ``` |
| coord.len() β shape.len() β DimensionMismatch |
| coord_i >= shape_i β IndexOutOfBounds |
| computed_idx >= buffer.len() β IndexOutOfBounds |
| ``` |
| |
| **Oracle Behavior**: |
| ``` |
| let mut t = ALLOC([2, 3]) |
| let s = VIEW(t, ...) // refcount = 2 |
| SET(s, [0,0], 99.0) // COW triggered |
| assert(refcount(s) = 1) |
| assert(GET(t, [0,0]) = 0.0) // Original unchanged |
| assert(GET(s, [0,0]) = 99.0) // Slice modified |
| ``` |
| |
| --- |
| |
| ### 4. Invariants (Must Hold After Every Operation) |
| |
| 1. **Physical Buffer Invariant**: |π«| β₯ max accessed address |
| 2. **Governance Correctness**: B_layout βΊ strides canonical for shape |
| 3. **Shape-Stride Consistency**: shape and strides same length |
| 4. **Offset Bounds**: offset < |π«| |
| 5. **Refcount Positivity**: refcount(data) β₯ 1 for live views |
| 6. **COW Correctness**: Materialization on shared tensor creates exclusive buffer |
| |
| --- |
| |
| ### 5. Pseudocode Contract Summary |
| |
| ``` |
| Contract(Op, Precond, InputState) β (OutputState, OwnershipEffect, MemoryEffect, FailureReasons) |
|
|
| OP-1: ALLOC(shape) |
| Pre: shape non-empty, β shape > 0 |
| In: N/A |
| Out: contiguous=1, own=1, offset=0, refcount=1 |
| Own: new Arc, refcount=1 |
| Mem: allocate β shape elements |
| Fail: EmptyTensor, OutOfMemory |
|
|
| OP-2: FREE |
| Pre: valid |
| In: any |
| Out: deallocated (refcount--) |
| Own: Arc::drop |
| Mem: free if refcountβ0 |
| Fail: none |
|
|
| OP-3: VIEW(ranges) |
| Pre: ranges valid for shape |
| In: any |
| Out: own=0, recomputed_contiguity, offset/stride scaled |
| Own: refcount++ |
| Mem: zero-copy |
| Fail: DimensionMismatch, InvalidSliceRange |
| |
| OP-4: TRANSPOSE(perm) |
| Pre: perm valid permutation |
| In: any |
| Out: shape/strides permuted, recomputed_contiguity |
| Own: none |
| Mem: metadata only |
| Fail: InvalidPermutation |
|
|
| OP-5: RESHAPE(new_shape) |
| Pre: size preserved, contiguous & exclusive only |
| In: contiguous=1, own=1 |
| Out: new shape, canonical strides, own=1 |
| Own: none |
| Mem: no allocation |
| Fail: ShapeMismatch, NotContiguous, NotExclusive |
| |
| OP-6: MATERIALIZE |
| Pre: always valid |
| In: any |
| Out: contiguous=1, own=1, canonical strides, offset=0 |
| Own: if needed, new Arc (old refcount--) |
| Mem: allocate + copy if non-canonical or shared |
| Fail: OutOfMemory |
| |
| OP-7: GET(coord) |
| Pre: coord valid |
| In: any |
| Out: unchanged |
| Own: none |
| Mem: read single element |
| Fail: DimensionMismatch, IndexOutOfBounds |
| |
| OP-8: SET(coord, value) |
| Pre: coord valid |
| In: any |
| Out: element written, own updated if COW |
| Own: refcount-- (old), refcount++ (new) if COW |
| Mem: if refcount>1, copy-on-write; else in-place |
| Fail: DimensionMismatch, IndexOutOfBounds |
| ``` |
| |
| --- |
| |
| ### 6. References |
| |
| - Memory Model: See MEMORY_MODEL.md for buffer layout formulas |
| - Governance State Machine: See GOVERNANCE_STATE_MACHINE.md for state transitions |
| - Temporal Safety: See TEMPORAL_SAFETY.md for lifetime proofs |
| - Proof Obligations: See PROOF_OBLIGATIONS.md for formal lemmas |
|
|
