On this page

Resources and payment

Spending two tokens from a balance of five looks simple. A useful contract must also say when spending is permitted, when the payment becomes recorded, and what must finish before another ordinary action can begin. A zero cost makes those distinctions especially clear: the balance can stay unchanged even though payment has occurred.

Read Reading a model for pre-state and post-state notation, and invariants and checking for the kinds of evidence used here.

Calculate the cost before testing affordability

The cost algebra begins with a signed base value, applies increases and reductions, and floors the final result at zero. An intermediate value may be negative. The payable result is nonnegative.

For a base of -2, increases totaling 5 and reductions totaling 1, the final result is 2. Flooring the base early would instead give 4. The cost reference develops that difference and the exact operator:

payment · input revision 3 · CC0 1.0

ModifiedCost(base, increases, reductions) ==
    MaxOf(0, base + SeqSum(increases) - SeqSum(reductions))

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

Knowing the amount answers an arithmetic question. Permission to act and permission to use a particular payment source remain separate conditions. A participant with enough tokens can still be outside the permitted timing window.

Follow one isolated payment attempt

The instructional payment model contains these state fields:

Field	Meaning
available	The participant’s spendable nonnegative balance.
paid	Whether this attempt’s payment has been recorded.
pending	Whether completion work remains for the paid attempt.
declined	Whether the participant declined this attempt.

Init supplies the configured starting funds and clears all three flags:

payment · input revision 3 · CC0 1.0

Init == /\ available = InitialFunds
        /\ paid = FALSE
        /\ pending = FALSE
        /\ declined = FALSE

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

An attempt is ready while none of the flags is set. The cost is fixed by the model’s cost inputs. This example has one payer, one balance and one attempt; it specializes payment obligations rather than interpreting every possible payment procedure in a larger system.

Read the payment step together

For the ordinary model, Pay requires a ready attempt and enough available funds. It debits the exact cost, records payment and makes completion pending in the same transition:

The ordinary configuration fixes LateUse = FALSE. Read paid' = ~LateUse below with that setting: it records TRUE in the post-state. The deliberately defective companion sets LateUse = TRUE, so that same assignment records FALSE until completion.

payment · input revision 3 · CC0 1.0

Pay == /\ Ready
       /\ available >= Cost
       /\ available' = available - Cost
       /\ paid' = ~LateUse
       /\ pending' = TRUE
       /\ UNCHANGED declined

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

With starting funds of five and a cost of two, the ordinary path has the following intended states:

Point	available	paid	pending	declined
Initially	5	FALSE	FALSE	FALSE
After Pay	3	TRUE	TRUE	FALSE
After Complete	3	TRUE	FALSE	FALSE

This table is a worked reading of the contract, not a retained checker trace. There is no ordinary intermediate state in which the debit has happened but payment remains unrecorded.

If funds are insufficient, Pay has no permitted next state. That does not add a “failed payment” that partly spends the balance. A request-processing implementation must reject such a proposal without mutation; that implementation behavior needs its own conformance evidence.

Zero is a payment; decline is a choice

At cost zero, an accepted Pay preserves available but sets paid and pending to TRUE. Something has happened even though the numerical balance is unchanged.

Decline instead applies to a ready attempt, sets declined to TRUE, and records no payment or debit. It does not become a free payment. After either payment or decline, this isolated model does not offer a new attempt by silently clearing history.

An absent cost component is another distinction. It says that the component is not present in the payment description. Removing that component and retaining an explicit zero component need not create the same events. The cost arithmetic alone cannot decide that procedural question.

Finish the completion boundary

While pending is true, the payment is recorded but completion work remains. Complete clears the pending flag and preserves the recorded use and balance. A surrounding procedure must respect this completion boundary before continuing ordinary work.

The behavior specification includes a fairness assumption for Complete:

payment · input revision 3 · CC0 1.0

Spec == Init /\ [][Next]_vars /\ WF_vars(Complete)

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

Here [] means “always,” and WF_vars(Complete) is weak fairness for the completion action over the model’s variables. If completion remains enabled, the behavior may not postpone it forever. This is an explicit scheduling assumption of the example, not a consequence of preserving a nonnegative balance. It does not implement the larger system’s checkpoint work.

Ask whether a property catches the relevant defect

The companion LateUse variant deliberately postpones the paid record until completion. At a zero cost, checking only the balance would not expose that gap. A property about pending payment and its recorded use can distinguish it.

The payment evidence retains both ordinary checks and the intended UseRecorded failures for zero and positive cost, alongside legal witness traces. Each result names its exact configured variant, actual diagnostic and bounds. A passing ordinary run and an intended failure in the companion establish only their stated bounds and assumptions.

Next, follow objects and lifetime to see why payment sources and targets need identities that survive interpretation without being silently reused.