proofs/containers/lru/bumpsh.bend
bend-collections-laws-containers@1.0.0.0 · 207 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
6import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/meta.bend as MT
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/basic.bend as BA
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bump.bend as BU
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
12
13# Counting on the shadow: fbump(c) increments counter c of the model.
14
15
16def CountOK(~V: Data, +spec: SP.Lru<V>, r: LR.LRU<&2, V>) -> Type:
17 Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : LR.LRU<&2, V>} & ({ST.model(~V, sh2) == spec : SP.Lru<V>} & {ST.good(~V, sh2) == True{} : Bool})>
18
19def 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
22def 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
25def keep(+ml: List<&2, U32>, +m2: AR.Tree<U32>, +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
30def bm_fin(~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}, +i: Nat, +h8: {Nat.is_le(8n, i) == True{} : Bool}, +m2: AR.Tree<U32>, +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
34def count_ins(~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}, 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<U32>, 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
46def count_ev(~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}, 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<U32>, 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
58def count_rm(~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}, 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<U32>, 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
70def count_hit(~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}, 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<U32>, 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
82def count_miss(~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}, 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<U32>, 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
96def CntM(~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>, +spec: SP.Lru<V>, r: LR.LRU<&2, V>) -> Type:
97 Sigma<&1, &1, AR.Tree<U32>, 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<V>} & {ST.good(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool})>
98
99def cntm_ins(~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}, 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<U32>, 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
110def cg_ins(~V: Data, l: SP.Lru<V>) -> SP.Lru<V>:
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
116def countg_ins(~V: Data, +sh: ST.Sh<V>, +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
121def cntm_ev(~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}, 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<U32>, 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
132def cg_ev(~V: Data, l: SP.Lru<V>) -> SP.Lru<V>:
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
138def countg_ev(~V: Data, +sh: ST.Sh<V>, +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
143def cntm_rm(~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}, 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<U32>, 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
154def cg_rm(~V: Data, l: SP.Lru<V>) -> SP.Lru<V>:
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
160def countg_rm(~V: Data, +sh: ST.Sh<V>, +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
165def cntm_hit(~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}, 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<U32>, 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
176def cg_hit(~V: Data, l: SP.Lru<V>) -> SP.Lru<V>:
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
182def countg_hit(~V: Data, +sh: ST.Sh<V>, +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
187def cntm_miss(~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}, 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<U32>, 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
198def cg_miss(~V: Data, l: SP.Lru<V>) -> SP.Lru<V>:
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
204def countg_miss(~V: Data, +sh: ST.Sh<V>, +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, {==}, {==}, {==}))