Formal Card-Game Systems
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

Payment descriptions, supplied candidates and commitment

The cost reference calculates an amount. The payment lesson then implements one wallet and one isolated attempt. This entry describes the larger reference profile’s payment interface, including obligations that it deliberately receives from a provider.

Preserve the component description

A payment can contain components with different categories and kinds. Ignoring deployment costs, ignoring resource-unit costs and ignoring every cost are distinct requests. The component filter retains the order of components that remain:

reference-profile · input revision 2 · CC0 1.0

EffectiveCosts(costs, ignoredCategories, ignoreResourceUnits, ignoreAll) ==
    SelectSeq(costs, LAMBDA c :
        ~IgnoreComponent(c, ignoredCategories, ignoreResourceUnits, ignoreAll))

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

The input is a sequence of well-shaped component records. Each component needs the fields consumed by the filter. The operator does not decide whether an instruction has permission to ignore those costs; it applies the supplied ignore settings. Nor does it remove a component just because its amount is zero.

For an authored example, consider a zero resource-unit component followed by a non-resource additional component. Ignoring resource-unit costs removes the first component and retains the second. With no ignore setting, the explicit zero remains in the description. This is a calculation explaining the contract, not a retained execution.

An inherent cost can also be applicable but absent. The separate applicable, exists and amount fields preserve that distinction. A present zero amount must not be substituted for every absent cost.

Admission consumes explicit witnesses

The runtime interface receives a payer, selected object identifiers, a proposed after-state and an evidence record:

reference-profile · input revision 2 · CC0 1.0

PaymentValid(t, p, bundle, candidate, evidence) ==
    /\ evidence.announced                                                   
    /\ evidence.full /\ evidence.restrictionBefore /\ evidence.restrictionAfter
    /\ ~evidence.mandatoryPrevents /\ ~evidence.staticPrevents
    /\ evidence.additionalAccepted
    /\ bundle \subseteq DOMAIN t.obj
    /\ \A i \in bundle : CanPayWith(t, p, i, i \in evidence.controlExceptions)
    /\ evidence.procedureValid

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

Read each conjunct as a separate obligation. Announcement and full payment, restrictions before and after payment, prevention, acceptance of additional costs, source membership, control exceptions and procedure validity have distinct roles. CanPayWith also excludes virtual units and requires the relevant control or exception.

These guards assume well-shaped records and identifiers at the places they read fields. They do not make the operator total over arbitrary TLA+ values.

The proposed candidate state is supplied by the surrounding procedure. In this interface, PaymentValid does not derive a debit from that state or independently prove every effect of payment. Its procedureValid input represents an obligation on the supplying evaluator. Setting a Boolean to true is not evidence that an arbitrary candidate is a correct payment implementation.

The wallet lesson specializes that boundary into a concrete debit and use-record transition. Its no-overspend and delayed-use results remain scoped to that specialization. The full-profile configurations supply their own concrete candidate states and witnesses.

Commitment is one transition

reference-profile · input revision 2 · CC0 1.0

DoPay(c) ==
    /\ PaymentValid(s, c.player, c.bundle, c.candidate, c.evidence)
    /\ s' = Commit(s, [c.candidate EXCEPT !.checkpointDue = TRUE], "Pay")

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

If admission fails, this action has no permitted successor. If it succeeds, the action passes the supplied candidate through Commit, marks a checkpoint as owed and records the payment event. The state is not exposed through an intermediate partially committed transition in this action.

Commit also handles newly active objects and their configured recurring units. Those effects depend on the current object set, metadata and control rules. It is more than a numerical subtraction, and its consumers must retain those dependencies.

Owed work constrains dispatch

reference-profile · input revision 2 · CC0 1.0

CheckpointOrderAllows(t, c) ==
    IF ~t.checkpointDue \/ c.op = "Checkpoint" THEN TRUE
    ELSE IF c.op = "CardOverride"
         THEN CardOverrideAuthorized(c) /\ CheckpointOverrideAllowed(t, c)
         ELSE FALSE

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

When a checkpoint is owed, ordinary dispatch is blocked. The checkpoint itself is admitted, and an explicitly authorized override has its own guarded exception. Clearing a flag outside those conditions is not an alternative implementation of the contract.

This dispatch guard does not supply the checkpoint’s cleanup, reactions or exact caller return. Continue with checkpoints and composition for those boundaries.

Consult cost and payment evidence for the configured calculations, procedures and controls. Complete source preservation and selected finite checks do not establish arbitrary provider validity, unrestricted cost interpretation or a general payment engine.