~/bend-docscommunity

proofs/containers/lru/idx.bend checks

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

12 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 ../../../spec/lib/common.bend as SC
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AT
import ../../lib/u32div.bend as UD
import ../../../src/containers/lru.bend as LR
import ./state.bend as ST
import ../../lib/words32.bend as W32

Definitions

def lt8_ne source · line 19 · raw

@+a:Nat -> @+b:Nat -> @+ha:{Nat.is_lt(a, 8n) == True{} : Bool} -> {Nat.is_eq(a, 8n+b) == False{} : Bool}

def off_ne source · line 22 · raw

@+x:Nat -> @+y:Nat -> @+o:Nat -> @+o2:Nat -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+ho2:{Nat.is_lt(o2, 8n) == True{} : Bool} -> @+h:{Bool.or(Bool.not(Nat.is_eq(x, y)), Bool.not(Nat.is_eq(o, o2))) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(x, o), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o2)) == False{} : Bool}

def av_z source · line 35 · raw

@+u:Nat -> @+s:Nat -> @+e:{Nat.add(u, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, 0n)) == s : Nat} -> {u == s : Nat}

def av_b source · line 38 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+u:Nat -> @+s:Nat -> @+c:Nat -> @+e:{Nat.add(u, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, c)) == s : Nat} -> @+h:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_eq(c, 0n) == b : Bool} -> {u == s : Nat}

def av_c source · line 50 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+u:Nat -> @+s:Nat -> @+c:Nat -> @+e:{Nat.add(u, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, c)) == s : Nat} -> @+h:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {u == s : Nat}

def av_w source · line 53 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Word(32n) -> @+y:Word(32n) -> @+h:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32{x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32{y})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(U32{x}, U32{y})) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32{x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32{y})) : Nat}

def add_val source · line 63 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:U32 -> @+b:U32 -> @+h:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(a, b)) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b)) : Nat}

a + b below 2^32 is exact

def pow_le source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_le(d, 32n) == True{} : Bool} -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, one)) == True{} : Bool}

2^d <= 2^32 for d <= 32

def d8 source · line 76 · raw

@+x:Nat -> Nat

def off_lt source · line 80 · raw

@+s:Nat -> @+sd:Nat -> @+hs:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+o:Nat -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(s, o), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd)) == True{} : Bool}

word o < 8 of a slot below 2^sd lies below 2^(3 + sd)

def shl_v source · line 85 · raw

@+x:U32 -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+v:Nat -> @+ev:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(x) == v : Nat} -> @+h:{Nat.is_lt(Nat.double(v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(x)) == Nat.double(v) : Nat}

def pidx_d8 source · line 90 · raw

@+s:U32 -> @+sd:Nat -> @+hsd:{Nat.is_le(3n+sd, 32n) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(s)) == d8(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s)) : Nat}

pidx s = 8s

def off_sym source · line 101 · raw

@+x:Nat -> @+o:Nat -> {Nat.add(o, d8(x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(x, o) : Nat}

def w0 source · line 104 · raw

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

def w1 source · line 107 · raw

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

def wo source · line 113 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+sd:Nat -> @+hsd:{Nat.is_le(3n+sd, 32n) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+o:U32 -> @+ho:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(o), 8n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.pidx(s), o)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(o)) : Nat}

pidx s + o for a small o

def w2 source · line 119 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+sd:Nat -> @+hsd:{Nat.is_le(3n+sd, 32n) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.hidx(s)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 2n) : Nat}

def w3 source · line 122 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+sd:Nat -> @+hsd:{Nat.is_le(3n+sd, 32n) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.tidx(s)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 3n) : Nat}

def w4 source · line 125 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+sd:Nat -> @+hsd:{Nat.is_le(3n+sd, 32n) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.dlo_idx(s)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 4n) : Nat}

def w5 source · line 128 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+sd:Nat -> @+hsd:{Nat.is_le(3n+sd, 32n) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.dhi_idx(s)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 5n) : Nat}