pascal/README.md

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

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)

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)

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

Transpose

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

cd pascal
fpc -O2 nraay_tensor_ref.pas -o nraay_tensor_ref
./nraay_tensor_ref

With gdb

fpc -g nraay_tensor_ref.pas
gdb ./nraay_tensor_ref

Unit Testing in Other Code

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 - Mathematical definitions
• Rust Implementation - Primary implementation
• Lemmas - Formal proofs