1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../src/containers/bitset.bend as B
5	
6	# The two facts about the word index `B.wordix(i) = i / 32` and the bit
7	# position `B.bitix(i) = i % 32` that the packed representation needs:
8	#
9	#   i <  32  ->  wordix(i) = 0      and  bitix(i) = i
10	#   wordix(32 + i) = 1 + wordix(i)  and  bitix(32 + i) = bitix(i)
11	#
12	# Both are proved from Base's own `Nat.divmod.go`, which is a structural
13	# recursion on the dividend, so 32 unfoldings of `Nat.add(32n, i)` are a
14	# definitional step (`peel_go` below is literally `{==}`); only the quotient
15	# accumulator has to be pushed out by an induction.
16	
17	def bump(p: Nat & Nat) -> Nat & Nat:
18	  (q, r) = p
19	  (1n+q, r)
20	
21	# The quotient accumulator of Nat.divmod.go is exactly an accumulator.
22	def acc(i: Nat, m: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(i, m, 1n+d, r) == bump(Nat.divmod.go(i, m, d, r)) : Nat & Nat}:
23	  match i m:
24	    case 0n _:
25	      {==}
26	    case 1n+np 0n:
27	      acc(np, r, 1n+d, 0n)
28	    case 1n+np 1n+mp:
29	      acc(np, mp, d, 1n+r)
30	
31	# 32 unfoldings: the dividend loses 32, the quotient gains one.
32	def peel_go(+i: Nat, +d: Nat) -> {Nat.divmod.go(Nat.add(32n, i), 31n, d, 0n) == Nat.divmod.go(i, 31n, 1n+d, 0n) : Nat & Nat}:
33	  {==}
34	
35	def peel(+i: Nat) -> {Nat.divmod(Nat.add(32n, i), 32n) == bump(Nat.divmod(i, 32n)) : Nat & Nat}:
36	  Equal.trans(Nat & Nat, Nat.divmod.go(Nat.add(32n, i), 31n, 0n, 0n), Nat.divmod.go(i, 31n, 1n, 0n), bump(Nat.divmod.go(i, 31n, 0n, 0n)),
37	    peel_go(i, 0n), acc(i, 31n, 0n, 0n))
38	
39	def fst_bump(p: Nat & Nat) -> {Pair.fst(Nat, Nat, bump(p)) == 1n+Pair.fst(Nat, Nat, p) : Nat}:
40	  (q, r) = p
41	  {==}
42	
43	def snd_bump(p: Nat & Nat) -> {Pair.snd(Nat, Nat, bump(p)) == Pair.snd(Nat, Nat, p) : Nat}:
44	  (q, r) = p
45	  {==}
46	
47	def wordix_peel(+i: Nat) -> {B.wordix(Nat.add(32n, i)) == 1n+B.wordix(i) : Nat}:
48	  Equal.trans(Nat, Pair.fst(Nat, Nat, Nat.divmod(Nat.add(32n, i), 32n)), Pair.fst(Nat, Nat, bump(Nat.divmod(i, 32n))), 1n+Pair.fst(Nat, Nat, Nat.divmod(i, 32n)),
49	    Equal.cong(Nat & Nat, Nat, pq => Pair.fst(Nat, Nat, pq), Nat.divmod(Nat.add(32n, i), 32n), bump(Nat.divmod(i, 32n)), peel(i)),
50	    fst_bump(Nat.divmod(i, 32n)))
51	
52	def bitix_peel(+i: Nat) -> {B.bitix(Nat.add(32n, i)) == B.bitix(i) : Nat}:
53	  Equal.trans(Nat, Pair.snd(Nat, Nat, Nat.divmod(Nat.add(32n, i), 32n)), Pair.snd(Nat, Nat, bump(Nat.divmod(i, 32n))), Pair.snd(Nat, Nat, Nat.divmod(i, 32n)),
54	    Equal.cong(Nat & Nat, Nat, pq => Pair.snd(Nat, Nat, pq), Nat.divmod(Nat.add(32n, i), 32n), bump(Nat.divmod(i, 32n)), peel(i)),
55	    snd_bump(Nat.divmod(i, 32n)))
56	
57	# A dividend that never reaches the divisor never advances the quotient.
58	def small_go(i: Nat, m: Nat, +r: Nat, +h: {Nat.is_le(i, m) == True{} : Bool}) -> {Nat.divmod.go(i, m, 0n, r) == (0n, Nat.add(r, i)) : Nat & Nat}:
59	  match i m:
60	    case 0n _:
61	      %Equal.sym(Nat, Nat.add(r, 0n), r, N.add_zero(r)) : {(0n, r) == (0n, _) : Nat & Nat}
62	      {==}
63	    case 1n+ +np 0n:
64	      Empty.absurd({Nat.divmod.go(1n+np, 0n, 0n, r) == (0n, Nat.add(r, 1n+np)) : Nat & Nat}, L.false_true(h))
65	    case 1n+ +np 1n+mp:
66	      %Equal.sym(Nat, Nat.add(r, 1n+np), 1n+Nat.add(r, np), N.add_succ(r, np)) : {Nat.divmod.go(np, mp, 0n, 1n+r) == (0n, _) : Nat & Nat}
67	      small_go(np, mp, 1n+r, h)
68	
69	def small(+i: Nat, +h: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {Nat.divmod(i, 32n) == (0n, i) : Nat & Nat}:
70	  small_go(i, 31n, 0n, N.lt_succ_le(i, 31n, h))
71	
72	def wordix_small(+i: Nat, +h: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {B.wordix(i) == 0n : Nat}:
73	  Equal.cong(Nat & Nat, Nat, pq => Pair.fst(Nat, Nat, pq), Nat.divmod(i, 32n), (0n, i), small(i, h))
74	
75	def bitix_small(+i: Nat, +h: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {B.bitix(i) == i : Nat}:
76	  Equal.cong(Nat & Nat, Nat, pq => Pair.snd(Nat, Nat, pq), Nat.divmod(i, 32n), (0n, i), small(i, h))
77	
78	# The form the word walk needs: for i >= 32, i = 32 + (i - 32).
79	def add_sub32(+i: Nat, +h: {Nat.is_lt(i, 32n) == False{} : Bool}) -> {Nat.add(32n, Nat.sub(i, 32n)) == i : Nat}:
80	  N.sub_add(i, 32n, N.not_lt_le(i, 32n, h))
81	
82	def wordix_step(+i: Nat, +h: {Nat.is_lt(i, 32n) == False{} : Bool}) -> {B.wordix(i) == 1n+B.wordix(Nat.sub(i, 32n)) : Nat}:
83	  L.subst(Nat, x => {B.wordix(x) == 1n+B.wordix(Nat.sub(i, 32n)) : Nat},
84	    Nat.add(32n, Nat.sub(i, 32n)), i, add_sub32(i, h), wordix_peel(Nat.sub(i, 32n)))
85	
86	def bitix_step(+i: Nat, +h: {Nat.is_lt(i, 32n) == False{} : Bool}) -> {B.bitix(i) == B.bitix(Nat.sub(i, 32n)) : Nat}:
87	  L.subst(Nat, x => {B.bitix(x) == B.bitix(Nat.sub(i, 32n)) : Nat},
88	    Nat.add(32n, Nat.sub(i, 32n)), i, add_sub32(i, h), bitix_peel(Nat.sub(i, 32n)))