proofs/containers/hash_table/table.bend checks

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

7 imports

import Base
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./buckets.bend as B
import ../../lib/words32.bend as W32

Definitions

def nths source · line 15 · raw

@ks:List<&2, String> -> @+i:Nat -> String

def keyof_c source · line 25 · raw

@+w:U32 -> @s:String -> @short:Bool -> String

the key of a full bucket with word w and stored string s

def keyof source · line 32 · raw

@+w:U32 -> @s:String -> String

def dec_c source · line 35 · raw

@+w:U32 -> @+l:U32 -> @+ks:List<&2, String> -> @empty:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk

def dec source · line 43 · raw

@+tb:List<&2, U32> -> @+ks:List<&2, String> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk

bucket i of the arrays

def dlist source · line 47 · raw

@+tb:List<&2, U32> -> @+ks:List<&2, String> -> @+m:Nat -> @+i:Nat -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>

buckets i .. i + m - 1

def at_dlist source · line 54 · raw

@+tb:List<&2, U32> -> @+ks:List<&2, String> -> @+m:Nat -> @+i:Nat -> @+j:Nat -> @+hj:{Nat.is_lt(j, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(dlist(tb, ks, m, i), j) == dec(tb, ks, Nat.add(i, j)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def buckets source · line 64 · raw

@+tb:List<&2, U32> -> @+ks:List<&2, String> -> @+n:Nat -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>

the bucket list of a table of n buckets

def at_buckets source · line 67 · raw

@+tb:List<&2, U32> -> @+ks:List<&2, String> -> @+n:Nat -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(buckets(tb, ks, n), j) == dec(tb, ks, j) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def nths_some source · line 72 · raw

@+ks:List<&2, String> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, ks)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(String, ks, i) == Some{nths(ks, i)} : Maybe<&2, String>}

def upd_upd source · line 81 · raw

@+xs:List<&2, String> -> @+i:Nat -> @+a:String -> @+b:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, xs, i, a), i, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, xs, i, b) : List<&2, String>}

def upd_self source · line 90 · raw

@+xs:List<&2, String> -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, xs, i, nths(xs, i)) == xs : List<&2, String>}