~/bend-docscommunity

proofs/containers/lru/dll.bend checks

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

16 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/table.bend as TB
import ../hash_table/buckets.bend as B
import ../hash_table/state.bend as HT
import ./state.bend as ST
import ./idx.bend as ID
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

Definitions

def lw_same source · line 33 · raw

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

def lw_other source · line 36 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+x:Nat -> @+o2:Nat -> @+ho2:{Nat.is_lt(o2, 8n) == True{} : Bool} -> @+hne:{Bool.or(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2))) == 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 ne_slot source · line 39 · raw

@+y:Nat -> @+x:Nat -> @+o:Nat -> @+o2:Nat -> @+h:{Nat.is_eq(y, x) == False{} : Bool} -> {Bool.or(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2))) == True{} : Bool}

def ne_word source · line 42 · raw

@+y:Nat -> @+x:Nat -> @+o:Nat -> @+o2:Nat -> @+h:{Nat.is_eq(o, o2) == False{} : Bool} -> {Bool.or(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2))) == True{} : Bool}

def lo_hi source · line 46 · raw

@+o:Nat -> @+h01:{Nat.is_lt(o, 2n) == True{} : Bool} -> @+o2:Nat -> @+h2:{Nat.is_le(2n, o2) == True{} : Bool} -> {Nat.is_eq(o, o2) == False{} : Bool}

a link word (o < 2) is not a data word (2 <= o2)

def seg_c source · line 53 · raw

@+l1:List<&2, U32> -> @+l2:List<&2, U32> -> @+s:Nat -> @+t:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(l1, s, 0n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(l2, s, 0n) : U32} -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(l1, s, 1n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(l2, s, 1n) : U32} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(l1, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(l2, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), q) : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(l1, s <> t, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(l2, s <> t, p, q) : Bool}

def seg_fs source · line 59 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, sl) == False{} : Bool} -> {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}

a write to a slot off the segment leaves it

def seg_app source · line 70 · raw

@+ll:List<&2, U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), p, q) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, a, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, p), q)) : Bool}

a segment splits at an append

def segq source · line 91 · raw

@+ll:List<&2, U32> -> @+t:List<&2, Nat> -> @+a:Nat -> @+p:U32 -> @+x:U32 -> @+y:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, a <> t, p, x) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(a <> t) == True{} : Bool} -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.lastn(t, a), 1n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.lastn(t, a), 1n), y), a <> t, p, y) == True{} : Bool}

re-target the last slot's next

def segp source · line 114 · raw

@+ll:List<&2, U32> -> @+b:Nat -> @+t:List<&2, Nat> -> @+x:U32 -> @+q:U32 -> @+y:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, b <> t, x, q) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(b <> t) == True{} : Bool} -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, 0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, 0n), y), b <> t, y, q) == True{} : Bool}

re-target the first slot's prev

def fll_fs source · line 127 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+fl:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, fl) == False{} : Bool} -> {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 lw_hi source · line 141 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h01:{Nat.is_lt(o, 2n) == True{} : Bool} -> @+x:Nat -> @+o2:Nat -> @+ho2:{Nat.is_lt(o2, 8n) == True{} : Bool} -> @+h2:{Nat.is_le(2n, o2) == 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 skey_fr source · line 144 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h01:{Nat.is_lt(o, 2n) == 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_fr source · line 175 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h01:{Nat.is_lt(o, 2n) == 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_fr source · line 182 · raw

@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h01:{Nat.is_lt(o, 2n) == 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}

Templates

template sent_fr source · line 147 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h01:{Nat.is_lt(o, 2n) == True{} : Bool} -> @+kl:List<&2, String> -> @+x:Nat -> @+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_fr source · line 158 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h01:{Nat.is_lt(o, 2n) == True{} : Bool} -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+sl:List<&2, Nat> -> {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, sl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template has_fr source · line 167 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+h01:{Nat.is_lt(o, 2n) == 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}