proofs/containers/hash_table/modn.bend checks

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

6 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/lemmas/proofs/word_value.bend as WV
import ../../lib/u32div.bend as UD
import ./cyc.bend as CY

Definitions

def pos source · line 13 · raw

@+n:Nat -> @+h:Nat -> @+t:Nat -> Nat

def dist source · line 16 · raw

@+n:Nat -> @+h:Nat -> @+j:Nat -> Nat

def dm_e2 source · line 19 · raw

@+bp:Nat -> @+v:Nat -> @g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_value.go_equation(bp, v, bp, 0n, 0n) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}

def dm_l2 source · line 23 · raw

@+bp:Nat -> @+v:Nat -> @g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_value.go_equation(bp, v, bp, 0n, 0n) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}

def dm_eq source · line 28 · raw

@+bp:Nat -> @+v:Nat -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}

v == (v / n) n + v mod n, and v mod n < n

def dm_lt source · line 31 · raw

@+bp:Nat -> @+v:Nat -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}

def absorb source · line 35 · raw

@+bp:Nat -> @+q:Nat -> @+r:Nat -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == Nat.mod(r, 1n+bp) : Nat}

(q n + r) mod n == r mod n

def mod_inner source · line 47 · raw

@+bp:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mod(Nat.add(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}

x + (y mod n) and x + y agree mod n

def pos_lt source · line 56 · raw

@+bp:Nat -> @+h:Nat -> @+t:Nat -> {Nat.is_lt(pos(1n+bp, h, t), 1n+bp) == True{} : Bool}

def dist_lt source · line 59 · raw

@+bp:Nat -> @+h:Nat -> @+j:Nat -> {Nat.is_lt(dist(1n+bp, h, j), 1n+bp) == True{} : Bool}

def pos_dist source · line 63 · raw

@+bp:Nat -> @+h:Nat -> @+j:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> {pos(1n+bp, h, dist(1n+bp, h, j)) == j : Nat}

walking dist(h, j) steps from h reaches j

def dist_pos source · line 72 · raw

@+bp:Nat -> @+h:Nat -> @+t:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+ht:{Nat.is_lt(t, 1n+bp) == True{} : Bool} -> {dist(1n+bp, h, pos(1n+bp, h, t)) == t : Nat}

the distance from h to the bucket t < n steps after h is t

def pos_next source · line 82 · raw

@+bp:Nat -> @+h:Nat -> @+t:Nat -> {Nat.mod(1n+pos(1n+bp, h, t), 1n+bp) == pos(1n+bp, h, 1n+t) : Nat}

the bucket after pos(h, t) is pos(h, t + 1)