1 import Base 2 import lawful-bytes@0.1.1.0/defs.bend as D 3 import ./defs.bend as F 4 import ./fields.bend as C 5 import ./LAWS.bend as L 6 import lawful-bytes@0.1.1.0/proof_core.bend as BC 7 import ./proof_list.bend as Q 8 import ./proof_cut.bend as Z 9 import ./proof_num.bend as NU 10 import ./proof_digits.bend as DG 11 12 # Proofs of the laws: `def L.name` proves `law name` of LAWS.bend. A Bytes can 13 # be used once, so each law about one goes through lawful-bytes' mirror 14 # (BC.bmirror): BC.BT(len, t) with a Tree t. 15 16 # Laws about a Bytes 17 # ================== 18 19 # One wrapper per law (written mechanically from LAWS.bend): it mirrors each 20 # Bytes b, rewrites the goal, transports the hypotheses and calls the mirror 21 # lemma `name_t`, which is law `name` with b replaced by BC.BT(l_b, t_b). 22 23 def cut_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, 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}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) -> 24 {F.pieces(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n)), D.view(b), U32.to_nat(from)) == List.take(&2, List<&2, U32>, F.split(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), n) : List<&2, List<&2, U32>>}: 25 (+l_b, m2_b) = m_b 26 (+t_b, +e_b) = m2_b 27 %e_b : {F.pieces(Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n)), D.view(_), U32.to_nat(from)) == List.take(&2, List<&2, U32>, F.split(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), n) : List<&2, List<&2, U32>>} 28 +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h) 29 +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht) 30 Z.cut_view_t(l_b, t_b, d, from, to, sep, n, h_t, hft, ht_t, hs) 31 32 def L.cut_view(b, d, from, to, sep, n, h, hft, ht, hs): 33 cut_view.go(b, d, from, to, sep, n, h, hft, ht, hs, BC.bmirror(b)) 34 35 def cut_ends.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, 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}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) -> 36 {F.nats(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from)), n) : List<&2, Nat>}: 37 (+l_b, m2_b) = m_b 38 (+t_b, +e_b) = m2_b 39 %e_b : {F.nats(Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n))) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from)), n) : List<&2, Nat>} 40 +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h) 41 +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht) 42 Z.cut_ends_t(l_b, t_b, d, from, to, sep, n, h_t, hft, ht_t, hs) 43 44 def L.cut_ends(b, d, from, to, sep, n, h, hft, ht, hs): 45 cut_ends.go(b, d, from, to, sep, n, h, hft, ht, hs, BC.bmirror(b)) 46 47 def cut_bounds.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, 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}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) -> 48 {F.within(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n)), U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}: 49 (+l_b, m2_b) = m_b 50 (+t_b, +e_b) = m2_b 51 %e_b : {F.within(Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n)), U32.to_nat(from), U32.to_nat(to)) == True{} : Bool} 52 +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h) 53 +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht) 54 Z.cut_bounds_t(l_b, t_b, d, from, to, sep, n, h_t, hft, ht_t, hs) 55 56 def L.cut_bounds(b, d, from, to, sep, n, h, hft, ht, hs): 57 cut_bounds.go(b, d, from, to, sep, n, h, hft, ht, hs, BC.bmirror(b)) 58 59 def cut_pair.go(-b: D.Bytes, +from: U32, +to: U32, +sep: U32, +n: Nat, m_b: BC.BMirror(b)) -> 60 {C.cut(b, from, to, sep, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) : D.Bytes & List<&2, U32>}: 61 (+l_b, m2_b) = m_b 62 (+t_b, +e_b) = m2_b 63 %e_b : {C.cut(_, from, to, sep, n) == (_, Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n))) : D.Bytes & List<&2, U32>} 64 Z.cut_pair_t(l_b, t_b, from, to, sep, n) 65 66 def L.cut_pair(b, from, to, sep, n): 67 cut_pair.go(b, from, to, sep, n, BC.bmirror(b)) 68 69 def num_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: 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}, m_b: BC.BMirror(b)) -> 70 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) == F.decb(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), Nat.pow(2n, 32n)) : Maybe<&2, Nat>}: 71 (+l_b, m2_b) = m_b 72 (+t_b, +e_b) = m2_b 73 %e_b : {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(_, from, to))) == F.decb(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), Nat.pow(2n, 32n)) : Maybe<&2, Nat>} 74 +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h) 75 +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht) 76 NU.num_view_t(l_b, t_b, d, from, to, h_t, hft, ht_t) 77 78 def L.num_view(b, d, from, to, h, hft, ht): 79 num_view.go(b, d, from, to, h, hft, ht, BC.bmirror(b)) 80 81 def num_pair.go(-b: D.Bytes, +from: U32, +to: U32, m_b: BC.BMirror(b)) -> 82 {C.num(b, from, to) == (b, Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) : D.Bytes & Maybe<&2, U32>}: 83 (+l_b, m2_b) = m_b 84 (+t_b, +e_b) = m2_b 85 %e_b : {C.num(_, from, to) == (_, Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(_, from, to))) : D.Bytes & Maybe<&2, U32>} 86 NU.num_pair_t(l_b, t_b, from, to) 87 88 def L.num_pair(b, from, to): 89 num_pair.go(b, from, to, BC.bmirror(b)) 90 91 def digits_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: 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}, m_b: BC.BMirror(b)) -> 92 {Pair.snd(D.Bytes, Bool, C.digits(b, from, to)) == F.all_digits(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool}: 93 (+l_b, m2_b) = m_b 94 (+t_b, +e_b) = m2_b 95 %e_b : {Pair.snd(D.Bytes, Bool, C.digits(_, from, to)) == F.all_digits(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool} 96 +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h) 97 +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht) 98 DG.digits_view_t(l_b, t_b, d, from, to, h_t, hft, ht_t) 99 100 def L.digits_view(b, d, from, to, h, hft, ht): 101 digits_view.go(b, d, from, to, h, hft, ht, BC.bmirror(b)) 102 103 def digits_pair.go(-b: D.Bytes, +from: U32, +to: U32, m_b: BC.BMirror(b)) -> 104 {C.digits(b, from, to) == (b, Pair.snd(D.Bytes, Bool, C.digits(b, from, to))) : D.Bytes & Bool}: 105 (+l_b, m2_b) = m_b 106 (+t_b, +e_b) = m2_b 107 %e_b : {C.digits(_, from, to) == (_, Pair.snd(D.Bytes, Bool, C.digits(_, from, to))) : D.Bytes & Bool} 108 DG.digits_pair_t(l_b, t_b, from, to) 109 110 def L.digits_pair(b, from, to): 111 digits_pair.go(b, from, to, BC.bmirror(b)) 112 113 def put_dec_view.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}, m_b: BC.BMirror(b)) -> 114 {D.view(C.put_dec(b, n)) == List.append(&2, U32, D.view(b), F.show(n)) : List<&2, U32>}: 115 (+l_b, m2_b) = m_b 116 (+t_b, +e_b) = m2_b 117 %e_b : {D.view(C.put_dec(_, n)) == List.append(&2, U32, D.view(_), F.show(n)) : List<&2, U32>} 118 +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h) 119 +hc_t = BC.tr(x => {Nat.is_le(Nat.add(D.size(x), 10n), D.cap(x)) == True{} : Bool}, b, l_b, t_b, e_b, hc) 120 DG.put_dec_view_t(l_b, t_b, d, n, h_t, hc_t) 121 122 def L.put_dec_view(b, d, n, h, hc): 123 put_dec_view.go(b, d, n, h, hc, BC.bmirror(b)) 124 125 def put_dec_ok.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}, m_b: BC.BMirror(b)) -> 126 {D.ok(C.put_dec(b, n), d) == True{} : Bool}: 127 (+l_b, m2_b) = m_b 128 (+t_b, +e_b) = m2_b 129 %e_b : {D.ok(C.put_dec(_, n), d) == True{} : Bool} 130 +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h) 131 +hc_t = BC.tr(x => {Nat.is_le(Nat.add(D.size(x), 10n), D.cap(x)) == True{} : Bool}, b, l_b, t_b, e_b, hc) 132 DG.put_dec_ok_t(l_b, t_b, d, n, h_t, hc_t) 133 134 def L.put_dec_ok(b, d, n, h, hc): 135 put_dec_ok.go(b, d, n, h, hc, BC.bmirror(b)) 136 137 138 # Lists, text and decimal numbers (no Bytes parameter) 139 # ==================================================== 140 141 def L.split_length(xs, sep): 142 Q.split_length(xs, sep) 143 144 def L.split_join(xs, sep): 145 Q.split_join(xs, sep) 146 147 def L.split_text(xs, sep): 148 Q.split_text(xs, sep) 149 150 def L.join_text(ps, sep): 151 Q.join_text(ps, sep) 152 153 def L.text_codes(s): 154 Q.text_codes(s) 155 156 def L.join_at(ps, sep, k, h): 157 Q.join_at(ps, sep, k, h) 158 159 def L.ends_join(ps, sep, from, k, h): 160 Q.ends_join(ps, sep, from, k, h) 161 162 def L.pieces_length(es, xs, from): 163 Q.pieces_length(es, xs, from) 164 165 def L.decb_fits(xs, n, h, hn): 166 Q.decb_fits(xs, n, h, hn)