proofs/containers/lru/touchsh.bend checks

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

24 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../lib/list.bend as LL
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../../spec/containers/lru.bend as SP
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ../../../src/containers/lru.bend as LR
import ../hash_table/state.bend as HT
import ./state.bend as ST
import ./trace.bend as TR
import ./unlink.bend as UL
import ./linktail.bend as LT
import ./rebuild.bend as RB
import ./touch.bend as TO
import ./perm.bend as PE
import ../hash_table/insf.bend as IF
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

Definitions

def sd29 source · line 32 · raw

@+k:Nat -> @+sd:Nat -> @+hk:{Nat.is_lt(k, 30n) == True{} : Bool} -> @+hs:{Nat.is_lt(sd, k) == True{} : Bool} -> {Nat.is_lt(3n+sd, 32n) == True{} : Bool}

Templates

template TouchOK source · line 29 · raw

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

template new_nil source · line 37 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+a:List<&2, Nat> -> @+s:Nat -> @+b0:Nat -> @+b2:List<&2, Nat> -> @+su:U32 -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+tail:U32 -> @+ht:{U32.is_eq(tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b0 <> b2), 0)) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(su), tail) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b0 <> b2)) == True{} : Bool} -> @+hbB:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, b0 <> b2) == True{} : Bool} -> Empty

the newest slot has nothing after it

template es_new source · line 48 · 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> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), fl}) == True{} : Bool} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s), key) == True{} : Bool} -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>} -> @+t3:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.Tr -> @+hsT:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t3) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.app(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), tr) : List<&2, U32>} -> @+hlo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trlo(tr) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), [s]), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), free, mT, k, sd, tabT, ksT, eT, t3, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), [s]), fl}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V>}

template tch_l source · line 53 · 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> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), fl}) == True{} : Bool} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s), key) == True{} : Bool} -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>} -> @+tr1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.Tr -> @+t2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hs2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.app(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), tr1) : List<&2, U32>} -> @+l1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trlo(tr1) == True{} : Bool} -> @+i1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trin(tr1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool} -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V> -> @lt:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/linktail.LtOK(V, cap, n, free, mT, tabT, ksT, eT, t2, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), s, r) -> TouchOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, r)

template tch_u source · line 66 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), fl}) == True{} : Bool} -> @+su:U32 -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s), key) == True{} : Bool} -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>} -> @-r1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V> -> @u:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/unlink.UnlOK(V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, r1) -> TouchOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.link_tail(&2, V, r1, su))

template tch_new source · line 83 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), fl}) == True{} : Bool} -> @+su:U32 -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s), key) == True{} : Bool} -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(su), tail) == True{} : Bool} -> TouchOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), fl}))

template tch_c source · line 97 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), fl}) == True{} : Bool} -> @+su:U32 -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s), key) == True{} : Bool} -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>} -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(su), tail) == c : Bool} -> TouchOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.touch_go(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), fl}), su, c))

template touch_sp source · line 105 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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:Nat -> @+su:U32 -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s), key) == True{} : Bool} -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>} -> @sp:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.Split(s, sl) -> TouchOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(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), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.touch(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su))

template touch_sh source · line 113 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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:Nat -> @+hmem:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == True{} : Bool} -> @+su:U32 -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s), key) == True{} : Bool} -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>} -> TouchOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(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), key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.touch(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su))

THEOREM (touch): the listed slot s, holding key with value v, becomes the newest; the model is the specification's drop-and-append of its entry.