proofs/containers/lru/linktail.bend checks

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

18 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 ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ../../../src/containers/lru.bend as LR
import ../hash_table/probe_impl.bend as PI
import ./state.bend as ST
import ./idx.bend as ID
import ./dll.bend as DL
import ./trace.bend as TR
import ./unlink.bend as UL
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/u32_tree.bend as UT

Definitions

def tr_single source · line 27 · raw

@+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.Tr -> @+xs:List<&2, Nat> -> @+s:Nat -> @+hin:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trin(tr, xs) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trout(tr, [s]) == True{} : Bool}

the written slots are all in xs, s is not: s is not written

def lnk_su source · line 72 · raw

@+su:U32 -> @+s:Nat -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(su) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s) : U32}

a slot's U32 is the U32 of its number

Templates

template LtOK source · line 23 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+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> -> @+sd:Nat -> @+sl:List<&2, Nat> -> @+s:Nat -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V> -> Type

template hd2 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} -> @+sl:List<&2, Nat> -> @+s:Nat -> @+head:U32 -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(sl, 0)) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pick(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), head) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, sl, [s]), 0) : U32}

template lt_fin source · line 48 · raw

@-V:Data -> @+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} -> @+cap:U32 -> @+n:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+head:U32 -> @+su:U32 -> @+s:Nat -> @+sl:List<&2, Nat> -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == False{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(sl) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, sl) == True{} : Bool} -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(sl, 0)) == True{} : Bool} -> @+hp2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(su)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(su)), 0)) == True{} : Bool} -> @+hs2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(su)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(su)), 0)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(s, 0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(s, 1n), 0) : List<&2, U32>} -> @+hg2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(su)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(su)), 0)), sl, 0, 0) == True{} : Bool} -> @st:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/unlink.Step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(su)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(su)), 0), sd, sl, 0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(su)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(su)), 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0), 0))) -> LtOK(V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, sl, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pick(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), head), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(su)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(su)), 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0), 0))})

template link_tail_ok source · line 80 · raw

@-V:Data -> @+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} -> @+cap:U32 -> @+n:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+head:U32 -> @+tail:U32 -> @+su:U32 -> @+s:Nat -> @+sl:List<&2, Nat> -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == False{} : Bool} -> @+hseg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), sl, 0, 0) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(sl) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, sl) == True{} : Bool} -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(sl, 0)) == True{} : Bool} -> @+ht:{U32.is_eq(tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0)) == True{} : Bool} -> LtOK(V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, sl, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.link_tail(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 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)}, su))

THEOREM (link_tail): a slot s off the recency list sl becomes its newest: the list sl ++ [s] is linked, with its head and tail.