proofs/word_encoding.bend
stelliferous@0.0.3.0 · 297 lines · 0 definitions
1# General-width bit-vector arithmetic used by the native-address obligation.
2import Base
3
4def concat(+n: Nat, +m: Nat, w: Word(n), tail: Word(m)) -> Word(Nat.add(n,m)):
5 match n:
6 case 0n:
7 match w:
8 case WNil{}:
9 tail
10 case 1n+p:
11 match w:
12 case WCon{b,rest}:
13 WCon{b,concat(p,m,rest,tail)}
14
15def shift(n: Nat, x: Nat) -> Nat:
16 match n:
17 case 0n:
18 x
19 case 1n+p:
20 Nat.double(shift(p,x))
21
22law double_add:
23 for +a: Nat
24 for +b: Nat
25 {Nat.double(Nat.add(a,b)) == Nat.add(Nat.double(a),Nat.double(b)) : Nat}
26
27def double_add(a,b):
28 match a:
29 case 0n:
30 {==}
31 case 1n+ +p:
32 %double_add(p,b) : {2n+Nat.double(Nat.add(p,b)) == 2n+_ : Nat}
33 {==}
34
35law zero_nat:
36 for +n: Nat
37 {Word.to_nat(n,Word.zero(n)) == 0n : Nat}
38
39def zero_nat(n):
40 match n:
41 case 0n:
42 {==}
43 case 1n+ +p:
44 %zero_nat(p) : {Nat.double(Word.to_nat(p,Word.zero(p))) == Nat.double(_) : Nat}
45 {==}
46
47law finish_lt_zero:
48 for +b: Bool
49 for +c: Cmp
50 {Cmp.is_lt(Word.cmp.fin(b,False{},c)) == Cmp.is_lt(c) : Bool}
51
52def finish_lt_zero(b,c):
53 match b c:
54 case False{} LT{}:
55 {==}
56 case False{} EQ{}:
57 {==}
58 case False{} GT{}:
59 {==}
60 case True{} LT{}:
61 {==}
62 case True{} EQ{}:
63 {==}
64 case True{} GT{}:
65 {==}
66
67law compare_high_only:
68 for +n: Nat
69 for +m: Nat
70 for +w: Word(n)
71 for +top: Word(m)
72 for +other: Word(m)
73 {Cmp.is_lt(Word.cmp(Nat.add(n,m),concat(n,m,w,top),concat(n,m,Word.zero(n),other))) == Cmp.is_lt(Word.cmp(m,top,other)) : Bool}
74
75def compare_high_only(n,m,w,top,other):
76 match n:
77 case 0n:
78 match w:
79 case WNil{}:
80 {==}
81 case 1n+ +p:
82 match w:
83 case WCon{+b,+rest}:
84 %compare_high_only(p,m,rest,top,other) : {Cmp.is_lt(Word.cmp.fin(b,False{},Word.cmp(Nat.add(p,m),concat(p,m,rest,top),concat(p,m,
85 Word.zero(p),other)))) == _ : Bool}
86 finish_lt_zero(b,Word.cmp(Nat.add(p,m),concat(p,m,rest,top),concat(p,m,Word.zero(p),other)))
87
88law nonnegative:
89 for +n: Nat
90 for +w: Word(n)
91 {Cmp.is_lt(Word.cmp(n,w,Word.zero(n))) == False{} : Bool}
92
93def nonnegative(n,w):
94 match n:
95 case 0n:
96 match w:
97 case WNil{}:
98 {==}
99 case 1n+ +p:
100 match w:
101 case WCon{+b,+rest}:
102 %nonnegative(p,rest) : {Cmp.is_lt(Word.cmp.fin(b,False{},Word.cmp(p,rest,Word.zero(p)))) == _ : Bool}
103 finish_lt_zero(b,Word.cmp(p,rest,Word.zero(p)))
104
105def truth(b: Bool) -> Type:
106 match b:
107 case False{}:
108 Empty
109 case True{}:
110 Unit
111
112def false_true(e: {False{} == True{} : Bool}) -> Empty:
113 %Equal.sym(Bool,False{},True{},e) : truth(_)
114 Unit{}
115
116law finish_one:
117 for +b: Bool
118 for +c: Cmp
119 for nonneg: {Cmp.is_lt(c) == False{} : Bool}
120 {Cmp.is_lt(Word.cmp.fin(b,True{},c)) == Cmp.is_eq(Word.cmp.fin(b,False{},c)) : Bool}
121
122def finish_one(b,c,nonneg):
123 match b c:
124 case False{} LT{}:
125 Empty.absurd({True{} == False{} : Bool},false_true(Equal.sym(Bool,True{},False{},nonneg)))
126 case False{} EQ{}:
127 {==}
128 case False{} GT{}:
129 {==}
130 case True{} LT{}:
131 Empty.absurd({True{} == False{} : Bool},false_true(Equal.sym(Bool,True{},False{},nonneg)))
132 case True{} EQ{}:
133 {==}
134 case True{} GT{}:
135 {==}
136
137law less_one_is_zero:
138 for +n: Nat
139 for +w: Word(1n+n)
140 {Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})) == Cmp.is_eq(Word.cmp(1n+n,w,Word.zero(1n+n))) : Bool}
141
142def less_one_is_zero(n,w):
143 match w:
144 case WCon{b,+rest}:
145 finish_one(b,Word.cmp(n,rest,Word.zero(n)),nonnegative(n,rest))
146
147type Split<-n: Nat,-m: Nat> is Data:
148 Parts{low: Word(n),high: Word(m)}
149
150def join(+n: Nat, +m: Nat, parts: Split<n,m>) -> Word(Nat.add(n,m)):
151 Parts{low,high} = parts
152 concat(n,m,low,high)
153
154def prepend(-n: Nat, -m: Nat, b: Bool, parts: Split<n,m>) -> Split<1n+n,m>:
155 Parts{low,high} = parts
156 Parts{WCon{b,low},high}
157
158def split(+n: Nat, +m: Nat, w: Word(Nat.add(n,m))) -> Split<n,m>:
159 match n:
160 case 0n:
161 Parts{WNil{},w}
162 case 1n+ +p:
163 match w:
164 case WCon{b,rest}:
165 prepend(p,m,b,split(p,m,rest))
166
167law join_prepend:
168 for +n: Nat
169 for +m: Nat
170 for +b: Bool
171 for +parts: Split<n,m>
172 {WCon{b,join(n,m,parts)} == join(1n+n,m,prepend(n,m,b,parts)) : Word(1n+Nat.add(n,m))}
173
174def join_prepend(n,m,b,parts):
175 Parts{low,high} = parts
176 {==}
177
178law recover:
179 for +n: Nat
180 for +m: Nat
181 for +w: Word(Nat.add(n,m))
182 {join(n,m,split(n,m,w)) == w : Word(Nat.add(n,m))}
183
184def recover(n,m,w):
185 match n:
186 case 0n:
187 {==}
188 case 1n+ +p:
189 match w:
190 case WCon{+b,+rest}:
191 %recover(p,m,rest) : {join(1n+p,m,prepend(p,m,b,split(p,m,rest))) == WCon{b,_} : Word(1n+Nat.add(p,m))}
192 Equal.sym(Word(1n+Nat.add(p,m)),WCon{b,join(p,m,split(p,m,rest))},join(1n+p,m,prepend(p,m,b,split(p,m,rest))),join_prepend(p,m,b,
193 split(p,m,rest)))
194
195law cmp_eq:
196 for +c: Cmp
197 for yes: {Cmp.is_eq(c) == True{} : Bool}
198 {c == EQ{} : Cmp}
199
200def cmp_eq(c,yes):
201 match c:
202 case LT{}:
203 Empty.absurd({LT{} == EQ{} : Cmp},false_true(yes))
204 case EQ{}:
205 {==}
206 case GT{}:
207 Empty.absurd({GT{} == EQ{} : Cmp},false_true(yes))
208
209law finish_eq_parts:
210 for +b: Bool
211 for +c: Cmp
212 for eq: {Word.cmp.fin(b,False{},c) == EQ{} : Cmp}
213 {b == False{} : Bool} & {c == EQ{} : Cmp}
214
215def finish_eq_parts(b,c,eq):
216 match b c:
217 case False{} LT{}:
218 Empty.absurd({False{} == False{} : Bool} & {LT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),LT{},EQ{},eq)))
219 case False{} EQ{}:
220 ({==},{==})
221 case False{} GT{}:
222 Empty.absurd({False{} == False{} : Bool} & {GT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),GT{},EQ{},eq)))
223 case True{} LT{}:
224 Empty.absurd({True{} == False{} : Bool} & {LT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),LT{},EQ{},eq)))
225 case True{} EQ{}:
226 Empty.absurd({True{} == False{} : Bool} & {EQ{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),GT{},EQ{},eq)))
227 case True{} GT{}:
228 Empty.absurd({True{} == False{} : Bool} & {GT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),GT{},EQ{},eq)))
229
230law zero_reflect:
231 for +n: Nat
232 for +w: Word(n)
233 for eq: {Word.cmp(n,w,Word.zero(n)) == EQ{} : Cmp}
234 {w == Word.zero(n) : Word(n)}
235
236def zero_step(+p: Nat, +b: Bool, +rest: Word(p), proof: {b == False{} : Bool} & {Word.cmp(p,rest,Word.zero(p)) == EQ{} : Cmp}, ih: {Word.cmp(p,
237 rest,Word.zero(p)) == EQ{} : Cmp} -> {rest == Word.zero(p) : Word(p)}) -> {WCon{b,rest} == Word.zero(1n+p) : Word(1n+p)}:
238 (head,tail) = proof
239 %Equal.sym(Bool,b,False{},head) : {WCon{_,rest} == Word.zero(1n+p) : Word(1n+p)}
240 %ih(tail) : {WCon{False{},rest} == WCon{False{},_} : Word(1n+p)}
241 {==}
242
243def zero_reflect(n,w,eq):
244 match n:
245 case 0n:
246 match w:
247 case WNil{}:
248 {==}
249 case 1n+ +p:
250 match w:
251 case WCon{+b,+rest}:
252 zero_step(p,b,rest,finish_eq_parts(b,Word.cmp(p,rest,Word.zero(p)),eq),e => zero_reflect(p,rest,e))
253
254law below_one_zero:
255 for +n: Nat
256 for +w: Word(1n+n)
257 for below: {Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})) == True{} : Bool}
258 {w == Word.zero(1n+n) : Word(1n+n)}
259
260def below_one_zero(n,w,below):
261 zero_reflect(1n+n,w,cmp_eq(Word.cmp(1n+n,w,Word.zero(1n+n)),Equal.trans(Bool,Cmp.is_eq(Word.cmp(1n+n,w,Word.zero(1n+n))),
262 Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})),True{},Equal.sym(Bool,Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})),
263 Cmp.is_eq(Word.cmp(1n+n,w,Word.zero(1n+n))),less_one_is_zero(n,w)),below)))
264
265law and_zero:
266 for +n: Nat
267 for +w: Word(n)
268 {Word.and(n,w,Word.zero(n)) == Word.zero(n) : Word(n)}
269
270def and_zero(n,w):
271 match n:
272 case 0n:
273 match w:
274 case WNil{}:
275 {==}
276 case 1n+ +p:
277 match w:
278 case WCon{False{},+rest}:
279 %and_zero(p,rest) : {WCon{False{},Word.and(p,rest,Word.zero(p))} == WCon{False{},_} : Word(1n+p)}
280 {==}
281 case WCon{True{},+rest}:
282 %and_zero(p,rest) : {WCon{False{},Word.and(p,rest,Word.zero(p))} == WCon{False{},_} : Word(1n+p)}
283 {==}
284
285law upper_zero:
286 for +n: Nat
287 for +m: Nat
288 for +low: Word(n)
289 for +high: Word(1n+m)
290 for bound: {Cmp.is_lt(Word.cmp(Nat.add(n,1n+m),concat(n,1n+m,low,high),concat(n,1n+m,Word.zero(n),WCon{True{},Word.zero(m)}))) == True{} : Bool}
291 {high == Word.zero(1n+m) : Word(1n+m)}
292
293def upper_zero(n,m,low,high,bound):
294 below_one_zero(m,high,Equal.trans(Bool,Cmp.is_lt(Word.cmp(1n+m,high,WCon{True{},Word.zero(m)})),Cmp.is_lt(Word.cmp(Nat.add(n,1n+m),concat(n,
295 1n+m,low,high),concat(n,1n+m,Word.zero(n),WCon{True{},Word.zero(m)}))),True{},Equal.sym(Bool,Cmp.is_lt(Word.cmp(Nat.add(n,1n+m),
296 concat(n,1n+m,low,high),concat(n,1n+m,Word.zero(n),WCon{True{},Word.zero(m)}))),Cmp.is_lt(Word.cmp(1n+m,high,WCon{True{},
297 Word.zero(m)})),compare_high_only(n,1n+m,low,high,WCon{True{},Word.zero(m)})),bound))