proofs/containers/hash_table/strings.bend checks

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

4 imports

import Base
import ../../../spec/containers/hash_table.bend as S
import ../../../src/math/hash.bend as HS
import ../../../src/containers/hash_table.bend as H

Definitions

def rr source · line 10 · raw

@+s:String -> @+acc:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(s, acc), "") == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(acc, s) : String}

def rev2 source · line 17 · raw

@+s:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(s, ""), "") == s : String}

def fold source · line 21 · raw

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

the hash of a key: the mix folded over its character codes

def hash_acc source · line 28 · raw

@+s:String -> @+h:U32 -> @+acc:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.hash_acc(s, h, acc) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(acc, s), fold(s, h)) : Pair(String, U32)}

def lword source · line 36 · raw

@+s:String -> U32

a key's long check word

def key_long source · line 39 · raw

@+s:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.key_long(s) == (s, lword(s)) : Pair(String, U32)}

def and_true source · line 42 · raw

@+e:Bool -> {Bool.and(e, True{}) == e : Bool}

def and_false source · line 49 · raw

@+e:Bool -> {Bool.and(e, False{}) == False{} : Bool}

def and_assoc source · line 56 · raw

@+e:Bool -> @+p:Bool -> @+q:Bool -> {Bool.and(Bool.and(e, p), q) == Bool.and(e, Bool.and(p, q)) : Bool}

def eq_acc source · line 63 · raw

@+a:String -> @+b:String -> @+ra:String -> @+rb:String -> @+e:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.eq_acc(a, b, ra, rb, e) == ((0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(ra, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(rb, b)), Bool.and(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b))) : Pair(Pair(String, String), Bool)}

def eq source · line 77 · raw

@+a:String -> @+b:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.eq(a, b) == ((a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b)) : Pair(Pair(String, String), Bool)}

THEOREM: eq is String equality, handing both strings back.

def copy_acc source · line 80 · raw

@+s:String -> @+ra:String -> @+rb:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.copy_acc(s, ra, rb) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(ra, s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rev_onto(rb, s)) : Pair(String, String)}

def str_copy source · line 87 · raw

@+s:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.str_copy(s) == (s, s) : Pair(String, String)}