1	import Base
2	
3	# Stores exact visible record and payload totals.
4	type Stats is Data:
5	  Stats{entries: Nat, payload_bytes: Nat}
6	
7	# Reports a deterministic aggregate after one logical key mutation.
8	type Decision is Data:
9	  Applied{stats: Stats}
10	
11	# Adds a previously absent live key and its encoded payload.
12	def added(current: Stats, key_bytes: Nat, value_bytes: Nat) -> Decision:
13	  match current:
14	    case Stats{entries, payload_bytes}:
15	      Applied{Stats{Nat.add(entries, 1n),
16	        Nat.add(payload_bytes, Nat.add(key_bytes, value_bytes))}}
17	
18	# Preserves totals when a mutation leaves a key absent.
19	def unchanged(current: Stats) -> Decision:
20	  Applied{current}
21	
22	# Removes one visible key, its key bytes, and its old value bytes.
23	def removed(current: Stats, key_bytes: Nat, value_bytes: Nat) -> Decision:
24	  match current:
25	    case Stats{entries, payload_bytes}:
26	      Applied{Stats{Nat.sub(entries, 1n),
27	        Nat.sub(payload_bytes, Nat.add(key_bytes, value_bytes))}}
28	
29	# Replaces a value without changing the visible key count.
30	def replaced(current: Stats, old_bytes: Nat, new_bytes: Nat) -> Decision:
31	  match current:
32	    case Stats{entries, payload_bytes}:
33	      Applied{Stats{entries, Nat.add(Nat.sub(payload_bytes, old_bytes), new_bytes)}}
34	
35	# Applies the visible effect of one key's before and after states.
36	def apply(
37	  current: Stats,
38	  key_bytes: Nat,
39	  before: Maybe<&1, Nat>,
40	  after: Maybe<&1, Nat>
41	) -> Decision:
42	  match before:
43	    case None{}:
44	      match after:
45	        case None{}: unchanged(current)
46	        case Some{new_bytes}: added(current, key_bytes, new_bytes)
47	    case Some{old_bytes}:
48	      match after:
49	        case None{}: removed(current, key_bytes, old_bytes)
50	        case Some{new_bytes}: replaced(current, old_bytes, new_bytes)
51	
52	# Projects aggregate totals from a successful mutation decision.
53	def result(decision: Decision) -> Stats:
54	  match decision:
55	    case Applied{stats}: stats
56	
57	def clone.nat(+value: Nat) -> Nat & Nat:
58	  (Nat.mul(1n, value), Nat.mul(1n, value))
59	
60	def clone.fields(
61	  entries: Nat & Nat,
62	  payload_bytes: Nat & Nat
63	) -> Stats & Stats:
64	  match entries:
65	    case (entries_left, entries_right):
66	      match payload_bytes:
67	        case (payload_left, payload_right):
68	          (Stats{entries_left, payload_left}, Stats{entries_right, payload_right})
69	
70	# Rebuilds independent copies of the exact aggregate totals.
71	def clone(+stats: Stats) -> Stats & Stats:
72	  match stats:
73	    case Stats{+entries, +payload_bytes}:
74	      clone.fields(clone.nat(entries), clone.nat(payload_bytes))