~/bend-docscommunity

proofs/containers/lru/proof.bend checks

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

17 imports
import Base
import ../../../spec/containers/lru.bend as SP
import ../../../spec/lib/common.bend as SC
import ../../lib/array.bend as AR
import ../../../src/math/u64.bend as W
import ../../../src/containers/lru.bend as LR
import ./state.bend as ST
import ./new.bend as NW
import ./basic.bend as BA
import ./rmat.bend as RM
import ./read.bend as RD
import ./contains.bend as CT
import ./add.bend as AD
import ./remove.bend as RV
import ./resize.bend as RZ
import ./purge.bend as PU
import ./keys.bend as KY

Templates

template new_ok source · line 58 · raw

@-V:Data -> @+cap:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/new.MadeOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.new(&2, V, cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.new(V, cap))

template capacity_ok source · line 61 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.capacity(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.capacity(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>, U32)}

template len_ok source · line 64 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.len(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.len(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>, U32)}

template counters_ok source · line 67 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.counters(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/basic.mtree(V, sh))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>, Array<U32>)}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/basic.mtree(V, sh))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.counters(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr})

template set_lifetime_ok source · line 70 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/basic.SetOK(V, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.set_lifetime(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), ns), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_lifetime_packed(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), ns))

template get_ok source · line 73 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.get(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), key, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.get(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), key, now))

template peek_ok source · line 76 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.peek(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), key, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.peek(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), key, now))

template contains_ok source · line 79 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.contains(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), key, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.contains(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), key, now))

template add_ok source · line 82 · raw

@-V:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+hcap:{Nat.is_le(Nat.double(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lru_es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.add(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), key, v, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.add(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), key, v, now))

template remove_ok source · line 85 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.remove(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.remove(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), key))

template resize_ok source · line 88 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+cap2:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Result<&2, &2, String, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.resize(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), cap2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.resize(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), cap2))

template purge_ok source · line 91 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.purge(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.purge(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh)))

template keys_ok source · line 94 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, List<&2, String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), now))

template lg_snoc source · line 100 · raw

@-V:Data -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.last_go(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, t, e), h) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

---- list facts ----

template snoc_last source · line 108 · raw

@-V:Data -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.last(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, es, e)) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

the appended entry is the newest (the SP.last of the recency order)

template snoc_length source · line 115 · raw

@-V:Data -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, es, e)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, es) : Nat}

template new_empty source · line 123 · raw

@-V:Data -> @+cap:U32 -> @+hz:{U32.is_eq(cap, 0) == False{} : Bool} -> @+hm:{U32.is_eq(cap, 4294967295) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Empty_Map.new_empty(V, cap, hz, hm)

---- Empty_Map, Length, Capacity ----

template new_rejects_zero source · line 128 · raw

@-V:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Empty_Map.new_rejects_zero(V)

template new_rejects_max source · line 131 · raw

@-V:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Empty_Map.new_rejects_max(V)

template length_value source · line 134 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Length.length_value(V, cap, on, life, es, c)

template capacity_value source · line 137 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Capacity.capacity_value(V, cap, on, life, es, c)

template add_present_order source · line 142 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+old:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{old} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_present_order(V, cap, on, life, es, c, key, v, now, old, hf)

---- Include (add) ---- a present key: its old entry is dropped and the new one is the newest

template add_present_newest source · line 146 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+old:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{old} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_present_newest(V, cap, on, life, es, c, key, v, now, old, hf)

template add_present_length source · line 150 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+old:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{old} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_present_length(V, cap, on, life, es, c, key, v, now, old, hf)

template add_room_order source · line 155 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hr:{U32.is_le(cap, U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, es))) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_room_order(V, cap, on, life, es, c, key, v, now, hf, hr)

an absent key with room: appended as the newest, nothing evicted

template add_room_newest source · line 160 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hr:{U32.is_le(cap, U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, es))) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_room_newest(V, cap, on, life, es, c, key, v, now, hf, hr)

template add_room_length source · line 164 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hr:{U32.is_le(cap, U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, es))) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_room_length(V, cap, on, life, es, c, key, v, now, hf, hr)

template add_evict_order source · line 169 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hfu:{U32.is_le(cap, U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, es))) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_evict_order(V, cap, on, life, es, c, key, v, now, hf, hfu)

an absent key when full: the oldest is evicted (reported), the new one is newest

template add_evict_newest source · line 174 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hfu:{U32.is_le(cap, U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, es))) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_evict_newest(V, cap, on, life, es, c, key, v, now, hf, hfu)

template add_evict_length source · line 179 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, h <> t, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hfu:{U32.is_le(cap, U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, h <> t))) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Include.add_evict_length(V, cap, on, life, h, t, c, key, v, now, hf, hfu)

eviction keeps the length (the cache holds at least the evicted entry)

template get_hit source · line 185 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, e, now) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Element.get_hit(V, cap, on, life, es, c, key, now, e, hf, hg)

---- Element: get (touches) and peek (does not) ---- a live hit returns the value and makes the key the newest

template get_hit_newest source · line 190 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, e, now) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Element.get_hit_newest(V, cap, on, life, es, c, key, now, e, hf, hg)

template get_miss source · line 195 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Element.get_miss(V, cap, on, life, es, c, key, now, hf)

a miss leaves the entries unchanged and reads as absent

template read_expired source · line 200 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+tracked:Bool -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, e, now) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Iter_Model.read_expired(V, cap, on, life, es, c, key, now, tracked, e, hf, hg)

an expired entry reads as absent and is removed

template peek_hit source · line 206 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, e, now) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Element.peek_hit(V, cap, on, life, es, c, key, now, e, hf, hg)

peek: a live hit returns the value and changes nothing

template peek_miss source · line 211 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Element.peek_miss(V, cap, on, life, es, c, key, now, hf)

template contains_live source · line 216 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, e, now) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Contains.contains_live(V, cap, on, life, es, c, key, now, e, hf, hg)

---- Contains ----

template contains_expired source · line 221 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, e, now) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Contains.contains_expired(V, cap, on, life, es, c, key, now, e, hf, hg)

template contains_absent source · line 226 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Contains.contains_absent(V, cap, on, life, es, c, key, now, hf)

template remove_present source · line 231 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Delete.remove_present(V, cap, on, life, es, c, key, e, hf)

---- Delete / Exclude (remove), Clear (purge), Iter_Model (keys) ----

template remove_absent source · line 235 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+key:String -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, es, key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Delete.remove_absent(V, cap, on, life, es, c, key, hf)

template purge_value source · line 239 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Clear.purge_value(V, cap, on, life, es, c)

template keys_fin_value source · line 242 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Iter_Model.keys_fin_value(V, cap, on, life, es, c)