proofs/containers/lru/rebuild.bend checks

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

18 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/hash_table.bend as S
import ../../../spec/containers/lru.bend as SP
import ../../lib/u32div.bend as UD
import ../hash_table/table.bend as TB
import ../hash_table/buckets.bend as B
import ../../../src/containers/hash_table.bend as H
import ./state.bend as ST
import ./lists.bend as LS
import ./trace.bend as TR
import ./unlink.bend as UL
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 subl_refl source · line 26 · raw

@+xs:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(xs, xs) == True{} : Bool}

def subl_ml source · line 33 · raw

@+xs:List<&2, Nat> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(xs, a) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool}

def subl_mr source · line 40 · raw

@+xs:List<&2, Nat> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(xs, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool}

def subl_app source · line 47 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(a, ys) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(b, ys) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), ys) == True{} : Bool}

def bslb_sub source · line 63 · raw

@+sl:List<&2, Nat> -> @+sl2:List<&2, Nat> -> @+ll:List<&2, U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) == True{} : Bool} -> @+sub:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(sl, sl2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl2, ll, b) == True{} : Bool}

def bsl_sub source · line 70 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+sl2:List<&2, Nat> -> @+ll:List<&2, U32> -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) == True{} : Bool} -> @+sub:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(sl, sl2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl2, ll, m) == True{} : Bool}

def tr_eq_bool source · line 77 · raw

@+a:Bool -> @+b:Bool -> @+e:{a == b : Bool} -> @+h:{b == True{} : Bool} -> {a == True{} : Bool}

Templates

template sall_sub source · line 56 · raw

@-V:Data -> @+p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.SP1<V> -> @+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, xs) == True{} : Bool} -> @+sub:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(ys, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, ys) == True{} : Bool}

template good_lk source · line 83 · 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} -> @+head2:U32 -> @+tail2:U32 -> @+lkT2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl2:List<&2, Nat> -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.Tr -> @+hp2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT2) == True{} : Bool} -> @+hs2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT2) == 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} -> @+hin:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trin(tr, sl2) == True{} : Bool} -> @+hseg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT2), sl2, 0, 0) == True{} : Bool} -> @+hh:{U32.is_eq(head2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(sl2, 0)) == True{} : Bool} -> @+ht:{U32.is_eq(tail2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl2, 0)) == True{} : Bool} -> @+hsub:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(sl, sl2) == True{} : Bool} -> @+hsub2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(sl2, sl) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(sl2) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, sl2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, sl) : Nat} -> @+hkeys:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(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), sl2))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head2, tail2, free, mT, k, sd, tabT, ksT, eT, lkT2, sl2, fl}) == True{} : Bool}

THEOREM: re-linking the recency list (a permutation sl2 of sl, link-word writes to its slots) keeps the invariant.