1	import Base
2	
3	# Selects appending, rollover, or rejection for an exact byte-record size.
4	type Decision is Data:
5	  Append{used_bytes: Nat}
6	  StartNextBlock{record_bytes: Nat}
7	  RecordTooLarge{}
8	
9	def nat.clone.pair(+value: Nat) -> Nat & Nat:
10	  (Nat.mul(1n, value), Nat.mul(1n, value))
11	
12	def decide.rollover(record_bytes: Nat, current_empty: Bool) -> Decision:
13	  match current_empty:
14	    case True{}: RecordTooLarge{}
15	    case False{}: StartNextBlock{record_bytes}
16	
17	# Chooses whether a record fits the current block without exceeding its cap.
18	def decide.current(
19	  used_bytes: Nat,
20	  record_bytes: Nat,
21	  fits_current: Bool
22	) -> Decision:
23	  match fits_current:
24	    case True{}: Append{Nat.add(used_bytes, record_bytes)}
25	    case False{}:
26	      decide.rollover(record_bytes, Nat.is_eq(used_bytes, 0n))
27	
28	def decide.sized.limits(
29	  +used_bytes: Nat,
30	  +record_bytes: Nat,
31	  limits: Nat & Nat,
32	  record_fits: Bool
33	) -> Decision:
34	  match limits:
35	    case (current_cap, comparison_cap):
36	      match record_fits:
37	        case False{}: RecordTooLarge{}
38	        case True{}:
39	          decide.current(used_bytes, record_bytes,
40	            Nat.is_le(Nat.add(used_bytes, record_bytes), comparison_cap))
41	
42	# Rejects a record above the block cap before considering current occupancy.
43	def decide.sized(
44	  used_bytes: Nat,
45	  record_bytes: Nat,
46	  max_bytes: Nat,
47	  record_fits: Bool
48	) -> Decision:
49	  decide.sized.limits(used_bytes, record_bytes, nat.clone.pair(max_bytes), record_fits)
50	
51	def decide.with.max(
52	  used_bytes: Nat,
53	  +record_bytes: Nat,
54	  limits: Nat & Nat
55	) -> Decision:
56	  match limits:
57	    case (record_cap, block_cap):
58	      decide.sized(used_bytes, record_bytes, block_cap,
59	        Nat.is_le(record_bytes, record_cap))
60	
61	# Admits, rolls over, or rejects one record using byte-exact limits.
62	def decide(used_bytes: Nat, record_bytes: Nat, max_bytes: Nat) -> Decision:
63	  decide.with.max(used_bytes, record_bytes, nat.clone.pair(max_bytes))
64	
65	def decide.target.placed(+used_bytes: Nat, +record_bytes: Nat, append: Bool) -> Decision:
66	  match append:
67	    case True{}: Append{Nat.add(used_bytes, record_bytes)}
68	    case False{}: StartNextBlock{record_bytes}
69	
70	# Rejects a record above the hard cap, otherwise appends or starts the next block.
71	def decide.target.sized(
72	  +used_bytes: Nat,
73	  +record_bytes: Nat,
74	  record_fits: Bool,
75	  append: Bool
76	) -> Decision:
77	  match record_fits:
78	    case False{}: RecordTooLarge{}
79	    case True{}: decide.target.placed(used_bytes, record_bytes, append)
80	
81	# Fills blocks up to a target size while admitting any record within the hard cap.
82	def decide.target(
83	  +used_bytes: Nat,
84	  +record_bytes: Nat,
85	  target_bytes: Nat,
86	  max_bytes: Nat
87	) -> Decision:
88	  decide.target.sized(used_bytes, record_bytes, Nat.is_le(record_bytes, max_bytes),
89	    Nat.is_eq(used_bytes, 0n) || Nat.is_le(Nat.add(used_bytes, record_bytes), target_bytes))