Relicense under the Sovereign Leviathan covenant; remove MIT and Apache

29f097e verified 20 days ago

11.7 kB

# NraayTensor Specification Suite

## Overview

This directory contains the **normative specifications** for the NraayTensor hardware-oriented tensor governance system. These documents define the contract that both Rust and Pascal implementations must conform to.

All specifications are derived from Ahmad's tensor semantic framework with temporal safety extensions (BLRD model).

---

## Document Index

### 1. [TENSOR_CONTRACT.md](TENSOR_CONTRACT.md)
**Purpose**: Complete operation interface specification

**Contents**:
- TensorDescriptor C-compatible layout (76 bytes, 8-byte aligned)
- 8 normative operations: ALLOC, FREE, VIEW, TRANSPOSE, RESHAPE, MATERIALIZE, GET, SET
- Pre-conditions and post-conditions for each operation
- Ownership effects (Arc refcount management)
- Memory effects (buffer allocation, offset, stride computation)
- Failure conditions and error handling
- Pseudocode contract summary

**Key Concepts**:
```
OP-1: ALLOC — Create tensor, B_layout=1, B_own=1, refcount=1
OP-2: FREE  — Destructor, Arc::drop, buffer deallocation when refcount→0
OP-3: VIEW  — Zero-copy slicing, new offset/strides, B_own→0, refcount++
OP-4: TRANSPOSE — Logical permutation, metadata-only, recompute B_layout
OP-5: RESHAPE — Safe size-preserving shape change (contiguous/exclusive only)
OP-6: MATERIALIZE — COW-based contiguity/exclusivity restoration
OP-7: GET  — Element access (read), no state change
OP-8: SET  — Element access (write), COW if refcount>1
```

**Critical Invariants**:
1. Physical buffer size never shrinks during view operations
2. All address computations bounded by buffer length
3. B_layout ⟺ canonical stride pattern
4. B_own ⟺ refcount = 1
5. Fail-closed: precondition failures leave tensor unchanged

---

### 2. [GOVERNANCE_STATE_MACHINE.md](GOVERNANCE_STATE_MACHINE.md)
**Purpose**: State space, transitions, and invariants

**Contents**:
- 4-state space: (B_layout, B_own) ∈ {(0,0), (0,1), (1,0), (1,1)}
- State diagram with all legal transitions
- Pre/post-conditions for every transition
- Canonical form definition and canonical strides formula
- Generation counter management (u64 for staleness detection)
- Invariant conditions (must hold in all states)
- Reachability matrix showing valid transition paths

**State Space**:
```
State 00: SHARED_NON_CANONICAL    — Multiple views, non-contiguous
State 01: SHARED_CANONICAL        — Multiple views, contiguous (rare)
State 10: EXCLUSIVE_NON_CANONICAL — Single owner, non-contiguous
State 11: EXCLUSIVE_CANONICAL     — Single owner, contiguous (creation state)
```

**Canonical Strides**:
```
For shape (s₀, s₁, ..., s_{d-1}):
  σᵢ = ∏_{j>i} sⱼ
Examples:
  [2, 3]     → [3, 1]
  [2, 3, 4]  → [12, 4, 1]
```

**Generation Counter**:
```
Incremented on materialization or exclusive write (COW)
Detects stale views after parent materialization
Check: view.generation < parent.generation → StaleFork error
```

---

### 3. [MEMORY_MODEL.md](MEMORY_MODEL.md)
**Purpose**: Physical storage layout and address generation

**Contents**:
- Physical storage (𝒫): 1D contiguous f32 array
- Semantic view (𝒮): (Shape, Offset, Strides) tuple
- Core index mapping formula: `phys_addr = offset + Σ(coord[i] * strides[i])`
- TensorDescriptor C-compatible binary layout (FFI-ready)
- Memory domain classification (Register, Local, Shared, Numa, Host, Device, Mmio)
- Stride/offset computation without framework overhead (O(d) where d=rank)
- Allocation patterns: dense, strided, sliced, transposed

**Index Mapping Formula**:
```
For logical coordinate X = (x₀, x₁, ..., x_{d-1}):
  physical_address(X) = offset + Σᵢ (xᵢ * strideᵢ)
Preconditions:
  - shape.len() = strides.len() = coord.len()
  - ∀ i: 0 ≤ xᵢ < sᵢ
  - physical_address < |𝒫|
```

**TensorDescriptor Layout** (76 bytes):
```
Offset   Size   Field                Type
0        8      data_ptr             *const f32
8        8      data_len             u64
16       8      shape_ptr            *const u64
24       8      shape_len            u64
32       8      strides_ptr          *const u64
40       8      strides_len          u64
48       8      offset               u64
56       1      is_contiguous        u8 (B_layout)
57       1      owns_storage         u8 (B_own)
58       2      _padding             u16
60       8      generation           u64
68       8      refcount (snapshot)  u64
```

---

### 4. [TEMPORAL_SAFETY.md](TEMPORAL_SAFETY.md)
**Purpose**: Lifetime proofs and use-after-free prevention

**Contents**:
- Lifetime algebra: ℒ_v (view lifetime), ℒ_ℬ (buffer lifetime), ℒ_𝓞 (Arc lifetime)
- Core temporal relation: `ℒ_v ⊆ ℒ_𝓞 ⊆ ℒ_ℬ`
- 5 executable lemmas with test implementations:
  - **Lemma 1**: Buffer lifetime safety (Arc::strong_count > 0 → buffer valid)
  - **Lemma 2**: Non-interference of shared views (COW isolation)
  - **Lemma 3**: Exclusive post-materialization (refcount=1 after materialize)
  - **Lemma 4**: Governance consistency (flags ⟺ state)
  - **Lemma 5**: Weak observer invariant (downgrade doesn't extend lifetime)
- Generation validation rules (staleness detection)
- Use-after-release rejection mechanisms
- COW isolation theorem with proof and executable test
**Core Theorem**: Buffer Lifetime Safety
```
∀ view V holding Arc<Vec<f32>>:
  Arc::strong_count(V.data) ≥ 1 while V is live
  ⟹ buffer remains allocated and accessible
  ⟹ lifetime(V) ⊆ lifetime(buffer(V)) ∎
```
**COW Isolation Theorem**:
```
If V_A and V_B forked from P, and V_A materializes:
  V_A.data = new Arc (exclusive)
  V_B.data = original Arc (still shared with P)
  ⟹ No interference between V_A and V_B
```
---
### 5. [PROOF_OBLIGATIONS.md](PROOF_OBLIGATIONS.md)
**Purpose**: Formal lemmas (PO-1 to PO-8) with test oracles
**Contents**:
- 8 proof obligations with formal statements and executable tests
- Test strategy for each obligation
- Cross-implementation validation approach
- Oracle behavior specifications (what Rust and Pascal must produce)
**Proof Obligations**:
```
PO-1: Contiguity Preservation
  Physical buffer size never shrinks, all addresses valid
PO-2: Mapping Uniqueness
  Index mapping is injective (no coordinate collisions)
PO-3: Governance Correctness
  B_layout ⟺ canonical strides, B_own ⟺ refcount=1
PO-4: Slice Soundness
  Slice coordinates map correctly to parent's physical addresses
PO-5: COW Isolation
  Materialization creates isolation, siblings unaffected
PO-6: Temporal Safety
  lifetime(view) ⊆ lifetime(buffer) via Arc::strong_count

PO-7: Materialization Correctness
  Values preserved, contiguity/exclusivity restored

PO-8: Generation Counter Validation
  Staleness detection after parent materialization
```
---
## Reading Guide
### For Implementers (Rust, Pascal)
1. **Start here**: [TENSOR_CONTRACT.md](TENSOR_CONTRACT.md)
   - Understand the 8 operations and their contracts
   - Implement each operation to match pre/post-conditions
2. **Then read**: [GOVERNANCE_STATE_MACHINE.md](GOVERNANCE_STATE_MACHINE.md)
   - Implement state transitions correctly
   - Maintain B_layout and B_own flags accurately
   - Manage generation counters
3. **Reference**: [MEMORY_MODEL.md](MEMORY_MODEL.md)
   - Implement address generation formula
   - Layout tensor descriptors for FFI
   - Understand memory domains for optimization
4. **Verify**: [TEMPORAL_SAFETY.md](TEMPORAL_SAFETY.md) + [PROOF_OBLIGATIONS.md](PROOF_OBLIGATIONS.md)
   - Run all 8 proof obligation tests
   - Verify against oracle behavior
   - Cross-check with other implementation
### For Architecture Review
Read in this order:
1. TENSOR_CONTRACT.md (high-level operations)
2. GOVERNANCE_STATE_MACHINE.md (state space safety)
3. TEMPORAL_SAFETY.md (lifetime guarantees)
4. MEMORY_MODEL.md (physical layout correctness)
5. PROOF_OBLIGATIONS.md (formal verification)
---
## Critical Invariants (Must Hold Everywhere)
1. **B_layout Correctness**: `B_layout = 1 ⟺ strides == canonical_strides(shape)`
2. **B_own Correctness**: `B_own = 1 ⟺ Arc::strong_count(data) = 1`
3. **Buffer Validity**: `offset < data.len() ∧ ∀ coord: addr(coord) < data.len()`
4. **Ownership Protection**: Shared tensors (B_own=0) cannot be exclusively modified without COW
5. **Materialization Correctness**: After MATERIALIZE, B_layout=1 ∧ B_own=1 ∧ offset=0
6. **Temporal Safety**: Buffer remains allocated while any view holds Arc reference
7. **Generation Monotonicity**: generation only increases (never resets)
---
## Fail-Closed Design
All operations adopt fail-closed semantics:
```
If precondition(op) fails:
  tensor state unchanged
  error returned
Else:
  operation executes
  postconditions guaranteed
  state update atomic
```
This ensures no partial updates or corrupted state on error.
---
## Implementation Checklist
### Rust Implementation
- [ ] Implement 8 operations matching TENSOR_CONTRACT.md
- [ ] Manage Arc lifecycle and refcount correctly
- [ ] Compute canonical strides per MEMORY_MODEL.md formula
- [ ] Implement COW in SET and MATERIALIZE
- [ ] Generate indices O(1) for rank 1, O(d) for rank d
- [ ] Pass all PO-1 through PO-8 tests from PROOF_OBLIGATIONS.md
- [ ] Verify temporal safety lemmas in TEMPORAL_SAFETY.md
### Pascal Implementation
- [ ] Implement reference counting (refcount management)
- [ ] Match TensorDescriptor C-compatible layout (MEMORY_MODEL.md)
- [ ] Call Rust via FFI or reimplement 8 operations identically
- [ ] Pass same oracle tests as Rust
- [ ] Verify cross-implementation consistency
---
## References
### External Standards
- Ahmad's Semantic Tensor Framework (original theory)
- BLRD Temporal Extension (lifetime algebra)
- C99 ABI (TensorDescriptor FFI layout)
### Related Documents
- NraayTensor README: ../nraay-tensor/README.md
- Implementation Notes: ../nraay-tensor/src/
- Test Suite: ../nraay-tensor/tests/
---
## Document Maintenance
**Version**: 1.0 (2025-09-22)  
**Authority**: Architecture Designer (Hardware-Oriented Tensor Governance)  
**License**: Sovereign Leviathan covenant (`LicenseRef-Sovereign-Leviathan-SL-AGPL3-001`)
---
## Quick Reference: State Machine Diagram
```
           Creation (ALLOC)
                 |
                 v
        ┌────────────────┐
        │ 11: Exclusive  │
        │   Canonical    │
        │ B_layout=1     │
        │ B_own=1        │
        └────┬───────┬───┘
             |       |
          VIEW()  TRANSPOSE()
             |       |
    ┌────────v───┐ ┌─v──────────┐
    │ 00: Shared │ │ 10: Excl.  │
    │ Non-Canon. │ │ Non-Canon. │
    │ B_own=0    │ │ B_layout=0 │
    └────────┬───┘ └─┬──────────┘
             |       |
             └─────┬─┘
                   |
            MATERIALIZE()
                   |
                   v
        ┌────────────────┐
        │ 11: Exclusive  │
        │   Canonical    │
        │ (always)       │
        └────────────────┘
```
---

## Summary

This specification suite provides:
- ✓ Complete operation interface (8 ops with pre/post-conditions)
- ✓ State machine correctness (4 states, valid transitions)
- ✓ Memory layout and FFI compatibility
- ✓ Temporal safety guarantees (no use-after-free)
- ✓ Formal verification (8 proof obligations with tests)
- ✓ Cross-implementation consistency (oracle tests)

**Implementations must pass all proof obligations and oracle tests to be conformant.**

	# NraayTensor Specification Suite

	## Overview

	This directory contains the normative specifications for the NraayTensor hardware-oriented tensor governance system. These documents define the contract that both Rust and Pascal implementations must conform to.

	All specifications are derived from Ahmad's tensor semantic framework with temporal safety extensions (BLRD model).

	---

	## Document Index

	### 1. [TENSOR_CONTRACT.md](TENSOR_CONTRACT.md)
	Purpose: Complete operation interface specification

	Contents:
	- TensorDescriptor C-compatible layout (76 bytes, 8-byte aligned)
	- 8 normative operations: ALLOC, FREE, VIEW, TRANSPOSE, RESHAPE, MATERIALIZE, GET, SET
	- Pre-conditions and post-conditions for each operation
	- Ownership effects (Arc refcount management)
	- Memory effects (buffer allocation, offset, stride computation)
	- Failure conditions and error handling
	- Pseudocode contract summary

	Key Concepts:
	```
	OP-1: ALLOC — Create tensor, B_layout=1, B_own=1, refcount=1
	OP-2: FREE — Destructor, Arc::drop, buffer deallocation when refcount→0
	OP-3: VIEW — Zero-copy slicing, new offset/strides, B_own→0, refcount++
	OP-4: TRANSPOSE — Logical permutation, metadata-only, recompute B_layout
	OP-5: RESHAPE — Safe size-preserving shape change (contiguous/exclusive only)
	OP-6: MATERIALIZE — COW-based contiguity/exclusivity restoration
	OP-7: GET — Element access (read), no state change
	OP-8: SET — Element access (write), COW if refcount>1
	```

	Critical Invariants:
	1. Physical buffer size never shrinks during view operations
	2. All address computations bounded by buffer length
	3. B_layout ⟺ canonical stride pattern
	4. B_own ⟺ refcount = 1
	5. Fail-closed: precondition failures leave tensor unchanged

	---

	### 2. [GOVERNANCE_STATE_MACHINE.md](GOVERNANCE_STATE_MACHINE.md)
	Purpose: State space, transitions, and invariants

	Contents:
	- 4-state space: (B_layout, B_own) ∈ {(0,0), (0,1), (1,0), (1,1)}
	- State diagram with all legal transitions
	- Pre/post-conditions for every transition
	- Canonical form definition and canonical strides formula
	- Generation counter management (u64 for staleness detection)
	- Invariant conditions (must hold in all states)
	- Reachability matrix showing valid transition paths

	State Space:
	```
	State 00: SHARED_NON_CANONICAL — Multiple views, non-contiguous
	State 01: SHARED_CANONICAL — Multiple views, contiguous (rare)
	State 10: EXCLUSIVE_NON_CANONICAL — Single owner, non-contiguous
	State 11: EXCLUSIVE_CANONICAL — Single owner, contiguous (creation state)
	```

	Canonical Strides:
	```
	For shape (s₀, s₁, ..., s_{d-1}):
	σᵢ = ∏_{j>i} sⱼ

	Examples:
	[2, 3] → [3, 1]
	[2, 3, 4] → [12, 4, 1]
	```

	Generation Counter:
	```
	Incremented on materialization or exclusive write (COW)
	Detects stale views after parent materialization
	Check: view.generation < parent.generation → StaleFork error
	```

	---

	### 3. [MEMORY_MODEL.md](MEMORY_MODEL.md)
	Purpose: Physical storage layout and address generation

	Contents:
	- Physical storage (𝒫): 1D contiguous f32 array
	- Semantic view (𝒮): (Shape, Offset, Strides) tuple
	- Core index mapping formula: `phys_addr = offset + Σ(coord[i] * strides[i])`
	- TensorDescriptor C-compatible binary layout (FFI-ready)
	- Memory domain classification (Register, Local, Shared, Numa, Host, Device, Mmio)
	- Stride/offset computation without framework overhead (O(d) where d=rank)
	- Allocation patterns: dense, strided, sliced, transposed

	Index Mapping Formula:
	```
	For logical coordinate X = (x₀, x₁, ..., x_{d-1}):
	physical_address(X) = offset + Σᵢ (xᵢ * strideᵢ)

	Preconditions:
	- shape.len() = strides.len() = coord.len()
	- ∀ i: 0 ≤ xᵢ < sᵢ
	- physical_address < \|𝒫\|
	```

	TensorDescriptor Layout (76 bytes):
	```
	Offset Size Field Type
	0 8 data_ptr *const f32
	8 8 data_len u64
	16 8 shape_ptr *const u64
	24 8 shape_len u64
	32 8 strides_ptr *const u64
	40 8 strides_len u64
	48 8 offset u64
	56 1 is_contiguous u8 (B_layout)
	57 1 owns_storage u8 (B_own)
	58 2 _padding u16
	60 8 generation u64
	68 8 refcount (snapshot) u64
	```

	---

	### 4. [TEMPORAL_SAFETY.md](TEMPORAL_SAFETY.md)
	Purpose: Lifetime proofs and use-after-free prevention

	Contents:
	- Lifetime algebra: ℒ_v (view lifetime), ℒ_ℬ (buffer lifetime), ℒ_𝓞 (Arc lifetime)
	- Core temporal relation: `ℒ_v ⊆ ℒ_𝓞 ⊆ ℒ_ℬ`
	- 5 executable lemmas with test implementations:
	- Lemma 1: Buffer lifetime safety (Arc::strong_count > 0 → buffer valid)
	- Lemma 2: Non-interference of shared views (COW isolation)
	- Lemma 3: Exclusive post-materialization (refcount=1 after materialize)
	- Lemma 4: Governance consistency (flags ⟺ state)
	- Lemma 5: Weak observer invariant (downgrade doesn't extend lifetime)
	- Generation validation rules (staleness detection)
	- Use-after-release rejection mechanisms
	- COW isolation theorem with proof and executable test

	Core Theorem: Buffer Lifetime Safety
	```
	∀ view V holding Arc<Vec<f32>>:
	Arc::strong_count(V.data) ≥ 1 while V is live
	⟹ buffer remains allocated and accessible
	⟹ lifetime(V) ⊆ lifetime(buffer(V)) ∎
	```

	COW Isolation Theorem:
	```
	If V_A and V_B forked from P, and V_A materializes:
	V_A.data = new Arc (exclusive)
	V_B.data = original Arc (still shared with P)
	⟹ No interference between V_A and V_B
	```

	---

	### 5. [PROOF_OBLIGATIONS.md](PROOF_OBLIGATIONS.md)
	Purpose: Formal lemmas (PO-1 to PO-8) with test oracles

	Contents:
	- 8 proof obligations with formal statements and executable tests
	- Test strategy for each obligation
	- Cross-implementation validation approach
	- Oracle behavior specifications (what Rust and Pascal must produce)

	Proof Obligations:
	```
	PO-1: Contiguity Preservation
	Physical buffer size never shrinks, all addresses valid

	PO-2: Mapping Uniqueness
	Index mapping is injective (no coordinate collisions)

	PO-3: Governance Correctness
	B_layout ⟺ canonical strides, B_own ⟺ refcount=1

	PO-4: Slice Soundness
	Slice coordinates map correctly to parent's physical addresses

	PO-5: COW Isolation
	Materialization creates isolation, siblings unaffected

	PO-6: Temporal Safety
	lifetime(view) ⊆ lifetime(buffer) via Arc::strong_count

	PO-7: Materialization Correctness
	Values preserved, contiguity/exclusivity restored

	PO-8: Generation Counter Validation
	Staleness detection after parent materialization
	```

	---

	## Reading Guide

	### For Implementers (Rust, Pascal)

	1. Start here: [TENSOR_CONTRACT.md](TENSOR_CONTRACT.md)
	- Understand the 8 operations and their contracts
	- Implement each operation to match pre/post-conditions

	2. Then read: [GOVERNANCE_STATE_MACHINE.md](GOVERNANCE_STATE_MACHINE.md)
	- Implement state transitions correctly
	- Maintain B_layout and B_own flags accurately
	- Manage generation counters

	3. Reference: [MEMORY_MODEL.md](MEMORY_MODEL.md)
	- Implement address generation formula
	- Layout tensor descriptors for FFI
	- Understand memory domains for optimization

	4. Verify: [TEMPORAL_SAFETY.md](TEMPORAL_SAFETY.md) + [PROOF_OBLIGATIONS.md](PROOF_OBLIGATIONS.md)
	- Run all 8 proof obligation tests
	- Verify against oracle behavior
	- Cross-check with other implementation

	### For Architecture Review

	Read in this order:
	1. TENSOR_CONTRACT.md (high-level operations)
	2. GOVERNANCE_STATE_MACHINE.md (state space safety)
	3. TEMPORAL_SAFETY.md (lifetime guarantees)
	4. MEMORY_MODEL.md (physical layout correctness)
	5. PROOF_OBLIGATIONS.md (formal verification)

	---

	## Critical Invariants (Must Hold Everywhere)

	1. B_layout Correctness: `B_layout = 1 ⟺ strides == canonical_strides(shape)`
	2. B_own Correctness: `B_own = 1 ⟺ Arc::strong_count(data) = 1`
	3. Buffer Validity: `offset < data.len() ∧ ∀ coord: addr(coord) < data.len()`
	4. Ownership Protection: Shared tensors (B_own=0) cannot be exclusively modified without COW
	5. Materialization Correctness: After MATERIALIZE, B_layout=1 ∧ B_own=1 ∧ offset=0
	6. Temporal Safety: Buffer remains allocated while any view holds Arc reference
	7. Generation Monotonicity: generation only increases (never resets)

	---

	## Fail-Closed Design

	All operations adopt fail-closed semantics:

	```
	If precondition(op) fails:
	tensor state unchanged
	error returned
	Else:
	operation executes
	postconditions guaranteed
	state update atomic
	```

	This ensures no partial updates or corrupted state on error.

	---

	## Implementation Checklist

	### Rust Implementation
	- [ ] Implement 8 operations matching TENSOR_CONTRACT.md
	- [ ] Manage Arc lifecycle and refcount correctly
	- [ ] Compute canonical strides per MEMORY_MODEL.md formula
	- [ ] Implement COW in SET and MATERIALIZE
	- [ ] Generate indices O(1) for rank 1, O(d) for rank d
	- [ ] Pass all PO-1 through PO-8 tests from PROOF_OBLIGATIONS.md
	- [ ] Verify temporal safety lemmas in TEMPORAL_SAFETY.md

	### Pascal Implementation
	- [ ] Implement reference counting (refcount management)
	- [ ] Match TensorDescriptor C-compatible layout (MEMORY_MODEL.md)
	- [ ] Call Rust via FFI or reimplement 8 operations identically
	- [ ] Pass same oracle tests as Rust
	- [ ] Verify cross-implementation consistency

	---

	## References

	### External Standards
	- Ahmad's Semantic Tensor Framework (original theory)
	- BLRD Temporal Extension (lifetime algebra)
	- C99 ABI (TensorDescriptor FFI layout)

	### Related Documents
	- NraayTensor README: ../nraay-tensor/README.md
	- Implementation Notes: ../nraay-tensor/src/
	- Test Suite: ../nraay-tensor/tests/

	---

	## Document Maintenance

	Version: 1.0 (2025-09-22)
	Authority: Architecture Designer (Hardware-Oriented Tensor Governance)
	License: Sovereign Leviathan covenant (`LicenseRef-Sovereign-Leviathan-SL-AGPL3-001`)

	---

	## Quick Reference: State Machine Diagram

	```
	Creation (ALLOC)
	\|
	v
	┌────────────────┐
	│ 11: Exclusive │
	│ Canonical │
	│ B_layout=1 │
	│ B_own=1 │
	└────┬───────┬───┘
	\| \|
	VIEW() TRANSPOSE()
	\| \|
	┌────────v───┐ ┌─v──────────┐
	│ 00: Shared │ │ 10: Excl. │
	│ Non-Canon. │ │ Non-Canon. │
	│ B_own=0 │ │ B_layout=0 │
	└────────┬───┘ └─┬──────────┘
	\| \|
	└─────┬─┘
	\|
	MATERIALIZE()
	\|
	v
	┌────────────────┐
	│ 11: Exclusive │
	│ Canonical │
	│ (always) │
	└────────────────┘
	```

	---

	## Summary

	This specification suite provides:
	- ✓ Complete operation interface (8 ops with pre/post-conditions)
	- ✓ State machine correctness (4 states, valid transitions)
	- ✓ Memory layout and FFI compatibility
	- ✓ Temporal safety guarantees (no use-after-free)
	- ✓ Formal verification (8 proof obligations with tests)
	- ✓ Cross-implementation consistency (oracle tests)

	Implementations must pass all proof obligations and oracle tests to be conformant.