1 import Base 2 import ../../lib/logic.bend as L 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 ../../lib/u32div.bend as UD 7 import ../../../src/math/u64.bend as W 8 import ../../../src/containers/lru.bend as LR 9 import ./state.bend as ST 10 import ./idx.bend as ID 11 import ./unlink.bend as UL 12 import ../../lib/words32.bend as W32 13 import ../../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 19 def 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 27 def 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 31 def rd(+one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree, +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}: 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, 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, z => (AR.thaw(U32, lkT), W32.nth0(AR.slots(U32, lkT), z)), UD.v(i), ST.off(s, o), hi)) 34 35 def 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 38 def gone_c(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree, +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 & 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 & 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, Array & 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, Array & 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 & 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 & 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 & 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 & 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 & 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 54 def gone_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree, +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 & 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, Array & 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 & 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), {==}))