proofs/containers/lru/resize.bend source
proofs/containers/lru/resize.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/containers/lru.bend as LRimport ./state.bend as STimport ./basic.bend as BAimport ./bumpsh.bend as BSimport ./rmat.bend as RMimport ../hash_table/probe_impl.bend as PIimport ../../lib/u32.bend as Uimport ./evict.bend as EVimport ../../lib/words32.bend as W32# resize: evicting the oldest until the cache fits.def RzOK(~V: Data, spec: SP.Lru<V> & U32, r: LR.LRU<&2, V> & Result<&2, &2, String, U32>) -> Type: Sigma<&1, &1, ST.Sh<V>, sh2 => Sigma<&1, &1, U32, e => {r == (ST.real(~V, sh2), Done{e}) : LR.LRU<&2, V> & Result<&2, &2, String, U32>} & ({spec == (ST.model(~V, sh2), e) : SP.Lru<V> & U32} & {ST.good(~V, sh2) == True{} : Bool})>># the count is the model's lengthdef n_len(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}) -> {U32.from_nat(SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl))) == n : U32}: +hk = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) Equal.trans(U32, U32.from_nat(SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl))), U32.from_nat(UD.v(n)), n, Equal.cong(Nat, U32, z => U32.from_nat(z), SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), UD.v(n), BA.len_model(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)), PI.from_v(n, k, N.lt_le(k, 32n, N.lt_trans(k, 30n, 32n, hk, {==})), BA.n_lt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)))def rz0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +ev: U32, +b: Bool) -> RzOK(~V, SP.shrink(~V, 0n, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), ev), LR.rz_go(&2, V, 0n, LR.rz_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), b), ev)): match b: case True{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (ev, ({==}, ({==}, hg)))) case False{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (ev, ({==}, ({==}, hg))))def rz_ev(~V: Data, +p: Nat, +ev: U32, +sh: ST.Sh<V>, +spec: SP.Lru<V>, -r: LR.LRU<&2, V>, co: BS.CountOK(~V, spec, r), rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> RzOK(~V, SP.shrink(~V, p, ST.model(~V, sh1), U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, ST.real(~V, sh1)), U32.inc(ev)))) -> RzOK(~V, SP.shrink(~V, p, spec, U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, r), U32.inc(ev))): match co: case Tuple{+sh1, Tuple{+e1, Tuple{+em1, g1}}}: ok = rec(sh1, g1) ok2 = L.subst(SP.Lru<V>, z => RzOK(~V, SP.shrink(~V, p, z, U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, ST.real(~V, sh1)), U32.inc(ev))), ST.model(~V, sh1), spec, em1, ok) L.subst(LR.LRU<&2, V>, z => RzOK(~V, SP.shrink(~V, p, spec, U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, z), U32.inc(ev))), ST.real(~V, sh1), r, Equal.sym(LR.LRU<&2, V>, r, ST.real(~V, sh1), e1), ok2)def lt0(+x: U32) -> {U32.is_lt(x, 0) == False{} : Bool}: Equal.trans(Bool, U32.is_lt(x, 0), Nat.is_lt(UD.v(x), 0n), False{}, U.is_lt_nat(x, 0), N.not_lt_zero(UD.v(x)))def rz_sl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +p: Nat, +ev: U32, +hb: {U32.is_lt(cap, n) == True{} : Bool}, rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> RzOK(~V, SP.shrink(~V, p, ST.model(~V, sh1), U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, ST.real(~V, sh1)), U32.inc(ev)))) -> RzOK(~V, SP.shrink(~V, p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, LR.evict_oldest(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))), U32.inc(ev))): match sl: case Nil{}: +en = Equal.trans(U32, n, U32.from_nat(0n), 0, Equal.sym(U32, U32.from_nat(0n), n, n_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl, hg)), {==}) Empty.absurd(RzOK(~V, SP.shrink(~V, p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Nil{})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, LR.evict_oldest(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}))), U32.inc(ev))), L.true_false(Equal.trans(Bool, True{}, U32.is_lt(cap, n), False{}, Equal.sym(Bool, U32.is_lt(cap, n), True{}, hb), L.subst(U32, z => {U32.is_lt(cap, z) == False{} : Bool}, 0, n, Equal.sym(U32, n, 0, en), lt0(cap))))) case Con{+s0, +t}: rz_ev(~V, p, ev, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.evict_oldest(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl})), EV.old_ev(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1), rec)def rz1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +p: Nat, +ev: U32, +b: Bool, +hb: {U32.is_lt(cap, n) == b : Bool}, rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> RzOK(~V, SP.shrink(~V, p, ST.model(~V, sh1), U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, ST.real(~V, sh1)), U32.inc(ev)))) -> RzOK(~V, Bool.pick(SP.Lru<V> & U32, b, SP.shrink(~V, p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, U32.inc(ev)), (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT))}, ev)), LR.rz_go(&2, V, 1n+p, LR.rz_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), b), ev)): match b: case True{}: rz_sl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, p, ev, hb, rec) case False{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (ev, ({==}, ({==}, hg))))def rz_f(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +p: Nat, +ev: U32, rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> RzOK(~V, SP.shrink(~V, p, ST.model(~V, sh1), U32.inc(ev)), LR.rz_go(&2, V, p, LR.rz_check(&2, V, ST.real(~V, sh1)), U32.inc(ev)))) -> RzOK(~V, SP.shrink(~V, 1n+p, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), ev), LR.rz_go(&2, V, 1n+p, LR.rz_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), ev)): +en = n_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) ok = rz1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, p, ev, U32.is_lt(cap, n), {==}, rec) L.subst(U32, z => RzOK(~V, Bool.pick(SP.Lru<V> & U32, U32.is_lt(cap, z), SP.shrink(~V, p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, U32.inc(ev)), (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT))}, ev)), LR.rz_go(&2, V, 1n+p, LR.rz_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), ev)), n, U32.from_nat(SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl))), Equal.sym(U32, U32.from_nat(SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl))), n, en), ok)# THEOREM: the eviction loop is the specification's shrinkdef rz_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +f: Nat, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +ev: U32) -> RzOK(~V, SP.shrink(~V, f, ST.model(~V, sh), ev), LR.rz_go(&2, V, f, LR.rz_check(&2, V, ST.real(~V, sh)), ev)): match f sh: case 0n ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: rz0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, ev, U32.is_lt(cap, n)) case 1n+p ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: rz_f(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, p, ev, sh1 => g1 => rz_ok(~V, one, h1, p, sh1, g1, U32.inc(ev)))# a new positive capacity keeps the invariantdef good_cap(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +cap2: U32, +hz: {U32.is_eq(cap2, 0) == False{} : Bool}) -> {ST.good(~V, ST.LS{cap2, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}: ST.good_intro(~V, cap2, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cpk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cmask(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cbits(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_csize(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cdepth(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cclus(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cuniq(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cn(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cload(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), Equal.cong(Bool, Bool, b => Bool.not(b), U32.is_eq(cap2, 0), False{}, hz), ST.g_cbsl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_chas(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_clen(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_ctail(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cdll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_ckeys(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cfree(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cfll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cfnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg))def rs_fin(~V: Data, spec: SP.Lru<V> & U32, -r: LR.LRU<&2, V> & Result<&2, &2, String, U32>, ok: RzOK(~V, spec, r)) -> RM.POK(~V, Result<&2, &2, String, U32>, SP.rs_done(~V, spec), r): match ok: case Tuple{+sh2, Tuple{+e, Tuple{+er, Tuple{+es, g}}}}: (sh2, (Done{e}, (er, (Equal.cong(SP.Lru<V> & U32, SP.Lru<V> & Result<&2, &2, String, U32>, z => SP.rs_done(~V, z), spec, (ST.model(~V, sh2), e), es), g))))def rs_c(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +cap2: U32, +z: Bool, +hz: {U32.is_eq(cap2, 0) == z : Bool}) -> RM.POK(~V, Result<&2, &2, String, U32>, SP.resize_c(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), cap2, z), LR.resize_go(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), cap2, z)): match z: case True{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (Fail{"capacity must be positive"}, ({==}, ({==}, hg)))) case False{}: +g2 = good_cap(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, cap2, hz) ok = rz_ok(~V, one, h1, U32.to_nat(n), ST.LS{cap2, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, g2, 0) +el = Equal.trans(Nat, U32.to_nat(n), UD.v(n), SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), {==}, Equal.sym(Nat, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), UD.v(n), BA.len_model(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg))) ok2 = L.subst(Nat, f => RzOK(~V, SP.shrink(~V, f, ST.model(~V, ST.LS{cap2, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), 0), LR.rz_go(&2, V, U32.to_nat(n), LR.rz_check(&2, V, ST.real(~V, ST.LS{cap2, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), 0)), U32.to_nat(n), SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), el, ok) rs_fin(~V, SP.shrink(~V, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), ST.model(~V, ST.LS{cap2, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), 0), LR.rz_go(&2, V, U32.to_nat(n), LR.rz_check(&2, V, ST.real(~V, ST.LS{cap2, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), 0), ok2)# THEOREM (resize): the specification's resizedef resize_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cap2: U32) -> RM.POK(~V, Result<&2, &2, String, U32>, SP.resize(~V, ST.model(~V, sh), cap2), LR.resize(&2, V, ST.real(~V, sh), cap2)): match sh: case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: rs_c(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, cap2, U32.is_eq(cap2, 0), {==})