PROOF.bend
lawful-bytes@0.1.0.0 · 552 lines · 0 definitions
1import Base
2import lawful-bytes@0.1.0.0/defs.bend as D
3import lawful-bytes@0.1.0.0/bytes.bend as B
4import lawful-bytes@0.1.0.0/fast.bend as FA
5import lawful-bytes@0.1.0.0/LAWS.bend as L
6import lawful-bytes@0.1.0.0/proof_core.bend as C
7import lawful-bytes@0.1.0.0/proof_ops.bend as O
8import lawful-bytes@0.1.0.0/proof_append.bend as X
9import lawful-bytes@0.1.0.0/proof_find.bend as F
10import lawful-bytes@0.1.0.0/proof_same.bend as S
11import lawful-bytes@0.1.0.0/proof_grow.bend as G
12import lawful-bytes@0.1.0.0/proof_shift.bend as H
13import lawful-bytes@0.1.0.0/proof_list.bend as Q
14import lawful-bytes@0.1.0.0/proof_fast_find.bend as FF
15import lawful-bytes@0.1.0.0/proof_fast_find2.bend as FF2
16import lawful-bytes@0.1.0.0/proof_fast_append.bend as FX
17
18# Proofs of the laws: `def L.name` proves `law name` of LAWS.bend. A Bytes can
19# be used once, so each law about one goes through its mirror (C.bmirror):
20# BT(len, t) with a Tree<U32> t, about which the lemmas may say as much as they
21# need. The `.go` def takes the mirror apart, rewrites the goal and transports
22# the hypotheses (C.tr).
23
24# Reading
25# =======
26
27def at_view.go(-b: D.Bytes, +d: Nat, +i: U32, h: {D.ok(b, d) == True{} : Bool},
28 hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}, m: C.BMirror(b)) ->
29 {Some{Pair.snd(D.Bytes, U32, B.at(b, i))} == List.get(&2, U32, D.view(b), U32.to_nat(i)) : Maybe<&2, U32>}:
30 (+len, m2) = m
31 (+t, +e) = m2
32 %e : {Some{Pair.snd(D.Bytes, U32, B.at(_, i))} == List.get(&2, U32, D.view(_), U32.to_nat(i)) : Maybe<&2, U32>}
33 +h2 = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, len, t, e, h)
34 C.at_view_t(len, t, d, i, C.ok_full(len, t, d, h2), C.ok_d(len, t, d, h2), C.ok_len(len, t, d, h2),
35 C.tr(x => {Nat.is_lt(U32.to_nat(i), D.size(x)) == True{} : Bool}, b, len, t, e, hi))
36
37def L.at_view(b, d, i, h, hi):
38 at_view.go(b, d, i, h, hi, C.bmirror(b))
39
40# Laws about a Bytes
41# ==================
42
43# One wrapper per law (written mechanically from LAWS.bend): the mirror lemma
44# `name_t` is law `name` with each Bytes b replaced by C.BT(l_b, t_b).
45
46def view_size.go(-b: D.Bytes, +d: Nat, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
47 {List.length(&2, U32, D.view(b)) == D.size(b) : Nat}:
48 (+l_b, m2_b) = m_b
49 (+t_b, +e_b) = m2_b
50 %e_b : {List.length(&2, U32, D.view(_)) == D.size(_) : Nat}
51 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
52 O.view_size_t(l_b, t_b, d, h_t)
53
54def L.view_size(b, d, h):
55 view_size.go(b, d, h, C.bmirror(b))
56
57def view_bytes.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
58 {D.all_bytes(D.view(b)) == True{} : Bool}:
59 (+l_b, m2_b) = m_b
60 (+t_b, +e_b) = m2_b
61 %e_b : {D.all_bytes(D.view(_)) == True{} : Bool}
62 O.view_bytes_t(l_b, t_b)
63
64def L.view_bytes(b):
65 view_bytes.go(b, C.bmirror(b))
66
67def cap_ok.go(-b: D.Bytes, +d: Nat, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
68 {D.cap(b) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}:
69 (+l_b, m2_b) = m_b
70 (+t_b, +e_b) = m2_b
71 %e_b : {D.cap(_) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
72 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
73 O.cap_ok_t(l_b, t_b, d, h_t)
74
75def L.cap_ok(b, d, h):
76 cap_ok.go(b, d, h, C.bmirror(b))
77
78def grow_view.go(-b: D.Bytes, +d: Nat, +e: Nat, h: {D.ok(b, d) == True{} : Bool}, he: {Nat.is_le(d, e) == True{} : Bool}, he29: {Nat.is_le(e, 29n) == True{} : Bool}, m_b: C.BMirror(b)) ->
79 {D.view(B.grow(b, e)) == D.view(b) : List<&2, U32>}:
80 (+l_b, m2_b) = m_b
81 (+t_b, +e_b) = m2_b
82 %e_b : {D.view(B.grow(_, e)) == D.view(_) : List<&2, U32>}
83 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
84 G.grow_view_t(l_b, t_b, d, e, h_t, he, he29)
85
86def L.grow_view(b, d, e, h, he, he29):
87 grow_view.go(b, d, e, h, he, he29, C.bmirror(b))
88
89def grow_ok.go(-b: D.Bytes, +d: Nat, +e: Nat, h: {D.ok(b, d) == True{} : Bool}, he: {Nat.is_le(d, e) == True{} : Bool}, he29: {Nat.is_le(e, 29n) == True{} : Bool}, m_b: C.BMirror(b)) ->
90 {D.ok(B.grow(b, e), e) == True{} : Bool}:
91 (+l_b, m2_b) = m_b
92 (+t_b, +e_b) = m2_b
93 %e_b : {D.ok(B.grow(_, e), e) == True{} : Bool}
94 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
95 G.grow_ok_t(l_b, t_b, d, e, h_t, he, he29)
96
97def L.grow_ok(b, d, e, h, he, he29):
98 grow_ok.go(b, d, e, h, he, he29, C.bmirror(b))
99
100def at_pair.go(-b: D.Bytes, +i: U32, m_b: C.BMirror(b)) ->
101 {B.at(b, i) == (b, Pair.snd(D.Bytes, U32, B.at(b, i))) : D.Bytes & U32}:
102 (+l_b, m2_b) = m_b
103 (+t_b, +e_b) = m2_b
104 %e_b : {B.at(_, i) == (_, Pair.snd(D.Bytes, U32, B.at(_, i))) : D.Bytes & U32}
105 C.at_pair_t(l_b, t_b, i)
106
107def L.at_pair(b, i):
108 at_pair.go(b, i, C.bmirror(b))
109
110def find_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc: {U32.is_lt(c, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
111 {U32.to_nat(Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) == D.first(D.view(b), U32.to_nat(from), U32.to_nat(to), c) : Nat}:
112 (+l_b, m2_b) = m_b
113 (+t_b, +e_b) = m2_b
114 %e_b : {U32.to_nat(Pair.snd(D.Bytes, U32, B.find(_, from, to, c))) == D.first(D.view(_), U32.to_nat(from), U32.to_nat(to), c) : Nat}
115 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
116 +ht_t = C.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
117 F.find_view_t(l_b, t_b, d, from, to, c, h_t, hft, ht_t, hc)
118
119def L.find_view(b, d, from, to, c, h, hft, ht, hc):
120 find_view.go(b, d, from, to, c, h, hft, ht, hc, C.bmirror(b))
121
122def find_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c: U32, m_b: C.BMirror(b)) ->
123 {B.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) : D.Bytes & U32}:
124 (+l_b, m2_b) = m_b
125 (+t_b, +e_b) = m2_b
126 %e_b : {B.find(_, from, to, c) == (_, Pair.snd(D.Bytes, U32, B.find(_, from, to, c))) : D.Bytes & U32}
127 F.find_pair_t(l_b, t_b, from, to, c)
128
129def L.find_pair(b, from, to, c):
130 find_pair.go(b, from, to, c, C.bmirror(b))
131
132def find2_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c1: U32, +c2: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc1: {U32.is_lt(c1, 256) == True{} : Bool}, hc2: {U32.is_lt(c2, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
133 {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2(b, from, to, c1, c2))) == D.first2(D.view(b), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}:
134 (+l_b, m2_b) = m_b
135 (+t_b, +e_b) = m2_b
136 %e_b : {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2(_, from, to, c1, c2))) == D.first2(D.view(_), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
137 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
138 +ht_t = C.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
139 F.find2_view_t(l_b, t_b, d, from, to, c1, c2, h_t, hft, ht_t, hc1, hc2)
140
141def L.find2_view(b, d, from, to, c1, c2, h, hft, ht, hc1, hc2):
142 find2_view.go(b, d, from, to, c1, c2, h, hft, ht, hc1, hc2, C.bmirror(b))
143
144def find2_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c1: U32, +c2: U32, m_b: C.BMirror(b)) ->
145 {B.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, B.find2(b, from, to, c1, c2))) : D.Bytes & U32}:
146 (+l_b, m2_b) = m_b
147 (+t_b, +e_b) = m2_b
148 %e_b : {B.find2(_, from, to, c1, c2) == (_, Pair.snd(D.Bytes, U32, B.find2(_, from, to, c1, c2))) : D.Bytes & U32}
149 F.find2_pair_t(l_b, t_b, from, to, c1, c2)
150
151def L.find2_pair(b, from, to, c1, c2):
152 find2_pair.go(b, from, to, c1, c2, C.bmirror(b))
153
154def same_view.go(-a: D.Bytes, -b: D.Bytes, +d: Nat, +e: Nat, +i: U32, +j: U32, +n: U32, ha: {D.ok(a, d) == True{} : Bool}, hb: {D.ok(b, e) == True{} : Bool}, hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(a)) == True{} : Bool}, hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}, m_a: C.BMirror(a), m_b: C.BMirror(b)) ->
155 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))) == D.list_eq(D.slice(D.view(a), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}:
156 (+l_a, m2_a) = m_a
157 (+t_a, +e_a) = m2_a
158 (+l_b, m2_b) = m_b
159 (+t_b, +e_b) = m2_b
160 %e_a : {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(_, i, b, j, n))) == D.list_eq(D.slice(D.view(_), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}
161 %e_b : {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(C.BT(l_a, t_a), i, _, j, n))) == D.list_eq(D.slice(D.view(C.BT(l_a, t_a)), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(_), U32.to_nat(j), U32.to_nat(n))) : Bool}
162 +ha_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, a, l_a, t_a, e_a, ha)
163 +hb_t = C.tr(x => {D.ok(x, e) == True{} : Bool}, b, l_b, t_b, e_b, hb)
164 +hi_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(x)) == True{} : Bool}, a, l_a, t_a, e_a, hi)
165 +hj_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hj)
166 S.same_view_t(l_a, t_a, l_b, t_b, d, e, i, j, n, ha_t, hb_t, hi_t, hj_t)
167
168def L.same_view(a, b, d, e, i, j, n, ha, hb, hi, hj):
169 same_view.go(a, b, d, e, i, j, n, ha, hb, hi, hj, C.bmirror(a), C.bmirror(b))
170
171def same_pair.go(-a: D.Bytes, -b: D.Bytes, +i: U32, +j: U32, +n: U32, m_a: C.BMirror(a), m_b: C.BMirror(b)) ->
172 {B.same(a, i, b, j, n) == (a, (b, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))))) : D.Bytes & (D.Bytes & Bool)}:
173 (+l_a, m2_a) = m_a
174 (+t_a, +e_a) = m2_a
175 (+l_b, m2_b) = m_b
176 (+t_b, +e_b) = m2_b
177 %e_a : {B.same(_, i, b, j, n) == (_, (b, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(_, i, b, j, n))))) : D.Bytes & (D.Bytes & Bool)}
178 %e_b : {B.same(C.BT(l_a, t_a), i, _, j, n) == (C.BT(l_a, t_a), (_, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(C.BT(l_a, t_a), i, _, j, n))))) : D.Bytes & (D.Bytes & Bool)}
179 S.same_pair_t(l_a, t_a, l_b, t_b, i, j, n)
180
181def L.same_pair(a, b, i, j, n):
182 same_pair.go(a, b, i, j, n, C.bmirror(a), C.bmirror(b))
183
184def set_view.go(-b: D.Bytes, +d: Nat, +i: U32, +v: U32, h: {D.ok(b, d) == True{} : Bool}, hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}, hv: {U32.is_lt(v, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
185 {D.view(B.set(b, i, v)) == List.set(&2, U32, D.view(b), U32.to_nat(i), v) : List<&2, U32>}:
186 (+l_b, m2_b) = m_b
187 (+t_b, +e_b) = m2_b
188 %e_b : {D.view(B.set(_, i, v)) == List.set(&2, U32, D.view(_), U32.to_nat(i), v) : List<&2, U32>}
189 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
190 +hi_t = C.tr(x => {Nat.is_lt(U32.to_nat(i), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hi)
191 O.set_view_t(l_b, t_b, d, i, v, h_t, hi_t, hv)
192
193def L.set_view(b, d, i, v, h, hi, hv):
194 set_view.go(b, d, i, v, h, hi, hv, C.bmirror(b))
195
196def set_ok.go(-b: D.Bytes, +d: Nat, +i: U32, +v: U32, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
197 {D.ok(B.set(b, i, v), d) == True{} : Bool}:
198 (+l_b, m2_b) = m_b
199 (+t_b, +e_b) = m2_b
200 %e_b : {D.ok(B.set(_, i, v), d) == True{} : Bool}
201 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
202 O.set_ok_t(l_b, t_b, d, i, v, h_t)
203
204def L.set_ok(b, d, i, v, h):
205 set_ok.go(b, d, i, v, h, C.bmirror(b))
206
207def push_view.go(-b: D.Bytes, +d: Nat, +v: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}, hv: {U32.is_lt(v, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
208 {D.view(B.push(b, v)) == List.append(&2, U32, D.view(b), [v]) : List<&2, U32>}:
209 (+l_b, m2_b) = m_b
210 (+t_b, +e_b) = m2_b
211 %e_b : {D.view(B.push(_, v)) == List.append(&2, U32, D.view(_), [v]) : List<&2, U32>}
212 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
213 +hc_t = C.tr(x => {Nat.is_lt(D.size(x), D.cap(x)) == True{} : Bool}, b, l_b, t_b, e_b, hc)
214 O.push_view_t(l_b, t_b, d, v, h_t, hc_t, hv)
215
216def L.push_view(b, d, v, h, hc, hv):
217 push_view.go(b, d, v, h, hc, hv, C.bmirror(b))
218
219def push_ok.go(-b: D.Bytes, +d: Nat, +v: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
220 {D.ok(B.push(b, v), d) == True{} : Bool}:
221 (+l_b, m2_b) = m_b
222 (+t_b, +e_b) = m2_b
223 %e_b : {D.ok(B.push(_, v), d) == True{} : Bool}
224 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
225 +hc_t = C.tr(x => {Nat.is_lt(D.size(x), D.cap(x)) == True{} : Bool}, b, l_b, t_b, e_b, hc)
226 O.push_ok_t(l_b, t_b, d, v, h_t, hc_t)
227
228def L.push_ok(b, d, v, h, hc):
229 push_ok.go(b, d, v, h, hc, C.bmirror(b))
230
231def append_view.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +e: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, he: {D.ok(src, e) == True{} : Bool}, hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
232 {D.view(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n))) == List.append(&2, U32, D.view(dst), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
233 (+l_dst, m2_dst) = m_dst
234 (+t_dst, +e_dst) = m2_dst
235 (+l_src, m2_src) = m_src
236 (+t_src, +e_src) = m2_src
237 %e_dst : {D.view(Pair.fst(D.Bytes, D.Bytes, B.append(_, src, s, n))) == List.append(&2, U32, D.view(_), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
238 %e_src : {D.view(Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(l_dst, t_dst), _, s, n))) == List.append(&2, U32, D.view(C.BT(l_dst, t_dst)), D.slice(D.view(_), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
239 +hd_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hd)
240 +he_t = C.tr(x => {D.ok(x, e) == True{} : Bool}, src, l_src, t_src, e_src, he)
241 +hs_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(x)) == True{} : Bool}, src, l_src, t_src, e_src, hs)
242 +hc_t = C.tr(x => {Nat.is_le(Nat.add(D.size(x), U32.to_nat(n)), D.cap(x)) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hc)
243 X.append_view_t(l_dst, t_dst, l_src, t_src, d, e, s, n, hd_t, he_t, hs_t, hc_t)
244
245def L.append_view(dst, src, d, e, s, n, hd, he, hs, hc):
246 append_view.go(dst, src, d, e, s, n, hd, he, hs, hc, C.bmirror(dst), C.bmirror(src))
247
248def append_ok.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
249 {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), d) == True{} : Bool}:
250 (+l_dst, m2_dst) = m_dst
251 (+t_dst, +e_dst) = m2_dst
252 (+l_src, m2_src) = m_src
253 (+t_src, +e_src) = m2_src
254 %e_dst : {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(_, src, s, n)), d) == True{} : Bool}
255 %e_src : {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(l_dst, t_dst), _, s, n)), d) == True{} : Bool}
256 +hd_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hd)
257 +hc_t = C.tr(x => {Nat.is_le(Nat.add(D.size(x), U32.to_nat(n)), D.cap(x)) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hc)
258 X.append_ok_t(l_dst, t_dst, l_src, t_src, d, s, n, hd_t, hc_t)
259
260def L.append_ok(dst, src, d, s, n, hd, hc):
261 append_ok.go(dst, src, d, s, n, hd, hc, C.bmirror(dst), C.bmirror(src))
262
263def append_pair.go(-dst: D.Bytes, -src: D.Bytes, +s: U32, +n: U32, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
264 {B.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}:
265 (+l_dst, m2_dst) = m_dst
266 (+t_dst, +e_dst) = m2_dst
267 (+l_src, m2_src) = m_src
268 (+t_src, +e_src) = m2_src
269 %e_dst : {B.append(_, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(_, src, s, n)), src) : D.Bytes & D.Bytes}
270 %e_src : {B.append(C.BT(l_dst, t_dst), _, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(l_dst, t_dst), _, s, n)), _) : D.Bytes & D.Bytes}
271 X.append_pair_t(l_dst, t_dst, l_src, t_src, s, n)
272
273def L.append_pair(dst, src, s, n):
274 append_pair.go(dst, src, s, n, C.bmirror(dst), C.bmirror(src))
275
276def len_view.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
277 {U32.to_nat(Pair.snd(D.Bytes, U32, B.len(b))) == D.size(b) : Nat}:
278 (+l_b, m2_b) = m_b
279 (+t_b, +e_b) = m2_b
280 %e_b : {U32.to_nat(Pair.snd(D.Bytes, U32, B.len(_))) == D.size(_) : Nat}
281 {==}
282
283def L.len_view(b):
284 len_view.go(b, C.bmirror(b))
285
286def len_pair.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
287 {B.len(b) == (b, Pair.snd(D.Bytes, U32, B.len(b))) : D.Bytes & U32}:
288 (+l_b, m2_b) = m_b
289 (+t_b, +e_b) = m2_b
290 %e_b : {B.len(_) == (_, Pair.snd(D.Bytes, U32, B.len(_))) : D.Bytes & U32}
291 {==}
292
293def L.len_pair(b):
294 len_pair.go(b, C.bmirror(b))
295
296def capacity_view.go(-b: D.Bytes, +d: Nat, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
297 {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity(b))) == D.cap(b) : Nat}:
298 (+l_b, m2_b) = m_b
299 (+t_b, +e_b) = m2_b
300 %e_b : {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity(_))) == D.cap(_) : Nat}
301 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
302 O.capacity_view_t(l_b, t_b, d, h_t)
303
304def L.capacity_view(b, d, h):
305 capacity_view.go(b, d, h, C.bmirror(b))
306
307def capacity_pair.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
308 {B.capacity(b) == (b, Pair.snd(D.Bytes, U32, B.capacity(b))) : D.Bytes & U32}:
309 (+l_b, m2_b) = m_b
310 (+t_b, +e_b) = m2_b
311 %e_b : {B.capacity(_) == (_, Pair.snd(D.Bytes, U32, B.capacity(_))) : D.Bytes & U32}
312 O.capacity_pair_t(l_b, t_b)
313
314def L.capacity_pair(b):
315 capacity_pair.go(b, C.bmirror(b))
316
317def truncate_view.go(-b: D.Bytes, +n: U32, h: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
318 {D.view(B.truncate(b, n)) == List.take(&2, U32, D.view(b), U32.to_nat(n)) : List<&2, U32>}:
319 (+l_b, m2_b) = m_b
320 (+t_b, +e_b) = m2_b
321 %e_b : {D.view(B.truncate(_, n)) == List.take(&2, U32, D.view(_), U32.to_nat(n)) : List<&2, U32>}
322 +h_t = C.tr(x => {Nat.is_le(U32.to_nat(n), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, h)
323 O.truncate_view_t(l_b, t_b, n, h_t)
324
325def L.truncate_view(b, n, h):
326 truncate_view.go(b, n, h, C.bmirror(b))
327
328def truncate_ok.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hn: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
329 {D.ok(B.truncate(b, n), d) == True{} : Bool}:
330 (+l_b, m2_b) = m_b
331 (+t_b, +e_b) = m2_b
332 %e_b : {D.ok(B.truncate(_, n), d) == True{} : Bool}
333 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
334 +hn_t = C.tr(x => {Nat.is_le(U32.to_nat(n), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hn)
335 O.truncate_ok_t(l_b, t_b, d, n, h_t, hn_t)
336
337def L.truncate_ok(b, d, n, h, hn):
338 truncate_ok.go(b, d, n, h, hn, C.bmirror(b))
339
340def shift_view.go(-b: D.Bytes, +d: Nat, +k: U32, h: {D.ok(b, d) == True{} : Bool}, hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
341 {D.view(B.shift(b, k)) == List.drop(&2, U32, D.view(b), U32.to_nat(k)) : List<&2, U32>}:
342 (+l_b, m2_b) = m_b
343 (+t_b, +e_b) = m2_b
344 %e_b : {D.view(B.shift(_, k)) == List.drop(&2, U32, D.view(_), U32.to_nat(k)) : List<&2, U32>}
345 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
346 +hk_t = C.tr(x => {Nat.is_le(U32.to_nat(k), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hk)
347 H.shift_view_t(l_b, t_b, d, k, h_t, hk_t)
348
349def L.shift_view(b, d, k, h, hk):
350 shift_view.go(b, d, k, h, hk, C.bmirror(b))
351
352def shift_ok.go(-b: D.Bytes, +d: Nat, +k: U32, h: {D.ok(b, d) == True{} : Bool}, hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
353 {D.ok(B.shift(b, k), d) == True{} : Bool}:
354 (+l_b, m2_b) = m_b
355 (+t_b, +e_b) = m2_b
356 %e_b : {D.ok(B.shift(_, k), d) == True{} : Bool}
357 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
358 +hk_t = C.tr(x => {Nat.is_le(U32.to_nat(k), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hk)
359 H.shift_ok_t(l_b, t_b, d, k, h_t, hk_t)
360
361def L.shift_ok(b, d, k, h, hk):
362 shift_ok.go(b, d, k, h, hk, C.bmirror(b))
363
364def to_list_view.go(-b: D.Bytes, +d: Nat, +s: U32, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
365 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n)) == D.slice(D.view(b), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>}:
366 (+l_b, m2_b) = m_b
367 (+t_b, +e_b) = m2_b
368 %e_b : {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(_, s, n)) == D.slice(D.view(_), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>}
369 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
370 +hs_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hs)
371 S.to_list_view_t(l_b, t_b, d, s, n, h_t, hs_t)
372
373def L.to_list_view(b, d, s, n, h, hs):
374 to_list_view.go(b, d, s, n, h, hs, C.bmirror(b))
375
376def to_list_pair.go(-b: D.Bytes, +s: U32, +n: U32, m_b: C.BMirror(b)) ->
377 {B.to_list(b, s, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n))) : D.Bytes & List<&2, U32>}:
378 (+l_b, m2_b) = m_b
379 (+t_b, +e_b) = m2_b
380 %e_b : {B.to_list(_, s, n) == (_, Pair.snd(D.Bytes, List<&2, U32>, B.to_list(_, s, n))) : D.Bytes & List<&2, U32>}
381 S.to_list_pair_t(l_b, t_b, s, n)
382
383def L.to_list_pair(b, s, n):
384 to_list_pair.go(b, s, n, C.bmirror(b))
385
386def same1_view.go(-b: D.Bytes, +d: Nat, +i: U32, +j: U32, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(b)) == True{} : Bool}, hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
387 {Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n)) == D.list_eq(D.slice(D.view(b), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}:
388 (+l_b, m2_b) = m_b
389 (+t_b, +e_b) = m2_b
390 %e_b : {Pair.snd(D.Bytes, Bool, B.same1(_, i, j, n)) == D.list_eq(D.slice(D.view(_), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(_), U32.to_nat(j), U32.to_nat(n))) : Bool}
391 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
392 +hi_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hi)
393 +hj_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, hj)
394 S.same1_view_t(l_b, t_b, d, i, j, n, h_t, hi_t, hj_t)
395
396def L.same1_view(b, d, i, j, n, h, hi, hj):
397 same1_view.go(b, d, i, j, n, h, hi, hj, C.bmirror(b))
398
399def same1_pair.go(-b: D.Bytes, +i: U32, +j: U32, +n: U32, m_b: C.BMirror(b)) ->
400 {B.same1(b, i, j, n) == (b, Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n))) : D.Bytes & Bool}:
401 (+l_b, m2_b) = m_b
402 (+t_b, +e_b) = m2_b
403 %e_b : {B.same1(_, i, j, n) == (_, Pair.snd(D.Bytes, Bool, B.same1(_, i, j, n))) : D.Bytes & Bool}
404 S.same1_pair_t(l_b, t_b, i, j, n)
405
406def L.same1_pair(b, i, j, n):
407 same1_pair.go(b, i, j, n, C.bmirror(b))
408
409
410# Making and lists (no Bytes parameter)
411# =====================================
412
413def L.empty_view(d):
414 G.empty_view(d)
415
416def L.empty_ok(d, hd):
417 G.empty_ok(d, hd)
418
419def L.of_list_view(d, xs, hd, hn, hb):
420 G.of_list_view(d, xs, hd, hn, hb)
421
422def L.of_list_ok(d, xs, hd, hn):
423 G.of_list_ok(d, xs, hd, hn)
424
425# Facts about the search and comparison definitions
426# =================================================
427
428def L.first_range(xs, from, to, c, hft, ht):
429 Q.first_range(xs, from, to, c, hft, ht)
430
431def L.first_hit(xs, from, to, c, hft, ht, hlt):
432 Q.first_hit(xs, from, to, c, hft, ht, hlt)
433
434def L.first_miss(xs, from, to, c, k, hk1, hk2):
435 Q.first_miss(xs, from, to, c, k, hk1, hk2)
436
437def L.first2_range(xs, from, to, c1, c2, hft, ht):
438 Q.first2_range(xs, from, to, c1, c2, hft, ht)
439
440def L.first2_hit(xs, from, to, c1, c2, hft, ht, hlt):
441 Q.first2_hit(xs, from, to, c1, c2, hft, ht, hlt)
442
443def L.first2_miss(xs, from, to, c1, c2, k, hk1, hk2):
444 Q.first2_miss(xs, from, to, c1, c2, k, hk1, hk2)
445
446def L.list_eq_true(xs, ys, h):
447 Q.list_eq_true(xs, ys, h)
448
449def L.list_eq_refl(xs):
450 Q.list_eq_refl(xs)
451
452# Fast versions (fast.bend)
453# =========================
454
455def fast_find.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc: {U32.is_lt(c, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
456 {FA.find(b, from, to, c) == B.find(b, from, to, c) : D.Bytes & U32}:
457 (+l_b, m2_b) = m_b
458 (+t_b, +e_b) = m2_b
459 %e_b : {FA.find(_, from, to, c) == B.find(_, from, to, c) : D.Bytes & U32}
460 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
461 +ht_t = C.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
462 FF.fast_find_t(l_b, t_b, d, from, to, c, h_t, hft, ht_t, hc)
463
464def L.fast_find(b, d, from, to, c, h, hft, ht, hc):
465 fast_find.go(b, d, from, to, c, h, hft, ht, hc, C.bmirror(b))
466
467def fast_find2.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c1: U32, +c2: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc1: {U32.is_lt(c1, 256) == True{} : Bool}, hc2: {U32.is_lt(c2, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
468 {FA.find2(b, from, to, c1, c2) == B.find2(b, from, to, c1, c2) : D.Bytes & U32}:
469 (+l_b, m2_b) = m_b
470 (+t_b, +e_b) = m2_b
471 %e_b : {FA.find2(_, from, to, c1, c2) == B.find2(_, from, to, c1, c2) : D.Bytes & U32}
472 +h_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
473 +ht_t = C.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
474 FF2.fast_find2_t(l_b, t_b, d, from, to, c1, c2, h_t, hft, ht_t, hc1, hc2)
475
476def L.fast_find2(b, d, from, to, c1, c2, h, hft, ht, hc1, hc2):
477 fast_find2.go(b, d, from, to, c1, c2, h, hft, ht, hc1, hc2, C.bmirror(b))
478
479def fast_find_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c: U32, m_b: C.BMirror(b)) ->
480 {FA.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, FA.find(b, from, to, c))) : D.Bytes & U32}:
481 (+l_b, m2_b) = m_b
482 (+t_b, +e_b) = m2_b
483 %e_b : {FA.find(_, from, to, c) == (_, Pair.snd(D.Bytes, U32, FA.find(_, from, to, c))) : D.Bytes & U32}
484 +rc = FA.rep(c)
485 +MN = U32.min(FF.FG(FA.words(from, to), U32.is_zero(FF.M0(t_b, from, rc)), (from >> 2n : U32), FF.M0(t_b, from, rc), rc, t_b), to)
486 %Equal.sym(D.Bytes & U32, FA.find(C.BT(l_b, t_b), from, to, c), (C.BT(l_b, t_b), MN), FF.fast_eq(l_b, t_b, from, to, c)) :
487 {_ == (C.BT(l_b, t_b), Pair.snd(D.Bytes, U32, _)) : D.Bytes & U32}
488 {==}
489
490def L.fast_find_pair(b, from, to, c):
491 fast_find_pair.go(b, from, to, c, C.bmirror(b))
492
493def fast_find2_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c1: U32, +c2: U32, m_b: C.BMirror(b)) ->
494 {FA.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, FA.find2(b, from, to, c1, c2))) : D.Bytes & U32}:
495 (+l_b, m2_b) = m_b
496 (+t_b, +e_b) = m2_b
497 %e_b : {FA.find2(_, from, to, c1, c2) == (_, Pair.snd(D.Bytes, U32, FA.find2(_, from, to, c1, c2))) : D.Bytes & U32}
498 +r1 = FA.rep(c1)
499 +r2 = FA.rep(c2)
500 +MN = U32.min(FF2.FG2(FA.words(from, to), U32.is_zero(FF2.M02(t_b, from, r1, r2)), (from >> 2n : U32), FF2.M02(t_b, from, r1, r2), r1, r2, t_b), to)
501 %Equal.sym(D.Bytes & U32, FA.find2(C.BT(l_b, t_b), from, to, c1, c2), (C.BT(l_b, t_b), MN), FF2.fast2_eq(l_b, t_b, from, to, c1, c2)) :
502 {_ == (C.BT(l_b, t_b), Pair.snd(D.Bytes, U32, _)) : D.Bytes & U32}
503 {==}
504
505def L.fast_find2_pair(b, from, to, c1, c2):
506 fast_find2_pair.go(b, from, to, c1, c2, C.bmirror(b))
507
508def fast_append_view.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +e: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, he: {D.ok(src, e) == True{} : Bool}, hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
509 {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n))) == List.append(&2, U32, D.view(dst), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
510 (+l_dst, m2_dst) = m_dst
511 (+t_dst, +e_dst) = m2_dst
512 (+l_src, m2_src) = m_src
513 (+t_src, +e_src) = m2_src
514 %e_dst : {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(_, src, s, n))) == List.append(&2, U32, D.view(_), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
515 %e_src : {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(l_dst, t_dst), _, s, n))) == List.append(&2, U32, D.view(C.BT(l_dst, t_dst)), D.slice(D.view(_), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
516 +hd_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hd)
517 +he_t = C.tr(x => {D.ok(x, e) == True{} : Bool}, src, l_src, t_src, e_src, he)
518 +hs_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(x)) == True{} : Bool}, src, l_src, t_src, e_src, hs)
519 +hc_t = C.tr(x => {Nat.is_le(Nat.add(D.size(x), U32.to_nat(n)), D.cap(x)) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hc)
520 FX.fast_append_view_t(l_dst, t_dst, l_src, t_src, d, e, s, n, hd_t, he_t, hs_t, hc_t)
521
522def L.fast_append_view(dst, src, d, e, s, n, hd, he, hs, hc):
523 fast_append_view.go(dst, src, d, e, s, n, hd, he, hs, hc, C.bmirror(dst), C.bmirror(src))
524
525def fast_append_ok.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
526 {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), d) == True{} : Bool}:
527 (+l_dst, m2_dst) = m_dst
528 (+t_dst, +e_dst) = m2_dst
529 (+l_src, m2_src) = m_src
530 (+t_src, +e_src) = m2_src
531 %e_dst : {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(_, src, s, n)), d) == True{} : Bool}
532 %e_src : {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(l_dst, t_dst), _, s, n)), d) == True{} : Bool}
533 +hd_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hd)
534 +hc_t = C.tr(x => {Nat.is_le(Nat.add(D.size(x), U32.to_nat(n)), D.cap(x)) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hc)
535 FX.fast_append_ok_t(l_dst, t_dst, l_src, t_src, d, s, n, hd_t, hc_t)
536
537def L.fast_append_ok(dst, src, d, s, n, hd, hc):
538 fast_append_ok.go(dst, src, d, s, n, hd, hc, C.bmirror(dst), C.bmirror(src))
539
540def fast_append_pair.go(-dst: D.Bytes, -src: D.Bytes, +s: U32, +n: U32, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
541 {FA.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}:
542 (+l_dst, m2_dst) = m_dst
543 (+t_dst, +e_dst) = m2_dst
544 (+l_src, m2_src) = m_src
545 (+t_src, +e_src) = m2_src
546 %e_dst : {FA.append(_, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(_, src, s, n)), src) : D.Bytes & D.Bytes}
547 %e_src : {FA.append(C.BT(l_dst, t_dst), _, s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(l_dst, t_dst), _, s, n)), _) : D.Bytes & D.Bytes}
548 FX.fast_append_pair_t(l_dst, t_dst, l_src, t_src, s, n)
549
550def L.fast_append_pair(dst, src, s, n):
551 fast_append_pair.go(dst, src, s, n, C.bmirror(dst), C.bmirror(src))
552