1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/array.bend as AR 5 import ../../../spec/containers/lru.bend as SP 6 import ../../lib/u32div.bend as UD 7 import ../../../src/containers/lru.bend as LR 8 import ./state.bend as ST 9 import ./basic.bend as BA 10 import ./bumpsh.bend as BS 11 import ./rmat.bend as RM 12 import ../hash_table/probe_impl.bend as PI 13 14 import ../../lib/u32.bend as U 15 import ./evict.bend as EV 16 import ../../lib/words32.bend as W32 17 18 # resize: evicting the oldest until the cache fits. 19 20 21 22 def RzOK(~V: Data, spec: SP.Lru & U32, r: LR.LRU<&2, V> & Result<&2, &2, String, U32>) -> Type: 23 Sigma<&1, &1, ST.Sh, 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 & U32} & {ST.good(~V, sh2) == True{} : Bool})>> 24 25 26 # the count is the model's length 27 def n_len(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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}: 28 +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)) 29 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))) 30 31 def rz0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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)): 32 match b: 33 case True{}: 34 (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (ev, ({==}, ({==}, hg)))) 35 case False{}: 36 (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (ev, ({==}, ({==}, hg)))) 37 38 def rz_ev(~V: Data, +p: Nat, +ev: U32, +sh: ST.Sh, +spec: SP.Lru, -r: LR.LRU<&2, V>, co: BS.CountOK(~V, spec, r), rec: @sh1: ST.Sh -> @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))): 39 match co: 40 case Tuple{+sh1, Tuple{+e1, Tuple{+em1, g1}}}: 41 ok = rec(sh1, g1) 42 ok2 = L.subst(SP.Lru, 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) 43 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) 44 45 46 def lt0(+x: U32) -> {U32.is_lt(x, 0) == False{} : Bool}: 47 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))) 48 49 def rz_sl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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 -> @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))): 50 match sl: 51 case Nil{}: 52 +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)), {==}) 53 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))))) 54 case Con{+s0, +t}: 55 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) 56 57 def rz1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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 -> @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 & 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)): 58 match b: 59 case True{}: 60 rz_sl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, p, ev, hb, rec) 61 case False{}: 62 (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (ev, ({==}, ({==}, hg)))) 63 64 def rz_f(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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 -> @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)): 65 +en = n_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 66 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) 67 L.subst(U32, z => RzOK(~V, Bool.pick(SP.Lru & 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) 68 69 # THEOREM: the eviction loop is the specification's shrink 70 def rz_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +f: Nat, +sh: ST.Sh, +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)): 71 match f sh: 72 case 0n ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 73 rz0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, ev, U32.is_lt(cap, n)) 74 case 1n+p ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 75 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))) 76 77 78 # a new positive capacity keeps the invariant 79 def good_cap(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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}: 80 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), 1 81 82 def rs_fin(~V: Data, spec: SP.Lru & 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): 83 match ok: 84 case Tuple{+sh2, Tuple{+e, Tuple{+er, Tuple{+es, g}}}}: 85 (sh2, (Done{e}, (er, (Equal.cong(SP.Lru & U32, SP.Lru & Result<&2, &2, String, U32>, z => SP.rs_done(~V, z), spec, (ST.model(~V, sh2), e), es), g)))) 86 87 def rs_c(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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)): 88 match z: 89 case True{}: 90 (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (Fail{"capacity must be positive"}, ({==}, ({==}, hg)))) 91 case False{}: 92 +g2 = good_cap(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, cap2, hz) 93 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) 94 +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))) 95 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) 96 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) 97 98 # THEOREM (resize): the specification's resize 99 def resize_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh, +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)): 100 match sh: 101 case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 102 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), {==})