proofs/containers/lru/meta.bend checks

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

8 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ./state.bend as ST
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def uset source · line 19 · raw

@+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:U32 -> Pair({Array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t), i, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)) : Array<U32>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x) : List<&2, U32>}))

a U32 array write: the new tree, still perfect, with its slots updated

def nth_other source · line 23 · raw

@+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+i:Nat -> @+x:U32 -> @+t2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t), i, x) : List<&2, U32>} -> @+j:Nat -> @+hne:{Nat.is_eq(i, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t2), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t), j) : U32}

nth0 after an update elsewhere, and at the update

def nth_same source · line 26 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:U32 -> @+t2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t), i, x) : List<&2, U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t2), i) == x : U32}

Templates

template good_m source · line 31 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+mT2: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} -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT2), 0n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 0n) : U32} -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT2), 1n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 1n) : U32} -> @+e2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT2), 2n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 2n) : U32} -> @+e6:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT2), 6n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 6n) : U32} -> @+e7:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT2), 7n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 7n) : U32} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT2, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}