proofs/containers/bitset/depth.bend
bend-collections-laws-containers@1.0.0.0 · 48 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/index.bend as IX
7
8# `B.depth_for(n)` picks the depth of the word array of an n-bit bitset: the
9# smallest d <= 31 with n <= 32 * 2^d, so the capacity of the representation
10# is 2^36 bits. The fact proved here is that the depth is always below 32
11# (hence every word index is a representable U32 and Base's index masking is
12# the identity). That the chosen depth actually holds n bits is the loop's own
13# exit test, and is carried as the explicit `fits` premise of the laws about
14# `new` (see proofs/bitset/state.bend): a bitset larger than the capacity
15# cannot be represented, exactly as in src/dynamic_array.bend.
16
17def pow2_same(+d: Nat) -> {B.pow2(d) == SC.pow2(d) : Nat}:
18 match d:
19 case 0n:
20 {==}
21 case 1n+p:
22 Equal.cong(Nat, Nat, Nat.double, B.pow2(p), SC.pow2(p), pow2_same(p))
23
24def depth_go_le(fuel: Nat, +n: Nat, +d: Nat, +cap: Nat, done: Bool, +hd: {Nat.is_le(Nat.add(d, fuel), 31n) == True{} : Bool}) -> {Nat.is_le(B.depth_go(fuel, n, d, cap, done), 31n) == True{} : Bool}:
25 match fuel done:
26 case 0n _:
27 %N.add_zero(d) : {Nat.is_le(_, 31n) == True{} : Bool}
28 hd
29 case 1n+ +f True{}:
30 N.le_trans(d, Nat.add(d, 1n+f), 31n, N.le_add_right(d, 1n+f), hd)
31 case 1n+ +f False{}:
32 depth_go_le(f, n, 1n+d, Nat.double(cap), Nat.is_le(n, Nat.mul(Nat.double(cap), 32n)),
33 L.subst(Nat, z => {Nat.is_le(z, 31n) == True{} : Bool}, Nat.add(d, 1n+f), 1n+Nat.add(d, f), N.add_succ(d, f), hd))
34
35# The depth is always below 32, so every word index is a representable U32
36# and Base's index masking over the word array is the identity.
37def depth_le(+n: Nat) -> {Nat.is_le(B.depth_for(n), 31n) == True{} : Bool}:
38 depth_go_le(31n, n, 0n, 1n, Nat.is_le(n, Nat.mul(1n, 32n)), N.le_refl(31n))
39
40def depth_lt(+n: Nat) -> {Nat.is_lt(B.depth_for(n), 32n) == True{} : Bool}:
41 N.le_lt_succ(B.depth_for(n), 31n, depth_le(n))
42
43# re-exports so proofs/bitset/state.bend does not need proofs/bitset/index.bend
44def wordix_small_alias(+i: Nat, +h: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {B.wordix(i) == 0n : Nat}:
45 IX.wordix_small(i, h)
46
47def wordix_step_alias(+i: Nat, +h: {Nat.is_lt(i, 32n) == False{} : Bool}) -> {B.wordix(i) == 1n+B.wordix(Nat.sub(i, 32n)) : Nat}:
48 IX.wordix_step(i, h)