kuilt-conformance/us.tractat.kuilt.conformance/RetirementReAssertion

RetirementReAssertion

class RetirementReAssertion<S : Quilted<S>>(val subject: String, val asserted: S, val retired: S, val reAsserted: S, val shows: (S) -> Boolean)

The assert → retire → re-assert shape a retiring binding names, plus the evidence that makes it a retirement rather than three unrelated writes.

The three states alone cannot carry that claim. Retirement is not expressible in the join-semilattice algebra: a removal is more information, so s → s.remove(k) moves up exactly as s → s.add(k) does. asserted ⊑ retired ⊑ reAsserted is therefore satisfied by any chain of three additions — which is how the guard used to pass with the shape it exists to protect entirely absent (#2157). So the binding also hands over a reading of its own public value surface: shows, a predicate over one named subject. That predicate is the only thing that can say "retired stopped showing what asserted showed, and reAsserted shows it again".

Type Parameters

the lattice type under test.

Constructors

RetirementReAssertion

constructor(subject: String, asserted: S, retired: S, reAsserted: S, shows: (S) -> Boolean)

Properties

asserted

val asserted: S

A sample that shows subject.

reAsserted

val reAsserted: S

A later sample still that shows it again — the re-assertion.

retired

val retired: S

A later sample that no longer shows it — the retirement.

shows

val shows: (S) -> Boolean

Reads subject off the binding's public value surface — "votes" in it.keys, it.contains("x"), it.store.values.isNotEmpty(). Must be a function of the value, not of object identity; the suite checks that by evaluating it on a freshly joined equal state.

subject

val subject: String

What the three states are about, in one short phrase — key "votes", element "x", the register's value. Appears in the failure message, and forces the binding author to say out loud what it is that gets retired.