~/bend-docscommunity

proofs/containers/lru/unlink.bend checks

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

20 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ../../../src/containers/lru.bend as LR
import ./state.bend as ST
import ./idx.bend as ID
import ./lists.bend as LS
import ./dll.bend as DL
import ./trace.bend as TR
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def sd1 source · line 27 · raw

@+sd:Nat -> @+h:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> {Nat.is_lt(1n+sd, 32n) == True{} : Bool}

def sd3 source · line 30 · raw

@+sd:Nat -> @+h:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> {Nat.is_le(3n+sd, 32n) == True{} : Bool}

def lnk_nz source · line 33 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Nat -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(b), 0) == False{} : Bool}

def ix_o source · line 40 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Nat -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(b))) == b : Nat}

the lk index of word o (< 8) of the slot of b's link

def ix_p source · line 43 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Nat -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(b)))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, 0n) : Nat}

def ix_n source · line 48 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Nat -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(b)))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, 1n) : Nat}

def wr source · line 54 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+i:U32 -> @+b:Nat -> @+o:Nat -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, o) : Nat} -> @+x:U32 -> {Array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), i, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)) : Array<U32>}

a write of word o of slot b (b < 2^sd): the new tree, its slots, its trace

def wr_s source · line 58 · raw

@+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+i:U32 -> @+b:Nat -> @+o:Nat -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, o) : Nat} -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, o), x) : List<&2, U32>}

def len_ll source · line 62 · raw

@+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+b:Nat -> @+o:Nat -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(b, o), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT))) == True{} : Bool}

def Step source · line 67 · raw

@+t0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+xs:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @r:Array<U32> -> Type

def self_in source · line 70 · raw

@+b:Nat -> @+t:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(b, b <> t) == True{} : Bool}

def pick_f source · line 108 · raw

@+c:Bool -> @+h:{c == False{} : Bool} -> @+x:U32 -> @+y:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pick(c, x, y) == y : U32}

Templates

template bnd_of source · line 73 · raw

@-V:Data -> @+x:Nat -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+sd:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, xs) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, xs) == True{} : Bool} -> {Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool}

template ul_q source · line 77 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+p:U32 -> @+s:Nat -> @+b:List<&2, Nat> -> @+hB:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s), 0) == True{} : Bool} -> @+hnB:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(b) == True{} : Bool} -> @+hbB:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, b) == True{} : Bool} -> Step(lkT, sd, b, p, 0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))), p, U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), 0)))

the successor's prev becomes p

template ul_p source · line 91 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+q:U32 -> @+x:U32 -> @+a:List<&2, Nat> -> @+hA:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), a, 0, x) == True{} : Bool} -> @+hnA:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(a) == True{} : Bool} -> @+hbA:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, a) == True{} : Bool} -> Step(lkT, sd, a, 0, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))), q, U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0)))

the predecessor's next becomes q

template hd_ok source · line 111 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+head:U32 -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+hbA:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, a) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pick(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), head) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0) : U32}

template tl_ok source · line 121 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+tail:U32 -> @+ht:{U32.is_eq(tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+hbB:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pick(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), tail) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0) : U32}

template UnlOK source · line 133 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+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> -> @+sd:Nat -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V> -> Type

template f_eq source · line 136 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+h:U32 -> @+h2:U32 -> @+t:U32 -> @+t2:U32 -> @+lk:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @-x:Array<U32> -> @+eh:{h == h2 : U32} -> @+et:{t == t2 : U32} -> @+ex:{x == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lk) : Array<U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, h, t, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), x} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, h2, t2, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lk)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>}

template ul_b source · line 141 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+cap:U32 -> @+n:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+head:U32 -> @+tail:U32 -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool} -> @+hbA:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, a) == True{} : Bool} -> @+hbB:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, b) == True{} : Bool} -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+ht:{U32.is_eq(tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+t1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+tr1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.Tr -> @+ea1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), 0)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t1) : Array<U32>} -> @+hs1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.app(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), tr1) : List<&2, U32>} -> @+hl1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trlo(tr1) == True{} : Bool} -> @+hi1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.trin(tr1, b) == True{} : Bool} -> @+hg1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t1), b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0) == True{} : Bool} -> @st2:Step(t1, sd, a, 0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t1), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0))) -> UnlOK(V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.ul_fin(&2, V, cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))))

template ul_a source · line 154 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+cap:U32 -> @+n:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+fr:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+head:U32 -> @+tail:U32 -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool} -> @+hbA:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, a) == True{} : Bool} -> @+hbB:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.PLive{fr, el}, b) == True{} : Bool} -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+ht:{U32.is_eq(tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+hsA:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), a, 0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s)) == True{} : Bool} -> @st1:Step(lkT, sd, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.set_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), 0))) -> UnlOK(V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.ul_fin(&2, V, cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))))