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

Ability definitions, instances and returns

An ability definition classifies work and identifies its source. A resolution instance binds one occurrence to a cursor, timing context and caller. Current availability, execution progress and recorded use are additional predicates with different boundaries.

For the guided explanation, read abilities and use. For withdrawal and restoration, read availability and lifetime.

Establish the definition’s shape and context

Inputs include an admitted ability kind, structured instruction sequence, source, controller, activity metadata and any supplied interpretation of restrictions. Instruction identifiers are typed sequence elements. Metadata strings are labels within the relevant carrier; the module does not parse arbitrary prose into a complete executable definition.

The basic shape rule distinguishes static definitions from categories with instructions:

reference-profile · input revision 2 · CC0 1.0

AbilityShape9(kind,instructions) ==
 kind \in AbilityKinds9 /\ IF kind = "Static" THEN Len(instructions) = 0 ELSE Len(instructions) > 0

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

A static ability category has no executing instruction sequence here. A conditional definition can separately have a state-based primary condition; that remains an instance-producing conditional mechanism, with its own recognition and retry guards. These two uses of state-dependent behavior should not be conflated.

Interrupt classification is another question. The interrupt flag and the supplied structure of an instruction can require interrupt handling without replacing the ability’s category, source or instance identity.

A source is a relationship, not a physical-name lookup

The source relation distinguishes printed, granted, lingering and rule origins:

reference-profile · input revision 2 · CC0 1.0

AbilitySource9(origin,printedObject,recipient,effectCreator,rule) ==
 CASE origin = "Printed" -> ObjectAbilitySource9(printedObject)
   [] origin = "Granted" -> ObjectAbilitySource9(recipient)
   [] origin = "Lingering" -> ObjectAbilitySource9(effectCreator)
   [] origin = "Rule" -> RuleAbilitySource9(rule)

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

A granted ability uses its recipient as the source under this relation. A lingering origin identifies its effect creator. A rule source has a different shape from an object source. None of these relationships makes the source’s physical owner the executor of every effect automatically.

An authored example is an ability granted by object 11 to object 12. Under the granted-origin branch, the source relationship names recipient 12. Replacing that relationship with the grantor’s identifier would change later activity, use provenance and self-reference questions. This explains the branch; it is not a reported execution.

Object references also retain their lifetime rules. Equal physical names do not authorize substitution after an object is renewed. Hosting and source-zone relationships must be checked where an instruction relies on them.

Distinguish presence, activity and permission to choose

AbilityActive9 first checks effective presence, then applies the relevant provider/source/activity branches. It includes explicit exceptions for particular contexts rather than deriving all activity from a face-up flag.

For example, a rule source relies on current rule permission. Object sources use current object data and their relevant exceptions. Facedown SideB objects have their own restriction. Departure holds and persistent or lingering membership are supplied through specific context records; they are not blanket permissions for all inactive sources.

Even an active ability still needs the appropriate timing, controller, target and affordability conditions before it can be chosen. An internal activity calculation also grants no right to publish hidden source metadata to an opponent.

Recognize conditional occurrences at a specific observation

A conditional definition and a recognized instance are different values. The instance captures a definition copy, checkpoint/occurrence identity and activity epoch. CheckpointCandidates96 separates trigger-pattern/stipulation checks from the state-based primary branch and its sibling/throttle conditions.

Recognition consumes supplied condition results tied to the relevant definition and snapshot. It is not a free-standing evaluator for every possible requirement. Later resolution also checks that the pending instance is still current and belongs to the proper window before beginning its instruction work.

A restored definition therefore does not automatically restore an older lost pending instance. A detached, already-started procedure has a different continuation contract from a pending offer.

Use the cursor and matching instruction receipt

An instance records its instructions, cursor, source zone, caller and phase. Its first instruction becomes imminent only under the source and scheduling guards. An interrupt boundary precedes resolution where required.

FinishAbilityInstruction9 requires a complete receipt for this instance and the instruction at its current cursor. Between instructions, the caller must wait for the appropriate checkpoint and newer chains before advancing. The frame’s local EXCEPT updates preserve its other fields; composition must also constrain the rest of the state.

For an authored example, a receipt for instruction 42 cannot complete cursor position one of <<41, 42>>. A receipt for the right instruction but another instance is also insufficient. Correct names of stages or fields cannot replace identity matching.

Record use and return at their separate boundaries

AbilityUseDue9 ties paid use to actual trigger payment and distinguishes optional effects/choices in other branches. Recognition, selection, payment and optional execution are not synonyms. A once-per-turn check needs the associated turn/source history rather than a newly cleared window flag.

After final instruction completion, return still waits for the final checkpoint and chains:

reference-profile · input revision 2 · CC0 1.0

ReturnAbility9(before,after,actualFinalCheckpointAndChainsComplete,caller) ==
 /\ before.complete /\ ~before.returned /\ actualFinalCheckpointAndChainsComplete /\ caller = before.caller
 /\ after = [before EXCEPT !.returned = TRUE]

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

The caller must match and the instance must not already have returned. A source departing does not manufacture that receipt. Conversely, a valid detachment boundary can permit continuation while leaving current target and effect checks in force.

The abilities evidence states the actual assertion and transition-driver scopes. The supplied syntax, eligibility, interpretation, payment and scheduling interfaces remain part of the meaning of each checked case. These contracts are not an unrestricted ability-language implementation or an unbounded proof of all interactions.