spec/TENSOR_CONTRACT.md

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)

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