Relicense under the Sovereign Leviathan covenant; remove MIT and Apache

29f097e verified 14 days ago

8.79 kB

# NraayTensor Pascal Reference Implementation

Semantic reference layer for the Rust tensor-core library, implemented in Free Pascal (FPC). This reference implementation serves as an **oracle** for validating the Rust implementation, ensuring correctness through cross-language verification.

## Architecture

### Semantic Stack (Bottom to Top)

```
    Application (tests.pas, validation.pas)
           ↓
    Tensor Operations (tensor.pas)
           ↓
    Materialization & Governance (materialize.pas, governance.pas)
           ↓
    Ownership State Machine (ownership.pas)
           ↓
    Descriptor & Tensor Array (descriptor.pas, tensor_array.pas)
           ↓
    Buffer Management (buffer.pas)
           ↓
    Physical Storage (single[])
```

## Modules

### 1. buffer.pas (Generation-tracked allocation)
- **TBuffer**: Physical storage with refcount and generation
- `AllocateBuffer()`: Allocate with generation tracking
- `CloneBuffer()`: Increment refcount (Arc::clone)
- `ReleaseBuffer()`: Decrement refcount, free at 0
- `IncrementGeneration()`: Temporal safety tracking

**Key Invariants:**
- Refcount > 0 always while allocated
- Generation monotonically increases
- Once freed (refcount=0), generation becomes invalid

### 2. tensor_array.pas (Arc<Vec> semantics)
- **TTensorArray**: Wraps TBuffer with generation tracking
- `CreateTensorArray()`: Allocate new array
- `CloneTensorArray()`: Share buffer (refcount++)
- `DropTensorArray()`: Release (refcount--)
- `CopyOnWrite()`: Clone data if refcount > 1
**Arc Semantics:**
- Multiple references to same buffer (shared)
- Mutation only allowed if exclusively owned (refcount=1)
- Mutation triggers new generation
### 3. descriptor.pas (C-compatible view metadata)
- **TTensorDescriptor**: Packed record (C ABI compatible)
  - `rank`: dimensionality
  - `shape_ptr`: → shape array
  - `strides_ptr`: → strides array
  - `offset`: logical offset in buffer
  - `len`: total elements
  - `is_contiguous` (B_layout): canonical strides?
  - `owns_storage` (B_own): refcount=1?
  - `generation`: temporal safety token
**Index Mapping:** `f(x_0,...,x_{d-1}) = offset + Σ(x_i * σ_i)`
### 4. ownership.pas (OWNED/SHARED/EXCLUSIVE states)
- **TOwnershipState**: Enumeration of ownership modes
- State transitions:
  - `OWNED` (refcount=1, mutable)
  - `SHARED` (refcount>1, immutable, COW)
  - `EXCLUSIVE` (after materialization, mutable)
**State Machine:**
```
OWNED --[clone]--> SHARED
SHARED --[materialize]--> EXCLUSIVE
EXCLUSIVE --[release]--> OWNED (if refcount becomes 1)
```
### 5. governance.pas (5 executable lemmas)
Proves correctness of tensor invariants:
1. **Lemma 1 (Shape-Rank)**: `rank(t) = len(shape)`
2. **Lemma 2 (Length Product)**: `len(t) = ∏ shape_i`
3. **Lemma 3 (Canonical Strides)**: `B_layout=1 ⟹ σ_i = ∏_{j>i} s_j`
4. **Lemma 4 (Exclusive Ownership)**: `B_own=1 ⟹ refcount=1`
5. **Lemma 5 (Generation Safety)**: `descriptor.generation = buffer.generation`

`ValidateAllLemmas()`: Verify all 5 proofs hold at once.

### 6. materialize.pas (Copy-on-write barrier)
Restores contiguity and exclusive ownership:

**Algorithm:**
1. If already materialized (B_layout=1 AND B_own=1): return
2. Allocate new contiguous buffer
3. Copy viewed elements in row-major order
4. Replace Arc with new exclusive buffer
5. Reset strides to canonical
6. Update generation, set B_layout=1, B_own=1

**Property:** "Preserving order, strict and bound"

### 7. tensor.pas (Main tensor operations)
Core operations mirroring Rust implementation:

- **ALLOC**: `CreateTensor(shape)` → new exclusive tensor
- **FREE**: `DestroyTensor(var t)` → decrement refcount
- **VIEW**: `Slice(t, ranges)` → zero-copy view (shared)
- **TRANSPOSE**: permute axes via stride rearrangement
- **MATERIALIZE**: `Materialize(var t)` → restore contiguity
- **GET/SET**: element access via logical coordinates

### 8. validation.pas (Conformance oracle)
Cross-implementation validation functions:

- `CompareDescriptors()`: Check equivalence
- `ValidateAlloc()`: Verify creation invariants
- `ValidateSlice()`: Check slicing semantics
- `ValidateTranspose()`: Verify axis permutation
- `ValidateMaterialize()`: Check materialization result
- `ValidateClone()`: Verify shared ownership
- `VerifyGovernanceLemmas()`: All 5 lemmas hold?

### 9. tests.pas (Comprehensive test suite)
10 core conformance tests:

1. Allocation
2. Element access
3. Clone (refcount=2)
4. Slicing (non-contiguous)
5. Transpose (shape permuted)
6. Materialization (contiguous+exclusive)
7. Generation tracking
8. Governance lemmas
9. Reference counting
10. Composite workflow

### 10. nraay_tensor_ref.pas (Main program)
Demonstration and test runner:
```
./nraay_tensor_ref
```

Exit codes:
- 0: All tests passed
- 1: Some tests failed
- 2: Fatal error

## Operation Semantics

### Allocation (ALLOC)
```pascal
t := CreateTensor([3, 4]);
{ Result:
  - Exclusive ownership (refcount=1)
  - Canonical strides (row-major)
  - B_layout=1, B_own=1, OWNED state
  - Generation=0 }
```

### Slicing (VIEW)
```pascal
ranges[0] := [1, 4, 1];  // start=1, end=4, step=1
ranges[1] := [1, 4, 1];
sliced := Slice(t, ranges);
{ Result:
  - Shared ownership (refcount→2)
  - Non-canonical strides (B_layout=0)
  - Offset adjusted, shape reduced
  - B_own=0, SHARED state
  - Same buffer, different view }
```

### Materialization (MATERIALIZE)
```pascal
Materialize(sliced);
{ Result:
  - Exclusive ownership (new buffer)
  - Canonical strides (row-major)
  - B_layout=1, B_own=1
  - Offset=0, new generation
  - EXCLUSIVE state }
```

### Transpose
```pascal
perm := [1, 0];  // swap axes
transposed := Transpose(t, perm);
{ Result:
  - Shape permuted: [3,4] → [4,3]
  - Strides permuted accordingly
  - B_layout likely=0 (non-canonical)
  - Shares buffer, different view }
```

## Governance Properties

### Binary Semantics (B_layout, B_own)

**B_layout (is_contiguous):**
- 1: Strides follow row-major canonical pattern
- 0: Strides do NOT follow canonical (from slicing/transpose)

**B_own (owns_storage):**
- 1: Exclusive ownership (refcount=1), can mutate
- 0: Shared ownership (refcount>1), immutable

### Generation Safety
Every buffer has monotonic generation counter:
```
buffer.generation = counter at allocation time
descriptor.generation = counter at view creation time
Use-after-free prevention: stale views detected by generation mismatch
```

## Compilation and Usage

### FPC Compilation
```bash
cd pascal
fpc -O2 nraay_tensor_ref.pas -o nraay_tensor_ref
./nraay_tensor_ref
```

### With gdb
```bash
fpc -g nraay_tensor_ref.pas
gdb ./nraay_tensor_ref
```

### Unit Testing in Other Code
```pascal
uses tensor, validation, tests;
procedure MyTest;
var
  t: TNraayTensor;
  report: TTestReport;
begin
  t := CreateTensor([2, 3]);
  report := ValidateAlloc(t);
  
  if report.passed then
    writeln('Test passed: ', report.details)
  else
    writeln('Test failed: ', report.details);
    
  DestroyTensor(t);
end;
```

## Cross-Language Conformance

This Pascal reference validates Rust implementation by:

1. **Operation Matching**: Each Rust op has Pascal equivalent
2. **State Verification**: Oracle functions check Rust output states
3. **Invariant Checking**: 5 governance lemmas verified independently
4. **Generation Tracking**: Temporal safety without language runtime
5. **Memory Semantics**: Arc behavior replicated with explicit refcount

### Testing Against Rust
1. Run Rust operation
2. Export resulting descriptor/buffer to Pascal format
3. Call validation oracle
4. Compare Oracle result with expected behavior

## Semantic Properties

### Invariants (Always True)
```
1. rank(t) = len(shape(t))
2. len(t) = ∏ shape_i
3. B_layout=1 → canonical strides
4. B_own=1 → refcount=1
5. generation(descriptor) = generation(buffer)
```

### State Safety
```
OWNED ← exclusive mutation OK, B_own=1
SHARED ← no mutation, COW barrier
EXCLUSIVE ← exclusive mutation OK, B_own=1
```

### Generation Transitions
```
- Allocation: generation_0 (global_counter++)
- Clone: inherits buffer.generation (same)
- Materialize: generation_new (global_counter++)
- Stale check: generation_mismatch → error
```

## Performance Notes

**Memory:** ~1200 LOC core, ~800 LOC validation
**No runtime overhead:** Direct memory access via strides
**Materialization:** O(n) copy only on COW violation or explicit call

## License

License: Sovereign Leviathan covenant (`LicenseRef-Sovereign-Leviathan-SL-AGPL3-001`)

This ensures:
- Open source compliance (GPL-3.0)
- AI company restrictions (GPL-3.0 clause 5)

## See Also

- [FORMAL_SPEC.md](../FORMAL_SPEC.md) - Mathematical definitions
- [Rust Implementation](../nraay-tensor/src/tensor.rs) - Primary implementation
- [Lemmas](../nraay-tensor/src/lemmas.rs) - Formal proofs

	# NraayTensor Pascal Reference Implementation

	Semantic reference layer for the Rust tensor-core library, implemented in Free Pascal (FPC). This reference implementation serves as an oracle for validating the Rust implementation, ensuring correctness through cross-language verification.

	## Architecture

	### Semantic Stack (Bottom to Top)

	```
	Application (tests.pas, validation.pas)
	↓
	Tensor Operations (tensor.pas)
	↓
	Materialization & Governance (materialize.pas, governance.pas)
	↓
	Ownership State Machine (ownership.pas)
	↓
	Descriptor & Tensor Array (descriptor.pas, tensor_array.pas)
	↓
	Buffer Management (buffer.pas)
	↓
	Physical Storage (single[])
	```

	## Modules

	### 1. buffer.pas (Generation-tracked allocation)
	- TBuffer: Physical storage with refcount and generation
	- `AllocateBuffer()`: Allocate with generation tracking
	- `CloneBuffer()`: Increment refcount (Arc::clone)
	- `ReleaseBuffer()`: Decrement refcount, free at 0
	- `IncrementGeneration()`: Temporal safety tracking

	Key Invariants:
	- Refcount > 0 always while allocated
	- Generation monotonically increases
	- Once freed (refcount=0), generation becomes invalid

	### 2. tensor_array.pas (Arc<Vec> semantics)
	- TTensorArray: Wraps TBuffer with generation tracking
	- `CreateTensorArray()`: Allocate new array
	- `CloneTensorArray()`: Share buffer (refcount++)
	- `DropTensorArray()`: Release (refcount--)
	- `CopyOnWrite()`: Clone data if refcount > 1

	Arc Semantics:
	- Multiple references to same buffer (shared)
	- Mutation only allowed if exclusively owned (refcount=1)
	- Mutation triggers new generation

	### 3. descriptor.pas (C-compatible view metadata)
	- TTensorDescriptor: Packed record (C ABI compatible)
	- `rank`: dimensionality
	- `shape_ptr`: → shape array
	- `strides_ptr`: → strides array
	- `offset`: logical offset in buffer
	- `len`: total elements
	- `is_contiguous` (B_layout): canonical strides?
	- `owns_storage` (B_own): refcount=1?
	- `generation`: temporal safety token

	Index Mapping: `f(x_0,...,x_{d-1}) = offset + Σ(x_i * σ_i)`

	### 4. ownership.pas (OWNED/SHARED/EXCLUSIVE states)
	- TOwnershipState: Enumeration of ownership modes
	- State transitions:
	- `OWNED` (refcount=1, mutable)
	- `SHARED` (refcount>1, immutable, COW)
	- `EXCLUSIVE` (after materialization, mutable)

	State Machine:
	```
	OWNED --[clone]--> SHARED
	SHARED --[materialize]--> EXCLUSIVE
	EXCLUSIVE --[release]--> OWNED (if refcount becomes 1)
	```

	### 5. governance.pas (5 executable lemmas)
	Proves correctness of tensor invariants:

	1. Lemma 1 (Shape-Rank): `rank(t) = len(shape)`
	2. Lemma 2 (Length Product): `len(t) = ∏ shape_i`
	3. Lemma 3 (Canonical Strides): `B_layout=1 ⟹ σ_i = ∏_{j>i} s_j`
	4. Lemma 4 (Exclusive Ownership): `B_own=1 ⟹ refcount=1`
	5. Lemma 5 (Generation Safety): `descriptor.generation = buffer.generation`

	`ValidateAllLemmas()`: Verify all 5 proofs hold at once.

	### 6. materialize.pas (Copy-on-write barrier)
	Restores contiguity and exclusive ownership:

	Algorithm:
	1. If already materialized (B_layout=1 AND B_own=1): return
	2. Allocate new contiguous buffer
	3. Copy viewed elements in row-major order
	4. Replace Arc with new exclusive buffer
	5. Reset strides to canonical
	6. Update generation, set B_layout=1, B_own=1

	Property: "Preserving order, strict and bound"

	### 7. tensor.pas (Main tensor operations)
	Core operations mirroring Rust implementation:

	- ALLOC: `CreateTensor(shape)` → new exclusive tensor
	- FREE: `DestroyTensor(var t)` → decrement refcount
	- VIEW: `Slice(t, ranges)` → zero-copy view (shared)
	- TRANSPOSE: permute axes via stride rearrangement
	- MATERIALIZE: `Materialize(var t)` → restore contiguity
	- GET/SET: element access via logical coordinates

	### 8. validation.pas (Conformance oracle)
	Cross-implementation validation functions:

	- `CompareDescriptors()`: Check equivalence
	- `ValidateAlloc()`: Verify creation invariants
	- `ValidateSlice()`: Check slicing semantics
	- `ValidateTranspose()`: Verify axis permutation
	- `ValidateMaterialize()`: Check materialization result
	- `ValidateClone()`: Verify shared ownership
	- `VerifyGovernanceLemmas()`: All 5 lemmas hold?

	### 9. tests.pas (Comprehensive test suite)
	10 core conformance tests:

	1. Allocation
	2. Element access
	3. Clone (refcount=2)
	4. Slicing (non-contiguous)
	5. Transpose (shape permuted)
	6. Materialization (contiguous+exclusive)
	7. Generation tracking
	8. Governance lemmas
	9. Reference counting
	10. Composite workflow

	### 10. nraay_tensor_ref.pas (Main program)
	Demonstration and test runner:
	```
	./nraay_tensor_ref
	```

	Exit codes:
	- 0: All tests passed
	- 1: Some tests failed
	- 2: Fatal error

	## Operation Semantics

	### Allocation (ALLOC)
	```pascal
	t := CreateTensor([3, 4]);
	{ Result:
	- Exclusive ownership (refcount=1)
	- Canonical strides (row-major)
	- B_layout=1, B_own=1, OWNED state
	- Generation=0 }
	```

	### Slicing (VIEW)
	```pascal
	ranges[0] := [1, 4, 1]; // start=1, end=4, step=1
	ranges[1] := [1, 4, 1];
	sliced := Slice(t, ranges);
	{ Result:
	- Shared ownership (refcount→2)
	- Non-canonical strides (B_layout=0)
	- Offset adjusted, shape reduced
	- B_own=0, SHARED state
	- Same buffer, different view }
	```

	### Materialization (MATERIALIZE)
	```pascal
	Materialize(sliced);
	{ Result:
	- Exclusive ownership (new buffer)
	- Canonical strides (row-major)
	- B_layout=1, B_own=1
	- Offset=0, new generation
	- EXCLUSIVE state }
	```

	### Transpose
	```pascal
	perm := [1, 0]; // swap axes
	transposed := Transpose(t, perm);
	{ Result:
	- Shape permuted: [3,4] → [4,3]
	- Strides permuted accordingly
	- B_layout likely=0 (non-canonical)
	- Shares buffer, different view }
	```

	## Governance Properties

	### Binary Semantics (B_layout, B_own)

	B_layout (is_contiguous):
	- 1: Strides follow row-major canonical pattern
	- 0: Strides do NOT follow canonical (from slicing/transpose)

	B_own (owns_storage):
	- 1: Exclusive ownership (refcount=1), can mutate
	- 0: Shared ownership (refcount>1), immutable

	### Generation Safety
	Every buffer has monotonic generation counter:
	```
	buffer.generation = counter at allocation time
	descriptor.generation = counter at view creation time

	Use-after-free prevention: stale views detected by generation mismatch
	```

	## Compilation and Usage

	### FPC Compilation
	```bash
	cd pascal
	fpc -O2 nraay_tensor_ref.pas -o nraay_tensor_ref
	./nraay_tensor_ref
	```

	### With gdb
	```bash
	fpc -g nraay_tensor_ref.pas
	gdb ./nraay_tensor_ref
	```

	### Unit Testing in Other Code
	```pascal
	uses tensor, validation, tests;

	procedure MyTest;
	var
	t: TNraayTensor;
	report: TTestReport;
	begin
	t := CreateTensor([2, 3]);
	report := ValidateAlloc(t);

	if report.passed then
	writeln('Test passed: ', report.details)
	else
	writeln('Test failed: ', report.details);

	DestroyTensor(t);
	end;
	```

	## Cross-Language Conformance

	This Pascal reference validates Rust implementation by:

	1. Operation Matching: Each Rust op has Pascal equivalent
	2. State Verification: Oracle functions check Rust output states
	3. Invariant Checking: 5 governance lemmas verified independently
	4. Generation Tracking: Temporal safety without language runtime
	5. Memory Semantics: Arc behavior replicated with explicit refcount

	### Testing Against Rust
	1. Run Rust operation
	2. Export resulting descriptor/buffer to Pascal format
	3. Call validation oracle
	4. Compare Oracle result with expected behavior

	## Semantic Properties

	### Invariants (Always True)
	```
	1. rank(t) = len(shape(t))
	2. len(t) = ∏ shape_i
	3. B_layout=1 → canonical strides
	4. B_own=1 → refcount=1
	5. generation(descriptor) = generation(buffer)
	```

	### State Safety
	```
	OWNED ← exclusive mutation OK, B_own=1
	SHARED ← no mutation, COW barrier
	EXCLUSIVE ← exclusive mutation OK, B_own=1
	```

	### Generation Transitions
	```
	- Allocation: generation_0 (global_counter++)
	- Clone: inherits buffer.generation (same)
	- Materialize: generation_new (global_counter++)
	- Stale check: generation_mismatch → error
	```

	## Performance Notes

	Memory: ~1200 LOC core, ~800 LOC validation
	No runtime overhead: Direct memory access via strides
	Materialization: O(n) copy only on COW violation or explicit call

	## License

	License: Sovereign Leviathan covenant (`LicenseRef-Sovereign-Leviathan-SL-AGPL3-001`)

	This ensures:
	- Open source compliance (GPL-3.0)
	- AI company restrictions (GPL-3.0 clause 5)

	## See Also

	- [FORMAL_SPEC.md](../FORMAL_SPEC.md) - Mathematical definitions
	- [Rust Implementation](../nraay-tensor/src/tensor.rs) - Primary implementation
	- [Lemmas](../nraay-tensor/src/lemmas.rs) - Formal proofs