proof_seq.bend
lawful-bytes@0.1.0.0 · 199 lines · 0 definitions
1import Base
2import lawful-bytes@0.1.0.0/defs.bend as D
3import lawful-words@0.1.0.0/defs.bend as W
4import lawful-words@0.1.0.0/proof_nat.bend as N
5import lawful-words@0.1.0.0/proof_bytes.bend as Y
6import lawful-arrays@0.1.0.0/proof_base.bend as AB
7
8# List facts the Bytes proofs need (take, set, append, unpack), for lists of
9# U32. Every variable is reusable.
10
11law take_zero:
12 for +xs: List<&2, U32>
13 {List.take(&2, U32, xs, 0n) == Nil{} : List<&2, U32>}
14
15def take_zero(xs):
16 match xs:
17 case Nil{}:
18 {==}
19 case Con{x, t}:
20 {==}
21
22law take_length:
23 for +xs: List<&2, U32>
24 for +n: Nat
25 for +h: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
26 {List.length(&2, U32, List.take(&2, U32, xs, n)) == n : Nat}
27
28def take_length(xs, n, h):
29 match xs n:
30 case Nil{} 0n:
31 {==}
32 case Nil{} 1n+p:
33 Empty.absurd({0n == 1n+p : Nat}, AB.false_ne_true(h))
34 case Con{x, t} 0n:
35 {==}
36 case Con{x, t} 1n+p:
37 %take_length(t, p, h) : {1n+List.length(&2, U32, List.take(&2, U32, t, p)) == 1n+_ : Nat}
38 {==}
39
40law take_take:
41 for +xs: List<&2, U32>
42 for +m: Nat
43 for +n: Nat
44 for +h: {Nat.is_le(n, m) == True{} : Bool}
45 {List.take(&2, U32, List.take(&2, U32, xs, m), n) == List.take(&2, U32, xs, n) : List<&2, U32>}
46
47def take_take(xs, m, n, h):
48 match xs m n:
49 case Nil{} _ _:
50 {==}
51 case Con{x, t} 0n 0n:
52 {==}
53 case Con{x, t} 0n 1n+q:
54 Empty.absurd({Nil{} == x <> List.take(&2, U32, t, q) : List<&2, U32>}, AB.false_ne_true(h))
55 case Con{x, t} 1n+p 0n:
56 {==}
57 case Con{x, t} 1n+p 1n+q:
58 %take_take(t, p, q, h) : {x <> List.take(&2, U32, List.take(&2, U32, t, p), q) == x <> _ : List<&2, U32>}
59 {==}
60
61law take_set:
62 for +xs: List<&2, U32>
63 for +m: Nat
64 for +i: Nat
65 for +v: U32
66 {List.take(&2, U32, List.set(&2, U32, xs, i, v), m) == List.set(&2, U32, List.take(&2, U32, xs, m), i, v) : List<&2, U32>}
67
68def take_set(xs, m, i, v):
69 match xs m i:
70 case Nil{} _ _:
71 {==}
72 case Con{x, t} 0n 0n:
73 {==}
74 case Con{x, t} 0n 1n+j:
75 {==}
76 case Con{x, t} 1n+p 0n:
77 {==}
78 case Con{x, t} 1n+p 1n+j:
79 %take_set(t, p, j, v) : {x <> List.take(&2, U32, List.set(&2, U32, t, j, v), p) == x <> _ : List<&2, U32>}
80 {==}
81
82# Setting index n and keeping n + 1 elements: the first n, then v.
83law take_set_succ:
84 for +xs: List<&2, U32>
85 for +n: Nat
86 for +v: U32
87 for +h: {Nat.is_lt(n, List.length(&2, U32, xs)) == True{} : Bool}
88 {List.take(&2, U32, List.set(&2, U32, xs, n, v), Nat.add(n, 1n)) == List.append(&2, U32, List.take(&2, U32, xs, n), [v]) : List<&2, U32>}
89
90def take_set_succ(xs, n, v, h):
91 match xs n:
92 case Nil{} _:
93 Empty.absurd({List.take(&2, U32, Nil{}, Nat.add(n, 1n)) == List.append(&2, U32, Nil{}, [v]) : List<&2, U32>},
94 AB.lt_zero_absurd(n, h))
95 case Con{x, t} 0n:
96 %Equal.sym(List<&2, U32>, List.take(&2, U32, t, 0n), Nil{}, take_zero(t)) : {v <> _ == [v] : List<&2, U32>}
97 {==}
98 case Con{x, t} 1n+p:
99 %take_set_succ(t, p, v, h) : {x <> List.take(&2, U32, List.set(&2, U32, t, p, v), Nat.add(p, 1n)) == x <> _ : List<&2, U32>}
100 {==}
101
102law take_append_l:
103 for +xs: List<&2, U32>
104 for +ys: List<&2, U32>
105 for +n: Nat
106 for +h: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
107 {List.take(&2, U32, List.append(&2, U32, xs, ys), n) == List.take(&2, U32, xs, n) : List<&2, U32>}
108
109def take_append_l(xs, ys, n, h):
110 match xs n:
111 case Nil{} 0n:
112 take_zero(ys)
113 case Nil{} 1n+p:
114 Empty.absurd({List.take(&2, U32, ys, 1n+p) == Nil{} : List<&2, U32>}, AB.false_ne_true(h))
115 case Con{x, t} 0n:
116 {==}
117 case Con{x, t} 1n+p:
118 %take_append_l(t, ys, p, h) : {x <> List.take(&2, U32, List.append(&2, U32, t, ys), p) == x <> _ : List<&2, U32>}
119 {==}
120
121# Unpacking
122# =========
123
124law unpack_length4:
125 for +ws: List<&2, U32>
126 {List.length(&2, U32, D.unpack(ws)) == Nat.mul(List.length(&2, U32, ws), 4n) : Nat}
127
128def unpack_length4(ws):
129 match ws:
130 case Nil{}:
131 {==}
132 case Con{w, t}:
133 %unpack_length4(t) : {4n+List.length(&2, U32, D.unpack(t)) == 4n+_ : Nat}
134 {==}
135
136law unpack_length:
137 for +ws: List<&2, U32>
138 {List.length(&2, U32, D.unpack(ws)) == Nat.mul(4n, List.length(&2, U32, ws)) : Nat}
139
140def unpack_length(ws):
141 Equal.trans(Nat, List.length(&2, U32, D.unpack(ws)), Nat.mul(List.length(&2, U32, ws), 4n),
142 Nat.mul(4n, List.length(&2, U32, ws)), unpack_length4(ws), N.mul_comm(List.length(&2, U32, ws), 4n))
143
144law unpack_append:
145 for +xs: List<&2, U32>
146 for +ys: List<&2, U32>
147 {D.unpack(List.append(&2, U32, xs, ys)) == List.append(&2, U32, D.unpack(xs), D.unpack(ys)) : List<&2, U32>}
148
149def unpack_append(xs, ys):
150 match xs:
151 case Nil{}:
152 {==}
153 case Con{+w, t}:
154 %unpack_append(t, ys) :
155 {W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> D.unpack(List.append(&2, U32, t, ys)) ==
156 W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> _ : List<&2, U32>}
157 {==}
158
159law all_bytes_unpack:
160 for +ws: List<&2, U32>
161 {D.all_bytes(D.unpack(ws)) == True{} : Bool}
162
163def all_bytes_unpack(ws):
164 match ws:
165 case Nil{}:
166 {==}
167 case Con{+w, t}:
168 %Equal.sym(Bool, U32.is_lt(W.byte(w, 0n), 256), True{}, Y.byte_lt(w, 0n)) :
169 {Bool.and(_, Bool.and(U32.is_lt(W.byte(w, 1n), 256), Bool.and(U32.is_lt(W.byte(w, 2n), 256),
170 Bool.and(U32.is_lt(W.byte(w, 3n), 256), D.all_bytes(D.unpack(t)))))) == True{} : Bool}
171 %Equal.sym(Bool, U32.is_lt(W.byte(w, 1n), 256), True{}, Y.byte_lt(w, 1n)) :
172 {Bool.and(True{}, Bool.and(_, Bool.and(U32.is_lt(W.byte(w, 2n), 256),
173 Bool.and(U32.is_lt(W.byte(w, 3n), 256), D.all_bytes(D.unpack(t)))))) == True{} : Bool}
174 %Equal.sym(Bool, U32.is_lt(W.byte(w, 2n), 256), True{}, Y.byte_lt(w, 2n)) :
175 {Bool.and(True{}, Bool.and(True{}, Bool.and(_,
176 Bool.and(U32.is_lt(W.byte(w, 3n), 256), D.all_bytes(D.unpack(t)))))) == True{} : Bool}
177 %Equal.sym(Bool, U32.is_lt(W.byte(w, 3n), 256), True{}, Y.byte_lt(w, 3n)) :
178 {Bool.and(True{}, Bool.and(True{}, Bool.and(True{},
179 Bool.and(_, D.all_bytes(D.unpack(t)))))) == True{} : Bool}
180 %Equal.sym(Bool, D.all_bytes(D.unpack(t)), True{}, all_bytes_unpack(t)) :
181 {Bool.and(True{}, Bool.and(True{}, Bool.and(True{}, Bool.and(True{}, _)))) == True{} : Bool}
182 {==}
183
184law all_bytes_take:
185 for +xs: List<&2, U32>
186 for +n: Nat
187 for +h: {D.all_bytes(xs) == True{} : Bool}
188 {D.all_bytes(List.take(&2, U32, xs, n)) == True{} : Bool}
189
190def all_bytes_take(xs, n, h):
191 match xs n:
192 case Nil{} _:
193 {==}
194 case Con{x, t} 0n:
195 {==}
196 case Con{+x, t} 1n+p:
197 %Equal.sym(Bool, U32.is_lt(x, 256), True{}, AB.and_true_l(U32.is_lt(x, 256), D.all_bytes(t), h)) :
198 {Bool.and(_, D.all_bytes(List.take(&2, U32, t, p))) == True{} : Bool}
199 all_bytes_take(t, p, AB.and_true_r(U32.is_lt(x, 256), D.all_bytes(t), h))