RFD 0085 — Incremental rule circuit compiler
State: accepted — partially implemented (incremental circuits remain gated; Product rollout is implemented but not yet the process default)
Decision
Argon will compile accepted rule programs into immutable incremental circuit plans and execute signed mutation batches through persistent circuit instances. The circuit compiler is a new reasoner backend. Existing maintenance and cache systems are reusable evidence and fallback mechanisms, not this RFD’s plan or architecture.
This record refines RFD 0018’s DBSP objective after RFD 0021 rejected a Feldera fork in favor of Argon’s own operators. It realizes RFD 0018’s signed Z-set, arrangement, incremental-maintenance, differential-oracle and durable-read-model direction as a persistent compiled rule circuit. It does not replace RFD 0018’s event-log authority, valid-time separation or independent Established oracle. Where RFD 0018 describes DRedc as the shipped incremental ceiling or batch WFS as the only WFS implementation, this record adds the gated circuit and Product backends while retaining those implementations as fallback and oracle paths.
Objective
Compile an accepted Argon rule program Q into a persistent circuit QΔ that
maps signed base-relation batches to signed derived-relation batches. This is
rule-program incrementalization, distinct from retaining parser or checker
queries between source revisions.
For every committed input prefix, the load-bearing equality is:
integrate(QΔ(input deltas through frontier t))
= Engine::evaluate(integrate(input deltas through frontier t))
The construction follows DBSP:
QΔ = differentiate ∘ lift(Q) ∘ integrate
Primary references:
- DBSP: Automatic Incremental View Maintenance for Rich Query Languages
- DBSP: Incremental Computation on Streams and Its Applications to Databases
The implementation sequence follows the DBSP implementation packet assembled from the repository’s decision records, current-engine audit and primary literature. That packet is design evidence rather than repository authority; this RFD is the decision record that ratifies the sequence.
The unpublished manuscript A Well-Founded Reasoning Substrate for Knowledge Representation informed the operator inventory. It is a local research input, not a publishable authority or normative dependency of this decision.
This RFD owns the complete program, but each phase has an independent admission boundary. Phase A is the ordinary set-valued, strict-stratified circuit. Phase B adds the evidence-for/evidence-against pair representation. Phase C admits retraction through that pair only after its provenance projection obligation is mechanized. Phase D adds incremental well-founded recursion. Phase E makes the state durable. No later phase is implied by an earlier phase’s implementation.
Terms and identity
RelationIdis the module-qualified relation identity plus its declared arity and canonical column schema. Generated helper relations use their generated, module-qualified identity. A short relation name is never an execution key.NodeIdis a collision-checked digest over the module commitment, local identity stratum/SCC identity, producer-rule identity, structural operator path, operator kind, input ports, relation identities, keys, projections and expressions. Node vector position is not identity. A digest collision is a compile refusal. An operator separately retains its global scheduling stratum. Whole-program rebasing changes scheduling order without changing local node identity.CircuitPlanIdcommits to the circuit schema version, the sorted multiset of exact compiled-rule commitments, and the complete canonicalCircuitPlanencoding. The plan retains 32 bytes per source rule, not another rule copy.CircuitInstanceIdis(tenant, fork, module commitment).- A
Frontieris the totally ordered event-log position for one tenant/fork. A batch names(prior_frontier, next_frontier, batch_commitment), wherenext_frontieris the exact successor committed by storage. A duplicate with the same next frontier and commitment is idempotent; a conflicting duplicate, gap or out-of-order batch is refused without state change.
The module commitment covers the canonical compiled rules independent of input enumeration order, rule identities, stratification, inline and other module-static relations, world assumptions, metric/clock declarations, canonical tuple/value encoding version, lowering version and optimizer version. It is the artifact’s semantic module commitment, not a storage generation. Storage generation is a coherence signal and frontier input. Circuit schema version belongs to the plan and checkpoint compatibility keys.
Boundary
source rules + catalog statistics
|
v
QueryEngine physical preparation
| optimized rules
| one accepted stratification
| physical strategy
| module commitment
|
v
incremental circuit compiler
|
v
immutable CircuitPlan + module commitment
|
v
CircuitInstance per tenant/fork/module
| persistent operator state
| persistent arrangements
| published frontier
v
signed derived batches and current model
System ownership
source packages
|
v
parser -> checker -> elaborator -> compiled rules + module commitment
|
v
incremental circuit compiler
|
immutable CircuitPlan
|
+----------------------+----------------------+
| |
v v
full evaluator and oracle CircuitInstance registry
|
tenant / fork / module
|
traces + arrangements + frontier
|
v
runtime read model
Implementation boundaries
incremental/
ir immutable typed plans and identities
commitment canonical versioned plan/module encodings
compile acyclic lowering and admission
compile/recursion SCC analysis and feedback-cut planning
circuit instance, frontier, scheduling, atomic publication
circuit/analysis immutable fusion, liveness and retention metadata derived from the plan
circuit/profile retained operator state and publication journals
circuit/profile/antijoin_support temporal exclusion support storage and preparation
circuit/profile/aggregate_state canonical retained aggregate fold model
circuit/profile/count_patch aggregate group preparation and atomic publication patch
circuit/profile/parity profiled-to-integrated retained-state parity checks
circuit/profile/sparse_profile sparse signed support, cardinality and rational histories
circuit/profile/transaction validated retained-state transaction preparation
circuit/profile/record_state/access selective record-backed evaluator reads
circuit/profile/record_state/codec semantic-to-record identity conversion
circuit/profile/record_state/prepare scalar and Product transaction preparation
circuit/profile/time_profile generic sparse logical-time delta history
circuit/join bilateral join state and journals
circuit/antijoin keyed exclusion state and journals
circuit/multijoin/record_codec record-backed scalar-key and evaluation-row adaptation
circuit/aggregate grouped fold state and journals
circuit/profile_eval/distinct temporal zero-crossing state
circuit/profile_eval/count temporal grouped cardinality state
circuit/profile_eval/count/change semantic and record input-delta derivation
circuit/profile_eval/count/fold generic retained aggregate-fold maintenance
circuit/profile_eval/count/output temporal aggregate output differentiation
circuit/profile_eval/profile_flow generic temporal transport, projection and publication helpers
circuit/profile_eval/factorized_aggregate factor/group transition orchestration
circuit/profile_eval/factorized_aggregate/record record-backed factorized adaptation
circuit/profile_eval/factorized_projection canonical projection folds and results
circuit/profile_eval/state_view/record shared ordinary/Product record execution; logical-time antijoin modes
checkpoint/schema frozen versioned wire declarations; no conversion or restore policy
checkpoint/canonical representation-neutral canonical sparse-profile validation
checkpoint/integrated integrated operator state conversion and reconstruction
checkpoint/factorized factorized aggregate profile conversion and reconstruction
checkpoint/migrate explicit conversion from supported historical wire schemas
checkpoint/payload payload validation and off-path instance reconstruction
checkpoint/profile whole-profile conversion and immutable-plan validation
checkpoint/record record-backed profile conversion and reconstruction
checkpoint/semantic semantic-profile conversion and reconstruction
checkpoint/state semantic/wire conversion and off-path instance reconstruction
checkpoint/validate restored-state invariants against the immutable plan
checkpoint/validate/semantic semantic-profile restored-state invariants
checkpoint/validate/record record-backed restored-state invariants
checkpoint/envelope bounded canonical framing, checksum and version dispatch
recursive_rules/adapter semantic recursive construction and transaction orchestration
recursive_rules/adapter/construction admission and immutable SCC-state construction
recursive_rules/adapter/assignment shared semantic and record-backed assignment preparation
recursive_rules/adapter/interned record-resolved read projection; no scheduling authority
recursive_rules/adapter/legacy_oracle test-only encoding boundary for differential evaluation
recursive_rules/adapter/plan_support fragment admission, relation shapes and join-cache construction
recursive_rules/adapter/record_codec stateless semantic/record delta conversion
recursive_rules/adapter/semantic_transaction frontier admission and semantic transaction preparation
recursive_rules/adapter/sink_profile recursive sink-profile selection and composition
program/well_founded record-native WFS state and atomic journals
executor/wfs immutable gamma lowering and batch oracle
nested_trace time-indexed signed trace algebra
recursive SCC-local nested-time scheduler
arrangement persistent indexed Z-set state
zset exact checked signed multiset
maintainer/circuit catalog adapter and whole-program routing
query_engine public construction seam
runtime durable append, visible frontier and cache ownership
Dependencies point downward through this list: runtime uses the query-engine facade; the maintainer adapts catalogs to circuit batches; circuit execution consumes immutable plans; operator modules depend on Z-sets and arrangements. The compiler never depends on mutable circuit state. Operator implementations do not read runtime catalogs, environment flags, storage generations or tenant registries. Recursive scheduling does not call the full evaluator; fallback is a maintainer-level whole-program decision.
factor and outer corrections
|
v
factorized_aggregate -- group selection, retained-state merge, journal
|
v
factorized_projection -- None | Linear | Distinct | Extrema, validation, value fold
|
v
temporal output correction
Live projection variants encode the aggregate family they maintain. Adding an indexed nonlinear fold changes projection mutation, merge, validation and observation there without adding representation branches to group-transition orchestration. The checkpoint DTO retains the generic legacy leaf shape only as a wire-compatibility boundary; runtime state never adopts it.
Files are split by state ownership, not merely by size. Transaction preflight
and publication remain centralized so an operator cannot publish independently.
Each operator module owns its state, journal, preflight, delta evaluation and
invariant tests. Canonical encoding is a separate module and must not use Rust
Debug output. Integration and benchmarks use only public circuit interfaces.
Join correction semantics are representation-independent; journal encoding is
not. The semantic backend journals time-indexed tuples. The record backend
journals canonical (key identity, time, tuple identity, weight) entries created
from the same semantic correction in the caller-owned record transaction.
Publication consumes those identities directly and never resolves a tuple to
reconstruct its key. The backend contract associates the journal type with the
state representation, so a semantic journal cannot reach record publication or
vice versa. Both forms still execute one bilinear join and correction algorithm.
Implemented architecture status (2026-07-18)
The implementation establishes this ownership path:
QueryEngine
|
+-- seed module-static inputs
+-- select policy and catalog compatibility
+-- prepare one owned physical rule program
v
typed admission decision
|
v
maintainer adapter -> immutable acyclic or whole-program circuit plan
As of 2026-07-20, recursion through negation is admitted through a typed well-founded component. This is a correctness and integration step, not the Phase-D incremental alternating-fixpoint algorithm:
signed program batch
|
v
dependency-filtered record deltas
|
+-- empty ------> retain inputs + (true, possible) pair
| |
| v
| emit no derived delta
|
`-- changed ----> transaction-local input snapshot
|
v
batch WFS from precision bottom
|
v
validate true subset-of possible
|
v
derive true + undefined deltas
|
validate all component journals
|
v
atomically publish state + frontier
The component retains exactly one record-native representation of its inputs,
well-founded-true extent and well-founded-possible extent. Checkpoints use the
same semantic state. Preparation either produces an explicit unchanged journal
or a complete replacement journal; failure cannot mutate published state.
Every changed dependency currently rebuilds the complete component from
precision bottom when the dependency’s logical membership changes. Positive
support changes that do not cross zero update sparse absolute input assignments
without changing the pair: WFS reads EDB set membership, so 1 -> 2 and
2 -> 1 cannot change gamma or its fixpoint. Reusing the previous approximation
across a membership change is forbidden until the Phase-D equivalence
obligation is discharged.
The stable-revision loop is representation-independent: it owns the sequential
upper = gamma(lower); lower = gamma(upper) order, precision-bottom start,
per-round K3 validation, convergence bound and round count. The current encoded
gamma oracle and future record-native coordinate circuits share this driver.
Committed transaction telemetry distinguishes WFS component rebuilds from
stable-revision rounds; unchanged and membership-invariant journals report zero
for both.
The record-native gamma coordinate is compiled as an ordinary program circuit after replacing in-component NAF reads with fixed-assumption input ports:
base record deltas -----------------------+
|
assumption-coordinate deltas v
| signed program circuit
v |
fixed-assumption antijoin ports |
| |
+----------------------------------+
|
exact gamma output delta
Executable gates cover both acyclic gamma bodies and positive-recursive gamma bodies while inserting and retracting assumptions. The encoded batch stability step remains production authority until the coordinate circuit is driven by the shared stable-revision scheduler and differentially reproduces complete true and possible pairs.
Gamma admission is immutable plan state. Its closed component plan contains an ordered vector of acyclic and positive-recursive lowerings; a nested well-founded component is a compile refusal. A domain-separated gamma commitment is included in the enclosing WFS component commitment and therefore in the whole-program plan identity. Runtime execution cannot silently switch between encoded and circuit gamma after checkpoint compatibility has been established. Admission also requires every embedded acyclic plan, nested recursive plan and recursive SCC to retain its canonical identity. Because an operator identity commits its input identities, relation columns, join keys, predicates, expressions, aggregate configuration and projection, this validates the complete connected physical body without a second lowering representation. Exact source-rule commitments and per-rule output correspondence then bind that canonical graph to the rewritten source. Semantic differential tests against fresh Established evaluation remain the independent compiler-correctness oracle.
The acyclic gamma session is a closed interned component over the parent WFS record arena and record transaction. It owns only transaction-local derivative state, an inner frontier and complete typed output extents. Each assumption revision prepares, validates and commits into that ephemeral component; record identities remain valid in the parent transaction. No nested program executor, record arena, checkpoint authority or published frontier exists. The session is discarded after the bottom-founded outer revision completes.
Positive-recursive gamma uses the same session boundary. Its signed assumption
changes enter the interned recursive correction journal; nested-time profiles,
causal distinct state and complete output extents remain transaction-local and
share the parent record transaction. Both gamma component kinds therefore expose
one revise(changes) -> complete typed extents contract to stable revision.
Gamma plans execute in checked mode: one fresh shared-arena session runs from precision bottom through the representation-independent stable revision scheduler, while the encoded batch evaluator independently computes the same transaction. Preparation publishes only when every gamma step and the complete true/possible pair agree. Direct EDB facts on WFS heads remain a separate transaction-local base extent and are set-unioned with derived gamma output.
Removing negative edges can split one WFS SCC into multiple gamma strata. The immutable gamma plan therefore owns an ordered closed vector of acyclic and positive-recursive components plus the canonical program flow plan. Each revision propagates record deltas through that vector in dependency order; all components share the parent transaction and advance once per revision. A failed inner stage poisons the disposable session. No partially advanced session, record transaction or gamma frontier enters published WFS state.
Gamma preparation uses owned sparse overlays. Acyclic stages accumulate record profiles, sink assignments and ordered multi-join journals against immutable published state, then finalize once. Positive-recursive stages additionally use a structurally shared scheduler snapshot: trace-spine batches remain shared while each correction publishes privately into the staged spine. Sparse projection assignments are chained against the staged scheduler and finalize as one generation advance. Outer preparation therefore performs no mutation of a published gamma component and copies no retained tuple history.
Gamma publication uses a sealed commit object. Sealing consumes the prepared component journals, validates their count, variant, generation and record transaction, and pairs each journal with its concrete mutable component before the record arena is published. The infallible commit phase therefore contains no parallel-vector alignment, variant fallback or validation-by-convention.
Gamma derivative state is a recoverable physical index, not checkpoint
authority. WFS checkpoints continue to encode only inputs, true and possible
extents. Restore instantiates empty gamma components, evaluates exactly
gamma(possible) over checkpoint inputs, requires equality with checkpoint
truth, and publishes the reconstructed profiles only inside the private restore
transaction. The first post-restore mutation therefore resumes retained gamma
state without serializing a second logical representation.
A fixed-delta benchmark over independent self-loop game nodes confirms the boundary. Adding one exit edge changes one logical region but rebuilds the full component:
| Retained edges | Component rebuild p50 | Established full evaluation p50 | Ratio |
|---|---|---|---|
| 100 | 337.67 us | 286.63 us | 1.18x |
| 1,000 | 3.767 ms | 3.160 ms | 1.19x |
| 10,000 | 42.470 ms | 35.736 ms | 1.19x |
The overhead is record conversion, K3 materialization, delta construction and transaction validation around the same batch WFS kernel. Unaffected frontiers reuse retained WFS state, report zero rebuilds and measured 0.538 us, 0.604 us and 1.057 us p50 at the same retained sizes. Mutation-local speed requires the proof-gated coupled-circuit design below.
Cross-frontier reuse retains gamma derivative state, not the previous WFS
approximation. For a changed base E -> E', the coordinate applies the signed
base correction together with the signed reset from its prior assumption to the
empty assumption. Stable revision then starts again with logical lower extent
empty. This computes gamma_E'(empty) incrementally while preserving the
bottom-founded lfp(gamma^2) construction. Seeding the new revision with the
prior true or possible extent is forbidden: arbitrary signed base changes do
not preserve the subset direction required by that shortcut.
The circuit-checked validation backend deliberately runs both the encoded batch kernel and a fresh record-native stable revision before publication. Its measured component-rebuild p50 is 1.854 ms, 23.442 ms and 276.36 ms at 100, 1,000 and 10,000 retained edges: 6.47x, 7.42x and 7.73x the established evaluator. These numbers measure a differential-validation configuration, not a production cutover. Circuit authority requires the differential gates below; retaining the encoded evaluation after those gates would make the cutover predictably slower.
Release circuit authority omits the encoded catalog and oracle evaluation. Its component-rebuild p50 is 1.560 ms, 20.472 ms and 243.51 ms at the same sizes, 15.8%, 12.7% and 11.9% below checked mode but 5.44x, 6.48x and 6.81x the established evaluator. Circuit authority removes duplicate execution; it does not make a fresh bottom-founded rebuild mutation-local. Production speedup requires retaining the coupled WFS coordinates across frontiers under the proof obligations below. Debug and test builds retain per-step and final-pair encoded differential checks; both configurations publish the circuit-produced pair.
Retaining gamma derivative state across frontiers produces rebuild medians of 1.517 ms, 19.499 ms and 230.54 ms. The corresponding established medians are 0.287 ms, 3.181 ms and 35.577 ms, making retained gamma 5.28x, 6.13x and 6.48x slower. The stable revision remains bottom-founded and must retract the prior possible assumption; on the independent self-loop workload that reset touches nearly every retained tuple. Retained physical indexes are necessary for incremental WFS, but they do not make the logical coordinate reset mutation-local. Removing that reset requires the coupled-coordinate proof gate in Phase D, not another storage optimization.
Changing one existing input’s positive support without crossing zero measured 1.349 us, 1.440 us and 1.915 us p50 at 100, 1,000 and 10,000 retained edges.
The common sampled-maintainer harness measures heap and semantic restoration at 10,000 retained edges. With separate gamma roles, caller-owned coordinate time and one causal coordinate representation, a 30-sample one-edge mutation measured 3.868 ms p50 for the circuit versus 44.493 ms for established maintenance: the circuit was 11.50x faster. Retained heap was 6,938,074 bytes versus 3,523,417 bytes, or 1.97x. Construction peaks were 48,986,175 and 9,906,899 bytes; mutation peaks were 13,279,511 and 14,451,485 bytes. The circuit transaction reported one WFS rebuild and two stable-revision rounds. A 100-edge mutation measured 6.089 ms circuit versus 46.918 ms established, or 7.71x faster, with the same retained heaps. Record-native rebuilding is already faster than the encoded established evaluator, but its work still depends on retained component size. The journal and commit work is proportional to touched input records; the alternating fixpoint remains a whole-component reset/replay rather than mutation-local maintenance.
Physical preparation fixes rule order, dictionary-independent module identity, catalog-bound execution constants, stratification, dependency metadata and coarse join strategy once. Accepted incremental lowering consumes that stratification directly. It does not invoke a second positive-recursion or stratification analysis. Unsupported physical operators and strategies remain typed refusals, and their evidence is retained in the selected fallback route.
Recursive trace time is the product order of outer committed frontier and inner fixed-point iteration. Its partial order and least upper bound are componentwise; compaction and suffix correction therefore cannot collapse an inner iteration merely because its outer frontier is earlier. The program instance owns outer frontier and transaction identity. Recursive components own only nested trace state.
Well-founded execution has two distinct clocks. A gamma revision frontier may
advance multiple times while stable revision computes one coordinate
publication. A coordinate epoch advances exactly once when the causal truth and
falsehood scheduler publishes that replacement. Coordinate scheduler state and
journals therefore use a private CoordinateEpoch type; conversion to the
generic recursive frontier occurs only at the nested scheduler boundary. Gamma
revision helpers cannot accept a coordinate epoch, so accidental synchronization
or comparison of the two clocks is unrepresentable.
Signed changes that reach a positive recursive component execute through the
nested circuit. One transaction-local evaluation session propagates each newly
produced feedback delta, maintains causal distinct zero crossings and prepares
the recursive trace, circuit state and relation projection as one journal.
Retractions confined to an acyclic upper stratum continue through the ordinary
circuit. Unsupported rule operators remain a whole-program admission refusal;
they do not produce a mixed circuit/batch transaction.
The published recursive trace materializes its current inner-iteration profile behind a shared immutable snapshot. Starting a mutation is therefore constant time per SCC relation rather than proportional to outer history. Publication updates only changed tuples and the canonical history and current profile are committed by the same prepared trace assignment.
Recursive body evaluation is stage-local. A feedback stage evaluates only its new profile against published state and the transaction-local overlay. For a join it emits each bilinear term exactly once:
new left join (published right + staged right)
+
(published left + staged left) join new right
+
new left join new right
The session returns only newly produced sink profiles. The recursive controller retains future iteration buckets until their causal iteration is sealed. A global suffix recomputation exists only as a test oracle; it is not a production maintenance path.
Causal distinct sealing is correction-driven and tuple-local. A tuple becomes active only when a candidate correction reaches it. Its cursor retains old and corrected support, old membership and the current membership difference. Late activation reconstructs that tuple’s retained prefix pointwise and validates its retained output history. A transaction-local wake index schedules only current candidate cells and future nonzero cells from an activated retained profile; iterations with no old or new support change do not revisit the tuple. The wake index is derived scheduling state, not a second checkpoint authority. Prepared cursor transitions and wake assignments publish only after every relation succeeds. The evaluator registers future candidate-bucket horizons separately, so an empty current output cannot terminate before an already-produced future candidate bucket. Untouched retained tuples are neither activated nor replayed.
Recursive implementation ownership follows the same publication boundary:
recursive/state.rs SCC facade and insertion scheduler
recursive/state/relation.rs candidate history and membership projection
recursive/state/distinct.rs tuple-local causal distinct session
recursive_rules/adapter.rs construction, admission and evaluator binding
recursive_rules/correction.rs signed causal correction orchestration
recursive_rules/transaction.rs prepared validation and atomic publication
recursive_rules/publication.rs jointly published scheduler/evaluator state
Candidate staging only consolidates the current bucket. Tuple activation and
retained-profile validation occur atomically at sealing. Consequently an
unsealed +Δ followed by -Δ neither activates a cursor nor extends the
iteration horizon, and staging does not clone the active cursor map.
Each recursive profile trace owns its cumulative inner-iteration deltas. Each
tuple-local sparse profile caches its checked integrated support; membership is
the support > 0 projection. A prepared patch changes cells, computes cached
support from the completed atomic assignment, and validates the caller’s exact
membership zero crossing before infallible publication. No independently
mutable candidate-support or settled-membership collection exists. Point
membership remains logarithmic in retained profile tuples. Full catalog
projection scans retained profiles and filters zero support; deletion-heavy
catalog materialization must be benchmarked before routing because causal
history deliberately outlives current membership.
Integrated operator output is retained only when a later derivative reads its prior value: join and antijoin inputs, aggregate inputs and distinct support. Other node deltas remain frontier-local. A sole-consumer scan followed directly by projection is fused during delta propagation. The immutable plan and its canonical identity remain unchanged. This removes redundant persistent stateless outputs and transient per-row binding maps without changing operator semantics or checkpoint authority.
Equality by construction
Differential equality is a gate, not a synchronization mechanism. The engine must not retain several mutable semantic copies and rely on tests or procedural update order to keep them equal. DBSP defines one algebraic state: integrated Z-set traces. Arrangements, settled recursive extents, catalogs, checkpoints and emitted batches are indexes or projections of that state.
The live ownership model is:
CommittedDelta<RelationId>
|
v
ProgramPlan.prepare(&PublishedSnapshot, delta)
|
v
ProgramJournal
|
v
publish once, infallibly
|
v
PublishedSnapshot
|-- one transaction token and outer frontier
|-- integrated typed relation/operator traces
|-- indexes owned by their authoritative traces
|-- nested recursive time below the outer frontier
`-- one union catalog + sparse base provenance on rule heads
PublishedSnapshot is the only live semantic state. For maintainer-owned
acyclic circuits, its catalog is authoritative for base input membership because
ProjectionMaintainer::read_model must return &RelationCatalog; the circuit
explicitly delegates input authority and retains only derivative state. A
standalone CircuitInstance remains self-contained. Delegated instances refuse
standalone checkpoints until the enclosing recovery record can restore the
catalog and circuit together. Derived support remains typed circuit authority.
The catalog is its read projection, and direct facts are retained separately
only for rule-head tuples whose base and derived support can overlap. The same
journal publishes all three zero-crossing decisions; no complete base or
derived catalog is retained.
Every component implements the same transaction algebra:
prepare(&PublishedState, Delta) -> Journal
validate(&PublishedState, &Journal) -> Result
publish(PublishedState, Journal) -> PublishedState
Preparation and validation are read-only. Publication consumes a fully checked
journal and cannot fail. Component journals compose in plan order into one
whole-program journal; lower strata, recursive components and sinks never
publish independently. The program instance alone owns outer frontier,
idempotence and last-commit identity. Recursive components own only nested
(outer frontier, iteration) traces.
Redundant physical state is allowed only behind an owner that makes divergence unrepresentable. An arrangement belongs to its relation trace and is changed by the same prevalidated assignment. Recursive membership is derived directly from the candidate profile’s private cached support. A checkpoint serializes one published snapshot; restore constructs and validates a replacement snapshot before registry adoption. No API can restore fields into a live instance individually.
String relation names and RelationCatalog exist only at the projection/input
boundary. Plans, committed deltas, dependencies, operator state, journals and
sinks use RelationId. Runtime and conformance callers construct and observe
incremental maintenance only through QueryEngine; circuit implementations,
checkpoint DTOs and journals are crate-private.
Target module ownership is:
incremental/
plan/ immutable typed IR, identity, compile, validate, encode
state/ published snapshot, traces, arrangements, operator state
transaction/ commit token, journal composition, prepare, publish
operator/ linear, join, antijoin, aggregate, distinct
recursion/ nested time, scheduler and recursive trace; no catalog
projection/ typed catalog input and snapshot-to-catalog projection
recovery/ snapshot checkpoint codec and candidate validation
maintainer/circuit admission and fallback adapter only
query_engine sole external construction and observation seam
runtime event-log durability and snapshot-registry adoption
File moves follow ownership changes; splitting a file without removing duplicated mutable authority does not satisfy this section.
Argon’s one-plan rule applies: source rules are lowered and optimized once, and
the incremental compiler derives component plans from that accepted optimized
plan. It does not re-stratify cloned CompiledRule trees into a parallel
planning hierarchy. Coarse physical choices such as worst-case-optimal joins,
factorized aggregates and recursion remain visible to incremental lowering.
The current rule-to-circuit compiler is bootstrap code until it consumes this
shared optimized plan.
The existing full evaluator remains the correctness oracle and fallback. The existing semi-naive insertion and delete/rederive maintainer remains a benchmark baseline; it is not the new circuit’s implementation substrate.
Canonical row ownership
The program snapshot owns one row identity space shared by every incremental
component. Persistent scheduler traces and temporal operator indexes store
RecordId; they do not own decoded payloads. The projection boundary retains the
encoded catalog required by ProjectionMaintainer::read_model, while the row
arena owns the single decoded payload used by rule evaluation.
ProgramSnapshot
|
+-- RecordArena
| |-- truncated payload digest -> collision bucket of RecordId
| `-- RecordId -> one adaptive boxed value slice
|
+-- ProgramCircuit
| |-- recursive candidate profiles: RecordId -> iteration cells
| `-- temporal arrangements: RecordId -> iteration weights
|
`-- ProgramRelationStore
`-- encoded catalog required by the public read-model contract
RecordId is local to one live program snapshot. Allocation order has no semantic
meaning and is never persisted, hashed into a plan identity or exposed through
the query interface. Checkpoint writers resolve IDs to canonical tuple bytes and
sort by tuple order. Restore interns those bytes into one fresh arena before it
publishes any component state. Different replay grouping or allocation order
therefore produces identical checkpoint bytes and read models.
The arena distinguishes ordered value vectors from variable bindings. Ordered vectors cover relation tuples and projected join or antijoin keys. Bindings cover operator rows and count correlation or outer keys; their variable entries must be strictly increasing and unique. A record-kind tag prevents a value vector from aliasing a binding with the same serialized shape.
The arena index is a 16-byte truncated BLAKE3 digest over the record-kind tag and
canonical bytes. The primary tree stores one RecordId directly per digest; a
separate sparse side table stores additional IDs only on an actual digest
collision. Candidate payload equality is checked after every digest match, so
truncation affects index size and lookup cost, not identity correctness.
Published records retain one boxed value slice. Values whose complete tuple can
use the fixed-width RecordCell carrier are stored inline in that slice. A
tuple containing an allocation-owning or larger value retains one ordinary
semantic Value slice instead. Fallback is selected for the whole tuple; the
arena never adds one allocation per uncommon cell. Both forms expose the same
borrowed RecordValues view and preserve structural Value equality.
Canonical bytes and the digest are transaction-local and are not duplicated in
the record. Bindings use a boxed sorted entry slice rather than a tree per
record. An index keyed by a second decoded tuple or binding is forbidden. Every
referenced ID must resolve, and encoded restore input is accepted only when the
decoded values re-encode to the same canonical bytes.
Preparation uses a transaction-local row overlay:
published arena + input delta
|
v
RecordTransaction
|-- reuse published IDs
`-- allocate provisional IDs in an isolated suffix
|
v
component journals reference published or provisional IDs
|
validate complete program journal
|
v
append arena suffix, then publish component journals infallibly
A refused transaction drops the overlay and cannot leak rows into published state. Validation proves that every provisional ID belongs to the journal’s overlay and that the arena base length still matches the published snapshot. Appending the validated suffix precedes component publication and performs no fallible semantic work.
The migration boundary is a complete maintainer-owned program. Every newly
admitted strict program uses one ProgramCircuit, including programs whose
component graph is entirely acyclic. Candidate profiles, temporal operator rows,
arrangement keys, antijoin keys and aggregate group keys change from decoded
payloads to RecordId together. Evaluator input, encoded and arrangement stores
are delegated to the enclosing projection and remain empty.
Adding an arena while either the scheduler or temporal profiles still retain
the same decoded tuple payload is forbidden: that would add a third physical
representation rather than replace one. Standalone circuits retain their
self-contained generic tuple state only as a differential oracle and as the
restore target for legacy acyclic checkpoints. New production admission never
constructs that carrier.
accepted optimized physical program
|
v
ProgramCircuitPlan
|
+--------+--------+
| |
acyclic components recursive components
| |
+--------+--------+
|
shared RecordArena
|
atomic ProgramJournal
|
ProgramRelationStore
|
public read-model catalog
legacy acyclic checkpoint --> restore-time migration --> record-native component
Every newly constructed strict component is record-native. Join, antijoin, distinct, Count, CountDistinct, Sum, Avg, Min and Max corrections publish through the shared record-profile journal. Legacy semantic acyclic checkpoint DTOs are migrated into that record-native component before the restored program becomes observable; no semantic acyclic runtime variant remains. Checkpoint validation derives the supported aggregate set from the same operator capability predicate used by record-profile admission.
Sparse row histories use one canonical small-vector representation. The common single-cell history is stored inline; longer recursive histories spill without changing evaluation semantics. Checkpoint DTOs continue to encode ordinary vectors, so this storage choice is neither a wire shape nor a second authority.
All currently admitted positive-recursive operator shapes cross this boundary together. There is no workload-specific alternate executor. Metrics count arena rows separately from candidate cells and temporal index cells so payload ownership is distinguishable from semantically necessary time and support indexes.
Semantic and record-backed execution share one value-access contract. Scan matching, repeated-variable equality and Generic Join key construction are one algorithm parameterized by borrowed value access; storage adapters cannot silently acquire different semantics. Comparisons borrow arena values. Cloning occurs only when an operator emits a new tuple or crosses a checkpoint, read-model or full-evaluation boundary.
A record-backed join interns each correction key and tuple once. The same canonical correction entries probe published and transaction-staged arrangements, then move into the join publication journal. No second projection, digest lookup or semantic-key journal is retained.
Transient operator rows use a session-local identity space. A local row owns a
canonical binding or value vector until it becomes part of a persistent
arrangement, support index, sink or prepared journal. Promotion then moves the
payload into the transaction record suffix once and caches the resulting
RecordId; repeated and overlapping promotion reuses that identity. Rows
discarded by filter, cancellation or liveness release never enter persistent
state.
one record transaction
|
+-- evaluation session ordinal 0
| |-- local scan/filter rows
| `-- explicit escape set --> cached RecordId promotion
|
+-- evaluation session ordinal 1
| `-- independent local identity space
|
`-- validated persistent record suffix
The transaction token plus caller-owned session ordinal prevents a stale local identity from resolving in a later recursive round. Session IDs and local row IDs are neither semantic nor durable. Promotion validates the complete escape set before mutating the record transaction. Digest matches always confirm structural payload equality, including after the local payload has moved and only its cached record remains.
Session-local lookup keys are ephemeral acceleration state. Each evaluation owns a randomized hash builder and maps a 64-bit key to an exact structural collision bucket. The seed and key never enter a row identity, journal, checkpoint or plan commitment. This avoids a cryptographic digest for every transient join binding while retaining exact equality and collision safety at the only semantic boundary.
Profile orchestration is parameterized by backend-owned transient and sink row
identities while retaining one immutable schedule. Scan, filter, map, project,
sink, join, distinct, antijoin and aggregate behavior remains behind one
ProfileStateView contract. This permits the record backend to replace owned
semantic rows operator by operator without copying the schedule or introducing
workload-specific execution routes.
The ordinary record backend implements the first complete native slice:
record scan
-> borrowed record-backed binding
-> binary join / fused or explicit projection
-> support distinct
-> sink identity
-> selective persistent promotion
A bijective unique-variable scan binding retains its canonical source tuple and an immutable shared variable-to-position map. Owned and record-backed bindings use the same allocation-free structural digest and exact equality check, so their identity is representation-independent. Join corrections reuse the source tuple identity when variable order matches and promote only keys and tuples required by the persistent arrangement journal. Distinct promotes only touched support identities and emits corrections under the original transient identity. Sink validation checks row kind without materializing values.
Filter evaluates directly through borrowed record bindings and preserves row
identity. Computed map retains the shared expression evaluator as semantic
authority, materializes one touched binding because that evaluator requires
stable borrowed Value references, and interns the result immediately. It does
not materialize the input profile. Scan, projection and sink carrier operations
are time-generic shared record-backend components rather than ordinary/Product
copies. Ordinary antijoin constructs persistent
arrangement corrections from transient bindings, reads retained support and
timelines directly by record identity, and emits borrowed retained bindings.
Semantic and record execution share one support zero-crossing transition law.
Ordinary count-family input reads transient rows without constructing semantic
profiles. Each touched compact binding is decoded once, then semantic and record
execution share one binding-change function. Corrections and retained groups
remain record-native through evaluation; record output resolves only an emitted
outer binding or extrema winner. Semantic and record output share one generic
aggregate-level law and temporal differentiation driver. Factorized aggregate
outer and factor inputs also read transient rows without constructing semantic
profiles and share aggregate binding-selection helpers with count-family input.
Ordinary factorized corrections and retained groups remain record-native through
evaluation. Projection preparation, group validation, scalar aggregate-level
evaluation and temporal differentiation are representation-generic. The record
emitter constructs only transient row identity; the shared temporal law owns
support weight. Ordinary multiway joins read produced transient value rows and
emit transient value identities directly. Semantic and record carriers share
one changed-input partition, trie-overlay Generic Join, temporal weight product
and error propagation path; only key access and output construction vary.
Product/WFS creates one transient identity space per staged revision and uses
the same record carrier for scan, filter, map, project, join, distinct, count,
factorized aggregate, multiway join and sink. Only escaping operator and sink
rows are promoted before persistent preparation. Product antijoin groups
corrections, reads touched retained windows and journals state by record
identity. Semantic and record execution share one generic causal differentiation
law over representation-owned keys and rows. The record emitter borrows the
retained tuple identity as a transient binding; the former semantic retained
window and reinterning adapter no longer exist.
The native multiway carrier codec is time-generic and accepts both semantic-key Product tries and compact interned-key ordinary tries. Both representations use the same changed-input partition, overlay traversal, temporal product and output emission driver. Product uses the same carrier without changing checkpoint key representation.
canonical tuple bytes
|
v
RecordArena intern
|
+-- all cells fixed-width --> Box<[RecordCell]>
|
`-- otherwise -------------> Box<[Value]>
|
v
RecordValues view
|
+-----------+-----------+
| |
scan / equality join key visitor
| |
+-----------+-----------+
|
emitted values only
|
cloned
Distribution posture
Distribution is sequenced after single-node correctness, not excluded. Phase-A execution remains local to one circuit instance, but its plan and state model must preserve these later distribution paths:
- every stateful operator declares its deterministic partition/exchange key;
- operator semantics remain pure Z-set transformations independent of worker identity and physical placement;
- plans retain explicit monotone strata and sealed non-monotone boundaries;
- transaction and iteration frontiers are instance-local logical times, never a process-global completion assumption;
- deterministic event-log replay can construct an identical read replica;
- tenant migration and replica cutover occur at an explicit logical frontier; and
- pushed federation fragments carry a placement-policy certification record sufficient to audit whether local evaluation plus merge equals global evaluation.
Positive set-valued strata may eventually use asynchronous, duplicate-tolerant lattice exchange. Signed Z-set deltas are not idempotent: distributed circuit exchange requires exactly-once, in-order delivery or an equivalent deduplication protocol. Negation, aggregates, well-founded alternation and bitemporal reads observe only sealed input frontiers. The implementation must not blur these two delivery contracts.
Circuit sharding across machines is last in the distribution sequence. Earlier paths are per-tenant placement, logical-time migration and deterministic read-replica replay. Any sharding proposal must demonstrate a measured crossover against the corresponding single-node arrangement.
Fallback is whole-program in this RFD. If any reachable rule, producer or operator is unsupported, compilation returns a typed refusal and creates no circuit state. The runtime evaluates the complete program with the full evaluator. A mixed circuit/batch plan requires a separate frozen-boundary and cross-backend atomicity design.
The correctness equality compares the complete published base-plus-derived catalog after projecting away engine-private state. Relation identities, canonical decoded tuples, Argon set membership, well-founded companion relations, and refusal/error outcomes must match. Dictionary allocation order, arrangement layout and node order are unobservable. For a circuit-admitted program every published relation has set semantics; internal operator streams retain exact integer multiplicities.
Data contract
A Z-set is an ordered map from canonical tuples to exact signed weights. Zero weights are absent. Weight accumulation is checked: overflow fails the batch and cannot mutate visible circuit state. Saturating arithmetic is forbidden.
Every input and intermediate batch is consolidated before it crosses an operator
boundary: equal tuples are summed with checked arithmetic and zero weights are
removed. Tuple encoding and ordering are canonical. RelationId carries arity;
an arity mismatch is an input or compile error, never a dropped row.
Circuit plans are immutable. Circuit instances own all mutable traces and arrangements. A plan never contains tenant or frontier state. An instance is usable only with the module commitment from which its plan was compiled.
CircuitPlan contains typed relation IDs, typed node IDs, typed input/output
ports, schemas, strata, monotonicity/sealing metadata, exchange keys, feedback
edges, sinks and the plan commitment. It is
canonically serializable and contains no mutable state. Scheduling is the stable
topological order of (stratum, SCC, NodeId), with feedback evaluated under the
nested-time order defined below.
Circuit operators
| Rule operator | Delta behavior | Retained state |
|---|---|---|
| singleton | emit one empty binding at the initial logical time | none unless consumed by a stateful operator |
| scan | forward input batch | relation trace |
| filter/map/compute | apply directly to batch | none |
| binding projection | retain selected variables as a joinable binding | none |
| join | bilateral delta join | both indexed inputs |
| multiway join | ordered multilinear delta join | one trie trace per logical atom |
| distinct | emit support zero-crossings | tuple weights |
| antijoin | emit right-support zero-crossings | left trace and right key counts |
| semijoin | emit positive right-support zero-crossings | same left trace and right key counts as antijoin |
| aggregate | update changed groups | group multiset and accumulator |
| recursion | nested delta fixpoint | recursive traces by iteration |
| sink | consolidate rule support | output weights |
union is an explicit linear operator between rule producers and a relation
boundary. It consolidates signed contributions without deduplicating them.
predicate-led body predicate-free prefix
input delta initial logical time only
| |
v v
scan singleton {}
| |
+-----------> join/filter/map <---------+
|
v
antijoin / aggregate
|
v
project -> distinct -> sink
Later frontiers inject only relation deltas. Stateful consumers retain the
initial singleton support; the singleton itself has no mutable authority.
Operator semantics:
singletonis the relational unit. It emits exactly one empty binding at the minimum logical time of a new circuit and never emits at a later frontier, recursive generation or evaluation-session ordinal. Empty bodies and bodies beginning with comparison, computation, negation or aggregation lower through this operator. The compiler does not invent a catalog relation or reorder the authored body. Stateful consumers retain its support through their ordinary join, antijoin or aggregate state, so checkpoints require no mutable singleton state.scanaccepts only the batch for itsRelationId, validates arity, and stages the exact base trace update. It does not decode or allocate relation identity.filterretains a row iff the existing expression evaluator returns true. False and undefined drop it, matching full evaluation.- Scalar filters carry one canonical predicate (
Comparisonor expressionDefined) plus an explicit selection (SatisfiesorDoesNotSatisfy). This representsnot <comparison>andnot <compute>as stateless selection, including nested negation.DoesNotSatisfyretains undefined results because Established NAF asks whether the inner atom has an extension; it is not Boolean operator inversion. Loud comparison or expression errors remain loud under either selection. Semantic and record-backed carriers interpret this same predicate IR; neither compiler path synthesizes an antijoin or reorders the rule. mapandcomputepreserve input weight. Non-injective outputs consolidate. A partial compute that is undefined drops the row. Expressions use the same value operations and error behavior as the full evaluator.binding projectionis the internal relational projection. It retains a canonical sorted subset of variables as a binding row, so subsequent joins can consume it. It does not impose set semantics; callers placedistinctexplicitly where projection collapses multiple supports. Terminalprojectremains the binding-to-head-tuple boundary.unionadds all producer weights. It does not impose set semantics.sinkconsolidates producer support, passes it through the relation-boundary distinct operator, and emits the resulting set delta in canonical order.
For join inputs A and B:
Δ(A ⋈ B) = ΔA ⋈ B_old + A_old ⋈ ΔB + ΔA ⋈ ΔB
Multiple rules may support the same tuple. Their signed contributions are summed before the relation-boundary distinct operator. Per-rule deduplication is not a substitute for relation-level support accounting.
Join
A join key is the canonical encoding of shared columns in declared key order. The output contains the left columns followed by right non-key columns. For each matching pair, weights multiply with checked arithmetic; contributions add and consolidate. Constants and repeated variables remain residual equality filters. Aliased inputs and self-joins still use two logical ports and the same old/old, old/delta, delta/old, delta/delta accounting.
Both committed arrangements are probed as pre-batch state. Temporary indexes
over ΔA and ΔB may be built for the cross term, but are staged state and are
not visible as committed arrangements until publication.
Antijoin and semijoin share one keyed existence-state representation. For left
stream L, right-key support R, and antijoin output A = L ▷ R, existential
semijoin is defined by the exact partition:
S = L - A
ΔS = ΔL - ΔA
The circuit therefore prepares one left arrangement/right-support journal and
selects its absent (A) or present (S) projection. Multiple right witnesses
never multiply left support. Nested predicate NAF with odd polarity lowers to
antijoin; even polarity lowers to semijoin. Checkpoint conversion and validation
use the same existence journal for both operators, preventing their zero-crossing
and recovery laws from diverging.
Interval-valued antijoin follows the same ownership rule. Its immutable compiled key and output projections are owned once by the plan and shared with the retained component. The component owns only mutable left/right temporal indexes; it does not clone semantic operator configuration into state. Checkpoint wire shape is unchanged because immutable projections remain plan-derived.
Explicit Kripke modal rules
The supported single-frame modal fragment lowers into ordinary relational operators. It has no modal-specific mutable state. The inner proposition is one positive predicate whose first column is the world; a modal is the sole body atom. The world domain contains both accessibility endpoints and every world in the proposition extent. A non-empty payload domain is the distinct projection of proposition payloads; a proposition with only a world column uses the relational singleton.
accessible(w, s) ----+--------------------------+
| |
proposition(s, p) ---+--> join --> diamond(w,p) |
|
accessible endpoints --+ |
proposition worlds -----+--> union --> distinct +--> World(w)
proposition payloads -------- project --> distinct --> Payload(p)
|
World x Payload -------------------------------------+--> Candidate(w,p)
|
Candidate x accessible -- antijoin proposition --> Missing(w,p,s)
|
Candidate ------------------------ antijoin Missing --> box(w,p)
diamond is existential support. box removes a candidate when any accessible
successor lacks positive proposition support. Absence therefore remains
open-world unknown and fails necessity. A dead-end world has no missing row, so
box is vacuously true. Edge and proposition changes use the ordinary join,
antijoin and distinct correction journals, including simultaneous commits and
checkpoint restoration.
An optimized 10-sample Criterion run on an Apple M5 Pro measured retraction of
one proposition from a retained 1,000-world self-loop frame at 46.046 µs for
the circuit and 519.62 ms for fresh Established evaluation at the median: an
11,284-fold latency ratio. The benchmark validates both diamond and box
extents against fresh evaluation before timing. This is a fixed-delta modal
shape, not a substitute for cross-shape latency and memory gates.
Physical preparation binds the modal accessibility and proposition relations by exact catalog name or one unique qualified-name suffix. Established evaluation and circuit compilation consume that same catalog-bound rule representation; generic scans never guess relation suffixes. Established processes plain and modal SCCs in canonical stratification order. Later positive, negation, aggregate and modal strata therefore consume complete lower modal extents, matching the circuit’s stratified relational plan.
Worst-case-optimal multiway join
A physical worst-case-optimal join is a first-class circuit node; it is never silently expanded into a binary join tree. The immutable node records the ordered predicate atoms, constant and repeated-variable guards, global variable order, head projection and one logical input port per atom. Plan identity includes that complete physical shape.
For ordered inputs R_0 .. R_n, define R'_i = R_i + ΔR_i. The transaction
uses the disjoint multilinear decomposition
Δ join(R_0 .. R_n)
= Σ_i join(R'_0 .. R'_(i-1), ΔR_i, R_(i+1) .. R_n)
Every changed derivation is assigned to its greatest changed input ordinal, so
simultaneous changes appear exactly once without enumerating all 2^n - 1
old/delta combinations. Signed weights multiply with the same checked
arithmetic as binary joins; relation-boundary distinct remains responsible for
set semantics.
Each logical atom retains a trie trace in the global variable order. A
transaction supplies read-only overlay nodes for R_i, ΔR_i or R'_i as
required by one decomposition term. Generic Join intersects the smallest
candidate set and probes the other participating tries. Constants,
variable-free guards and repeated variables use the same matcher as full
evaluation. Trie corrections are staged once and publish only after all output
terms, downstream operators and program validation succeed.
Published trie and prepared-patch child storage use the same adaptive ordered map: zero fanout has no allocation, one child uses a single boxed node and higher fanout uses a B-tree. Insertion promotes and retraction demotes this representation. Traversal, overlays and checkpoint entries expose one ordered trie abstraction, so storage density does not create a second evaluation, transaction or persistence path.
Inside a recursive component, an atom trie cannot retain only integrated
support. It retains the sparse inner-iteration profile for every key. A
correction joins atom profiles at the maximum participating inner time and
emits the correction at that time; collapsing the profile would move a
retraction to iteration zero and violate causal distinct support. Transactional
overlay layers therefore preserve both key support and iteration cells.
Recursive reader identity is (multiway-join node, atom ordinal), not only the
relation or node, so repeated aliases remain distinct. The nested plan assigns
each reader to immediate or delayed input from same-stratum producer structure;
runtime batches remain relation-addressed.
physical prepared rule
|
v
multiway join plan ------------------------+
atoms + variable order + projection |
| |
v v
per-atom trie traces <-- signed deltas -- overlay selector
| |
+-------- Generic Join visitor <--+
|
v
signed output Z-set
|
v
relation-boundary distinct
The implementation must extract the existing full-evaluation trie builder and Generic Join visitor behind one relation-read interface before circuit wiring. Required gates are full-evaluator parity, binary-join parity, simultaneous multi-input corrections, self-join aliasing, ground guards, repeated variables, negative corrections, checked overflow, prepared-journal atomicity, checkpoint round-trip, recursive temporal correction, atom-addressed feedback, and triangle/clique scale controls. Admission remains a typed whole-program fallback unless these gates pass for the selected physical shape.
The implemented cut admits this node for acyclic and positive-recursive components. Recursive atoms retain sparse inner-time terminal weights; scalar and temporal tries share one topology, overlay, preparation and Generic Join visitor. Same-stratum atom reads are delayed structurally, and checkpoint recovery preserves the next signed correction. Well-founded recursive components remain outside this admission boundary.
Profiled tries store arena-owned scalar identities on prefix edges rather than owned semantic values. Semantic construction and record-backed serving are explicit state variants; conversion drops integrated scalar tries. One generic trie, overlay, journal and Generic Join implementation serves both variants. The record variant interns keys through the transaction that prepares the component and resolves identities only when producing a semantic binding. Checkpoint encoding resolves keys into canonical semantic order; restore re-interns them through the prepared record suffix. Journal validation requires the state and journal variants to match before publication.
Antijoin
The right side retains exact support per join key; the left side retains exact
rows grouped by that key. A left delta is emitted unchanged only when the new
right support for its key is zero. A right transition 0 -> positive retracts
the complete post-left-delta bucket; positive -> 0 asserts it. Simultaneous
left/right changes are evaluated from the old traces plus the consolidated batch
so each output row is emitted once. Negative right support or positive-to-negative
overshoot at the settled lower-stratum boundary is an invariant failure.
The entire lower stratum reaches its staged fixed point before an upper-stratum antijoin observes its new trace. No lower or upper result is published until the whole transaction succeeds.
Inside a positive recursive SCC, negation is admitted only for a predicate in a sealed lower stratum. The antijoin retains the left side as an inner-iteration profile and the right side as integrated support by correlation key. Right corrections are valid only at inner iteration zero. The plan records and validates that the antijoin right input is a non-delayed sealed scan; recursive negation remains a well-founded fallback. Profiled left state and right support publish through one prepared journal. Checkpoints require one canonical state entry for every profiled antijoin and validate key shape, tuple width, positive support, ordering, and uniqueness before restoration.
Aggregates
An aggregate is keyed by its correlated outer/group columns and retains the
weighted multiset for each group. A changed result emits -1 for the old output
and +1 for the new output. Empty-group behavior and undefined values match the
full evaluator.
countsums multiplicities with checked integer arithmetic.sumuses the exact numeric domain and errors of the full value evaluator.averageretains exact sum and count and performs the same exact division as full evaluation.count-distinctretains per-value support and counts zero-to-positive values.minimumandmaximumretain an ordered support map so deletion reveals the next supported value.
Projection, grouping, numeric coercion, empty input and overflow are tested per aggregate kind before that kind is admitted. An unimplemented kind refuses the whole program.
Projection-free count inside a positive recursive SCC uses a compact temporal
representation. Each correlation key retains one sparse BigInt cardinality
profile and an index of complete outer bindings to sparse support profiles; it
does not retain the joined input rows a second time.
Cardinality prefixes must remain in 0..=usize::MAX; outer prefixes are
nonnegative checked i64 supports. Outer support is not Boolean: distinct
recursive derivations can contribute the same binding at different causal
iterations. Integrated evaluation, temporal profiles and checkpoints preserve
the same multiplicity, while the recursive scheduler applies relation-level
zero-crossing semantics.
The upstream join arrangement owns row identity. Before derivative authority is
delegated, exact integrated aggregate parity is reconstructed from the retained
aggregate-input operator, not from a duplicate row map in count.
Factorized aggregate admission preserves the full evaluator’s authored factor
partition. It does not lower independent factors into their Cartesian product
or into independently materialized Int counts: either expansion changes the
physical bound, and early projection of a factor cardinality can report an
overflow even when another factor is empty. A factorized aggregate circuit node
therefore owns one summary trace per independent factor and combines factor
cardinalities in BigInt before the single value-domain projection.
For a cardinality aggregate, every factor retains cardinality by outer key. For
a projected aggregate, the value factor additionally retains the fold support;
the other factors retain only cardinality. A touched outer key reads old and
prepared summaries, emits one old retraction and one new assertion, and stages
all factor patches in one journal. sum scales the value fold by the exact
product of other cardinalities. minimum, maximum, average, and
count-distinct use other factors only as a nonempty gate. Checkpoint order is
outer key, factor ordinal, then canonical value.
outer parameter trace ------------------------------+
|
factor 0 pipeline --> cardinality summary -----------+
factor 1 pipeline --> value/cardinality summary -----+--> exact factor fold
factor N pipeline --> cardinality summary -----------+ |
v
old/new aggregate delta
delayed recursive outer -----------+
+---- correlated count ---- output
sealed aggregate body -------------+ |
v
correlation key
|-- shared cardinality timeline
`-- full outer binding -> support timeline
The sealed body may be an ordered connected pipeline of predicates, filters and
computations when every filter and computation dependency is bound inside that
pipeline. Disconnected factors and dependencies available only from the outer
binding retain the generic aggregate lowering. The compiler emits the explicit
operator; evaluators do not infer it from a Distinct/join graph.
Sealed body scans carry the existing immutable sealed-relation metadata. Node time domain is derived transitively from the plan: filters, computations and projections preserve it, and a join is origin-only exactly when both inputs are origin-only. Origin-only joins use an ordinary signed arrangement without a per-row iteration map and reject nonzero inner time. Joins reachable from a delayed scan retain the nested-time representation. Checkpoints store the same logical iteration rows and reconstruct the physical layout from the committed plan; no independent layout flag is persisted.
The shared arrangement stores a unique join-key bucket inline and allocates a nested Z-set only when a second distinct tuple has the same key. Promotion, demotion and ordinary weight changes use one absolute-weight transition. This preserves signed multiplicity and deterministic iteration while avoiding one tree allocation per key in the common fully keyed body-join shape.
Profiled evaluation derives transient consumer counts from the immutable DAG. An operator delta is released after its last scheduled consumer unless integrated derivative authority requires it across frontiers. This applies the same plan liveness to scans, filters, computations and joins instead of keeping every frontier-local intermediate through session preparation.
Whole-program compilation likewise derives a typed flow plan from stratum scan
and recursive dependency metadata. Each relation is identified by module, name
and arity and records its last consuming stratum. One flow entry composes two
ownership classes: frontier-owned external tuple deltas and arena-owned derived
RecordId deltas. External rows are not interned into the append-only arena;
derived rows retain identity across component boundaries. Both sources resolve
as one logical input and are released together at the last consumer. Public
output is a separate signed record set and therefore does not extend flow
lifetime.
external InputBatch --------------------------+
frontier-owned Tuple Z-sets |
v
ProgramFlow[RelationId]
|
component record output --> derived RecordId --+
| |
+--> public record output +--> current component input
|
compiled last consumer --> release entry
A profiled evaluation session validates each stage against published state plus its transaction-local overlay. Only the consolidated session is validated against published state at commit. This permits a later feedback stage to cancel a row created earlier in the same transaction without treating the intermediate retraction as an underflow.
Compilation pipeline
CompiledRule[]
|
+--> range restriction and tier admission (already complete)
|
+--> signed dependency graph and stratification
|
+--> rule-local logical operators
|
+--> union support from all producers of each relation
|
+--> relation-boundary distinct
|
+--> stratum scheduling and feedback edges
|
+--> stable structural operator identities
v
CircuitPlan { inputs, strata, nodes, sinks, commitment }
The production compiler consumes the optimized logical plan plus stratification.
It preserves fused recursion, worst-case-optimal joins, CSR access and
factorized operators as coarse incremental operators when expanding them into
binary nodes would discard their physical advantage. A direct CompiledRule
lowering is permitted as a Phase-A bootstrap and oracle surface; it is not the
final runtime seam. The coarse physical plan is not sufficient by itself when
it hides antijoins, aggregates or feedback edges.
Compilation first applies the same rule preparation as full evaluation. Values
stored in plans are dictionary-independent; instance-local dense IDs are resolved
when an instance is seeded. Inline-set and other module-static relations become
explicit immutable input relations. Every CompiledAtom variant is either mapped
to a circuit operator with identical expression semantics or produces a typed,
whole-program refusal. No atom, rule or producer is omitted. The compiler verifies
relation arity, variable binding, stratum order, positive feedback and that every
relation producer reaches exactly one relation-boundary distinct node.
Stateful join
old A arrangement old B arrangement
^ ^
| |
new ΔA -- staged index --+---- probe B_old ------+----+
\ \ |
+------------------ join new ΔB ---------------+--> Δ(A join B)
new ΔB -- staged index --+---- probe A_old ------+----+
The batch result contains all three bilinear terms. Both arrangements update only after probes observe the pre-batch state, then commit atomically with the operator output.
Nested-time join trace
Recursive joins retain inner iteration because nested time uses
max(current_iteration, retained_iteration). Equal consolidated relations with
different inner profiles are not interchangeable. Prior-frontier state must not
be retimed to iteration zero.
canonical iteration profile
|
| one prepared assignment
v
temporal arrangement: join key -> iteration -> matching tuples
^
|
correction tuple -- project key once -- probe matching timeline
|
v
emit at max(correction iteration, retained iteration)
The iteration profile is semantic state. The temporal arrangement is its owned, derived index: it is updated through the same prepared assignment and rebuilt from the profile during checkpoint restore. A legacy checkpoint projection may remain encoded for format compatibility, but restore validates it against the rebuilt index and never adopts it as authority. The index is not independently published. The physical representation is key-first, not one independent arrangement per iteration. An absent join key therefore costs one ordered-map probe rather than one probe per retained iteration; present keys visit only matching time buckets and emitted matches.
Distinct support transition
old weight delta new weight emitted set delta
--------- ----- ---------- -----------------
0 +n > 0 +1
>0 -n 0 -1
>0 +/- > 0 0
0 0 0 0
0 -n < 0 invariant failure
>0 -n < 0 invariant failure
Negative transient weights are legal inside differential operators before a
complete batch is consolidated. A relation-boundary distinct state has the
invariant old_weight >= 0; its consolidated new_weight must also be
non-negative. It emits only 0 -> positive and positive -> 0 crossings. A
published set-valued Argon relation therefore contains weights only in {0, 1}.
Atomic application
One mutation commit is one circuit batch. The instance stages every operator update, checks weight arithmetic and convergence, computes derived deltas, and only then publishes the new state and frontier. Failure leaves the prior state and frontier observable.
Storage first appends the authoritative event batch atomically. Circuit
maintenance then advances the read model from prior_frontier to
next_frontier. Until publication, readers continue to see the complete prior
frontier; they never combine durable base state at the new frontier with derived
state at the old frontier. A caller requiring read-your-commit waits for circuit
publication or receives an unavailable/maintenance-failed result. Event-log reads
may expose the durable append independently, but are not derived-model reads.
Publication is a compare-and-publish under the instance registry: the current instance ID, plan ID and frontier must equal those used to stage the batch. State, arrangements, output deltas and frontier replace the old snapshot together.
durable mutation batch
|
v
validate plan commitment and frontier
|
v
stage affected-node delta journals
|
v
propagate signed deltas in stratum order
|
v
check arithmetic, convergence, output invariants
|
+----+----+
| success | failure
v v
publish discard staged state
state + retain old frontier
frontier poison if rollback is not provable
Readers address published frontiers only. No reader can observe a base batch whose derived batch is not published at the same frontier.
Typed input refusal, checked overflow and convergence exhaustion occur entirely in staged state: they retain a reusable prior instance, mark the durable frontier as pending, and require retry or rebuild before later batches can pass. An internal invariant failure, corrupt committed state, or failure after mutation of shared state poisons the instance. A poisoned instance accepts no batch. Recovery restores a compatible checkpoint or rebuilds from the event log, then replays the failed batch and suffix in order. Later frontiers cannot skip it.
Recursion
Positive recursive components use nested time: outer transaction time and inner fixpoint-iteration time.
transaction delta
|
v
external SCC inputs ----> iteration 0 delta
|
v
recursive body circuit
|
v
relation-boundary distinct
|
+----------+----------+
| nonempty | empty
v v
feedback iteration publish SCC delta
The compiler admits this path only when recursive dependencies are positive. Recursion through negation remains on the well-founded batch evaluator until an incremental alternating-fixpoint design has its own correctness argument.
Within an SCC, timestamps use the product order over
(transaction_frontier, iteration). Storage may sort timestamps
lexicographically, but that storage order is not semantic time. A correction at
outer frontier t joins retained inner iterations at
(t, max(correction_iteration, retained_iteration)). Each iteration consumes
the prior iteration’s consolidated new support, applies every recursive
producer, unions support at the relation boundary and feeds only support
crossings back. The SCC settles when every feedback batch is empty. Iteration
count is bounded by the configured convergence policy and failure remains
staged.
This construction admits signed batches reaching a positive recursive SCC. Negative tuples are not replayed through an ordinary insertion loop. The body circuit retains nested-time arrangements, and a causal distinct session compares the corrected candidate profile with the prior candidate and output profiles at each sealed iteration. It therefore removes unfounded cyclic support while retaining independent or later alternative support. Cycles, diamonds, last support, alternative support, retract/reassert, mutual recursion and generated mutation traces are differential gates against fresh full evaluation.
The recursive operator follows the DBSP fixed-point construction itself; it is
not an ordinary feedback loop around the derivative of distinct:
outer signed input
|
v
inner delta-zero injection -----> (+) <---- checked inner delay
| ^
v |
inner integration |
| |
v |
lifted rule body |
| |
v |
distinct |
| |
v |
inner differentiation ------+
|
v
inner limit extraction
|
v
signed recursive output
The whole nested operator is incrementalized across the outer transaction
stream. Its inner integration and differentiation are semantic operators and
must be present in the circuit IR and retained state. Applying only a
distinct suffix correction and feeding it through delay is not equivalent:
for p(x) :- seed(x); p(x) :- p(x), deleting seed(x) makes such a loop move a
spurious self-support to successively later iterations forever. Inner
integration makes the delayed retraction visible to the lifted body snapshot;
inner differentiation then emits only the change between adjacent snapshots,
eliminating circular support.
The body evaluator reads retained per-iteration profiles, so a correction at
iteration i joins a retained row at j at max(i, j). It preserves transient
inner profiles whose outer-integrated weight is zero because those transients
can still change later recursive iterations. The extracted limit, not an empty
ad-hoc correction queue, defines completion.
The integrated inner stream is authoritative for relation-boundary support; its distinct-and-differentiated stream is authoritative for recursive changes. Delayed body inputs, arrangements and encoded catalogs are owned indexes or projections and must accept removals. A signed transaction cannot publish the nested stream while leaving any projection at the prior membership. One prepared token owns all assignments. The production signed route is admitted only for circuit-selected programs; the established evaluator remains the independent fallback and differential oracle. DRed with counting remains a correct alternative backend, but it is not substituted inside this DBSP circuit.
Persistence and recovery
projection checkpoint envelope
|-- tenant + fork + module commitment
|-- physical ProgramCircuitPlan commitment + circuit schema version
|-- derivation semantic epoch + execution configuration
|-- durable generation + exact event-prefix commitment
|-- independent circuit frontier + last published batch commitment
|-- authoritative union catalog + sparse rule-head base provenance
`-- ordered component states
|-- acyclic derivative state; delegated inputs and sinks omitted
`-- recursive scheduler + profiles; evaluator projections omitted
|
v
decode off-path -> validate complete envelope -> replay suffix -> audit
|
v
atomic projection-snapshot adoption -> serve
Circuit state is replaceable. The append-only event log remains authoritative. An incompatible or corrupt checkpoint is discarded and rebuilt; it is never partially adopted.
Checkpoint checksums detect accidental corruption; they are not authentication tags. Restore trusts the configured durable store as the checkpoint source. Tenant/fork scope, module and plan commitments, durable-prefix identity and retained-state invariants prevent accidental cross-context adoption, but an attacker able to replace trusted checkpoint bytes is outside this cache threat model and must be handled by storage integrity and access control.
The acyclic projection codec implements this boundary in the reasoning layer.
It binds tenant, fork, module, physical plan, derivation epoch, exact durable
prefix, circuit frontier, last batch and complete projection commit in one
canonical checksummed envelope. The union catalog and sparse rule-head base
provenance are encoded once. Embedded circuits carry explicit input, output and
derivative authority markers; delegated inputs and sinks are absent. Restore
constructs the circuit off-path, validates both directions of catalog/circuit
membership, and only then constructs a replacement projection. Integrated and
profile-only embedded circuit codecs both preserve the next mutation. Recursive
component checkpoints retain tuple-major candidate profiles with exact inner
iteration multiplicities, and restore the nested profile circuit without
serialized encoded catalog or arrangement projections. Standalone components
reconstruct evaluator base support from their enclosing base catalog. They do
not retain an encoded catalog copy: catalog views encode nonrecursive base
support on demand and read recursive membership from the scheduler. Evaluator
projection ownership is a sum type. Its internal variant contains base support
and arrangements; its external variant contains neither, so authority and
payload cannot disagree. Maintainer-owned restore constructs the external
variant directly instead of constructing internal projections and immediately
discarding them. The enclosing projection owns published membership and the
nested profiled circuit owns correction support. A restored component produces
the same next signed correction while its nested circuit remains at local
frontier zero.
All nested checkpoint layers use one shared framing encoder. It reserves the
20-byte magic/version/length header, writes canonical CBOR directly into the
final buffer, backfills the body length and appends one checksum. Program,
recursive-component, recursive-scheduler and circuit envelopes therefore no
longer construct a complete body and copy it into a second complete buffer.
The resulting bytes, versions and checksums are identical to the former
two-buffer encoding. Nested checkpoint payloads remain separately materialized;
removing that wire-level byte-vector nesting requires an explicit versioned
migration.
Whole-program checkpoints bind an ordered plan-derived component identity for
every acyclic and recursive stratum, retain program frontier/publication/config
once in the enclosing projection, and assign a fresh process instance on
restore so prepared journals from before recovery are invalid. Mixed programs
round-trip canonically, preserve duplicate retry identity, and produce the same
recursive retraction and upper-only mutation after restoration. Runtime durable
adoption exports and restores these envelopes only through the QueryEngine
facade; the runtime never names circuit plans or concrete maintainers.
durable manifest root
|-- ordered immutable event segments
`-- exact append-batch lengths
|
v
coherent snapshot + scope/order/content/count prefix commitment
|
+-- checkpoint prefix --> restore circuit off-path
|
`-- later append batches --> replay one ProjectionCommit each
|
v
validate final storage generation
|
v
replace ModelCache under one lock
The file-backed durable store records each successful append length beside the ordered segment list in the same atomic manifest. Recovery refuses suffix acceleration for legacy manifests that cannot prove those boundaries; it never guesses transaction grouping. A checkpoint is recovery-eligible only when its canonical event-prefix digest matches the durable log and the sealing store’s event bodies and next event sequence match that same prefix. Local-only warm segments may still accelerate the same live store, but cannot be adopted during durable recovery.
A persisted segment contains exactly one model representation. Circuit routes store the enclosing incremental projection envelope and leave the legacy columnar field empty; established routes store only the columnar model. Warm startup and crash recovery both restore the same circuit envelope and derive the read-only columnar index from its validated catalog. Transitional segments that contain both remain readable, but new writers never create dual payload authority.
Tip recovery restores the hot maintainer directly. Behind-tip recovery builds a private scoped store from the checkpoint prefix, restores there, replays each preserved append batch sequentially, and transfers the completed model cache only after its final storage generation equals the fully hydrated serving store. Any refusal leaves the serving cache cold, so the established full evaluation path remains the correctness fallback. The restored cache remains incrementally mutable; the first post-recovery mutation does not force a full evaluation.
The persistence unit is the enclosing projection snapshot, not an isolated
CircuitInstance. Production components delegate input, output and evaluator
projection authority; component bytes are incomplete without the union catalog
and sparse direct-fact provenance that own those projections. Persisting a
complete base catalog or a second derived catalog would create dual authority.
The envelope therefore stores the union catalog once, stores direct facts only
on produced relations, and stores derivative state in delegated components.
Restore validates every produced tuple against sparse base provenance unioned
with component-owned derived support.
Checkpoint encoding is canonical, resource-bounded and content-committed. It includes relation schemas, operator-state versions, per-iteration recursive candidate profiles, bilateral arrangements, scheduler support and the last published program batch. Restore reconstructs physical indexes from the live committed plan, validates component ordinal and kind, consolidates every recursive profile, reconstructs catalog membership, and rejects extra, missing, unordered, zero-weight or shape-incompatible entries. Profiles are not reconstructed from integrated state because integration discards inner time.
Circuit frontier and durable event watermark are independent: initial seeding, no-op commits and conservative recursive rebuilds do not establish a fixed arithmetic mapping. Recovery binds both values explicitly. An event sequence number and count prove freshness but not prefix identity, so adoption requires an append-only durable-log prefix commitment. A checkpoint is written to a temporary object, verified, and made visible atomically. Restore builds and validates a new snapshot off-path, assigns a fresh process instance identity, replays the ordered suffix, and swaps only the complete snapshot. Prepared journals are never persisted or reusable across restart. The differential audit is mandatory in tests and debug recovery; production may use configured sampling, but always checks encoding, commitments and operator invariants.
Fallback, recovery and module replacement
compiled program
|
+-- admitted --> build/restore circuit --> replay suffix --> publish
|
+-- typed refusal -----------------------> full evaluator
live circuit -- staged batch failure --> retain old frontier --> retry/rebuild
|
+-- invariant failure --> poison --> checkpoint restore
\-> full event-log rebuild
new module commitment --> compile + seed/replay new instance
|
compare old registry key
|
atomic registry swap
|
old instance drains/discards
A module commitment change stops admission of new batches to the old instance. The runtime compiles the new plan, seeds or replays it through a chosen event-log frontier, verifies it against full evaluation, and atomically swaps the registry entry only if the scope and expected old registry key still match. Batches that arrive during construction remain ordered in the log and replay before or after the swap. The old instance may serve its published frontier until replacement; it never processes a batch under the new commitment.
Delivery program
Phase A: strict-stratified circuit
|
+--> measured go/no-go against full evaluation and DRedc
|
v
Phase B: evidence-for/evidence-against pair circuits (assert-only)
|
v
Phase C: pair retraction after formal provenance gate
|
v
Phase D: proof-gated coupled well-founded circuits
|
v
Phase E: checkpoint, recovery and production scale
Phase A — circuit compiler and strict-stratified parity
Phase A is independently useful and replaces no fallback until its oracle and benchmark gates pass. Its internal order is:
Runtime circuit selection is off by default during Phase A and requires the
OXC_ENABLE_INCREMENTAL_CIRCUITS operational flag. An unsupported program,
catalog representation or disabled flag selects the established whole-program
maintainer before circuit state is created.
OXC_REQUIRE_INCREMENTAL_CIRCUITS is the validation mode: it enables circuit
selection and turns any catalog, preparation, compilation or restoration
fallback into a typed failure. Product-specific require flags select their
named fail-closed policy. The Established well-founded escape hatch can combine
with the ordinary require flag without permitting admission fallback.
The Linux compiler-test job runs every oxc-runtime test binary once with this
mode. The route-pinned and default Established runs each passed 945 tests with
three skipped. This includes mutation, recursive checkpoint, durable recovery,
ontology example-corpus and projection-cache integration coverage.
- Exact Z-sets, typed refusals, immutable plans and per-frontier differential equality with full evaluation.
- Positive acyclic scan, filter, map, compute, union, join, distinct and sink.
- Delta-local transactional state and signed arrangements. Work and memory on the mutation hot path must scale with the affected delta, not total retained state. Settled relation support may not become negative.
- Qualified schema-carrying
RelationId; structural collision-checkedNodeId; committedCircuitPlanIdand scopedCircuitInstanceId. - Explicit
(prior frontier, next frontier, batch commitment)application with duplicate idempotence and conflict, gap and stale-plan refusal. - Stratified antijoin with lower-stratum settlement, followed by count, sum, average, count-distinct, minimum and maximum.
- Positive recursive SCCs using the DBSP recursive derivative with outer transaction time and inner iteration time. Signed feedback is admitted only after cycle, diamond, alternative-support, last-support and generated mutation differentials.
ProjectionMaintainerimplementation exposed only throughQueryEngine. Durable append precedes maintenance; the per-scope visible watermark advances only after successful circuit publication. The full evaluator remains the permanent fallback and kill-switch target.
The Phase-A measurement compares full recomputation, the existing incremental
maintainer and the circuit on identical commit streams. It covers shallow
insertion, recursive insertion, low-overlap retraction, high-overlap retraction
waves, dense mutual-support cliques and a mixed recorded trace. Fixed-size
deltas are measured while retained state grows through 10^4, 10^5, 10^6
and 10^7 facts. Results include p50/p95/p99 mutation-to-visible latency, peak
and retained memory, arrangement probes, fixpoint rounds, affected cardinality
and emitted cardinality. Compilation, seeding, cloning and destruction are
reported separately.
Proceeding beyond Phase A requires both:
- exact catalog equality after every commit; and
- at least a fivefold win on high-overlap retraction at
10^6facts or above, while shallow insertion, recursive insertion and low-overlap retraction remain within 20 percent of the existing maintainer.
A high-overlap win below twofold parks Phases B through D. An intermediate result requires a recorded owner decision using the published measurements.
Targeted measurements on 2026-07-19 do not yet discharge the complete matrix gate. A ten-sample 100-fact high-overlap retraction over one million input facts measured circuit p50/p95/p99 latency of 143.459/167.083/167.083 microseconds, versus 623.479/631.566/631.566 milliseconds for the established maintainer. Exact retained-entry telemetry identified 1,000,000 typed input tuples duplicating the authoritative encoded catalog. Delegating base-input authority to that catalog reduced requested retained heap from 292,527,744 to 100,908,937 bytes, 33.9 percent below the established maintainer’s 152,749,040 bytes. Measured peak heap fell from 708,189,124 to 538,703,743 bytes, 12.4 percent above the established maintainer’s 479,310,928 bytes. The focused latency and retained memory requirements are exceeded; the remaining workloads, scales and variance measurements are still required by the Phase-A gate.
Observed runtime telemetry enabled an adjacent million-fact gate run on
2026-07-20 at revision 51932c581. With 100-fact deltas and 30 samples, circuit
versus established p50 was 0.505 versus 317.818 ms for shallow insertion, 0.509
versus 2,093.220 ms for low-overlap retraction, 0.660 versus 654.261 ms for wide
recursive insertion, and 0.250 versus 631.499 ms for high-overlap retraction.
The four speedups are 629, 4,114, 991 and 2,528 times. Observed circuit work was
respectively 100/0, 100/0, 0/1 and 0/0 arrangement-probe/recursive-round counts.
The focused latency gate passes. Peak heap remains 1.68–2.10 times established;
recursive insertion retains 1.68 times established while the other three
controls retain less. The complete 10^4–10^7, dense, mixed-trace and
cross-machine matrix remains open.
The evaluator’s last-consumer policy also covers Distinct. Zero-crossing
evaluation borrows its input; after validation, an exclusive input profile
moves into the distinct journal. Shared or retained profiles remain borrowed
and are cloned only because another consumer exists. This is the same ownership
contract used by union, join and sink, not a distinct-specific representation.
On the million-fact shallow control, construction peak fell from 2,509,624,433
to 2,394,523,289 bytes, 4.6 percent, with unchanged 486,716,234-byte retained
heap. Wide and dense recursive peaks were unchanged.
Record-backed join corrections are encoded into arena identities at the join boundary rather than retained as semantic tuples until state preparation. The join-delta type is parameterized by the owning profile representation, making a semantic journal invalid for record-backed state at compile time. Both representations use one orchestration function for input conversion and the nonlinear correction term; representation adapters own only retained-state probing and journal encoding. The resulting single semantic kernel preserves the exact three-term bilinear delta law without maintaining two evaluators.
Thirty-sample million-fact controls with 100-fact deltas reduced shallow construction peak from 2,394,523,289 to 2,385,809,537 bytes and wide-recursive construction peak from 1,962,000,198 to 1,910,669,498 bytes. Retained heap was 486,716,042 and 425,172,351 bytes respectively. Observed transaction work remained 100 probes and zero rounds for shallow insertion, and zero probes and one round for wide recursive insertion. The shallow peak now occurs during join-output construction, so further reduction belongs inside the join input and output lifetime rather than state-journal conversion.
The nonlinear correction join uses a sorted borrowed arrangement over its authoritative correction Z-set. A contiguous vector stores tuple references and weights, compares projected fields in place and owns neither tuple payloads nor one materialized key per tuple. This preserves the single join visitor and removes both transient tuple duplication and per-key tree storage. On the million-fact shallow control, construction peak fell from 2,385,809,537 to 2,081,562,849 bytes, 12.75 percent, while retained heap remained 486,716,042 bytes. The origin-only million-fact wide-recursive path does not construct this index and remained at a 1,910,669,498-byte peak and 425,172,351-byte retained heap. Transaction work remained respectively 100/0 and 0/1 arrangement probes/recursive rounds.
Phase instrumentation placed the next construction peak after profile overlay
preparation, at record publication. The transaction and arena previously used
different digest-index representations, and every pending payload repeated its
digest. Both now use one compact RecordDigestIndex, with a first-ID tree and a
separate tree only for actual digest collisions. Publication transfers
disjoint index nodes, explicitly merges overlapping collision buckets and
moves digest-free payloads into stable record IDs. The million-fact shallow
construction peak fell from 2,081,562,849 to 1,988,233,345 bytes, 4.48 percent,
with unchanged 486,716,042-byte retained heap. The wide-recursive peak fell
from 1,910,669,498 to 1,817,345,146 bytes with unchanged 425,172,351-byte
retained heap. Observed probes and rounds were unchanged.
Two publication-index prototypes were rejected after measurement. A 256-way
digest-sharded binary-leveled B-tree left the shallow construction peak at
1,988,233,345 bytes and added 189,072 retained bytes: the peak is the required
coexistence of published and prepared indexes, not global merge workspace. A
second prototype froze the prepared index into a sorted (digest, record ID)
segment. It also left peak unchanged; direct sorted replay increased retained
heap by 17,001,864 bytes through sparse B-tree packing, while record-ID-order
replay restored retained heap but still did not change peak. Both prototypes
were removed. Further publication reduction requires a broader atomic ownership
protocol or persistent index, not another local container representation.
The retained arena therefore uses the persistent-index alternative. Its primary digest-to-record mapping is one sorted contiguous vector searched by binary search. A transaction independently uses a mutable ordered map. Atomic publication consumes that map, classifies pre-existing digests into the sparse collision table and merges new primary entries into the vector. Exact payload comparison remains the authority after every digest lookup; the index changes storage only and cannot alias distinct records.
On the 10,000-component recursive multiway control with a 100-row delta, this reduced retained heap from 15,846,195 to 14,980,023 bytes and mutation peak from 40,254,972 to 39,388,800 bytes. Construction peak and every logical record, trace and trie count were unchanged. Against the 9,842,015-byte Established control, retained overhead fell from 1.61 to 1.52 times.
The cumulative representation changes also remove the dense-recursion construction blocker. A 100,000-fact dense mutual-support workload that had stopped after 612 seconds at 17.77 GiB RSS now completes with a 1,162,073,678-byte requested-allocation peak and 262,193,596-byte retained heap. Thirty 100-fact retraction samples measured 194.595 ms p50 and 254.383 ms p95, with 34,600 arrangement probes and five productive recursive rounds per operation. No dense speedup is inferred because the established control was not rerun after these circuit-only changes.
The end-to-end conformance replay builds every positive ontology through the driver, materializes its canonical EDB and compares established and circuit-preferred maintenance with fresh evaluation after retract, absent-retract, reassert and duplicate-assert frontiers. Seeded rows are used when an actual compiled rule input contains one; otherwise the harness creates a deterministic tuple from that predicate’s constants and repeated-variable shape. Empty relation presence is normalized while signed rows remain exact. The current corpus exercises 29 eligible ontologies. Twenty-eight mutation replays comprise three seeded-input and 25 synthetic-input cases; one rule-free package has no input to mutate. All 29 packages select a circuit route: 27 acyclic and two recursive. The gate pins the two recursive package paths and fails any eligible package that regresses to fallback, so semantic equality cannot pass by silently leaving the circuit. All replayed frontiers agree with fresh evaluation under both maintenance modes.
The expanded matrix exposes a separate recursive retained-state blocker. At 100,000 facts, recursive insertion retained 1,051,926,002 bytes after base-input delegation, versus 24,601,021 bytes for the established maintainer. Exact entry counts were: 200,000 encoded read-model tuples; 200,000 integrated operator rows; 200,000 integrated join-arrangement entries; 100,000 integrated sinks; 400,000 temporal-profile rows; 400,004 candidate-trace entries; 200,004 output- trace entries; 100,000 candidate-support tuples; 100,000 settled tuples; 200,000 evaluator-encoded tuples; and 200,000 evaluator-arrangement entries. The recursive circuit’s duplicated integrated and temporal join states, trace history/current profiles and evaluator projections require an ownership redesign before production routing.
The join shape is now immutable circuit-plan metadata and participates in plan identity. This removed the prior empty-baseline and repeated-positive-mutation shape ambiguity. Maintainer-owned recursive components consequently use temporal profiles as their sole derivative authority; integrated operators, ordinary join arrangements and sinks are absent by construction. Profiled evaluation also stops retaining operator profiles already represented by temporal join inputs. Standalone circuits retain integrated state and checkpoint behavior.
A ten-sample 100-fact insertion over 100,000 input facts measured 278,859,701 retained bytes and 626,956,372 peak bytes after these changes. The recursive scheduler now retains cumulative inner-iteration profiles directly instead of duplicating them with per-frontier historical traces; durable outer history belongs to event replay. Before the ownership change the same scale retained 1,051,926,002 bytes. Exact circuit counts fell to zero integrated operator rows, arrangements and sinks, and 200,000 temporal- profile rows; candidate trace entries are bounded at 200,000 and the persistent output timeline is absent; maintainer-owned evaluator encoded, evaluator arrangement, and candidate-support entries are zero. Recursive membership is projected from cached support in the candidate profiles; there is no separate settled index. The measured circuit p50 was 44.195 ms versus 59.605 ms and 24,601,021 retained bytes for the established maintainer. This is a substantial structural reduction, not a production gate win: the remaining temporal profile, candidate history, settled membership, and published relation overlap still retains 11.3 times the established heap. This insertion sample is 1.35 times faster, but temporal trace ownership and compaction remain prerequisites for routing.
Symbolicated sampling identified avoidable transient work rather than an
inherent incremental cost. Profile staging cloned accumulated input and sink
maps on every recursive round, while causal distinct cloned and replaced its
complete active map at every iteration. Per-profile prepared journals and a
globally validated per-entry distinct seal preserve failure atomicity without
either copy. At 10,000 retained facts and the same 100-fact delta, p50 fell from
75.293 to 44.799 milliseconds; at 100,000 facts it fell from 75.324 to 45.846
milliseconds. The nearly flat retained-state scaling remains, with 39–40
percent less mutation latency. Candidate-profile patch preparation now also
consolidates every logical (tuple, iteration) cell before producing absolute
assignments, so multiple changes cannot overwrite rather than compose.
Durable candidate history is tuple-major: each tuple owns a sorted, zero-pruned
sparse iteration profile. The logical trace remains the same signed
(tuple, iteration, weight) relation, while causal activation reads only the
touched tuple’s events. Transaction staging stays iteration-major and prepares
one checked assignment per consolidated logical cell. An activated tuple caches
its immutable sparse history once, avoiding a retained-map lookup on each later
round. At 100,000 facts this reduced retained heap by 3.2 percent and peak heap
by 6.2 percent without regressing the profile-guided latency gain.
Sealed lower-stratum negation is now incremental inside positive recursive
SCCs. A branched-chain workload asserts 100 lower ban facts and changes
exactly 1,500 derived tuples. At 10,000 edges the circuit measured 11.097 ms p50
versus 46.992 ms established, a 4.23-times speedup. At 100,000 edges it measured
11.179 ms versus 521.101 ms, a 46.6-times speedup. Retained heap was 17.1 and
16.7 times established at the two scales. The semantic and latency results are
favorable; the memory result prevents default routing.
Projection-free recursive count is a dedicated fused operator. It consumes
the recursive outer and independently scanned body without constructing the
parameter-domain distinct or outer-by-body join. At 10,000 lower-stratum rows,
a one-row mutation of one 10,000-row correlated group measured 0.024 ms p50
versus 5.167 ms established, a 219-times speedup. Changing 100 groups of 100
rows measured 2.460 ms versus 410.961 ms, a 167-times speedup. Retained heap was
3,520,778 and 3,982,413 bytes respectively, 2.23 and 2.49 times established.
The profiled state contained three cells for the single-group case and 300 for
the 100-group case, rather than 10,000 expanded joined rows.
Independent aggregate factors retain one sparse summary per factor rather than their Cartesian product. With 10,000 input facts split into two ten-row factors per group, retracting one row from each of 100 groups measured 1.041 ms p50 for the circuit versus 1.162 seconds established, a 1,116-times speedup over five samples. Retained heap was 2,008,488 bytes versus 1,693,936 bytes established, or 1.19 times; mutation peak was lower at 2,910,804 bytes versus 4,341,282 bytes. The mutation changed 200 observable aggregate tuples and performed 100 keyed arrangement probes.
The same fused operator accepts a connected body pipeline containing a predicate, filter, computation and second predicate. For 100 correlated groups, 10,000 rows in each of the two body relations and a 200-row mutation across those relations, 30 samples measured 2.961/3.052/3.091 ms p50/p95/p99 versus 395.477/399.538/401.162 ms established, a 134-times p50 speedup. Origin-only join storage and inline singleton arrangement buckets reduced circuit retained heap from 28,855,027 to 17,949,079 bytes in the first ten-sample run and 17,964,387 bytes in the 30-sample run, a 37.7 percent reduction. Replacing complete base, derived and union catalogs with one union catalog plus sparse rule-head base provenance reduced a later ten-sample run from 17,964,387 to 16,376,752 bytes, another 8.8 percent; this is 5.18 times the established 3,162,697 bytes. Releasing frontier-local deltas after their last DAG consumer reduced construction peak from 68,533,677 to 51,523,245 bytes, 24.8 percent. This remains 7.77 times the established 6,634,768 bytes. Mutation peak is 18,270,222 bytes versus 8,244,838 established, or 2.22 times, down 8.0 percent from 19,861,793 bytes. Construction is the larger transient blocker. The 20,300 retained logical rows show that exact opposite-side join support, rather than timestamp or nested-bucket overhead, is now the dominant retained cost. This workload remains ineligible for default routing until that ownership overlaps less with the published lower-stratum catalog.
The canonical RecordId implementation was subsequently measured with exact
arena cardinalities after replacing retained canonical bytes and shared payload
allocations with collision-checked digest buckets and boxed decoded payloads.
At 10,000 rows with a 100-row wide-recursion mutation, 30 samples measured
0.992/1.223/1.311 ms p50/p95/p99, 19,243,524 retained bytes and 19,866,221
mutation-peak bytes. The arena retained 20,300 value records and no binding
records. The connected count pipeline mutates both body relations, so the same
requested delta produces 200 changed rows; it measured 3.325/3.482/3.673 ms,
17,492,400 retained bytes and 19,488,181 mutation-peak bytes. Its arena retained
20,800 records: 20,400 values and 400 bindings. The compact index removed about
1.4 MB from the pipeline result, but the remaining one-use value records still
overlap the encoded published catalog. This memory result blocks default routing
and requires a catalog/read-view ownership cut; binding representation is not
the dominant cost.
A targeted ten-sample comparison against the actual full-recompute maintainer, not the matrix performance gate, used the same 10,000-row, 100-row mutation. Wide recursion measured 0.911 ms circuit p50 versus 16.436 ms full recompute; retained heap was 19,243,524 versus 2,418,708 bytes, and construction peak was 59,436,189 versus 13,499,191 bytes. The connected count pipeline measured about 3.325 ms circuit p50 versus 430.119 ms full recompute; retained heap was 17,492,400 versus 3,160,138 bytes, and mutation peak was 19,488,181 versus 8,242,279 bytes. This targeted result demonstrates roughly 18-times and 129-times mutation speedups respectively, while confirming 7.96-times and 5.53-times retained-memory regressions. It does not satisfy the default-routing memory gate.
The subsequent ownership cut removed the persistent encoded catalog from
program circuits. Published union membership and sparse rule-head base
provenance are sets of RecordId; only prepared sink deltas retain signed
weights. Catalog and columnar forms are boundary projections, and columnar
construction sorts semantic rows independently of record allocation order.
Direct point lookup resolves a tuple to its existing record identity without
scanning or interning. Initial construction and restore use validated seed
transactions in the program arena; mutation membership uses the same prepared
transaction as the affected operator state.
On the combined direct-restore and ownership-cut implementation, the same 30-sample wide workload measured 0.884/0.993/1.001 ms p50/p95/p99, 17,865,525 retained bytes and 19,769,990 mutation-peak bytes. The same count pipeline measured 3.271/3.419/3.722 ms, 16,142,663 retained bytes and 18,136,684 mutation-peak bytes. Relative to the compact-record implementation, retained heap fell 7.2 percent for wide recursion and 7.7 percent for the count pipeline. The pipeline still retains 5.11 times the full-recompute heap and 2.20 times its mutation peak. Construction peaks remain 59,436,189 and 51,523,629 bytes. The duplicate catalog is no longer the retained-memory blocker; temporal arrangements, candidate profiles and arena indexing now dominate. Default routing remains disabled pending the complete matrix gate and further retained-state reduction.
A 2026-07-21 breadth run fixed state at 10,000 rows, delta at 100 rows and five samples for every Phase-A workload. It validated every transition before measurement. Circuit versus Established p50 latency was:
| Workload | Circuit (ms) | Established (ms) | Ratio |
|---|---|---|---|
| shallow insertion | 0.588 | 2.646 | 4.50x faster |
| wide recursive insertion | 0.672 | 5.306 | 7.89x faster |
| well-founded exit assertion | 6.229 | 47.083 | 7.56x faster |
| deep-chain recursive insertion | 21.046 | 9.846 | 2.14x slower |
| recursive multiway retraction | 5.036 | 73.008 | 14.50x faster |
| upper recursive retraction | 0.610 | 10.610 | 17.39x faster |
| lower negation assertion | 7.756 | 45.971 | 5.93x faster |
| lower count assertion | 2.148 | 401.311 | 186.83x faster |
| lower count pipeline assertion | 4.304 | 613.258 | 142.49x faster |
| factorized count retraction | 1.202 | 1,195.429 | 994.53x faster |
| low-overlap retraction | 0.586 | 18.302 | 31.24x faster |
| high-overlap retraction | 0.342 | 4.939 | 14.44x faster |
| projected sum retraction | 1.484 | 266.124 | 179.33x faster |
| dense mutual-support retraction | 115.963 | 397.955 | 3.43x faster |
| mixed recorded trace | 3.488 | 20.537 | 5.89x faster |
Deep-chain insertion violates the 20-percent non-regression requirement. Retained memory also remains excessive for recursive multiway state at 73.06 MB versus 9.84 MB and dense mutual support at 26.97 MB versus 6.02 MB. This run is a breadth diagnostic, not the Phase-A gate: it lacks the required larger scales, 30-sample variance and full recomputation leg. The next gate work targets the deep-chain scheduler and recursive multiway/trie ownership before scaling the matrix.
A 1 kHz sample of 30 deep-chain mutations attributed hot-path work to record lookup, trace-key traversal, B-tree insertion and per-probe timeline materialization. Record-native retained joins now consume an inline sparse timeline directly from the trace visitor; the common one-time, one-tuple probe allocates no timeline map or Z-set. On matched 20-sample runs, circuit p50 fell to 20.470 ms while Established measured 9.756 ms. The 2.10-times regression is smaller but remains outside the gate; record conversion and per-round profile publication remain the next targets.
Trace key visitation now bypasses the general level-merging cursor when a trace has exactly one immutable consolidated batch. Record point lookup hashes a borrowed value slice and compares that slice through the existing digest index; it no longer clones a tuple into a temporary boxed payload. The canonical CBOR encoder accepts a value slice, so this path retains one encoding and identity authority. On 50 deep-chain samples, circuit p50 fell to 18.490 ms with unchanged retained and peak memory, but remains 1.90 times the matched 9.749 ms Established result. Recursive multiway measured 4.669 ms and dense mutual support measured 76.125 ms after the same change; neither regressed relative to their preceding 4.910 ms and 82.568 ms circuit measurements.
An empty transactional Z-set view now validates and bulk-builds its ordered absolute assignments instead of point-inserting every changed row. Later stages retain the point-update path because they must compose against prior staged assignments. The bulk path leaves the view unchanged if any row overflows. On matched workloads, deep-chain p50 fell again to 17.634 ms, recursive multiway to 4.540 ms and dense mutual support to 63.985 ms. Memory and observed work cardinalities were unchanged. Deep-chain remains 1.81 times slower than Established; multiway is 14.99 times faster and dense mutual support is 5.24 times faster.
A post-architecture breadth rerun at 10,000 rows, 100-row deltas and five samples measured 0.524 ms shallow insertion, 0.517 ms wide recursion, 6.386 ms well-founded exit assertion, 4.629 ms recursive multiway retraction, 62.616 ms dense mutual-support retraction and 1.894 ms for the mixed recorded trace. Each matched or improved its preceding circuit result. A separate 20-sample deep-chain run measured 17.126 ms circuit versus 9.725 ms Established, a 1.76-times regression. It executes 100 recursive rounds, 4,950 arrangement probes and emits 5,050 tuples. Borrowed record interning was tested and rejected because matched measurements showed no reliable improvement; no additional record representation was retained. Deep-chain round overhead remains the sole latency non-regression failure at this control scale.
A 2026-07-22 current-build rerun used 10,000 retained rows, a 100-row delta and 30 samples. Deep-chain insertion measured 14.456/16.526/16.549 ms circuit p50/p95/p99 versus 10.698/11.234/11.249 ms Established. The circuit remains 35.1 percent slower at p50 and therefore still fails the 20-percent non-regression gate. It executed 100 recursive rounds and 10,200 observed arrangement probes. Circuit retained heap was 3,137,463 bytes versus 2,420,557 bytes Established (1.30 times); construction and mutation peaks were 0.89 and 0.79 times Established respectively.
The matched recursive multiway retraction measured 4.868/5.208/5.420 ms circuit versus 68.394/73.427/74.399 ms Established, a 14.0-times p50 speedup. Circuit retained heap was 19,275,571 bytes versus 9,842,015 bytes (1.96 times), construction peak was 48,134,420 versus 38,067,003 bytes (1.26 times), and mutation peak was 43,684,348 versus 28,024,369 bytes (1.56 times). The latency gate passes; retained and mutation memory remain replacement blockers.
Recursive semantic staging previously encoded each accepted tuple once for duplicate detection and again for journal insertion. The read view now accepts the already validated canonical encoding, retaining one encoded assignment authority. On the same deep-chain configuration and 30 samples, circuit p50/p95 fell from 14.456/16.526 ms to 11.483/11.864 ms. Established measured 9.563/11.515 ms. The circuit p50 is 20.08 percent slower: a 20.6 percent improvement over the preceding circuit result, but still narrowly outside the 20-percent gate. Retained, construction-peak and mutation-peak memory were unchanged.
Staged duplicate detection and journal insertion then became one ordered-map entry operation instead of a membership probe followed by insertion. Two independent 30-sample runs measured circuit p50 at 11.458 and 11.523 ms versus 9.709 and 9.678 ms Established. The circuit was respectively 18.0 and 19.1 percent slower, passing the 20-percent control-scale non-regression gate in both runs. P95 was 11.818 and 11.766 ms. Logical work, retained state and all heap measurements were unchanged.
Unary trie paths then stopped caching live_keys; the value is exactly the
path terminal’s liveness plus its sole child’s count. This removes a derived
field whose equality previously depended on every promotion, demotion and
publication path updating it consistently. On the 10,000-component recursive
multiway workload, retained heap fell from 19,275,571 to 18,715,571 bytes and
mutation peak fell from 43,684,348 to 43,124,348 bytes. Construction peak was
unchanged. The 30-sample circuit p50 was 4.959 ms versus 81.809 ms Established;
the circuit retained-memory ratio improved from 1.96 to 1.90 times.
Unary prefixes with no terminal tuple then received a distinct compact node inside the same generic trie. Terminal absence is structural; these nodes own only their key and child rather than an always-empty temporal weight. Prefixes that are also terminals retain the weighted path representation, and promotion, demotion, overlays and checkpoint entries remain representation-independent. On the same 30-sample workload, circuit retained heap fell from 18,715,571 to 17,035,571 bytes and mutation peak from 43,124,348 to 41,444,348 bytes. Construction peak was unchanged. Circuit p50 improved from 4.959 to 4.692 ms versus 65.007 ms Established; the retained-memory ratio improved from 1.90 to 1.73 times.
Canonical value records then stored compact one- and two-cell tuples inline. These frequent records no longer require a separately allocated cell slice; wider compact tuples and uncommon semantic values retain their existing lossless representations. On the same 30-sample workload, circuit retained heap fell from 17,035,571 to 15,844,179 bytes, construction peak fell from 48,134,420 to 46,943,028 bytes and mutation peak fell from 41,444,348 to 40,252,956 bytes. Circuit p50 was 4.716 ms versus 63.254 ms Established. The retained-memory ratio improved from 1.73 to 1.61 times; construction and mutation peaks were respectively 1.23 and 1.44 times Established.
At 100,000 components with the same 100-row delta and 30 samples, the inline record representation measured 43.009/44.045/44.271 ms circuit p50/p95/p99 versus 686.979/699.287/724.369 ms Established. Circuit retained heap was 149,834,083 bytes versus 101,715,851 bytes (1.47 times), construction peak was 462,067,018 versus 380,667,267 bytes (1.21 times), and mutation peak was 400,249,974 versus 282,025,420 bytes (1.42 times). The circuit remained 16.0 times faster at p50 while the retained-memory ratio improved from the prior 1.83-times measurement at this scale.
The corpus-driven differential then built every eligible conformance package
and compared Established, circuit-preferred, Product-preferred and fresh
evaluation. All 31 packages retained circuit admission. Thirty packages
completed retract, repeated-retract, reassert and duplicate-assert replays with
exact catalog equality after every frontier; five used existing input rows and
25 used deterministic synthetic rows. The remaining package contained no rule
input to mutate. Both expected recursive packages selected RecursiveCircuit;
no eligible package fell back.
The final-head 100,000-row, 100-row-delta, 30-sample Phase-A control ran on
2026-07-24 at revision 81fc95d58. Each workload ran in a separate optimized
process. Every circuit selected its required route and validated the full
catalog before and after sampling.
| Workload | Circuit p50/p95 | Established p50/p95 | p50 speedup | Probes/rounds |
|---|---|---|---|---|
| shallow insertion | 0.392/0.648 ms | 28.806/30.718 ms | 73.5× | 100/0 |
| wide recursive insertion | 0.430/0.523 ms | 58.066/60.978 ms | 134.9× | 300/1 |
| low-overlap retraction | 0.385/0.537 ms | 206.494/210.381 ms | 536.6× | 100/0 |
| high-overlap retraction | 0.263/0.327 ms | 61.569/64.291 ms | 233.7× | 0/0 |
| Workload | Retained C/E (ratio) | Construction peak C/E (ratio) | Mutation peak C/E (ratio) |
|---|---|---|---|
| shallow insertion | 32.911/54.972 MB (0.599×) | 199.574/121.647 MB (1.641×) | 135.411/131.869 MB (1.027×) |
| wide recursive insertion | 26.775/24.601 MB (1.088×) | 88.494/114.787 MB (0.771×) | 95.086/119.249 MB (0.797×) |
| low-overlap retraction | 32.900/54.955 MB (0.599×) | 199.494/121.623 MB (1.640×) | 135.365/128.747 MB (1.051×) |
| high-overlap retraction | 8.537/15.120 MB (0.565×) | 97.927/48.190 MB (2.032×) | 37.845/49.010 MB (0.772×) |
The first three workloads affected and emitted exactly 100 derived tuples. High-overlap retraction affected 100 inputs and emitted no derived change. Observed work therefore tracks the changed frontier rather than total model size. This scale passes the Phase-A latency conditions; the retained recursive ratio is 1.088× and construction peaks remain above Established for the two acyclic controls and high-overlap construction. Reproduce one row with:
OXC_SAMPLED_WORKLOAD=shallow_insert OXC_SAMPLED_STATE=100000 \
OXC_SAMPLED_DELTA=100 OXC_SAMPLED_COUNT=30 \
cargo bench -p oxc-reasoning --bench incremental_sampled --features bench-support
The final-head one-million-row controls used separate processes per implementation to keep allocator reservation from overlapping between maintainers:
| Workload | Circuit p50 | Established p50 | Circuit retained | Established retained |
|---|---|---|---|---|
| shallow insertion | 0.363 ms | 320.874 ms | 311,902,826 B | 561,408,256 B |
| wide recursive insertion | 0.423 ms | 645.292 ms | 250,855,327 B | 253,069,789 B |
| low-overlap retraction | 0.364 ms | 2,090.161 ms | 311,890,546 B | 561,391,896 B |
| high-overlap retraction | 0.248 ms | 633.624 ms | 84,866,742 B | 152,749,744 B |
The circuit was respectively 883, 1,526, 5,738 and 2,558 times faster at p50. All four circuit retained heaps were at or below Established: the ratios were 0.556, 0.991, 0.556 and 0.556. Circuit mutation peak was 1.03 times Established for shallow and low-overlap maintenance, 0.81 times for recursive insertion and 0.80 times for high-overlap retraction. Construction peak was 1.63 times Established for shallow and low-overlap, 0.75 times for recursive insertion and 2.03 times for high-overlap. Mutation work remained independent of retained cardinality.
At ten million rows, the 30-sample high-overlap control measured 0.258 ms circuit p50 versus 6,793.497 ms Established, a 26,361-times speedup. Circuit retained heap was 851,881,566 bytes versus 1,552,374,336 bytes Established; mutation peak was 3,865,498,830 versus 5,120,219,008 bytes. Circuit construction peak was 10,162,097,863 bytes versus 5,035,068,150 bytes Established. The required large-scale high-overlap latency and retained-state result passes; construction remains a separate optimization target.
Every remaining circuit workload also completed 30 samples at 100,000 rows, selected its required route and validated the complete catalog transition. This covered factorized count, well-founded exit, deep recursion, text-key multiway recursion, upper- and lower-stratum changes, recursive count and count pipelines, projected sum and maximum, dense mutual support, and a mixed recorded trace. Three-sample Established controls were used only to detect regressions, not as release-grade variance evidence:
| Workload | Circuit p50 | Established p50 | Retained ratio |
|---|---|---|---|
| well-founded exit | 52.624 ms | 524.349 ms | 1.41 |
| deep recursive insertion | 11.470 ms | 59.028 ms | 1.09 |
| text-key multiway retraction | 48.512 ms | 1,086.944 ms | 1.98 |
| upper-stratum retraction | 0.314 ms | 114.613 ms | 0.84 |
| lower-stratum negation assertion | 4.173 ms | 496.313 ms | 1.52 |
| recursive count assertion | 1.818 ms | 3,816.232 ms | 0.55 |
| recursive count pipeline assertion | 2.201 ms | 3,946.810 ms | 0.85 |
| projected sum retraction | 1.248 ms | 2,911.354 ms | 0.71 |
| projected maximum retraction | 1.767 ms | 2,903.440 ms | 1.97 |
| mixed recorded trace | 1.351 ms | 171.176 ms | 0.84 |
The circuit therefore showed no latency blocker in this cross-shape pass. Retained memory is concentrated in text-key multiway state and the extrema index; those representations remain default-routing optimization targets. The factorized-count Established control exceeded three minutes before completing three samples, and dense recursion has no bounded matched Established result; neither incomplete control is reported as a comparison.
Extrema-tree nodes then stopped caching subtree length and support-cell count. Both values are exact structural folds used only by diagnostics and checkpoint capacity planning; balancing and semantic lookup do not consume them. Removing the duplicate counters makes their equality structural rather than dependent on every path-copy and rotation constructor. On the 100,000-row projected-maximum workload, retained heap fell from 31,182,127 to 29,582,127 bytes and mutation peak fell from 62,936,471 to 61,336,471 bytes. Construction peak remained 125,415,315 bytes. The 30-sample p50 was 1.857 ms versus 1.767 ms before the change; this single-run difference is not treated as a latency claim. The retained-memory ratio improved from 1.97 to 1.87 times Established.
The extrema tree then stopped retaining a winner profile at every internal node. Ordered winner queries now traverse the authoritative temporal support profiles directly; all winner times are the causal closure of support times. Negative or overflowing support remains a loud query error. Tree construction, path copying and rotation consequently contain no orientation-dependent semantic maintenance. On the same workload, retained heap fell again from 29,582,127 to 27,182,127 bytes and mutation peak from 61,336,471 to 58,936,471 bytes. Construction peak remained 125,415,315 bytes. The 30-sample p50 was 2.072 ms versus 1.857 ms with cached winners, an 11.6 percent cost retained in exchange for removing duplicated semantic state; the circuit remains more than 1,400 times faster than the three-sample Established control. The retained- memory ratio improved from 1.87 to 1.71 times Established.
All-text tuples then stopped owning duplicate String values. The record arena
already owns a canonical singleton record for each scalar used by trie edges;
wider text tuples now contain those ScalarId values. Singleton records remain
the sole string owners, tuple records and tries share their identity, and
record views resolve the reference through their published or transactional
arena context. Restore reconstructs the same ownership through ordinary record
interning, without a string pool or second checkpoint representation.
On the 100,000-component text-key multiway workload, retained heap fell from 307,479,837 to 185,691,947 bytes, construction peak from 640,413,315 to 518,625,425 bytes and mutation peak from 681,600,893 to 559,813,003 bytes. The final 30-sample p50 was 49.027 ms versus 48.512 ms before the change; the 1.1 percent difference is not treated as a latency regression. Relative to Established, the retained-memory ratio improved from 1.98 to 1.19 times, construction peak from 1.39 to 1.12 times and mutation peak from 1.56 to 1.29 times.
Construction phase telemetry then located the shallow-program peak inside the
correction-by-correction join. Record arrangement deltas already own canonical
(key, time, tuple) order; their constructor now enforces that order, and the
join merges the two ordered streams instead of building a duplicate keyed
index over the right correction. Repeated-key ranges still form the complete
Cartesian product, while probe telemetry retains its prior per-left-row
definition.
At 100,000 rows the shallow construction peak fell from 216,754,809 to 211,925,329 bytes. At one million rows it fell from 2,120,750,729 to 2,072,630,281 bytes, removing 48,120,448 bytes of transient index state. Retained and mutation-peak memory were unchanged. The 30-sample million-row p50 was 0.419 ms; the circuit remains 770 times faster than the matched Established p50 while its construction-peak ratio improves from 1.77 to 1.73 times.
Phase boundaries then isolated the next peak inside record distinct evaluation. The old path separately materialized the touched-row set, a promotion map, retained profiles, grouped corrections, output corrections and the record journal. Record distinct now consumes its input into one grouped correction authority. Each row is validated and promoted as that authority is drained, and the same row correction directly produces the zero-crossing output and persistent journal. Batch and single-row promotion share the same cached record identity; batch promotion retains its validate-before-mutate contract.
On the 100,000-row shallow control this reduced construction peak from 211,925,329 to 207,040,154 bytes. On the million-row control it reduced the peak from 2,072,630,281 to 2,037,063,114 bytes, another 35,567,167 bytes or 1.7 percent. Retained heap remained 311,888,378 bytes and mutation peak remained 1,357,928,337 bytes. The construction ratio against the 1,196,584,158-byte Established control is 1.70 times. A repeated 30-sample run measured 0.010 ms p50, but this revision claims only the memory change because that latency is not comparable with the earlier feature-instrumented run.
The next phase boundary placed the remaining peak in sink-row promotion. That path previously collected every escaping evaluation identity into a set, then constructed a second identity-to-record map before producing the record sink profiles. Promotion now validates the complete input before mutation and then consumes it directly into record profiles through the same cached single-row promotion primitive used by distinct. This removes two transaction-sized identity indexes without weakening failure atomicity.
The 100,000-row shallow construction peak fell from 207,040,154 to 204,692,322 bytes. The million-row peak fell from 2,037,063,114 to 2,001,032,146 bytes, removing another 36,030,968 bytes. Retained heap and mutation peak remained 311,888,378 and 1,357,928,337 bytes. The construction ratio against Established is now 1.67 times. Two non-instrumented 30-sample controls measured 0.009 ms p50; the memory reduction remains the claimed effect. The remaining shallow construction peak is inside the initial record join, not distinct, promotion, state preparation or sink publication.
Join phase telemetry separated arrangement construction from cross-term emission. The correction output previously grew while both consumed input profiles remained live, even though their record arrangements were already self-contained. Record join now releases each owned input immediately after arrangement; borrowed inputs remain unaffected. This is a lifetime change, not a second representation or specialized execution path.
The 100,000-row shallow construction peak fell from 204,692,322 to 197,837,922 bytes. The million-row peak fell from 2,001,032,146 to 1,945,059,330 bytes, removing another 55,972,816 bytes. Retained heap and mutation peak again remained 311,888,378 and 1,357,928,337 bytes. The construction ratio against Established is now 1.63 times. The 30-sample million-row p50 remained 0.009 ms. The next measured peak is persistent distinct-state preparation after join evaluation.
Record distinct corrections then adopted the same row-major
row -> sparse temporal profile representation as retained distinct support.
Evaluation no longer expands a grouped row correction into a time-major
journal for state preparation to regroup. Ordinary and Product preparation use
one kernel, and prepared assignments use the same map shape; an empty temporal
profile denotes deletion. Initial assignments therefore move the correction
tree directly into prepared state. Candidate sinks derive their required
time-major external delta without becoming a second state authority.
This representation change is memory-neutral in retained and mutation state. At 100,000 rows, shallow construction increased from 197,837,922 to 199,492,842 bytes while wide-recursive construction decreased from 91,551,406 to 88,491,705 bytes. At one million shallow rows construction increased from 1,945,059,330 to 1,949,033,290 bytes, 0.20 percent; retained heap remained 311,888,378 bytes, mutation peak remained 1,357,928,337 bytes and the 30-sample p50 remained 0.009 ms. The small shallow cost is accepted because it removes a representation conversion and makes ordinary and product-time state preparation structurally identical.
Adaptive trie child storage reduced the 10,000-state recursive multiway retraction workload’s retained heap from 73,058,699 to 31,378,459 bytes and its mutation peak from 97,468,172 to 55,784,956 bytes. The same 20-sample run measured 4.955 ms p50, compared with 5.036 ms before the representation change; logical state remained 70,000 keys, 140,003 nodes and 140,000 edges. Applying the same adaptive child map to prepared trie patches subsequently reduced construction peak from 139,208,745 to 64,075,097 bytes. Retained heap remained 31,378,459 bytes, mutation peak remained 55,784,956 bytes and the 20-sample p50 measured 4.910 ms. Prepared patches and published tries now share one storage policy rather than relying on a dense transaction-only map. A matched Established run measured 68.047 ms p50, 38,066,979 construction-peak bytes, 28,024,345 mutation-peak bytes and 9,842,015 retained bytes. Circuit construction is therefore 1.68 times Established instead of 3.66 times, while mutation peak is 1.99 times and retained state is 3.19 times Established. Recursive multiway retained memory is not yet within the replacement gate.
Trie terminal nodes subsequently stopped carrying prefix-only metadata and child storage. A terminal is represented by its temporal weight; only a node with a suffix owns a boxed branch. The existing generic update, overlay, Generic Join and logical checkpoint-entry interfaces are unchanged, so this is one physical representation shared by full and incremental evaluation rather than an arity-specific second index. Promotion preserves a key that is both a terminal and a prefix; demotion restores the compact terminal after its final child is removed.
On matched optimized 30-sample recursive_multiway_retract runs at 100,000
components and a 100-row delta, p50/p95 changed from 43.062/43.810 ms to
43.974/44.783 ms. Retained heap fell from 283,043,307 to 270,245,419 bytes
(4.5 percent), and mutation peak fell from 533,457,438 to 520,661,310 bytes
(2.4 percent); construction peak was unchanged at 543,278,362 bytes. The 2.1
percent p50 cost is retained because the workload remains 15.6 times faster
than the matched Established p50 of 683.942 ms. Retained heap remains 2.66
times Established’s 101,715,851 bytes, so this improves but does not discharge
the replacement memory gate.
Singleton prefixes were then represented as boxed path nodes whose sole child is inline. Zero, one and multiple children normalize to terminal, path and branch forms after every publication. This removes one allocation per unary prefix without inflating terminal nodes; logical node/edge metrics, ordered traversal, prepared overlays and checkpoint entries remain representation- independent.
On the same 100,000-component, 100-row, 30-sample workload, path compression changed p50/p95 from 43.974/44.783 ms to 42.857/43.898 ms. Retained heap fell from 270,245,419 to 253,445,419 bytes (6.2 percent) and mutation peak from 520,661,310 to 503,861,310 bytes (3.2 percent); construction peak remained 543,278,362 bytes. Relative to the trie before terminal and path compaction, retained heap is 10.5 percent lower and p50 is 0.5 percent lower. The circuit is 16.0 times faster than Established, but still retains 2.49 times its heap; the replacement memory gate remains open.
That representation was subsequently refined because projection-seed
interning made stateless base rows permanent arena records. Projection
membership is now adaptive per semantic tuple: an existing program-arena
record is referenced by RecordId; otherwise the projection retains the
canonical encoded tuple. Projection construction and checkpoint restore only
look up existing records and never intern rows. The two physical forms are
disjoint and materialize through one semantic catalog interface.
base relation tuple
|
v
existing program record? ---- yes ----> RecordId membership
|
no
v
canonical encoded membership
| circuit profiles / traces
| |
+-------------------+-------------------------+
v
union materialized-model view
|
v
semantic catalog / checkpoint
This preserves compact recursive membership without forcing projection-only inputs into the append-only arena. On a one-million-row high-overlap workload, 100-row retraction and ten samples, retained heap fell from 254,163,116 to 101,506,613 bytes while p50 measured 0.348 ms. Arena cardinality fell from 1,100,100 to 100,000 records. A one-million-row recursive-wide control retained 602,119,645 bytes, 872 bytes above the record-native measurement, with 2,000,300 arena records and a 1.020 ms ten-sample p50. The all-encoded prototype retained 747,591,236 bytes on that control and was rejected because it duplicated record-backed recursive outputs as encoded keys.
The projection subsequently stopped retaining derived membership entirely.
AdaptiveRelations owns only base facts; circuit profiles and recursive traces
are the sole derived authority. Full-model reads, point membership, columnar
construction and checkpoint serialization synthesize the set union with sparse
direct facts on rule-head relations. Relation-specific reads use a component
API and full materialization streams borrowed derived values directly into the
catalog, avoiding an intermediate derived-tuple vector.
At one million rows, ten samples and delta 100, wide recursion retained 590,500,456 bytes, down 11,619,189 bytes from adaptive union membership. P50 improved from 1.020 to 0.911 ms and mutation peak fell from 793,347,886 to 781,729,513 bytes. At 100,000 rows, retained heap changed from 61,475,053 to 60,313,616 bytes for wide recursion, 67,682,276 to 66,519,967 bytes for upper retraction, 152,964,526 to 149,479,025 bytes for lower NAF, and 26,590,992 to 26,164,212 bytes for the mixed trace. Candidate/settled and profile/temporal metric pairs remain views of shared physical traces, not additional stores.
Recursive components borrow accepted external relations instead of cloning each semantic Z-set before staging iteration zero. Validation remains strict at the recursive boundary and the staged profile owns the transaction journal. On the million-row wide workload, construction peak fell from 5,203,105,269 to 5,011,486,993 bytes.
Published retry identity now retains the last output delta as weighted
RecordId sets. Public ProgramBatchOutcome values and checkpoint envelopes
remain semantic: preparation resolves the compact retry state only for an
idempotent duplicate, checkpoint encoding resolves it canonically, and restore
interns the logical output after component validation. Unknown record IDs fail
loudly. The million-row wide workload retained 425,167,720 bytes, down
165,332,736 bytes from semantic retry output; mutation peak fell by the same
amount to 616,396,777 bytes, with 0.980 ms p50 over ten samples. High-overlap
retained heap fell from 101,506,613
to 90,210,574 bytes. Construction peak is unchanged because preparation still
owns semantic output until the atomic commit.
Program flow is keyed by typed relation identity. Immutable consumer metadata
is compiled into the program plan and its commitment. External deltas retain
frontier ownership; derived deltas, public output and downstream flow share
record identities. A relation is released before preparing its last consumer.
Prepared program journals retain no semantic output copy. Interned acyclic
components publish record sink deltas directly. Interned recursive components
expose their scheduler’s record output directly to program flow; the program no
longer clones and re-interns the resolved semantic output. Fanout tests cover a
relation consumed by adjacent and nonadjacent strata; signed four-stratum
differentials match full evaluation for insertion and retraction. Public
apply resolves semantic output only after atomic commit.
Record-backed profile evaluation owns the semantic-to-record sink boundary.
Operator rows remain semantic only while a transaction evaluates its schedule;
settled and candidate sink profiles leave that boundary as RecordId profiles.
Recursive scheduling and interned acyclic publication consume those identities
without cloning tuples or interning them again. The record transaction token
continues to bind prepared sink identities to the transaction that created
them. Semantic profile evaluation retains its semantic sink type, so the two
backends share rule evaluation without retaining parallel output authorities.
Product-time rule sessions use the same boundary: component settled and
candidate profiles remain record-native through outer-coordinate consolidation.
Only an inter-component relation with a later consumer is resolved into the
semantic profile required by the next component’s scan interface. The program
flow owner performs that projection and immediately retires it after the last
consumer; final Product publication never reconstructs semantic sink profiles.
The Product session module owns only construction, staged evaluation, audit,
and atomic publication. Its lifecycle, fault-injection and physical-kernel
fixtures live in an owned test submodule, so expanding the conformance surface
does not enlarge the production transaction boundary.
Semantic, record-backed and Product sessions call one input-identity validator
before evaluation. A relation must equal the plan relation selected by its
qualified name, including module and arity; unknown or same-name mismatched
identities fail before record interning or session mutation. Product retry with
the valid identity then proceeds from unchanged state.
Distinct corrections follow the backend representation. Semantic evaluation
journals Row; record-backed ordinary and Product evaluation journal RowRef.
Record distinct preparation interns each touched row once, uses that identity
for retained support preparation, and exposes tuple-valued candidate sinks as
the underlying RecordId. Candidate publication therefore cannot diverge from
the support journal or create a second record identity. Backend-associated
distinct and candidate types keep this distinction structural while sharing
the zero-crossing algorithm.
Antijoin journals follow the same representation rule. Record-backed ordinary
and Product evaluation retain arrangement-key, tuple and blocker-key identities
in ProfiledRecordAntijoinDelta; semantic evaluation retains semantic keys.
The retained-window read interns each touched key once and returns its identity
map with the semantic evaluation window. Journal construction reuses that map,
and record state preparation consumes the identity journal directly. The
backend contract associates the complete antijoin journal type rather than only
its blocker correction, preventing mixed semantic and record fields.
Factorized aggregate journals are also backend-associated. Record evaluation
publishes BindingKeyRef groups containing record-backed factor corrections;
record state preparation accepts only that type. Non-extrema corrections cross
the semantic-to-record boundary once after output differentiation. Extrema
evaluation already requires record corrections to compare retained indexes, so
the journal retains that exact correction instead of discarding it and
re-interning the semantic source. Count journals follow the same rule: semantic
evaluation publishes semantic groups, while record-backed ordinary and Product
evaluation publish BindingKeyRef groups and record-backed folds. Record state
preparation consumes those identities directly. Record extrema evaluation also
retains outer keys as BindingKeyRef and resolves a semantic binding only when
constructing an externally visible output row. Conversion therefore occurs
once at the evaluation boundary, and the journal and prepared state cannot
diverge through separate representations. Extrema validation integrates the
record-native input profile directly; it does not intern a sentinel binding or
publish an unreferenced record solely to exercise validation.
Multiway-join input follows the same backend boundary. The evaluation backend
associates its input type: semantic evaluation receives tuple profiles, while
record-backed ordinary and Product evaluation receives RecordScanProfile.
Orchestration delays either semantic or record profiles without converting
them. Interned multiway state resolves each input record only long enough to
validate constants and repeated variables, then interns only the projected
join-key values. Product gamma currently retains semantic multiway keys, so its
record-aware semantic codec performs the same projection without interning;
this preserves the Product state representation while eliminating complete
tuple-profile reconstruction. Produced operator profiles remain semantic until
operator outputs become record-native.
Interned multiway tries use a canonical hybrid scalar key. Integers representable
as i32 remain inline; every other value, including out-of-range integers, uses
the arena’s canonical scalar identity. The representation is exclusive rather
than a cache: an integer has exactly one key form, checkpoint serialization
resolves both forms to the same semantic Value, and restore deterministically
selects the same form. This removes singleton-record payload and digest-index
ownership for common join keys without widening every trie edge to Value.
An all-interned external-flow prototype was rejected: the million-row high-overlap workload retained 242,913,309 bytes and 1,100,000 arena records. Preserving external ownership restored retained memory to 90,215,846 bytes and 100,000 records; p50 was 0.338 ms over three samples. This boundary is an ownership invariant, not a second persistent model representation.
The million-row single-recursive-component control measured 5,011,493,121 bytes construction peak, 425,173,008 bytes retained and 616,402,065 bytes mutation peak. The 6,128-byte construction difference from the preceding 5,011,486,993-byte run is noise: this workload has no inter-component edge. Component preparation still reconstructs semantic scan profiles, so the next cut is record-native component input and sink output rather than another program-level representation.
Direct recursive record-output propagation measured 5,011,492,656 bytes construction peak, 425,172,279 bytes retained and 616,401,336 bytes mutation peak on the one-sample million-row control. The negligible change confirms that the dominant remaining construction allocation precedes the component output boundary: semantic scan/profile preparation and recursive assignment journals.
Recursive admission subsequently became ownership-transferring. The program moves the accepted semantic batch into the recursive component; impulse deltas become iteration-zero profile buckets without cloning. Signed projection assignments use one typed encoded-key accumulator borrowing those profiles and the recursive result, shared by semantic and interned paths. The million-row construction peak fell from 5,011,492,656 to 4,819,874,188 bytes, 3.8 percent. Retained memory remained 425,172,279 bytes and mutation peak remained 616,401,336 bytes. Component input is still semantic at scan evaluation, but it now has one frontier owner rather than parallel batch and profile owners.
Record-profiled sessions no longer retain a session-local input profile map. That map was updated after every stage but was never read, committed or checkpointed; operator derivative state is the sole staged authority. Removing the redundant input authority reduced the million-row construction peak from 4,819,874,188 to 4,628,255,056 bytes, 4.0 percent. Retained and mutation memory were unchanged.
Record-profiled scan admission uses one mixed input envelope. External
frontier-owned deltas remain semantic profiles; derived feedback remains
RecordId profiles. Representation dispatch occurs only at Scan and
DelayedScan: both paths call the same slice-based binding constructor, while
the record path resolves pending or published IDs through the frontier
transaction. Downstream rows and operators remain representation-independent.
Missing or non-value records fail loudly before state preparation.
Recursive feedback therefore no longer follows
RecordId -> Tuple Z-set -> tuple profile -> binding row. It remains record
backed until scan construction. The million-row construction peak fell from
4,628,255,056 to 4,245,017,958 bytes, 8.3 percent. Retained memory remained
425,172,279 bytes and mutation peak remained 616,401,336 bytes. Record scan
tests cover semantic parity, repeated variables, constants, signed weights,
pending transaction IDs and non-value record refusal.
The ten-sample latency control measured 0.995 ms p50 and 1.355 ms p95, versus 0.980 ms and 1.326 ms before the construction cuts. The 1.5 and 2.2 percent differences are within run variance; record-backed feedback did not introduce a material mutation-latency regression.
Interned recursive prepared state is now a distinct type rather than a semantic
prepared journal parameterized by RecordId. It retains the scheduler record
transaction, record-profile journal and signed assignments, but no resolved
semantic outcome, duplicate payload or standalone frontier metadata. Signed
assignments resolve record tuples directly into their final journal and do not
materialize an intermediate semantic output Z-set. The million-row construction
peak remained 4,245,017,958 bytes, locating the peak before final assignment and
publication assembly.
Record-profile finalization consumes staged operator, join, antijoin, distinct and aggregate maps when constructing semantic conversion journals. It no longer clones the entire staged profile before conversion; each source container drops as its journal is built. The wide construction peak remained 4,245,017,958 bytes, confirming that the measured peak occurs before final profile conversion. The ownership cut remains structural: prepared state has one owner through finalization.
Benchmark-only phase observation located the remaining peak inside the feedback join: record scan peaked at 3,207,115,614 bytes and join construction peaked at 4,245,019,046 bytes. The evaluator now transfers a node profile into join preparation when the join is its last consumer. Binding rows are consumed into tuple corrections by moving values from their bindings; shared or retained nodes remain borrowed. This is derived from the same immutable consumer counts used for operator liveness.
The million-row construction peak fell from 4,245,017,958 to 3,791,864,069 bytes, 10.7 percent. Retained memory remained 425,172,279 bytes and mutation peak remained 616,401,336 bytes. The benchmark observer is opt-in and records only allocator counters at named preparation boundaries; production builds contain no observer state.
Join accumulation consumes its staged cross-term profile. This preserves transactional overflow validation while moving disjoint iteration buckets and values instead of cloning them. On the million-row workload, the feedback join previously held both the 846,284,576-byte staged result and its accumulated copy; its phase peak fell from 3,526,734,470 to 3,207,115,614 bytes. The overall construction peak remains 3,791,865,157 bytes at final semantic-to-record preparation. This identifies record-native session staging, rather than further join-local ownership changes, as the next representation boundary.
Final record preparation consumes semantic correction journals and moves row, tuple, binding, and aggregate-key values into the transaction-owned record suffix. Preparation remains atomic: published state is borrowed, assignments remain private, and only a fully validated prepared state can commit. This removes clone-based ownership at the representation boundary but does not lower the million-row construction peak, which remains 3,791,865,157 bytes. The remaining peak therefore reflects simultaneous semantic staged authority and record preparation metadata, not cloned payload values inside the conversion loop.
Record-profile state supports direct correction-overlay preparation. Operator, join, antijoin, distinct, and aggregate corrections remain in record identity space; checked merge produces the same private prepared assignments as semantic conversion without resolving payloads. Exact cancellation prunes every state family. Overflow, negative support, or shape divergence leaves published state unchanged. This primitive is the finalization boundary required before the recursive session itself can retain record-native staged authority.
The recursive session now retains that correction overlay directly in record identity space. One representation-typed state-view interface preserves the single scheduled evaluator: semantic standalone circuits read semantic state, while program-owned circuits read published and transaction-staged record overlays. Join evaluation emits correction against both record overlays plus correction against correction exactly once. Distinct, antijoin, and aggregate operators fold the same two record overlays before applying their correction. Finalization applies the record overlay directly; the semantic join, antijoin, distinct, and aggregate conversion adapters no longer exist.
On the million-row recursive insertion workload, construction peak fell from 3,791,865,157 to 3,143,330,926 bytes, 17.1 percent. Retained heap was 425,120,895 bytes and mutation peak was 616,349,952 bytes. The remaining construction peak occurs during feedback scan expansion at 3,143,330,926 bytes. Final record-profile publication no longer raises the peak.
A ten-sample mutation control measured 0.756 ms p50 and 1.167 ms p95. Its construction peak was 3,143,329,838 bytes, retained heap was 425,119,807 bytes, and mutation peak was 616,348,864 bytes.
The remaining scan peak is addressed through one canonical compact binding:
strictly increasing (variable, value) pairs in one exact-size allocation.
Record payloads adopt this type first while preserving their canonical CBOR
bytes and digest exactly. Evaluator rows, linear operators, joins, aggregates,
and profile keys will adopt the same type together; an alternate compact row
variant is forbidden because equal bindings must remain structurally equal by
construction.
After the evaluator-wide cut, the million-row phase run measured a 2,536,851,923-byte construction peak, 19.3 percent below record-native staging and 51.2 percent below the original 5,203,105,237 bytes. Retained heap remained 425,120,895 bytes because compact bindings replace only frontier-local rows. The diagnostic mutation sample measured 1.234 ms. A ten-sample control measured 0.842 ms p50 and 1.302 ms p95. Construction peak was 2,536,850,835 bytes and retained heap was 425,119,807 bytes.
Map evaluation reads compact bindings through a variable-lookup interface on the existing expression interpreter. The prior dense vector adapter, whose length depended on the largest sparse variable identifier, is removed. Missing variable, conditional, builtin, arithmetic, and undefined-expression behavior continues to come from the one evaluator.
Temporal join arrangements subsequently moved from nested singleton maps to a
shared immutable differential trace spine. Each batch is sorted and
consolidated by (key, iteration, tuple). Occupied geometric levels own
immutable batches; preparation probes only touched cells, validates checked
weights and cardinality changes, and plans level merges before an infallible
spine replacement. Key reads binary-search every occupied batch and merge only
the matching ranges. Checkpoints enumerate the logical consolidated trace, so
batch boundaries and compaction timing do not enter durable identity.
signed operator delta
|
v
consolidate delta batch -----> exact touched-cell probes across retained levels
| |
+----------------------+---------------+
v
validate weights and cardinality
|
v
plan geometric level merges
|
v
sealed replacement spine
|
atomic publication boundary
v
[L0] [L1] [L2] ... [Ln] immutable sorted batches
\ \ \ /
+---- binary key-range merge ----> operator reader
A generated mixed-update oracle exposed and preserves a critical compaction regression: resizing for a smaller delta must not truncate occupied higher levels. A fixed-delta regression also proves that preparing one changed cell against 4,096 retained cells performs fewer than 128 key comparisons and no full trace materialization. Record-backed join and antijoin readers use the same key-local cursor; full logical materialization is restricted to explicit checkpoint and conversion boundaries.
Repeated same-machine measurements used five runs of 300 samples at 10,000 retained rows and a 100-row requested delta. Before trace compaction, wide recursion measured 0.962–1.053 ms p50 with a 0.995 ms median; the compact trace measured 0.931–0.985 ms with a 0.949 ms median. The connected count pipeline measured 3.513–3.591 ms before compaction and 3.443–3.508 ms afterward, with 3.527 and 3.448 ms medians. The trace is 4.6 and 2.2 percent faster at the medians. Earlier isolated 30-sample results suggesting a 31–35 percent regression were not reproducible under repeated measurement.
Recursive candidate history subsequently adopted the same trace spine. Sparse tuple profiles now exist only as key-local ephemeral views; snapshots share immutable batches, preparation changes only touched keys and checkpoints retain the logical tuple-to-ordered-cells wire. At 10,000 retained rows, wide recursion retained 6,931,869 bytes, down 61.2 percent from the compact-record record-membership implementation. At 100,000 rows, 30 samples measured 0.945/1.041/1.220 ms p50/p95/p99, 67,435,629 retained bytes and 86,551,342 mutation-peak bytes. The temporal and candidate traces held 200,000 entries each in two and one batches, consuming 4.8 and 3.2 MB of entry capacity. Candidate compaction reduced retained heap another 13.2 percent from the temporal-only trace result. The connected count pipeline retained 6.21 MB at 10,000 rows. Latency is fixed-delta local; arena payload/index ownership remains the principal memory difference from the established maintainer.
Ordinary acyclic joins apply the same ownership rule without temporal profiles:
bilateral arrangements are the sole retained join-input state. A ten-sample
100-fact insertion over two 100,000-row binary inputs measured 352.583
microseconds p50 and 214,339,662 retained bytes, versus 27.461 milliseconds and
54,972,080 bytes for the established maintainer. Removing the redundant generic
join inputs eliminated 200,000 operator rows and reduced circuit retained heap
by 42.0 percent. The remaining 100,000 support rows are explicitly owned by the
ordinary-stratum Distinct operator; generic operator rows are zero. The
latency result is favorable. Maintainer-owned circuits retain no typed sinks:
the encoded read catalog owns output membership, while direct facts on rule-head
relations use sparse provenance and derived membership comes from Distinct
support. This preserves EDB/IDB overlap without three complete catalogs.
Retained heap fell another 8.2 percent, but the 3.90-times retained and
4.84-times peak heap ratios are not production gate wins.
A separate recursive-correction benchmark compares one committed causal mutation with fresh full evaluation. Repeated Criterion measurements after the recursive hot-path optimizations and seal-boundary activation were:
| workload | scale | causal circuit | full evaluation | ratio |
|---|---|---|---|---|
| deletion cascade | 16 | 0.177 ms | 0.080 ms | 2.2x slower |
| deletion cascade | 32 | 0.433 ms | 0.294 ms | 1.5x slower |
| deletion cascade | 64 | 1.214 ms | 1.173 ms | 1.0x slower |
| deletion cascade | 128 | 4.229 ms | 4.892 ms | 1.2x faster |
| alternative support | 16 | 0.030 ms | 0.088 ms | 2.9x faster |
| alternative support | 32 | 0.053 ms | 0.313 ms | 5.9x faster |
| alternative support | 64 | 0.140 ms | 1.211 ms | 8.6x faster |
| alternative support | 128 | 0.543 ms | 4.927 ms | 9.1x faster |
Correctness passed. Stage-local body evaluation, key-first temporal arrangements and tuple-local distinct sealing reduced causal latency by 89–99.8 percent relative to the first causal implementation. Alternative-support maintenance is 2.9–9.1 times faster than full evaluation. Deletion cascades cross over from 2.2 times slower at scale 16 to 1.2 times faster at scale 128. Each cell is the midpoint of ten Criterion samples after a three-second warmup and an approximately five-second measurement interval. This remains a focused microbenchmark, not a general performance claim; retiming retained inner profiles is not a valid optimization.
After candidate history moved to the trace spine, 30-sample causal-circuit confidence intervals were:
| workload | scale | causal circuit interval | prior full-evaluation midpoint | ratio at circuit midpoint |
|---|---|---|---|---|
| deletion cascade | 16 | 0.135–0.136 ms | 0.080 ms | 1.7x slower |
| deletion cascade | 32 | 0.281–0.284 ms | 0.294 ms | 1.0x faster |
| deletion cascade | 64 | 0.603–0.616 ms | 1.173 ms | 1.9x faster |
| deletion cascade | 128 | 1.352–1.367 ms | 4.892 ms | 3.6x faster |
| alternative support | 16 | 0.023–0.025 ms | 0.088 ms | 3.7x faster |
| alternative support | 32 | 0.031–0.033 ms | 0.313 ms | 9.9x faster |
| alternative support | 64 | 0.053–0.054 ms | 1.211 ms | 22.5x faster |
| alternative support | 128 | 0.172–0.229 ms | 4.927 ms | 25.4x faster |
The full-evaluation column is the unchanged prior baseline and was not rerun in the 30-sample trace measurement. The causal values therefore demonstrate the trace implementation’s progression, not a new matched-machine ratio claim.
Heap values are live requested allocations relative to the pre-construction process baseline, not RSS, allocator reservation, stack or mapped-file size. The million-row Phase-A matrix now covers shallow and recursive insertion, low/high-overlap retraction, lower-stratum negation, fused count, a connected count pipeline, a mixed three-commit trace and dense mutual support. Completed pairs are 13.5–5,594 times faster at p50. High-overlap retraction retains 33.9 percent less heap than the established maintainer and reaches 15.4 percent more peak heap. Every other completed pair retains 2.6–7.9 times the established heap. Established recursive count exceeded a ten-minute bound; its connected variant was stopped after 245 seconds. Both dense-clique implementations failed to construct and sample within ten minutes: the circuit reached 17.77 GiB RSS and the established path reached 24.15 GB maximum RSS. Exact p50/p95/p99 and heap values are recorded beside the benchmark. Repeated-machine variance, the 10-million-fact run and recursive round/probe telemetry remain open. The latency gate passes; retained and construction memory prevent default routing.
Dense phase tracing later identified a separate frontier-local amplification:
the transitive rule materialized (x, y, z) join bindings although its sole
Project consumer retained only (x, z). Project nodes with one Join predecessor
now pass their projection into the join emitter. Each bilinear term consolidates
the projected tuple directly; the immutable plan, join-input arrangements and
checkpoint identity do not change. At 100,000 dense inputs this reduced
construction peak from 2,539,749,342 to 1,687,412,386 bytes, 33.6 percent, and
measured 98.913 ms p50 over three samples. Retained heap remained 262,193,524
bytes because candidate and temporal histories remain authoritative.
The scheduler boundary subsequently became consuming. Once an inner iteration is sealed, its sink Z-set moves from the candidate queue into the distinct scheduler; only future buckets remain queued. This preserves delayed future work while removing a transaction-length duplicate of every consumed bucket. The dense construction peak fell again to 1,367,329,752 bytes, 19.0 percent below projection-aware emission and 46.2 percent below its original 2,539,749,342-byte control. Retained state remained unchanged.
Operator-profile ownership follows one plan-derived last-consumer policy. Unretained profiles move into an exclusive unary Union, Join input or terminal Sink; shared and retained profiles remain borrowed. Terminal sinks consume tuple rows directly rather than cloning tuple payloads into a second profile. The same dense control measured 83.197 ms p50 and 85.279 ms p95 over ten samples. Construction peak fell from 1,367,329,752 to 1,250,791,694 bytes, 8.5 percent, and 50.8 percent from the original control. Retained state remained 262,193,524 bytes.
Join evaluation exposes one canonical row-emission kernel. Callers that need a Z-set collect that stream; temporal correction evaluation instead accumulates rows directly into the destination iteration. This changes neither bilinear terms nor plan/checkpoint identity. On the million-row wide-recursion control, construction peak fell from 2,536,851,555 to 1,962,000,150 bytes, 22.7 percent; two five-sample controls measured 0.744–0.937 ms p50 and 1.314–1.502 ms p95. Retained heap and mutation peak remained 425,119,807 and 616,348,864 bytes. Dense construction changed only 0.3 percent to 1,246,692,866 bytes, so its remaining transient is not the materialized join-result boundary.
Signed publication records two independent effects: relation visibility and evaluator projection assignments. Once projection authority is delegated, a newly populated relation publishes only its relation identifier, and an already-visible relation publishes no evaluator journal. Internal projection authority and base-support ownership still require the checked tuple journal. This removes state that had no consumer instead of adding a second tuple representation. Dense live heap after signed-assignment preparation fell from 1,113,786,852 to 899,725,844 bytes, 19.2 percent. Construction peak remained 1,246,692,866 bytes at the earlier recursive join/scheduler transition.
Scheduler finalization consumes its transaction-local candidate and output profiles. The prepared trace validates against a borrowed settled delta; that same delta then moves into the transaction outcome, while timed buckets move into the journal. Dense construction peak fell from 1,246,692,866 to 1,241,018,934 bytes, 0.5 percent. Ten samples measured 84.216 ms p50 and 87.775 ms p95. The million-row wide control retained its 1,962,000,150-byte peak and measured 0.701 ms p50 over five samples.
Join correction emission accumulates into the transaction-local output that already owns published terms. The allocating interface is an adapter over that same accumulator, so ownership transfer does not create a second correction algorithm or representation. Invalid overlay metadata is rejected before the caller-owned output changes; later errors discard the enclosing prepared transaction. Dense construction peak fell from 1,241,018,934 to 1,205,741,822 bytes, 2.8 percent, while retained heap remained 262,193,524 bytes. Ten samples measured 83.934 ms p50 and 89.958 ms p95. The million-row wide control remained byte-identical at a 1,962,000,150-byte peak and measured 0.732 ms p50 over five samples.
Work telemetry follows the same prepare/validate/commit boundary as semantic state. Each circuit evaluation session counts keyed arrangement probes; each recursive scheduler records productive feedback rounds. Prepared component journals carry those values and the whole-program journal checks and sums them before publication. Failed preparation cannot change the last published measurement. Duplicate and effective-empty transactions publish zero. The counters are observational: checkpoint payloads, plan identities and derivation commitments exclude them, and restore begins without a measurement. The sampled benchmark records forward-transaction counters before the inverse restoration and sums multi-commit traces. A 10,000-row, ten-fact wide recursive insertion reported zero arrangement probes and one recursive round; the dense recursive retraction control reported 3,460 probes and five rounds. On an adjacent warm 30-sample 100,000-row dense control, observed telemetry measured 86.043 ms p50 versus 83.087 ms without telemetry, a 3.6 percent cost. Peak and retained heap increased by 48 and 72 bytes respectively.
Phase B — pair-encoded value model
Every logical relation becomes two parallel integer-weighted streams carrying
evidence-for and evidence-against. Negation swaps streams; bilattice operations
are cross-stream value operators. Integer multiplicity remains the DBSP weight:
Truth4 and positive-Boolean provenance are not weight semirings. This phase is
assert-only and must reproduce both ordinary and $undefined:: extents while
preserving the I ⊆ J K3 gate.
Phase C — retraction under the pair
Retraction is admitted only after the deletion behavior of the provenance projection is mechanized. Provenance remains a side-track keyed by atom, polarity, rule and witness; it does not replace integer circuit weights. Until the gate is discharged, pair-bearing retractions use the existing conservative fallback.
Phase D — incremental well-founded semantics
Recursion through negation uses precision-positive coordinates. For fixed base
extent E, let gamma_E(I) be the reduct least model under assumption I and
let the finite relevant domain be D_E = gamma_E(empty). Antitonicity gives
gamma_E(I) subset D_E for every assumption. The retained semantic coordinates
are definite truth T and definite falsehood F; compatibility with the public
representation is U = D_E ∖ F, where U is possible truth. Define:
C_E(T, F) = (
gamma_E(D_E ∖ F),
D_E ∖ gamma_E(T)
)
C_E is monotone in componentwise subset order: increasing F decreases the
first gamma assumption and therefore increases its output; increasing T
decreases the second gamma output and therefore increases its complement. Its
least fixpoint from (empty, empty) maps exactly to the precision-least stable
revision fixpoint (T,U), hence to the batch well-founded model. This
equivalence is mechanized before the dynamic circuit becomes production
authority.
Argon.Reasoning.Datalog.DynamicCoupled also proves the affected-region
settlement theorem used by Product. Regional least-fixpoint recomputation equals
the complete positive-coordinate least fixpoint when the prior and new fixed
points agree outside independently selected true and false regions and the
regional fixed point is also fixed outside those regions. A second theorem
proves that exterior closure for every region-restricted revision step is a
stronger sufficient condition. This matches Product’s separate affected-
coordinate sets and separates the minimal semantic obligation from a static
closure proof. Product still requires evidence that its concrete dependency
closure establishes the premises and that its worklist computes the regional
least fixed point for every admitted mutation; finite differential tests do not
prove those properties.
The same module proves a worklist theorem: any sequence starting at the empty
regional state, whose every step is below one complete regional revision, and
which terminates at a regional fixed point equals the regional least fixed
point. Consequence partition and processing order do not appear in the result.
The same file proves the concrete bridge used by the implementation: any next
coordinate state contained in both the selected region and the complete
gamma-derived positive revision is below the regional revision. Its worklist
corollary reduces runtime correspondence to gamma-bound containment, region
containment and final fixed-point agreement rather than an opaque regional-
step premise.
Runtime regional feedback is represented by an opaque certified-step type.
Production construction is private to the differentiated driver and admits
only positive truth transitions produced by the current truth gamma revision
and positive falsehood transitions produced by the current domain-minus-
possible transition. It cannot invent a candidate through the scheduler API,
cannot admit signed overdeletion, and cannot reseed an already-published tuple
outside the selected region. This makes the runtime step an
under-approximation of the gamma transitions by construction. Before each
scheduler output enters accumulated regional state, delta-local checks require
every truth addition to exist in the current truth-gamma output and every
falsehood addition to exist in the current domain-minus-possible output. This
enforces the Lean gamma-bound and region-bound premises at the concrete
worklist boundary without scanning the complete retained component. Connecting
gamma derivative exactness to the formal complete gamma revision remains an
audit and proof obligation.
An independent persistent-state differential exercises that concrete
derivative boundary over all 512 three-node move graphs and all eight fixed
assumptions. One state advances only through signed assumption deltas while a
second state receives complete target assignments; all 4,096 gamma outputs
agree. This checks the exact runtime API used by Product separately from the
existing direct semantic oracle comparison.
Recursive finalization accepts only a quiescent-session type. Converting a
mutable session into that type exhaustively rejects an unprocessed required
profile suffix, pending evaluator feedback, or an unsealed current candidate
bucket. Product and ordinary recursive callers share this boundary; a future
caller cannot publish a merely presumed fixed point by calling finalization
directly.
The differentiated driver returns an opaque certified regional revision only
after sparse coordinate containment, expected scheduler deltas, gamma outputs,
and both coupled assumptions agree on the complete selected region. Its fields
are private and publication consumes the certified result. Other subsystem
callers therefore cannot construct a publishable regional result while
bypassing the fixed-point boundary checks.
signed base correction
|
+----------------+----------------+
| | |
v v v
domain gamma true gamma possible gamma
gamma_E(empty) gamma_E(D_E ∖ F) gamma_E(T)
| | |
v v v
delta D delta T delta U
| | |
+----------------+----------------+
|
v
causal coupled-coordinate scheduler
delta F = delta(D_E ∖ U)
|
consolidate + feedback
|
v
settled least fixpoint (T, F)
|
U = D_E ∖ F; undefined = U ∖ T
The three gamma roles share one immutable plan and record arena but own separate
mutable derivative state. The domain role maintains gamma_E(empty) outside
coordinate feedback. The true and possible roles accept signed assumption
corrections from the coupled scheduler. Complement is a set zero-crossing
operator owned by this component; it is not admitted as an ordinary recursive
antijoin because monotonicity holds only for the complete coupled operator.
Its derivative evaluates domain and possible changes simultaneously and emits
only net falsehood zero crossings; transient update order cannot manufacture a
false correction.
The gamma session boundary accepts record-native assumption deltas and returns
the exact settled output delta. Full-assumption revision is a compatibility
wrapper over this boundary. An inactive role consumes an explicit empty step at
the common epoch. This keeps tuple encoding and complete-extent construction out
of the coupled scheduler; it does not collapse gamma’s internal recursive
profile into coordinate authority.
Fresh construction and checkpoint recovery also retain sparse coordinate candidate profiles keyed by stable-revision round. The existing causal recursive distinct scheduler is the sole durable T/F representation; the former parallel coordinate trace and durable T/U pair are absent. T/U is a transient projection of scheduler truth, scheduler falsehood and the retained domain. Stable revision streams each exact desired candidate bucket to the scheduler, which subtracts the corresponding retained bucket and clears any obsolete retained tail before atomic publication. Desired and correction profiles are not materialized in parallel. This establishes the ownership and deletion boundary without making evaluation mutation-local: gamma still computes desired buckets from precision bottom. Direct signed gamma candidate corrections remain required so a mutation can avoid whole-component profile replacement.
The candidate boundary is the input support of each final semantic distinct,
not its settled sink delta. Acyclic circuit staging exposes that pre-distinct
profile together with the settled profile. Recursive staging exposes the causal
scheduler’s consolidated candidate journal together with its settled output.
This distinction is observable when one of two witnesses is removed: candidate
support changes by -1 while membership does not change. The coupled WFS driver
must consume candidate corrections; using only settled gamma deltas can retain
a nonleast self-supported fixed point after deletion.
Gamma revision therefore has one typed result containing both semantic candidate-support corrections and settled membership corrections. Component candidate relations are normalized to the gamma output identities; intermediate relations continue to flow only as settled membership. Direct output facts are candidate roots except where the recursive scheduler already owns that relation’s direct impulse. This prevents counting one direct fact through two physical owners.
A single mutable gamma state per role is insufficient for direct coupled
maintenance. Driving that state from the outer scheduler’s latest settled
correction degenerates into equation iteration around the previous fixpoint.
The six-edge Gray-code differential test reaches a two-state oscillation after
adding (1, 0): one truth atom and one falsehood atom alternate signed
admission forever. Increasing the limit from 32 to 256 does not converge. The
candidate boundary is correct; the missing state is gamma support indexed by
the WFS iteration whose candidate bucket it produced. A correction to bucket
k must re-evaluate the retained gamma profile at k, not the role’s final
assumption from the prior transaction.
The required logical time is therefore
(program frontier, WFS iteration, gamma recursion iteration). The latter two
coordinates are a nested product time within one atomic program transaction.
Flattening them into one scalar or cloning an entire gamma circuit per WFS
round is not the target architecture: the former obscures ordering and the
latter multiplies retained arrangements. Profile operators must become
parametric over an ordered iteration time, with ordinary recursion using
u32 and coupled gamma using an explicit product time. The coordinate
scheduler remains the sole T/F authority.
Product-time distinct cannot reuse a scalar prefix scan. For incomparable
times a and b, two candidate witnesses require settled corrections
a:+1, b:+1, and join(a,b):-1; otherwise integrating at the join reports
membership two instead of one. The implementation computes the finite
join-closure of touched times, thresholds causal support at each point, and
applies Möbius inversion over the induced partial order. Bilinear joins stamp
output with the componentwise lattice join, and recursive delay advances only
the gamma-inner coordinate.
Product-time antijoin uses the same join-closure and Möbius kernel. For each touched key, it integrates the left tuple support and right-key support at every causal time, selects the left support exactly where right support is zero, then differentiates that output lattice. An incomparable right blocker therefore does not suppress a left tuple until their join time. Retained left rows are key-indexed; left or right corrections visit only touched keys and never clone the complete retained relation. Negative causal support on either input is an invariant failure carrying the operator and product time.
Coordinate candidate history uses the recursive scheduler’s transaction
frontier and stable-revision round. Gamma history uses the common gamma epoch as
its outer time and positive-recursive iteration as its inner time.
Domain, true and possible roles publish the same final epoch; the domain role
advances through explicit empty steps when a revision round does not change its
assumption. Upper and lower gamma calls execute in distinct role states, so one
physical profile never mixes gamma(T) with gamma(U). This avoids a third
timestamp dimension: the enclosing program frontier controls atomic publication
while the globally ordered gamma epoch uniquely identifies coordinate work.
Gamma revision time is supplied by the coupled driver and each session refuses
anything other than its exact successor epoch; role-local clock inference cannot
silently desynchronize the coordinate circuit.
The scheduler is a differentiated least-fixed-point circuit, not equation iteration starting at the previously published pair. Each retained coordinate tuple carries causal support rooted in current base, domain and gamma deltas. Removing the last root retracts unsupported coordinate cycles. This history-independent support invariant is required because iterating the stable equations from an old fixed point after an arbitrary signed mutation can settle at a non-least fixed point.
Preparation stages the base correction into all three gamma roles, derives
domain and coordinate corrections, and alternates consolidated delta T and
delta F feedback until both nested-time frontiers are empty. It then derives
true and undefined output deltas, seals every gamma and coordinate journal, and
publishes records, inputs, coordinates and frontier atomically. Debug and test
builds independently evaluate from precision bottom and require exact (T,U)
equality after every mutation.
The role-separated product-time prototype is deliberately not production authority yet. Its acyclic component path supports ordered gamma strata, multiway joins, ordinary and correlated aggregates, and factorized aggregates through the same record-native temporal operator state used by ordinary incremental execution. Positive-recursive components reuse the record-native recursive SCC scheduler, preserve nested candidate and settled profiles, and publish through the same variant-safe component transaction. On the sampled 10,000-state, 100-edge exit mutation with ten samples, the established path measured 6.17 ms p50 and 6.94 MB retained heap. After assigning derivative authority exclusively to nonlinear product profiles, the product-time path measured 17.09 ms p50 and 7.17 MB retained heap. The authority correction removed 20,100 duplicate binding records and reduced the retained-memory ratio from 1.81x to 1.03x. At that revision, stable-equation iteration still materialized complete role outputs. The committed Criterion comparison over 10,000 retained self-loop states and one exit-edge insertion, with 20 samples, measured 4.136 ms for the established gamma circuit and 14.069 ms for the product-time gamma circuit: a 3.40x latency ratio. The later joint-reset result below supersedes this historical measurement. Neither result supports changing the production default. An attempted direct candidate-feedback cut failed the smallest WFS differential by oscillating to the iteration limit. That cut is rejected evidence that candidate corrections require the exact WFS-iteration-indexed support described above; passing memory gates alone does not admit the product path.
Signed candidate retractions cannot be placed mechanically in the bucket where their invalidation is discovered. A retained witness may have entered at a later WFS bucket; placing its retraction earlier makes the causal support prefix negative. Retractions are placed at the earliest bucket at or after discovery whose complete suffix has sufficient support. This placement is computed from the one retained candidate profile and does not introduce a second extent.
Coordinate and gamma candidate roots form one overdelete/rederive transaction. Resetting only the gamma assumptions can leave an obsolete coordinate witness; resetting only coordinates can allow gamma state to reintroduce an unsupported cycle. A signed mutation first overdeletes affected roots in both stores, settles their joint corrections, then rederives from surviving base roots. Role assumptions at publication must equal their coordinate inputs exactly; stable output equality alone is insufficient because it can persist a lagging assumption that fails on the next mutation.
The product prototype computes a tuple-local affected closure by probing both Boolean extremes of newly affected true and false coordinates. It clears only the selected coordinate candidate histories, leaves unrelated histories resident, then rederives Boolean membership inside the closed region. Selected candidate profiles use tuple-keyed trace reads; they do not materialize and filter the complete relation history. Raw proof multiplicity remains internal to gamma operators, and gamma delta calls construct membership changes only for touched records. Equivalent rule decompositions are therefore observationally identical at the outer coordinate boundary. Signed mutation, recursive, mixed-plan, Gray-code and conformance replay gates pass.
On the committed 10,000-state fixed-delta benchmark with 20 samples, this whole-component reset measured 14.341 ms against 4.146 ms for the established circuit, a 3.46x ratio. The prior product path measured 14.069 ms in the same harness. The 1.9% product regression is consistent with clearing all retained coordinate roots for a one-edge mutation. That result validated correctness, not replacement performance, and motivated the affected-region cut below.
After tuple-local closure, touched-output gamma deltas, selected complement projection and direct falsehood reads, the same benchmark measured 8.372 ms against 4.122 ms for the established circuit, a 2.03x ratio. This is a 41.6% reduction from the 14.341 ms whole-component reset and a 66.9% reduction from an intermediate 25.296 ms selective implementation that still materialized complete gamma outputs on every probe. Production selection remained unchanged because the replacement performance gate had not passed.
Positive rederivation expands the affected region without speculative two-extreme probes. A candidate outside the overdeleted region is suppressed when its published Boolean root is still resident; when no root was published, the candidate is admitted because it has no history requiring overdelete. This preserves the single Boolean-root representation and reduced the benchmark to 8.058 ms against 4.023 ms, a 2.00x ratio. The remaining difference is not attributed to complete-output reconstruction or component-wide reset.
The 10,000-state mutation matrix localizes the remaining cost. Empty frontiers measured 0.911 us for product and 0.935 us for established execution. A support- only duplicate input measured 2.178 us and 2.138 us respectively. The semantic one-edge mutation measured 7.930 ms and 3.992 ms. Product overhead is therefore confined to affected WFS maintenance; idle dispatch and non-boundary input maintenance are at parity.
Product gamma role publication uses one complete representation per role.
Published assumption, direct and derived extents are the only complete
authorities. A revision borrows those extents and records sparse absolute final
assignments. Reads consult the assignment first and the published extent
otherwise. Prepared publication contains only the assignment journals; after
frontier, role, component and record-transaction validation, commit applies
them without fallible work. Derived output membership remains a projection of
direct > 0 or derived > 0 and is never retained as another extent. Returning
a complete stable-revision result may materialize that projection transiently.
Dropping either a revision session or prepared publication cannot mutate
published state.
flowchart LR
Input[Signed base and assumption deltas] --> Eval[Product-time rule evaluation]
Published[Published role extents and operator state] --> Overlay[Read-only published plus sparse overlay]
Input --> Overlay
Overlay --> Eval
Eval --> RoleJournal[Sparse absolute role assignments]
Eval --> OperatorJournal[Sparse operator journals]
Eval --> MultiJoinJournal[Sparse multiway-join journals]
RoleJournal --> Validate[Frontier, role, component, support and record validation]
OperatorJournal --> Validate
MultiJoinJournal --> Validate
Validate --> Commit[Infallible atomic publication]
Commit --> Published
Published --> Rebase[Completed-epoch replacement builder]
OperatorJournal --> Rebase
MultiJoinJournal --> Rebase
Rebase -->|every completed epoch, touched identities only| Validate
The sparse role journal removes transaction-local clones of all nine role extents and makes cancellation canonical: a final weight equal to its published weight leaves no assignment. Relation identities are canonicalized before an assumption correction enters either the shadow input or its journal. The full reasoning suite measured 938 passing tests with one skipped, and strict clippy completed without warnings. On the same 10,000-state Criterion workload, the product path measured 8.117 ms in an adjacent run where the established path measured 4.124 ms, a 1.97x ratio. This result does not establish a latency improvement over the earlier 7.930 ms product measurement. Sampling attributes the dominant remaining time to product gamma assumption-delta staging and antijoin evaluation, not journal publication.
Operator publication subsequently adopted the same representation rule. Evaluation already produced a sparse validated operator journal, but finish cloned the complete operator state, applied that journal and compacted every temporal profile before every publication. Ordinary revisions now publish the journal directly. An intermediate implementation prepared a fully compacted replacement every thirty-second operator generation. Sparse completed-epoch closure described below supersedes that global replacement. The record-native antijoin window also projects retained profiles for touched keys directly instead of constructing and then rereading a temporary semantic antijoin state.
On the 10,000-state one-edge insertion, this reduced product time from 8.009 ms to 4.035 ms. The adjacent established measurement was 4.178 ms, making product 1.04x faster for that insertion. Retraction measured 3.705 ms product versus 3.380 ms established, making product 1.10x slower. Thirty-two alternating insertions and retractions, including periodic compactions, measured 131.11 ms product versus 118.36 ms established, a 1.11x total-time ratio. With the thirty-second-generation compaction interval, this became 126.28 ms product versus 117.74 ms established, a 1.07x total-time ratio. The established engine remains the default until broader mutation shapes pass their gates.
The standalone sustained-mutation probe uses the same fixture as the Criterion latency benchmark and reports allocator-retained, peak and percentile data. At 10,000 retained states and 1,024 alternating semantic mutations, established execution measured 3.895 ms p50, 5.386 ms p95, 5.555 ms p99 and 5.856 ms maximum, with 6.35 MB final retained heap and 10.36 MB mutation peak. Product execution measured 3.902 ms p50, 5.305 ms p95, 8.303 ms p99 and 9.053 ms maximum. Product is therefore 1.00x at p50, 0.99x at p95, 1.49x at p99 and 1.55x at the compaction maximum; it remains 1.04x in final retained memory and 1.65x in mutation peak. At this intermediate stage, retained-memory growth was bounded, but prepared compaction still required a complete replacement and remained the tail-latency and transient-memory target.
The same 1,024-mutation probe over 5,000 independent two-node negation cycles alternates an exit edge whose deletion must remove an unsupported coordinate cycle. After candidate-causal overdelete, established execution measured 3.879 ms p50, 4.095 ms p95, 5.316 ms p99 and 5.614 ms maximum. Product execution measured 3.978 ms p50, 5.417 ms p95, 8.281 ms p99 and 9.345 ms maximum. Product is 1.03x at p50, 1.32x at p95, 1.56x at p99 and 1.66x at the compaction maximum. Final retained and mutation peak ratios remain 1.04x and 1.65x. Unsupported-cycle correction is therefore near parity outside prepared compaction, with the same tail target as the self-loop workload.
A Boolean gamma output can remain present while its derivational support changes. This occurs when retracting an exit from a negation cycle: the obsolete coordinate assumption can immediately replace the removed base derivation, so settled gamma membership alone reports no boundary crossing. Overdelete now seeds the affected truth and falsehood regions from both settled membership changes and touched gamma candidates. Candidate touches also grow the region during the overdelete closure, allowing a support change hidden behind an alternative derivation to reach the coordinate cycle that depends on it. Candidate multiplicity remains internal to gamma; the coordinate scheduler still publishes one Boolean root. This removes unsupported cycles without introducing a second coordinate representation. An exhaustive differential over all 512 directed graphs on three nodes and every one of their nine possible single-edge toggles agrees with fresh well-founded evaluation.
Checkpoint payloads remain physical-engine independent. Restore now accepts an
explicit well-founded engine internally, reconstructs Product role and
coordinate state from semantic inputs and the (truth, possible) pair, and
requires that reconstruction to reproduce the checkpoint pair. A dedicated
restore-then-retract differential and forty alternating exit mutations spanning
repeated completed-epoch closures agree with fresh evaluation.
Checkpoint encoding, input-authority validation and gamma reconstruction are
owned by the well-founded checkpoint module. Mutation preparation remains in
the component orchestrator. Both modules extend the same component state; the
split introduces neither a checkpoint-side state copy nor an engine-specific
semantic representation.
Published membership queries, tuple projection and retained-state metrics are
owned by a read-model module over that same component state. Observation cannot
prepare, validate or commit a revision; mutation orchestration does not encode
the public true/undefined projection.
Prepared component variants, validation, sealing, transaction metrics and the
infallible validated commit are owned by a component-transaction module.
Evaluation produces that typed journal but cannot publish it directly;
checkpoint and read-model code cannot construct a validated commit. All three
modules borrow the same component state and introduce no parallel authority.
Product and Established well-founded evaluation are separate engine drivers.
Each driver owns its revision sessions and returns a validated evaluation
artifact containing the candidate semantic pair, prepared gamma state and
revision count. Engine dispatch, oracle comparison, output projection and
component-transaction assembly remain engine-neutral orchestration.
Semantic tuple, record-identity and encoded-catalog translation is isolated in
a stateless record-codec module shared by oracle auditing and checkpoint
recovery. The codec cannot inspect or mutate component, scheduler, engine or
frontier state; callers remain responsible for transactional record interning.
External support staging returns one of three typed input revisions: unchanged,
support-only or membership-changing. Only the membership-changing variant
carries a semantic gamma correction. Input staging validates tuple shape,
support non-negativity and record identity but cannot evaluate an engine or
publish assignments; the coordinator selects those later phases explicitly.
Fresh Established oracle preparation is isolated from both engine drivers. It
owns complete-base materialization, encoded-catalog evaluation and conversion
back to record coordinates, then returns an immutable base/pair observation.
Audit comparison and refusal remain in engine-neutral orchestration before
transaction sealing.
Checked record-extent algebra and public output projection are stateless
modules. Product’s sparse coordinate deltas and Established’s complete pair
difference converge on the same true/undefined sink representation. In audit
builds, sparse Product projection must equal complete pair differencing before
the coordinator can construct a component transaction.
The materialized-model relation-name view is the ordered union of base relation
names and circuit-produced relation names. It is derived from the authoritative
base store and component state, not a separately updated registry. Consequently
a head that is empty at construction and first becomes nonempty after a
mutation is visible to columnar projection immediately.
The 63-frontier Gray-code mutation differential now explicitly constructs the
Product engine. A mixed acyclic/positive-recursive, two-relation component also
produces the same terminal model when four signed changes are submitted in one
batch or in three different sequential orders. The full reasoning suite
measured 974 passing tests with one skipped, and strict clippy completed without
warnings.
MaintenanceMode::PreferCircuits and MaintenanceMode::RequireCircuits select
the qualified Product engine for admitted well-founded components.
MaintenanceMode::Established remains the process default and disables
circuits. MaintenanceMode::PreferEstablishedWfsCircuits and
MaintenanceMode::RequireEstablishedWfsCircuits retain all admitted
incremental operators while selecting Established well-founded evaluation as
an operational escape hatch. PreferUnauditedProductCircuits and
RequireUnauditedProductCircuits remain explicit route-pinning names for
qualification code. Mutation and restore-then-mutate differentials exercise
both engines through the query engine. Runtime circuit selection requires
OXC_ENABLE_INCREMENTAL_CIRCUITS; OXC_USE_ESTABLISHED_WFS_INCREMENTAL_CIRCUITS
then selects the Established well-founded escape hatch. Construction and
checkpoint recovery resolve the same maintenance policy.
OXC_ENABLE_AUDITED_PRODUCT_INCREMENTAL_CIRCUITS selects
MaintenanceMode::PreferAuditedProductCircuits when ordinary incremental
circuits are enabled. Audited Product computes the complete candidate pair and compares it with
fresh Established WFS evaluation before publication on every effective
mutation. A mismatch fails the transaction before circuit, record, frontier or
checkpoint state changes. Audit choice is not persisted, so the same checkpoint
restores under Product, audited Product or Established policy.
OXC_REQUIRE_UNAUDITED_PRODUCT_INCREMENTAL_CIRCUITS and
OXC_REQUIRE_AUDITED_PRODUCT_INCREMENTAL_CIRCUITS each imply circuit and their
named Product policy, and convert any admission fallback into an error. Product
integration and canary gates use these fail-closed selectors so Established
fallback cannot produce a false pass. When both Product enable flags or both
Product require flags are set, the audited policy takes precedence.
For non-required modes, the Established escape-hatch flag overrides both
Product enable flags. Product-specific require flags override the escape hatch,
so a fail-closed qualification job cannot silently test Established instead.
flowchart TD
F[Runtime maintenance flags] --> R{Circuits required?}
R -->|Product-specific require| RP[Required Product policy]
R -->|ordinary require plus escape| RE[Required circuits with Established WFS]
R -->|ordinary require| RU[Required circuits with Product WFS]
R -->|no| I{Circuits enabled?}
I -->|no| D[Established whole-program maintainer]
I -->|yes, escape| PE[Preferred circuits with Established WFS]
I -->|yes, audited| PA[Preferred circuits with audited Product WFS]
I -->|yes| PU[Preferred circuits with Product WFS]
RE --> C[Shared circuit compiler and non-WFS operators]
RU --> C
PE --> C
PA --> C
PU --> C
Runtime discovery first captures these values in a named flag record, then
converts that record to one maintenance mode. No positional Boolean API exists,
so adding or reordering a selector cannot exchange audited and unaudited policy
without a field-name change. Production maintainer coverage verifies that raw,
audited and Established policies survive full rebuild; raw and audited policies
also restore from the same engine-neutral checkpoint and retain their selected
engine across subsequent mutations.
The internal engine discriminator uses the same explicit names:
Established, UnauditedProduct, and AuditedProduct. A bare Product engine
state cannot conceal whether an independent publication oracle is active.
Live engine state represents audit policy inside the Product rule-state variant;
Established state cannot carry Product audit policy, and no parallel boolean can
drift from the selected physical engine.
The default-routing benchmark uses one exit assertion against 10,000 retained
well-founded rows and 10 measured mutations. Product p50 is 49,583 nanoseconds,
versus 4,214,542 nanoseconds for the Established-WFS circuit and 37,685,791
nanoseconds for the whole-program Established maintainer: 85.00 and 760.05
times faster, respectively. Product retained heap is 4,581,046 bytes versus
5,046,722 for the Established-WFS circuit. Its 22,847,444-byte construction
peak remains 2.31 times the whole-program Established peak; construction cost
remains a separate optimization target.
A scoped divergence injection fires after Product preparation and before
validation. The audited mutation is refused while the program frontier, record
arena metrics, derived output and checkpoint bytes remain identical to their
pre-mutation values, directly gating the rollback boundary.
Defeasibility elaborated into ordinary strict support, blocking and public-head
rules requires no defeasibility-specific incremental operator. Its positive and
negative dependencies enter the same component planner, stratifier and
well-founded circuit as handwritten strict rules. Artifacts that retain
executable defeasibility metadata remain outside Product admission and use the
established compatibility path. Model maintenance does not imply explanation
or proof-tag parity; provenance remains a separate publication contract.
A well-founded SCC may contain outputs that participate only in
positive recursion while another output is read under in-SCC negation. Gamma
assumptions are supplied only for relations whose rewritten rules actually read
an $assumed:: shadow. Gamma construction records that output-to-shadow map
once and refuses a rewritten read without a corresponding physical input.
Product therefore ignores assumption corrections for a positive-only SCC
output instead of requiring a nonexistent shadow input. A
direct insert/retract/reinsert differential and the compiled-defeasibility
runtime suite pin this mixed SCC shape against fresh Established evaluation.
The runtime proof-tag reader consumes only the inert compilation carrier. It
computes a strict-only least fixed point by excluding default-support producers:
surviving tuples in that fixed point are +Δ; other surviving compiled
defeat conclusions are +∂. This preserves partial provenance through
strict recursion instead of treating a populated strict support relation as a
definite proof. For an absent public tuple, a populated default-support relation
identifies defeated-default cause C6 and −∂. Evaluation and incremental
maintenance never consult this metadata, so explanation cannot alter circuit
admission, state or publication.
An end-to-end compiled-artifact differential exercises a recursive defeat
target whose attacker reads that target. Audited Product remains on the
recursive circuit while a Gray-cycle history visits all four
eligibility/exclusion base states, including exclusion without eligibility, in
both insertion and retraction directions. The public coordinate traverses
unblocked, undefined, reinstated and removed states. Each effective WFS mutation
is compared with Established evaluation before publication, and a fresh-store
assertion separately gates the initially-empty public projection.
The artifact carries both emitted events and non-executable defeat-compilation
provenance through binary encoding and runtime loading; the test rejects either
legacy executable defeat metadata or missing compiled provenance. A separate
three-subject mutation matrix retains simultaneous true, undefined and absent
states. Mutating one subject preserves the other subjects’ public coordinates
while every effective mutation remains audited against Established evaluation.
A second compiled-artifact scenario covers an acyclic exception-to-exception:
a default attacker blocks a default target, a strict rule defeats that attacker,
and retraction reinstates the attacker. The complete mutation cycle stays on
the acyclic circuit and pins its two-valued semantics separately from recursive
well-founded undefinedness.
The corresponding emitted-rule benchmark retains 10,000 eligible subjects and
alternates one exclusion for 128 mutations. Established measured 33.470 ms p50;
Product measured 0.296 ms p50, a 113.0-fold improvement. Product construction
peak was 72.26 MB versus 54.81 MB, 1.32 times Established. Final retained heap
was 29.09 MB versus 20.51 MB, 1.42 times Established. Product mutation peak was
29.22 MB versus 30.23 MB Established. The result isolates steady mutation
benefit from the explicit cost of retaining derivative state.
A post-modularization rerun with the same 10,000-subject, 128-mutation workload
measured 0.284 ms Product versus 34.333 ms Established at p50, a 121.0-fold
improvement. Product construction peak remained 72.26 MB, final retained heap
29.09 MB and mutation peak 29.22 MB. The transaction, engine-driver, input,
oracle, codec and projection boundaries therefore introduced no measured hot-
path or retained-state regression.
Benchmark-only logical-state telemetry attributes the retained difference. Both
engines retain 70,000 profiled rows, 30,000 temporal-trace entries, 20,000
coordinate candidates and the same 10,000 value records. Product additionally
retains 40,000 gamma-assumption rows and 60,000 gamma-derived rows; direct and
output rows are zero. These 100,000 record-keyed Boolean summaries account for
the 8.58 MB heap difference. They are required incremental read state. The
initial published representation carried general signed Z-set weights
despite a validated set invariant, identifying a representation mismatch.
Published Product gamma assumption, direct and derived summaries now use
relation-indexed record sets. Signed weights exist only in the prepared journal;
validation restricts terminal assignments to zero or one before infallible set
publication. Domain publication remains a distinct weighted-extent patch and
does not share the summary journal. On the same compiled-defeat workload,
Product final retained heap fell from 29.09 MB to 27.62 MB, reducing the ratio
to Established from 1.42 to 1.35. Product p50 fell from 0.280 ms to 0.212 ms;
the stronger published representation therefore reduced both memory and lookup
cost without changing logical row counts.
The same compiled-artifact scenario checkpoints the undefined state, restores
the Product circuit from the durable semantic payload, then removes and
reasserts the exclusion. The restored route remains recursive and both
post-restore frontiers pass the Established audit. Recovery comparison treats
an empty relation entry and its canonical absence as the same semantic extent;
it still compares every populated relation plus the shared translation,
world-assumption and metric-resolution frame exactly.
A two-module differential assembles the artifact through workspace symbol
collection and the combined defeat-plane pass. The attacker imports and reads a
target in another module; qualified eligibility and exclusion mutations still
traverse true, undefined and reinstated target states on audited Product. This
gates qualified internal relation identity across elaboration, planning,
inter-component flow and runtime publication without a cross-module circuit
special case.
The end-to-end wfs_recursion conformance ontology passes through the compiled
CLI with both runtime flags enabled: its two language-level assertions pass and
its twelve-mutation scenario produces exactly the two declared winning
positions. The generated reasoning conformance replay also passes every
supported vector and retract/reassert mutation against the established engine.
Completed-epoch rebase now publishes profile state and multiway-join state as one validated transaction. Previously, periodic profile compaction left multiway-join temporal tries unbounded. Rebase integrates every terminal’s closed history into at most one cell at the next epoch frontier, preserves the semantic or interned trie representation, and refuses overflow or negative support before publication. This operation is intentionally not exposed as generic product-lattice compaction: inner coordinates from an earlier outer epoch are incomparable with the next outer epoch until the earlier epoch is closed. A product-time multiway-join test verifies that three retained cells collapse to one without changing integrated support.
The completed-epoch builder traverses prepared trace levels directly and merges
sparse absolute assignments with immutable published profiles. It does not
clone a complete RecordWfsGammaCircuitState. A differential covering
operators, joins, antijoins, distinct, count and factorized aggregate state,
including cancellation and untouched keys, matches the former
clone-then-compact implementation.
After this change, the 10,000-state, 1,024-mutation self-loop probe measured 3.823 ms established versus 3.880 ms product at p50, 4.009 ms versus 4.128 ms at p95, 4.142 ms versus 6.792 ms at p99, and 4.496 ms versus 6.935 ms maximum. Final retained heap remained 6.35 MB established versus 6.59 MB product. Mutation peak fell from 17.09 MB before the direct builder to 12.46 MB, or 1.20x the 10.36 MB established peak instead of 1.65x. The two-cycle workload measured 3.774 ms versus 3.921 ms at p50, 4.046 ms versus 4.163 ms at p95, 4.127 ms versus 6.908 ms at p99 and 4.373 ms versus 7.105 ms maximum, with the same 1.20x peak-memory ratio. These measurements preceded sparse completed-epoch closure.
The next compaction form is sparse completed-epoch closure. For a logical
identity x changed in a closed outer epoch e, let H_x contain its retained
cells and committed correction. Closure replaces H_x with
((e + 1, 0), sum(H_x)), deleting the identity when the sum is zero. The
completed-epoch contract excludes later input at an outer coordinate less than
or equal to e; therefore (e + 1, 0) is less than or equal to every future
evaluation time and all future reads observe the same integrated weight. An
identity untouched in epoch e was last closed at an earlier (k + 1, 0),
which is also less than or equal to every future time, so it does not require
restamping. Bilinear operators have emitted the closed epoch’s corrections
before their retained arrangements are rewritten.
Closure granularity is the retained logical identity: operator row, arranged
key and tuple, antijoin support key, distinct row, aggregate group,
or multiway-join atom key. The current aggregate journal closes the complete
touched group; subprofile-granular aggregate journals remain a scaling
refinement. Preparation visits only identities named by the
sparse journal, performs checked summation and emits absolute deletions plus at
most one frontier assignment. Published state remains the sole complete
authority; commit remains an infallible journal application. This changes
periodic O(S + H) time and O(S) transient space into sparse journal work.
Each immutable trace batch is a packed ordered page tree with 256-entry leaves
and fanout-32 branches. Closure seek-scans selected keys, path-copies only
intersecting leaves and their ancestors, and shares disjoint subtrees by
identity. A 100,000-key test closing one identity copies at most 512 entries and
16 nodes while sharing more than 300 unrelated nodes. Keys spanning leaves and
multi-value keys retain ordered semantics. This is not a lazy global frontier:
no hidden normalization metadata enters reads, checkpoints or timestamp
comparison.
The implementation applies this closure to operator rows, join-side key/tuple identities, antijoin support keys, distinct rows, count and factorized-aggregate groups, and semantic or interned multiway-join atom keys. Ordered multiway-join rounds close against their evolving prepared overlay, so repeated changes to one key retain correct support and live-key metadata without materializing a complete trie. The production transaction now has one representation: sparse profile journals plus sparse multiway-join journals. The complete rebase exists only as a differential test oracle. Every Product stage must return exactly one journal for every admitted multiway-join node. Validation rejects missing, extra, wrong-arity or state-incompatible journals before profile preparation, and repeats the same exact-set check when sealing the transaction. This invariant is active in raw Product builds; it does not depend on the test-only semantic shadow. Fault injection removes one journal and proves rejection before publication followed by a successful identical retry. The retained admission evidence also owns the exact physical node set for binary joins, scalar and correlated aggregates, and factorized aggregates. These kernels always produce a journal, including an empty correction, so raw Product rejects a missing or extra family journal before preparing retained state. Fault injection covers each family and a valid identical retry. Antijoin, semijoin and distinct journals remain sparse by contract: they are absent when neither input contributes a correction, and every present journal is still validated by retained-state preparation. Their backend contract returns one typed result containing output plus an explicit optional retained correction. Shared evaluation owns journal-map insertion for semantic, record-backed ordinary and Product modes. Missing map entries are therefore a represented no-correction outcome rather than an implicit backend side effect. Binary join uses the corresponding mandatory-journal result: every backend returns output and its complete bilateral arrangement correction as one value, and shared evaluation inserts it exactly once. Product’s admitted-node check is therefore a defensive validation of a structurally total kernel result rather than the mechanism that couples output to retained state. Scalar, correlated-count and factorized aggregate kernels use the same mandatory-journal result. Output and the complete touched-group correction cannot be returned independently, and shared evaluation is the only journal map writer. All total profile-state families therefore have one ownership model across ordinary and Product logical time.
With sparse closure, the 10,000-state, 1,024-mutation self-loop probe measured 3.724 ms established versus 3.373 ms product at p50, 4.684 ms versus 4.657 ms at p95, 5.200 ms versus 4.798 ms at p99, and 5.379 ms versus 4.967 ms maximum. Product final retained heap was 6.59 MB versus 6.35 MB established, while mutation peak was 10.36 MB for both engines: 1.04x retained and approximately 1.00x peak. The two-cycle workload measured 3.829 ms versus 3.834 ms at p50, 4.037 ms versus 3.968 ms at p95, 4.122 ms versus 4.033 ms at p99, and 4.970 ms versus 4.420 ms maximum. Its Product mutation peak was 10.84 MB versus 10.37 MB, a 1.05x ratio. The periodic tail and its 1.65x peak-memory regression are absent in these sustained runs.
Fixed-delta scaling is not yet achieved. With 128 mutations of one self-loop, 1,000 retained states measured 0.402 ms established and 0.332 ms product at p50, while 50,000 retained states measured 21.17 ms and 22.27 ms. The Product path therefore remains approximately linear in retained state despite sparse operator publication. Inspection identifies complete coordinate/domain work: ordinary mutation projects the full truth/possible pair and falsehood, duplicates complete gamma outputs and assumptions, constructs a complete next pair, performs complete-state equality checks, and differences complete old and new outputs.
The delta-native coordinate design keeps published domain plus scheduler truth
and falsehood as the sole semantic authorities. A mutation returns sparse
domain, truth and falsehood corrections. Truth output is the truth correction;
undefined output is computed only over records touched by any of the three
corrections using D and not T and not F before and after the overlaid update.
Gamma assumptions and outputs use read overlays for affected records. Complete
pair projection remains available for checkpoints and explicit oracle
validation, but is not part of ordinary Product publication. Production-local
validation checks set weights, disjoint truth/falsehood, coordinate containment
in domain, and gamma agreement over touched and affected records.
Affected truth and falsehood selections are owned by one typed region value.
Discovery may grow either coordinate explicitly; final publication consumes the
mutable region and produces a certified region only after every sparse truth and
falsehood correction is contained in its corresponding selection. Subsequent
gamma/coordinate agreement checks accept only that certified value. This makes
coordinate swapping and unchecked exterior publication structurally difficult,
and mirrors Lean’s paired PositiveRegion. The certificate proves sparse-write
containment; it does not by itself prove prior/new global exterior agreement or
that the runtime worklist computes the regional least fixed point.
Audited Product additionally derives prior and Established-target falsehood from
their domains and possible coordinates, then rejects any truth or falsehood
change outside the certified region before the existing complete-pair equality
gate. This directly exercises the first premise of the Lean affected-region
theorem during canary execution without adding a complete scan to ordinary
Product.
The first delta-native publication slice is complete. Product domain state now publishes checked absolute assignments while Established uses an explicit replacement variant. Initial Product construction and checkpoint reconstruction publish their complete domain as the same checked assignment form. Non-owning extent overlays provide checked point membership and selected-record projection for domain and coordinate reads. Scheduler truth and falsehood point APIs read the retained coordinate authority directly. Ordinary Product sink projection uses sparse simultaneous domain/truth/falsehood corrections and is differentially checked against complete pair differencing. The complete pair is still materialized inside the differentiated driver at this intermediate stage. The reasoning suite measured 980 passing tests with one skipped after these changes.
Coordinate revision now retains four transaction-local Boolean views as sparse absolute assignments over scheduler truth, scheduler falsehood and derived possible reads. Fixed-point rounds validate a complete incoming correction before applying only its touched assignments; they do not clone assignments accumulated by earlier rounds. Sparse set algebra and validation are isolated from driver orchestration. Production agreement checks visit only the affected truth or falsehood region.
On the 128-mutation fixed-delta probe, 1,000 retained self-loops measured 0.398 ms Established versus 0.285 ms Product at p50. At 50,000 retained self-loops they measured 20.65 ms versus 20.76 ms. Product mutation peak was 47.89 MB versus 50.62 MB Established at 50,000 states; final retained heap was 31.95 MB versus 30.74 MB. The local overlay work therefore does not add a retained-state scan, but the approximately 73-fold Product latency increase for a 50-fold state increase confirms that complete pair projection and final pair materialization still dominate fixed-delta scaling.
The completed delta-native cut removes those traversals. Ordinary Product
revision reads scheduler truth and falsehood by record, derives possible as
domain - falsehood, retains only affected-region rederivation, validates the
prepared scheduler’s sparse truth and falsehood corrections, and projects sink
changes from the simultaneous sparse domain/truth/falsehood transition. The
prepared component no longer retains an unused pair. Complete pair projection
remains only for initial construction, checkpoint observation and explicit
debug oracles. Tests assert that an ordinary Product mutation does not create
one.
Domain revision follows the same rule. Product gamma returns a sparse settled domain correction; the driver reads it through a checked published-plus-delta view, and publication validates and commits sparse absolute assignments. A complete gamma base is built only for Established execution, initial Product construction or an enabled debug oracle. The Boolean read authority, sparse coordinate algebra and driver orchestration are separate modules.
On the same 128-mutation probe after this cut, 1,000 retained self-loops measured 0.401 ms Established versus 0.052 ms Product at p50. At 50,000 retained self-loops they measured 19.30 ms versus 0.117 ms. Product therefore improved 7.7 times and 164 times respectively. Its p50 grew 2.26 times across a 50-fold retained-state increase, rather than approximately linearly. At 50,000 states, Product mutation peak was 33.07 MB versus 50.62 MB Established; final retained heap remained 31.95 MB versus 30.74 MB. A 10,000-node two-cycle correction measured 0.089 ms Product versus 3.628 ms Established, a 41.0-fold improvement. The complete reasoning library reports 932 passing tests with one skipped, and strict all-target Clippy reports no warnings. The end-to-end conformance corpus passes with both incremental-circuit and Product-circuit runtime flags enabled.
A dedicated aggregate probe validates every insert/retract cycle against fresh Established evaluation before timing one changed value in one retained hot group. An unprojected cardinality control with 10,000 values and 128 alternating mutations measured 0.397 ms Product versus 2.929 ms Established at p50; factorized Count measured 0.401 ms versus 3.104 ms. Product retained memory was at parity and mutation peak was 0.62 times Established for both shapes. The unprojected Product control measured 0.189 ms at 1,000 values and 1.222 ms at 50,000 values, while Established measured 0.305 ms and 16.64 ms.
The actual hot-subprofile workload uses projected Sum, forcing the retained group to contain one value profile per input. At 1,000 values, Product measured 11.24 ms versus 5.85 ms Established; at 10,000 values it measured 113.22 ms versus 61.53 ms. Product is 1.84 times slower and scales linearly with group width. Count publication now carries and closes only correction-named input, value and outer subprofiles, but the 50,000-value unprojected control remained 1.217 ms after that change versus 1.222 ms before it. Publication is therefore not the dominant term. Subprofile evaluation and an incrementally maintained aggregate summary are required to remove whole-group work.
After replacing projected Sum value histories with temporal projected-count and exact-sum profiles, the 10,000-value, 16-mutation workload measured 0.350 ms Product versus 2.945 ms Established at p50: Product is 8.42 times faster rather than 1.84 times slower. Product mutation peak was 3.15 MB versus 5.05 MB, while final retained heap was 2.95 MB for both implementations. Product construction peak remained higher at 22.13 MB versus 18.30 MB. The mutation result establishes constant-width scalar-fold work for Sum; it does not cover the pending indexed CountDistinct, Min or Max representation.
Dedicated nonlinear controls use the same 10,000-value, 16-mutation hot group and verify every insert/retract cycle against fresh evaluation. CountDistinct measured 16.03 ms Product versus 12.65 ms Established at p50. Min measured 112.64 ms versus 62.60 ms, and Max measured 113.24 ms versus 59.75 ms. Product is respectively 1.27, 1.80 and 1.90 times slower. These controls pin the remaining whole-value-map scan and provide the acceptance baseline for the ordered indexes below.
After adding a typed CountDistinct fold with authoritative support leaves and a derived temporal presence-count profile, the same CountDistinct workload measured 0.341 ms Product versus 2.787 ms Established at p50: Product is 8.18 times faster. Product mutation peak was 6.17 MB versus 8.07 MB and final retained heap remained at parity, 5.86 MB versus 5.87 MB. The record-backed path resolves only correction-named leaves; resolving the complete retained value map would leave mutation time linear despite the scalar root summary.
Aggregate state is specialized by algebra rather than forcing every aggregate
through a complete value multiset scan. Count retains only its temporal row
cardinality. Sum and Avg retain temporal projected cardinality and exact sum;
these are homomorphic folds over signed input corrections. CountDistinct keeps
one support trace per value in an ordered map and places the nonlinear
support > 0 boundary at the leaf before summing leaf-presence profiles into a
temporal root count. Min and Max are not invertible
group folds: they keep ordered value-support leaves and use a persistent
augmented tree to derive the temporal winner after retraction. Equal numeric
values remain separate semantic value leaves, preserving value identity.
flowchart LR
Delta[Touched aggregate corrections] --> Kind{Aggregate algebra}
Kind -->|Count| Cardinality[Temporal cardinality]
Kind -->|Sum or Avg| Linear[Temporal projected count and exact sum]
Kind -->|CountDistinct| DistinctLeaf[Value support leaf]
Kind -->|Min or Max| ExtremaLeaf[Ordered numeric support leaf]
DistinctLeaf --> DistinctRoot[Temporal presence-count root]
ExtremaLeaf --> ValueTree[Path-copied augmented value tree]
DistinctLeaf --> DistinctPatch[Validated touched-value assignments]
ExtremaLeaf --> ExtremaPatch[Correction-named tree paths]
Cardinality --> Result[Root result profile]
Linear --> Result
DistinctRoot --> Result
ValueTree --> Result
Result --> Mobius[Canonical old/new Möbius correction]
Mobius --> Output[Aggregate output delta]
Delta --> Journal[Sparse absolute subprofile or root journal]
DistinctPatch --> Journal
ExtremaPatch --> Journal
Journal --> Validate[Complete validation before publication]
Validate --> Commit[Infallible atomic commit]
Support leaves or scalar fold profiles are the semantic authority. Internal tree metadata is a deterministic function of children and is neither journaled nor serialized. Checkpoints encode scalar profiles or canonical ordered value support leaves and rebuild metadata. CountDistinct computes a presence-profile correction from only the old and new touched leaf and applies it to the derived root count. A touched extrema leaf path-copies only its search path and recomputes ancestors using the existing lattice join-closure and Möbius operators. Count/Sum/Avg target work proportional to correction cells plus affected output outers; CountDistinct/Min/Max add logarithmic value-index work. Enumerating every affected outer remains necessary because each is an observable output.
The indexed 10,000-value, 16-mutation controls measured 0.403 ms Product versus
3.115 ms Established for Min and 0.393 ms versus 3.027 ms for Max at p50. Product
is respectively 7.73 and 7.71 times faster. Final retained heap was 9.96 MB for
both implementations. Product mutation peak was 10.27 MB versus 12.17 MB for
Established. Product construction peak remained higher at 26.77 MB versus
22.95 MB. Common integral extrema keys use an inline i64; non-integral and
out-of-range keys retain exact rational ordering. Tree nodes share keys and
unchanged subtrees through reference-counted immutable paths. This removes the
previous retained-state premium without weakening exact numeric semantics.
A 2026-07-23 current-head acyclic projected-Sum control retained 10,000 values, retracted 100 values per mutation, and sampled 100 target operations. Circuit p50 was 1.076 ms versus 283.431 ms Established, a 263.5-fold speedup. Circuit retained heap was 1.389 MB versus 1.601 MB, and mutation peak was 4.593 MB versus 5.806 MB. Circuit construction peak remained higher at 10.346 MB versus 5.002 MB. The result confirms the optimized aggregate mutation path after integration with the current base; the 2.07-fold construction peak remains a routing gate. A phase-attributed rerun localized the 10.347 MB peak to initial record-join preparation. Heap remained near 9.0 MB through profile-state commit and fell to 4.205 MB when the prepared overlay released, before reaching 1.391 MB retained. The remaining construction premium is transient ownership overlap at the record-join/profile publication boundary rather than a second retained aggregate authority. Initial publication, record interning, checkpoint restoration and complete epoch rebasing build a balanced tree directly from canonical key order. Point mutations alone use path-copy insertion. Bulk construction removes transient persistent paths but does not remove the measured construction-peak premium; allocation-phase attribution remains required for that peak.
Production-gate rerun and remaining factorized fold
A 2026-07-21 optimized rerun used 10,000 retained values or states and 128 alternating mutations. Every benchmark asserts the selected circuit route and validates each mutation cycle against fresh established evaluation.
| Workload | Product/circuit p50 | Established p50 | Speedup | Product retained / established | Product mutation peak / established |
|---|---|---|---|---|---|
| WFS independent self-loops | 0.068 ms | 3.749 ms | 54.8x | 1.04x | 0.66x |
| WFS independent two-cycles | 0.099 ms | 3.937 ms | 40.0x | 1.04x | 0.66x |
| Projected Sum | 0.391 ms | 2.794 ms | 7.15x | 1.00x | 0.62x |
| Projected CountDistinct | 0.394 ms | 2.774 ms | 7.05x | 1.00x | 0.76x |
| Projected Min | 0.434 ms | 2.807 ms | 6.47x | 1.00x | 0.84x |
| Projected Max | 0.443 ms | 2.787 ms | 6.29x | 1.00x | 0.84x |
| Factorized projected Sum | 0.406 ms | 2.755 ms | 6.79x | 0.99x | 0.62x |
| Factorized projected CountDistinct | 0.400 ms | 2.776 ms | 6.94x | 1.00x | 0.76x |
| Factorized projected Min | 0.553 ms | 3.496 ms | 6.32x | 1.00x | 0.85x |
| Factorized projected Max | 0.477 ms | 3.439 ms | 7.21x | 1.00x | 0.85x |
After separating count change derivation, fold maintenance and output differentiation, the same Projected Sum shape measured 0.396 ms Product versus 2.833 ms Established at p50, preserving the 7.15x speedup. Product retained heap was 0.998x, mutation peak was 0.407x and construction peak was 0.945x Established. The module boundaries therefore introduced no measured latency or memory regression.
An ordinary recursive upper-stratum retraction of 100 facts measured 0.504 ms for the circuit and 10.434 ms for established maintenance, a 20.7x speedup. Its retained heap ratio was 1.35x; construction peak was 3.64x and mutation peak was 0.95x. The WFS Product controls had a 1.02x construction-peak ratio.
The initial factorized result identified a complete-value-map scan. Live tagged
factor projection state now contains only None, Linear, Distinct, and
Extrema. The checkpoint DTO retains generic legacy leaves solely for decoding
and canonical reconstruction.
Factorized Sum and Avg retain temporal projected count plus exact sum and the
factor product consumes that scalar result. A 10,000-value rerun reduced Product
p50 from 59.072 ms to 0.406 ms while established maintenance measured 2.755 ms.
Product retained heap was 0.99x, mutation peak was 0.62x, and construction peak
was 1.21x established. Nonlinear factor projections retain authoritative leaves;
they do not coexist with a scalar fold.
Factorized CountDistinct reuses the ordinary temporal presence fold. Each touched value computes one zero-crossing correction against retained support; the factor output reads the resulting scalar presence profile and does not scan retained values. Checkpoints encode the authoritative support leaves and rebuild the presence profile from the immutable aggregate kind. Record evaluation resolves only values named by the correction. At 10,000 values and 128 alternating mutations, the first indexed implementation measured 1.802 ms p50 against 3.061 ms established, a 1.70x speedup. Atomic publication still cloned the retained record-key map before applying one leaf patch. Publication now prepares absolute assignments only for correction-named leaves, validates them without mutating published state, and installs the sparse patch during the infallible commit phase. Epoch closure rebases only those assignments. The same workload then measured 0.400 ms Product against 2.776 ms established, a 6.94x speedup. Product retained memory was 0.997 times established, mutation peak was 0.764 times established, and construction peak was 1.204 times established.
Factorized Min and Max reuse the ordinary persistent temporal extrema index. Canonical projections contain a path-copied augmented tree; signed WFS coordinates retain an explicit delta until they combine with canonical state. The record-backed evaluator interns only correction-named values and resolves only temporal winners for output. It does not convert the retained record-key index to a semantic value map. Prepared epoch assignments carry the extrema keys named by the correction, so frontier closure rebases only those paths. Tree nodes retain a derived subtree cell count, allowing transaction metrics to observe retained size without enumerating support leaves. The 10,000-value, 128-mutation controls above validate every insertion and retraction against fresh established evaluation. Product retained memory was 0.998 times established, mutation peak was 0.846 times established, and construction peak was 1.149 times established for both orientations.
Checkpoint payload version 14 introduces the tagged factor-projection field.
Versions 12 and 13 retain the factor value map as a frozen decode-only field.
Restoration uses immutable plan metadata to migrate Sum and Avg maps to
Linear, CountDistinct maps to Distinct, Min and Max maps to Extrema, and
non-value factors to None before validation or publication. Version 14 always
emits the frozen field empty. Projection variants are mutually exclusive by
construction in semantic state, record state, epoch rebasing, and checkpoint
restoration.
Checkpoint envelope version 15 introduced source-bound physical-plan identity. Version 16 additionally commits each operator’s local identity stratum separately from its global scheduling stratum. The circuit operator schema remains version 13, so module, relation and node identities remain stable. Restore accepts envelope versions 12 through 14 by recomputing their canonical version-2 plan identity and version 15 by recomputing its source-bound version-3 identity. It validates the unchanged operator graph and state, then re-emits version 16. This preserves existing checkpoints, prevents physical components from detaching from their exact lowered rules, and makes schedule rebasing explicit rather than an implicit identity exception.
Removing the generic live leaf variant did not regress the indexed paths. A post-change 10,000-value, 128-mutation run measured Product versus Established p50 at 0.412 versus 2.838 ms for factorized Sum, 0.421 versus 2.872 ms for CountDistinct, 0.444 versus 2.927 ms for Min, and 0.440 versus 2.871 ms for Max. Product final retained-memory ratios were 0.995, 0.997, 0.998 and 0.998; mutation-peak ratios were 0.623, 0.764, 0.846 and 0.846. Construction-peak ratios remained 1.210, 1.204, 1.149 and 1.149 respectively.
Phase-attributed heap probes locate the premium in initial seed application. At 10,000 values, seed application peaked at 25.09 MB Product versus 21.25 MB Established; plan construction used 21.7 KB in both paths and instance construction used 37.0 KB versus 41.9 KB. At 1,000 values the seed-application gap was 0.383 MB, confirming linear transient cost of about 383 bytes per seeded value. Retained state remained at parity. The remaining source is inside seed evaluation or publication rather than plan or instance construction.
Fine-grained preparation boundaries narrow this further. Before record-native
extrema evaluation begins, the 10,000-value Product path holds 19.94 MB versus
16.10 MB Established: the complete 3.83 MB premium is already present. Extrema
change validation then adds approximately 4.65 MB in both paths. The remaining
construction premium is therefore upstream product-time scan, join or recursive
preparation state, not the extrema index or its semantic-to-record conversion.
The aggregate benchmark exposes these boundaries through
OXC_AGGREGATE_PREPARATION_PHASES=1.
Embedded Product corrections now intern impulse tuples at classification and
carry RecordId profiles through recursive preparation; direct semantic and
interned assignment deltas share one validation kernel. This removes a second
semantic tuple authority but leaves the 10,000-value construction peak
unchanged at 27.04 MB. Raw input-tuple duplication is therefore not the peak
source. Derived binding, join or recursive preparation profiles remain the
linear transient candidates.
Initial Product observation previously cloned the complete settled domain only
to compute possible = domain - falsehood, while retaining the same domain
delta for publication. It now projects that difference through a checked
published-plus-delta view and constructs only the required possible extent.
The 10,000-value factorized-Min construction peak remained 29.37 MB versus
25.55 MB Established. The clone was a duplicate authority but was allocated
after the earlier preparation peak; removing it narrows the remaining source
without changing the measured maximum.
Product revision construction also cloned the immutable base batch into the domain, possible and truth role sessions before executing any role. Sessions now borrow one base authority. At 10,000 values, revision-session current heap fell from 9.82 MB to 4.07 MB. Initially creating a mutable shadow batch while each role executed lowered the domain-role peak from 26.72 MB to 22.89 MB but left the overall peak unchanged. Empty assumption deltas now evaluate the borrowed base directly; a mutable copy is created only when shadow-assumption facts must be appended. Domain, possible and truth role peaks consequently fell to 20.97, 23.22 and 25.48 MB. The complete factorized-Min construction peak fell from 29.37 MB to 27.45 MB, 1.074 times the 25.55 MB Established peak. Remaining overhead is accumulated staged derivative state retained for atomic three-role commit, not input-batch ownership.
This representation advances the checkpoint payload to version 13. Version 12 stores aggregate input, value and outer histories without aggregate-kind metadata; Sum and Avg therefore depend on the complete value map for recovery. The version-12 DTO remains frozen and decodable. Restore binds it to the live physical plan and structurally validates the old aggregate indexes. A delegated profiled checkpoint may omit materialized operator rows, so version-12 Sum/Avg value histories are folded once into exact scalar timelines during restore and then discarded. Version 13 always emits a tagged fold payload and rejects a payload variant inconsistent with the plan. Versions older than 12 remain rejected. Migration is canonical validation and reconstruction before publication; a failure cannot partially install state.
Generated aggregate mutation streams compare all six admitted numeric aggregate kinds with the fresh fold oracle after every simultaneous and partitioned batch, including incomparable ProductTime cells, empty and undefined projections, outer multiplicity and nonnumeric admission boundaries. This gate also exercises factorized Count, CountDistinct, Sum, Avg, Min and Max in the product-time well-founded circuit across initial publication, an independent factor insertion, checkpoint restoration and a value-factor retraction. The non-factorized six-kind matrix crosses the same restore-then-retract boundary. An additional Product differential requires both Filter and Map inside a well-founded component and crosses insertion, restore and retraction. This gate found a cardinality-neutral replacement defect: projected values changed while the net row count stayed constant, so retained outers were not scheduled and the aggregate output remained stale. A value-profile correction now schedules those outers independently of row-count change in both semantic and record paths. The regression pins replacement of one supported value by another and the resulting old/new output crossing.
The well-founded candidate path has the analogous provenance obligation. In
the graph {0 -> 2, 1 -> 0}, replacing 0 -> 2 with 0 -> 1 leaves the
cardinality of the rule head unchanged but changes the model to the undefined
cycle 0 <-> 1. Summing the insertion and retraction before candidate
selection erased both the derived correction and its candidate identity,
leaving win(0) stale. Product gamma now stages mixed-sign input as negative
then positive micro-batches at one logical outer coordinate. Settled corrections
remain additive; candidate records form a set union. The enclosing role advances
once and the complete operation remains one validated atomic transaction.
An exhaustive differential covers every graph on three nodes, every unordered
pair of toggled edges, one batched mutation and both sequential orders: 55,296
Product transitions agree with fresh well-founded evaluation. The minimal
replacement also passes after Product checkpoint reconstruction, with live and
restored checkpoints converging byte-for-byte. A mixed-sign batch spanning the
base, p, and q relations of one mutual-negation component agrees with fresh
evaluation for both true and undefined projections.
The checkpoint differential also replaces one aggregate input with another in
one cardinality-neutral batch for Count, CountDistinct, Sum, Avg, Min and Max.
Both ordinary and factorized aggregate plans agree with fresh well-founded
evaluation, and live and restored Product states converge after the replacement
and a subsequent retraction.
An integrated mixed-component differential seeds a positively recursive
two-node cycle from one direct fact, restores a checkpoint, then retracts the
cycle’s last external support. Both live and restored Product states remove the
unsupported cycle and agree with fresh evaluation. This gate exposed two
representations of an empty well-founded relation: absent in the checkpoint and
present with an empty extent after gamma reconstruction. WellFoundedPair
canonicalizes empty extents to absence at construction, so checkpoint equality
and runtime equality use the same representation by construction.
Failure atomicity is engine-independent at the program boundary. Established
and Product gates force a zero-round convergence failure, negative support and
signed-weight overflow after a valid publication. Each failure preserves the
program frontier, record-arena metrics and checkpoint bytes exactly. This
covers nested-revision termination and checked input-weight failure without a
Product-specific recovery path.
WFS checkpoint restoration treats the supplied base catalog as authoritative.
The immutable program plan classifies each dependency by provenance before
restoration. External dependencies must equal the base catalog at exact positive
support weights. Dependencies produced by an earlier stratum must contain any
direct base support; their derived support is validated by the complete restored
model because it is not external base authority. These checks run before
interning checkpoint rows or rebuilding either gamma engine. A Product gate
rejects independently corrupted truth and possible coordinates and also a
byte-valid checkpoint paired with a different external base snapshot; an
unchanged checkpoint reconstructs to identical bytes.
Support multiplicity is retained independently from Boolean membership in both
engines. Adding or removing one of two identical WFS input supports emits no
derived delta and performs no WFS revision; removing the final support performs
exactly one revision. The same boundary holds after checkpoint restoration,
and live and restored checkpoints converge after the final deletion.
Checkpoint ordering is semantic rather than allocator-dependent. Multi-join
tries freeze resolved values in value order, then re-establish destination-key
order after catalog or record identifiers are rebound during restoration.
Recovery audits construct the oracle through MaintenanceMode::Established
with the same explicit evaluation inputs as the restored circuit; no parallel
catalog assembly can omit the evaluation-clock relation.
Whole-program composition is gated for both engines across an acyclic lower
stratum, a WFS component and an acyclic upper consumer. After checkpoint
restoration, one batch retracts both a lower-stratum seed and a WFS base edge;
the lower relation, true and undefined WFS projections and upper visible
relation all agree with fresh evaluation, and live and restored checkpoints
converge.
Direct facts on a WFS head remain a separate support authority from rule-derived
truth. Both engines checkpoint a tuple supported simultaneously by a direct fact
and a rule, remove the direct support without removing truth, then remove the
derivation and retract truth. Live and restored outputs agree after each
boundary and converge to identical checkpoints.
A two-relation mutual-negation component gates p, q and both undefined
projections in one transaction clock. Both engines restore after initial direct
head and seed publication, then process a simultaneous seed/direct-head
retraction followed by a four-relation mixed-sign replacement. Every projection
agrees with fresh evaluation after each frontier and restored checkpoints
converge with live state.
Product gamma is independently gated before stable revision. One persistent
gamma state walks all 512 directed graphs on three nodes in Gray-code order;
for every base graph it walks all eight fixed WFS assumptions in Gray-code
order. All 4,096 Γ_E(I) results equal the direct rule oracle, while base and
assumption histories both change incrementally and each base frontier is
validated before publication.
Every integrated WFS fresh-evaluation assertion now reconstructs the published
pair from retained coordinates before comparing semantic output. Pair
construction requires T to be a subset of U; domain validation requires
U to be a subset of D_E. Because U = D_E - F, these checks also require
T and F to be disjoint. The exhaustive graph, partition, restore, aggregate
and mixed-stratum differentials therefore gate K3 invariants at every asserted
frontier rather than only comparing visible sinks.
The recursive gamma variant adds a positive transitive rule after the
antimonotone seed. One persistent Product state walks all 256 combinations of
two-node move and link graphs and all four fixed assumptions: 1,024
evaluations agree with a direct seed-plus-least-positive-closure oracle. This
independently gates the positive recursive component inside each gamma role.
The production maintainer boundary explicitly selects Product mode, verifies
that the recursive program carrier owns a Product WFS engine, round-trips the
projection checkpoint, and applies exit insertion, retraction and reassertion.
At every mutation the live Product route, restored Product route, Established
circuit and fresh evaluator publish the same complete read model; live and
restored projection checkpoints converge.
The repository ontology conformance replay constructs retained Established,
ordinary circuit and require-Product circuit maintainers for every admitted package,
then compares all three after mutation and checkpoint restoration, with fresh
Established evaluation as an additional oracle. On the gamma-bound head it
admitted all 32 eligible packages and replayed 188 mutations: nine seeded-input
mutations, 179 synthesized initially-empty-input mutations and 25 atomic multi-
input replacements. No package fell back or failed to build; both recursive
packages retained recursive routing. Product construction and checkpoint
restore are fail-closed, so Established fallback cannot satisfy this gate.
The combined oxc-reasoning, oxc-runtime and oxc-driver nextest surface
passes 2,947 tests with six skipped. The temporal-conjunction corpus entry has
explicit positive and exclusion goldens, so the general corpus gate and the
incremental differential both validate that fixture rather than accepting a
positive package with no semantic assertion.
Product-authored projection checkpoints restore directly in Established mode,
and Established-authored projection checkpoints restore directly in Product
mode. Both backends emit identical checkpoint bytes before either switch, and
each switched instance follows the same subsequent mutation stream. Engine
selection is therefore runtime policy, not persisted semantic state, providing
rollback and rollout paths without checkpoint migration.
Audited Product restoration independently evaluates Established WFS from the checkpoint’s validated base support before reconstructing Product physical state. The restored truth/possible pair must equal that oracle before the program can become readable. This closes the interval between checkpoint publication and the first audited mutation: a deterministic Product defect cannot validate its own prior checkpoint and then serve it without an independent comparison.
Audited Product also compares every maintained domain, truth and possible gamma
role against an independent stability_step evaluation at the role’s current
assumption. Empty and absent relations are canonicalized before comparison.
Mismatch aborts the transaction before coordinate publication; a fault-injection
test verifies that the frontier, model, record arena and checkpoint remain
unchanged. One opaque audit policy is selected for the complete revision and is
required by every production domain, truth and possible revision method, so a
new call site cannot omit the selected audit accidentally. Ordinary Product
does not construct the oracle.
Product rule-circuit construction also classifies every physical operator into one of eight semantic obligations: empty, unit, input, positive relational, existence, set boundary, aggregate or publication. The Rust match is exhaustive, so adding a physical operator cannot compile until its obligation is assigned. Admission retains both that theorem family and an exact physical-kernel tag: empty, singleton, scan, delayed scan, join, multijoin, filter, map, binding projection, tuple projection, union, antijoin, semijoin, distinct, aggregate, factorized aggregate, correlated count or sink. A new variant therefore cannot hide inside an existing broad family, and review evidence can name the concrete kernel present at each plan node. Aggregate admission is fail-closed at construction; collection and other unsupported aggregate semantics cannot survive until mutation execution. This classification is the index for per-operator refinement work, not itself a proof that an implementation satisfies its assigned obligation. The six-kind aggregate fragment is one exhaustive circuit-IR predicate shared by rule compilation, Product admission, physical dispatch and checkpoint validation. These boundaries cannot independently grow incompatible kind lists; adding a protocol kind makes the closed classification fail to compile until it is explicitly admitted or refused. Canonical-plan validation also requires aggregate group variables to be strictly ordered and an optional result variable to be fresh relative to the group. Generic, factorized and correlated-count nodes share this binding invariant. Malformed extraction metadata cannot receive Product admission or survive checkpoint plan validation. Admission evidence is issued only for a structurally canonical plan whose identifier recomputes from its complete operator, schedule and metadata commitment. Every session rechecks that canonical identity as well as the operator-obligation map. A stale identifier therefore cannot authorize an operator mutation merely because the old and new operators belong to the same semantic family. The same per-node admission evidence owns Generic Join arity together with its physical-kernel and semantic-obligation classification. Product rule state no longer retains a second node-to-arity map. Every temporal trie journal is validated against the admitted node and arity before publication; missing state is refused during circuit construction, while a missing journal, an extra journal or a shape mismatch refuses the transaction. Construction also compares the admission-owned node sets with the independently allocated antijoin/semijoin, distinct, scalar/correlated aggregate and factorized- aggregate state maps. A missing or extra retained-state owner therefore fails before the circuit can accept input. Fault tests remove and add a distinct-state owner and require construction-boundary refusal. Join, existence, distinct, scalar/correlated aggregate and factorized-aggregate retained state use one closed family-to-kernel classification. Construction and journal validation consume that classification rather than repeating kernel lists and diagnostic labels at each boundary.
DifferentialOperators.lean defines the signed-relation target for seven of
those eight families. Empty and unit have constant-transition laws; input and
publication use identity change. Selection and projection commute with change;
union is linear; join uses the full bilinear derivative including the
change-by-change term. A three-input join uses all seven nonempty combinations
of retained and changed input support, followed by arbitrary binding selection
and collision-consolidating projection. This is the multilinear derivative
required by a three-atom multiway join. Antijoin and semijoin have separate theorems for
remaining supported, losing last support, gaining first support and remaining
unsupported. Distinct emits exactly zero, one or minus one according to its old
and new zero crossings, so changes that alter support magnitude without
altering membership emit zero. These theorems prove the algebra the physical
operators must implement. They do not prove the Rust methods implement it; the
node-local semantic audit checks that concrete correspondence during tests.
Lean also emits a generated differential-operator layer containing concrete
signed transitions for empty, unit, input, selection, collision projection,
bilateral union, bilinear join, antijoin and semijoin support boundaries,
a cyclic ternary multiway join, distinct zero crossings and publication. Executable finite selection,
projection, join and existence-support definitions have proved equality to the
canonical denotations before their results are emitted. Rust applies each pair
of endpoints to a retained production circuit and compares its emitted delta
with Lean. The test-only Product node audit independently compares the record
backend with this scalar production backend at every physical node. Together
these gates form a finite cross-language chain from the canonical operator
semantics through scalar execution to Product record execution; they do not
constitute universal Rust refinement proofs.
The multiway vector joins binary atoms (x, y), (y, z) and (z, x) whose
rows have deliberately different orders, uses variable order [x, y, z], and
projects x. It changes all three inputs simultaneously with non-unit signed
support. Its expected delta is computed by Lean’s generic binding-selection and
projection theorem over the proved seven-term derivative, then replayed through
the retained worst-case-optimal multiway-join kernel. This proves the generic
Lean denotation and its correspondence to Rust for this finite nontrivial
fixture. Arbitrary Rust plans remain covered by production differentials and
node-local semantic auditing rather than a universal refinement theorem.
The same Lean layer computes every one of 512 Boolean support states for three
cyclic binary atoms over three rows each. Rust traverses those states in forward
and reverse Gray-code order through all six atom orders. Each plan derives the
required canonical first-occurrence variable order and exercises projections to
each variable, two ordered variable pairs, a constant and a repeated variable.
All 43,008 retained frontiers compare both emitted change and retained output
with Lean. This exhausts that finite binding domain and catches plan-order,
projection-collision and insertion/retraction history errors; it does not
quantify over unbounded relations or arbitrary compiled atom shapes.
Binary join uses a separate Lean-generated radix-three matrix with duplicate
keys on both sides. Six projections retain a left value, right value, ordered
pair, collision-consolidated key, constant, or repeated left value. Rust runs
each projection with both physical operand orientations through forward and
reverse reflected histories. All 17,496 frontiers compare emitted change and
retained output with Lean, covering bilateral non-unit support, projection
collisions and both retained arrangements.
Antijoin and semijoin additionally use a Lean-generated radix-three matrix over
three left rows and three right rows. Two right rows share one key, so the 729
support assignments distinguish one witness, duplicate witnesses, last-witness
removal and support changes that do not cross zero. Rust traverses forward and
reverse reflected histories through both retained production operators. All
2,916 frontiers compare emitted change and retained output with Lean. The
reflected-radix traversal and its completeness and one-row/one-unit adjacency
checks are shared with factor-summary conformance rather than reimplemented per
operator family.
Composition, binary join, multiway join and existence matrices use one retained
replay driver for state-space completeness, emitted signed changes and retained
sink equality. Matrix modules own only plan construction, input encoding and
Lean-output decoding; adding a matrix cannot silently omit one of the common
checks.
The generated wire schema is isolated from replay and plan construction, so a
schema revision does not enlarge the operator harness and a matrix implementation
cannot redefine its deserialized contract locally.
The same generated layer contains an explicitly composed
join-antijoin-filter-project-distinct plan. Lean proves its executable finite
definition equal to the corresponding canonical operator composition, then
computes both output rows for all 256 Boolean assignments of four left rows,
two join supports and two blocker supports. Rust traverses every assignment in
forward and reverse Gray-code histories. Every frontier changes one input fact
and must produce the exact Lean-derived signed output change as well as the
exact retained output. This checks 512 retained composition frontiers without
assuming that locally correct operator deltas necessarily compose correctly.
StratifiedAggregate.lean models an aggregate result as a deterministic guard
fixed by the completed lower stratum. It proves guarded compiled reduct
evaluation and gamma equal the normal-program semantics of the selected
grounding. This keeps aggregation outside the growing same-stratum fixpoint.
AggregateDenotation.lean then defines the six admitted folds over consolidated
nonnegative support. Count, sum and average preserve multiplicity; count-distinct,
minimum and maximum use positive presence. Average is exact rational division.
Its closed denotational tag contains those six folds plus refusal; the generated
wire layer maps it to surface/runtime names, so the Reasoning layer does not
import Syntax merely to classify physical folds.
Count and sum return zero on empty input, while average and extrema return no
result. Unsupported collection, set-collection, string-join and percentile
kinds have no denotation. The Accepts predicate is the concrete completed-
stratum guard after rule-specific group extraction and result binding.
Scalar, factorized, semantic and record-backed aggregate outputs use one Rust
result-binding function. It extends the canonical outer/group binding only when
the result variable is absent; an already-bound result fails with an
inconsistent-binding error instead of being overwritten. Canonical plans require
the same freshness statically, so construction and execution enforce one
binding invariant. Group extraction likewise uses one binding-access operation
for canonical semantic bindings and borrowed record bindings. A representation-
parity test uses a record whose physical column order differs from variable
order, requires both representations to produce the same canonical group and
the same present or absent projected value, and requires the same unbound-group-
variable refusal. Projection absence contributes to row cardinality but not to
the projected value multiset, matching Established aggregate evaluation.
The aggregate denotation is executable. Lean emits a separate generated vector
layer covering every admitted kind, exact rational inputs, duplicates, empty
inputs, bare cardinality, a refused kind, and factorized Cartesian products with
empty factors and exact scaling. A Rust replay invokes the production
fold_aggregate method and the incremental aggregate_result_from_support
method, then compares their normalized exact results with the Lean-computed
value. A third replay compares combine_factorized_fold with results that Lean
computes by denotationally expanding the Cartesian product; the Rust path never
performs that expansion. Each factorized vector also defines a second endpoint.
The incremental node initializes the first endpoint, applies the signed factor
differences, and must emit the Lean-computed old/new correction while retaining
the exact second-endpoint cardinality and value support for every factor. Each
transition runs in one changed two-column correlated group beside an unchanged
group, with distinct non-unit outer supports. The gate checks group-key
extraction, multiplicity-preserving result binding, and isolation as well as
empty-factor activation, simultaneous factor changes, extrema winner retraction,
and distinct-support replacement. All replays share one tagged Rust
schema loader. CI re-emits and diffs the
committed artifact, so changing either denotation or vector inputs cannot
silently preserve stale expectations. This establishes the scalar and retained-
support fold correspondence and a finite cross-language gate for factor-summary
combination, retained-summary transitions, finite multi-column correlated group
extraction, group isolation, and multiplicity-preserving numeric result binding.
FactorizedAggregate.lean proves the general binary algebra beneath summary
combination: Cartesian cardinality multiplies, a projection owned by one factor
scales its exact sum by the other factor’s cardinality, and its active projected
average is invariant under nonempty scaling. Its active projected values are
preserved when the other factor is active or empty when it is not.
The canonical retained projected-factor summary is also defined in Lean as
cardinality plus signed support per projected value. Lean proves that integrating
an arbitrary signed relation change is exactly pointwise summary addition, and
that multiplying this summary by an independent factor’s cardinality equals
summarizing the expanded Cartesian relation. These theorems apply to arbitrary
finite relations and integer supports rather than the generated fixture domain.
Universal correspondence from Rust’s retained factor-summary methods to this
denotation remains open; generated histories, node-local auditing and full-model
differentials cover that runtime boundary operationally.
The generated aggregate layer also exhausts retained factor-summary histories
for count, count-distinct, sum, average, minimum and maximum. Each kind has two
three-row factors; the projected factor contains values -1, 2 and 2, so
the state space includes duplicate-value support as well as extrema and sign
changes. Every row has support zero, one or two. Lean expands the Cartesian
product and computes every result for all 729 radix-three factor-support
assignments. Rust traverses those assignments in forward and reverse reflected
radix-three Gray-code order through the real factorized node, checking
the signed output change, retained factor cardinalities and retained value
support at every frontier. Adjacent states change exactly one row by one, so the
histories cover zero crossings and multiplicity-only changes. This adds 8,748
retained transitions without using the runtime summary-combination algorithm as
its own oracle.
The same 8,748 transitions also pass independently through the semantic profile
backend and the EvaluationRowId record profile entry used by Product
evaluation. Inputs use session-local row identities, outputs are materialized
through the production resolver, and retained journals publish persistent arena
identities.
Both emitted deltas must equal the Lean result. After every atomic publication,
the complete record state is resolved and must equal the semantic profile
state. This covers first-use projection publication, duplicate-value insertion
and retraction, extrema replacement, and record interning across long-lived
histories. Distinct-value patching preserves untouched values and explicitly
publishes values introduced when a factor changes from no projection to a
distinct projection. Extrema-index equality is defined by orientation and its
ordered key-to-support relation; persistent tree shape is an internal indexing
choice and cannot make semantically equal retained states compare unequal.
The corrected first-use publication changes persisted circuit semantics, so the
derivation semantic epoch advances and older circuit checkpoints are rebuilt
rather than trusted with incomplete distinct-value support.
The prior canonical-row test adapter, its separate extrema implementation, and
its partial record-group decoder were removed. Factorized Product evaluation
now has one record implementation for every aggregate kind; the exhaustive
history gate tests that implementation directly.
Semantic and record evaluation also call one representation-generic retained
transition kernel. That kernel selects affected outer bindings, prepares
distinct zero-crossing corrections, merges cardinality and value support,
canonicalizes extrema, and validates every temporal prefix. Only row identity
resolution and output emission remain backend-specific. A change to retained
factor semantics therefore cannot update one backend while bypassing the other.
Ordinary projected aggregates follow the same single-backend rule. Their
semantic/record parity and zero-cardinality replacement tests now construct
session-local evaluation rows, invoke the production record evaluator, and
materialize its output through the production resolver. The canonical-row
record adapter, its separate record-extrema group evaluator, and the partial
count-group decoder were removed. The remaining extrema module contains only
the exact semantic key and shared index-error translation used by production
folds.
Join and distinct record evaluation follow the same ownership rule. Production
and differential tests both intern session-local EvaluationRowId values,
execute the retained record evaluator, and materialize results only at the
comparison boundary. The canonical-row join and distinct adapters, their
record-arrangement conversion, and their duplicate retained-join emitter were
removed. Product-time, published/staged/correction cross terms, persistent
journal identity and distinct zero crossings are therefore tested against the
same implementations used by maintained programs.
Ordinary iteration time and Product gamma time instantiate one generic record
state view. Scan, multijoin, filter, map, projection, sink, join, distinct,
count and factorized aggregate routing therefore cannot diverge by adding or
changing a method in only one engine. A typed mode supplies the logical time,
retained antijoin support and antijoin transition because scalar exclusion
support and Product-time temporal exclusion have different state algebras.
Ordinary profiling hooks are also mode policy; they do not alter evaluation.
Canonical bindings and transaction-local record bindings also implement one
binding-access contract. Filter comparison, definedness, expression-input
admission, map evaluation and binding projection call one representation-
generic kernel. Tuple projection uses the same contract for constants,
variables and unbound-variable failures. Record comparisons retain borrowed values, and expression
evaluation materializes a compact binding at most once, so this correspondence
does not require tuple-wide conversion on the comparison path.
Antijoin retains one intentional mode boundary. Ordinary scalar support uses
the four sealed-support transitions; Product time uses temporal support and
Möbius differentiation over the logical-time join closure. Product semantic
and record evaluation both call the same key/row-generic temporal
differentiator. Ordinary and Product record emission also use one canonical
positional binding-order constructor, so their tuple identities cannot diverge.
Multiway joins instantiate one generic trie evaluator with semantic or interned
key codecs. Record-backed execution has one EvaluationRowId adapter for both
ordinary and Product logical time. The prior canonical-row record adapter and
its duplicate output codecs were test-only and are removed; tests now invoke
the production adapter and resolve its session-local output directly.
A post-audit-mode sustained probe uses 10,000 states, alternates one edge between two destinations for 128 mutations, and verifies that the final derived model returns to its initial state. Ordinary Product measured 0.106 ms p50 versus 4.446 ms Established, a 41.8-times speedup. Product final retained heap was 1.038 times Established, mutation peak was 0.662 times Established, and construction peak was 0.989 times Established. The explicit audited policy does not add complete-pair materialization or Established evaluation to ordinary Product.
Product is suitable for explicit gated use only when all of the following hold:
- gamma parity for every fixed assumption under signed base and assumption histories;
T intersect F = empty,T subset U subset D_E, complement correctness and equivalence between fixed points ofC_Eand stable revision;- the affected-region and worklist theorems are conditional; the runtime admits a regional revision only after checking prior/new exterior agreement, final regional exterior stability, gamma-target containment, monotone candidate emission, and scheduler quiescence;
- last-support deletion of unsupported positive and coordinate cycles;
- exact direct-head fact handling, nested-time termination, checked weights, transaction atomicity and checkpoint reconstruction from semantic state;
- differentials over odd and even negation loops, self loops, mutually recursive relations, exit insertion and deletion, alternative support, simultaneous domain/base changes, every false/undefined/true transition, mutation-order permutations and restore-then-mutate streams; and
- fixed-delta scaling over independent game regions demonstrating work proportional to the affected region rather than the retained component.
An operator-refinement matrix compiles one well-founded program whose gamma plan contains every admitted semantic obligation: empty, unit, input, positive relational, existence, set boundary, aggregate and publication. It traverses all 243 support assignments for five input tuples at multiplicities zero, one and two in both forward and reverse order. Each history is checkpointed and restored halfway through before continuing. Consecutive assignments include support-only changes, zero crossings, corrections of magnitude two and mixed- relation batches. Product output is compared with fresh Established evaluation after every frontier. The matrix also requires both engines to initialize predicate-free rules from an empty first batch. This gate exposed and now pins two initialization boundaries: an initial empty batch is a real first well-founded revision, and Product empty staging evaluates acyclic components as well as advancing recursive ones. Once an acyclic component has completed its initial singleton stage, an empty accepted delta skips it; this preserves the steady-state sparse path. The matrix’s exact manifest contains 14 kernels: empty, singleton, scan, join, multijoin, filter, map, tuple projection, union, antijoin, distinct, aggregate and sink, plus semijoin through nested double negation. Delayed scan, binding projection, factorized aggregate and correlated count are not mislabeled as matrix coverage. Separate Product tests assert each exact kernel before executing delayed recursive feedback insertion and retraction, modal diamond projection and retraction, all six factorized numeric mutation histories, or recursive correlated-count replacement. The complete Product-focused surface constructs every admitted physical kernel through the exact manifest before evaluation.
Every Product rule-circuit stage in the Rust test build also runs the semantic profile backend from the same published and transaction-local retained state. The audit compares every physical node’s signed output, settled sinks, candidate sinks and the resulting retained operator families before the record state can continue. Multiway-join journals are applied to cloned published tries after every transaction-local prior round, then compared as resolved semantic key/time state; equal stage output cannot conceal a divergent retained trie that would affect a later mutation. A test-only per-instance fault removes the record journal, verifies rejection at this boundary, then disables the fault and confirms the same unpublished input succeeds. Antijoin traces compare by materialized key/time support, not trace-batch segmentation. The canonical record decoder is generic over logical time and antijoin-support representation so this audit uses the same decoder as scalar checkpoint tests rather than maintaining a second Product shadow representation. Product-time extrema corrections are decoded symmetrically with their existing encoder. The audit is test-only and adds no production mutation work.
The runtime checks and differentials establish a fail-closed gated path, not
default semantic authority. CompiledGamma.lean defines the two-input reduct
operator directly over compiled relational rules: positive literals read the
growing reduct state while negative literals read the fixed gamma assumption.
The kernel proves this operator equal to the ground normal-program reduct step,
and proves their least-fixed-point gamma results and signed gamma transitions
equal. This covers relational atoms and deterministic comparison/compute
guards. It does not cover aggregates or prove that the Rust physical operators
implement the compiled denotation.
DifferentialOperators.lean also defines unary, binary and three-input
exact-derivative refinement boundaries. It proves that exact stateful derivatives compose through
both sequential nodes and binary fan-in, including simultaneous changes from
both upstream branches, and through direct three-input fan-in. The three-input
contract includes all seven nonempty combinations of changed and retained
inputs. These compositions reconstruct the operator’s new retained output.
This closes structural composition of unary, binary and three-input nodes at
the signed-relation denotation level. Identity, union, selection, projection,
Cartesian product, and join have explicit exact-derivative witnesses; product
and join include the simultaneous change-change term. Antijoin and semijoin
have complete four-case support-transition derivatives, and distinct has a
complete zero-crossing derivative; all three satisfy the same compositional
contract. Lean-computed transition vectors replay these denotations through
retained production circuits. The concrete unary replay includes a conditional
Map whose many-to-one result binding is projected and consolidated, covering
expression evaluation, result-variable insertion and downstream collision
handling across a signed mutation. Every operator vector is also expressed as
actual CompiledRule input: constants, identity, selection, projection, map,
union, binary and multiway join, antijoin, double-negation semijoin, set
boundary and publication. The compiler-selected graph must emit the
Lean-derived membership zero-crossing rather than the raw Z-set correction.
This checks lowering and execution together while preserving the distinction
between internal multiplicity and published set semantics. It does not prove that every Rust physical method satisfies an
exact-derivative premise or that the concrete physical plan denotes the
compiled reduct.
The same file proves the full arbitrary-arity support derivative. For any finite family of aligned input relations, the derivative is the sum over every nonempty subset of changed inputs, multiplied by retained support from the complement. The kernel proves this powerset expansion equals the exact product change, then lifts it through binding selection and collision-consolidating projection. The multiway-join algebra is therefore not limited to the three-input instance. Correspondence from the Rust Generic Join trie and its temporal journals to this denotation remains a physical-method obligation. An independent retained temporal differential exercises the concrete trie and journal implementation at every arity from two through eight. Its histories include simultaneous all-input changes from support one to support two, forcing every nonempty derivative subset to contribute. Expected output is computed only as the difference of the before/after scalar support products. The test also covers zero crossings, mixed zero/non-unit support, reactivation and complete retraction; it does not reuse trie evaluation as its oracle.
Aggregate denotation has a separate Lean-computed vector layer for all six
admitted numeric kinds, empty groups, duplicate projections, exact rationals,
factorized transitions and exhaustive retained factor histories. Rust checks
those vectors at the Established fold, incremental support fold, factorized
summary and record-profile boundaries. A further replay builds actual compiled
aggregate rules, applies them through retained CircuitInstance state and
compares their published result tuples with the Lean values. Factorized vectors
also build real independent-factor rules, require the compiler to select
FactorizedAggregate, and compare the retained before-to-after publication
delta with Lean’s Cartesian denotation. Count vectors additionally compile
through the positive-recursive-body path, require CorrelatedCount rather than
the generic aggregate operator, and compare its published tuples with Lean’s
empty and nonempty count denotation. This connects source-rule lowering to the
concrete aggregate operators and publication path;
Product mutation matrices independently compare the same physical kernels with
fresh Established evaluation.
The remaining default-routing gap is therefore the concrete correspondence from
the Rust physical methods to the signed operator denotations, the concrete
physical plan’s correspondence with the compiled reduct operator. Canonical
plan admission now derives binding-variable sets along the physical operator
graph. Aggregate group variables must occur in both the outer and folded input;
factorized groups must occur in every factor; projected values must occur in
the selected folded input; and correlated-count outer and input declarations
must exactly equal their derived physical bindings. Malformed extraction
metadata is therefore refused before completed-stratum state construction.
Finite exhaustive graphs, ontology replay, audited
execution, and fresh Established comparison detect divergence but do not prove
that correspondence for every program.
Product and Established construction now share one additional translation-input
gate. The actual WellFoundedEvaluationPlan rewrite is built once from the
retained component rules; its canonical module commitment must equal the module
commitment carried by every acyclic or positive-recursive gamma physical
component. Each physical component also retains its sorted multiset of canonical
compiled-rule commitments. Their combined multiset must equal the rewritten
rule multiset exactly, so an omitted, duplicated, or substituted rule is refused
without recompiling the physical plan or retaining another rule copy. These
commitments are part of CircuitPlanId; checkpoint validation therefore cannot
detach them from the operator graph. The same checker independently derives
rewritten rule-head identities and arities and requires their exact equality with the
acyclic sink and positive-recursive output relation set; a correct source hash
cannot conceal a missing, extra or renamed physical output. Rewritten bodies
independently yield their complete relation dependency identities and arities; these must
equal the union of physical Scan, DelayedScan and Generic Join inputs. Faults
that rename a physical input or output while preserving the source commitment
are refused. Rule-head projection is also checked without recompilation. The
validator walks each sink through its set boundary and union to the connected
rule producers, then recomputes each producer node identity from the exact
rewritten rule, physical stratum, canonical output path and actual operator.
Every rewritten rule must match exactly one connected Project or Generic Join
producer for its output relation, every producer must be matched, and its head
slots must equal the compiled rule head. A detached producer, wrong relation,
wrong constant, reordered variable or substituted projection is refused before
state construction. Candidate lookup is indexed by output relation, so this
validation is linear when relations have one producer and does not recompile
rule bodies. Every embedded acyclic, nested-recursive and recursive-SCC plan must
also retain its canonical identity. Operator identities recursively commit body
inputs, columns, join keys, predicates, expressions, aggregate configuration and
projections, so any detached or mutated physical body is refused generically.
This proves source/plan integrity, not that the compiler selected the denotationally
correct operator graph. The physical-plan refinement obligation above remains
open. Successful source validation returns opaque
ValidatedGammaCircuitPlan evidence. Production well-founded gamma-state
construction accepts that evidence rather than a raw gamma plan, so neither
Established nor Product construction can depend on a caller remembering a
separate validation step. Lower-level circuit constructors remain available to
focused kernel tests but are not the whole-program production seam.
Product rollout does not claim a universal proof that every Rust physical plan
refines its denotation. Instead, admission is fail-closed and the release gate
combines validated source-to-plan identity, Lean vectors, exhaustive finite
kernels, generated retained differentials, ontology replay, checkpoint
continuation, and an independently selectable Established oracle. Product is
the well-founded engine under ordinary circuit enablement. Established remains
both the process default when circuits are disabled and an explicit
well-founded escape hatch when circuits are enabled.
The generated whole-program reasoning layer provides a direct executable bridge
for a finite source fragment. Lean computes true and undefined extents for 12
programs covering recursion, negation, joins, comparisons, modal stripping,
grouped count/sum/min/max, empty aggregates, and two well-founded cycles. Rust
rebuilds each emitted program and evaluates it through fresh evaluation plus
cold and retained RequireEstablishedWfsCircuits, RequireCircuits, and
RequireAuditedProductCircuits programs receiving their
facts through empty input, forward insertion/retraction, full reassertion, and
reverse retraction/insertion. Lean independently computes true and undefined
extents at all 148 frontiers. Required admission makes fallback impossible.
Well-founded vectors select Established gamma through the explicit escape-hatch
mode and Product gamma through ordinary and audited circuit modes. At the first
full-input frontier each retained
program is checkpointed, restored with the matching EDB and policy identity, and
then continues the same trace. All three incremental policies must match at every
frontier; fresh and cold incremental evaluation must match the final model. This closes static and
forward/reverse mutation correspondence for those fixtures. It does not prove
universal physical-method correspondence or every arbitrary mutation order;
those claims remain outside the rollout evidence.
The batched Lean differential broadens cold-construction coverage beyond those
fixed fixtures. A deterministic generator emits 1,600 range-restricted programs:
700 relational compositions and 300 each for ordered comparisons,
recursion-through-negation, and grouped aggregates. The same generated program
is evaluated by Lean, fresh Established evaluation, fail-closed ordinary
incremental maintenance, and fail-closed Product maintenance seeded with its
facts as EDB state. All Rust paths must reproduce Lean’s true and undefined
extents. Incremental routes use RequireCircuits and
RequireUnauditedProductCircuits, so an admission failure or Established
fallback fails the gate. This tests many source-program compositions directly
against Lean. Every 700-program relational batch reserves one mandatory case for
a four-predicate cyclic join projected to one variable; the remaining 699 cases
retain deterministic feature generation. This extends direct Product
differential coverage beyond the proved and exhaustively enumerated three-input
join without relying on probabilistic feature selection. Each program then
follows five retained EDB frontiers: empty, full,
one rule-read-fact retraction, full reassertion, and empty. Both incremental routes
checkpoint and restore at the first full frontier; all 16,000 retained route models are compared with Lean’s
true and undefined extents. This broadens mutation-history evidence but does not
replace the universal physical-method correspondence argument.
DynamicGamma.lean isolates the history algebra from compiler correctness. It
proves that exact signed differences between consecutive semantic gamma results
telescope to the final semantic result. CompiledGamma.lean connects that
algebra to the compiled relational denotation and its grounded semantic gamma;
it deliberately stops before the Rust physical plan. A persistent Product
differential walks every two-node edge-support assignment with support weights
zero, one and two, including simultaneous corrections with weights from minus
two through two, and checks every fixed assumption against semantic gamma. This
establishes the signed-set algebra and exercises non-Boolean support histories;
it does not replace the remaining per-operator compiler refinement argument.
Product domain ownership
Established gamma retains its evaluated domain because no subordinate rule state exposes equivalent support. Product gamma does not retain a second domain map. Its domain role’s direct and derived record sets are the canonical support authority; published domain membership is their Boolean union.
Product domain role
+-- direct records ----+
+-- derived records ----+--> borrowed Boolean union
+--> tuple-local mutation reads
+--> sparse coordinate projection
+--> optional complete-pair observation
The union view supplies checked point membership to temporal overlays, coordinate differentiation and sink projection. It allocates no retained state and does not scan untouched records. Checkpoint and public full-model reads may materialize the union transiently. Established domain replacement remains variant-local; Product transactions cannot publish an independent domain map.
Record identity lifetime
RecordId is process-local storage identity, not checkpoint or semantic
identity. The arena may contain records created by committed evaluation but no
longer reachable from retained operator state. No component reclaims or remaps
records independently. Reclamation uses the semantic program-checkpoint boundary:
published ProgramProjection
|
+--> encode semantic component state and catalogs
+--> restore off-path into a fresh RecordArena
+--> validate program/catalog agreement
+--> restore projection-owned relation indexes
'--> atomic whole-snapshot swap
The old program remains published until every restore and validation step succeeds. Compaction runs before a subsequent user transaction, never after that transaction commits. It is considered only after at least 4,096 new record identities and two-times growth from the last compact arena. This amortizes reconstruction while bounding append-only garbage. The threshold is ephemeral policy state and is not part of semantic checkpoint identity.
The fixed-delta benchmark asserts before timing that inserting the exit edge
publishes win(0) and retracting it removes win(0) under both well-founded
engines. Three adjacent 20-sample runs over 10,000 retained self-loop states and
32 alternating mutations measured Product at 1.775 ms, 1.743 ms and 1.739 ms.
The corresponding Established-WFS circuit measurements were 135.26 ms, 128.20
ms and 139.87 ms. The last adjacent comparison is 80.4 times faster for Product.
This result covers one tuple-local mutation shape; it does not replace the
cross-shape latency, retained-memory and peak-memory gates for default routing.
Phase E — persistence and scale
Canonical projection checkpoints contain authoritative base/derived catalogs, component derivative state, arrangements, scheduler profiles and published-batch identity. Delegated input, sink and evaluator projections are omitted. Compatibility binds tenant, fork, module commitment, physical program-plan commitment, circuit schema version, derivation semantic epoch, execution configuration, circuit frontier, durable generation and event-prefix commitment. Restore validates the complete envelope off-path, replays the suffix and audits against full evaluation before atomic snapshot publication.
Temporal record ownership
The whole-program record arena is the sole owner of decoded temporal tuples.
Temporal relation support, producer provenance, pair indexes, NAF correlation
indexes and durable multiway-join keys retain record identities. They do not
retain Tuple, Value or canonical tuple bytes. Interval vectors and producer
addresses remain temporal-trace state because they are not derivable from
membership alone. Transaction-local semantic working sets may decode values,
but they are discarded before publication and checkpointing.
flowchart LR
B[Semantic temporal batch] --> RT[One program record transaction]
RT --> T[RecordId temporal trace journal]
RT --> P[RecordId pair and NAF journals]
RT --> M[Record-key multiway journals]
T --> V[Validate support and transaction token]
P --> V
M --> V
V --> A[Publish record suffix]
A --> C[Commit temporal indexes and trace]
C --> F[Publish frontier and output]
C --> W[Resolve records into semantic checkpoint DTO]
W --> R[Restore into one fresh record transaction]
Every prepared temporal journal carries the record-transaction token that created its provisional identities. Validation rejects a journal paired with another transaction. All fallible interning, support arithmetic and shape validation precede publication. The arena suffix publishes first; subsequent trace and component commits are prevalidated assignment-only operations. A failure therefore preserves arena length, temporal state, component indexes, frontier and checkpoint bytes.
Runtime identities never enter checkpoint compatibility. The temporal wire payload remains relation name, canonical semantic tuple and coalesced interval support. Encoding resolves record identities through the live arena; restore interns semantic rows through one fresh program transaction and reconstructs every trace and index against those identities. Checkpoint bytes consequently remain independent of allocation order and existing checkpoint versions remain readable without a schema migration.
The conversion gate requires all of the following:
- direct support, derived many-to-one provenance, pair indexes, NAF indexes and multiway source vectors reuse the same record identity for an equal tuple;
- every retained temporal record identity resolves through the program arena;
- a failed or stale prepare after provisional interning leaves arena length, trace, indexes, frontier and checkpoint bytes unchanged;
- forced digest collisions remain payload-distinct through temporal provenance and index lookup;
- checkpoint bytes are independent of local record-allocation order, restoration may assign different local identities, and the next mutation remains equal;
- last-support deletion removes temporal provenance and index references without leaving an unresolved identity; and
- retained, construction-peak and mutation-peak measurements report record counts alongside trace contribution and index-reference counts.
The native metric-temporal fragment admits acyclic unary box_minus,
box_plus, diamond_minus, or diamond_plus rules whose operands are
predicates and whose heads project bound operand variables or constants.
Interval-preserving positive rules of the form H(projection) :- P(pattern) are
trace-native components, so aliases and filtered projections may occur before,
after, or between temporal operators without crossing a membership-only
boundary. Reordering, repeated-variable and constant selection, many-to-one
projection, chains, fanout, multiple producers of one head, and direct facts on
derived heads share one trace. Acyclic binary since and until rules over two
predicate operands use keyed arrangements in the same trace and admit crossed
operand shapes, Cartesian joins, constants, repeated variables, and projected
heads. Positive recursive SCCs composed of interval-preserving projections and
unary or binary temporal rules retain producer/source contribution cells across
frontiers. Growth follows a sparse changed-tuple frontier. Support shrink uses
causal overdelete, exact-source rederivation, and then the same sparse frontier;
old cyclic support cannot justify itself across a retraction. Binary recursive
rules build transaction-local reverse dependencies from contribution
provenance. Those indexes contain addresses, not support, and cannot become a
second relation authority. Exact least-fixpoint reconstruction remains the
construction, checkpoint-recovery, and differential oracle path.
Each rule remains in a typed ProgramComponent, not a parallel maintainer.
A positive recursive temporal SCC may contain a positive relational join of
arbitrary arity. Its interval image is the intersection of every source
support. Two-predicate matching shares the neutral binary trace infrastructure
used by since and until. Larger joins use the canonical WCOJ atom order and
atom-ordered source provenance. Acyclic joins retain one WCOJ trie per atom;
recursive settlement creates one transaction-local WCOJ working set per
producer and applies round deltas to it. The working set is discarded before
publication and therefore cannot become a second relation authority. NAF,
and analytical-provider components in a temporal-connected program fall back
before circuit state is created. Comparison, compute, aggregate, and modal atoms
inside a metric-temporal program are language-level OE1351 refusals in the
established evaluator; circuit admission does not define an independent
semantics for them.
Explicit single-frame modal rules use the relational lowering above. Modal
companions, nested modal operands and federation truth carriers remain outside
that fragment.
recursive frontier tuples
|
v
transaction-local WCOJ working set
+-- one trie per ordered atom port
+-- apply current-round membership corrections
`-- restrict each changed port to changed tuples
|
v
affected ordered source vectors
|
v
intersect support from the shared temporal trace
|
v
producer/source assignments -> next recursive frontier
|
`-- discard working set before atomic publication
Metric-temporal maintenance requires an interval-valued component boundary;
ordinary FactDelta is insufficient because equal tuple membership can carry a
different valid-time support. Temporal components therefore consume signed
interval changes keyed by (relation, tuple). One program-local relation trace
owns direct support and producer-tagged derived support. A consumer reads the
producer’s trace entry directly; it does not retain a private input copy. The
effective relation is the coalesced union of direct and producer contributions.
Tuple membership is only the projection support != empty, never a second
authority.
One nonrecursive temporal stratum may contain independent temporal and ordinary positive rules. Admission selects a unary/binary temporal, projection, pair join, or multiway join component per rule; it does not require every rule in the stratum to share one operator family. All components still read and write the same trace transaction and publish one frontier.
Producer identity is independent of component scheduling. An acyclic component owns one canonical producer identity; a recursive SCC owns one per rule. The trace rejects duplicate identities during construction, and plan commitments bind each identity explicitly. Component vector position is never provenance.
durable commit with valid-time events
|
v
canonical event-to-EDB contribution projection
|
v
coalesced PRE/POST support for touched tuples
|
v
signed TemporalFactDelta(PRE - POST, POST - PRE)
|
v
shared direct + producer-tagged relation trace
|
v
compiled tuple constraints and projection
|-- injective: support by projected tuple
`-- many-to-one: projected tuple -> source contributions
|
+----------+-----------+
| |
v v
projection/unary image keyed pair or multiway WCOJ
identity or box/diamond since/until or relational intersection
| |
+----------+-----------+
v
old/new support difference
|
v
temporal worklist to fixpoint
|
+----------+-----------+
| |
v v
synthesized catalog membership projection
interval view (support is non-empty)
Unary operators recompute only tuples whose operand support changed and emit
new_image - old_image plus old_image - new_image. Binary operators arrange
both operands by their shared binding key and revisit only keys touched on
either side. Arbitrary-arity acyclic joins retain one membership-only WCOJ trie
per ordered atom port. A transaction stages trie corrections, restricts each
changed port to each changed tuple, and evaluates affected bindings against
both prior and staged roots. The union is the exact candidate set whose
atom-ordered contribution cells may have changed. Recursive multiway growth
uses the same changed-port restriction over a transaction-local trie working
set updated between rounds. Recursive deletion indexes every ordered source in
existing contribution provenance, clears dependent cells causally, rederives
exact addresses, then applies the same sparse frontier. Ordinary relational
conjunction uses pairwise interval-set
intersection; it does not impersonate a temporal operator. Recursive deletion
seeds invalidation from both effective-support
shrink and direct-support shrink. The latter is required when obsolete cyclic
support masks removal of the last direct seed. Each invalidated
(producer, output, source) cell is cleared exactly, dependent cells are
invalidated transitively, and all cleared cells are rederived against the
overdeleted trace before sparse forward settlement. Multi-source invalidation
uses a transaction-local reverse dependency index over old ordered provenance;
growth uses final staged operand tuples. The established finite-materializability
guard remains the publication gate. Checkpoints encode direct coalesced support
and reconstructible plans, not expanded time points or derived indexes. The
shared interval algebra supplies exact set difference over finite and infinite
endpoints so operator deltas never use sentinels or timeline-width iteration.
Before recursive settlement, the trace classifies every staged direct-support
assignment by exact interval difference. If old \\ new is empty for every
touched cell, the mutation is monotone: a sparse relation/tuple worklist
recomputes only producer contributions reachable from changed operands. Unary
rules visit only changed source tuples; binary rules build transaction-local
key indexes and enumerate only pairs touching a changed operand. Any direct
support shrink or replacement enters causal overdelete/rederive. This boundary
is semantic, not heuristic: retained cyclic support is safe during growth,
while shrink must remove causal descendants before testing which cells can be
rederived. Both paths write the same producer/source cells in the shared trace.
An SCC whose input relations have no effective support change creates no
settlement session; a two-SCC differential pins one additive mutation to one
observed recursive settlement.
staged direct support
|
v
old \\ new empty for every touched direct cell?
| yes | no
v v
sparse changed-tuple worklist seed direct/effective shrink roots
| |
| +----------- causal overdelete ----------+
| | clear producer/output/source cell |
| | enqueue dependent output tuple |
| +------------------------------------------+
| |
| rederive cleared cells
| |
| sparse changed-tuple worklist
| |
+---------------+----------------+
v
shared trace changed?
| yes | no
'--- next v
finite guard
|
v
atomic publication
ProjectionChanges bundles membership retractions, membership assertions and
temporal support changes into one commit argument. A maintainer either validates
and publishes all three or publishes none. A maintainer without an
interval-valued component refuses a nonempty temporal delta before changing
state; runtime then discards that projection and rebuilds from durable events.
For every temporal operand, preparation derives the expected empty/nonempty
carrier transitions from old and new interval support and requires exact
equality with the effective tuple-membership delta. This rejects a commit that
supplies only one representation while retaining support-only changes whose
carrier remains present.
Unary publication uses the program transaction boundary. One sparse trace transaction stages direct assignments, walks components in dependency order, and propagates only relations whose effective support changed. Preparation computes next operator images and empty/nonempty membership transitions without mutating live state. Validation precedes an assignment-only commit of the trace, base membership, frontier, durable commit identity, and read-model generation. The read model synthesizes intervals from the trace; direct facts and every producer on the same head are coalesced rather than overwritten.
Tuple projection is compiled once. Runtime projection performs only arity, constant, and repeated-column checks followed by indexed column moves. An injective projection stores one support set per output tuple. A many-to-one projection retains source-keyed contribution cells under each output tuple so changing or retracting one source cannot erase another. The coalesced output is computed from those cells and is not retained as a second authority. Projected output tuples, rather than physical operand tuples, enter the downstream temporal worklist. Unary projection admission increments the derivation semantic epoch to 10; native binary temporal admission increments it to 11; trace-native relational projection admission increments it to 12; recursive unary and binary temporal admission increments it to 13; trace-native two-predicate relational join admission increments it to 14. Arbitrary-arity acyclic relational join admission increments it to 15. Trace-native temporal predicate exclusion admission increments it to 16.
Program checkpoint version 9 persists the direct relation trace once and recomputes producer images topologically on restore. Plan-only component DTOs cannot duplicate fanout operands. Component-owned relations are omitted from catalog sidecars because content-addressed catalog bytes deliberately omit evaluation metadata. Restore rejects unordered relations or tuples, malformed or non-coalesced intervals, support without positive direct membership, plan or scope mismatch, and noncanonical encodings. Version-3 unary checkpoints migrate their sole input map into the shared trace; version-4 unary checkpoints, version-5 binary checkpoints, version-6 projection checkpoints, version-7 recursive checkpoints, version-8 join checkpoints, and older non-temporal versions remain decodable. Projection producers, acyclic binary join indexes, recursive binary pair contributions, acyclic multiway tries, reverse dependency indexes, and all other recursive producer images are rebuilt rather than persisted. The trace is the sole live and persisted interval authority; the catalog is a synthesized read view.
Binary components retain reconstructible join key -> tuple indexes for each
operand. Support remains exclusively in the shared trace. A transaction stages
index membership by join key from the final effective support, unions old and
staged-new counterpart buckets, and recomputes each affected tuple pair once.
Pending producer support has one output-partitioned representation; it is not
duplicated in source and output indexes. Typed pair provenance prevents one
Cartesian or projected collision from erasing another. Both operand changes,
index assignments, pair contributions, downstream support, tuple membership,
and the frontier publish through one program journal. An infinite-tail since
or until image refuses the journal before any index or trace assignment
commits.
Temporal binary operators and ordinary relational joins instantiate one generic
trace-pair component. The component owns retained operand indexes and the common
prepare/commit journal; its operator owns tuple matching, projection, and
support algebra. Since/until compute a metric image, while relational
conjunction computes interval intersection. This division prevents duplicated
index publication logic without conflating their semantics.
Closed-world predicate exclusion uses the same pair indexes but evaluates one
left contribution against the union of every matching right witness. The
operator computes left support \\ coalesce(right witness support) and retains
only unary left provenance. A right change invalidates the left bucket for its
join key; unrelated keys are not visited. Right support is read from the shared
trace and is never copied into the index.
changed left tuples ---------+
v
affected left keys ---> staged pair index
^ |
changed right tuples --------+ v
matching right tuples from final membership
|
left support from trace ---------------------------+-- union/coalesce
|
v
interval difference
|
v
unary source contribution
|
v
shared temporal trace
The pair specialization admits one positive predicate and one predicate NAF. The generalized conjunctive component admits arbitrary positive predicate and metric support expressions with multiple predicate NAF lookups. Multiple local existential witnesses contribute their support union. A program with NAF over a relation whose effective per-concept world is open remains on the established engine because absence is not definite falsity. NAF over an explicitly closed relation remains circuit-admissible even when the package default or unrelated concepts are open. Positive and modal operators do not read the world map. Non-predicate negands and recursion through NAF remain explicit refusals.
The established temporal materializer uses the same existential semantics. Variables local to a negated predicate are not ground-input requirements; every tuple extending the current positive binding contributes to one coalesced witness-support union. Treating an unbound local variable as an empty ground lookup would incorrectly derive through an existing witness and is a differential-oracle defect, not an admissible circuit difference.
Temporal rule compilation has one conjunctive normal form. It assigns stable source ports to predicate leaves, retains metric operators as support-expression nodes, separates positive conjuncts from predicate-NAF lookups, and records one head projection. The same normal form owns the flattened positive atom vector consumed by WCOJ, every relation identity used by support lookup, and each NAF correlation projection into positive source columns. The executable operator retains only resolution-dependent metric windows and source ports; it cannot retain divergent relation or correlation metadata. Positive variables use first-occurrence WCOJ order. Each NAF records correlated variables in positive order and local existentials in negand-source order. A head variable must be positively bound; a NAF-local variable cannot become a head binding.
Support evaluators exchange module-qualified RelationId values. Conversion
to catalog relation names occurs only at the temporal-trace adapter boundary;
operator interfaces cannot silently alias equal strings from different plan
identities. The trace owns one canonical name-to-RelationId registry built
from component plans and refuses conflicting module or arity identities before
loading catalog state. Retained direct-support partitions and producer-output
ownership are keyed by those typed identities. String keys exist only on
external catalog, mutation, and checkpoint adapters and are resolved through
the registry before retained state changes.
compiled rule body
|
v
temporal conjunctive normal form
+-- positive support expressions
| +-- predicate source ports
| +-- unary metric image
| `-- binary metric image
+-- predicate NAF lookups
| +-- correlated variables
| +-- positive-source correlation projection
| +-- predicate relation identity
| `-- local existentials
+-- positive WCOJ variable order
+-- complete source order
`-- head projection
|
+---- projection / unary / binary / join / exclusion specialization
`---- generalized conjunctive component
Existing specialized plans consume this normal form rather than reparsing rule shapes independently. The generalized component may therefore replace those specializations without changing source identity, variable order, projection, or NAF correlation semantics. WCOJ accepts fixed correlated bindings and descends only matching trie prefixes when a negand changes; it does not retain a second positive-match relation.
flowchart LR
Delta[effective support changes] --> Pos[staged positive WCOJ tries]
Delta --> Neg[staged correlation-to-witness indexes]
Neg --> Keys[affected correlation keys]
Keys --> Old[restricted published WCOJ descent]
Keys --> New[restricted staged WCOJ descent]
Pos --> Changed[positive-port affected matches]
Old --> Affected[deduplicated positive source vectors]
New --> Affected
Changed --> Affected
Affected --> Eval[normal-form support evaluator]
Neg --> Eval
Trace[shared temporal support trace] --> Eval
Eval --> Journal[one atomic producer/index journal]
Journal --> Trace
The NAF arrangement stores exactly correlation key -> witness tuples.
Existential bindings are not retained as another index level because execution
only observes their support union. Positive tries store membership and keys;
all interval support remains in the shared trace. Published witness buckets are
borrowed during support evaluation rather than cloned per candidate; only a
staged overlay materializes its changed witness view. The prepared journal
validates the positive port count and NAF index count before publication.
Generated generalized-conjunction coverage runs 128 deterministic multi-key frontiers spanning positive and NAF membership insertion, deletion and support replacement. Every frontier is compared with fresh full evaluation, and each stream continues through checkpoint restoration. Recursive lower-stratum NAF coverage adds 96 generated graph frontiers spanning seed, edge and blocker membership and support changes, including cycles and checkpoint continuation.
Positive recursive temporal SCCs may read predicate NAF from completed lower strata. They use the same normal form, support evaluator, source-vector provenance, and transaction-local WCOJ/NAF arrangements. The lower relation is frozen during each SCC fixpoint. Positive-support growth and NAF-support shrink use sparse frontier settlement. Positive-support shrink, NAF-support growth, or mixed replacement refreshes the affected conjunctive producer, seeds changed output identities into causal overdelete/rederive, and resumes sparse frontier settlement. Cyclic self-support is removed before rederivation. Neither path invokes Established, clears the whole SCC, or duplicates interval support. The transaction-local reverse adjacency owns each contribution address once; per-input keys retain only integer indexes into that table, so an arbitrary-arity source vector is not copied for every incident input port. One producer-aligned settlement workspace lazily owns both plain multiway WCOJ state and generalized-conjunctive WCOJ/NAF state. Producer ordinal has one workspace authority rather than parallel vectors. Conjunctive input refresh is a separate transaction-local snapshot: one prior WCOJ/NAF working set advances atomically to the input-current snapshot, enumerates the union of prior and current affected source vectors, evaluates their current support, and is then discarded. A removed positive tuple probes only the prior roots, an inserted tuple probes only the staged roots, and a tuple absent from both probes neither. NAF correlation refresh descends one root set when positive membership did not change; identical prior/current WCOJ descent cannot produce another candidate. Causal overdelete changes recursive membership after that point, so the settlement workspace is built lazily from the post-overdelete trace rather than relabeling the input-current WCOJ as settlement-current. Both snapshots are discarded before publication and neither becomes retained relation authority.
flowchart LR
Prior[prior committed trace] --> Refresh[refresh working set]
Input[input-current trace] --> Refresh
Refresh --> Candidates[old and new source vectors]
Candidates --> Assign[assign current producer support]
Assign --> Overdelete[causal overdelete]
Overdelete --> Settle[post-overdelete settlement workspace]
Settle --> Rederive[exact rederive and sparse frontier]
Rederive --> Publish[atomic trace publication]
Refresh -.discard.-> Drop1[transaction-local]
Settle -.discard.-> Drop2[transaction-local]
Metric binary provenance is a typed left/right pair. Relational-join provenance is an atom-ordered source vector, including for two-atom joins. The distinct representation preserves aliased atom ports and extends to arbitrary arity without reinterpreting a metric contribution key. Both remain source keys under the same producer/output contribution map.
Ordinary and interval-valued join compilers call one canonical metadata builder for ordered atom ports, relation identities, columns, and first-occurrence variable order. The temporal compiler cannot drift from the ordinary WCOJ binding layout while its retained support representation remains independent. The interval join plan stores that atom vector and variable order directly; binary execution is a specialization over the first two atom ports, not a second left/right plan representation.
Binary temporal semantics are a stateless operator containing only the compiled
tuple projection, window, and since/until operation. The acyclic component
wraps that operator with retained operand indexes. A recursive producer stores
only the stateless operator. Settlement constructs transaction-local pair
indexes, multiway trie working sets, or reverse-dependency indexes from the
staged trace and contribution provenance. Recursive state therefore cannot
accidentally publish or checkpoint an acyclic index as a second membership
authority.
Recursive binary differential coverage includes since and until, nonzero
windows, two-round tuple propagation, support-only replacement, pair-collision
survival, edge and seed retraction, removal of an unfounded cycle, checkpoint
continuation, and iteration-bound failure followed by a successful retry at the
same frontier. Every accepted result is compared with fresh Established
evaluation; each test asserts the temporal circuit route so fallback cannot
satisfy the oracle accidentally.
Recursive three-predicate coverage checks initial least-fixpoint construction, checkpoint reconstruction, causal edge retraction, exact interval support, and fresh-evaluator parity. It asserts the temporal circuit route. A 100-node, five-sample recursive multiway replacement measured circuit p50 1.596 ms and p95 2.003 ms versus full-evaluation p50 31.872 ms and p95 37.558 ms, a 19.97-fold p50 speedup. A 1,000-node control was terminated after two minutes in full evaluation and is not reported.
Acyclic relational-join coverage compares initial construction, support-only replacement, checkpoint restoration, and Cartesian many-to-one pair removal with fresh Established evaluation. Three-predicate coverage additionally checks checkpoint reconstruction, final tuple retraction, and survival of a colliding alternative contribution. Every case asserts the temporal circuit route.
The arbitrary-arity benchmark retains recent(x), anchor(x), and guard(x)
arrangements and alternates valid-time support for base tuples. At 1,000 rows
and one mutation, ten release samples measured p50 0.713 ms for the circuit and
21.737 ms for full evaluation, a 30.50-fold speedup. At 10,000 rows, one
mutation measured 4.007 ms versus 1,876.521 ms, a 468.34-fold speedup; 100
simultaneous mutations measured 5.201 ms versus 1,885.681 ms, a 362.60-fold
speedup. The circuit retained 30,000 trie keys and 10,000 producer cells. These
are latency measurements, not retained-memory replacement evidence.
The predicate-exclusion benchmark retains aligned base(x) and excluded(x)
arrangements and changes only excluded support. On an Apple M5 Pro, 1,000
rows and one mutation measured circuit p50 0.006 ms versus established p50
26.171 ms, a 4,052.51-fold speedup. One hundred simultaneous mutations measured
0.228 ms versus 27.636 ms, a 121.06-fold speedup. At 10,000 rows and one
mutation, five samples measured 0.005 ms versus 3,790.854 ms, a 758,170.83-fold
speedup; five samples expose scale but do not establish production percentiles.
The established materializer scans negand tuples for every positive binding in
this workload. A 100,000-row control was terminated without reporting a result.
The circuit retains two operand arrangements and one producer contribution per
left tuple.
Acyclic temporal transactions do not construct the recursive finite-materialization guard. Its data-extent calculation scans all direct support and is required only when a recursive component can extend endpoints; computing it for acyclic projection, join, or exclusion would turn sparse mutation latency into a function of total temporal state.
The native support-only benchmark retains 100,000 independently interval-stamped
input tuples and alternates one tuple between two disjoint intervals. Each
circuit sample applies one identified TemporalFactDelta; each control sample
clones the base catalog and runs the established full temporal evaluation. Ten
release samples on an Apple M5 Pro measured a one-rule circuit at p50 1,709 ns
and p95 45,084 ns versus full-evaluation p50 217,735,333 ns and p95 223,634,792
ns: 127,405 times faster at p50. A four-rule chain measured circuit p50 4,917
ns and p95 48,333 ns versus full-evaluation p50 566,281,542 ns and p95
588,555,625 ns: 115,168 times faster at p50. This isolates admitted unary
support-only shapes; it does not estimate binary, recursive, event-scan delta
assembly, or new-identity fallback costs.
A 20-sample many-to-one control retained 100,000 two-column input tuples, projected groups of 100 sources to one output, chained that output through a second unary temporal rule, and changed one source interval per sample. Circuit p50 was 16,917 ns and p95 24,250 ns versus full-evaluation p50 147,272,375 ns and p95 149,163,916 ns: 8,706 times faster at p50. This measures source provenance aggregation and downstream support propagation, not membership-only short-circuiting.
A 100-sample binary since control retained 1,000 aligned tuples in each
operand and changed one left support per sample. Circuit p50 was 2,834 ns and
p95 4,792 ns versus full-evaluation p50 39,562,292 ns and p95 40,140,792 ns:
13,960 times faster at p50. Changing all 1,000 left supports in each transaction
measured circuit p50 3,135,042 ns and p95 4,201,125 ns versus full-evaluation
p50 40,652,958 ns and p95 42,024,084 ns: 13.0 times faster at p50. Both runs
retained 2,000 arranged tuples, 2,000 join-key buckets, 1,000 producer cells,
and 1,000 sink tuples. The full evaluator’s current binary materializer uses a
nested operand join, so a 100,000-row control is quadratic and was not a
practical comparison; the circuit uses shared-variable keyed arrangements.
A ten-sample acyclic relational-join control retained 1,000 aligned tuples in the temporal input and ordinary anchor relation, then changed one input support per sample. Circuit p50 was 0.247 ms and p95 0.288 ms versus full-evaluation p50 46.350 ms and p95 49.262 ms: 188 times faster at p50. The circuit retained 2,000 arranged tuples, 2,000 join-key buckets, and 2,000 producer cells across the temporal image and join. A 100,000-row control did not complete one bounded comparison within 90 seconds because the established temporal materializer uses a nested relational join; it was terminated and is not reported as a speedup.
A 100-sample recursive identity control retained 10,000 base tuples and the same 10,000-tuple recursive closure, then changed one base interval per sample. The exact affected-SCC rebuild measured circuit p50 94.274 ms and p95 96.698 ms versus Established p50 22.136 ms and p95 23.214 ms: the first recursive backend was 4.26 times slower. After retained causal deletion replaced mutation-time reconstruction, the same 100-sample shape measured circuit p50 1.351 ms and p95 1.411 ms versus Established p50 22.404 ms and p95 25.559 ms: 16.59 times faster at p50. Construction and checkpoint recovery retain exact reconstruction as an independent correctness path.
For monotone recursive growth, 100 insertions into a retained 10,000-row recursive identity workload measured circuit p50 1.302 ms and p95 1.331 ms versus Established p50 21.718 ms and p95 22.117 ms: 16.68 times faster. A 20-insertion 100,000-row run measured circuit p50 14.249 ms and p95 14.545 ms versus Established p50 258.070 ms and p95 268.001 ms: 18.11 times faster. Both runs add one new direct tuple per frontier and compare the final model with fresh evaluation. Growth and shrink now use the same retained contribution representation; only their settlement algorithms differ.
A 20-sample recursive binary chain control retained one seed, 99 temporal edges, and a 100-tuple closure, then changed the seed interval. Exact SCC reconstruction originally measured circuit p50 16.546 ms versus Established p50 14.759 ms. Retained causal deletion with a transaction-local binary reverse dependency index measured circuit p50 0.723 ms and p95 0.800 ms versus Established p50 15.357 ms and p95 15.559 ms: 21.25 times faster at p50. The circuit retained 100 producer cells and 100 sink tuples.
A three-sample 1,000-tuple chain measured circuit p50 1,776.563 ms and p95 1,798.802 ms under exact reconstruction versus Established p50 9,943.131 ms and p95 10,013.046 ms. Retained causal deletion subsequently measured circuit p50 8.282 ms and p95 8.662 ms versus Established p50 10,064.654 ms and p95 10,085.062 ms: 1,215 times faster at p50. The retained result has only three samples and is a scaling signal, not a production latency gate.
A five-sample recursive relational-chain control routes a [0,0]
diamond_plus seed into an ordinary recursive two-predicate join and alternates
the seed support. At 100 nodes, circuit p50 was 1.111 ms versus Established p50
12.785 ms: 11.51 times faster. At 1,000 nodes, circuit p50 was 8.101 ms versus
Established p50 10,704.844 ms: 1,321 times faster. Both runs compare the final
model with fresh evaluation. Five samples are sufficient to expose scaling, not
to establish a production latency percentile.
Temporal deltas are support differences, not raw event intervals. For every
touched (relation, tuple), runtime projects both the pre-commit and post-commit
live-event sets through the same concept and relation closure used by full
catalog seeding. It coalesces all supporting intervals, then emits
PRE - POST and POST - PRE. This preserves overlap supported by duplicate
assertions and handles a replacement assertion atomically. The materialized
model cannot supply pre-commit base support because its interval catalog may
already contain derived support; durable base events or retained base-support
state are the only authorities.
The evaluation clock is an explicit retained input. Compilation rewrites every
today() in one rule to one fresh variable and prepends the reserved singleton
scan $evaluation_clock(day). The rewrite is idempotent and refreshes every
enclosing NAF projection mask. Runtime captures one day per operation and
installs, refreshes and checkpoints the singleton through the same catalog and
transaction carriers as user facts. User deltas cannot write reserved input
relations.
runtime operation captures EvaluationInputs(day)
|
v
normalize today() -> clock variable
|
v
canonical $evaluation_clock(Date(day)) singleton
|
+-----------+-----------+
| |
v v
Established off-path circuit signed delta
rebuild on rollover -Date(old), +Date(new)
| |
+-----------+-----------+
v
one published materialized model
|
v
checkpoint identity binds evaluation day
Clock changes for ordinary rules are signed circuit transactions. An enumerate-derived rule reads the clock while materializing its frozen EDB, so a clock change rebuilds that EDB and the circuit off-path under the same captured day before publication. Warm columnar state remains the sole frozen model representation; its maintainer reads the clock singleton from that columnar model rather than retaining a duplicate day field. Aggregate subpipelines admit predicate scans, comparisons, computed bindings and predicate negation. Negation lowers through the same sealed antijoin constructor used by an outer rule body, so schedule metadata, relation arity, join keys and nonmonotone boundaries cannot diverge between the two contexts. Nested aggregates, modal atoms and temporal atoms inside an aggregate remain typed whole-program refusals. Supported well-founded components select Product, audited Product or Established gamma through explicit maintenance policy. Unsupported constructs are typed compile refusals; no rule is silently omitted.
Verification
The generated Lean differential evaluates 1,600 cold programs and 16,000 retained
incremental-route frontiers. Every history retracts a fact read by an enabled rule and
crosses checkpoint restoration; ordinary incremental and Product must match Lean’s true and undefined
extents at every frontier. The authoritative differential passed in 88.44
seconds. The complete oxc-reasoning suite passed 1,302 tests with one skipped
in 105.90 seconds; strict all-target, all-feature Clippy and formatting passed.
Fixed-vector and generated-history replay use one shared K3 model comparator;
conformance paths cannot independently drift on truth or undefined diagnostics.
A post-correspondence bounded rollout probe retained 10,000 independent game states and alternated one edge for 128 mutations. Product measured 0.063 ms p50 versus 3.899 ms Established, a 62.0-times speedup. Product final retained heap was 0.900 times Established and mutation peak was 0.476 times Established. Product construction peak remained 1.372 times Established; construction is therefore still a rollout optimization target, not a retained-state regression.
Program flow transfers each accepted profile into its final consumer. The record-backed Product evaluator consumes that owned profile directly; only the borrowed kernel-test convenience path clones it. This removes a redundant full profile copy without adding a second retained representation. Positive-recursive components likewise consume the Product-time profile and move its signed buckets into recursive logical time. Component outputs needed by later strata remain profiles in program flow; terminal settled and candidate outputs are consolidated directly into record extents as each component finishes. The revision driver therefore receives its native extent representation instead of retaining and subsequently converting a second whole-program profile map. The rule-session transaction retains physical operator journals, but it does not retain cumulative copies of settled and candidate output profiles: production propagation consumes each stage result immediately. Cumulative prepared-result accessors remain test-only for kernel assertions and are absent from release construction. Product program flow is representation-generic. Production interns external semantic facts once at the program boundary, then carries record identities through acyclic components, positive-recursive components and downstream strata. Gamma-assumption changes enter the same flow as record profiles under their compiled shadow-relation identity. They are no longer decoded to tuples, rebuilt as semantic profiles and re-interned before evaluation. The test-only physical-method audit resolves record inputs back to semantic tuples so the independent semantic backend still checks the production record path. In bounded 10,000-value construction probes, factorized-min Product peak heap fell from 29,118,641 to 23,945,202 bytes and edge-replacement Product peak heap fell from 35,206,998 to 27,353,955 bytes. Removing the production output mirrors first reduced edge replacement from 33,944,177 to 32,355,519 bytes; record-native flow accounts for the remaining reduction. Factorized-min Product construction is 0.875 times the corresponding 27,349,240-byte Established peak. Edge replacement still retains three staged gamma-role journals during atomic construction and remains 1.095 times its 24,990,650-byte Established peak.
Product temporal antijoin preparation reads retained state through a validated key-window view. The view checks physical key metadata once, then materializes one affected key while differentiating it; it does not copy the complete affected retained window. Left corrections are also the sole source for their arrangement journal instead of being accumulated into a parallel assignment map. These are representation and lifetime changes: the same antijoin derivative, temporal support trace and atomic journal remain authoritative. On the 10,000-game, 128-mutation edge-replacement control, Product construction peak fell from 27,353,955 to 23,535,563 bytes and is 0.942 times the 24,975,690-byte Established peak. Product p50 was 0.060 ms versus 3.907 ms Established, a 65.4-times speedup. Final retained heap was 4,184,481 bytes versus 4,651,381 bytes Established, and mutation peak was 4,622,199 bytes versus 9,725,441 bytes. The 10,000-value factorized-Min control measured a 23,938,898-byte Product construction peak versus 27,346,584 bytes Established, with 0.937 ms Product p50 versus 3.196 ms Established. Streaming retained antijoin windows therefore removes the remaining measured Product construction premium on both bounded controls without adding another state representation.
Every deterministic and generated mutation stream compares the integrated circuit output with a fresh full evaluation after every frontier. Gates also cover batch permutation, cancellation, checkpoint/restore, module commitment changes, arithmetic overflow, operator failure and the circuit kill switch. Integrated WFS and Product differentials live in a dedicated program-test module; generic program transactions, recursive strata and flow tests remain in the parent module. Ledger, catalog and record-resolution fixtures remain shared from one parent definition rather than copied between suites.
The admitted replacement matrix also constructs an Established maintainer for
the same rules, initial EDB and mutations. Join, direct-head overlap, antijoin,
comparison filters, computed map/projection, individual constants, repeated
predicate variables, constant heads, all numeric aggregates, bare-count
existence, constant aggregate projections, aggregate-local filter/map pipelines,
aggregate-local predicate negation, factorized outer-only negation,
unary/binary/conditional/builtin scalar expressions, compact date arithmetic,
text indirection, undefined-expression row removal, union support, physical
multiway join, generated mixed acyclic mutations and named recursive support
transitions compare Established, circuit and fresh evaluation after every
frontier. Each circuit assertion pins its selected route, and each Established
assertion pins the disabled-circuit route. Product-specific mutation and restore
coverage includes constant heads, constant recursive arguments, repeated
predicate variables, compact dates, text indirection, symbolic identity,
conditional partial expressions, undefined-row removal, exact rounding and
calendar builtins. Nested zone-aware and wall-clock chains cover instant
parsing, time-zone validation and conversion, DST-aware zoned-day shifts,
plain-datetime shifts, civil date/time recomposition and wall-to-zone
conversion across mutation and checkpoint restoration. A loud scalar type
error is also required to preserve the prior frontier, model and byte-identical
checkpoint. Product aggregate coverage
includes bare-count existence transitions and a filtered/computed projected Sum
over exact rational inputs across checkpoint restoration.
Predicate-free compute, empty-body constants, global negation, leading numeric
aggregation and computed-prefix joins additionally compare scalar circuit,
program circuit and fresh evaluation. Checkpoint restoration occurs both while
global negation is blocked and while constant support is visible. A recursive
constant base rule exercises singleton emission inside nested-time evaluation.
The Established delta-seeded inserter requires a leading predicate; its route
selection therefore uses full recomputation for predicate-free prefixes rather
than evaluating a different body order.
Scalar NAF coverage includes positive and double-negated comparisons, defined
and undefined computations, aggregate-local scalar negation, mutation and
checkpoint restoration. Division by zero pins the distinction between
DoesNotSatisfy and ordinary Boolean inversion.
Modal coverage includes diamond witnesses, universal box support, open-world
missing successors, dead-end vacuity, accessibility insertion and retraction,
proposition insertion and retraction, simultaneous edge/proposition changes,
last-payload-domain removal, nullary payloads and checkpoint restoration.
Nested predicate NAF coverage checks multiple existential witnesses, removal of
one versus the last witness, different correlation keys, aggregate-local
existence without witness multiplication, mutation and checkpoint restoration.
Catalog comparisons remove empty relation entries because Established retains
those storage entries while circuit projections omit them; tuple contents and
relation semantics must otherwise be exact.
Circuit admission first runs the Established full-program open-world taint
guard. It then reduces a top-level NAF chain ending at an effectively open
predicate to the same constant as Established: odd depth is false and removes
the rule; even depth is true and removes the atom. Other producers of the same
head and downstream positive consumers remain in the circuit. The same
reduction applies to conjunction-level atoms inside a numeric aggregate body.
An odd-depth atom becomes an explicit typed relational zero; even depth removes
the identity atom. This preserves empty-input Count, CountDistinct, Sum, Avg,
Min, Max and bare-existence behavior without aggregate-specific retained state.
Other embedded open-world NAF shapes still force a typed whole-program refusal.
Build and checkpoint restoration use the same normalized execution rules under
the original accepted program’s module identity. Distinct source programs that
normalize to the same operators therefore cannot share checkpoints, and
changing effective world assumptions rejects an incompatible checkpoint.
Retained plans use a canonical statistics-free body order: every base relation
has the same neutral structural cost and derived relations remain unknown. Full
evaluation may choose a fresh SIP order from current relation sizes, but mutable
catalog cardinalities cannot change a retained plan commitment between
construction and checkpoint restoration. Source-corpus recovery after
asserting into an initially empty join input is the regression gate for this
boundary.
Negative admission controls pin fallback for remaining open-world NAF shapes
and nonpositive relation weights. Positive, modal and explicitly closed-NAF
programs admit catalogs containing unrelated open-world concepts. Any positive
input support is one live logical fact in both engines. Record-backed base
projection retains its exact integer weight,
so construction, mutation and checkpoint restoration preserve the Established
catalog rather than collapsing publication to weight one.
Valid-time metadata is retained by the projection even when the rule program
has no temporal operator: temporal-only durable commits update the pass-through
sidecar without changing circuit membership, and checkpoint restoration
reconstructs the same metadata.
Production route controls require the circuit route for the supported explicit
modal and metric-temporal fragments. Language-invalid temporal mixtures,
non-numeric aggregates and nested aggregates retain defensive typed
whole-program refusal coverage at the internal compiler boundary; they are not
production source-program fallback cases.
Aggregate-local negation instead requires the circuit route and
compares all six numeric folds, bare existence, existential blocker support,
atomic blocker replacement and checkpoint restoration with Established and
fresh evaluation.
Inline-set values are canonicalized to sorted unique values when rules compile; catalog seeding repeats that canonicalization defensively for older decoded rules. Seeding replaces the reserved relation with its exact content-addressed extent instead of trusting preexisting state. Individual references enter the catalog identity space at this boundary, so inline membership and ordinary fact bindings use the same representation. The content-addressed relation name, stored values and seeded relation therefore describe one set by construction. Duplicate literals cannot create a non-set weight, change admission according to rule order or force a catalog fallback. Differentials exercise duplicate and individual inline-set values through Established, ordinary circuit and Product routes across retraction and assertion.
The compiled ontology corpus runs three independent maintainers from the same
elaborated rules and EDB: Established, Established-WFS circuit preference, and
Product-WFS circuit preference. Every admitted package compares all three with
fresh evaluation after initialization and after mutating every compiled input
relation through retraction, repeated absent retraction, reassertion and
duplicate assertion. The semantic comparison includes tuple weights, explicit
valid-time support, metric resolution and every program-observed world
assumption. Temporal packages additionally replace and restore support without
changing membership. Every admitted plan checkpoints after its first input
sequence, restores under the same required route and continues the remaining
stream. Multi-input packages also execute one atomic cross-relation replacement
and restoration. The current corpus admits 32 packages and exercises 188 input
sequences, including nine seeded inputs, plus 25 atomic multi-input sequences;
one package has no compiled rule input. The identity-equality package proves the
diagonal result, then retracts and reasserts the concept extent through
Established, circuit, Product and fresh evaluation. Both recursive corpus
packages route through the recursive circuit under Product.
The same differential runner accepts an explicit external corpus root without
changing engine semantics. Corpus discovery, artifact resolution, semantic
comparison, differential-session ownership, mutation scenarios and orchestration
are separate test modules. The session alone owns the three maintainers, EDB,
generation and checkpoint lifecycle, so a scenario cannot advance one engine
without the others. External artifacts mutate seeded tuples only because
compiled terms do not retain enough source type information to synthesize valid
values. The Sharpe ontology corpus at revision 9937171e7e contains 17
manifests: 11 build under the current compiler, require RecursiveCircuit and
pass reversible mutation parity; six fail source compilation before maintenance
selection. Its seven authoritative ontology test packages also pass 868 source
tests.
Release mutation timing is workload-dependent. Sharpe core is 14.96 times
faster than Established, and the five authoritative packages other than
market-calendar are approximately 21.9 times faster in aggregate. The
market-calendar $arm sequence previously remained 3.85 times slower after
transient-key optimization because calendar-roll lowering produced approximately
nine million distinct Cartesian record pairs before a semantic equality filter.
Generic compiled-rule variable aliasing is forbidden: semantic equality can
equate different numeric and temporal representations, while join identity is
structural.
Equality normalization therefore runs during elaboration, before type evidence is erased. It uses a second variable-sort analysis that does not propagate a sort through the equality being removed. Only two variables with independent domain-individual evidence are unified; numeric, temporal, reflective, unknown and conflicting sorts retain their comparison. Nested scopes are excluded. An unrelated computed binding may coexist with normalization, while a compute that reads or writes an aliased variable blocks it. Surface rule identity is captured first, identical predicate conjuncts created by the alias collapse to one, and ordinary alpha canonicalization runs afterward. Predicate deduplication is restricted to predicates touching the new alias; unrelated duplicate conjuncts remain unchanged.
flowchart LR
S[Resolved rule with type guards] --> P[Independent sort evidence]
P -->|both domain individuals| U[Unify variables and remove equality]
P -->|otherwise| F[Retain semantic equality filter]
U --> A[Alpha canonicalization]
F --> A
A --> W[Shared rule artifact]
W --> E[Established evaluator]
W --> C[Incremental circuit compiler]
The shared lowering prevents engine-specific semantic drift. The measured market-calendar sequence is 0.338 seconds circuit versus 1.690 seconds Established, a 5.00-times speedup; the preceding circuit run was 21.600 seconds. Across all 11 buildable Sharpe ontology packages, aggregate mutation time is 1.375 seconds circuit versus 11.698 seconds Established, an 8.51-times speedup, with no route fallback or differential mismatch. Circuit construction remains 2.89 times Established across that corpus and is tracked separately from steady-state mutation latency.
The primary circuit selector uses require-circuit mode: catalog or compiler refusal fails construction rather than silently substituting Established. Prefer-circuit mode remains the production rollout policy where correctness fallback is required.
Admission completeness is defined at the production source boundary, not by
the set of defensive errors exposed by the scalar circuit compiler. Every
source-valid rule program that Established can evaluate is a circuit-parity
obligation when every stored catalog fact has positive support. Raw temporal and
modal atoms are dispatched to program components before scalar compilation;
today() is normalized to the explicit evaluation-clock relation; collection
aggregates, temporal well-founded recursion, modal companions, and temporal
mixtures with scalar or aggregate operators are rejected by the language or
Established before circuit admission. Their internal compiler errors protect
layering invariants and are not evidence of a supported-program fallback.
Negative catalog weights remain a distinct state-compatibility refusal because
they do not denote set-valued source facts. Catalog admission preserves that
distinction as typed evidence: nonpositive support and a residual open-world
negation observation cannot collapse into one generic fallback reason. Signed
catalog admission requires exact weight transitions through scans, joins,
distinct support, publication and checkpoint recovery; filtering negative
weights at the circuit input would not match the Established weighted
evaluation semantics. Tests of internal refusal shapes
must identify themselves as defensive-boundary tests; production parity tests
must enter through source elaboration or the whole-program selector and assert
the selected route.
Required negative and transition coverage includes:
- unsupported atom, producer and mixed-program refusal with no circuit state;
- duplicate batch idempotence, conflicting duplicate, frontier gap and stale plan rejection;
- bilateral and aliased join deltas in one batch;
- multiple rule support, cancellation, support overshoot and zero crossings;
- antijoin left-only, right-only and simultaneous zero-crossing changes;
- every aggregate under insert, retract, value replacement and empty-group transitions;
- recursive cycle, diamond, alternative-support, last-support and retract/reassert streams;
- failure after durable append followed by retry, checkpoint replay and full rebuild; and
- module hot swap with concurrent appended batches.
Tests assert route evidence so an oracle cannot pass while silently using full recomputation. The kill switch routes the whole program through the full evaluator without reading or mutating circuit state.
Steady-state benchmarks time delta application only. Parsing, compilation, process startup, state cloning and destruction are reported separately. Each result records total model size, affected frontier size, emitted delta size, arrangement probes, retained-state bytes and mutation-to-visible-frontier latency.
The evaluation-input benchmark isolates dependency selectivity: copy(x)
materializes a large clock-independent relation while evaluation_day(d) alone
depends on today(). It alternates two evaluation days after both maintainers
are constructed. On an Apple M5 Pro with an optimized build, 100,000 retained
rows and 100 rollovers measured 12.292 us circuit p50 versus 100.701 ms
Established p50 (8,192x). At 1,000,000 rows and 20 rollovers it measured
14.625 us versus 1.234 s (84,385x). The circuit work is proportional to the
one affected clock-dependent output; Established reevaluates the million-row
unaffected copy. Reproduce with:
cargo bench -p oxc-reasoning --bench incremental_evaluation_inputs \
--features bench-support -- --rows 1000000 --samples 20
Existing work to reuse
The current arrangement implementation supplies canonical join-key construction, bucket probing and decode-sharing techniques. It must be refactored behind a signed persistent API; its set-membership and caller-managed eviction semantics cannot be copied unchanged.
The current lockstep mutation tests supply the per-frontier full-recompute oracle, route evidence, kill-switch pattern and transitive-closure workloads. The current delete/rederive maintainer remains a differential and performance baseline.
Conservative dependency analysis supplies the required refusal discipline: unknown producers or operators force fallback. Negation memoization supplies referenced-variable projection tests, but persistent antijoin requires signed right-support counts rather than cached Boolean verdicts.