1 import Base 2 import ./defs.bend as D 3 import ./bytes.bend as B 4 import ./fast.bend as FA 5 import ./LAWS.bend as L 6 import ./proof_core.bend as C 7 import ./proof_ops.bend as O 8 import ./proof_append.bend as X 9 import ./proof_find.bend as F 10 import ./proof_same.bend as S 11 import ./proof_grow.bend as G 12 import ./proof_shift.bend as H 13 import ./proof_list.bend as Q 14 import ./proof_fast_find.bend as FF 15 import ./proof_fast_find2.bend as FF2 16 import ./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 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 27 def 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 37 def 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 46 def 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 54 def L.view_size(b, d, h): 55 view_size.go(b, d, h, C.bmirror(b)) 56 57 def 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 64 def L.view_bytes(b): 65 view_bytes.go(b, C.bmirror(b)) 66 67 def 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 75 def L.cap_ok(b, d, h): 76 cap_ok.go(b, d, h, C.bmirror(b)) 77 78 def 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 86 def L.grow_view(b, d, e, h, he, he29): 87 grow_view.go(b, d, e, h, he, he29, C.bmirror(b)) 88 89 def 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 97 def L.grow_ok(b, d, e, h, he, he29): 98 grow_ok.go(b, d, e, h, he, he29, C.bmirror(b)) 99 100 def 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 107 def L.at_pair(b, i): 108 at_pair.go(b, i, C.bmirror(b)) 109 110 def 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 119 def 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 122 def 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 129 def L.find_pair(b, from, to, c): 130 find_pair.go(b, from, to, c, C.bmirror(b)) 131 132 def 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 141 def 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 144 def 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 151 def L.find2_pair(b, from, to, c1, c2): 152 find2_pair.go(b, from, to, c1, c2, C.bmirror(b)) 153 154 def 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 168 def 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 171 def 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 181 def L.same_pair(a, b, i, j, n): 182 same_pair.go(a, b, i, j, n, C.bmirror(a), C.bmirror(b)) 183 184 def 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 193 def 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 196 def 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 204 def L.set_ok(b, d, i, v, h): 205 set_ok.go(b, d, i, v, h, C.bmirror(b)) 206 207 def 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 216 def L.push_view(b, d, v, h, hc, hv): 217 push_view.go(b, d, v, h, hc, hv, C.bmirror(b)) 218 219 def 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 228 def L.push_ok(b, d, v, h, hc): 229 push_ok.go(b, d, v, h, hc, C.bmirror(b)) 230 231 def 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 245 def 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 248 def 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 260 def 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 263 def 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 273 def L.append_pair(dst, src, s, n): 274 append_pair.go(dst, src, s, n, C.bmirror(dst), C.bmirror(src)) 275 276 def 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 283 def L.len_view(b): 284 len_view.go(b, C.bmirror(b)) 285 286 def 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 293 def L.len_pair(b): 294 len_pair.go(b, C.bmirror(b)) 295 296 def 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 304 def L.capacity_view(b, d, h): 305 capacity_view.go(b, d, h, C.bmirror(b)) 306 307 def 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 314 def L.capacity_pair(b): 315 capacity_pair.go(b, C.bmirror(b)) 316 317 def 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 325 def L.truncate_view(b, n, h): 326 truncate_view.go(b, n, h, C.bmirror(b)) 327 328 def 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 337 def L.truncate_ok(b, d, n, h, hn): 338 truncate_ok.go(b, d, n, h, hn, C.bmirror(b)) 339 340 def 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 349 def L.shift_view(b, d, k, h, hk): 350 shift_view.go(b, d, k, h, hk, C.bmirror(b)) 351 352 def 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 361 def L.shift_ok(b, d, k, h, hk): 362 shift_ok.go(b, d, k, h, hk, C.bmirror(b)) 363 364 def 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 373 def 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 376 def 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 383 def L.to_list_pair(b, s, n): 384 to_list_pair.go(b, s, n, C.bmirror(b)) 385 386 def 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 396 def 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 399 def 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 406 def 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 413 def L.empty_view(d): 414 G.empty_view(d) 415 416 def L.empty_ok(d, hd): 417 G.empty_ok(d, hd) 418 419 def L.of_list_view(d, xs, hd, hn, hb): 420 G.of_list_view(d, xs, hd, hn, hb) 421 422 def 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 428 def L.first_range(xs, from, to, c, hft, ht): 429 Q.first_range(xs, from, to, c, hft, ht) 430 431 def L.first_hit(xs, from, to, c, hft, ht, hlt): 432 Q.first_hit(xs, from, to, c, hft, ht, hlt) 433 434 def L.first_miss(xs, from, to, c, k, hk1, hk2): 435 Q.first_miss(xs, from, to, c, k, hk1, hk2) 436 437 def L.first2_range(xs, from, to, c1, c2, hft, ht): 438 Q.first2_range(xs, from, to, c1, c2, hft, ht) 439 440 def L.first2_hit(xs, from, to, c1, c2, hft, ht, hlt): 441 Q.first2_hit(xs, from, to, c1, c2, hft, ht, hlt) 442 443 def L.first2_miss(xs, from, to, c1, c2, k, hk1, hk2): 444 Q.first2_miss(xs, from, to, c1, c2, k, hk1, hk2) 445 446 def L.list_eq_true(xs, ys, h): 447 Q.list_eq_true(xs, ys, h) 448 449 def L.list_eq_refl(xs): 450 Q.list_eq_refl(xs) 451 452 # Fast versions (fast.bend) 453 # ========================= 454 455 def 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 464 def 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 467 def 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 476 def 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 479 def 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 490 def L.fast_find_pair(b, from, to, c): 491 fast_find_pair.go(b, from, to, c, C.bmirror(b)) 492 493 def 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 505 def L.fast_find2_pair(b, from, to, c1, c2): 506 fast_find2_pair.go(b, from, to, c1, c2, C.bmirror(b)) 507 508 def 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 522 def 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 525 def 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 537 def 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 540 def 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 550 def L.fast_append_pair(dst, src, s, n): 551 fast_append_pair.go(dst, src, s, n, C.bmirror(dst), C.bmirror(src)) 552