proofs/containers/hash_table/insa.bend checks

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

15 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./words.bend as WR
import ./strings.bend as STR
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./state.bend as ST
import ./probe_all.bend as PA
import ./insm.bend as IM
import ../../lib/words32.bend as W32

Definitions

def len_upd source · line 23 · raw

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

def nths_upd_same source · line 34 · raw

@+xs:List<&2, String> -> @+i:Nat -> @+v:String -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, xs, i, v), i) == v : String}

def nths_upd_other source · line 43 · raw

@+xs:List<&2, String> -> @+i:Nat -> @+j:Nat -> @+v:String -> @+h:{Nat.is_eq(i, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, xs, i, v), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(xs, j) : String}

def dd_c source · line 58 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_eq(a, b) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(Nat.double(a), Nat.double(b)) == c : Bool} -> {c == False{} : Bool}

def dd_ne source · line 66 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_eq(a, b) == False{} : Bool} -> {Nat.is_eq(Nat.double(a), Nat.double(b)) == False{} : Bool}

def eo_c source · line 69 · raw

@+a:Nat -> @+b:Nat -> @+c:Bool -> @+hc:{Nat.is_eq(Nat.double(a), 1n+Nat.double(b)) == c : Bool} -> {c == False{} : Bool}

def eo_ne source · line 76 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_eq(Nat.double(a), 1n+Nat.double(b)) == False{} : Bool}

def oe_ne source · line 79 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_eq(1n+Nat.double(a), Nat.double(b)) == False{} : Bool}

def w_other source · line 84 · raw

@+tb:List<&2, U32> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+j:Nat -> @+hne:{Nat.is_eq(e, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), L), Nat.double(j)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, Nat.double(j)) : U32}

def l_other source · line 87 · raw

@+tb:List<&2, U32> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+j:Nat -> @+hne:{Nat.is_eq(e, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), L), 1n+Nat.double(j)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, 1n+Nat.double(j)) : U32}

def w_same source · line 90 · raw

@+tb:List<&2, U32> -> @+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/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), L), Nat.double(e)) == w : U32}

def l_same source · line 93 · raw

@+tb:List<&2, U32> -> @+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/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), L), 1n+Nat.double(e)) == L : U32}

def dec_same_c source · line 96 · raw

@+w:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+s:Nat -> @+sk:String -> @+emp:Bool -> @+h:{Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, emp)), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, emp)))), s))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, s, sk), emp) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, emp) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def dec_other source · line 104 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+sk:String -> @+j:Nat -> @+hne:{Nat.is_eq(e, j) == False{} : Bool} -> @+hns:{Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(tb, kl, j)), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(tb, kl, j)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L))))) == 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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), sk), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(tb, kl, j) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def dec_at source · line 110 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+sk:String -> @+hw0:{U32.is_eq(w, 0) == False{} : Bool} -> @+htb:{Nat.is_lt(1n+Nat.double(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, tb)) == True{} : Bool} -> @+hkl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl)) == 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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), sk), e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, L, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, sk)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def idx_lt source · line 118 · raw

@+i:Nat -> @+p:Nat -> @+n:Nat -> @+h:{Nat.is_le(Nat.add(i, 1n+p), n) == True{} : Bool} -> {Nat.is_lt(i, n) == True{} : Bool}

def idx_next source · line 121 · raw

@+i:Nat -> @+p:Nat -> @+n:Nat -> @+h:{Nat.is_le(Nat.add(i, 1n+p), n) == True{} : Bool} -> {Nat.is_le(Nat.add(1n+i, p), n) == True{} : Bool}

def ns_dec source · line 124 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+sk:String -> @+n:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), n) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(tb, kl, i)), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(tb, kl, i)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L))))) == True{} : Bool}

def con_eq source · line 127 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+x:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+y:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+ha:{a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hx:{x == y : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>} -> {a <> x == b <> y : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def dl_same source · line 130 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+sk:String -> @+n:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), n) == True{} : Bool} -> @+m:Nat -> @+i:Nat -> @+hmi:{Nat.is_le(Nat.add(i, m), n) == True{} : Bool} -> @+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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), sk), m, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(tb, kl, m, i) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def dl_ins source · line 138 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+sk:String -> @+n:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), n) == True{} : Bool} -> @+hw0:{U32.is_eq(w, 0) == False{} : Bool} -> @+htb:{Nat.is_lt(1n+Nat.double(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, tb)) == True{} : Bool} -> @+hkl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl)) == True{} : Bool} -> @+m:Nat -> @+i:Nat -> @+d:Nat -> @+hed:{Nat.add(i, d) == e : Nat} -> @+hmi:{Nat.is_le(Nat.add(i, m), n) == 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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), sk), 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/buckets.BF{w, L, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, sk)}) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def buckets_put source · line 155 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+e:Nat -> @+w:U32 -> @+L:U32 -> @+sk:String -> @+n:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), n) == True{} : Bool} -> @+hw0:{U32.is_eq(w, 0) == False{} : Bool} -> @+htb:{Nat.is_lt(1n+Nat.double(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, tb)) == True{} : Bool} -> @+hkl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl)) == 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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), sk), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, L, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, sk)}) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

THEOREM: the written arrays decode to the old buckets with bucket e replaced

def len_dlist source · line 158 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+m:Nat -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(tb, kl, m, i)) == m : Nat}

def ks_short source · line 167 · raw

@+c:U32 -> @+t:String -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.short_c(c, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c), "") == SCon{Chr{c}, t} : String}

def ks_c source · line 175 · raw

@+c:U32 -> @+t:String -> @+sh:Bool -> @+hsh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.short_c(c, t) == sh : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kw_c(c, t, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.st_c(c, t, sh)) == SCon{Chr{c}, t} : String}

def keyof_stored source · line 183 · raw

@+key:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key)) == key : String}

THEOREM: a key's word and the string the probe hands back decode to the key