proofs/containers/lru/gone.bend
bend-collections-laws-containers@1.0.0.0 · 58 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/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/proofs/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
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/lru/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
14
15# gone: the implementation's expiry test of a slot is the specification's
16# test of its entry.
17
18
19def exp_c(+d: W.U64, +now: W.U64, +z: Bool, +hz: {W.is_zero(d) == z : Bool}) -> {LR.expired_choose(d, now, z) == Bool.pick(Bool, z, False{}, W.le_signed(d, now)) : Bool}:
20 match z:
21 case True{}:
22 {==}
23 case False{}:
24 {==}
25
26# the two expiry tests agree
27def exp_eq(+d: W.U64, +now: W.U64) -> {LR.expired(d, now) == SP.expired(d, now) : Bool}:
28 exp_c(d, now, W.is_zero(d), {==})
29
30# a read of word o of slot s
31def rd(+one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +i: U32, +s: Nat, +o: Nat, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hi: {UD.v(i) == ST.off(s, o) : Nat}) -> {Array.get(U32, AR.thaw(U32, lkT), i) == (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, o)) : Array<U32> & U32}:
32 +hl = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(3n+sd)) == True{} : Bool}, ST.off(s, o), UD.v(i), Equal.sym(Nat, UD.v(i), ST.off(s, o), hi), ID.off_lt(s, sd, hs0, o, ho))
33 Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, lkT), i), (AR.thaw(U32, lkT), W32.nth0(AR.slots(U32, lkT), UD.v(i))), (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, o)), UT.uget(3n+sd, hsd, lkT, hpl, i, hl), Equal.cong(Nat, Array<U32> & U32, z => (AR.thaw(U32, lkT), W32.nth0(AR.slots(U32, lkT), z)), UD.v(i), ST.off(s, o), hi))
34
35def su_lt(+su: U32, +s: Nat, +sd: Nat, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}) -> {Nat.is_lt(UD.v(su), SC.pow2(sd)) == True{} : Bool}:
36 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)
37
38def gone_c(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +su: U32, +s: Nat, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +now: W.U64, +kk: String, +vv: V, +c: Bool, +hc: {U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 3n), 0) == c : Bool}) -> {LR.gone_t(su, now, AR.thaw(U32, lkT), Bool.not(c)) == (AR.thaw(U32, lkT), SP.gone(~V, SP.LE{kk, vv, ST.lw(AR.slots(U32, lkT), s, 3n), W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}}, now)) : Array<U32> & Bool}:
39 match c:
40 case True{}:
41 L.subst(Bool, z => {(AR.thaw(U32, lkT), False{}) == (AR.thaw(U32, lkT), Bool.pick(Bool, z, False{}, SP.expired(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now))) : Array<U32> & Bool}, True{}, U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 3n), 0), Equal.sym(Bool, U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 3n), 0), True{}, hc), {==})
42 case False{}:
43 +hsu = su_lt(su, s, sd, hsv, hs0)
44 +i4 = Equal.trans(Nat, UD.v(LR.dlo_idx(su)), ST.off(UD.v(su), 4n), ST.off(s, 4n), ID.w4(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 4n), UD.v(su), s, hsv))
45 +i5 = Equal.trans(Nat, UD.v(LR.dhi_idx(su)), ST.off(UD.v(su), 5n), ST.off(s, 5n), ID.w5(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 5n), UD.v(su), s, hsv))
46 +E1 = Equal.cong(Array<U32> & U32, Array<U32> & Bool, r => LR.gone_lo(su, now, r), Array.get(U32, AR.thaw(U32, lkT), LR.dlo_idx(su)), (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, 4n)), rd(one, h1, lkT, sd, hsd, hpl, LR.dlo_idx(su), s, 4n, {==}, hs0, i4))
47 +E2 = Equal.cong(Array<U32> & U32, Array<U32> & Bool, r => LR.gone_hi(ST.lw(AR.slots(U32, lkT), s, 4n), now, r), Array.get(U32, AR.thaw(U32, lkT), LR.dhi_idx(su)), (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, 5n)), rd(one, h1, lkT, sd, hsd, hpl, LR.dhi_idx(su), s, 5n, {==}, hs0, i5))
48 +E3 = Equal.cong(Bool, Array<U32> & Bool, z => (AR.thaw(U32, lkT), z), LR.expired(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now), SP.expired(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now), exp_eq(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now))
49 +E4 = L.subst(Bool, z => {(AR.thaw(U32, lkT), SP.expired(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now)) == (AR.thaw(U32, lkT), Bool.pick(Bool, z, False{}, SP.expired(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now))) : Array<U32> & Bool}, False{}, U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 3n), 0), Equal.sym(Bool, U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 3n), 0), False{}, hc), {==})
50 Equal.trans(Array<U32> & Bool, LR.gone_lo(su, now, Array.get(U32, AR.thaw(U32, lkT), LR.dlo_idx(su))), LR.gone_lo(su, now, (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, 4n))), (AR.thaw(U32, lkT), SP.gone(~V, SP.LE{kk, vv, ST.lw(AR.slots(U32, lkT), s, 3n), W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}}, now)), E1, Equal.trans(Array<U32> & Bool, LR.gone_hi(ST.lw(AR.slots(U32, lkT), s, 4n), now, Array.get(U32, AR.thaw(U32, lkT), LR.dhi_idx(su))), LR.gone_hi(ST.lw(AR.slots(U32, lkT), s, 4n), now, (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, 5n))), (AR.thaw(U32, lkT), SP.gone(~V, SP.LE{kk, vv, ST.lw(AR.slots(U32, lkT), s, 3n), W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}}, now)), E2, Equal.trans(Array<U32> & Bool, (AR.thaw(U32, lkT), LR.expired(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now)), (AR.thaw(U32, lkT), SP.expired(W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}, now)), (AR.thaw(U32, lkT), SP.gone(~V, SP.LE{kk, vv, ST.lw(AR.slots(U32, lkT), s, 3n), W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}}, now)), E3, E4)))
51
52# THEOREM (gone): the implementation's test of slot s is the specification's
53# test of an entry with s's timing words
54def gone_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +su: U32, +s: Nat, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +now: W.U64, +kk: String, +vv: V) -> {LR.gone(AR.thaw(U32, lkT), su, now) == (AR.thaw(U32, lkT), SP.gone(~V, SP.LE{kk, vv, ST.lw(AR.slots(U32, lkT), s, 3n), W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}}, now)) : Array<U32> & Bool}:
55 +hsu = su_lt(su, s, sd, hsv, hs0)
56 +i3 = Equal.trans(Nat, UD.v(LR.tidx(su)), ST.off(UD.v(su), 3n), ST.off(s, 3n), ID.w3(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 3n), UD.v(su), s, hsv))
57 +E = Equal.cong(Array<U32> & U32, Array<U32> & Bool, r => LR.gone_r(su, now, r), Array.get(U32, AR.thaw(U32, lkT), LR.tidx(su)), (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, 3n)), rd(one, h1, lkT, sd, hsd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3))
58 Equal.trans(Array<U32> & Bool, LR.gone(AR.thaw(U32, lkT), su, now), LR.gone_r(su, now, (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s, 3n))), (AR.thaw(U32, lkT), SP.gone(~V, SP.LE{kk, vv, ST.lw(AR.slots(U32, lkT), s, 3n), W.U64{ST.lw(AR.slots(U32, lkT), s, 4n), ST.lw(AR.slots(U32, lkT), s, 5n)}}, now)), E, gone_c(~V, one, h1, lkT, sd, hsd, hpl, su, s, hsv, hs0, now, kk, vv, U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 3n), 0), {==}))