proofs/word_power_of_two.bend
stelliferous@0.0.2.0 · 342 lines · 24 definitions
1
2import Base
3import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
4import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
5
6def power(+width: Nat,depth: Nat) -> Word(width):
7 match width:
8 case 0n:
9 WNil{}
10 case 1n+rest:
11 match depth:
12 case 0n:
13 WCon{True{},Word.zero(rest)}
14 case 1n+previous:
15 WCon{False{},power(rest,previous)}
16
17def mask(+width: Nat,depth: Nat) -> Word(width):
18 match width:
19 case 0n:
20 WNil{}
21 case 1n+rest:
22 match depth:
23 case 0n:
24 Word.zero(1n+rest)
25 case 1n+previous:
26 WCon{True{},mask(rest,previous)}
27
28law put_into_zero:
29 for +width: Nat
30 for +bit: Bool
31 {Word.shl.put(width,bit,Word.zero(width)) == Bool.pick(Word(width),bit,power(width,0n),Word.zero(width)) : Word(width)}
32
33def put_into_zero(width,bit):
34 match width:
35 case 0n:
36 match bit:
37 case False{}: {==}
38 case True{}: {==}
39 case 1n+ +rest:
40 match bit:
41 case False{}:
42 %put_into_zero(rest,False{}) : {WCon{False{},Word.shl.put(rest,False{},Word.zero(rest))} == WCon{False{},_} : Word(1n+rest)}
43 {==}
44 case True{}:
45 %put_into_zero(rest,False{}) : {WCon{True{},Word.shl.put(rest,False{},Word.zero(rest))} == WCon{True{},_} : Word(1n+rest)}
46 {==}
47
48law shift_power:
49 for +width: Nat
50 for +depth: Nat
51 {Word.shl(width,power(width,depth)) == power(width,1n+depth) : Word(width)}
52
53def shift_power(width,depth):
54 match width:
55 case 0n: {==}
56 case 1n+ +rest:
57 match depth:
58 case 0n:
59 %put_into_zero(rest,True{}) : {WCon{False{},Word.shl.put(rest,True{},Word.zero(rest))} == WCon{False{},_} : Word(1n+rest)}
60 {==}
61 case 1n+ +previous:
62 %shift_power(rest,previous) : {WCon{False{},Word.shl.put(rest,False{},power(rest,previous))} == WCon{False{},_} : Word(1n+rest)}
63 Equal.cong(Word(rest),Word(1n+rest),w => WCon{False{},w},Word.shl.put(rest,False{},power(rest,previous)),Word.shl(rest,power(rest,
64 previous)),Equal.sym(Word(rest),Word.shl(rest,power(rest,previous)),Word.shl.put(rest,False{},power(rest,previous)),
65 WordArithmetic.shift_put(rest,power(rest,previous))))
66
67law native_power:
68 for +depth: Nat
69 {U32.shln(1,depth) == U32{power(32n,depth)} : U32}
70
71def native_power(depth):
72 match depth:
73 case 0n: {==}
74 case 1n+ +previous:
75 %Equal.sym(U32,U32.shln(1,previous),U32{power(32n,previous)},native_power(previous)) : {U32.shl(_) == U32{power(32n,1n+previous)} : U32}
76 Equal.cong(Word(32n),U32,w => U32{w},Word.shl(32n,power(32n,previous)),power(32n,1n+previous),shift_power(32n,previous))
77
78law subtract_one:
79 for +width: Nat
80 for +word: Word(width)
81 {Word.sub(width,word,power(width,0n)) == Word.adc(width,word,Word.zero(width),True{},False{}) : Word(width)}
82
83def subtract_one(width,word):
84 match width:
85 case 0n: {==}
86 case 1n+rest:
87 match word:
88 case WCon{False{},tail}: {==}
89 case WCon{True{},tail}: {==}
90
91law zero_subtract_zero:
92 for +width: Nat
93 {Word.adc(width,Word.zero(width),Word.zero(width),True{},True{}) == Word.zero(width) : Word(width)}
94
95def zero_subtract_zero(width):
96 match width:
97 case 0n: {==}
98 case 1n+ +rest:
99 %zero_subtract_zero(rest) : {WCon{False{},Word.adc(rest,Word.zero(rest),Word.zero(rest),True{},True{})} == WCon{False{},_} : Word(1n+rest)}
100 {==}
101
102law decrement_power:
103 for +width: Nat
104 for +depth: Nat
105 {Word.adc(width,power(width,depth),Word.zero(width),True{},False{}) == mask(width,depth) : Word(width)}
106
107def decrement_power(width,depth):
108 match width:
109 case 0n: {==}
110 case 1n+ +rest:
111 match depth:
112 case 0n:
113 %zero_subtract_zero(rest) : {WCon{False{},Word.adc(rest,Word.zero(rest),Word.zero(rest),True{},True{})} == WCon{False{},_} : Word(1n+rest)}
114 {==}
115 case 1n+ +previous:
116 %decrement_power(rest,previous) : {WCon{True{},Word.adc(rest,power(rest,previous),Word.zero(rest),True{},False{})} == WCon{True{},
117 _} : Word(1n+rest)}
118 {==}
119
120law mask_preserves_bounded:
121 for +width: Nat
122 for +depth: Nat
123 for +word: Word(width)
124 for bound: {Cmp.is_lt(Word.cmp(width,word,power(width,depth))) == True{} : Bool}
125 {Word.and(width,word,mask(width,depth)) == word : Word(width)}
126
127def mask_preserves_bounded(width,depth,word,bound):
128 match width:
129 case 0n:
130 match word:
131 case WNil{}: {==}
132 case 1n+ +rest:
133 match depth:
134 case 0n:
135 %Equal.sym(Word(1n+rest),word,Word.zero(1n+rest),WordEncoding.below_one_zero(rest,word,bound)) : {Word.and(1n+rest,_,
136 Word.zero(1n+rest)) == _ : Word(1n+rest)}
137 WordEncoding.and_zero(1n+rest,Word.zero(1n+rest))
138 case 1n+ +previous:
139 match word:
140 case WCon{False{},+tail}:
141 %mask_preserves_bounded(rest,previous,tail,Equal.trans(Bool,Cmp.is_lt(Word.cmp(rest,tail,power(rest,previous))),
142 Cmp.is_lt(Word.cmp.fin(False{},False{},Word.cmp(rest,tail,power(rest,previous)))),True{},Equal.sym(Bool,
143 Cmp.is_lt(Word.cmp.fin(False{},False{},Word.cmp(rest,tail,power(rest,previous)))),Cmp.is_lt(Word.cmp(rest,tail,power(rest,
144 previous))),WordEncoding.finish_lt_zero(False{},Word.cmp(rest,tail,power(rest,previous)))),bound)) : {WCon{False{},
145 Word.and(rest,tail,mask(rest,previous))} == WCon{False{},_} : Word(1n+rest)}
146 {==}
147 case WCon{True{},+tail}:
148 %mask_preserves_bounded(rest,previous,tail,Equal.trans(Bool,Cmp.is_lt(Word.cmp(rest,tail,power(rest,previous))),
149 Cmp.is_lt(Word.cmp.fin(True{},False{},Word.cmp(rest,tail,power(rest,previous)))),True{},Equal.sym(Bool,
150 Cmp.is_lt(Word.cmp.fin(True{},False{},Word.cmp(rest,tail,power(rest,previous)))),Cmp.is_lt(Word.cmp(rest,tail,power(rest,
151 previous))),WordEncoding.finish_lt_zero(True{},Word.cmp(rest,tail,power(rest,previous)))),bound)) : {WCon{True{},
152 Word.and(rest,tail,mask(rest,previous))} == WCon{True{},_} : Word(1n+rest)}
153 {==}
154
155def native_word_mask(+depth: Nat,+word: Word(32n),bound: {Cmp.is_lt(Word.cmp(32n,word,power(32n,
156 depth))) == True{} : Bool}) -> {U32.and(U32{word},U32.sub(U32{power(32n,depth)},1)) == U32{word} : U32}:
157 %Equal.sym(Word(32n),Word.sub(32n,power(32n,depth),power(32n,0n)),mask(32n,depth),Equal.trans(Word(32n),Word.sub(32n,power(32n,depth),
158 power(32n,0n)),Word.adc(32n,power(32n,depth),Word.zero(32n),True{},False{}),mask(32n,depth),subtract_one(32n,power(32n,depth)),
159 decrement_power(32n,depth))) : {U32{Word.and(32n,word,_)} == U32{word} : U32}
160 Equal.cong(Word(32n),U32,w => U32{w},Word.and(32n,word,mask(32n,depth)),word,mask_preserves_bounded(32n,depth,word,bound))
161
162law native_mask_preserves_bounded:
163 for +depth: Nat
164 for +index: U32
165 {U32.is_lt(index,U32.shln(1,depth)) == True{} : Bool} -> {U32.and(index,U32.sub(U32.shln(1,depth),1)) == index : U32}
166
167def native_mask_preserves_bounded(depth,index):
168 match index:
169 case U32{+word}:
170 %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.is_lt(U32{word},
171 _) == True{} : Bool} -> {U32.and(U32{word},U32.sub(_,1)) == U32{word} : U32}
172 bound => native_word_mask(depth,word,bound)
173
174law compare_zero:
175 for +width: Nat
176 {Word.cmp(width,Word.zero(width),Word.zero(width)) == EQ{} : Cmp}
177
178def compare_zero(width):
179 match width:
180 case 0n: {==}
181 case 1n+ +rest:
182 %compare_zero(rest) : {Word.cmp.fin(False{},False{},Word.cmp(rest,Word.zero(rest),Word.zero(rest))) == Word.cmp.fin(False{},False{},_) : Cmp}
183 {==}
184
185law positive_power:
186 for +width: Nat
187 for +depth: Nat
188 for fits: {Nat.is_lt(depth,width) == True{} : Bool}
189 {Word.cmp(width,Word.zero(width),power(width,depth)) == LT{} : Cmp}
190
191def positive_power(width,depth,fits):
192 match width:
193 case 0n:
194 match depth:
195 case 0n: Empty.absurd({Word.cmp(0n,WNil{},power(0n,0n)) == LT{} : Cmp},WordEncoding.false_true(fits))
196 case 1n+rest: Empty.absurd({Word.cmp(0n,WNil{},power(0n,1n+rest)) == LT{} : Cmp},WordEncoding.false_true(fits))
197 case 1n+ +rest:
198 match depth:
199 case 0n:
200 %compare_zero(rest) : {Word.cmp.fin(False{},True{},Word.cmp(rest,Word.zero(rest),Word.zero(rest))) == Word.cmp.fin(False{},True{},_) : Cmp}
201 {==}
202 case 1n+ +previous:
203 %positive_power(rest,previous,fits) : {Word.cmp.fin(False{},False{},Word.cmp(rest,Word.zero(rest),power(rest,
204 previous))) == Word.cmp.fin(False{},False{},_) : Cmp}
205 {==}
206
207law compare_equal_low_bits:
208 for +comparison: Cmp
209 {Word.cmp.fin(False{},False{},comparison) == comparison : Cmp}
210
211def compare_equal_low_bits(comparison):
212 match comparison:
213 case LT{}: {==}
214 case EQ{}: {==}
215 case GT{}: {==}
216
217law power_monotone:
218 for +width: Nat
219 for +lower: Nat
220 for +upper: Nat
221 for fits: {Nat.is_lt(upper,width) == True{} : Bool}
222 for ordered: {Nat.is_le(lower,upper) == True{} : Bool}
223 {Cmp.is_le(Word.cmp(width,power(width,lower),power(width,upper))) == True{} : Bool}
224
225def power_monotone(width,lower,upper,fits,ordered):
226 match width:
227 case 0n: {==}
228 case 1n+ +rest:
229 match lower upper:
230 case 0n 0n:
231 %compare_zero(rest) : {Cmp.is_le(Word.cmp.fin(True{},True{},Word.cmp(rest,Word.zero(rest),
232 Word.zero(rest)))) == Cmp.is_le(Word.cmp.fin(True{},True{},_)) : Bool}
233 {==}
234 case 0n 1n+ +previous:
235 %positive_power(rest,previous,fits) : {Cmp.is_le(Word.cmp.fin(True{},False{},Word.cmp(rest,Word.zero(rest),power(rest,
236 previous)))) == Cmp.is_le(Word.cmp.fin(True{},False{},_)) : Bool}
237 {==}
238 case 1n+previous 0n:
239 Empty.absurd({Cmp.is_le(Word.cmp(1n+rest,power(1n+rest,1n+previous),power(1n+rest,0n))) == True{} : Bool},WordEncoding.false_true(ordered))
240 case 1n+ +low 1n+ +high:
241 %Equal.sym(Cmp,Word.cmp.fin(False{},False{},Word.cmp(rest,power(rest,low),power(rest,high))),Word.cmp(rest,power(rest,low),power(rest,
242 high)),compare_equal_low_bits(Word.cmp(rest,power(rest,low),power(rest,high)))) : {Cmp.is_le(_) == True{} : Bool}
243 power_monotone(rest,low,high,fits,ordered)
244
245law power_value:
246 for +width: Nat
247 for +depth: Nat
248 for fits: {Nat.is_lt(depth,width) == True{} : Bool}
249 {Word.to_nat(width,power(width,depth)) == WordEncoding.shift(depth,1n) : Nat}
250
251def power_value(width,depth,fits):
252 match width:
253 case 0n:
254 match depth:
255 case 0n: Empty.absurd({0n == WordEncoding.shift(0n,1n) : Nat},WordEncoding.false_true(fits))
256 case 1n+rest: Empty.absurd({0n == WordEncoding.shift(1n+rest,1n) : Nat},WordEncoding.false_true(fits))
257 case 1n+ +rest:
258 match depth:
259 case 0n:
260 %WordEncoding.zero_nat(rest) : {1n+Nat.double(Word.to_nat(rest,Word.zero(rest))) == 1n+Nat.double(_) : Nat}
261 {==}
262 case 1n+ +previous:
263 %power_value(rest,previous,fits) : {Nat.double(Word.to_nat(rest,power(rest,previous))) == Nat.double(_) : Nat}
264 {==}
265
266law pad_zero:
267 for +width: Nat
268 {Word.shr.pad(width,Word.zero(width)) == Word.zero(1n+width) : Word(1n+width)}
269
270def pad_zero(width):
271 match width:
272 case 0n: {==}
273 case 1n+ +rest:
274 %pad_zero(rest) : {WCon{False{},Word.shr.pad(rest,Word.zero(rest))} == WCon{False{},_} : Word(2n+rest)}
275 {==}
276
277law pad_power:
278 for +width: Nat
279 for +depth: Nat
280 for fits: {Nat.is_lt(depth,width) == True{} : Bool}
281 {Word.shr.pad(width,power(width,depth)) == power(1n+width,depth) : Word(1n+width)}
282
283def pad_power(width,depth,fits):
284 match width:
285 case 0n:
286 match depth:
287 case 0n: Empty.absurd({Word.shr.pad(0n,power(0n,0n)) == power(1n,0n) : Word(1n)},WordEncoding.false_true(fits))
288 case 1n+rest: Empty.absurd({Word.shr.pad(0n,power(0n,1n+rest)) == power(1n,1n+rest) : Word(1n)},WordEncoding.false_true(fits))
289 case 1n+ +rest:
290 match depth:
291 case 0n:
292 %pad_zero(rest) : {WCon{True{},Word.shr.pad(rest,Word.zero(rest))} == WCon{True{},_} : Word(2n+rest)}
293 {==}
294 case 1n+ +previous:
295 %pad_power(rest,previous,fits) : {WCon{False{},Word.shr.pad(rest,power(rest,previous))} == WCon{False{},_} : Word(2n+rest)}
296 {==}
297
298law native_half_power:
299 for +depth: Nat
300 for fits: {Nat.is_lt(depth,31n) == True{} : Bool}
301 {U32.shr(U32.shln(1,1n+depth)) == U32.shln(1,depth) : U32}
302
303def native_half_power(depth,fits):
304 %Equal.sym(U32,U32.shln(1,1n+depth),U32{power(32n,1n+depth)},native_power(1n+depth)) : {U32.shr(_) == U32.shln(1,depth) : U32}
305 %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.shr(U32{power(32n,1n+depth)}) == _ : U32}
306 Equal.cong(Word(32n),U32,w => U32{w},Word.shr.pad(31n,power(31n,depth)),power(32n,depth),pad_power(31n,depth,fits))
307
308law native_power_bound:
309 for +depth: Nat
310 for bound: {Nat.is_le(depth,31n) == True{} : Bool}
311 {U32.is_le(U32.shln(1,depth),2147483648) == True{} : Bool}
312
313def native_power_bound(depth,bound):
314 %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.is_le(_,2147483648) == True{} : Bool}
315 power_monotone(32n,depth,31n,{==},bound)
316
317def native_allocatable(+depth: Nat,bound: {Nat.is_le(depth,30n) == True{} : Bool}) ->
318 {U32.is_le(U32.shln(1,depth),1073741824) == True{} : Bool}:
319 %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.is_le(_,1073741824) == True{} : Bool}
320 power_monotone(32n,depth,30n,{==},bound)
321
322def positive_double(value: Nat,positive: {Nat.is_lt(0n,Nat.double(value)) == True{} : Bool}) -> {Nat.is_lt(0n,value) == True{} : Bool}:
323 match value:
324 case 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
325 case 1n+rest: {==}
326
327
328
329def nonempty_power_depth(+width: Nat,+depth: Nat,positive: {Nat.is_lt(0n,Word.to_nat(width,power(width,depth))) == True{} : Bool}) ->
330 {Nat.is_lt(depth,width) == True{} : Bool}:
331 match width:
332 case 0n: Empty.absurd({Nat.is_lt(depth,0n) == True{} : Bool},WordEncoding.false_true(positive))
333 case 1n+ +rest:
334 match depth:
335 case 0n: {==}
336 case 1n+ +previous:
337 nonempty_power_depth(rest,previous,positive_double(Word.to_nat(rest,power(rest,previous)),positive))
338
339def native_nonempty_depth(+depth: Nat,positive: {Nat.is_lt(0n,U32.to_nat(U32.shln(1,depth))) == True{} : Bool}) ->
340 {Nat.is_lt(depth,32n) == True{} : Bool}:
341 nonempty_power_depth(32n,depth,
342 %native_power(depth) : {Nat.is_lt(0n,U32.to_nat(_)) == True{} : Bool} positive)