1 import Base 2 import ./logic.bend as L 3 import ./nat.bend as N 4 import ./u32.bend as U 5 import ./list.bend as LL 6 import ../../spec/lib/common.bend as SC 7 import ./lemmas/proofs/nat_algebra.bend as NA 8 9 # Functional correctness of the installed Base.Array get/swap/set/new 10 # algorithms (base.bend 2142-2272), proved against their actual definitions. 11 # 12 # Arrays are linear, so every statement is about thaw(t): the array built from a 13 # Data mirror tree t of identical shape. This keeps arrays out of live proof 14 # terms. The meaning of a tree is its in-order slot list; indices are U32 below 15 # the Base size 2^d (d < 32), so Base index masking is the identity. 16 17 type Tree<-T: Data> is Data: 18 TLeaf{value: T} 19 TNode{lo: Tree, hi: Tree} 20 21 def thaw(-T: Data, t: Tree) -> Array: 22 match t: 23 case TLeaf{x}: 24 ALeaf{x} 25 case TNode{l, r}: 26 ANode{thaw(T, l), thaw(T, r)} 27 28 def freeze(-T: Data, a: Array) -> Tree: 29 match a: 30 case ALeaf{+x}: 31 TLeaf{x} 32 case ANode{xs, ys}: 33 TNode{freeze(T, xs), freeze(T, ys)} 34 35 def slots(-T: Data, t: Tree) -> List<&2, T>: 36 match t: 37 case TLeaf{x}: 38 Con{x, Nil{}} 39 case TNode{l, r}: 40 SC.append(T, slots(T, l), slots(T, r)) 41 42 def perfect(-T: Data, +d: Nat, t: Tree) -> Bool: 43 match d t: 44 case 0n TLeaf{x}: 45 True{} 46 case 0n TNode{l, r}: 47 False{} 48 case 1n+p TLeaf{x}: 49 False{} 50 case 1n+p TNode{l, r}: 51 Bool.and(perfect(T, p, l), perfect(T, p, r)) 52 53 # Mirror of an update at a Nat index (proof-level description of the new tree). 54 # `left` is this node's branch decision (see ndec); passing it as a parameter 55 # avoids matching on a computed value. 56 def ndec(d: Nat, +j: Nat) -> Bool: 57 match d: 58 case 0n: 59 False{} 60 case 1n+q: 61 Nat.is_lt(j, SC.pow2(q)) 62 63 def tupd(-T: Data, d: Nat, t: Tree, +j: Nat, +v: T, left: Bool) -> Tree: 64 match d t left: 65 case 0n TLeaf{x} _: 66 TLeaf{v} 67 case 0n TNode{l, r} _: 68 TNode{l, r} 69 case 1n+p TLeaf{x} _: 70 TLeaf{x} 71 case 1n+ +p TNode{l, r} True{}: 72 TNode{tupd(T, p, l, j, v, ndec(p, j)), r} 73 case 1n+ +p TNode{l, r} False{}: 74 TNode{l, tupd(T, p, r, Nat.sub(j, SC.pow2(p)), v, ndec(p, Nat.sub(j, SC.pow2(p))))} 75 76 def upd(-T: Data, +d: Nat, t: Tree, +j: Nat, +v: T) -> Tree: 77 tupd(T, d, t, j, v, ndec(d, j)) 78 79 def trep(-T: Data, +d: Nat, +v: T) -> Tree: 80 match d: 81 case 0n: 82 TLeaf{v} 83 case 1n+p: 84 TNode{trep(T, p, v), trep(T, p, v)} 85 86 # ---- pure tree facts ---- 87 88 def freeze_thaw(-T: Data, +t: Tree) -> {freeze(T, thaw(T, t)) == t : Tree}: 89 match t: 90 case TLeaf{x}: 91 {==} 92 case TNode{+l, +r}: 93 %Equal.sym(Tree, freeze(T, thaw(T, l)), l, freeze_thaw(T, l)) : {TNode{_, freeze(T, thaw(T, r))} == TNode{l, r} : Tree} 94 %Equal.sym(Tree, freeze(T, thaw(T, r)), r, freeze_thaw(T, r)) : {TNode{l, _} == TNode{l, r} : Tree} 95 {==} 96 97 def pf_left(-T: Data, +p: Nat, +l: Tree, +r: Tree, +pf: {perfect(T, 1n+p, TNode{l, r}) == True{} : Bool}) -> {perfect(T, p, l) == True{} : Bool}: 98 L.and_left(perfect(T, p, l), perfect(T, p, r), pf) 99 100 def pf_right(-T: Data, +p: Nat, +l: Tree, +r: Tree, +pf: {perfect(T, 1n+p, TNode{l, r}) == True{} : Bool}) -> {perfect(T, p, r) == True{} : Bool}: 101 L.and_right(perfect(T, p, l), perfect(T, p, r), pf) 102 103 def slots_length(-T: Data, +d: Nat, +t: Tree, +pf: {perfect(T, d, t) == True{} : Bool}) -> {SC.length(T, slots(T, t)) == SC.pow2(d) : Nat}: 104 match d t: 105 case 0n TLeaf{x}: 106 {==} 107 case 0n TNode{l, r}: 108 Empty.absurd({SC.length(T, slots(T, TNode{l, r})) == 1n : Nat}, L.false_true(pf)) 109 case 1n+p TLeaf{x}: 110 Empty.absurd({1n == Nat.double(SC.pow2(p)) : Nat}, L.false_true(pf)) 111 case 1n+ +p TNode{+l, +r}: 112 %Equal.sym(Nat, SC.length(T, SC.append(T, slots(T, l), slots(T, r))), Nat.add(SC.length(T, slots(T, l)), SC.length(T, slots(T, r))), LL.length_append(T, slots(T, l), slots(T, r))) : {_ == Nat.double(SC.pow2(p)) : Nat} 113 %Equal.sym(Nat, SC.length(T, slots(T, l)), SC.pow2(p), slots_length(T, p, l, pf_left(T, p, l, r, pf))) : {Nat.add(_, SC.length(T, slots(T, r))) == Nat.double(SC.pow2(p)) : Nat} 114 %Equal.sym(Nat, SC.length(T, slots(T, r)), SC.pow2(p), slots_length(T, p, r, pf_right(T, p, l, r, pf))) : {Nat.add(SC.pow2(p), _) == Nat.double(SC.pow2(p)) : Nat} 115 Equal.sym(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p))) 116 117 def trep_perfect(-T: Data, +d: Nat, +v: T) -> {perfect(T, d, trep(T, d, v)) == True{} : Bool}: 118 match d: 119 case 0n: 120 {==} 121 case 1n+p: 122 L.and_intro(perfect(T, p, trep(T, p, v)), perfect(T, p, trep(T, p, v)), trep_perfect(T, p, v), trep_perfect(T, p, v)) 123 124 def trep_slots(-T: Data, +d: Nat, +v: T) -> {slots(T, trep(T, d, v)) == SC.replicate(T, SC.pow2(d), v) : List<&2, T>}: 125 match d: 126 case 0n: 127 {==} 128 case 1n+p: 129 %Equal.sym(List<&2, T>, slots(T, trep(T, p, v)), SC.replicate(T, SC.pow2(p), v), trep_slots(T, p, v)) : {SC.append(T, _, _) == SC.replicate(T, Nat.double(SC.pow2(p)), v) : List<&2, T>} 130 %Equal.sym(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p))) : {SC.append(T, SC.replicate(T, SC.pow2(p), v), SC.replicate(T, SC.pow2(p), v)) == SC.replicate(T, _, v) : List<&2, T>} 131 LL.replicate_add(T, SC.pow2(p), SC.pow2(p), v) 132 133 # ---- index helpers ---- 134 135 def leaf_update(-T: Data, +x: T, +v: T, +j: Nat, +hj: {Nat.is_lt(j, 1n) == True{} : Bool}) -> {Con{v, Nil{}} == SC.update(T, Con{x, Nil{}}, j, v) : List<&2, T>}: 136 match j: 137 case 0n: 138 {==} 139 case 1n+q: 140 Empty.absurd({Con{v, Nil{}} == Con{x, Nil{}} : List<&2, T>}, N.lt_zero_absurd(q, hj)) 141 142 def leaf_value(-T: Data, +y: T, +j: Nat, +x: T, +hj: {Nat.is_lt(j, 1n) == True{} : Bool}, +hx: {SC.nth(T, Con{y, Nil{}}, j) == Some{x} : Maybe<&2, T>}) -> {y == x : T}: 143 match j: 144 case 0n: 145 L.some_inj(T, y, x, hx) 146 case 1n+q: 147 Empty.absurd({y == x : T}, N.lt_zero_absurd(q, hj)) 148 149 def len_lt(-T: Data, +p: Nat, +l: Tree, +j: Nat, +pl: {perfect(T, p, l) == True{} : Bool}, +h: {Nat.is_lt(j, SC.pow2(p)) == True{} : Bool}) -> {Nat.is_lt(j, SC.length(T, slots(T, l))) == True{} : Bool}: 150 %Equal.sym(Nat, SC.length(T, slots(T, l)), SC.pow2(p), slots_length(T, p, l, pl)) : {Nat.is_lt(j, _) == True{} : Bool} 151 h 152 153 def len_le(-T: Data, +p: Nat, +l: Tree, +j: Nat, +pl: {perfect(T, p, l) == True{} : Bool}, +h: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {Nat.is_le(SC.length(T, slots(T, l)), j) == True{} : Bool}: 154 %Equal.sym(Nat, SC.length(T, slots(T, l)), SC.pow2(p), slots_length(T, p, l, pl)) : {Nat.is_le(_, j) == True{} : Bool} 155 h 156 157 def upper_lt(+j: Nat, +p: Nat, +hj: {Nat.is_lt(j, SC.pow2(1n+p)) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(j, SC.pow2(p)), SC.pow2(p)) == True{} : Bool}: 158 N.sub_lt(j, SC.pow2(p), SC.pow2(p), le, L.subst(Nat, n => {Nat.is_lt(j, n) == True{} : Bool}, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p)), hj)) 159 160 def right_update(-T: Data, +p: Nat, +l: Tree, +r: Tree, +j: Nat, +v: T, +pl: {perfect(T, p, l) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v) == SC.append(T, slots(T, l), SC.update(T, slots(T, r), Nat.sub(j, SC.pow2(p)), v)) : List<&2, T>}: 161 %slots_length(T, p, l, pl) : {SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v) == SC.append(T, slots(T, l), SC.update(T, slots(T, r), Nat.sub(j, _), v)) : List<&2, T>} 162 LL.update_append_right(T, slots(T, l), slots(T, r), j, v, len_le(T, p, l, j, pl, le)) 163 164 def right_nth(-T: Data, +p: Nat, +l: Tree, +r: Tree, +j: Nat, +pl: {perfect(T, p, l) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j) == SC.nth(T, slots(T, r), Nat.sub(j, SC.pow2(p))) : Maybe<&2, T>}: 165 %slots_length(T, p, l, pl) : {SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j) == SC.nth(T, slots(T, r), Nat.sub(j, _)) : Maybe<&2, T>} 166 LL.nth_append_right(T, slots(T, l), slots(T, r), j, len_le(T, p, l, j, pl, le)) 167 168 # ---- the Nat mirror of an update ---- 169 170 def tupd_perfect(-T: Data, +d: Nat, +t: Tree, +j: Nat, +v: T, +b: Bool, +pf: {perfect(T, d, t) == True{} : Bool}) -> {perfect(T, d, tupd(T, d, t, j, v, b)) == True{} : Bool}: 171 match d t b: 172 case 0n TLeaf{x} _: 173 {==} 174 case 0n TNode{l, r} _: 175 pf 176 case 1n+p TLeaf{x} _: 177 pf 178 case 1n+ +p TNode{+l, +r} True{}: 179 L.and_intro(perfect(T, p, tupd(T, p, l, j, v, ndec(p, j))), perfect(T, p, r), tupd_perfect(T, p, l, j, v, ndec(p, j), pf_left(T, p, l, r, pf)), pf_right(T, p, l, r, pf)) 180 case 1n+ +p TNode{+l, +r} False{}: 181 L.and_intro(perfect(T, p, l), perfect(T, p, tupd(T, p, r, Nat.sub(j, SC.pow2(p)), v, ndec(p, Nat.sub(j, SC.pow2(p))))), pf_left(T, p, l, r, pf), tupd_perfect(T, p, r, Nat.sub(j, SC.pow2(p)), v, ndec(p, Nat.sub(j, SC.pow2(p))), pf_right(T, p, l, r, pf))) 182 183 def tupd_slots(-T: Data, +d: Nat, +t: Tree, +j: Nat, +v: T, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +b: Bool, +eb: {ndec(d, j) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {slots(T, tupd(T, d, t, j, v, b)) == SC.update(T, slots(T, t), j, v) : List<&2, T>}: 184 match d t b: 185 case 0n TLeaf{x} _: 186 leaf_update(T, x, v, j, hj) 187 case 0n TNode{l, r} _: 188 Empty.absurd({slots(T, TNode{l, r}) == SC.update(T, slots(T, TNode{l, r}), j, v) : List<&2, T>}, L.false_true(pf)) 189 case 1n+p TLeaf{x} _: 190 Empty.absurd({Con{x, Nil{}} == SC.update(T, Con{x, Nil{}}, j, v) : List<&2, T>}, L.false_true(pf)) 191 case 1n+ +p TNode{+l, +r} True{}: 192 Equal.trans(List<&2, T>, SC.append(T, slots(T, tupd(T, p, l, j, v, ndec(p, j))), slots(T, r)), SC.append(T, SC.update(T, slots(T, l), j, v), slots(T, r)), SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), 193 Equal.cong(List<&2, T>, List<&2, T>, xs => SC.append(T, xs, slots(T, r)), slots(T, tupd(T, p, l, j, v, ndec(p, j))), SC.update(T, slots(T, l), j, v), tupd_slots(T, p, l, j, v, eb, ndec(p, j), {==}, pf_left(T, p, l, r, pf))), 194 Equal.sym(List<&2, T>, SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), SC.append(T, SC.update(T, slots(T, l), j, v), slots(T, r)), LL.update_append_left(T, slots(T, l), slots(T, r), j, v, len_lt(T, p, l, j, pf_left(T, p, l, r, pf), eb)))) 195 case 1n+ +p TNode{+l, +r} False{}: 196 +k = Nat.sub(j, SC.pow2(p)) 197 +le = N.not_lt_le(j, SC.pow2(p), eb) 198 Equal.trans(List<&2, T>, SC.append(T, slots(T, l), slots(T, tupd(T, p, r, k, v, ndec(p, k)))), SC.append(T, slots(T, l), SC.update(T, slots(T, r), k, v)), SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), 199 Equal.cong(List<&2, T>, List<&2, T>, xs => SC.append(T, slots(T, l), xs), slots(T, tupd(T, p, r, k, v, ndec(p, k))), SC.update(T, slots(T, r), k, v), tupd_slots(T, p, r, k, v, upper_lt(j, p, hj, le), ndec(p, k), {==}, pf_right(T, p, l, r, pf))), 200 Equal.sym(List<&2, T>, SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), SC.append(T, slots(T, l), SC.update(T, slots(T, r), k, v)), right_update(T, p, l, r, j, v, pf_left(T, p, l, r, pf), le))) 201 202 def upd_perfect(-T: Data, +d: Nat, +t: Tree, +j: Nat, +v: T, +pf: {perfect(T, d, t) == True{} : Bool}) -> {perfect(T, d, upd(T, d, t, j, v)) == True{} : Bool}: 203 tupd_perfect(T, d, t, j, v, ndec(d, j), pf) 204 205 def upd_slots(-T: Data, +d: Nat, +t: Tree, +j: Nat, +v: T, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {slots(T, upd(T, d, t, j, v)) == SC.update(T, slots(T, t), j, v) : List<&2, T>}: 206 tupd_slots(T, d, t, j, v, hj, ndec(d, j), {==}, pf) 207 208 # ---- U32 index bridges ---- 209 210 def lt_bridge(+i: U32, +p: Nat, +hp: {Nat.is_lt(p, 32n) == True{} : Bool}, +b: Bool, +eb: {U32.is_lt(i, U.pow2u(p)) == b : Bool}) -> {Nat.is_lt(U32.to_nat(i), SC.pow2(p)) == b : Bool}: 211 Equal.trans(Bool, Nat.is_lt(U32.to_nat(i), SC.pow2(p)), Nat.is_lt(U32.to_nat(i), U32.to_nat(U.pow2u(p))), b, 212 Equal.cong(Nat, Bool, n => Nat.is_lt(U32.to_nat(i), n), SC.pow2(p), U32.to_nat(U.pow2u(p)), Equal.sym(Nat, U32.to_nat(U.pow2u(p)), SC.pow2(p), U.pow2u_value(p, hp))), 213 Equal.trans(Bool, Nat.is_lt(U32.to_nat(i), U32.to_nat(U.pow2u(p))), U32.is_lt(i, U.pow2u(p)), b, Equal.sym(Bool, U32.is_lt(i, U.pow2u(p)), Nat.is_lt(U32.to_nat(i), U32.to_nat(U.pow2u(p))), U.is_lt_nat(i, U.pow2u(p))), eb)) 214 215 def sub_bridge(+i: U32, +p: Nat, +hp: {Nat.is_lt(p, 32n) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), U32.to_nat(i)) == True{} : Bool}) -> {U32.to_nat(U32.sub(i, U.pow2u(p))) == Nat.sub(U32.to_nat(i), SC.pow2(p)) : Nat}: 216 Equal.trans(Nat, U32.to_nat(U32.sub(i, U.pow2u(p))), Nat.sub(U32.to_nat(i), U32.to_nat(U.pow2u(p))), Nat.sub(U32.to_nat(i), SC.pow2(p)), 217 U.sub_nat(i, U.pow2u(p), L.subst(Nat, n => {Nat.is_le(n, U32.to_nat(i)) == True{} : Bool}, SC.pow2(p), U32.to_nat(U.pow2u(p)), Equal.sym(Nat, U32.to_nat(U.pow2u(p)), SC.pow2(p), U.pow2u_value(p, hp)), le)), 218 Equal.cong(Nat, Nat, n => Nat.sub(U32.to_nat(i), n), U32.to_nat(U.pow2u(p)), SC.pow2(p), U.pow2u_value(p, hp))) 219 220 # ---- Base.Array.size / get / swap / set / new ---- 221 222 def size_thaw(-T: Data, +d: Nat, +t: Tree, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.size(T, thaw(T, t)) == (thaw(T, t), U.pow2u(d)) : Array & U32}: 223 match d t: 224 case 0n TLeaf{x}: 225 {==} 226 case 0n TNode{l, r}: 227 Empty.absurd({Array.size(T, thaw(T, TNode{l, r})) == (thaw(T, TNode{l, r}), 1) : Array & U32}, L.false_true(pf)) 228 case 1n+p TLeaf{x}: 229 Empty.absurd({Array.size(T, ALeaf{x}) == (ALeaf{x}, U.pow2u(1n+p)) : Array & U32}, L.false_true(pf)) 230 case 1n+ +p TNode{+l, +r}: 231 %Equal.sym(Array & U32, Array.size(T, thaw(T, l)), (thaw(T, l), U.pow2u(p)), size_thaw(T, p, l, pf_left(T, p, l, r, pf))) : {Array.size.node(T, thaw(T, r), _) == (ANode{thaw(T, l), thaw(T, r)}, U32.shl(U.pow2u(p))) : Array & U32} 232 {==} 233 234 # Base 2.0.32 passes each descent step its branch decision z; eb names it as 235 # U32.is_lt(i, U32.shr(2^d)), the value Base computes, so callers pass {==}. 236 def get_go(-T: Data, +d: Nat, +t: Tree, +i: U32, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +b: Bool, +eb: {U32.is_lt(i, U32.shr(U.pow2u(d))) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get.go(T, thaw(T, t), U.pow2u(d), i, b) == (thaw(T, t), x) : Array & T}: 237 match d t b: 238 case 0n TLeaf{+y} _: 239 %leaf_value(T, y, U32.to_nat(i), x, hi, hx) : {(ALeaf{y}, y) == (ALeaf{y}, _) : Array & T} 240 {==} 241 case 0n TNode{l, r} _: 242 Empty.absurd({Array.get.go(T, thaw(T, TNode{l, r}), 1, i, b) == (thaw(T, TNode{l, r}), x) : Array & T}, L.false_true(pf)) 243 case 1n+p TLeaf{y} _: 244 Empty.absurd({Array.get.go(T, ALeaf{y}, U.pow2u(1n+p), i, b) == (ALeaf{y}, x) : Array & T}, L.false_true(pf)) 245 case 1n+ +p TNode{+l, +r} True{}: 246 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd) 247 +pl = pf_left(T, p, l, r, pf) 248 +hil = lt_bridge(i, p, hp, True{}, L.subst(U32, w => {U32.is_lt(i, w) == True{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb)) 249 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.lo(T, thaw(T, r), Array.get.go(T, thaw(T, l), _, i, U32.is_lt(i, U32.shr(_)))) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array & T} 250 %Equal.sym(Array & T, Array.get.go(T, thaw(T, l), U.pow2u(p), i, U32.is_lt(i, U32.shr(U.pow2u(p)))), (thaw(T, l), x), get_go(T, p, l, i, x, hp, hil, Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, l), U32.to_nat(i)), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), SC.nth(T, slots(T, l), U32.to_nat(i)), LL.nth_append_left(T, slots(T, l), slots(T, r), U32.to_nat(i), len_lt(T, p, l, U32.to_nat(i), pl, hil))), hx), U32.is_lt(i, U32.shr(U.pow2u(p))), {==}, pl)) : {Array.swap.lo(T, thaw(T, r), _) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array & T} 251 {==} 252 case 1n+ +p TNode{+l, +r} False{}: 253 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd) 254 +pl = pf_left(T, p, l, r, pf) 255 +le = N.not_lt_le(U32.to_nat(i), SC.pow2(p), lt_bridge(i, p, hp, False{}, L.subst(U32, w => {U32.is_lt(i, w) == False{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb))) 256 +j = U32.sub(i, U.pow2u(p)) 257 +ej = sub_bridge(i, p, hp, le) 258 +hir = L.subst(Nat, n => {Nat.is_lt(n, SC.pow2(p)) == True{} : Bool}, Nat.sub(U32.to_nat(i), SC.pow2(p)), U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), Nat.sub(U32.to_nat(i), SC.pow2(p)), ej), upper_lt(U32.to_nat(i), p, hi, le)) 259 +hxr = L.subst(Nat, n => {SC.nth(T, slots(T, r), n) == Some{x} : Maybe<&2, T>}, Nat.sub(U32.to_nat(i), SC.pow2(p)), U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), Nat.sub(U32.to_nat(i), SC.pow2(p)), ej), Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, r), Nat.sub(U32.to_nat(i), SC.pow2(p))), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), SC.nth(T, slots(T, r), Nat.sub(U32.to_nat(i), SC.pow2(p))), right_nth(T, p, l, r, U32.to_nat(i), pl, le)), hx)) 260 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.hi(T, thaw(T, l), Array.get.go(T, thaw(T, r), _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_)))) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array & T} 261 %Equal.sym(Array & T, Array.get.go(T, thaw(T, r), U.pow2u(p), j, U32.is_lt(j, U32.shr(U.pow2u(p)))), (thaw(T, r), x), get_go(T, p, r, j, x, hp, hir, hxr, U32.is_lt(j, U32.shr(U.pow2u(p))), {==}, pf_right(T, p, l, r, pf))) : {Array.swap.hi(T, thaw(T, l), _) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array & T} 262 {==} 263 264 def swap_go(-T: Data, +d: Nat, +t: Tree, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +b: Bool, +eb: {U32.is_lt(i, U32.shr(U.pow2u(d))) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.swap.go(T, thaw(T, t), U.pow2u(d), i, v, b) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array & T}: 265 match d t b: 266 case 0n TLeaf{+y} _: 267 %leaf_value(T, y, U32.to_nat(i), x, hi, hx) : {(ALeaf{v}, y) == (ALeaf{v}, _) : Array & T} 268 {==} 269 case 0n TNode{l, r} _: 270 Empty.absurd({Array.swap.go(T, thaw(T, TNode{l, r}), 1, i, v, b) == (thaw(T, upd(T, 0n, TNode{l, r}, U32.to_nat(i), v)), x) : Array & T}, L.false_true(pf)) 271 case 1n+p TLeaf{y} _: 272 Empty.absurd({Array.swap.go(T, ALeaf{y}, U.pow2u(1n+p), i, v, b) == (thaw(T, upd(T, 1n+p, TLeaf{y}, U32.to_nat(i), v)), x) : Array & T}, L.false_true(pf)) 273 case 1n+ +p TNode{+l, +r} True{}: 274 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd) 275 +pl = pf_left(T, p, l, r, pf) 276 +hil = lt_bridge(i, p, hp, True{}, L.subst(U32, w => {U32.is_lt(i, w) == True{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb)) 277 +ti = U32.to_nat(i) 278 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.lo(T, thaw(T, r), Array.swap.go(T, thaw(T, l), _, i, v, U32.is_lt(i, U32.shr(_)))) == (thaw(T, upd(T, 1n+p, TNode{l, r}, ti, v)), x) : Array & T} 279 %Equal.sym(Bool, Nat.is_lt(ti, SC.pow2(p)), True{}, hil) : {Array.swap.lo(T, thaw(T, r), Array.swap.go(T, thaw(T, l), U.pow2u(p), i, v, U32.is_lt(i, U32.shr(U.pow2u(p))))) == (thaw(T, tupd(T, 1n+p, TNode{l, r}, ti, v, _)), x) : Array & T} 280 %Equal.sym(Array & T, Array.swap.go(T, thaw(T, l), U.pow2u(p), i, v, U32.is_lt(i, U32.shr(U.pow2u(p)))), (thaw(T, upd(T, p, l, ti, v)), x), swap_go(T, p, l, i, v, x, hp, hil, Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, l), ti), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), SC.nth(T, slots(T, l), ti), LL.nth_append_left(T, slots(T, l), slots(T, r), ti, len_lt(T, p, l, ti, pl, hil))), hx), U32.is_lt(i, U32.shr(U.pow2u(p))), {==}, pl)) : {Array.swap.lo(T, thaw(T, r), _) == (thaw(T, TNode{tupd(T, p, l, ti, v, ndec(p, ti)), r}), x) : Array & T} 281 {==} 282 case 1n+ +p TNode{+l, +r} False{}: 283 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd) 284 +pl = pf_left(T, p, l, r, pf) 285 +ti = U32.to_nat(i) 286 +nb = lt_bridge(i, p, hp, False{}, L.subst(U32, w => {U32.is_lt(i, w) == False{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb)) 287 +le = N.not_lt_le(ti, SC.pow2(p), nb) 288 +j = U32.sub(i, U.pow2u(p)) 289 +k = Nat.sub(ti, SC.pow2(p)) 290 +ej = sub_bridge(i, p, hp, le) 291 +hir = L.subst(Nat, n => {Nat.is_lt(n, SC.pow2(p)) == True{} : Bool}, k, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), k, ej), upper_lt(ti, p, hi, le)) 292 +hxr = L.subst(Nat, n => {SC.nth(T, slots(T, r), n) == Some{x} : Maybe<&2, T>}, k, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), k, ej), Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, r), k), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), SC.nth(T, slots(T, r), k), right_nth(T, p, l, r, ti, pl, le)), hx)) 293 +ih = swap_go(T, p, r, j, v, x, hp, hir, hxr, U32.is_lt(j, U32.shr(U.pow2u(p))), {==}, pf_right(T, p, l, r, pf)) 294 +ih2 = L.subst(Nat, n => {Array.swap.go(T, thaw(T, r), U.pow2u(p), j, v, U32.is_lt(j, U32.shr(U.pow2u(p)))) == (thaw(T, upd(T, p, r, n, v)), x) : Array & T}, U32.to_nat(j), k, ej, ih) 295 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.hi(T, thaw(T, l), Array.swap.go(T, thaw(T, r), _, U32.sub(i, _), v, U32.is_lt(U32.sub(i, _), U32.shr(_)))) == (thaw(T, upd(T, 1n+p, TNode{l, r}, ti, v)), x) : Array & T} 296 %Equal.sym(Bool, Nat.is_lt(ti, SC.pow2(p)), False{}, nb) : {Array.swap.hi(T, thaw(T, l), Array.swap.go(T, thaw(T, r), U.pow2u(p), j, v, U32.is_lt(j, U32.shr(U.pow2u(p))))) == (thaw(T, tupd(T, 1n+p, TNode{l, r}, ti, v, _)), x) : Array & T} 297 %Equal.sym(Array & T, Array.swap.go(T, thaw(T, r), U.pow2u(p), j, v, U32.is_lt(j, U32.shr(U.pow2u(p)))), (thaw(T, upd(T, p, r, k, v)), x), ih2) : {Array.swap.hi(T, thaw(T, l), _) == (thaw(T, TNode{l, tupd(T, p, r, k, v, ndec(p, k))}), x) : Array & T} 298 {==} 299 300 # Public Base entry points. Premises: the tree is perfect of depth d < 32 and 301 # the index is below 2^d; x is the value currently stored at that index. 302 def get(-T: Data, +d: Nat, +t: Tree, +i: U32, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get(T, thaw(T, t), i) == (thaw(T, t), x) : Array & T}: 303 %Equal.sym(Array & U32, Array.size(T, thaw(T, t)), (thaw(T, t), U.pow2u(d)), size_thaw(T, d, t, pf)) : {Array.get.at(T, i, _) == (thaw(T, t), x) : Array & T} 304 %Equal.sym(U32, U32.and(i, U32.sub(U.pow2u(d), 1)), i, U.mask_pow2u(i, d, hd, hi)) : {Array.get.go(T, thaw(T, t), U.pow2u(d), _, U32.is_lt(_, U32.shr(U.pow2u(d)))) == (thaw(T, t), x) : Array & T} 305 get_go(T, d, t, i, x, hd, hi, hx, U32.is_lt(i, U32.shr(U.pow2u(d))), {==}, pf) 306 307 def swap(-T: Data, +d: Nat, +t: Tree, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.swap(T, thaw(T, t), i, v) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array & T}: 308 %Equal.sym(Array & U32, Array.size(T, thaw(T, t)), (thaw(T, t), U.pow2u(d)), size_thaw(T, d, t, pf)) : {Array.swap.at(T, i, v, _) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array & T} 309 %Equal.sym(U32, U32.and(i, U32.sub(U.pow2u(d), 1)), i, U.mask_pow2u(i, d, hd, hi)) : {Array.swap.go(T, thaw(T, t), U.pow2u(d), _, v, U32.is_lt(_, U32.shr(U.pow2u(d)))) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array & T} 310 swap_go(T, d, t, i, v, x, hd, hi, hx, U32.is_lt(i, U32.shr(U.pow2u(d))), {==}, pf) 311 312 def set(-T: Data, +d: Nat, +t: Tree, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.set(T, thaw(T, t), i, v) == thaw(T, upd(T, d, t, U32.to_nat(i), v)) : Array}: 313 %Equal.sym(Array & T, Array.swap(T, thaw(T, t), i, v), (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x), swap(T, d, t, i, v, x, hd, hi, hx, pf)) : {Array.set.fin(T, _) == thaw(T, upd(T, d, t, U32.to_nat(i), v)) : Array} 314 {==} 315 316 def new(-T: Data, +d: Nat, +v: T) -> {Array.new(T, d, v) == thaw(T, trep(T, d, v)) : Array}: 317 match d: 318 case 0n: 319 {==} 320 case 1n+p: 321 %Equal.sym(Array, Array.new(T, p, v), thaw(T, trep(T, p, v)), new(T, p, v)) : {ANode{_, _} == ANode{thaw(T, trep(T, p, v)), thaw(T, trep(T, p, v))} : Array} 322 {==} 323 324 def clone(-T: Data, +t: Tree) -> {Array.clone(T, thaw(T, t)) == (thaw(T, t), thaw(T, t)) : Array & Array}: 325 match t: 326 case TLeaf{x}: 327 {==} 328 case TNode{+l, +r}: 329 %Equal.sym(Array & Array, Array.clone(T, thaw(T, l)), (thaw(T, l), thaw(T, l)), clone(T, l)) : {Array.clone.node(T, _, Array.clone(T, thaw(T, r))) == (ANode{thaw(T, l), thaw(T, r)}, ANode{thaw(T, l), thaw(T, r)}) : Array & Array} 330 %Equal.sym(Array & Array, Array.clone(T, thaw(T, r)), (thaw(T, r), thaw(T, r)), clone(T, r)) : {Array.clone.node(T, (thaw(T, l), thaw(T, l)), _) == (ANode{thaw(T, l), thaw(T, r)}, ANode{thaw(T, l), thaw(T, r)}) : Array & Array} 331 {==} 332 333 # ---- get after set (Base.Array.set then Base.Array.get) ---- 334 335 def get_set_same(-T: Data, +d: Nat, +t: Tree, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get(T, Array.set(T, thaw(T, t), i, v), i) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), v) : Array & T}: 336 +t2 = upd(T, d, t, U32.to_nat(i), v) 337 %Equal.sym(Array, Array.set(T, thaw(T, t), i, v), thaw(T, t2), set(T, d, t, i, v, x, hd, hi, hx, pf)) : {Array.get(T, _, i) == (thaw(T, t2), v) : Array & T} 338 get(T, d, t2, i, v, hd, hi, 339 L.subst(List<&2, T>, ys => {SC.nth(T, ys, U32.to_nat(i)) == Some{v} : Maybe<&2, T>}, SC.update(T, slots(T, t), U32.to_nat(i), v), slots(T, t2), Equal.sym(List<&2, T>, slots(T, t2), SC.update(T, slots(T, t), U32.to_nat(i), v), upd_slots(T, d, t, U32.to_nat(i), v, hi, pf)), LL.nth_update_same(T, slots(T, t), U32.to_nat(i), v, LL.nth_lt_length(T, slots(T, t), U32.to_nat(i), x, hx))), 340 upd_perfect(T, d, t, U32.to_nat(i), v, pf)) 341 342 def get_set_other(-T: Data, +d: Nat, +t: Tree, +i: U32, +j: U32, +v: T, +x: T, +y: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hj: {Nat.is_lt(U32.to_nat(j), SC.pow2(d)) == True{} : Bool}, +ne: {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == False{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +hy: {SC.nth(T, slots(T, t), U32.to_nat(j)) == Some{y} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get(T, Array.set(T, thaw(T, t), i, v), j) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), y) : Array & T}: 343 +t2 = upd(T, d, t, U32.to_nat(i), v) 344 %Equal.sym(Array, Array.set(T, thaw(T, t), i, v), thaw(T, t2), set(T, d, t, i, v, x, hd, hi, hx, pf)) : {Array.get(T, _, j) == (thaw(T, t2), y) : Array & T} 345 get(T, d, t2, j, y, hd, hj, 346 L.subst(List<&2, T>, ys => {SC.nth(T, ys, U32.to_nat(j)) == Some{y} : Maybe<&2, T>}, SC.update(T, slots(T, t), U32.to_nat(i), v), slots(T, t2), Equal.sym(List<&2, T>, slots(T, t2), SC.update(T, slots(T, t), U32.to_nat(i), v), upd_slots(T, d, t, U32.to_nat(i), v, hi, pf)), Equal.trans(Maybe<&2, T>, SC.nth(T, SC.update(T, slots(T, t), U32.to_nat(i), v), U32.to_nat(j)), SC.nth(T, slots(T, t), U32.to_nat(j)), Some{y}, LL.nth_update_other(T, slots(T, t), U32.to_nat(i), U32.to_nat(j), v, ne), hy)), 347 upd_perfect(T, d, t, U32.to_nat(i), v, pf))