proofs/containers/lru/walk.bend checks

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

23 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
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/hash_table.bend as H
import ../../../src/containers/lru.bend as LR
import ../hash_table/table.bend as TB
import ../hash_table/state.bend as HT
import ../hash_table/keysw.bend as KW
import ../hash_table/strings.bend as STR
import ../hash_table/arena.bend as AN
import ./state.bend as ST
import ./unlink.bend as UL
import ./gone.bend as GO
import ./idx.bend as ID
import ./touch.bend as TO
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK

Definitions

def mapk source · line 43 · raw

@+ll:List<&2, U32> -> @+kl:List<&2, String> -> @l:List<&2, Nat> -> List<&2, String>

the keys of the slots of l

def racc source · line 51 · raw

@+ll:List<&2, U32> -> @+kl:List<&2, String> -> @back:List<&2, Nat> -> @acc:List<&2, String> -> List<&2, String>

the keys of the slots of back prepended to acc, one by one

def rok source · line 59 · raw

@+ll:List<&2, U32> -> @back:List<&2, Nat> -> @+fr:Nat -> Bool

every slot of back is below fr and its prev is the next slot of back

def ra_rapp source · line 66 · raw

@+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+l:List<&2, Nat> -> @+b:List<&2, Nat> -> @+acc:List<&2, String> -> {racc(ll, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.rapp(l, b), acc) == racc(ll, kl, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, mapk(ll, kl, l), acc)) : List<&2, String>}

def lo_idem source · line 75 · raw

@+l:List<&2, Nat> -> @+p:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(l, p)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(l, p) : U32}

def fo_of source · line 82 · raw

@+r:List<&2, Nat> -> @+a:U32 -> @+h:{U32.is_eq(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(r, 0)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(r, a) == a : U32}

def WSt source · line 126 · raw

@+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+sd:Nat -> @+x:Nat -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> Type

def ws_e1 source · line 129 · 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} -> @+kl:List<&2, String> -> @+x:Nat -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hs0:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.wk_step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.WK{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, KT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(x)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.wk_word(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, KT), acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 2n))) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.Walk}

def ws_r0 source · line 133 · 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} -> @+kl:List<&2, String> -> @+x:Nat -> @+hs0:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {Array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(x)))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 0n)) : Pair(Array<U32>, U32)}

def ws_sh source · line 138 · 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} -> @+kl:List<&2, String> -> @+x:Nat -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hs0:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 2n)) == True{} : Bool} -> WSt(lkT, kl, sd, x, acc, KT)

def ws_lg source · line 148 · 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} -> @+kl:List<&2, String> -> @+x:Nat -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hs0:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 2n)) == False{} : Bool} -> WSt(lkT, kl, sd, x, acc, KT)

def ws_d source · line 175 · 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} -> @+kl:List<&2, String> -> @+x:Nat -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hs0:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+d:Bool -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 2n)) == d : Bool} -> WSt(lkT, kl, sd, x, acc, KT)

def wstep source · line 183 · 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} -> @+kl:List<&2, String> -> @+x:Nat -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hs0:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> WSt(lkT, kl, sd, x, acc, KT)

THEOREM: one step of the walk prepends the slot's key and moves to its prev

def WOK source · line 188 · raw

@+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+sd:Nat -> @+back:List<&2, Nat> -> @+acc:List<&2, String> -> @+at:U32 -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> Type

def wl_2 source · line 191 · raw

@+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+sd:Nat -> @+x:Nat -> @+r:List<&2, Nat> -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.wk_step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.WK{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, KT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(x)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.WK{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), kl, x) <> acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 0n)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.Walk} -> @wo:WOK(lkT, kl, sd, r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), kl, x) <> acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 0n), K2) -> WOK(lkT, kl, sd, x <> r, acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(x), KT)

def wl_1 source · line 198 · raw

@+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+sd:Nat -> @+x:Nat -> @+r:List<&2, Nat> -> @+acc:List<&2, String> -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @st:WSt(lkT, kl, sd, x, acc, KT) -> @rec:(@+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hs2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == kl : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> WOK(lkT, kl, sd, r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), kl, x) <> acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), x, 0n), K2)) -> WOK(lkT, kl, sd, x <> r, acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(x), KT)

def walk source · line 205 · 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} -> @+kl:List<&2, String> -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+back:List<&2, Nat> -> @+acc:List<&2, String> -> @+at:U32 -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hr:{rok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), back, fr) == True{} : Bool} -> @+hat:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(back, at) == at : U32} -> WOK(lkT, kl, sd, back, acc, at, KT)

THEOREM: the walk from the first slot of back, for its length, prepends the keys of back one by one and keeps ks

Templates

template some_v source · line 33 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+m:Maybe<&2, V> -> @+hmm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == m : Maybe<&2, V>} -> @+hsm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> Sigma<&1, &1, V, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>}>

the value of a live slot

template rok_app source · line 90 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+el:List<&2, Maybe<&2, V>> -> @+l:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fr:Nat -> @+p:U32 -> @+q:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, l, p, q) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, l, fr, el) == True{} : Bool} -> @+hb:{rok(ll, b, fr) == True{} : Bool} -> @+hp:{U32.is_eq(p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)) == True{} : Bool} -> {rok(ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.rapp(l, b), fr) == True{} : Bool}

the list sl, reversed, keeps its links backwards

template km_v source · line 105 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+t:List<&2, Nat> -> @pv:Sigma<&1, &1, V, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>}> -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t)) == mapk(ll, kl, t) : List<&2, String>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, s <> t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s) <> mapk(ll, kl, t) : List<&2, String>}

template km source · line 114 · 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.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl)) == mapk(ll, kl, sl) : List<&2, String>}

the keys of live slots are the model's keys