def get_set_other

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

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/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

342def get_set_other(-T: Data, +d: Nat, +t: Tree<T>, +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> & T}:
343  +t2 = upd(T, d, t, U32.to_nat(i), v)
344  %Equal.sym(Array<T>, 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> & 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))