~/bend-docscommunity

proofs/containers/lru/gone.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/gone.bend as Gone

13 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/lru.bend as SP
import ../../lib/u32div.bend as UD
import ../../../src/math/u64.bend as W
import ../../../src/containers/lru.bend as LR
import ./state.bend as ST
import ./idx.bend as ID
import ./unlink.bend as UL
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def exp_c source · line 19 · raw

@+d:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+z:Bool -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.is_zero(d) == z : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.expired_choose(d, now, z) == Bool.pick(Bool, z, False{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.le_signed(d, now)) : Bool}

def exp_eq source · line 27 · raw

@+d:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.expired(d, now) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expired(d, now) : Bool}

the two expiry tests agree

def rd source · line 31 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(s, o) : Nat} -> {Array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, o)) : Pair(Array<U32>, U32)}

a read of word o of slot s

def su_lt source · line 35 · raw

@+su:U32 -> @+s:Nat -> @+sd:Nat -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool}

Templates

template gone_c source · line 38 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+su:U32 -> @+s:Nat -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+kk:String -> @+vv:V -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, 3n), 0) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.gone_t(su, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), Bool.not(c)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.LE{kk, vv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, 5n)}}, now)) : Pair(Array<U32>, Bool)}

template gone_ok source · line 54 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+su:U32 -> @+s:Nat -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+kk:String -> @+vv:V -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.gone(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), su, now) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.LE{kk, vv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s, 5n)}}, now)) : Pair(Array<U32>, Bool)}

THEOREM (gone): the implementation's test of slot s is the specification's test of an entry with s's timing words