~/bend-docscommunity

proofs/containers/lru/bump.bend checks

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

15 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
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/lru.bend as LR
import ./state.bend as ST
import ./meta.bend as MT
import ./basic.bend as BA
import ../../lib/list.bend as LL
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def BumpOK source · line 20 · raw

@+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+i:Nat -> @r:Array<U32> -> Type

def lt_i source · line 24 · raw

@+i:Nat -> @+hi:{Nat.is_lt(1n+i, 32n) == True{} : Bool} -> {Nat.is_lt(i, 32n) == True{} : Bool}

def vlt source · line 27 · raw

@+x:U32 -> @+i:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(x) == i : Nat} -> @+hi:{Nat.is_lt(i, 32n) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(5n)) == True{} : Bool}

def ne_si source · line 30 · raw

@+i:Nat -> {Nat.is_eq(i, 1n+i) == False{} : Bool}

def s1_of source · line 33 · raw

@+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+c:U32 -> @+i:Nat -> @+hi:{Nat.is_lt(1n+i, 32n) == True{} : Bool} -> @+hI:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(16, U32.shl(c))) == i : Nat} -> @+hJ:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(17, U32.shl(c))) == 1n+i : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 5n, mT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(16, U32.shl(c))), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i)))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i, U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i))) : List<&2, U32>}

def upd_id source · line 38 · raw

@+xs:List<&2, U32> -> @+j:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, xs, j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(xs, j)) == xs : List<&2, U32>}

writing a word's own value changes nothing

def bump_nw source · line 48 · raw

@+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+c:U32 -> @+i:Nat -> @+hi:{Nat.is_lt(1n+i, 32n) == True{} : Bool} -> @+hI:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(16, U32.shl(c))) == i : Nat} -> @+hJ:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(17, U32.shl(c))) == 1n+i : Nat} -> @+hz:{U32.is_eq(U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i)), 0) == False{} : Bool} -> BumpOK(mT, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.bump_hi(Array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i))), c, False{}))

no wrap of the low word

def bump_w source · line 62 · raw

@+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+c:U32 -> @+i:Nat -> @+hi:{Nat.is_lt(1n+i, 32n) == True{} : Bool} -> @+hI:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(16, U32.shl(c))) == i : Nat} -> @+hJ:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(17, U32.shl(c))) == 1n+i : Nat} -> @+hz:{U32.is_eq(U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i)), 0) == True{} : Bool} -> BumpOK(mT, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.bump_hi(Array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i))), c, True{}))

the low word wraps: the high word is incremented too

def bump_c source · line 81 · raw

@+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+c:U32 -> @+i:Nat -> @+hi:{Nat.is_lt(1n+i, 32n) == True{} : Bool} -> @+hI:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(16, U32.shl(c))) == i : Nat} -> @+hJ:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(17, U32.shl(c))) == 1n+i : Nat} -> @+z:Bool -> @+hz:{U32.is_eq(U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i)), 0) == z : Bool} -> BumpOK(mT, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.bump_hi(Array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), i))), c, z))

def bump_ok source · line 90 · raw

@+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+c:U32 -> @+i:Nat -> @+hi:{Nat.is_lt(1n+i, 32n) == True{} : Bool} -> @+hI:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(16, U32.shl(c))) == i : Nat} -> @+hJ:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.add(17, U32.shl(c))) == 1n+i : Nat} -> BumpOK(mT, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.bump(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT)))

THEOREM (bump): counter c's words i, i + 1 become the 64-bit increment of their value; every other meta word is kept.