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