1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../src/containers/bitset.bend as B
6	import ./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	
17	def 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	
24	def 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.
37	def 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	
40	def 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
44	def 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	
47	def 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)