Accounting Method: Credits Stored on Operations
What This Concept Is
Accounting assigns charges to operations and stores unused credit to pay future work. A valid proof never spends credit that was not earned under its initial conditions. Credits may be attached to elements, bits or a global account; they are proof bookkeeping rather than runtime fields you must implement.
Why It Matters Here
The cost unit determines the credit charge. Counting a move between two stacks as one event differs from counting its pop and push separately. Both models can be useful, but combining their numbers invalidates the proof.
Concrete Examples
Stack multipop. Charge each push 2 under a model with unit push/pop work: pay 1 to push and leave 1 on the element for its eventual pop. Each element can be popped once. Include fixed per-call overhead for an empty multipop; a zero-element operation need not have literally zero machine cost.
Binary counter. On increment, pay for the zero-to-one flip and place one credit on that new one bit. A one-to-zero flip consumes its stored credit. Charging 2 per increment bounds the number of flips from an all-zero counter, with a declared overflow policy. Bit flips are not automatically equal to arbitrary-precision integer runtime cost.
Two-stack queue. Count each stack push/pop as one unit. Enqueue costs
1 and can be charged 3: two credits wait with the input-stack element for
its later pop from In and push to Out. Dequeue costs one additional pop
from Out, charged 1. Each element transfers at most once. If a dequeue
transfers k elements, its actual primitive count is 2k+1, not k+1 in
this model. The credit ledger pays the 2k transfer work.
Common Confusion / Misconceptions
Accounting and potential methods are not a hierarchy of truth or a claim that some structures forbid credits. A potential often summarizes the same outstanding credit. A charge chosen to fit one sample trace is not a proof that every future prefix stays solvent.
How To Use It
Choose primitives, state the initial credit and explain when each credit is created/spent. Check every legal operation, including empty and invalid operations under the API. Construct an adversarial sequence that delays spending credits, then verify the ledger still covers the eventual burst.
Check Yourself
Why does each queue element need two transfer credits in the primitive model? How would the proof change from a nonempty input stack? Why should empty-operation overhead be stated?
Mini Drill or Application
Enqueue three values then dequeue all three. Feedback: 3 enqueue pushes, 6 transfer primitives, 3 output pops = 12 actual primitives. Charges 3 per enqueue and 1 per dequeue total 12.
Read This Only If Stuck
CLRS: accounting examples. Translate all charges into the same primitive units before comparing two derivations.