~/bend-docscommunity

proofs/containers/lru/basic.bend checks

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

16 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
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 ../hash_table/state.bend as HT
import ../hash_table/probe_impl.bend as PI
import ./state.bend as ST
import ./meta.bend as MT
import ../hash_table/get.bend as G
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def ct5 source · line 80 · raw

@+a1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+a2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+a3:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+a4:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+a5:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+b1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+b2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+b3:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+b4:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+b5:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e1:{a1 == b1 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64} -> @+e2:{a2 == b2 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64} -> @+e3:{a3 == b3 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64} -> @+e4:{a4 == b4 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64} -> @+e5:{a5 == b5 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.CT{a1, a2, a3, a4, a5} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.CT{b1, b2, b3, b4, b5} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr}

def w64_eq source · line 87 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+i:Nat -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, i) : U32} -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 1n+i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 1n+i) : U32} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(a, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(b, i) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64}

def ctr_eq source · line 92 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+e16:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 16n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 16n) : U32} -> @+e17:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 17n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 17n) : U32} -> @+e18:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 18n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 18n) : U32} -> @+e19:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 19n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 19n) : U32} -> @+e20:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 20n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 20n) : U32} -> @+e21:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 21n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 21n) : U32} -> @+e22:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 22n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 22n) : U32} -> @+e23:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 23n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 23n) : U32} -> @+e24:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 24n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 24n) : U32} -> @+e25:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 25n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(b, 25n) : U32} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr}

the counters of two meta word lists that agree on words 16 .. 25

def w64_eq_l source · line 95 · raw

@+a:List<&2, U32> -> @+i:Nat -> @+lo:U32 -> @+hi:U32 -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, i) == lo : U32} -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(a, 1n+i) == hi : U32} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(a, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64{lo, hi} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64}

def oth3 source · line 113 · raw

@+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+on:U32 -> @+lo:U32 -> @+hi:U32 -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, mT, 3n, on)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n, on) : List<&2, U32>} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, mT, 3n, on), 4n, lo)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, mT, 3n, on)), 4n, lo) : List<&2, U32>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, mT, 3n, on), 4n, lo), 5n, hi)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, mT, 3n, on), 4n, lo)), 5n, hi) : List<&2, U32>} -> @+j:Nat -> @+n3:{Nat.is_eq(3n, j) == False{} : Bool} -> @+n4:{Nat.is_eq(4n, j) == False{} : Bool} -> @+n5:{Nat.is_eq(5n, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, mT, 3n, on), 4n, lo), 5n, hi)), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), j) : U32}

word j of the meta list after the three lifetime writes, j not 3, 4, 5

Templates

template es_len_m source · line 23 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+s:Nat -> @+m:Maybe<&2, V> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> @+r:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+t:List<&2, Nat> -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, t) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, s, m), r)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, t) : Nat}

template es_len source · line 31 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+fr:Nat -> @+sl:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, sl, fr, el) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, sl) : Nat}

every slot live: one entry per slot

template len_model source · line 41 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n) : Nat}

the model's length is the count n

template n_lt source · line 45 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool}

n is below 2^k

template capacity_ok source · line 51 · 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)}

THEOREM: capacity is the specification's; the cache is unchanged.

template len_ok source · line 57 · 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)}

THEOREM: len is the specification's; the cache is unchanged.

template mtree source · line 65 · raw

@-V:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>

template counters_ok source · line 72 · 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, 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, mtree(V, sh))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.counters(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr})

THEOREM: counters hands back the cache and a copy of the meta words, whose counter words are the specification's counters.

template lru_eq source · line 100 · raw

@-V:Data -> @+cap:U32 -> @+a:U32 -> @+a2:U32 -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+b2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+es2:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+c2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr -> @+ea:{a == a2 : U32} -> @+eb:{b == b2 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64} -> @+ee:{es == es2 : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> @+ec:{c == c2 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, a, b, es, c} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, a2, b2, es2, c2} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V>}

the model's fields

template SetOK source · line 109 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+spec:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V> -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V> -> Type

template sl_go source · line 117 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+on:U32 -> SetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, on, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_life(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), s, on), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT)})

template set_lifetime_ok source · line 143 · 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 -> 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))

THEOREM: set_lifetime is the specification's; the invariant is kept.