PROOF.bend

lawful-bytes@0.1.1.0 · 552 lines · 39 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-bytes@0.1.1.0/fast.bend as FA
5import lawful-bytes@0.1.1.0/LAWS.bend as L
6import lawful-bytes@0.1.1.0/proof_core.bend as C
7import lawful-bytes@0.1.1.0/proof_ops.bend as O
8import lawful-bytes@0.1.1.0/proof_append.bend as X
9import lawful-bytes@0.1.1.0/proof_find.bend as F
10import lawful-bytes@0.1.1.0/proof_same.bend as S
11import lawful-bytes@0.1.1.0/proof_grow.bend as G
12import lawful-bytes@0.1.1.0/proof_shift.bend as H
13import lawful-bytes@0.1.1.0/proof_list.bend as Q
14import lawful-bytes@0.1.1.0/proof_fast_find.bend as FF
15import lawful-bytes@0.1.1.0/proof_fast_find2.bend as FF2
16import lawful-bytes@0.1.1.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