~/bend-docscommunity

proofs/containers/lru/perm.bend checks

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

16 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../../spec/containers/lru.bend as SP
import ../hash_table/state.bend as HT
import ../hash_table/insf.bend as IF
import ./state.bend as ST
import ./lists.bend as LS
import ./trace.bend as TR
import ./unlink.bend as UL
import ./rebuild.bend as RB
import ./touch.bend as TO
import ../../lib/nat_list.bend as NL

Definitions

def sub_xt source · line 22 · raw

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

def sub_tx source · line 27 · raw

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

def trin_sub source · line 31 · raw

@+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.Tr -> @+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trin(tr, xs) == True{} : Bool} -> @+sub:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.subl(xs, ys) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trin(tr, ys) == True{} : Bool}

def nd_snoc source · line 39 · raw

@+x:List<&2, Nat> -> @+s:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, [s])) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(x), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, x))) : Bool}

x ++ [s]: duplicate-free when x is and s is not in it

def nd_xt source · line 44 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), [s])) == True{} : Bool}

def len_xt source · line 47 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), [s])) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) : Nat}

def nd_snoc_s source · line 63 · raw

@+x:List<&2, String> -> @+k:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, x, [k])) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(x), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(k, x))) : Bool}

Templates

template keys_x source · line 54 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, a)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, b))) : List<&2, String>}

template keys_t source · line 58 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), [s]))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, a)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, b))), [0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s)]) : List<&2, String>}

template keys_xt source · line 66 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), [s])))) == True{} : Bool}