Prism VM Evolution Implementation Plan

This plan implements the features described in in/in-4.md through in/in-7.md, plus the CNF-2 and canonical interning semantics in in/in-9.md through in/in-14.md, the milestone-gated testing workflow in in/in-15.md, the homomorphic collapse contract in in/in-16.md, and the conceptual contract in in/in-17.md, the Min(Prism) projection commutation track in in/in-18.md, the topos/sheaf formalization in in/in-19.md, the hyperlattice/Cayley-Dickson framing in in/in-20.md, and the semantic justification patches in in/in-21.md through in/in-25.md (gauge symmetry, canonical novelty, hyperoperator fixed points, ordinal boundary), plus the Agda proof roadmap in in/in-26.md, as a concrete evolution of the current prism_vm.py implementation. The commutation glossary in in/glossary.md is normative for ambiguous terms and test obligations.

Each in/in-*.md note now includes a short NOTE header indicating whether it has been refined, consolidated, or obsoleted. See audit_in_versions.md for the current cross-version audit.

Goals

Establish the Ledger + candidate pipeline as the canonical execution path.
Converge on CNF-2 symmetric rewrite semantics with a fixed-arity candidate pipeline (slot1 enabled from m2; hyperstrata visibility enforced under test guards).
Enforce univalence: full-key equality for interning and no truncation aliasing.
Introduce self-hosted CD coordinates as interned CNF-2 objects and define aggregation as coordinate-space normalization.
Preserve a stable, testable baseline while the new mode is built out.
Stage arena scheduling and 2:1 BSP locality as performance-only concerns.

Non-Goals (Initial MVP)

Full hierarchical arena migration across levels (L1/L2/global).
Perfect allocator for all graph rewrite rules beyond ADD.
Full macro system or higher-order quotation semantics.
Persistent event-log storage or snapshotting for CQRS beyond in-memory.
Treating 2:1 locality as a semantic invariant before functional correctness is locked down.
Ordinal-indexed termination proofs or proof-theoretic strength claims.

Baseline Summary (Current Code)

prism_vm.py uses a stable heap (Manifest) with:

opcode, arg1, arg2, active_count arrays.
Hash-consing via trace_cache (hint-only; no retroactive pointer rewrites).
Static optimization and branchless dispatch (optimize_ptr, dispatch_kernel).
kernel_add and a stub kernel_mul.

Architecture Decision

Ledger + candidate pipeline is the canonical execution path. Baseline PrismVM stays as an oracle. Arena scheduling is performance-only and must be denotation-invariant with respect to the Ledger CNF-2 engine; minimal scheduler variants are required by m3 for invariance tests, while performance-grade locality begins at m4+. Ledger denotation is the spec; ID equality is engine-local until baseline migrates to the Ledger interner.

Foundational Commitments (Active Now)

These are already in effect in code/tests and are treated as non-negotiable.

Canonical identity is ledger interning; interning is semantic compression (no reclamation of unique structure).
Univalence is enforced by full key-byte equality and a semantic id cap.
CORRUPT is a hard semantic error (alias risk); OOM is a resource boundary.
Sorting/swizzling and scheduling are renormalization only and must not affect denotation after q.
BSPˢ is a gauge symmetry: any BSPˢ effect must be erased by q.

Semantic Commitments (Staged)

CNF-2 symmetric rewrite semantics are the target for BSP. Every rewrite site emits exactly two candidate slots (enabled or disabled).
Slot1 continuation is enabled at m2; hyperstrata visibility is enforced under test guards (m3 normative) to justify continuation.
m1 uses the intrinsic cycle path; CNF-2 pipeline is gated off until m2.
Univalence is enforced by full-key equality (hash as hint only) and no truncation aliasing in key encoding.
CD coordinates are interned CNF-2 objects (OP_COORD_*), and coordinate equality is pointer equality.
Evaluator (Manifest/Arena) and Canonicalizer (Ledger) are linked by a total quotient map q; denotation is defined by projecting provisional nodes through q and must commute with scheduling (see in/in-16.md). q is an irreversible coarse-graining boundary, not an evaluator or scheduling step.
Reserved glyphs/roles are normative: q is meaning-forming projection, σ denotes BSPˢ permutation (gauge), and ρ denotes pointer/id remaps induced by renormalization. Never describe σ or ρ as q.
Glossary adjunction/coherence discipline is normative: any new polysemous term must declare axes, commutation equations, and test obligations.
Entropy terms are semantic descriptors (Arena vs canonical vs hyperoperator vs gauge); do not add counters unless a test explicitly requires it.
Hyperstrata visibility rule is normative from m2 for CNF-2 slot1: pre-step rows are immutable during a cycle, and within-cycle visibility is defined by the (s,t) staging order; the frozen read model is the hyperstrata collapse corollary.
2:1 BSP swizzle/locality is staged as a performance invariant:
- m1-m2: rank-only sort (or no sort) is acceptable for correctness tests.
- m3: denotation invariance must hold across unsorted/rank/morton/block scheduler variants (even if slow).
- m4+: 2:1 swizzle is mandatory for the performance profile, but must not change denotation (same canonical ids/decoded normal forms).
Baseline PrismVM is a regression implementation through m3; comparisons are on decoded normal forms and termination behavior, not raw ids.
Canonical novelty monotonicity and hyperoperator representation fixed points are semantic justifications (m3-m4); they do not imply termination and do not require operational counters (see in/in-22.md through in/in-25.md). These claims are scoped to the pre-CORRUPT (id-cap) regime.
Min(Prism) witness principle: semantic invariants proved under projection π_K are treated as representative at scale (m3+).

Staged Commitments (Not Yet Enforced)

No-copy sharing and alpha-equivalence collapse (see placeholder tests).
Binding without names (structural or coordinate-based encoding).
Damage/locality instrumentation as a performance-only concern (m4+).

Univalence Contract (Fixed-Width, No-Ambiguity Semantics)

Definition

Univalence = no ambiguity of identity. A proposed node maps to exactly one canonical node iff its full encoded key bytes are identical. Hashing, sorting, or indexing strategies may accelerate lookup, but equality is decided only by full key-byte equality.

Univalence does not require the absence of hash collisions; it requires that collisions never introduce ambiguity. Full-key comparison (or structurally collision-free indexing) is mandatory.

Canonical Key

For every interned node, define a canonical key K after canonicalization:

K = encode(op)
  || encode(rep(a1))
  || encode(rep(a2))
  || encode(extra(op))

Where:

rep(id) = canonical representative of id
- equals id in m1–m3
- becomes find(id) if rewrite-union is introduced later
Commutative ops (ADD, later others):
- sort (rep(a1), rep(a2)) before encoding
extra(op) is empty unless explicitly defined (e.g. future flags)

Two nodes are equal iff their full K byte sequences are identical.

Fixed-Width Encoding Mode (m1–m3)

In m1–m3, K uses a fixed-width encoding:

op -> 1 byte
rep(a1) -> 16 bits
rep(a2) -> 16 bits
total: 5 bytes

This encoding is injective only over a bounded id domain.

Therefore, the id bound is a semantic invariant, not a memory limit.

Representational Cap (Hard Semantic Invariant)

Define (naming is capacity vs legal id):

LEDGER_CAPACITY = 65535 (backing array length / capacity)
MAX_ID = 65534 (max legal id; LEDGER_CAPACITY - 1)
MAX_COUNT = MAX_ID + 1 (next-free upper bound; equals LEDGER_CAPACITY)
id = 0 reserved for NULL
id = 1 reserved for ZERO

Invariant:

All reachable ids used in key encoding must satisfy id <= MAX_ID.
ledger.count is a next-free pointer and may equal MAX_COUNT (full).
Any allocation that would make count > MAX_COUNT is CORRUPT.

Violating this invariant would cause key aliasing and destroy univalence.

Therefore:

Exceeding MAX_ID is CORRUPT, not OOM.
Continuing execution past this point is semantically undefined and forbidden.

Deterministic Corruption Handling (JAX-Safe)

To maintain determinism and avoid undefined behavior in JIT-compiled code:

Device-side (checked packing / interning):

If any of the following occur:
- count > MAX_COUNT
- a1 > MAX_ID
- a2 > MAX_ID
Then:
- set a persistent corrupt = True flag in the Ledger/interner state
- clamp offending values to a safe sentinel (e.g. 0) to keep execution defined
- continue execution without crashing or branching on host state

Host-side:

After block_until_ready():
- if corrupt == True, raise a hard runtime error:

RuntimeError("CORRUPT: key encoding alias risk (id width exceeded)")

This guarantees:

no silent ambiguity
deterministic failure
identical behavior across CPU/GPU backends

Indexing Rule

Hashes, buckets, sorted lanes, or Morton orderings are acceleration only.
Equality is decided only by full key-byte comparison.
Any index backend must be rebuildable from the canonical event stream and must preserve full-key equality semantics.

Relationship to COORD Primitives

The fixed-width id cap is intentional and semantic.

Growth beyond this bound is expected to occur via structure, not scalar ids:

COORD primitives (OP_COORD_*) represent arbitrarily large coordinate spaces as interned CNF-2 DAGs
Coordinate equality is pointer equality
Coordinate normalization happens before parent nodes are packed and interned

Thus:

semantic expressiveness can grow without widening id fields
the id bound remains a correctness invariant, not a scalability bottleneck

Future Extension: Variable-Length Key Encoding (Explicit Milestone)

Variable-length key encoding is not permitted implicitly.

A future milestone may introduce:

a new KeyCodecVarLen
varint or structural encoding of child ids
a radix/trie index backend

This is a semantic upgrade, not an optimization, and must:

preserve the Univalence Contract
preserve determinism
pass the same univalence and injectivity test suite

Until that milestone is explicitly landed, fixed-width hard-cap mode is the law.

Summary (Non-Negotiables)

Univalence means no ambiguity, not “no hash collisions”
Fixed-width keys are acceptable only with a semantic id cap
Exceeding the cap is CORRUPT, not OOM
Partial allocation of "new" proposals is invalid; fixed-width mode must treat any unmet new allocation as CORRUPT (no silent spawn clipping).
COORD enables structural growth without widening ids
Var-length encoding, if added, is a deliberate semantic transition

Denotation Contract

Define a shared denotation interface used for cross-engine comparisons:

denote(ptr, store) -> normal_form_ptr and pretty(ptr) -> string/tuple.
Soundness: pretty(denote_engine(expr)) == pretty(denote_ledger(expr)).
Idempotence: denote(denote(x)) == denote(x).
ID equivalence is engine-local until baseline migrates to the Ledger interner.
Termination: within the same step budget, either both converge or both do not; non-termination or timeout is treated as a mismatch.
CORRUPT dominance: if corrupt == True at any point, the denotation result must be ("corrupt", ...); clamped sentinel values must never be reported as ("ok", ...).
OOM dominance: if oom == True at any point, the denotation result must be ("oom", ...); sentinel ids returned by stop paths are not semantic values.
Univalence alignment: any engine-level compare or normalization must preserve the Univalence Contract (full key-byte equality, corrupt trap on overflow).
Structural invariants (hashes, pointer topology checks) are implementation diagnostics only; semantic claims must be stated via pretty(denote(q(...))).
Homomorphic projection: define q(provisional_node) -> canonical_id and compare denotations only after projection; evaluator steps must commute with q up to canonical rewrite (see in/in-16.md).
Normal-form reporting: pretty should return tagged outcomes (e.g., ("ok", decoded), ("oom", ...), ("corrupt", ...), ("timeout", steps)).

Locked Decisions

Read model backend (m1): keep the current ordered index (sorted lanes + binary search), maintained via full-array merge in m1. Tests assert full-key equality and do not assume any specific index structure so trie or hash-bucket indexes can replace it later.
Univalence encoding (m1): hard-cap mode with 5-byte key; enforce LEDGER_CAPACITY = 65535, MAX_ID = 65534, and checked packing for a1/a2.
Aggregation scope (m4): coordinate aggregation applies to OP_ADD only; OP_MUL remains Peano-style until explicitly lifted.

Workstreams and Tasks (Tests-First Policy)

For each step below:

Add pytest tests for expected behavior and a null hypothesis case.
Add program fixtures (in tests/ or a dedicated programs/) mirroring the pytest coverage for black-box validation.
Commit tests first, then implement, then commit again.

Section 0 is Ledger-only (m1). Sections 1-2 land in m2 to introduce the CNF-2 pipeline and the q boundary. Sections 4-9 supply scheduler variants needed for m3 denotation invariance; performance-grade locality remains m4+.