~/bend-docscommunity

proofs/containers/hash_table/cyc.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as Cyc

11 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/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/u32div.bend as UD
import ../../math/u64/u64div.bend as UV
import ../../../src/containers/hash_table.bend as H
import ../../lib/words32.bend as W32

Definitions

def msk source · line 19 · raw

@+k:Nat -> U32

def and_mod source · line 23 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.and(x, msk(k))) == Nat.mod(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) : Nat}

x & (2^k - 1) is x mod 2^k

def next_val source · line 34 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+i:U32 -> @+hk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, msk(k))) == Nat.mod(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) : Nat}

the next bucket, cyclically

def sub_split source · line 40 · raw

@+a:Nat -> @+n:Nat -> @+m:Nat -> @+ha:{Nat.is_le(a, n) == True{} : Bool} -> @+hn:{Nat.is_le(n, m) == True{} : Bool} -> {Nat.sub(m, a) == Nat.add(Nat.sub(n, a), Nat.sub(m, n)) : Nat}

def mod_plus source · line 50 · raw

@+n:Nat -> @+r:Nat -> @+h:{Nat.is_lt(r, n) == True{} : Bool} -> {Nat.mod(Nat.add(n, r), n) == r : Nat}

(N + r) mod N == r for r < N

def mod_small source · line 54 · raw

@+n:Nat -> @+r:Nat -> @+h:{Nat.is_lt(r, n) == True{} : Bool} -> {Nat.mod(r, n) == r : Nat}

def lt_add_r source · line 57 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, x), Nat.add(b, x)) == True{} : Bool}

def wrap_free source · line 61 · raw

@+a:Nat -> @+b:Nat -> @+n:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+han:{Nat.is_le(a, n) == True{} : Bool} -> {Nat.add(b, Nat.sub(n, a)) == Nat.add(n, Nat.sub(b, a)) : Nat}

b + (n - a) == n + (b - a) when a <= b and a <= n

def dist_le source · line 68 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+a:U32 -> @+b:U32 -> @+hb:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == True{} : Bool} -> @+han:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == True{} : Bool} -> @+hab:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b)) == True{} : Bool} -> {Nat.mod(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.sub(b, a)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == Nat.mod(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) : Nat}

def dist_gt source · line 76 · raw

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

def dist_g source · line 106 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+j:Nat -> @+hkj:{Nat.add(k, j) == 32n : Nat} -> @+a:U32 -> @+b:U32 -> @+ha:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == True{} : Bool} -> @+hb:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b)) == c : Bool} -> {Nat.mod(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.sub(b, a)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == Nat.mod(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) : Nat}

def dist source · line 114 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+j:Nat -> @+hkj:{Nat.add(k, j) == 32n : Nat} -> @+a:U32 -> @+b:U32 -> @+ha:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == True{} : Bool} -> @+hb:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.and(U32.sub(b, a), msk(k))) == Nat.mod(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(k, one)) : Nat}

THEOREM: (b - a) & mask is the cyclic distance from a to b.