Crate coven_merge 

The merge of §8, §9 and §15, as functions with no I/O.

apply implements the merge proof’s incremental step. Its order-free definition is checked in tests. recompute runs the three removal steps over a closed region (proofs/merge.md B9). Values are opaque to the merge. The database supplies CHECK results and unique claims after resolving references, using its own SQL semantics.

Structs

Cell

The winning write and its value in one column (_coven_cells).

Change

A row change carries the generation on the authoring device (§8.3).

ColumnValue

A column’s value and the parent generations recorded with it. The metadata follows the winning setter, including for values kept as lost.

ConstraintColumns

A foreign key’s columns in declaration order (Appendix B.5).

Constraints

CHECK and unique results on merged values after reference substitution.

ForeignKey

A foreign key’s stable identity, independent of SQLite’s positional id (Appendix B.5).

History

A finite, causally closed set of writes satisfying the merge proof’s four assumptions. It is also an in-memory oracle for an applied set. Test support: requires test-utils outside this crate’s unit tests.

InvalidAudience

Text that is neither store nor a circle’s canonical id.

LostKey

A value is identified by the column and write that set it.

LostValue

A value replaced only by writes that had not read it (_coven_lost).

Parent

The parent and odd incarnation a reference names (§9.1).

Provenance

The changes one row change used, in role order: the generation source first, then each replaced setter in the authored column order, then the sources its operations used beyond those, then its foreign-key causes in execution order. A source that fills several roles appears once per role.

Reference

One reference in the merged values, before null substitution.

RemovalResult

Removals and reference readings for a closed region. Replace prior removal records for ALL rows in region, including rows absent from removed, so rows whose reasons cleared come back. Their merged states never change.

RowId

A row is one table, primary key and audience, with generations of its own.

RowState

One table, key and audience’s merged state. Removed rows retain this state; a removal never advances their generation (§8.4).

RowUpdate

The complete new row state and the changes to its lost-value records.

Slot

A positive position in the store’s shared sequence (§5). Slot 0 names nothing: a prefix applied through 0 has applied no slot, and that count stays a plain u64.

SlotPast

A sequence past backed by the consumer’s write-to-slot lookup. latest names the greatest timestamp in the authored prefix and own past, not necessarily the write in its last slot.

SlotRange

The slots from a first one through a last number, in order: empty when the first lies past the last. The last stays a plain number, since 0 (nothing applied) ends an empty range.

Timestamp

§7.2: 48-bit milliseconds, a 16-bit counter, and a 64-bit device id, ordered in that order. No clock is read here.

UniqueClaim

One unique value and the latest claim order of its current input setters.

UniqueConstraint

A unique constraint’s ordered terms and optional partial predicate (Appendix B.5). Column terms use their names; expression terms retain their SQL text.

Write

A decoded write’s merge inputs, independent of its storage encoding.

WriteId

One device’s numbered write (§4).

Enums

Audience

Every synced row reaches the store or one circle (§15).

ClaimOrder

Publication order of a unique value’s input setter (§9.2). Local writes follow every published claim, in their original number order.

Group

Rows competing for one unique value or one key across audiences.

LostChange

A change to the row’s lost-value records, to commit with its merged state.

MergeError

Invalid input to the pure merge; no partially changed state is returned.

OnDelete

The foreign key’s ON DELETE action (§9.1).

Operation

One row’s insert, update or delete. A delete cannot set columns.

ReferenceValue

What a reference reads as in the app’s table. Substitution changes neither its winning write nor its timestamp; lost values stay as written (§9.1).

RemovalRow

The row facts removal reads from merged state, never from prior removals.

Rule

A rule recorded for a removed row. Every rule that holds at the end is included; unique/other-audience rules retain the once-judged decision.

Traits

FullRemovalView

Full row enumeration for comparison with incremental removal in tests.

RemovalView

Abstract database view for the removal rules. All answers are functions of the merged state and applied admin slots, independent of which rows are removed. An adapter can prepare this view in memory; the merge itself performs no I/O.

WriteOracle

Access to applied write metadata. The arriving write is not yet in this view. Implementations must report missing metadata, never invent it, and a failure to read it is their own error, never a missing write. No applied row-change history is required by the incremental step.

WritePast

A causally closed authored past. Its frontier bounds the timestamps of every covered write; sequence order itself is not timestamp order.

Functions

apply

Apply one write to one row (proofs/merge.md B5; Lean step). It touches only the supplied row. All past writes must be applied and the arriving write must be absent from the oracle. Call for each changed row against the same pre-write oracle, then commit all results in the database’s transaction. Parity, future generations, missing metadata and overflow are checked here. A nonzero generation needs a read at least as recent as its earliest recorded changer. That is the locally checkable part of assumption 3: the canonical record cannot tell whether another read write also reached the generation. The authoring database establishes the full witness when producing a change; test histories validate it explicitly. The input state is unchanged on every error path.

generation_present

Whether a row at generation is present: a row starts absent at 0 and each insert or delete advances it, so an odd generation is an incarnation (§8.3).

had_read

The authored prefix plus the author’s earlier originals (§7.1). A later publication never enlarges that prefix.

recompute

Recompute only the rows whose removal a change to touched can change: the touched rows and, through any chain, their children and rivals, in the union of the before/after views. Including old edges releases former losers and children when a claim/reference changes. Their parents and rivals in the after view, closed the same way, are evaluated with them, so proofs/merge.md B9 (Audience.lean, removal_local) gives exactly the full recomputation’s answer there. Every other row’s inputs and dependencies are unchanged, so its removal stands; a parent’s other children are never read. The caller must include admin changes’ rows among touched. No global row enumeration is performed by this function. Each competition group is expanded at most once in each view, so rivals are visited by group membership rather than by every pair of competing rows.

removals

Recompute every row using §8.4’s three steps. The view controls iteration order; no choice of monotone rule order changes the result (proofs/merge.md B8).

resolve_reference

Resolve a winning reference against its parent’s generation, before CHECK and unique evaluation. Substitution affects the app’s row, while lost values retain the written reference (§9.1).

slot

Test support: the slot numbered number, which must be positive.