1 import Base 2 import ../../lib/nat.bend as N 3 import ../../lib/array.bend as AR 4 import ../../../spec/lib/common.bend as SC 5 import ../../../spec/containers/lru.bend as SP 6 import ../../../src/containers/lru.bend as LR 7 import ./state.bend as ST 8 import ./meta.bend as MT 9 import ./basic.bend as BA 10 import ./bump.bend as BU 11 import ../../lib/words32.bend as W32 12 13 # Counting on the shadow: fbump(c) increments counter c of the model. 14 15 16 def CountOK(~V: Data, +spec: SP.Lru, r: LR.LRU<&2, V>) -> Type: 17 Sigma<&1, &1, ST.Sh, sh2 => {r == ST.real(~V, sh2) : LR.LRU<&2, V>} & ({ST.model(~V, sh2) == spec : SP.Lru} & {ST.good(~V, sh2) == True{} : Bool})> 18 19 def lo8(+i: Nat, +h8: {Nat.is_le(8n, i) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 8n) == True{} : Bool}) -> {Nat.is_eq(i, j) == False{} : Bool}: 20 N.is_eq_sym_false(j, i, N.is_eq_lt(j, i, N.lt_le_trans(j, 8n, i, hj, h8))) 21 22 def lo8s(+i: Nat, +h8: {Nat.is_le(8n, i) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 8n) == True{} : Bool}) -> {Nat.is_eq(1n+i, j) == False{} : Bool}: 23 lo8(1n+i, N.le_trans(8n, i, 1n+i, h8, N.le_succ(i)), j, hj) 24 25 def keep(+ml: List<&2, U32>, +m2: AR.Tree, +i: Nat, +x: U32, +y: U32, +e: {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, ml, i, x), 1n+i, y) : List<&2, U32>}, +j: Nat, +h1: {Nat.is_eq(i, j) == False{} : Bool}, +h2: {Nat.is_eq(1n+i, j) == False{} : Bool}) -> {W32.nth0(AR.slots(U32, m2), j) == W32.nth0(ml, j) : U32}: 26 Equal.trans(U32, W32.nth0(AR.slots(U32, m2), j), W32.nth0(SC.update(U32, SC.update(U32, ml, i, x), 1n+i, y), j), W32.nth0(ml, j), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, j), AR.slots(U32, m2), SC.update(U32, SC.update(U32, ml, i, x), 1n+i, y), e), Equal.trans(U32, W32.nth0(SC.update(U32, SC.update(U32, ml, i, x), 1n+i, y), j), W32.nth0(SC.update(U32, ml, i, x), j), W32.nth0(ml, j), W32.nth0_upd_other(SC.update(U32, ml, i, x), 1n+i, j, y, h2), W32.nth0_upd_other(ml, i, j, x, h1))) 27 28 29 # the meta words of m2: i and i + 1 written, the invariant's words kept 30 def bm_fin(~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}, +i: Nat, +h8: {Nat.is_le(8n, i) == True{} : Bool}, +m2: AR.Tree, +pm2: {AR.perfect(U32, 5n, m2) == True{} : Bool}, +x: U32, +y: U32, +e: {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), i, x), 1n+i, y) : List<&2, U32>}) -> {ST.good(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}: 31 MT.good_m(~V, cap, n, head, tail, free, mT, m2, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, keep(AR.slots(U32, mT), m2, i, x, y, e, 0n, lo8(i, h8, 0n, {==}), lo8s(i, h8, 0n, {==})), keep(AR.slots(U32, mT), m2, i, x, y, e, 1n, lo8(i, h8, 1n, {==}), lo8s(i, h8, 1n, {==})), keep(AR.slots(U32, mT), m2, i, x, y, e, 2n, lo8(i, h8, 2n, {==}), lo8s(i, h8, 2n, {==})), keep(AR.slots(U32, mT), m2, i, x, y, e, 6n, lo8(i, h8, 6n, {==}), lo8s(i, h8, 6n, {==})), keep(AR.slots(U32, mT), m2, i, x, y, e, 7n, lo8(i, h8, 7n, {==}), lo8s(i, h8, 7n, {==})), pm2) 32 33 34 def count_ins(~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}, bo: BU.BumpOK(mT, 16n, LR.bump(0, AR.thaw(U32, mT)))) -> CountOK(~V, 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), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 35 match bo: 36 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 37 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 16n, x), 1n+16n, y) : List<&2, U32>}} 38 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(0, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 39 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 16n, {==}, m2, pm2, x, y, ee) 40 +e3 = keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 3n, {==}, {==}) 41 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 5n, {==}, {==})) 42 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), SP.inc64(ST.w64(AR.slots(U32, mT), 16n)), ST.w64(AR.slots(U32, mT), 18n), ST.w64(AR.slots(U32, mT), 20n), ST.w64(AR.slots(U32, mT), 22n), ST.w64(AR.slots(U32, mT), 24n), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 19n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 21n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 23n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 25n, {==}, {==}))) 43 (ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_ins(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 44 45 46 def count_ev(~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}, bo: BU.BumpOK(mT, 18n, LR.bump(1, AR.thaw(U32, mT)))) -> CountOK(~V, 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), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 47 match bo: 48 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 49 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 18n, x), 1n+18n, y) : List<&2, U32>}} 50 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(1, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 51 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 18n, {==}, m2, pm2, x, y, ee) 52 +e3 = keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 3n, {==}, {==}) 53 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 5n, {==}, {==})) 54 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), SP.inc64(ST.w64(AR.slots(U32, mT), 18n)), ST.w64(AR.slots(U32, mT), 20n), ST.w64(AR.slots(U32, mT), 22n), ST.w64(AR.slots(U32, mT), 24n), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 17n, {==}, {==})), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 21n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 23n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 25n, {==}, {==}))) 55 (ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_ev(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 56 57 58 def count_rm(~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}, bo: BU.BumpOK(mT, 20n, LR.bump(2, AR.thaw(U32, mT)))) -> CountOK(~V, 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), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 59 match bo: 60 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 61 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 20n, x), 1n+20n, y) : List<&2, U32>}} 62 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(2, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 63 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 20n, {==}, m2, pm2, x, y, ee) 64 +e3 = keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 3n, {==}, {==}) 65 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 5n, {==}, {==})) 66 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), ST.w64(AR.slots(U32, mT), 18n), SP.inc64(ST.w64(AR.slots(U32, mT), 20n)), ST.w64(AR.slots(U32, mT), 22n), ST.w64(AR.slots(U32, mT), 24n), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 17n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 19n, {==}, {==})), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 23n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 25n, {==}, {==}))) 67 (ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_rm(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 68 69 70 def count_hit(~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}, bo: BU.BumpOK(mT, 22n, LR.bump(3, AR.thaw(U32, mT)))) -> CountOK(~V, 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), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 3, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 71 match bo: 72 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 73 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 22n, x), 1n+22n, y) : List<&2, U32>}} 74 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(3, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 75 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 22n, {==}, m2, pm2, x, y, ee) 76 +e3 = keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 3n, {==}, {==}) 77 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 5n, {==}, {==})) 78 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), ST.w64(AR.slots(U32, mT), 18n), ST.w64(AR.slots(U32, mT), 20n), SP.inc64(ST.w64(AR.slots(U32, mT), 22n)), ST.w64(AR.slots(U32, mT), 24n), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 17n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 19n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 21n, {==}, {==})), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 25n, {==}, {==}))) 79 (ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_hit(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 80 81 82 def count_miss(~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}, bo: BU.BumpOK(mT, 24n, LR.bump(4, AR.thaw(U32, mT)))) -> CountOK(~V, 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), SP.c_miss(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 4, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 83 match bo: 84 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 85 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 24n, x), 1n+24n, y) : List<&2, U32>}} 86 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(4, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 87 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 24n, {==}, m2, pm2, x, y, ee) 88 +e3 = keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 3n, {==}, {==}) 89 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 5n, {==}, {==})) 90 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), ST.w64(AR.slots(U32, mT), 18n), ST.w64(AR.slots(U32, mT), 20n), ST.w64(AR.slots(U32, mT), 22n), SP.inc64(ST.w64(AR.slots(U32, mT), 24n)), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 17n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 19n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 21n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 23n, {==}, {==})), ew) 91 (ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_miss(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 92 93 94 # ---- counting with the new meta tree exposed, and on any shadow ---- 95 96 def CntM(~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>, +spec: SP.Lru, r: LR.LRU<&2, V>) -> Type: 97 Sigma<&1, &1, AR.Tree, m2 => {r == ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}) : LR.LRU<&2, V>} & ({ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}) == spec : SP.Lru} & {ST.good(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool})> 98 99 def cntm_ins(~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}, bo: BU.BumpOK(mT, 16n, LR.bump(0, AR.thaw(U32, mT)))) -> CntM(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, 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), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 100 match bo: 101 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 102 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 16n, x), 1n+16n, y) : List<&2, U32>}} 103 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(0, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 104 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 16n, {==}, m2, pm2, x, y, ee) 105 +e3 = keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 3n, {==}, {==}) 106 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 5n, {==}, {==})) 107 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), SP.inc64(ST.w64(AR.slots(U32, mT), 16n)), ST.w64(AR.slots(U32, mT), 18n), ST.w64(AR.slots(U32, mT), 20n), ST.w64(AR.slots(U32, mT), 22n), ST.w64(AR.slots(U32, mT), 24n), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 19n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 21n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 23n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 16n, x, y, ee, 25n, {==}, {==}))) 108 (m2, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_ins(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 109 110 def cg_ins(~V: Data, l: SP.Lru) -> SP.Lru: 111 match l: 112 case SP.L{cap, on, life, es, c}: 113 SP.L{cap, on, life, es, SP.c_ins(c)} 114 115 # THEOREM: fbump(0) counts on any shadow 116 def countg_ins(~V: Data, +sh: ST.Sh, +hg: {ST.good(~V, sh) == True{} : Bool}) -> CountOK(~V, cg_ins(~V, ST.model(~V, sh)), LR.fbump(&2, V, 0, ST.real(~V, sh))): 117 match sh: 118 case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 119 count_ins(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, BU.bump_ok(mT, 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), 0, 16n, {==}, {==}, {==})) 120 121 def cntm_ev(~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}, bo: BU.BumpOK(mT, 18n, LR.bump(1, AR.thaw(U32, mT)))) -> CntM(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, 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), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 122 match bo: 123 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 124 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 18n, x), 1n+18n, y) : List<&2, U32>}} 125 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(1, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 126 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 18n, {==}, m2, pm2, x, y, ee) 127 +e3 = keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 3n, {==}, {==}) 128 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 5n, {==}, {==})) 129 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), SP.inc64(ST.w64(AR.slots(U32, mT), 18n)), ST.w64(AR.slots(U32, mT), 20n), ST.w64(AR.slots(U32, mT), 22n), ST.w64(AR.slots(U32, mT), 24n), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 17n, {==}, {==})), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 21n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 23n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 18n, x, y, ee, 25n, {==}, {==}))) 130 (m2, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_ev(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 131 132 def cg_ev(~V: Data, l: SP.Lru) -> SP.Lru: 133 match l: 134 case SP.L{cap, on, life, es, c}: 135 SP.L{cap, on, life, es, SP.c_ev(c)} 136 137 # THEOREM: fbump(1) counts on any shadow 138 def countg_ev(~V: Data, +sh: ST.Sh, +hg: {ST.good(~V, sh) == True{} : Bool}) -> CountOK(~V, cg_ev(~V, ST.model(~V, sh)), LR.fbump(&2, V, 1, ST.real(~V, sh))): 139 match sh: 140 case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 141 count_ev(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, BU.bump_ok(mT, 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), 1, 18n, {==}, {==}, {==})) 142 143 def cntm_rm(~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}, bo: BU.BumpOK(mT, 20n, LR.bump(2, AR.thaw(U32, mT)))) -> CntM(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, 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), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 144 match bo: 145 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 146 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 20n, x), 1n+20n, y) : List<&2, U32>}} 147 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(2, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 148 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 20n, {==}, m2, pm2, x, y, ee) 149 +e3 = keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 3n, {==}, {==}) 150 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 5n, {==}, {==})) 151 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), ST.w64(AR.slots(U32, mT), 18n), SP.inc64(ST.w64(AR.slots(U32, mT), 20n)), ST.w64(AR.slots(U32, mT), 22n), ST.w64(AR.slots(U32, mT), 24n), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 17n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 19n, {==}, {==})), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 23n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 20n, x, y, ee, 25n, {==}, {==}))) 152 (m2, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_rm(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 153 154 def cg_rm(~V: Data, l: SP.Lru) -> SP.Lru: 155 match l: 156 case SP.L{cap, on, life, es, c}: 157 SP.L{cap, on, life, es, SP.c_rm(c)} 158 159 # THEOREM: fbump(2) counts on any shadow 160 def countg_rm(~V: Data, +sh: ST.Sh, +hg: {ST.good(~V, sh) == True{} : Bool}) -> CountOK(~V, cg_rm(~V, ST.model(~V, sh)), LR.fbump(&2, V, 2, ST.real(~V, sh))): 161 match sh: 162 case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 163 count_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, BU.bump_ok(mT, 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), 2, 20n, {==}, {==}, {==})) 164 165 def cntm_hit(~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}, bo: BU.BumpOK(mT, 22n, LR.bump(3, AR.thaw(U32, mT)))) -> CntM(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, 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), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 3, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 166 match bo: 167 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 168 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 22n, x), 1n+22n, y) : List<&2, U32>}} 169 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(3, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 170 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 22n, {==}, m2, pm2, x, y, ee) 171 +e3 = keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 3n, {==}, {==}) 172 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 5n, {==}, {==})) 173 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), ST.w64(AR.slots(U32, mT), 18n), ST.w64(AR.slots(U32, mT), 20n), SP.inc64(ST.w64(AR.slots(U32, mT), 22n)), ST.w64(AR.slots(U32, mT), 24n), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 17n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 19n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 21n, {==}, {==})), ew, BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 24n, keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 24n, {==}, {==}), keep(AR.slots(U32, mT), m2, 22n, x, y, ee, 25n, {==}, {==}))) 174 (m2, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_hit(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 175 176 def cg_hit(~V: Data, l: SP.Lru) -> SP.Lru: 177 match l: 178 case SP.L{cap, on, life, es, c}: 179 SP.L{cap, on, life, es, SP.c_hit(c)} 180 181 # THEOREM: fbump(3) counts on any shadow 182 def countg_hit(~V: Data, +sh: ST.Sh, +hg: {ST.good(~V, sh) == True{} : Bool}) -> CountOK(~V, cg_hit(~V, ST.model(~V, sh)), LR.fbump(&2, V, 3, ST.real(~V, sh))): 183 match sh: 184 case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 185 count_hit(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, BU.bump_ok(mT, 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), 3, 22n, {==}, {==}, {==})) 186 187 def cntm_miss(~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}, bo: BU.BumpOK(mT, 24n, LR.bump(4, AR.thaw(U32, mT)))) -> CntM(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, 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), SP.c_miss(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 4, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): 188 match bo: 189 case Tuple{+m2, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, e}}}}}}: 190 +ee = {e : {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), 24n, x), 1n+24n, y) : List<&2, U32>}} 191 +er = Equal.cong(Array, LR.LRU<&2, V>, z => LR.F{cap, n, head, tail, free, z, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, LR.bump(4, AR.thaw(U32, mT)), AR.thaw(U32, m2), ea) 192 +g = bm_fin(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, 24n, {==}, m2, pm2, x, y, ee) 193 +e3 = keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 3n, {==}, {==}) 194 +e4 = BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 4n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 4n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 5n, {==}, {==})) 195 +ec = BA.ct5(ST.w64(AR.slots(U32, m2), 16n), ST.w64(AR.slots(U32, m2), 18n), ST.w64(AR.slots(U32, m2), 20n), ST.w64(AR.slots(U32, m2), 22n), ST.w64(AR.slots(U32, m2), 24n), ST.w64(AR.slots(U32, mT), 16n), ST.w64(AR.slots(U32, mT), 18n), ST.w64(AR.slots(U32, mT), 20n), ST.w64(AR.slots(U32, mT), 22n), SP.inc64(ST.w64(AR.slots(U32, mT), 24n)), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 16n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 16n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 17n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 18n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 18n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 19n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 20n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 20n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 21n, {==}, {==})), BA.w64_eq(AR.slots(U32, m2), AR.slots(U32, mT), 22n, keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 22n, {==}, {==}), keep(AR.slots(U32, mT), m2, 24n, x, y, ee, 23n, {==}, {==})), ew) 196 (m2, (er, (BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, m2)), SP.c_miss(ST.ctr(AR.slots(U32, mT))), e3, e4, {==}, ec), g))) 197 198 def cg_miss(~V: Data, l: SP.Lru) -> SP.Lru: 199 match l: 200 case SP.L{cap, on, life, es, c}: 201 SP.L{cap, on, life, es, SP.c_miss(c)} 202 203 # THEOREM: fbump(4) counts on any shadow 204 def countg_miss(~V: Data, +sh: ST.Sh, +hg: {ST.good(~V, sh) == True{} : Bool}) -> CountOK(~V, cg_miss(~V, ST.model(~V, sh)), LR.fbump(&2, V, 4, ST.real(~V, sh))): 205 match sh: 206 case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: 207 count_miss(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, BU.bump_ok(mT, 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), 4, 24n, {==}, {==}, {==}))