State transitions

Replay a bank account’s history, one event at a time, to get today’s balance.

state-transitions.py · output · proof · check · try it in the playground

The question

A bank account opens with 100. Then three things happen, in this order: a deposit of 25, a withdrawal of 40, and a withdrawal of 20.

Nobody writes the balance down after each event. Instead, we keep the list of events and work the balance out from it whenever we need it, the way an auditor replays a ledger.

What is the balance after event 3, and can we see how each event changed it?

What we tell eyekind: the history

# event(Number, Kind, Amount), numbered consecutively from 1.
fact(opening_balance(100))
fact(event(1, 'deposit', 25))
fact(event(2, 'withdraw', 40))
fact(event(3, 'withdraw', 20))

A fact is something we simply state as true. The first says the account opened with 100. The others are the event log: event number, kind of event, amount. The events must be numbered 1, 2, 3, … without gaps, because each balance is worked out from the balance just before it.

Each balance is a state of the account, and each event is a transition: a step from one state to the next.

What we tell eyekind: the rules

implied_by(balance(0, Amount), opening_balance(Amount))
implied_by(
  balance(N, Amount),
  [
    gt(N, 0),
    event(N, 'deposit', Value),
    is_(Before, sub(N, 1)),
    balance(Before, Previous),
    is_(Amount, add(Previous, Value)),
  ],
)
implied_by(
  balance(N, Amount),
  [
    gt(N, 0),
    event(N, 'withdraw', Value),
    is_(Before, sub(N, 1)),
    balance(Before, Previous),
    is_(Amount, sub(Previous, Value)),
  ],
)
query(balance(3, Amount))

implied_by(conclusion, conditions) is a backward rule: the conclusion holds when all the conditions in the list hold. eyekind uses it on demand, only when someone asks about a balance. Capitalized names such as N, Amount and Previous are variables: placeholders that stand for whatever value makes the rule fit.

In everyday words the three rules say:

Inside the rules, gt(N, 0) means “N is greater than 0”. is_(Before, sub(N, 1)) calculates N − 1 and calls the result Before; add and sub are addition and subtraction. The rules refer back to balance itself, one event earlier, so asking for balance 3 leads to balance 2, then 1, then 0.

Nothing is stored and overwritten. Every state is simply one value of balance(N, Amount). The last line, query(...), is the question: which Amount makes balance(3, Amount) true?

What eyekind concludes

// Answers: each instance of a query() that holds.
balance(3, 65)

The first line is a comment saying what follows: the answers to the query. There is one: after the three events, the balance is 65.

The proof, line by line

eyekind --proof writes down how it reached each answer. This is the complete proof:

// Answers: each instance of a query() that holds.
balance(3, 65)

// Clauses: the program clauses the steps cite, by clause number.
clause(1, fact(opening_balance(100)))
clause(2, fact(event(1, 'deposit', 25)))
clause(3, fact(event(2, 'withdraw', 40)))
clause(4, fact(event(3, 'withdraw', 20)))
clause(5, implied_by(balance(0, Amount), opening_balance(Amount)))
clause(6, implied_by(balance(N, Amount), [gt(N, 0), event(N, 'deposit', Value), is(Before, sub(N, 1)), balance(Before, Previous), is(Amount, add(Previous, Value))]))
clause(7, implied_by(balance(N, Amount), [gt(N, 0), event(N, 'withdraw', Value), is(Before, sub(N, 1)), balance(Before, Previous), is(Amount, sub(Previous, Value))]))

// Steps: each goal, what justifies it (a clause, a builtin, a control, or an
// absence or collection taken on trust), the bindings and the goals it uses.
step(balance(3, 65), clause(7), {N: 3, Amount: 65, Value: 20, Before: 2, Previous: 85}, [gt(3, 0), event(3, 'withdraw', 20), is(2, sub(3, 1)), balance(2, 85), is(65, sub(85, 20))])
step(gt(3, 0), 'builtin', {}, [])
step(event(3, 'withdraw', 20), clause(4), {}, [])
step(is(2, sub(3, 1)), 'builtin', {}, [])
step(balance(2, 85), clause(7), {N: 2, Amount: 85, Value: 40, Before: 1, Previous: 125}, [gt(2, 0), event(2, 'withdraw', 40), is(1, sub(2, 1)), balance(1, 125), is(85, sub(125, 40))])
step(gt(2, 0), 'builtin', {}, [])
step(event(2, 'withdraw', 40), clause(3), {}, [])
step(is(1, sub(2, 1)), 'builtin', {}, [])
step(balance(1, 125), clause(6), {N: 1, Amount: 125, Value: 25, Before: 0, Previous: 100}, [gt(1, 0), event(1, 'deposit', 25), is(0, sub(1, 1)), balance(0, 100), is(125, add(100, 25))])
step(gt(1, 0), 'builtin', {}, [])
step(event(1, 'deposit', 25), clause(2), {}, [])
step(is(0, sub(1, 1)), 'builtin', {}, [])
step(balance(0, 100), clause(5), {Amount: 100}, [opening_balance(100)])
step(opening_balance(100), clause(1), {}, [])
step(is(125, add(100, 25)), 'builtin', {}, [])
step(is(85, sub(125, 40)), 'builtin', {}, [])
step(is(65, sub(85, 20)), 'builtin', {}, [])

It has three parts:

Two kinds of justification occur:

Read the steps as sentences:

  1. Balance 3 is 65, by rule 7 (withdrawal) with N = 3, Value = 20, Before = 2, Previous = 85: 3 is greater than 0, event 3 withdraws 20, 3 − 1 = 2, balance 2 is 85, and 85 − 20 = 65.
  2. 3 is greater than 0: a calculation.
  3. Event 3 withdraws 20: fact 4.
  4. 3 − 1 = 2: a calculation.
  5. Balance 2 is 85, by rule 7 with N = 2, Value = 40, Before = 1, Previous = 125: because balance 1 is 125 and 125 − 40 = 85.
  6. 2 is greater than 0: a calculation.
  7. Event 2 withdraws 40: fact 3.
  8. 2 − 1 = 1: a calculation.
  9. Balance 1 is 125, by rule 6 (deposit) with N = 1, Value = 25, Before = 0, Previous = 100: because balance 0 is 100 and 100 + 25 = 125.
  10. 1 is greater than 0: a calculation.
  11. Event 1 deposits 25: fact 2.
  12. 1 − 1 = 0: a calculation.
  13. Balance 0 is 100, by rule 5 with Amount = 100, because the opening balance is 100.
  14. The opening balance is 100: fact 1; it uses nothing.
  15. 100 + 25 = 125: a calculation.
  16. 125 − 40 = 85: a calculation.
  17. 85 − 20 = 65: a calculation.

Read from the bottom of the ledger up, this is the replay: 100, then 125, then 85, then 65. Every step leans only on steps that do not lean back on it.

Checked: what the report says

A proof is only worth something if someone else can check it. eyekind -c generates the proof and checks it against the program; --check-proof checks a saved proof. The checker never reasons by itself: it only confirms each step against the program. This is the complete report:

// Checked answers: these follow from the input program.
balance(3, 65)

// C1-C8: resolution, acyclicity, justification, coverage,
// re-decision, boundary consistency, relevance and witness integrity.
condition('C1', 'resolution', 'ok', 8)
condition('C2', 'well_founded', 'ok', 17)
condition('C3', 'justification', 'ok', 17)
condition('C4', 'coverage', 'ok', 17)
condition('C5', 're_decision', 'ok', 9)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 18)
condition('C8', 'witness_integrity', 'ok', 0)

// Proof statistics: recorded steps and how they were checked.
steps(17)
verified(8)
recomputed(9)
composed(0)
trusted(0)
claims(1)

// This verdict applies to the claims above; it does not establish completeness.
verdict('checked')

Each condition line names a check, says 'ok', and counts what it looked at:

The statistics repeat this: 17 steps, 8 verified against the program, 9 recomputed, none taken on trust. The verdict is checked: a balance of 65 after event 3 follows from the program. As the last comment says, this confirms the claim; it does not say there could be no other answers.

Try it

eyekind examples/state-transitions.py            # the answers
eyekind --proof examples/state-transitions.py    # answers with their proof

Or open it in the playground. Things to try on a copy of the program:

Takeaway

An audit trail you can trust: the final number comes with every intermediate balance and every calculation that led to it, each one rechecked.