1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
# req-070
Given a bucket, `bucket`, if the procedure
`is_bucket_balance_up_to_date(bucket)` as described in req-035 returns TRUE,
then `bucket.balance` is equal to the difference between the amounts of the
drips into it and the amounts of the transactions out of it.
Sources: req-036, ass-008
Satisfied by: req-030, req-070, req-071, req-072, req-073
## Proof
Grant req-030, req-070, req-071, req-072, req-073.
Let `bucket` be a bucket, and suppose that
`is_bucket_balance_up_to_date(bucket)` as described in req-035 returns TRUE.
It follows that:
- `bucket.balance_cache_key` is of the form `<string>:<string>`
- The first part is the ID of a drip: call it `drip`
- There is no `drip_2` such that `drip_2.timestamp > drip.timestamp`
- The first part is the ID of a transaction: call it `transaction`
- There is no `transaction_2` such that
`transaction_2.timestamp > transaction.timestamp`
Given req-071, when `bucket.balance_cache_key` was last set to this value,
running `calculate_bucket_balance(bucket)` immediately afterwards would have
left `bucket.balance_cache_key` and `bucket.balance` unchanged, even under the
pretence that `is_bucket_balance_up_to_date(bucket)` returns FALSE.
Given req-030, running `calculate_bucket_balance(bucket)` at that time under
that pretence would have set `bucket.balance` to the difference between the
amounts of the drips into the bucket and the amounts of the transactions out of
the bucket.
Since there is no `drip_2` such that `drip_2.bucket_id = bucket.id` and
`drip_2.timestamp > drip.timestamp`, it follows that there are no more drips
into the bucket now than there were then. Symmetrically, it follows that there
are no more transactions out of the bucket now than there were then.
Given req-072, it follows that there were no more drips into the bucket then
than there are now.
It follows that there are the same drips into the bucket then and now. It
follows from that, given req-072, that the amounts of the drips into the bucket
are the same now as they were then.
Given req-073, and the assumption that the time we are considering is the last
time `bucket.balance_cache_key` was set, it follows that no transactions have
been deleted or updated since then, and so it likewise follows that the amounts
of the transactions are the same now as they were then.
It follows that the difference between the amounts of the drips into it and the
amounts of the transactions out of it has not changed since then. Since that is
ex hypothesi equal to the value of `bucket.balance` which was set at that time,
and since ex hypothesi that is the same value of `bucket.balance` which obtains
now, it follows that `bucket.balance` is equal to the difference between the
amounts of the drips into the bucket and the amounts of the transactions out of
the bucket. QED.
|
