def tupd_slots

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:183

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

183def tupd_slots(-T: Data, +d: Nat, +t: Tree<T>, +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)))