LatticeLawHarness

class LatticeLawHarness<S : Quilted<S>>(val initial: S, val alphabet: List<LatticeOp<S>>, val serializer: KSerializer<S>, val criticalShapes: List<List<String>> = defaultCriticalShapes(alphabet), val floors: VacuityFloors = VacuityFloors.DEFAULT, val replicaCount: Int = 3, val opsPerReplica: Int = 8)

Drives replicaCount replicas (default 3) through opsPerReplica random operations distributed across them, then merges in every possible pairwise order and asserts all replicas converge to the same value.

Two-pass approach:

  1. From initial, each replica builds its own independent history of opsPerReplica local ops.

  2. Every permutation of those replica states is folded into a fresh merge from initial; all must equal the canonical merge (fold in natural order). This exercises commutativity and associativity under random delivery orderings.

Multiplatform: uses Random (seed constructor) for determinism — the same seed produces the same outcome on JVM, wasmJs, and native.

Every permutation is additionally asserted to encode to the same bytes under serializer (#1957) — see assertAllPermutationsConverge.

Scope of the byte assertion — read before trusting a green run. Every comparison it makes is between two encodings produced in one process on one target, so it proves order-independence within a target and nothing more. It does not prove two targets agree on the bytes — that dimension is pinned separately, by the cross-target golden vectors in CanonicalGoldenVectorTest (:kuilt-crdt's commonTest).

More sharply: on JVM and Android this assertion has near-zero discriminating power. The map merges underneath most CRDTs return a HashMap, and java.util.HashMap iterates in bucket order — largely a function of the key set and table capacity, both invariant under the fold order — so a permutation almost always emits identically whether or not the type is canonical. Only largely: putVal appends to the tail of a bin and iteration walks each bin head→tail, so keys that collide into one bucket iterate in insertion order, and there the fold order does show through. A few short ReplicaId keys in a 16-slot table collide rarely enough that this is not something to count on in either direction. Kotlin/Native and Kotlin/Wasm preserve insertion order throughout, which is the fold order, so they see the defect reliably. When you bind a new CRDT to this suite, verify on macosArm64Test or wasmJsTest — a green jvmTest is not evidence of canonicality. (Types whose merge yields a LinkedHashSet, e.g. via Set.plus, are insertion-ordered on the JVM too and do fail there — so a JVM red is meaningful even though a JVM green is not.)

Constructors

Link copied to clipboard
constructor(initial: S, alphabet: List<LatticeOp<S>>, serializer: KSerializer<S>, criticalShapes: List<List<String>> = defaultCriticalShapes(alphabet), floors: VacuityFloors = VacuityFloors.DEFAULT, replicaCount: Int = 3, opsPerReplica: Int = 8)
constructor(initial: S, gen: OperationGenerator<S>, serializer: KSerializer<S>, replicaCount: Int = 3, opsPerReplica: Int = 8)

Bind a type that has not declared an alphabet yet.

Properties

Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard

The alphabet as a uniform random draw — the shape the pool builder consumes.

Link copied to clipboard
val initial: S
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
val serializer: KSerializer<S>

Functions

Link copied to clipboard

measureVacuity over seeds, with every floor in floors asserted — and the measured values returned either way, so a caller can print them on a green run.

Link copied to clipboard

Measure how much the generator actually searched, over the pools of seeds. Asserts nothing.

Link copied to clipboard
fun run(seed: Long): S

Run with a single seed; assert convergence. Returns the converged state.

Link copied to clipboard

Assert both laws that relate the two bracketings of a join, in one pass over causalPool: for every ordered triple, (a ⊔ b) ⊔ c and a ⊔ (b ⊔ c) must be equal (associativity), and — only once they are equal — must encode to the same bytes (canonicality).

Link copied to clipboard

Run runAssociativeLaws over every seed in seeds.

Link copied to clipboard

The codec laws: a state that has been through encode/decode is interchangeable with the one that has not — over causalPool, O(pool²).

Link copied to clipboard

Run runCodecLaws over every seed in seeds, summing what each pool searched.

Link copied to clipboard

Both bracketing laws over every word of length 1..L the alphabet can spell, on one replica — and on failure, the shortest word that breaks them. Returns the number of words searched on a green run.

Link copied to clipboard

The three join laws that are not about bracketing — commutativity, idempotence and least-upper-bound — over causalPool, plus the byte law on the commutativity pair.

Link copied to clipboard

Run runOtherJoinLaws over every seed in seeds.

Link copied to clipboard
fun runSeeds(seeds: LongRange): List<S>

Run over every seed in seeds; returns the converged state for each.