1 import Base 2 import ./defs.bend as D 3 import ./proof_base.bend as B 4 import ./proof_tree.bend as P 5 6 # Array.swap and Array.set keep a tree perfect, for any element type. Such 7 # elements cannot be copied, so no mirror: the lemmas return the new array as a 8 # witness beside the equations, and each subtree is used once. 9 10 # Array.size(a) is (b, n) with b == a. 11 def SizeW(-T: Type, -a: Array) -> Type: 12 &b:Array -> &n:U32 -> {Array.size(T, a) == (b, n) : Array & U32} & {b == a : Array} 13 14 law size_node_eq: 15 for -T: Type 16 for -xs: Array 17 for -ys: Array 18 for -b: Array 19 for -n: U32 20 for e: {Array.size(T, xs) == (b, n) : Array & U32} 21 {Array.size(T, ANode{xs, ys}) == (ANode{b, ys}, U32.shl(n)) : Array & U32} 22 23 def size_node_eq(T, xs, ys, b, n, e): 24 %Equal.sym(Array & U32, Array.size(T, xs), (b, n), e) : 25 {Array.size.node(T, ys, _) == (ANode{b, ys}, U32.shl(n)) : Array & U32} 26 {==} 27 28 def size_w.node(-T: Type, -xs: Array, ys: Array, w: SizeW(T, xs)) -> SizeW(T, ANode{xs, ys}): 29 (b, n, e, q) = w 30 (ANode{b, ys}, U32.shl(n), size_node_eq(T, xs, ys, b, n, e), P.anode_eq(T, b, ys, xs, ys, q, {==})) 31 32 def size_w(-T: Type, a: Array) -> SizeW(T, a): 33 match a: 34 case ALeaf{x}: 35 (ALeaf{x}, 1, {==}, {==}) 36 case ANode{xs, ys}: 37 size_w.node(T, xs, ys, size_w(T, xs)) 38 39 # Array.swap.go(a, ...) is (na, old) with na as perfect as a at every depth. 40 def SwapW(-T: Type, -a: Array, -n: U32, -i: U32, -v: T, -z: Bool, -d: Nat) -> Type: 41 &na:Array -> &old:T -> {Array.swap.go(T, a, n, i, v, z) == (na, old) : Array & T} 42 & {D.full(T, na, d) == D.full(T, a, d) : Bool} 43 44 law lo_eq: 45 for -T: Type 46 for -ys: Array 47 for -r: Array & T 48 for -na: Array 49 for -old: T 50 for e: {r == (na, old) : Array & T} 51 {Array.swap.lo(T, ys, r) == (ANode{na, ys}, old) : Array & T} 52 53 def lo_eq(T, ys, r, na, old, e): 54 %Equal.sym(Array & T, r, (na, old), e) : {Array.swap.lo(T, ys, _) == (ANode{na, ys}, old) : Array & T} 55 {==} 56 57 law hi_eq: 58 for -T: Type 59 for -xs: Array 60 for -r: Array & T 61 for -na: Array 62 for -old: T 63 for e: {r == (na, old) : Array & T} 64 {Array.swap.hi(T, xs, r) == (ANode{xs, na}, old) : Array & T} 65 66 def hi_eq(T, xs, r, na, old, e): 67 %Equal.sym(Array & T, r, (na, old), e) : {Array.swap.hi(T, xs, _) == (ANode{xs, na}, old) : Array & T} 68 {==} 69 70 law and_eq_l: 71 for -a: Bool 72 for -c: Bool 73 for -b: Bool 74 for e: {a == c : Bool} 75 {Bool.and(a, b) == Bool.and(c, b) : Bool} 76 77 def and_eq_l(a, c, b, e): 78 %e : {Bool.and(a, b) == Bool.and(_, b) : Bool} 79 {==} 80 81 law and_eq_r: 82 for -b: Bool 83 for -a: Bool 84 for -c: Bool 85 for e: {a == c : Bool} 86 {Bool.and(b, a) == Bool.and(b, c) : Bool} 87 88 def and_eq_r(b, a, c, e): 89 %e : {Bool.and(b, a) == Bool.and(b, _) : Bool} 90 {==} 91 92 def swap_w.lo(-T: Type, -xs: Array, ys: Array, +n: U32, +i: U32, -v: T, +d: Nat, 93 w: SwapW(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n))), B.pred(d))) -> 94 SwapW(T, ANode{xs, ys}, n, i, v, True{}, d): 95 match d: 96 case 0n: 97 (na, old, e, q) = w 98 (ANode{na, ys}, old, 99 lo_eq(T, ys, Array.swap.go(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))), na, old, e), {==}) 100 case 1n+p: 101 (na, old, e, q) = w 102 (ANode{na, ys}, old, 103 lo_eq(T, ys, Array.swap.go(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))), na, old, e), 104 and_eq_l(D.full(T, na, p), D.full(T, xs, p), D.full(T, ys, p), q)) 105 106 def swap_w.hi(-T: Type, xs: Array, -ys: Array, +n: U32, +i: U32, -v: T, +d: Nat, 107 w: SwapW(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v, U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n))), B.pred(d))) -> 108 SwapW(T, ANode{xs, ys}, n, i, v, False{}, d): 109 match d: 110 case 0n: 111 (na, old, e, q) = w 112 (ANode{xs, na}, old, 113 hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v, 114 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e), {==}) 115 case 1n+p: 116 (na, old, e, q) = w 117 (ANode{xs, na}, old, 118 hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v, 119 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e), 120 and_eq_r(D.full(T, xs, p), D.full(T, na, p), D.full(T, ys, p), q)) 121 122 def swap_w(-T: Type, a: Array, +n: U32, +i: U32, v: T, +z: Bool, +d: Nat) -> SwapW(T, a, n, i, v, z, d): 123 match a z d: 124 case ALeaf{x} _ 0n: 125 (ALeaf{v}, x, {==}, {==}) 126 case ALeaf{x} _ 1n+p: 127 (ALeaf{v}, x, {==}, {==}) 128 case ANode{xs, ys} True{} _: 129 +h = U32.shr(n) 130 swap_w.lo(T, xs, ys, n, i, v, d, swap_w(T, xs, h, i, v, U32.is_lt(i, U32.shr(h)), B.pred(d))) 131 case ANode{xs, ys} False{} _: 132 +h = U32.shr(n) 133 +j = U32.sub(i, h) 134 swap_w.hi(T, xs, ys, n, i, v, d, swap_w(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)), B.pred(d))) 135 136 # The array a swap leaves is perfect: the steps after Array.size. 137 def swap_full.fin(-T: Type, -a: Array, -b: Array, +n: U32, +i: U32, -v: T, +d: Nat, 138 hf: {D.full(T, a, d) == True{} : Bool}, q: {b == a : Array}, 139 w: SwapW(T, b, n, U32.and(i, U32.sub(n, 1)), v, U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)), d)) -> 140 {D.full(T, Pair.fst(Array, T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v, 141 U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)))), d) == True{} : Bool}: 142 (na, old, e, f) = w 143 %Equal.sym(Array & T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v, 144 U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n))), (na, old), e) : 145 {D.full(T, Pair.fst(Array, T, _), d) == True{} : Bool} 146 Equal.trans(Bool, D.full(T, na, d), D.full(T, b, d), True{}, f, 147 Equal.trans(Bool, D.full(T, b, d), D.full(T, a, d), True{}, 148 Equal.cong(Array, Bool, x => D.full(T, x, d), b, a, q), hf)) 149 150 def swap_full.go(-T: Type, -a: Array, +d: Nat, +i: U32, v: T, hf: {D.full(T, a, d) == True{} : Bool}, 151 w: SizeW(T, a)) -> {D.full(T, Pair.fst(Array, T, Array.swap(T, a, i, v)), d) == True{} : Bool}: 152 (b, +n, e, q) = w 153 %Equal.sym(Array & U32, Array.size(T, a), (b, n), e) : 154 {D.full(T, Pair.fst(Array, T, Array.swap.at(T, i, v, _)), d) == True{} : Bool} 155 +j = U32.and(i, U32.sub(n, 1)) 156 swap_full.fin(T, a, b, n, i, v, d, hf, q, swap_w(T, b, n, j, v, U32.is_lt(j, U32.shr(n)), d)) 157 158 law swap_full: 159 for -T: Type 160 for a: Array 161 for +d: Nat 162 for +i: U32 163 for v: T 164 for hf: {D.full(T, a, d) == True{} : Bool} 165 {D.full(T, Pair.fst(Array, T, Array.swap(T, a, i, v)), d) == True{} : Bool} 166 167 def swap_full(T, a, d, i, v, hf): 168 swap_full.go(T, a, d, i, v, hf, size_w(T, a)) 169 170 def set_full.fin(-T: Type, -a: Array, -b: Array, +n: U32, +i: U32, -v: T, +d: Nat, 171 hf: {D.full(T, a, d) == True{} : Bool}, q: {b == a : Array}, 172 w: SwapW(T, b, n, U32.and(i, U32.sub(n, 1)), v, U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)), d)) -> 173 {D.full(T, Array.set.fin(T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v, 174 U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)))), d) == True{} : Bool}: 175 (na, old, e, f) = w 176 %Equal.sym(Array & T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v, 177 U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n))), (na, old), e) : 178 {D.full(T, Array.set.fin(T, _), d) == True{} : Bool} 179 Equal.trans(Bool, D.full(T, na, d), D.full(T, b, d), True{}, f, 180 Equal.trans(Bool, D.full(T, b, d), D.full(T, a, d), True{}, 181 Equal.cong(Array, Bool, x => D.full(T, x, d), b, a, q), hf)) 182 183 def set_full.go(-T: Type, -a: Array, +d: Nat, +i: U32, v: T, hf: {D.full(T, a, d) == True{} : Bool}, 184 w: SizeW(T, a)) -> {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}: 185 (b, +n, e, q) = w 186 %Equal.sym(Array & U32, Array.size(T, a), (b, n), e) : 187 {D.full(T, Array.set.fin(T, Array.swap.at(T, i, v, _)), d) == True{} : Bool} 188 +j = U32.and(i, U32.sub(n, 1)) 189 set_full.fin(T, a, b, n, i, v, d, hf, q, swap_w(T, b, n, j, v, U32.is_lt(j, U32.shr(n)), d)) 190 191 law set_full: 192 for -T: Type 193 for a: Array 194 for +d: Nat 195 for +i: U32 196 for v: T 197 for hf: {D.full(T, a, d) == True{} : Bool} 198 {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool} 199 200 def set_full(T, a, d, i, v, hf): 201 set_full.go(T, a, d, i, v, hf, size_w(T, a))