proofs/containers/hash_table/shift.bend checks

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

30 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../lib/word.bend as WD
import ../../lib/u32div.bend as UD
import ../../../src/math/hash.bend as HS
import ../../../src/containers/hash_table.bend as H
import ./words.bend as WR
import ./table.bend as TB
import ./buckets.bend as B
import ./modn.bend as M
import ./cyc.bend as CY
import ./arr.bend as AX
import ./inv.bend as IV
import ./probe_impl.bend as PI
import ./probe_all.bend as PA
import ./insm.bend as IM
import ./insa.bend as IA
import ./insert.bend as IS
import ./rehash.bend as RH
import ./grow.bend as GR
import ./ring.bend as RG
import ./hole.bend as HO
import ./rawins.bend as RI
import ./keys.bend as K2
import ./delmv.bend as DM
import ../../lib/words32.bend as W32

Types

type DSt source · line 73 · raw

Data

DS

@iU:U32 -> @h:Nat -> @kU:U32 -> @dk:Nat -> @T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> DSt

Definitions

def d_other source · line 37 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+l:U32 -> @+j:Nat -> @+hne:{Nat.is_eq(e, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(tb, kl, j) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def d_at source · line 41 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+l:U32 -> @+htb:{Nat.is_lt(1n+Nat.double(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, tb)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, U32.is_eq(w, 0)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def d_same source · line 45 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+l:U32 -> @+n:Nat -> @+m:Nat -> @+i:Nat -> @+hei:{Nat.is_lt(e, i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, m, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(tb, kl, m, i) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def d_ins source · line 52 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+l:U32 -> @+n:Nat -> @+htb:{Nat.is_lt(1n+Nat.double(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, tb)) == True{} : Bool} -> @+m:Nat -> @+i:Nat -> @+d:Nat -> @+hed:{Nat.add(i, d) == e : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, m, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(tb, kl, m, i), d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, U32.is_eq(w, 0))) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def put_dec source · line 67 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+l:U32 -> @+n:Nat -> @+htb:{Nat.is_lt(1n+Nat.double(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, tb)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, U32.is_eq(w, 0))) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

THEOREM: writing (w, l) into bucket e decodes as bucket e replaced

def dq10 source · line 78 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

the invariant; dq<i> names the conjunction of its components from i on, so no statement repeats the rest of the chain (dp<i>: the invariant gives it)

def dq9 source · line 81 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq8 source · line 84 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq7 source · line 87 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq6 source · line 90 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq5 source · line 93 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq4 source · line 96 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq3 source · line 99 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq2 source · line 102 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dq1 source · line 105 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dinvF source · line 108 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

def dp1 source · line 111 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq1(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp2 source · line 114 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq2(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp3 source · line 117 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq3(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp4 source · line 120 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq4(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp5 source · line 123 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq5(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp6 source · line 126 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq6(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp7 source · line 129 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq7(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp8 source · line 132 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq8(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp9 source · line 135 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq9(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp10 source · line 138 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {dq10(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dp11 source · line 141 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(h, 1n+bp) == True{} : Bool}

def q1 source · line 144 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(iU), h) == True{} : Bool}

def q2 source · line 147 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == True{} : Bool}

def q3 source · line 150 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool}

def q4 source · line 153 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == 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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool}

def q5 source · line 156 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == 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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{})}, 1n+bp) == True{} : Bool}

def q6 source · line 159 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == 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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), V0, 1n+bp}, 1n+bp) == True{} : Bool}

def q7 source · line 162 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{V0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp}, 1n+bp) == True{} : Bool}

def q8 source · line 165 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(V0, 1n+bp)) == True{} : Bool}

def q9 source · line 168 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Bool.not(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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), e0))) == True{} : Bool}

def q10 source · line 171 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_le(1n, dk) == True{} : Bool}

def q11 source · line 174 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0)) == True{} : Bool}

def q12 source · line 177 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hq:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(h, 1n+bp) == True{} : Bool}

def q_mk source · line 180 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+h1:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(iU), h) == True{} : Bool} -> @+h2:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == True{} : Bool} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+h4:{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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), h, dk}, 1n+bp) == True{} : Bool} -> @+h5:{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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{})}, 1n+bp) == True{} : Bool} -> @+h6:{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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), V0, 1n+bp}, 1n+bp) == True{} : Bool} -> @+h7:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{V0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp}, 1n+bp) == True{} : Bool} -> @+h8:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(V0, 1n+bp)) == True{} : Bool} -> @+h9:{Bool.not(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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), e0))) == True{} : Bool} -> @+h10:{Nat.is_le(1n, dk) == True{} : Bool} -> @+h11:{Nat.is_le(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0)) == True{} : Bool} -> @+h12:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}

def dinv source · line 183 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @st:DSt -> Bool

def dfuel source · line 188 · raw

@+bp:Nat -> @+e0:Nat -> @+f:Nat -> @st:DSt -> Bool

def dfin source · line 195 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Bool

what the deletion leaves

def f1 source · line 198 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+h:{dfin(kl, K, bp, V0, Tf) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, Tf) == True{} : Bool}

def f2 source · line 201 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+h:{dfin(kl, K, bp, V0, Tf) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool}

def f3 source · line 204 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+h:{dfin(kl, K, bp, V0, Tf) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp)}, 1n+bp) == True{} : Bool}

def f4 source · line 207 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+h:{dfin(kl, K, bp, V0, Tf) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp) == True{} : Bool}

def f5 source · line 210 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+h:{dfin(kl, K, bp, V0, Tf) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{V0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp) == True{} : Bool}

def f6 source · line 213 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+h:{dfin(kl, K, bp, V0, Tf) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), 1n+bp), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(V0, 1n+bp)) == True{} : Bool}

def f_mk source · line 216 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+Tf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+g1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, Tf) == True{} : Bool} -> @+g2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+g3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+g4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp) == True{} : Bool} -> @+g5:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{V0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp) == True{} : Bool} -> @+g6:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, Tf), kl, 1n+bp), 1n+bp), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(V0, 1n+bp)) == True{} : Bool} -> {dfin(kl, K, bp, V0, Tf) == True{} : Bool}

def DelOK source · line 219 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+f:Nat -> @+iU:U32 -> @+kU:U32 -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Type

def DelOKs source · line 222 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+f:Nat -> @st:DSt -> Type

def g_hdn source · line 230 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(dk, 1n+bp) == True{} : Bool}

def g_hkn source · line 233 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n+bp) == True{} : Bool}

def g_hkK source · line 236 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool}

def g_hhK source · line 239 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool}

def g_hhk source · line 242 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_eq(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == False{} : Bool}

def g_ekv source · line 245 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kU) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk) : Nat}

def g_eiv source · line 248 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(iU) == h : Nat}

def g_hh2 source · line 251 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kU)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+K)) == True{} : Bool}

def g_ews source · line 254 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(kU)) == Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) : Nat}

def g_ewl source · line 257 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(kU))) == 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) : Nat}

def eqS source · line 260 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.sh_step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), iU, kU) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.sh_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), iU, kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Sh}

def eqL source · line 265 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.sh_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), iU, kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), False{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.sh_mv(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)))) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Sh}

def at_k source · line 270 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), kl, U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def sc_nr source · line 274 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(K, one) == 1n+bp : Nat}

def lt_sc source · line 277 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+x:U32 -> @+v:Nat -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(x) == v : Nat} -> @+hv:{Nat.is_lt(v, 1n+bp) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.sc(K, one)) == True{} : Bool}

def mdist source · line 280 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+a:U32 -> @+b:U32 -> @+va:Nat -> @+vb:Nat -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a) == va : Nat} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b) == vb : Nat} -> @+hva:{Nat.is_lt(va, 1n+bp) == True{} : Bool} -> @+hvb:{Nat.is_lt(vb, 1n+bp) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.and(U32.sub(b, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, va, vb) : Nat}

def mvv source · line 286 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == Nat.is_ge(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)), dk) : Bool}

THEOREM: the implementation's move test compares the scanned bucket's distance from home with the gap's

def len_v source · line 294 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{})) == 1n+bp : Nat}

def lt_lv source · line 297 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+x:Nat -> @+hx:{Nat.is_lt(x, 1n+bp) == True{} : Bool} -> {Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}))) == True{} : Bool}

def e_iu source · line 300 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {iU == U32.from_nat(h) : U32}

def g_htb source · line 304 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_lt(1n+Nat.double(h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T))) == True{} : Bool}

def g_occk source · line 307 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == c : Bool} -> {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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))) == Bool.not(c) : Bool}

def step_end source · line 312 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == True{} : Bool} -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T)

an empty scanned bucket: the gap is cleared and the deletion ends

def g_hbk source · line 323 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)))))))} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def g_e0f source · line 326 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {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/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), e0)) == False{} : Bool}

def ne_occ_c source · line 329 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+x:Nat -> @+y:Nat -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, x)) == True{} : Bool} -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, y)) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(x, y) == c : Bool} -> {c == False{} : Bool}

def g_nke source · line 336 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), e0) == False{} : Bool}

def dne_c source · line 339 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> @+c:Bool -> @+hc2:{Nat.is_eq(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0)) == c : Bool} -> {c == False{} : Bool}

def g_dlt source · line 348 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> {Nat.is_lt(dk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0)) == True{} : Bool}

the scanned bucket is full, so the empty e0 lies further on

def g_nv source · line 351 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == Nat.mod(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 1n+bp) : Nat}

def eq_mv source · line 358 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.shift(1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.sh_step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), iU, kU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), iU, kU) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.shift(1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.sh_mv(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), iU, kU) : Array<U32>}

the implementation reaches the move test

def nhe_c source · line 361 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(h, e0) == c : Bool} -> {c == False{} : Bool}

def g_nhe source · line 371 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {Nat.is_eq(h, e0) == False{} : Bool}

the gap is not the empty bucket ahead

def g_hzh source · line 377 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def ev2 source · line 380 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(h))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(h)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))))), kl, 1n+bp), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 1n+bp), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)))))))}) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def mv_fin source · line 387 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> @+hm:{U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == True{} : Bool} -> @r:DelOK(kl, K, bp, V0, p, kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(h))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(h)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))))) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T)

def step_move source · line 394 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hfu:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> @+hm:{U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == True{} : Bool} -> @rec:(@+st2:DSt -> @+hi2:{dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2:{dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T)

def sk_fin source · line 415 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> @+hm:{U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == False{} : Bool} -> @r:DelOK(kl, K, bp, V0, p, iU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), T) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T)

def step_skip source · line 421 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hfu:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> @+hm:{U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == False{} : Bool} -> @rec:(@+st2:DSt -> @+hi2:{dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2:{dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T)

def step_mvc source · line 433 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hfu:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == False{} : Bool} -> @+m:Bool -> @+hm:{U32.is_ge(U32.and(U32.sub(kU, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), U32.and(U32.sub(kU, iU), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == m : Bool} -> @rec:(@+st2:DSt -> @+hi2:{dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2:{dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T)

def step_c source · line 440 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+iU:U32 -> @+h:Nat -> @+kU:U32 -> @+dk:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hi:{dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool} -> @+p:Nat -> @+hfu:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, dk))), 0) == c : Bool} -> @rec:(@+st2:DSt -> @+hi2:{dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2:{dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T)

def loop source · line 448 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+V0:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e0:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+f:Nat -> @+st:DSt -> @+hi:{dinv(kl, K, bp, V0, e0, st) == True{} : Bool} -> @+hfu:{dfuel(bp, e0, f, st) == True{} : Bool} -> DelOKs(kl, K, bp, V0, f, st)

THEOREM: the backward shift, run with enough fuel, ends with whole clusters

def cr_i source · line 458 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j))) == True{} : Bool}

def from_refl source · line 461 · raw

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

def to_refl source · line 469 · raw

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

def DelAt source · line 478 · raw

@+kl:List<&2, String> -> @+K:Nat -> @+bp:Nat -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+i:Nat -> Type

def d_hiK source · line 481 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+kl:List<&2, String> -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, OT) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+huo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+hoi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool} -> {Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool}

def d_ev source · line 484 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+kl:List<&2, String> -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, OT) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+huo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+hoi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.from_nat(i)) == i : Nat}

def d_hlen source · line 487 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+kl:List<&2, String> -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, OT) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+huo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+hoi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool} -> {Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp))) == True{} : Bool}

def d_kv source · line 490 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+kl:List<&2, String> -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, OT) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+huo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+hoi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(U32.from_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, i, 1n) : Nat}

def z0_c source · line 496 · raw

@+O:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+i:Nat -> @+e0:Nat -> @+hz0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(O, e0) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hlen:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, O)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(i, e0) == c : Bool} -> {Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(O, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), e0))) == True{} : Bool}

def d_fin source · line 503 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+kl:List<&2, String> -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, OT) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+huo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+hoi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool} -> @+e0:Nat -> @lo:DelOK(kl, K, bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}), 1n+bp, U32.from_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(U32.from_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), OT) -> DelAt(kl, K, bp, OT, i)

def d_e0 source · line 509 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+kl:List<&2, String> -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, OT) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+huo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+hoi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool} -> @e0p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.Empty0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp) -> DelAt(kl, K, bp, OT, i)

def del_ok source · line 520 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+bp:Nat -> @+hN:{1n+bp == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K) : Nat} -> @+kl:List<&2, String> -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, OT) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+bp) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)) == True{} : Bool} -> @+huo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool} -> @+hoi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool} -> @+hem:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 1n+bp), 1n+bp), 1n+bp) == True{} : Bool} -> DelAt(kl, K, bp, OT, i)

THEOREM: deleting bucket i of a clustered table with a free bucket leaves a clustered table of copies of the other buckets