~/bend-docscommunity

proofs/containers/hash_table/delmv.bend checks

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

15 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/containers/hash_table.bend as H
import ./buckets.bend as B
import ./inv.bend as IV
import ./state.bend as ST
import ./lookup.bend as LK
import ./tools.bend as T
import ./insm.bend as IM
import ./rehash.bend as RH
import ./ring.bend as RG
import ./keys.bend as K2

Definitions

def hlen2 source · line 22 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 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 at_vh source · line 25 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> {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), h) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def at_vk source · line 28 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> {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), k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def at_vo source · line 31 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+j:Nat -> @+hh:{Nat.is_eq(h, j) == False{} : Bool} -> @+hk:{Nat.is_eq(k, j) == False{} : Bool} -> {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), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def fm_o source · line 37 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+src:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{V, src, m}, n) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+hch:{Nat.is_eq(h, j) == False{} : Bool} -> @+ck:Bool -> @+hck:{Nat.is_eq(k, j) == ck : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{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), src, m}, j) == True{} : Bool}

def fm_k source · line 45 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+src:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{V, src, m}, n) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+ch:Bool -> @+hch:{Nat.is_eq(h, j) == ch : Bool} -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{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), src, m}, j) == True{} : Bool}

def from_move_m source · line 53 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+src:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{V, src, m}, n) == True{} : Bool} -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{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), src, m}, q) == True{} : Bool}

def from_move source · line 62 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+src:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{V, src, m}, n) == True{} : Bool} -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{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), src, m}, n) == True{} : Bool}

THEOREM: after the move every full bucket is still a copy

def tw_c source · line 65 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hox:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x) == True{} : Bool} -> @+p:Nat -> @+hp:{Nat.is_lt(p, n) == True{} : Bool} -> @+hat:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, p) == x : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhn:{Nat.is_lt(h, n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(k, p) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(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, x) == True{} : Bool}

def tw source · line 75 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hox:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x) == True{} : Bool} -> @+hhn:{Nat.is_lt(h, n) == True{} : Bool} -> @w0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/rehash.EqAt(V, n, x) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(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, x) == True{} : Bool}

def tm_i source · line 80 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hhn:{Nat.is_lt(h, n) == True{} : 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.anyeq(V, n, x)) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(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, x)) == True{} : Bool}

def to_move_m source · line 87 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+src:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+ms:Nat -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{src, V, n}, ms) == True{} : Bool} -> @+hhn:{Nat.is_lt(h, n) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, ms) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{src, 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}, q) == True{} : Bool}

def to_move source · line 97 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+src:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+ms:Nat -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{src, V, n}, ms) == True{} : Bool} -> @+hhn:{Nat.is_lt(h, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{src, 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}, ms) == True{} : Bool}

THEOREM: after the move every original bucket still has a copy

def uqr_b source · line 102 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+k:Nat -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, bs)) == True{} : Bool} -> @+j:Nat -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hu:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.uq_b(bs, j, x) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.uq_b(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), j, x) == True{} : Bool}

def uqr_i source · line 109 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+k:Nat -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, bs)) == True{} : Bool} -> @+n:Nat -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{bs}, n) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(k, j) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{})}, j) == True{} : Bool}

def uq_rm source · line 117 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+k:Nat -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, bs)) == True{} : Bool} -> @+n:Nat -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{bs}, n) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{})}, m) == True{} : Bool}

THEOREM: emptying a bucket keeps keys and links unique

def pno_rm_i source · line 126 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+k:Nat -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{V}, n) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+key:String -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, key} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(k, j) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), key}, j) == True{} : Bool}

def pno_rm source · line 134 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+k:Nat -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{V}, n) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+key:String -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, key} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), key}, m) == True{} : Bool}

def nsr_o source · line 142 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+k:Nat -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{V}, n) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+key:String -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, key} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+hc:{Nat.is_eq(k, j) == False{} : Bool} -> @+o:Bool -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)) == o : Bool} -> {Bool.not(Bool.and(o, Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, j)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))) == True{} : Bool}

def nsr_i source · line 152 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+k:Nat -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{V}, n) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+key:String -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, key} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(k, j) == c : Bool} -> {Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), j)), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), j)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))) == True{} : Bool}

def ns_rm source · line 159 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+k:Nat -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{V}, n) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+key:String -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, key} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), m) == True{} : Bool}

def uq_move source · line 169 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+k:Nat -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{V}, n) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+key:String -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, key} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+h:Nat -> @+hhn:{Nat.is_lt(h, n) == True{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, key})}, n) == True{} : Bool}

THEOREM: moving a bucket into an empty bucket keeps keys and links unique

def bupd_self source · line 175 · raw

@+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(xs, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(xs, k)) == xs : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def occn_rm source · line 185 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+k:Nat -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(V, n) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(V, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), n) : Nat}

emptying a full bucket k < n: one fewer full bucket

def occn_move source · line 191 · raw

@+V:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+k:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, k) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hbo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hzh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(V, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hhk:{Nat.is_eq(h, k) == False{} : Bool} -> @+hlh:{Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hlk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, V)) == True{} : Bool} -> @+hkn:{Nat.is_lt(k, n) == True{} : Bool} -> @+hhn:{Nat.is_lt(h, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(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) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(V, n) : Nat}

THEOREM: the move keeps the number of full buckets