On this page

Cost algebra and payment boundaries¶

The cost contract combines a signed base with increases and reductions, then floors the final result at zero. It defines the amount. Payment permission, source eligibility, atomic commitment and completion are separate obligations.

For a guided introduction, read resources and payment. For the meaning of a finite checking claim, read invariants and checking.

Final modified cost¶

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

ModifiedCost takes a base value and sequences of increases and reductions. Sum the increases, sum the reductions, combine them with the base, and floor that combined value once at zero.

Part	Contract meaning
Base	A signed starting amount.
Increases	The admitted increase amounts, combined before the final floor.
Reductions	The admitted reduction amounts, subtracted before the final floor.
Result	The combined amount if positive, otherwise zero.

The operator does not decide which modifiers are applicable or who may supply them. Those decisions belong to the surrounding rule and its inputs. The returned amount does not itself authorize an action.

Worked arithmetic cases¶

These are authored evaluations that explain the contract, not reports of a model-checker run.

Base	Total increases	Total reductions	Combined intermediate	Final amount
3	2	1	4	4
3	0	5	-2	0
-2	5	1	2	2
0	0	0	0	0

The third row exposes early flooring. Clamping its base to zero before adding increases and subtracting reductions produces four, which differs from the contracted result of two. Clamping after each reduction can also make the order of otherwise combined modifiers matter. The final floor belongs after the complete calculation.

The arithmetic may use signed intermediates without allowing a negative payable cost or a negative spendable balance. These are different domains with different roles in the specification.

Zero, absence and decline¶

An explicit zero component remains a component of a payment description. An absent component is not present in that description. A declined payment is a participant’s choice about an attempt. These three cases can have different event and permission consequences even when none removes tokens.

The instructional payment model makes the zero-versus-decline distinction observable:

Outcome	Balance change	`paid`	`pending`	`declined`
Accept a zero payment from the ready state.	None.	`TRUE`	`TRUE`	`FALSE`
Decline from the ready state.	None.	`FALSE`	`FALSE`	`TRUE`

The model’s pending flag records that paid work has not completed. Completion clears that flag and preserves the use record. An implementation must not infer whether payment occurred solely from the balance difference.

Admission and atomic commitment¶

Before accepting payment, a procedure must establish the applicable amount, payment permission, eligible sources and full affordability. A valid source may need to belong to the payer or carry an explicit exception; a numerical balance alone cannot establish eligibility in a richer source model.

The small released example specializes those obligations to one nonnegative balance and one isolated attempt. Its ordinary Pay action commits the debit and use record together. Insufficient funds produce no permitted Pay successor. A false action predicate does not create a partially paid state or an automatic state-changing error transition.

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

This specialization is not a general interpreter for compound costs, replacement effects, permission-changing sources or every surrounding ability procedure. A wider model that accepts supplied validity witnesses must identify what the supplying evaluator is assumed to establish.

Completion and repeated use¶

The payment example preserves its paid or declined history for the isolated attempt. It does not reset itself into a new attempt. In a surrounding procedure, reopening a window or returning from child work must not silently erase that history.

A completion boundary separates accepted payment from readiness to continue. Safety properties can ask whether every pending ordinary payment already has its use recorded, whether the balance stays nonnegative, and whether commitment can repeat. A progress property asking that completion eventually happens also needs the model’s scheduling and provider assumptions.