~/bend-docscommunity

proofs/containers/hash_table/hole.bend checks

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

14 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/math/hash.bend as HS
import ./buckets.bend as B
import ./modn.bend as M
import ./cyc.bend as CY
import ./probe_all.bend as PA
import ./insm.bend as IM
import ./insert.bend as IS
import ./ring.bend as RG
import ./rehash.bend as RH

Definitions

def hb_lt source · line 23 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 1n+bp) == True{} : Bool}

def ox_c source · line 32 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+a:Nat -> @+h:Nat -> @+q:Nat -> @+hp:{Bool.and(Bool.or(Nat.is_eq(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, q)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(bs, n, a, q, h)) == True{} : Bool} -> @+t:Nat -> @+ht:{Nat.is_lt(t, 1n+q) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(t, q) == c : Bool} -> @rec:(@hlt:{Nat.is_lt(t, q) == True{} : Bool} -> {Bool.or(Nat.is_eq(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, t)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, t)))) == True{} : Bool}) -> {Bool.or(Nat.is_eq(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, t)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, t)))) == True{} : Bool}

def opx_inst source · line 39 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+a:Nat -> @+m:Nat -> @+h:Nat -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(bs, n, a, m, h) == True{} : Bool} -> @+t:Nat -> @+ht:{Nat.is_lt(t, m) == True{} : Bool} -> {Bool.or(Nat.is_eq(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, t)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, a, t)))) == True{} : Bool}

def opx_pre source · line 46 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+a:Nat -> @+m:Nat -> @+h:Nat -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(bs, n, a, m, h) == True{} : Bool} -> @+m2:Nat -> @+hm:{Nat.is_le(m2, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(bs, n, a, m2, h) == True{} : Bool}

def or_f source · line 54 · raw

@+x:Bool -> @+y:Bool -> @+h:{Bool.or(x, y) == True{} : Bool} -> @+hx:{x == False{} : Bool} -> {y == True{} : Bool}

def occ_of_opx source · line 58 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+bp:Nat -> @+a:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+h:Nat -> @+m:Nat -> @+hm:{Nat.is_le(m, 1n+bp) == True{} : Bool} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(bs, 1n+bp, a, m, h) == True{} : Bool} -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h), m) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(bs, 1n+bp, a, m) == True{} : Bool}

a path that does not reach h is full

def ooc_bit source · line 70 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+i:Nat -> @+p:Nat -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, p)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(i, p) == c : Bool} -> {Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), p))) == True{} : Bool}

def opx_of_occ source · line 78 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+i:Nat -> @+n:Nat -> @+a:Nat -> @+m:Nat -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(bs, n, a, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), n, a, m, i) == True{} : Bool}

emptying bucket i leaves every full path full except at i

def hlen2 source · line 89 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> {Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}))) == True{} : Bool}

def mv_h2 source · line 92 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+p:Nat -> @+c:Bool -> @+hc:{Nat.is_eq(h, p) == c : Bool} -> @+hold:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, p))) == True{} : Bool} -> @+hck:{Nat.is_eq(k, p) == False{} : Bool} -> {Bool.or(False{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), p))) == True{} : Bool}

def mv_h source · line 99 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+p:Nat -> @+c:Bool -> @+hc:{Nat.is_eq(h, p) == c : Bool} -> @+hold:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, p))) == True{} : Bool} -> @+ck:Bool -> @+hck:{Nat.is_eq(k, p) == ck : Bool} -> {Bool.or(ck, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), p))) == True{} : Bool}

def opx_move source · line 107 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+n:Nat -> @+a:Nat -> @+m:Nat -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(V, n, a, m, h) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), n, a, m, k) == True{} : Bool}

THEOREM: after the move, paths are full except at the new gap k

def dist_split2 source · line 119 · raw

@+bp:Nat -> @+a:Nat -> @+h:Nat -> @+j:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, j)) == True{} : Bool} -> {Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, a, j) : Nat}

a path from a through h to j: its length splits at h

def dp_c source · line 129 · raw

@+bp:Nat -> @+i:Nat -> @+j:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hne:{Nat.is_eq(i, j) == False{} : Bool} -> @+d:Nat -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, i, j) == d : Nat} -> {Nat.is_le(1n, d) == True{} : Bool}

def dist_pos1 source · line 138 · raw

@+bp:Nat -> @+i:Nat -> @+j:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hne:{Nat.is_eq(i, j) == False{} : Bool} -> {Nat.is_le(1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, i, j)) == True{} : Bool}

distinct buckets are at least one step apart

def h0_o source · line 144 · raw

@+O:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hij:{Nat.is_eq(i, j) == False{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(O, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), x), j))) == True{} : Bool} -> @+o:Bool -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x) == o : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(o, Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(O, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), x), j), i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), x), i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), x), j)), Nat.is_le(1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, i, j))))) == True{} : Bool}

def h0_i source · line 153 · raw

@+O:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+hlen:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, O)) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(O, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(i, j) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(O, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), i, 1n}, j) == True{} : Bool}

def hole_init source · line 162 · raw

@+O:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+hlen:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, O)) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(O, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(O, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), i, 1n}, m) == True{} : Bool}

THEOREM: emptying a bucket of a clustered table starts the invariant

def dist_k source · line 173 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == dk : Nat}

def hk_c source · line 176 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == c : Bool} -> {c == False{} : Bool}

def h_ne_k source · line 185 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> {Nat.is_eq(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == False{} : Bool}

the scan position is not the gap

def e_bad source · line 190 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == False{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hoj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)) == True{} : Bool} -> @+hop:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j), h) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)) == True{} : Bool} -> @+hge:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j)) == True{} : Bool} -> @+c3:Bool -> @+hc3:{Nat.is_eq(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j)) == c3 : Bool} -> Empty

def e_c source · line 207 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == False{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hoj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)) == True{} : Bool} -> @+hop:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j), h) == True{} : Bool} -> @+himp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)), Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j))) == True{} : Bool} -> @+c2:Bool -> @+hc2:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)) == c2 : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)) == True{} : Bool}

def e_o source · line 214 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == False{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, j) == True{} : Bool} -> @+o:Bool -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)) == o : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j))) == True{} : Bool}

def hole_end_m source · line 222 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == False{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PClus{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)}, m) == True{} : Bool}

def hole_end source · line 231 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == False{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool}

THEOREM: when the scan meets an empty bucket, the clusters are whole

def s_ne source · line 237 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hskip:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), dk) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hc2:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)) == True{} : Bool} -> @+c3:Bool -> @+hc3:{Nat.is_eq(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j)) == c3 : Bool} -> {c3 == False{} : Bool}

def s_imp source · line 250 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hskip:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), dk) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+himp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)), Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j))) == True{} : Bool} -> @+c2:Bool -> @+hc2:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)) == c2 : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(c2, Nat.is_le(1n+dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j))) == True{} : Bool}

def sk_o source · line 257 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hskip:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), dk) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, j) == True{} : Bool} -> @+o:Bool -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)) == o : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(o, Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)), Nat.is_le(1n+dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, j))))) == True{} : Bool}

def hole_skip_m source · line 265 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hskip:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), dk) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, 1n+dk}, m) == True{} : Bool}

def hole_skip source · line 274 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+hskip:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), dk) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, 1n+dk}, 1n+bp) == True{} : Bool}

THEOREM: skipping a bucket whose path starts after the gap keeps the invariant one step further

def hkk source · line 280 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hmv:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n+bp) == True{} : Bool}

def m_at_h source · line 283 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hmv:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n}, h) == True{} : Bool}

def m_o source · line 295 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hmv:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hkj:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), j) == False{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, j) == True{} : Bool} -> @+o:Bool -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)) == o : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(o, Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.opx(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)), j)), Nat.is_le(1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), j))))) == True{} : Bool}

def m_k source · line 303 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hmv:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+hc:{Nat.is_eq(h, j) == False{} : Bool} -> @+ck:Bool -> @+hck:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), j) == ck : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n}, j) == True{} : Bool}

def m_i source · line 310 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hmv:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(h, j) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n}, j) == True{} : Bool}

def hole_move_m source · line 317 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hmv:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n}, m) == True{} : Bool}

def hole_move source · line 326 · raw

@+K:Nat -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+dk:Nat -> @+hd1:{Nat.is_le(1n, dk) == True{} : Bool} -> @+hdn:{Nat.is_lt(dk, 1n+bp) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hmv:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == True{} : Bool} -> @+hlen:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{V, 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHole{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, b), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n}, 1n+bp) == True{} : Bool}

THEOREM: moving the scanned bucket into the gap moves the gap to it