src/transfer/RestorePolicy.bend

mylsm-lsm-store@0.6.0.1 · 35 lines · 8 definitions

1import Base
2
3# Classifies invalid, terminal, and continuing block traversal states.
4type Advance is Data:
5  Invalid{}
6  Finish{}
7  Continue{remaining: Nat}
8
9# Decrements the declared block count exactly once after a validated block.
10def after_block(remaining: Nat) -> Advance:
11  match remaining:
12    case 0n: Invalid{}
13    case 1n: Finish{}
14    case 1n+rest: Continue{rest}
15
16# Returns the number of blocks left in a continuing traversal.
17def remaining(decision: Advance) -> Nat:
18  match decision:
19    case Continue{remaining}: remaining
20    case _: 0n
21
22def write.page.size() -> Nat:
23  16n
24
25def write.pages(entries: Nat) -> Nat:
26  Nat.div(Nat.add(entries, 15n), write.page.size())
27
28def write.fuel(entries: Nat) -> Nat:
29  Nat.add(Nat.mul(3n, write.pages(entries)), 1n)
30
31def max.exchange.bytes() -> Nat:
32  67108864n
33
34def exchange.fits(limit: Nat, size: Nat) -> Bool:
35  Nat.is_le(size, limit)