Selected scope and correspondence¶
The full reference preserves one fixed asymmetric profile. Its source inventory contains 2,502 selected top-level contracts, 1,029 explicitly selected nested helpers, 16 semantic roots and nine subject families. The three teaching packages are separate authored specializations with their own evidence.
The source browser can also show supporting model definitions and instantiated aliases. Its larger entry count does not enlarge the accepted contract denominator. Other fixture-local helpers remain complete in their owning definitions and exact module downloads; dependency listings preserve paths through those helpers.
What the finite comparisons establish¶
The selected reference has 67 public configurations: 58 completed ordinary checks and nine intended negative controls. Among the positive configurations, 35 have actual state-changing transitions and 23 are prepared assertion fixtures. Their result records retain the configured specifications rather than inferring class from a module name.
The corresponding source comparison investigates complete typed state sets, initial sets and labelled-transition multisets for those same finite profiles. Each of the nine deliberately defective variants reaches its intended named invariant failure. These comparisons retain the configured inputs and typed mapping; matching counts alone would be insufficient.
The profiles overlap. Adding their state counts does not produce the state count of a combined game. Nor do their successful outcomes establish every possible instance size, external provider or branch.
Source preservation is distinct from measured reachability¶
The frozen inventory also contains 4,849 candidate branch boundaries. This is a mechanical token inventory, not proof that every consequential semantic branch was identified or executed.
A preserved-unexercised disposition means the exact mapped boundary remains in the retained source, with an explicit absence of individual execution measurement. It does not mean the branch was removed, implemented later, or reached by every associated model. Every selected contract and nested helper remains inspectable.
The contract inventory records associated configurations, source destinations, reviews and context limits. A family association identifies the relevant evidence; it does not turn a passing family result into an arbitrary-argument theorem for each helper.
Retained context limits¶
Context |
Preserved scope |
Limit |
|---|---|---|
Typed values |
Selected integers, Booleans, sets, records, tuples and finite functions, with explicit typed keys and values. |
General unsupported runtime classes and arbitrary outside-domain values are not covered. |
Atomic labels |
One consistent finite mapping for registered labels, record keys, reflected domains and admitted computed labels. |
Whole-label relabelling does not preserve arbitrary observations of a string’s characters. |
Sequences |
Proper sequences of typed elements, including deck/order inputs and canonical name-part tuples. |
A primitive string is a separate carrier; arbitrary character-level sequence applications are not included. |
Constructed labels |
Recorded finite seat/zone/event combinations and registered example/copy suffixes. |
Other constructors or unconstrained inputs need their own mapping obligations. |
Renderer guards |
The exact pinned TLC rendering shapes exercised by registry checks. |
|
Choice |
The finite choices actually explored and predicates that identify unique minima or indices. |
Nonunique generic |
Providers |
The selected metadata, legality, activity, authorization, payment and return witnesses. |
A true witness flag is not an independently implemented interpreter or arbitrary-provider correctness proof. |
The full payment interface illustrates a material provider boundary: PaymentValid leaves its candidate argument unexamined. DoPay commits the supplied candidate, relying on the provider-established procedureValid and other witnesses. A true flag alone does not establish a correct debit or complete payment. The registry profile likewise keeps its supplied default-activity specialization explicit, including SourceDefaultActivitySA = FALSE in the selected adapter context.
Synthetic example families select explicit equations and structured facts. An opaque sourceSHA value in a fact adapter remains a historical equality/provenance token. It does not certify a newly authored item catalogue or supply executable text. See the vocabulary guide.
Tool and interpretation qualifications¶
The identity-control configurations use the same complete state-variable set with control fields first in the stuttering/fairness tuple. This avoids a pinned TLC evaluation-order failure involving heterogeneous location values; it does not add a new gameplay rule or waive liveness checking. The actual tuple override is visible in each configuration record.
Large assertion fixtures explicitly receive the recorded larger heap bound. An earlier out-of-memory attempt remains failed evidence. Likewise, the retained operation fixture warning about an absent-field EXCEPT update is a no-op qualification, not successful mutation sensitivity; its distinct guard control supplies the intended negative result.
Project source, source interpretation, neutral correspondence, finite model checking, implementation conformance, complete-game execution and universal theorem proof remain separate claims. This release has no admitted unbounded theorem-proof or complete-engine result. Use each exact result’s source, assumptions, warnings and reproduction bundle when deciding whether it supports another use.