r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope
On this page

Characteristics and their context

A card’s metadata, its current object state and the value used by an instruction are different things. Metadata may describe a printed number. The current object may have lost access to its printed characteristics. An instruction may then need an effective value after an explicit substitution or adjustment.

Read zones and setup for the initial metadata and object context, and costs for the separate calculation of a payable amount. These contracts describe a particular two-seat reference profile; they do not define a universal schema for every card game.

Start with well-shaped inputs

The metadata is a finite table indexed by physical card identifiers. A current object refers to one of those identifiers and carries its own form, kind, location and face information. A lookup such as cardData[o.card] requires that the key exists. A function that reads a field is not automatically a total validator for arbitrary TLA+ values.

Characteristic values also have distinct domains:

Input

Expected meaning

Canonical name parts

A sequence of canonical strings supplied in metadata.

A numeric part

A record containing present, isX and a signed integer amount.

Printed subtypes

A set drawn from the profile’s subtype vocabulary.

Subtype counts

A finite function from subtype labels to nonnegative counts.

Object context

Current form, kind, location, face and any explicit conversion or effect inputs.

These validators and value projections are not state transitions: evaluating a characteristic does not spend a balance, finish an instruction or change an object’s controller. The enclosing procedure supplies the current context, applicable adjustments and permission to use the result. It also distinguishes the owner, source controller and effect executor, and projects only the information the observer may inspect.

These domains matter to source correspondence. Sequence operations are applied to typed elements. Renaming a whole atomic label does not establish that arbitrary operations on the characters of its spelling are preserved.

A number can be absent, fixed or supplied later

An absent number and a present zero are represented differently. The number-part validator also reserves a placeholder amount of zero for a supplied X value:

reference-profile · input revision 2 · CC0 1.0

NumberPartValid(p) ==
    /\ p.present \in BOOLEAN /\ p.isX \in BOOLEAN /\ p.amount \in Int
    /\ (~p.present => ~p.isX)
    /\ ((~p.present \/ p.isX) => p.amount = 0)

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

The present field answers whether the characteristic exists. isX answers whether its value must be supplied in context. amount stores the fixed integer only when that is the relevant case. An absent part cannot also be an X part.

NumberValue projects a value for payment or another use. A fixed part returns its stored amount. A supplied X uses the announced amount for payment and zero outside payment. Permission to announce that amount, and any restriction on it, remains a separate obligation.

For an authored example, compare an absent part, a present fixed zero, and a present X with an announced payment value of three. Their numerical projections may be 0, 0 and 3, but the first two still disagree about existence. Replacing every absent part with a present zero would lose information used by later procedures. This is an explanatory calculation, not a retained execution.

A signed stored value also differs from a nonnegative payable cost. The final floor described in the cost reference is a later operation; it should not be inserted into every metadata lookup.

Route each value to its consumer

The same numeric-part representation serves different questions. Keep the question attached to the value instead of treating every displayed number as a payment:

Characteristic

Consumer and boundary

progress requirement

A threshold against the relevant counter count; satisfying it does not itself authorize scoring.

Objective points

A contribution from eligible objectives in the appropriate objective area; a game outcome is recorded at its ending boundary.

Strength

An effective comparison value, separate from whether the interacting abilities are permitted.

Capacity demand and starting capacity

A requirement and a supply. A default starting value applies when the relevant profile has no specified starting value.

Deck minimum and import budget

Deck-construction inputs for the applicable profile face and context, with policy checks supplied separately.

Base connection and deployed contributions

Inputs combined into a connection value, with their applicable adjustments supplied explicitly.

For exact context selection, follow ProfileStartingCapacity and ProfileDeckValues. For the point-total boundary, continue with turns. Affiliation, type and uniqueness metadata also constrain their respective consumers; recording a uniqueness marker alone does not enforce a global restriction on controlled objects.

Name equality does not replace object identity

Canonical name parts provide a comparison value. They do not allocate an object identifier, and these operators do not normalize arbitrary language or typography into a canonical form. That normalization is an input responsibility.

A reference to the source object and a reference to all objects with a matching name select different sets:

reference-profile · input revision 2 · CC0 1.0

NameReference(isSelf, source, objects, names, name) ==
    IF isSelf THEN {source} \cap objects ELSE CopiesOfName(objects,names,name)

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

As an authored example, suppose live objects 11 and 12 have equal canonical name values. A name comparison can select both. A self-reference to object 11 selects only 11, if it is still in the supplied object set. It does not silently retarget object 12, or a later successor of 11, just because their metadata agrees. See objects and lifetime for explicit successor references.

Effective subtypes use counts before membership

Printed membership supplies the starting count. Gains add counts, losses subtract them, and a subtype is effective only while its balance is positive:

reference-profile · input revision 2 · CC0 1.0

EffectiveSubtypes(base, gains, losses) ==
    {t \in Subtypes2 : SubtypeBalance(base,gains,losses,t) > 0}

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

For an authored example with an admitted subtype label t, a base count of one, one gain and one loss leaves t present. One loss with no gain removes it. The calculation uses counts before producing a set, so it preserves information that a sequence of simple set insertions and deletions could erase.

The surrounding CardSubtypesForView contract chooses the appropriate base, including an explicit conversion case. It also checks whether the current object retains printed characteristics. In this profile, a deployed facedown SideB card does not expose its printed type/subtype characteristics through those projections. Knowing which physical card it is does not bypass that context rule.

Keep characteristics, activity and observation separate

A characteristic lookup is not permission to execute an ability. Default activity depends on game start and current object state; an explicit exception may alter an ability’s activity. An operation’s executor may differ from its source controller. Those questions need their own guards before a calculated strength, capacity demand or point value is used.

Text metadata likewise distinguishes rule-bearing segments from other presentation. GameplayTextProjection selects the supplied rule representations; it does not parse arbitrary prose or establish that those representations implement every instruction. Presentation fields and artwork positions do not perform gameplay work.

Likewise, the model’s internal metadata is broader than a participant’s permitted observation. Current visibility decides which identities or fields a participant may inspect. A public count, a visible face and permission to read underlying metadata are not interchangeable facts.

Consult schema and setup evidence for the exact selected inputs and scope of each result. A model association does not show that every characteristic operator or branch was reached. The supplied metadata, context values and effect interpretation remain explicit boundaries of the contracts described here.