proofs/containers/lru/hw.bend checks

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

18 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
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 ../hash_table/buckets.bend as B
import ../hash_table/state.bend as HT
import ../hash_table/table.bend as TB
import ../hash_table/tools.bend as TL
import ./state.bend as ST
import ./dll.bend as DL
import ./elfr.bend as EF
import ./walk.bend as WL
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK

Definitions

def ne_hi source · line 24 · raw

@+o2:Nat -> @+o:Nat -> @+h:{Nat.is_lt(o2, 3n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> {Nat.is_eq(o, o2) == False{} : Bool}

def lw_lo3 source · line 27 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+x:Nat -> @+o2:Nat -> @+ho2:{Nat.is_lt(o2, 8n) == True{} : Bool} -> @+h:{Nat.is_lt(o2, 3n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), x, o2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, x, o2) : U32}

def seg_hw source · line 30 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), sl, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, sl, p, q) : Bool}

def fll_hw source · line 37 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+fl:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), fl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.fll(ll, fl) : Bool}

def skey_hw source · line 47 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+kl:List<&2, String> -> @+x:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), kl, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, x) : String}

def bslb_hw source · line 58 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) : Bool}

def bsl_hw source · line 65 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) : Bool}

def mapk_hw source · line 72 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+kl:List<&2, String> -> @+xs:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/walk.mapk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), kl, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/walk.mapk(ll, kl, xs) : List<&2, String>}

Templates

template has_hw source · line 50 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h3:{Nat.is_le(3n, o) == True{} : Bool} -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+sl:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), sl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, ll, sl) : Bool}

template live_same source · line 83 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+y:Nat -> @+w:V -> @+hlen:{Nat.is_lt(y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, el)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, Some{w}), y) == True{} : Bool}

the written slot is live

template sl_c source · line 86 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+y:Nat -> @+w:V -> @+fr:Nat -> @+x:Nat -> @+t:List<&2, Nat> -> @+hlen:{Nat.is_lt(y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, el)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, x <> t, fr, el) == True{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, t, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, Some{w})) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(y, x) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, x <> t, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, Some{w})) == True{} : Bool}

template slok_live source · line 102 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+y:Nat -> @+w:V -> @+fr:Nat -> @+xs:List<&2, Nat> -> @+hlen:{Nat.is_lt(y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, el)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, el) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, Some{w})) == True{} : Bool}

a value written anywhere keeps every listed slot live

template sent_fs source · line 112 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+kl:List<&2, String> -> @+x:Nat -> @+hyx:{Nat.is_eq(y, x) == False{} : Bool} -> @+m:Maybe<&2, V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), kl, x, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, x, m) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template es_fs source · line 125 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+xs:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), kl, el, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, xs) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

a write to a slot off xs leaves the entries of xs