proofs/containers/lru/drop.bend
bend-collections-laws-containers@1.0.0.0 · 30 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
8import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
14
15# drop_core: a detached slot's value is taken out, the slot is pushed on the
16# free list, the count goes down and counter c goes up.
17
18
19# THEOREM (drop_core)
20def drop_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +hpe: {AR.perfect(Maybe<&2, V>, sd, eT) == True{} : Bool}, +su: U32, +s: Nat, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +c: U32) -> {LR.drop_core(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, c) == (LR.fbump(&2, V, c, LR.F{cap, U32.sub(n, 1), head, tail, H.link(su), AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.nidx(su)), free))}), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s)) : LR.LRU<&2, V> & Maybe<&2, V>}:
21 +hsu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(su), Equal.sym(Nat, UD.v(su), s, hsv), hs0)
22 +hd = N.lt_trans(sd, 3n+sd, 32n, N.lt_le_trans(sd, 1n+sd, 3n+sd, N.lt_succ(sd), N.le_trans(1n+sd, 2n+sd, 3n+sd, N.le_succ(1n+sd), N.le_succ(2n+sd))), hsd)
23 +hx = HT.nthm_some(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su), UT.len_of(Maybe<&2, V>, sd, eT, hpe, UD.v(su), hsu))
24 +es = AR.swap(Maybe<&2, V>, sd, eT, su, None{}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su)), hd, hsu, hx, hpe)
25 +iN = Equal.trans(Nat, UD.v(LR.nidx(su)), ST.off(UD.v(su), 1n), ST.off(s, 1n), ID.w1(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 1n), UD.v(su), s, hsv))
26 +el = UL.wr(one, h1, lkT, sd, hsd, hpl, LR.nidx(su), s, 1n, {==}, hs0, iN, free)
27 +E1 = Equal.cong(Array<Maybe<&2, V>> & Maybe<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.drop_e(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(U32, lkT), su, c, r), Array.swap(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, None{}), (AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su))), es)
28 +E2 = Equal.cong(Array<U32>, LR.LRU<&2, V> & Maybe<&2, V>, z => (LR.F{cap, U32.sub(n, 1), head, tail, H.link(su), LR.bump(c, AR.thaw(U32, mT)), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), z}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su))), Array.set(U32, AR.thaw(U32, lkT), LR.nidx(su), free), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.nidx(su)), free)), el)
29 +E3 = Equal.cong(Nat, LR.LRU<&2, V> & Maybe<&2, V>, z => (LR.fbump(&2, V, c, LR.F{cap, U32.sub(n, 1), head, tail, H.link(su), AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.nidx(su)), free))}), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), z)), UD.v(su), s, hsv)
30 Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.drop_e(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(U32, lkT), su, c, Array.swap(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, None{})), LR.drop_e(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(U32, lkT), su, c, (AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su)))), (LR.fbump(&2, V, c, LR.F{cap, U32.sub(n, 1), head, tail, H.link(su), AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.nidx(su)), free))}), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s)), E1, Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, (LR.F{cap, U32.sub(n, 1), head, tail, H.link(su), LR.bump(c, AR.thaw(U32, mT)), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), Array.set(U32, AR.thaw(U32, lkT), LR.nidx(su), free)}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su))), (LR.fbump(&2, V, c, LR.F{cap, U32.sub(n, 1), head, tail, H.link(su), AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.nidx(su)), free))}), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su))), (LR.fbump(&2, V, c, LR.F{cap, U32.sub(n, 1), head, tail, H.link(su), AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.nidx(su)), free))}), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s)), E2, E3))