1	import Base
2	import ../../lib/logic.bend as L
3	import ../../../src/containers/hash_table.bend as H
4	
5	# Check words, bit by bit (generic in the width; U32 is width 32 = 1 + 31).
6	#   top(p)   the word with only its top bit set  (U32: 2^31, H.tag())
7	#   low(p)   every bit but the top one            (U32: 2^31 - 1)
8	#   one(p)   the word 1
9	
10	def top(+p: Nat) -> Word(1n+p):
11	  match p:
12	    case 0n:
13	      WCon{True{}, WNil{}}
14	    case 1n+q:
15	      WCon{False{}, top(q)}
16	
17	def low(+p: Nat) -> Word(1n+p):
18	  match p:
19	    case 0n:
20	      WCon{False{}, WNil{}}
21	    case 1n+q:
22	      WCon{True{}, low(q)}
23	
24	def one(+p: Nat) -> Word(2n+p):
25	  WCon{True{}, Word.zero(1n+p)}
26	
27	# the top bit
28	def topb(+p: Nat, w: Word(1n+p)) -> Bool:
29	  match p w:
30	    case 0n WCon{b, WNil{}}:
31	      b
32	    case 1n+q WCon{b, t}:
33	      topb(q, t)
34	
35	def tag_top() -> {H.tag() == U32{top(31n)} : U32}:
36	  {==}
37	
38	def low_lit() -> {2147483647 == U32{low(31n)} : U32}:
39	  {==}
40	
41	def one_lit() -> {1 == U32{one(30n)} : U32}:
42	  {==}
43	
44	def zero_lit() -> {0 == U32{Word.zero(32n)} : U32}:
45	  {==}
46	
47	# ---- comparison with the top bit ----
48	
49	def ge_fin_false(+c: Cmp, +b: Bool) -> {Cmp.is_ge(Word.cmp.fin(b, False{}, c)) == Cmp.is_ge(c) : Bool}:
50	  match c b:
51	    case LT{} _:
52	      {==}
53	    case EQ{} True{}:
54	      {==}
55	    case EQ{} False{}:
56	      {==}
57	    case GT{} _:
58	      {==}
59	
60	def ge_top_leaf(+b: Bool) -> {Cmp.is_ge(Word.cmp(1n, WCon{b, WNil{}}, top(0n))) == b : Bool}:
61	  match b:
62	    case True{}:
63	      {==}
64	    case False{}:
65	      {==}
66	
67	# w >= 2^p is its top bit
68	def ge_top(+p: Nat, +w: Word(1n+p)) -> {Cmp.is_ge(Word.cmp(1n+p, w, top(p))) == topb(p, w) : Bool}:
69	  match p w:
70	    case 0n WCon{b, WNil{}}:
71	      ge_top_leaf(b)
72	    case 1n+q WCon{b, t}:
73	      Equal.trans(Bool, Cmp.is_ge(Word.cmp.fin(b, False{}, Word.cmp(1n+q, t, top(q)))), Cmp.is_ge(Word.cmp(1n+q, t, top(q))), topb(q, t), ge_fin_false(Word.cmp(1n+q, t, top(q)), b), ge_top(q, t))
74	
75	# ---- or / and with top and low ----
76	
77	def or_true(+b: Bool) -> {Bool.or(b, True{}) == True{} : Bool}:
78	  match b:
79	    case True{}:
80	      {==}
81	    case False{}:
82	      {==}
83	
84	def or_false(+b: Bool) -> {Bool.or(b, False{}) == b : Bool}:
85	  match b:
86	    case True{}:
87	      {==}
88	    case False{}:
89	      {==}
90	
91	def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
92	  match b:
93	    case True{}:
94	      {==}
95	    case False{}:
96	      {==}
97	
98	def and_false(+b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}:
99	  match b:
100	    case True{}:
101	      {==}
102	    case False{}:
103	      {==}
104	
105	def topb_or_top(+p: Nat, +x: Word(1n+p)) -> {topb(p, Word.or(1n+p, x, top(p))) == True{} : Bool}:
106	  match p x:
107	    case 0n WCon{b, WNil{}}:
108	      or_true(b)
109	    case 1n+q WCon{b, t}:
110	      topb_or_top(q, t)
111	
112	def topb_and_low(+p: Nat, +x: Word(1n+p)) -> {topb(p, Word.and(1n+p, x, low(p))) == False{} : Bool}:
113	  match p x:
114	    case 0n WCon{b, WNil{}}:
115	      and_false(b)
116	    case 1n+q WCon{b, t}:
117	      topb_and_low(q, t)
118	
119	def topb_or(+p: Nat, +x: Word(1n+p), +y: Word(1n+p)) -> {topb(p, Word.or(1n+p, x, y)) == Bool.or(topb(p, x), topb(p, y)) : Bool}:
120	  match p x y:
121	    case 0n WCon{a, WNil{}} WCon{b, WNil{}}:
122	      {==}
123	    case 1n+q WCon{a, s} WCon{b, t}:
124	      topb_or(q, s, t)
125	
126	def topb_zero(+p: Nat) -> {topb(p, Word.zero(1n+p)) == False{} : Bool}:
127	  match p:
128	    case 0n:
129	      {==}
130	    case 1n+q:
131	      topb_zero(q)
132	
133	def topb_one(+p: Nat) -> {topb(1n+p, one(p)) == False{} : Bool}:
134	  topb_zero(p)
135	
136	# clearing the top bit of x with the top bit set gives back x without it
137	def and_low_or_top(+p: Nat, +x: Word(1n+p), +h: {topb(p, x) == False{} : Bool}) -> {Word.and(1n+p, Word.or(1n+p, x, top(p)), low(p)) == x : Word(1n+p)}:
138	  match p x:
139	    case 0n WCon{b, WNil{}}:
140	      Equal.cong(Bool, Word(1n), c => WCon{c, WNil{}}, Bool.and(Bool.or(b, True{}), False{}), b, Equal.trans(Bool, Bool.and(Bool.or(b, True{}), False{}), False{}, b, and_false(Bool.or(b, True{})), Equal.sym(Bool, b, False{}, h)))
141	    case 1n+q WCon{b, t}:
142	      +e1 = Equal.trans(Bool, Bool.and(Bool.or(b, False{}), True{}), Bool.or(b, False{}), b, and_true(Bool.or(b, False{})), or_false(b))
143	      +e2 = and_low_or_top(q, t, h)
144	      Equal.trans(Word(2n+q), WCon{Bool.and(Bool.or(b, False{}), True{}), Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q))}, WCon{b, Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q))}, WCon{b, t},
145	        Equal.cong(Bool, Word(2n+q), c => WCon{c, Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q))}, Bool.and(Bool.or(b, False{}), True{}), b, e1),
146	        Equal.cong(Word(1n+q), Word(2n+q), w => WCon{b, w}, Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q)), t, e2))
147	
148	# ---- nonzero words ----
149	
150	def eq_fin_false(+b: Bool, +c: Cmp, +h: {Cmp.is_eq(c) == False{} : Bool}) -> {Cmp.is_eq(Word.cmp.fin(b, False{}, c)) == False{} : Bool}:
151	  match c:
152	    case LT{}:
153	      {==}
154	    case EQ{}:
155	      Empty.absurd({Cmp.is_eq(Word.cmp.fin(b, False{}, EQ{})) == False{} : Bool}, L.true_false(h))
156	    case GT{}:
157	      {==}
158	
159	def top_nonzero_g(+p: Nat, +w: Word(1n+p), +h: {topb(p, w) == True{} : Bool}) -> {Cmp.is_eq(Word.cmp(1n+p, w, Word.zero(1n+p))) == False{} : Bool}:
160	  match p w:
161	    case 0n WCon{True{}, WNil{}}:
162	      {==}
163	    case 0n WCon{False{}, WNil{}}:
164	      Empty.absurd({Cmp.is_eq(Word.cmp(1n, WCon{False{}, WNil{}}, Word.zero(1n))) == False{} : Bool}, L.false_true(h))
165	    case 1n+q WCon{b, t}:
166	      eq_fin_false(b, Word.cmp(1n+q, t, Word.zero(1n+q)), top_nonzero_g(q, t, h))
167	
168	def fin_tf(+c: Cmp) -> {Cmp.is_eq(Word.cmp.fin(True{}, False{}, c)) == False{} : Bool}:
169	  match c:
170	    case LT{}:
171	      {==}
172	    case EQ{}:
173	      {==}
174	    case GT{}:
175	      {==}
176	
177	def bit0_nonzero(+p: Nat, +t: Word(p)) -> {Cmp.is_eq(Word.cmp(1n+p, WCon{True{}, t}, Word.zero(1n+p))) == False{} : Bool}:
178	  fin_tf(Word.cmp(p, t, Word.zero(p)))
179	
180	# ---- the U32 check words ----
181	
182	def lt_ge(+c: Cmp) -> {Cmp.is_lt(c) == Bool.not(Cmp.is_ge(c)) : Bool}:
183	  match c:
184	    case LT{}:
185	      {==}
186	    case EQ{}:
187	      {==}
188	    case GT{}:
189	      {==}
190	
191	def not_true(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
192	  match b:
193	    case True{}:
194	      Empty.absurd({True{} == False{} : Bool}, L.false_true(h))
195	    case False{}:
196	      {==}
197	
198	# a code below 2^31 has its top bit clear
199	def small_top(+cw: Word(32n), +h: {U32.is_lt(U32{cw}, H.tag()) == True{} : Bool}) -> {topb(31n, cw) == False{} : Bool}:
200	  +c = Word.cmp(32n, cw, top(31n))
201	  not_true(topb(31n, cw), Equal.trans(Bool, Bool.not(topb(31n, cw)), Bool.not(Cmp.is_ge(c)), True{}, Equal.cong(Bool, Bool, z => Bool.not(z), topb(31n, cw), Cmp.is_ge(c), Equal.sym(Bool, Cmp.is_ge(c), topb(31n, cw), ge_top(31n, cw))), Equal.trans(Bool, Bool.not(Cmp.is_ge(c)), Cmp.is_lt(c), True{}, Equal.sym(Bool, Cmp.is_lt(c), Bool.not(Cmp.is_ge(c)), lt_ge(c)), h)))
202	
203	def is_short_top(+w: Word(32n)) -> {H.is_short(U32{w}) == topb(31n, w) : Bool}:
204	  ge_top(31n, w)
205	
206	def short_is_short(+c: U32) -> {H.is_short(H.short_word(c)) == True{} : Bool}:
207	  match c:
208	    case U32{+cw}:
209	      Equal.trans(Bool, H.is_short(U32{Word.or(32n, cw, top(31n))}), topb(31n, Word.or(32n, cw, top(31n))), True{}, is_short_top(Word.or(32n, cw, top(31n))), topb_or_top(31n, cw))
210	
211	def short_nonzero(+c: U32) -> {U32.is_eq(H.short_word(c), 0) == False{} : Bool}:
212	  match c:
213	    case U32{+cw}:
214	      top_nonzero_g(31n, Word.or(32n, cw, top(31n)), topb_or_top(31n, cw))
215	
216	# masking a short word gives back its character code
217	def short_back(+c: U32, +h: {U32.is_lt(c, H.tag()) == True{} : Bool}) -> {U32.and(H.short_word(c), 2147483647) == c : U32}:
218	  match c:
219	    case U32{+cw}:
220	      Equal.cong(Word(32n), U32, w => U32{w}, Word.and(32n, Word.or(32n, cw, top(31n)), low(31n)), cw, and_low_or_top(31n, cw, small_top(cw, h)))
221	
222	def short_inj(+a: U32, +b: U32, +ha: {U32.is_lt(a, H.tag()) == True{} : Bool}, +hb: {U32.is_lt(b, H.tag()) == True{} : Bool}, +e: {H.short_word(a) == H.short_word(b) : U32}) -> {a == b : U32}:
223	  Equal.trans(U32, a, U32.and(H.short_word(a), 2147483647), b, Equal.sym(U32, U32.and(H.short_word(a), 2147483647), a, short_back(a, ha)),
224	    Equal.trans(U32, U32.and(H.short_word(a), 2147483647), U32.and(H.short_word(b), 2147483647), b, Equal.cong(U32, U32, z => U32.and(z, 2147483647), H.short_word(a), H.short_word(b), e), short_back(b, hb)))
225	
226	def lw_word(+hw: Word(32n)) -> Word(32n):
227	  Word.or(32n, Word.and(32n, hw, low(31n)), one(30n))
228	
229	def long_top(+hw: Word(32n)) -> {topb(31n, lw_word(hw)) == False{} : Bool}:
230	  +x = Word.and(32n, hw, low(31n))
231	  %Equal.sym(Bool, topb(31n, Word.or(32n, x, one(30n))), Bool.or(topb(31n, x), topb(31n, one(30n))), topb_or(31n, x, one(30n))) : {_ == False{} : Bool}
232	  %Equal.sym(Bool, topb(31n, x), False{}, topb_and_low(31n, hw)) : {Bool.or(_, topb(31n, one(30n))) == False{} : Bool}
233	  topb_one(30n)
234	
235	def long_is_long(+h: U32) -> {H.is_short(H.long_word(h)) == False{} : Bool}:
236	  match h:
237	    case U32{+hw}:
238	      Equal.trans(Bool, H.is_short(U32{lw_word(hw)}), topb(31n, lw_word(hw)), False{}, is_short_top(lw_word(hw)), long_top(hw))
239	
240	def or_bit0(+p: Nat, +b: Bool, +t: Word(p)) -> {Word.or(1n+p, WCon{b, t}, WCon{True{}, Word.zero(p)}) == WCon{True{}, Word.or(p, t, Word.zero(p))} : Word(1n+p)}:
241	  Equal.cong(Bool, Word(1n+p), z => WCon{z, Word.or(p, t, Word.zero(p))}, Bool.or(b, True{}), True{}, or_true(b))
242	
243	def long_nonzero(+h: U32) -> {U32.is_eq(H.long_word(h), 0) == False{} : Bool}:
244	  match h:
245	    case U32{WCon{+b0, +rest}}:
246	      +b = Bool.and(b0, True{})
247	      +t = Word.and(31n, rest, low(30n))
248	      +u = Word.or(31n, t, Word.zero(31n))
249	      L.subst(Word(32n), w => {Cmp.is_eq(Word.cmp(32n, w, Word.zero(32n))) == False{} : Bool}, WCon{True{}, u}, lw_word(WCon{b0, rest}), Equal.sym(Word(32n), lw_word(WCon{b0, rest}), WCon{True{}, u}, or_bit0(31n, b, t)), bit0_nonzero(31n, u))
250	
251	# a long word is never a short word
252	def long_not_short(+h: U32, +c: U32, +e: {H.long_word(h) == H.short_word(c) : U32}) -> Empty:
253	  L.true_false(Equal.trans(Bool, True{}, H.is_short(H.short_word(c)), False{}, Equal.sym(Bool, H.is_short(H.short_word(c)), True{}, short_is_short(c)), Equal.trans(Bool, H.is_short(H.short_word(c)), H.is_short(H.long_word(h)), False{}, Equal.cong(U32, Bool, z => H.is_short(z), H.short_word(c), H.long_word(h), Equal.sym(U32, H.long_word(h), H.short_word(c), e)), long_is_long(h))))
254	
255	
256	
257	
258	# a word with its top bit set is its low bits with the top bit set
259	def or_and_low_top(+p: Nat, +x: Word(1n+p), +h: {topb(p, x) == True{} : Bool}) -> {Word.or(1n+p, Word.and(1n+p, x, low(p)), top(p)) == x : Word(1n+p)}:
260	  match p x:
261	    case 0n WCon{b, WNil{}}:
262	      Equal.cong(Bool, Word(1n), c => WCon{c, WNil{}}, Bool.or(Bool.and(b, False{}), True{}), b, Equal.trans(Bool, Bool.or(Bool.and(b, False{}), True{}), True{}, b, or_true(Bool.and(b, False{})), Equal.sym(Bool, b, True{}, h)))
263	    case 1n+q WCon{b, t}:
264	      +e1 = Equal.trans(Bool, Bool.or(Bool.and(b, True{}), False{}), Bool.and(b, True{}), b, or_false(Bool.and(b, True{})), and_true(b))
265	      Equal.trans(Word(2n+q), WCon{Bool.or(Bool.and(b, True{}), False{}), Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q))}, WCon{b, Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q))}, WCon{b, t},
266	        Equal.cong(Bool, Word(2n+q), c => WCon{c, Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q))}, Bool.or(Bool.and(b, True{}), False{}), b, e1),
267	        Equal.cong(Word(1n+q), Word(2n+q), w => WCon{b, w}, Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q)), t, or_and_low_top(q, t, h)))
268	
269	def short_eta(+x: U32, +h: {H.is_short(x) == True{} : Bool}) -> {H.short_word(U32.and(x, 2147483647)) == x : U32}:
270	  match x:
271	    case U32{+w}:
272	      Equal.cong(Word(32n), U32, z => U32{z}, Word.or(32n, Word.and(32n, w, low(31n)), top(31n)), w, or_and_low_top(31n, w, Equal.trans(Bool, topb(31n, w), H.is_short(U32{w}), True{}, Equal.sym(Bool, H.is_short(U32{w}), topb(31n, w), is_short_top(w)), h)))