proofs/containers/dynamic_array/steps.bend source
proofs/containers/dynamic_array/steps.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/list.bend as LLimport ../../lib/u32.bend as Uimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/dynamic_array.bend as Simport ../../../src/containers/dynamic_array.bend as DAimport ../../../src/containers/types/dynamic_array.bend as Eimport ./layout.bend as LYimport ./state.bend as STimport ./growth.bend as GRimport ./walk.bend as W# One actual public operation on a good shadow's array yields the array of a# new good shadow, and (abstract state, observation) equals the spec step.def StepOK(-T: Data, sh: ST.Shadow<T>, op: E.Op<T>) -> Type: Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {DA.step(T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : DA.DynArray<&2, T> & E.Obs<T>} & ({ST.good(T, sh2) == True{} : Bool} & {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : S.Model<T> & E.Obs<T>})>>def length_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Length{}): +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) (ST.Sh{l, d, n, t}, (E.ONat{n}, ({==}, (g, %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, d, xs}, E.ONat{n}) == (S.M{l, d, xs}, E.ONat{_}) : S.Model<T> & E.Obs<T>} {==}))))def capacity_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Capacity{}): +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) (ST.Sh{l, d, n, t}, (E.ONat{SC.pow2(d)}, ({==}, (g, {==}))))# ---- facts shared by indexed operations ----def n_le_cap(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}: L.subst(Nat, k => {Nat.is_le(n, k) == True{} : Bool}, SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, T>, d, t, ST.g_perfect(T, l, d, n, t, g)), LY.lay_le(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g)))def idx_lt(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(U32.from_nat(i)), SC.pow2(d)) == True{} : Bool}: L.subst(Nat, k => {Nat.is_lt(k, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi)), hi)def idx_slot(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +x: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>}) -> {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), U32.to_nat(U32.from_nat(i))) == Some{x} : Maybe<&2, Maybe<&2, T>>}: L.subst(Nat, k => {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), k) == Some{x} : Maybe<&2, Maybe<&2, T>>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi)), hx)# ---- get ----def get_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Get{i}): match b: case True{}: +ss = AR.slots(Maybe<&2, T>, t) +xs = LY.somes(T, ss) +x = SC.nth(T, xs, i) +hi = N.lt_le_trans(i, n, SC.pow2(d), eb, n_le_cap(T, l, d, n, t, g)) (ST.Sh{l, d, n, t}, (E.OItem{S.item_result(T, x)}, ( %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {DA.obs_item(T, DA.get_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i)), (AR.thaw(Maybe<&2, T>, t), x), AR.get(Maybe<&2, T>, d, t, U32.from_nat(i), x, ST.lt32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), idx_lt(T, l, d, n, t, i, g, hi), idx_slot(T, l, d, n, t, i, x, g, hi, LY.lay_nth(T, ss, n, i, ST.g_lay(T, l, d, n, t, g), eb)), ST.g_perfect(T, l, d, n, t, g))) : {DA.obs_item(T, DA.get_found(T, l, d, SC.pow2(d), n, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Result<&2, &2, E.Error, T>, DA.slot_result(T, x), S.item_result(T, x), ST.slot_item(T, x)) : {(DA.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)}, E.OItem{_}) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, {==})))) case False{}: +ss = AR.slots(Maybe<&2, T>, t) +xs = LY.somes(T, ss) (ST.Sh{l, d, n, t}, (E.OItem{Fail{E.IndexOutOfRange{}}}, ( %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {DA.obs_item(T, DA.get_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OItem{Fail{E.IndexOutOfRange{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, %Equal.sym(Maybe<&2, T>, SC.nth(T, xs, i), None{}, LL.nth_none(T, xs, i, L.subst(Nat, k => {Nat.is_le(k, i) == True{} : Bool}, n, SC.length(T, xs), Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, ss, n, ST.g_lay(T, l, d, n, t, g))), N.not_lt_le(i, n, eb)))) : {(S.M{l, d, xs}, E.OItem{Fail{E.IndexOutOfRange{}}}) == (S.M{l, d, xs}, E.OItem{S.item_result(T, _)}) : S.Model<T> & E.Obs<T>} {==}))))def get_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Get{i}): get_case(T, l, d, n, t, i, g, Nat.is_lt(i, n), {==})# ---- writes through Base.Array.set / swap at a checked Nat index ----def set_arr(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +w: Maybe<&2, T>, +x: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>}) -> {Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, w)) : Array<Maybe<&2, T>>}: L.subst(Nat, k => {Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, k, w)) : Array<Maybe<&2, T>>}, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi), AR.set(Maybe<&2, T>, d, t, U32.from_nat(i), w, x, ST.lt32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), idx_lt(T, l, d, n, t, i, g, hi), idx_slot(T, l, d, n, t, i, x, g, hi, hx), ST.g_perfect(T, l, d, n, t, g)))def swap_arr(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +w: Maybe<&2, T>, +x: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i) == Some{x} : Maybe<&2, Maybe<&2, T>>}) -> {Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, w)), x) : Array<Maybe<&2, T>> & Maybe<&2, T>}: L.subst(Nat, k => {Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), w) == (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, k, w)), x) : Array<Maybe<&2, T>> & Maybe<&2, T>}, U32.to_nat(U32.from_nat(i)), i, U.to_nat_from_nat(i, d, ST.le32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), hi), AR.swap(Maybe<&2, T>, d, t, U32.from_nat(i), w, x, ST.lt32(d, l, ST.g_depth(T, l, d, n, t, g), ST.g_limit(T, l, d, n, t, g)), idx_lt(T, l, d, n, t, i, g, hi), idx_slot(T, l, d, n, t, i, x, g, hi, hx), ST.g_perfect(T, l, d, n, t, g)))# slots of an updated tree (index below the capacity).def upd_slots(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +w: Maybe<&2, T>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, w)) == SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i, w) : List<&2, Maybe<&2, T>>}: AR.upd_slots(Maybe<&2, T>, d, t, i, w, hi, ST.g_perfect(T, l, d, n, t, g))# ---- set ----def set_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Set{i, v}): match b: case True{}: +ss = AR.slots(Maybe<&2, T>, t) +xs = LY.somes(T, ss) +hi = N.lt_le_trans(i, n, SC.pow2(d), eb, n_le_cap(T, l, d, n, t, g)) +t2 = AR.upd(Maybe<&2, T>, d, t, i, Some{v}) +hs = upd_slots(T, l, d, n, t, i, Some{v}, g, hi) +hlay = ST.g_lay(T, l, d, n, t, g) +hlen = LY.lay_len(T, ss, n, hlay) (ST.Sh{l, d, n, t2}, (E.OUnit{Done{Unit{}}}, ( %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {DA.obs_unit(T, DA.set_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) == (ST.real(T, ST.Sh{l, d, n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), Some{v}), AR.thaw(Maybe<&2, T>, t2), set_arr(T, l, d, n, t, i, Some{v}, SC.nth(T, xs, i), g, hi, LY.lay_nth(T, ss, n, i, hlay, eb))) : {(DA.DA{l, d, SC.pow2(d), n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, d, n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (ST.good_intro(T, l, d, n, t2, ST.g_limit(T, l, d, n, t, g), ST.g_depth(T, l, d, n, t, g), AR.upd_perfect(Maybe<&2, T>, d, t, i, Some{v}, ST.g_perfect(T, l, d, n, t, g)), L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, n) == True{} : Bool}, SC.update(Maybe<&2, T>, ss, i, Some{v}), AR.slots(Maybe<&2, T>, t2), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, i, Some{v}), hs), LY.lay_set(T, ss, n, i, v, hlay, eb))), %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, i, Some{v}), hs) : {(S.M{l, d, LY.somes(T, _)}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Set{i, v}) : S.Model<T> & E.Obs<T>} %Equal.sym(List<&2, T>, LY.somes(T, SC.update(Maybe<&2, T>, ss, i, Some{v})), SC.update(T, xs, i, v), LY.somes_set(T, ss, n, i, v, hlay, eb)) : {(S.M{l, d, _}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Set{i, v}) : S.Model<T> & E.Obs<T>} %Equal.sym(Nat, SC.length(T, xs), n, hlen) : {(S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(i, _), (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {(S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>} {==})))) case False{}: +ss = AR.slots(Maybe<&2, T>, t) +xs = LY.somes(T, ss) +hlen = LY.lay_len(T, ss, n, ST.g_lay(T, l, d, n, t, g)) (ST.Sh{l, d, n, t}, (E.OUnit{Fail{E.IndexOutOfRange{}}}, ( %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {DA.obs_unit(T, DA.set_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.IndexOutOfRange{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, %Equal.sym(Nat, SC.length(T, xs), n, hlen) : {(S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(i, _), (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {(S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) : S.Model<T> & E.Obs<T>} {==}))))def set_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +i: Nat, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Set{i, v}): set_case(T, l, d, n, t, i, v, g, Nat.is_lt(i, n), {==})# ---- push ----def len_slots(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(n, SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t))) == True{} : Bool}: L.subst(Nat, k => {Nat.is_lt(n, k) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t)), Equal.sym(Nat, SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, T>, d, t, ST.g_perfect(T, l, d, n, t, g))), hn)def pi_arr(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(n), Some{v}) == AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v})) : Array<Maybe<&2, T>>}: set_arr(T, l, d, n, t, n, Some{v}, None{}, g, hn, LY.push_free(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g), len_slots(T, l, d, n, t, g, hn)))def pi_good(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {ST.good(T, ST.Sh{l, d, 1n+n, AR.upd(Maybe<&2, T>, d, t, n, Some{v})}) == True{} : Bool}: +ss = AR.slots(Maybe<&2, T>, t) +t2 = AR.upd(Maybe<&2, T>, d, t, n, Some{v}) ST.good_intro(T, l, d, 1n+n, t2, ST.g_limit(T, l, d, n, t, g), ST.g_depth(T, l, d, n, t, g), AR.upd_perfect(Maybe<&2, T>, d, t, n, Some{v}, ST.g_perfect(T, l, d, n, t, g)), L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, 1n+n) == True{} : Bool}, SC.update(Maybe<&2, T>, ss, n, Some{v}), AR.slots(Maybe<&2, T>, t2), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, n, Some{v}), upd_slots(T, l, d, n, t, n, Some{v}, g, hn)), LY.lay_push(T, ss, n, v, ST.g_lay(T, l, d, n, t, g), len_slots(T, l, d, n, t, g, hn))))def pi_model(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {LY.somes(T, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v}))) == SC.snoc(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), v) : List<&2, T>}: +ss = AR.slots(Maybe<&2, T>, t) Equal.trans(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v}))), LY.somes(T, SC.update(Maybe<&2, T>, ss, n, Some{v})), SC.snoc(T, LY.somes(T, ss), v), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, T>, ys => LY.somes(T, ys), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v})), SC.update(Maybe<&2, T>, ss, n, Some{v}), upd_slots(T, l, d, n, t, n, Some{v}, g, hn)), LY.somes_push(T, ss, n, v, ST.g_lay(T, l, d, n, t, g), len_slots(T, l, d, n, t, g, hn)))def room_nat(+n: Nat, +d: Nat, +b: Bool, +e: {Nat.is_lt(n, SC.pow2(d)) == b : Bool}) -> {Nat.is_lt(n, SC.pow2(d)) == b : Bool}: edef push_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +room: Bool, +er: {Nat.is_lt(n, SC.pow2(d)) == room : Bool}, +grow: Bool, +eg: {Nat.is_lt(d, l) == grow : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Push{v}): match room grow: case True{} _: +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) +hn = room_nat(n, d, True{}, er) +t2 = AR.upd(Maybe<&2, T>, d, t, n, Some{v}) (ST.Sh{l, d, 1n+n, t2}, (E.OUnit{Done{Unit{}}}, ( %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), True{}, er) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == (ST.real(T, ST.Sh{l, d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(n), Some{v}), AR.thaw(Maybe<&2, T>, t2), pi_arr(T, l, d, n, t, v, g, hn)) : {(DA.DA{l, d, SC.pow2(d), 1n+n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (pi_good(T, l, d, n, t, v, g, hn), %Equal.sym(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, t2)), SC.snoc(T, xs, v), pi_model(T, l, d, n, t, v, g, hn)) : {(S.M{l, d, _}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Push{v}) : S.Model<T> & E.Obs<T>} %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(_, SC.pow2(d)), (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), True{}, hn) : {(S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} {==})))) case False{} True{}: +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) +nf = room_nat(n, d, False{}, er) +t1 = {AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})} : AR.Tree<Maybe<&2, T>>} +g1 = GR.grow_good(T, l, d, n, t, g, eg) +hn = N.le_lt_trans(n, SC.pow2(d), SC.pow2(1n+d), n_le_cap(T, l, d, n, t, g), N.pow2_lt_succ(d)) +t2 = AR.upd(Maybe<&2, T>, 1n+d, t1, n, Some{v}) (ST.Sh{l, 1n+d, 1n+n, t2}, (E.OUnit{Done{Unit{}}}, ( %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, er) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(d, l), True{}, eg) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Array<Maybe<&2, T>>, DA.grown(T, d, AR.thaw(Maybe<&2, T>, t)), AR.thaw(Maybe<&2, T>, t1), ST.grown_eq(T, d, t)) : {(DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, Array.set(Maybe<&2, T>, _, U32.from_nat(n), Some{v})}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t1), U32.from_nat(n), Some{v}), AR.thaw(Maybe<&2, T>, t2), pi_arr(T, l, 1n+d, n, t1, v, g1, hn)) : {(DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, 1n+d, 1n+n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (pi_good(T, l, 1n+d, n, t1, v, g1, hn), %Equal.sym(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, t2)), SC.snoc(T, LY.somes(T, AR.slots(Maybe<&2, T>, t1)), v), pi_model(T, l, 1n+d, n, t1, v, g1, hn)) : {(S.M{l, 1n+d, _}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Push{v}) : S.Model<T> & E.Obs<T>} %Equal.sym(List<&2, T>, LY.somes(T, AR.slots(Maybe<&2, T>, t1)), xs, GR.grow_model(T, d, t)) : {(S.M{l, 1n+d, SC.snoc(T, _, v)}, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Push{v}) : S.Model<T> & E.Obs<T>} %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(_, SC.pow2(d)), (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, nf) : {(S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(d, l), True{}, eg) : {(S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>} {==})))) case False{} False{}: +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) +nf = room_nat(n, d, False{}, er) (ST.Sh{l, d, n, t}, (E.OUnit{Fail{E.CapacityExceeded{}}}, ( %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, er) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l))) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(d, l), False{}, eg) : {DA.obs_unit(T, DA.push_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, %Equal.sym(Nat, SC.length(T, xs), n, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, ST.g_lay(T, l, d, n, t, g))) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(_, SC.pow2(d)), (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, nf) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_lt(d, l), False{}, eg) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>} {==}))))def push_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +v: T, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Push{v}): push_case(T, l, d, n, t, v, g, Nat.is_lt(n, SC.pow2(d)), {==}, Nat.is_lt(d, l), {==})# ---- pop ----def pop_spec(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +m: Nat, +h: {SC.length(T, xs) == 1n+m : Nat}) -> {S.pop(T, l, d, xs) == (S.M{l, d, SC.init(T, xs)}, E.OItem{S.item_result(T, SC.nth(T, xs, m))}) : S.Model<T> & E.Obs<T>}: match xs: case Nil{}: Empty.absurd({S.pop(T, l, d, Nil{}) == (S.M{l, d, Nil{}}, E.OItem{S.item_result(T, None{})}) : S.Model<T> & E.Obs<T>}, N.zero_succ(m, h)) case Con{+x, +r}: %Equal.sym(Maybe<&2, T>, SC.nth(T, Con{x, r}, m), SC.last(T, Con{x, r}), LY.nth_last(T, Con{x, r}, m, h)) : {(S.M{l, d, SC.init(T, Con{x, r})}, E.OItem{S.item_result(T, SC.last(T, Con{x, r}))}) == (S.M{l, d, SC.init(T, Con{x, r})}, E.OItem{S.item_result(T, _)}) : S.Model<T> & E.Obs<T>} {==}def pop_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Pop{}): match n: case 0n: +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) (ST.Sh{l, d, 0n, t}, (E.OItem{Fail{E.EmptyArray{}}}, ({==}, (g, %Equal.sym(List<&2, T>, xs, Nil{}, LL.length_zero_nil(T, xs, LY.lay_len(T, AR.slots(Maybe<&2, T>, t), 0n, ST.g_lay(T, l, d, 0n, t, g)))) : {(S.M{l, d, _}, E.OItem{Fail{E.EmptyArray{}}}) == S.pop(T, l, d, _) : S.Model<T> & E.Obs<T>} {==})))) case 1n+ +m: +ss = AR.slots(Maybe<&2, T>, t) +xs = LY.somes(T, ss) +x = SC.nth(T, xs, m) +hlay = ST.g_lay(T, l, d, 1n+m, t, g) +hm = N.lt_succ(m) +hi = N.lt_le_trans(m, 1n+m, SC.pow2(d), hm, n_le_cap(T, l, d, 1n+m, t, g)) +t2 = AR.upd(Maybe<&2, T>, d, t, m, None{}) +hs = upd_slots(T, l, d, 1n+m, t, m, None{}, g, hi) (ST.Sh{l, d, m, t2}, (E.OItem{S.item_result(T, x)}, ( %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m), None{}), (AR.thaw(Maybe<&2, T>, t2), x), swap_arr(T, l, d, 1n+m, t, m, None{}, x, g, hi, LY.lay_nth(T, ss, 1n+m, m, hlay, hm))) : {DA.obs_item(T, DA.pop_found(T, l, d, SC.pow2(d), m, _)) == (ST.real(T, ST.Sh{l, d, m, t2}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Result<&2, &2, E.Error, T>, DA.slot_result(T, x), S.item_result(T, x), ST.slot_item(T, x)) : {(DA.DA{l, d, SC.pow2(d), m, AR.thaw(Maybe<&2, T>, t2)}, E.OItem{_}) == (ST.real(T, ST.Sh{l, d, m, t2}), E.OItem{S.item_result(T, x)}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (ST.good_intro(T, l, d, m, t2, ST.g_limit(T, l, d, 1n+m, t, g), ST.g_depth(T, l, d, 1n+m, t, g), AR.upd_perfect(Maybe<&2, T>, d, t, m, None{}, ST.g_perfect(T, l, d, 1n+m, t, g)), L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, m) == True{} : Bool}, SC.update(Maybe<&2, T>, ss, m, None{}), AR.slots(Maybe<&2, T>, t2), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, m, None{}), hs), LY.lay_pop(T, ss, m, hlay))), %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, m, None{}), hs) : {(S.M{l, d, LY.somes(T, _)}, E.OItem{S.item_result(T, x)}) == S.pop(T, l, d, xs) : S.Model<T> & E.Obs<T>} %Equal.sym(List<&2, T>, LY.somes(T, SC.update(Maybe<&2, T>, ss, m, None{})), SC.init(T, xs), LY.somes_pop(T, ss, m, hlay)) : {(S.M{l, d, _}, E.OItem{S.item_result(T, x)}) == S.pop(T, l, d, xs) : S.Model<T> & E.Obs<T>} Equal.sym(S.Model<T> & E.Obs<T>, S.pop(T, l, d, xs), (S.M{l, d, SC.init(T, xs)}, E.OItem{S.item_result(T, x)}), pop_spec(T, l, d, xs, m, LY.lay_len(T, ss, 1n+m, hlay)))))))# ---- clear ----def clear_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Clear{}): +t2 = AR.trep(Maybe<&2, T>, d, None{}) (ST.Sh{l, d, 0n, t2}, (E.OUnit{Done{Unit{}}}, ( %Equal.sym(Array<Maybe<&2, T>>, DA.empty_slots(T, d), AR.thaw(Maybe<&2, T>, t2), ST.empty_eq(T, d)) : {(DA.DA{l, d, SC.pow2(d), 0n, _}, E.OUnit{Done{Unit{}}}) == (ST.real(T, ST.Sh{l, d, 0n, t2}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (ST.good_intro(T, l, d, 0n, t2, ST.g_limit(T, l, d, n, t, g), ST.g_depth(T, l, d, n, t, g), AR.trep_perfect(Maybe<&2, T>, d, None{}), L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, 0n) == True{} : Bool}, SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.slots(Maybe<&2, T>, t2), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})), LY.lay_rep(T, SC.pow2(d)))), %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})) : {(S.M{l, d, LY.somes(T, _)}, E.OUnit{Done{Unit{}}}) == (S.M{l, d, Nil{}}, E.OUnit{S.ok_unit()}) : S.Model<T> & E.Obs<T>} %Equal.sym(List<&2, T>, LY.somes(T, SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})), Nil{}, LY.somes_rep(T, SC.pow2(d))) : {(S.M{l, d, _}, E.OUnit{Done{Unit{}}}) == (S.M{l, d, Nil{}}, E.OUnit{S.ok_unit()}) : S.Model<T> & E.Obs<T>} {==}))))# ---- to_list ----def to_list_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.ToList{}): match n: case 0n: +ss = AR.slots(Maybe<&2, T>, t) +xs = LY.somes(T, ss) (ST.Sh{l, d, 0n, t}, (E.OList{xs}, ( %Equal.sym(List<&2, T>, xs, Nil{}, LL.length_zero_nil(T, xs, LY.lay_len(T, ss, 0n, ST.g_lay(T, l, d, 0n, t, g)))) : {(DA.DA{l, d, SC.pow2(d), 0n, AR.thaw(Maybe<&2, T>, t)}, E.OList{Nil{}}) == (ST.real(T, ST.Sh{l, d, 0n, t}), E.OList{_}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, {==})))) case 1n+ +m: +ss = AR.slots(Maybe<&2, T>, t) +xs = LY.somes(T, ss) +hlay = ST.g_lay(T, l, d, 1n+m, t, g) +hd = ST.g_depth(T, l, d, 1n+m, t, g) +hl = ST.g_limit(T, l, d, 1n+m, t, g) +pf = ST.g_perfect(T, l, d, 1n+m, t, g) +hm = N.succ_le_lt(m, SC.pow2(d), n_le_cap(T, l, d, 1n+m, t, g)) (ST.Sh{l, d, 1n+m, t}, (E.OList{xs}, ( %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m)), (AR.thaw(Maybe<&2, T>, t), W.slot(T, ss, m)), W.get_slot(T, l, d, t, m, hd, hl, hm, pf)) : {DA.obs_list(T, DA.tl_done(T, l, d, SC.pow2(d), 1n+m, DA.tl_go(1n+m, T, Nil{}, _))) == (ST.real(T, ST.Sh{l, d, 1n+m, t}), E.OList{xs}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Array<Maybe<&2, T>> & List<&2, T>, DA.tl_go(1n+m, T, Nil{}, (AR.thaw(Maybe<&2, T>, t), W.slot(T, ss, m))), (AR.thaw(Maybe<&2, T>, t), W.tvals(1n+m, T, ss, Nil{})), W.tl_thaw(1n+m, T, l, d, t, Nil{}, hd, hl, hm, pf)) : {DA.obs_list(T, DA.tl_done(T, l, d, SC.pow2(d), 1n+m, _)) == (ST.real(T, ST.Sh{l, d, 1n+m, t}), E.OList{xs}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(List<&2, T>, W.tvals(1n+m, T, ss, Nil{}), xs, W.tvals_model(T, ss, 1n+m, hlay)) : {(DA.DA{l, d, SC.pow2(d), 1n+m, AR.thaw(Maybe<&2, T>, t)}, E.OList{_}) == (ST.real(T, ST.Sh{l, d, 1n+m, t}), E.OList{xs}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, {==}))))# ---- reserve ----def feasible_fuel(+l: Nat, +d: Nat, +k: Nat, +hdl: {Nat.is_le(d, l) == True{} : Bool}, +hp: {Nat.is_le(k, SC.pow2(l)) == True{} : Bool}) -> {Nat.is_le(k, SC.pow2(Nat.add(d, Nat.sub(l, d)))) == True{} : Bool}: L.subst(Nat, x => {Nat.is_le(k, SC.pow2(x)) == True{} : Bool}, l, Nat.add(d, Nat.sub(l, d)), Equal.sym(Nat, Nat.add(d, Nat.sub(l, d)), l, N.sub_add(l, d, hdl)), hp)def spec_fuel(+d: Nat, +k: Nat) -> {Nat.is_le(k, SC.pow2(Nat.add(d, k))) == True{} : Bool}: N.lt_le(k, SC.pow2(Nat.add(d, k)), N.lt_le_trans(k, SC.pow2(k), SC.pow2(Nat.add(d, k)), GR.pow2_gt(k), N.pow2_mono(k, Nat.add(d, k), L.subst(Nat, x => {Nat.is_le(k, x) == True{} : Bool}, Nat.add(k, d), Nat.add(d, k), N.add_comm(k, d), N.le_add_right(k, d)))))def reserve_case(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +k: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +fits: Bool, +ef: {Nat.is_le(k, SC.pow2(d)) == fits : Bool}, +feas: Bool, +ep: {Nat.is_le(k, DA.pow2(l)) == feas : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Reserve{k}): match fits feas: case True{} _: +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) (ST.Sh{l, d, n, t}, (E.OUnit{Done{Unit{}}}, ( %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, ef) : {DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, ef) : {(S.M{l, d, xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} {==})))) case False{} True{}: +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) +f = Nat.sub(l, d) +sh2 = GR.sgrow(T, f, k, ST.Sh{l, d, n, t}) +hdl = ST.g_depth(T, l, d, n, t, g) +hp = GR.fits_nat(k, l, True{}, ep) -mP = {ST.model(T, sh2) == S.M{l, S.fit(f, d, k), xs} : S.Model<T>} -gP = {ST.good(T, sh2) == True{} : Bool} +hf = L.subst(Nat, x => {Nat.is_le(x, l) == True{} : Bool}, l, Nat.add(d, f), Equal.sym(Nat, Nat.add(d, f), l, N.sub_add(l, d, hdl)), N.le_refl(l)) (sh2, (E.OUnit{Done{Unit{}}}, ( %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, sh2), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_le(k, DA.pow2(l)), True{}, ep) : {DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, sh2), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(DA.DynArray<&2, T>, DA.grow_until(T, f, k, ST.real(T, ST.Sh{l, d, n, t})), ST.real(T, sh2), GR.grow_until_real(T, f, k, ST.Sh{l, d, n, t})) : {(_, E.OUnit{Done{Unit{}}}) == (ST.real(T, sh2), E.OUnit{Done{Unit{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (Pair.snd(mP, gP, GR.sgrow_props(T, f, k, l, d, n, t, g, hf, Nat.is_le(k, SC.pow2(d)), {==})), %Equal.sym(S.Model<T>, ST.model(T, sh2), S.M{l, S.fit(f, d, k), xs}, Pair.fst(mP, gP, GR.sgrow_props(T, f, k, l, d, n, t, g, hf, Nat.is_le(k, SC.pow2(d)), {==}))) : {(_, E.OUnit{Done{Unit{}}}) == S.step(T, S.M{l, d, xs}, E.Reserve{k}) : S.Model<T> & E.Obs<T>} %Equal.sym(Nat, S.fit(f, d, k), S.fit(k, d, k), GR.fe_case(f, k, d, k, feasible_fuel(l, d, k, hdl, hp), spec_fuel(d, k), Nat.is_le(k, SC.pow2(d)), {==})) : {(S.M{l, _, xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(d)), (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {(S.M{l, S.fit(k, d, k), xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_le(k, SC.pow2(l)), True{}, hp) : {(S.M{l, S.fit(k, d, k), xs}, E.OUnit{Done{Unit{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>} {==})))) case False{} False{}: +xs = LY.somes(T, AR.slots(Maybe<&2, T>, t)) (ST.Sh{l, d, n, t}, (E.OUnit{Fail{E.CapacityExceeded{}}}, ( %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {DA.obs_unit(T, DA.reserve_checked(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_le(k, DA.pow2(l)), False{}, ep) : {DA.obs_unit(T, DA.reserve_room(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), k, _)) == (ST.real(T, ST.Sh{l, d, n, t}), E.OUnit{Fail{E.CapacityExceeded{}}}) : DA.DynArray<&2, T> & E.Obs<T>} {==}, (g, %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, ef) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(k, SC.pow2(l)), (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) : S.Model<T> & E.Obs<T>} %Equal.sym(Bool, Nat.is_le(k, SC.pow2(l)), False{}, GR.fits_nat(k, l, False{}, ep)) : {(S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) == Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, S.fit(k, d, k), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}})) : S.Model<T> & E.Obs<T>} {==}))))def reserve_ok(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +k: Nat, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> StepOK(T, ST.Sh{l, d, n, t}, E.Reserve{k}): reserve_case(T, l, d, n, t, k, g, Nat.is_le(k, SC.pow2(d)), {==}, Nat.is_le(k, DA.pow2(l)), {==})# ---- every operation ----def step_ok(-T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> StepOK(T, sh, op): match sh op: case ST.Sh{+l, +d, +n, +t} E.Length{}: length_ok(T, l, d, n, t, g) case ST.Sh{+l, +d, +n, +t} E.Capacity{}: capacity_ok(T, l, d, n, t, g) case ST.Sh{+l, +d, +n, +t} E.Get{+i}: get_ok(T, l, d, n, t, i, g) case ST.Sh{+l, +d, +n, +t} E.Set{+i, +v}: set_ok(T, l, d, n, t, i, v, g) case ST.Sh{+l, +d, +n, +t} E.Push{+v}: push_ok(T, l, d, n, t, v, g) case ST.Sh{+l, +d, +n, +t} E.Pop{}: pop_ok(T, l, d, n, t, g) case ST.Sh{+l, +d, +n, +t} E.Reserve{+k}: reserve_ok(T, l, d, n, t, k, g) case ST.Sh{+l, +d, +n, +t} E.Clear{}: clear_ok(T, l, d, n, t, g) case ST.Sh{+l, +d, +n, +t} E.ToList{}: to_list_ok(T, l, d, n, t, g)