proofs/containers/lru/trace.bend checks

type Tr source · line 16 · raw

Data

• TNil

  Tr

• TW

  @y:Nat -> @o:Nat -> @v:U32 -> @t:Tr -> Tr

def app source · line 21 · raw

@+ll:List<&2, U32> -> @tr:Tr -> List<&2, U32>

def trlo source · line 29 · raw

@tr:Tr -> Bool

def trin source · line 37 · raw

@tr:Tr -> @+xs:List<&2, Nat> -> Bool

def trout source · line 44 · raw

@tr:Tr -> @+xs:List<&2, Nat> -> Bool

def tcat source · line 52 · raw

@a:Tr -> @b:Tr -> Tr

def app_cat source · line 59 · raw

@+ll:List<&2, U32> -> @+a:Tr -> @+b:Tr -> {app(ll, tcat(a, b)) == app(app(ll, b), a) : List<&2, U32>}

def lo_cat source · line 67 · raw

@+a:Tr -> @+b:Tr -> @+ha:{trlo(a) == True{} : Bool} -> @+hb:{trlo(b) == True{} : Bool} -> {trlo(tcat(a, b)) == True{} : Bool}

def in_cat source · line 74 · raw

@+a:Tr -> @+b:Tr -> @+xs:List<&2, Nat> -> @+ha:{trin(a, xs) == True{} : Bool} -> @+hb:{trin(b, xs) == True{} : Bool} -> {trin(tcat(a, b), xs) == True{} : Bool}

def lt8 source · line 81 · raw

@+o:Nat -> @+h:{Nat.is_lt(o, 2n) == True{} : Bool} -> {Nat.is_lt(o, 8n) == True{} : Bool}

def len_tr source · line 86 · raw

@+ll:List<&2, U32> -> @+tr:Tr -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, app(ll, tr)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) : Nat}

def bsl_tr source · line 109 · raw

@+ll:List<&2, U32> -> @+tr:Tr -> @+h:{trlo(tr) == 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, app(ll, tr), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) : Bool}

def fll_tr source · line 117 · raw

@+ll:List<&2, U32> -> @+tr:Tr -> @+h:{trlo(tr) == True{} : Bool} -> @+fl:List<&2, Nat> -> @+hout:{trout(tr, fl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.fll(app(ll, tr), fl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.fll(ll, fl) : Bool}

def seg_tr source · line 126 · raw

@+ll:List<&2, U32> -> @+tr:Tr -> @+h:{trlo(tr) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+hout:{trout(tr, sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(app(ll, tr), sl, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, sl, p, q) : Bool}

def lw_tr source · line 136 · raw

@+ll:List<&2, U32> -> @+tr:Tr -> @+h:{trlo(tr) == True{} : Bool} -> @+x:Nat -> @+o2:Nat -> @+ho2:{Nat.is_lt(o2, 8n) == True{} : Bool} -> @+hout:{trout(tr, [x]) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(app(ll, tr), x, o2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, x, o2) : U32}

def lw_tr_hi source · line 146 · raw

@+ll:List<&2, U32> -> @+tr:Tr -> @+h:{trlo(tr) == 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(app(ll, tr), x, o2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, x, o2) : U32}

def trin_r source · line 176 · raw

@+tr:Tr -> @+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{trin(tr, x) == True{} : Bool} -> {trin(tr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool}

def trin_l source · line 183 · raw

@+tr:Tr -> @+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{trin(tr, a) == True{} : Bool} -> {trin(tr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool}

def trin_cons source · line 190 · raw

@+tr:Tr -> @+s:Nat -> @+x:List<&2, Nat> -> @+h:{trin(tr, x) == True{} : Bool} -> {trin(tr, s <> x) == True{} : Bool}

def trout_r source · line 198 · raw

@+tr:Tr -> @+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+hin:{trin(tr, a) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool} -> {trout(tr, x) == True{} : Bool}

def trout_l source · line 206 · raw

@+tr:Tr -> @+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+hin:{trin(tr, x) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool} -> {trout(tr, a) == True{} : Bool}

def trout_tail source · line 213 · raw

@+tr:Tr -> @+s:Nat -> @+x:List<&2, Nat> -> @+h:{trout(tr, s <> x) == True{} : Bool} -> {trout(tr, x) == True{} : Bool}

template es_tr source · line 93 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+tr:Tr -> @+h:{trlo(tr) == True{} : Bool} -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+sl:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, app(ll, tr), kl, el, sl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template has_tr source · line 101 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+tr:Tr -> @+h:{trlo(tr) == 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, app(ll, tr), sl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, ll, sl) : Bool}

template not_vac source · line 154 · raw

@-V:Data -> @+y:Nat -> @+fl:List<&2, Nat> -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, y) == True{} : Bool} -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.flok(V, fl, fr, el) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, fl) == c : Bool} -> {Bool.not(c) == True{} : Bool}

template out_of_in source · line 163 · raw

@-V:Data -> @+tr:Tr -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hin:{trin(tr, sl) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, sl, fr, el) == True{} : Bool} -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.flok(V, fl, fr, el) == True{} : Bool} -> {trout(tr, fl) == True{} : Bool}