proofs/containers/hash_table/arr.bend

bend-collections-laws-containers@1.0.0.0 · 36 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/word.bend as WD
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
11
12# Base.Array reads on the mirror trees of the hash map's arrays, and the
13# bucket index arithmetic (bucket i's word at 2i, its link at 2i + 1).
14
15
16# 2^d <= 2^32 for d < 32
17
18# the word index 2i and the link index 2i + 1 of bucket i
19def ix_w(+i: U32, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +h: {Nat.is_lt(1n+Nat.double(UD.v(i)), SC.pow2(d)) == True{} : Bool}) -> {UD.v(U32.shl(i)) == Nat.double(UD.v(i)) : Nat}:
20  U.shl_value(i, d, N.lt_le(d, 32n, hd), N.lt_trans(Nat.double(UD.v(i)), 1n+Nat.double(UD.v(i)), SC.pow2(d), N.lt_succ(Nat.double(UD.v(i))), h))
21
22def ix_l1(+one: Nat, +h1: {one == 1n : Nat}, +i: U32, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +h: {Nat.is_lt(1n+Nat.double(UD.v(i)), SC.pow2(d)) == True{} : Bool}) -> {UD.v(U32.inc(U32.shl(i))) == 1n+Nat.double(UD.v(i)) : Nat}:
23  +ew = ix_w(i, d, hd, h)
24  +hb = L.subst(Nat, z => {Nat.is_lt(1n+z, WD.sc(32n, one)) == True{} : Bool}, Nat.double(UD.v(i)), UD.v(U32.shl(i)), Equal.sym(Nat, UD.v(U32.shl(i)), Nat.double(UD.v(i)), ew), N.lt_le_trans(1n+Nat.double(UD.v(i)), SC.pow2(d), WD.sc(32n, one), h, W32.pow_le32(one, h1, d, hd)))
25  Equal.trans(Nat, UD.v(U32.inc(U32.shl(i))), 1n+UD.v(U32.shl(i)), 1n+Nat.double(UD.v(i)), W32.inc_val(one, h1, U32.shl(i), hb), Equal.cong(Nat, Nat, z => 1n+z, UD.v(U32.shl(i)), Nat.double(UD.v(i)), ew))
26
27def ix_l(+i: U32, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +h: {Nat.is_lt(1n+Nat.double(UD.v(i)), SC.pow2(d)) == True{} : Bool}) -> {UD.v(U32.inc(U32.shl(i))) == 1n+Nat.double(UD.v(i)) : Nat}:
28  ix_l1(1n, {==}, i, d, hd, h)
29
30# reading a word array at an index below its size
31def getw(+d: Nat, +t: AR.Tree<U32>, +j: U32, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hj: {Nat.is_lt(UD.v(j), SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(U32, d, t) == True{} : Bool}) -> {Array.get(U32, AR.thaw(U32, t), j) == (AR.thaw(U32, t), W32.nth0(AR.slots(U32, t), UD.v(j))) : Array<U32> & U32}:
32  +hl = L.subst(Nat, z => {Nat.is_lt(UD.v(j), z) == True{} : Bool}, SC.pow2(d), SC.length(U32, AR.slots(U32, t)), Equal.sym(Nat, SC.length(U32, AR.slots(U32, t)), SC.pow2(d), AR.slots_length(U32, d, t, pf)), hj)
33  AR.get(U32, d, t, j, W32.nth0(AR.slots(U32, t), UD.v(j)), hd, hj, W32.nth_some(AR.slots(U32, t), UD.v(j), hl), pf)
34
35def nths_of(+d: Nat, +t: AR.Tree<String>, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(String, d, t) == True{} : Bool}) -> {SC.nth(String, AR.slots(String, t), j) == Some{TB.nths(AR.slots(String, t), j)} : Maybe<&2, String>}:
36  TB.nths_some(AR.slots(String, t), j, L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, SC.pow2(d), SC.length(String, AR.slots(String, t)), Equal.sym(Nat, SC.length(String, AR.slots(String, t)), SC.pow2(d), AR.slots_length(String, d, t, pf)), hj))