proofs/containers/lru/ent.bend
bend-collections-laws-containers@1.0.0.0 · 43 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
3import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
4import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
5import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
9
10# The entry add stores, from the lifetime words: the specification's mk.
11
12
13def EntOK(~V: Data, +mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +v: V, +now: W.U64, +key: String) -> Type:
14 Sigma<&1, &1, U32, t => Sigma<&1, &1, U32, lo => Sigma<&1, &1, U32, hi => {LR.entry_of(&2, V, AR.thaw(U32, mT), v, now) == (AR.thaw(U32, mT), LR.E{v, t, lo, hi}) : Array<U32> & LR.Ent<&2, V>} & {SP.LE{key, v, t, W.U64{lo, hi}} == SP.mk(~V, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), key, v, now) : SP.Ent<V>}>>>
15
16
17def ent_d(~V: Data, +mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +v: V, +now: W.U64, +key: String, +d: W.U64, +hd: {W.add(now, ST.w64(AR.slots(U32, mT), 4n)) == d : W.U64}, +e0: {LR.entry_of(&2, V, AR.thaw(U32, mT), v, now) == (AR.thaw(U32, mT), LR.ent_dl(&2, V, v, W.add(now, ST.w64(AR.slots(U32, mT), 4n)))) : Array<U32> & LR.Ent<&2, V>}, +hsp: {SP.LE{key, v, 1, W.add(now, ST.w64(AR.slots(U32, mT), 4n))} == SP.mk(~V, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), key, v, now) : SP.Ent<V>}) -> EntOK(~V, mT, pm, v, now, key):
18 match d:
19 case W.U64{+lo, +hi}:
20 +e1 = Equal.cong(W.U64, Array<U32> & LR.Ent<&2, V>, z => (AR.thaw(U32, mT), LR.ent_dl(&2, V, v, z)), W.add(now, ST.w64(AR.slots(U32, mT), 4n)), W.U64{lo, hi}, hd)
21 +s1 = Equal.cong(W.U64, SP.Ent<V>, z => SP.LE{key, v, 1, z}, W.add(now, ST.w64(AR.slots(U32, mT), 4n)), W.U64{lo, hi}, hd)
22 (1, (lo, (hi, (Equal.trans(Array<U32> & LR.Ent<&2, V>, LR.entry_of(&2, V, AR.thaw(U32, mT), v, now), (AR.thaw(U32, mT), LR.ent_dl(&2, V, v, W.add(now, ST.w64(AR.slots(U32, mT), 4n)))), (AR.thaw(U32, mT), LR.E{v, 1, lo, hi}), e0, e1), Equal.trans(SP.Ent<V>, SP.LE{key, v, 1, W.U64{lo, hi}}, SP.LE{key, v, 1, W.add(now, ST.w64(AR.slots(U32, mT), 4n))}, SP.mk(~V, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), key, v, now), Equal.sym(SP.Ent<V>, SP.LE{key, v, 1, W.add(now, ST.w64(AR.slots(U32, mT), 4n))}, SP.LE{key, v, 1, W.U64{lo, hi}}, s1), hsp)))))
23
24
25def ent_c(~V: Data, +mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +v: V, +now: W.U64, +key: String, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, mT), 3n), 0) == c : Bool}, +e0: {LR.entry_of(&2, V, AR.thaw(U32, mT), v, now) == LR.ent_if(&2, V, v, now, AR.thaw(U32, mT), Bool.not(c)) : Array<U32> & LR.Ent<&2, V>}) -> EntOK(~V, mT, pm, v, now, key):
26 match c:
27 case True{}:
28 +hs = Equal.sym(SP.Ent<V>, SP.mk(~V, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), key, v, now), SP.LE{key, v, 0, W.zero()}, Equal.cong(Bool, SP.Ent<V>, b => SP.mk_c(~V, ST.w64(AR.slots(U32, mT), 4n), key, v, now, b), U32.is_eq(W32.nth0(AR.slots(U32, mT), 3n), 0), True{}, hc))
29 (0, (0, (0, (e0, hs))))
30 case False{}:
31 +hs = Equal.sym(SP.Ent<V>, SP.mk(~V, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), key, v, now), SP.LE{key, v, 1, W.add(now, ST.w64(AR.slots(U32, mT), 4n))}, Equal.cong(Bool, SP.Ent<V>, b => SP.mk_c(~V, ST.w64(AR.slots(U32, mT), 4n), key, v, now, b), U32.is_eq(W32.nth0(AR.slots(U32, mT), 3n), 0), False{}, hc))
32 +g4 = UT.uget(5n, {==}, mT, pm, 4, {==})
33 +g5 = UT.uget(5n, {==}, mT, pm, 5, {==})
34 +e1 = Equal.cong(Array<U32> & U32, Array<U32> & LR.Ent<&2, V>, r => LR.life_lo(&2, V, v, now, r), Array.get(U32, AR.thaw(U32, mT), 4), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 4n)), g4)
35 +e2 = Equal.cong(Array<U32> & U32, Array<U32> & LR.Ent<&2, V>, r => LR.life_hi(&2, V, v, now, W32.nth0(AR.slots(U32, mT), 4n), r), Array.get(U32, AR.thaw(U32, mT), 5), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 5n)), g5)
36 +e3 = Equal.trans(Array<U32> & LR.Ent<&2, V>, LR.entry_of(&2, V, AR.thaw(U32, mT), v, now), LR.ent_if(&2, V, v, now, AR.thaw(U32, mT), True{}), LR.life_hi(&2, V, v, now, W32.nth0(AR.slots(U32, mT), 4n), Array.get(U32, AR.thaw(U32, mT), 5)), e0, e1)
37 ent_d(~V, mT, pm, v, now, key, W.add(now, ST.w64(AR.slots(U32, mT), 4n)), {==}, Equal.trans(Array<U32> & LR.Ent<&2, V>, LR.entry_of(&2, V, AR.thaw(U32, mT), v, now), LR.life_hi(&2, V, v, now, W32.nth0(AR.slots(U32, mT), 4n), Array.get(U32, AR.thaw(U32, mT), 5)), (AR.thaw(U32, mT), LR.ent_dl(&2, V, v, W.add(now, ST.w64(AR.slots(U32, mT), 4n)))), e3, e2), hs)
38
39# THEOREM: entry_of builds an entry whose timing is the specification's mk
40def ent_ok(~V: Data, +mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +v: V, +now: W.U64, +key: String) -> EntOK(~V, mT, pm, v, now, key):
41 +g3 = UT.uget(5n, {==}, mT, pm, 3, {==})
42 +e0 = Equal.cong(Array<U32> & U32, Array<U32> & LR.Ent<&2, V>, r => LR.ent_ttl(&2, V, v, now, r), Array.get(U32, AR.thaw(U32, mT), 3), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 3n)), g3)
43 ent_c(~V, mT, pm, v, now, key, U32.is_eq(W32.nth0(AR.slots(U32, mT), 3n), 0), {==}, e0)