proofs/containers/bitset/walk.bend
bend-collections-laws-containers@1.0.0.0 · 91 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as MD
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/index.bend as IX
8
9# The word-list walks of proofs/bitset/model.bend, re-expressed as a single
10# indexed access. This is the step that lets src/bitset.bend address the word
11# directly (Base.Array, O(1)) instead of walking the list:
12#
13# get_walk(ws, i) = word_get(word wordix(i) of ws, bitix(i))
14# put_walk(ws, i, v) = ws with word wordix(i) replaced by
15# word_put(v, that word, bitix(i))
16
17# Word q of the list (0 beyond the end; the callers always stay in range).
18def nthw(ws: List<&2, U32>, q: Nat) -> U32:
19 match ws q:
20 case Nil{} _:
21 0
22 case Con{w, t} 0n:
23 w
24 case Con{w, t} 1n+p:
25 nthw(t, p)
26
27def shrn_zero(+k: Nat) -> {U32.shrn(0, k) == 0 : U32}:
28 match k:
29 case 0n:
30 {==}
31 case 1n+p:
32 %Equal.sym(U32, U32.shrn(0, p), 0, shrn_zero(p)) : {U32.shr(_) == 0 : U32}
33 {==}
34
35def word_get_zero(+k: Nat) -> {B.word_get(0, k) == False{} : Bool}:
36 %Equal.sym(U32, U32.shrn(0, k), 0, shrn_zero(k)) : {B.low(_) == False{} : Bool}
37 {==}
38
39# ---- get ----
40
41def get_case(+w: U32, +t: List<&2, U32>, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +ih: {MD.get_walk(t, Nat.sub(i, 32n)) == B.word_get(nthw(t, B.wordix(Nat.sub(i, 32n))), B.bitix(Nat.sub(i, 32n))) : Bool}) -> {MD.get_pick(b, w, i, MD.get_walk(t, Nat.sub(i, 32n))) == B.word_get(nthw(Con{w, t}, B.wordix(i)), B.bitix(i)) : Bool}:
42 match b:
43 case True{}:
44 %Equal.sym(Nat, B.wordix(i), 0n, IX.wordix_small(i, eb)) : {B.word_get(w, i) == B.word_get(nthw(Con{w, t}, _), B.bitix(i)) : Bool}
45 %Equal.sym(Nat, B.bitix(i), i, IX.bitix_small(i, eb)) : {B.word_get(w, i) == B.word_get(w, _) : Bool}
46 {==}
47 case False{}:
48 %Equal.sym(Nat, B.wordix(i), 1n+B.wordix(Nat.sub(i, 32n)), IX.wordix_step(i, eb)) : {MD.get_walk(t, Nat.sub(i, 32n)) == B.word_get(nthw(Con{w, t}, _), B.bitix(i)) : Bool}
49 %Equal.sym(Nat, B.bitix(i), B.bitix(Nat.sub(i, 32n)), IX.bitix_step(i, eb)) : {MD.get_walk(t, Nat.sub(i, 32n)) == B.word_get(nthw(t, B.wordix(Nat.sub(i, 32n))), _) : Bool}
50 ih
51
52def get_index(ws: List<&2, U32>, +i: Nat) -> {MD.get_walk(ws, i) == B.word_get(nthw(ws, B.wordix(i)), B.bitix(i)) : Bool}:
53 match ws:
54 case Nil{}:
55 Equal.sym(Bool, B.word_get(0, B.bitix(i)), False{}, word_get_zero(B.bitix(i)))
56 case Con{+w, +t}:
57 get_case(w, t, i, Nat.is_lt(i, 32n), {==}, get_index(t, Nat.sub(i, 32n)))
58
59# ---- put ----
60
61def put_case(+v: Bool, +w: U32, +t: List<&2, U32>, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +ih: {MD.put_walk(t, Nat.sub(i, 32n), v) == SC.update(U32, t, B.wordix(Nat.sub(i, 32n)), B.word_put(v, nthw(t, B.wordix(Nat.sub(i, 32n))), B.bitix(Nat.sub(i, 32n)))) : List<&2, U32>}) -> {MD.put_pick(b, v, w, i, t, MD.put_walk(t, Nat.sub(i, 32n), v)) == SC.update(U32, Con{w, t}, B.wordix(i), B.word_put(v, nthw(Con{w, t}, B.wordix(i)), B.bitix(i))) : List<&2, U32>}:
62 match b:
63 case True{}:
64 %Equal.sym(Nat, B.wordix(i), 0n, IX.wordix_small(i, eb)) : {Con{B.word_put(v, w, i), t} == SC.update(U32, Con{w, t}, _, B.word_put(v, nthw(Con{w, t}, _), B.bitix(i))) : List<&2, U32>}
65 %Equal.sym(Nat, B.bitix(i), i, IX.bitix_small(i, eb)) : {Con{B.word_put(v, w, i), t} == Con{B.word_put(v, w, _), t} : List<&2, U32>}
66 {==}
67 case False{}:
68 %Equal.sym(Nat, B.wordix(i), 1n+B.wordix(Nat.sub(i, 32n)), IX.wordix_step(i, eb)) : {Con{w, MD.put_walk(t, Nat.sub(i, 32n), v)} == SC.update(U32, Con{w, t}, _, B.word_put(v, nthw(Con{w, t}, _), B.bitix(i))) : List<&2, U32>}
69 %Equal.sym(Nat, B.bitix(i), B.bitix(Nat.sub(i, 32n)), IX.bitix_step(i, eb)) : {Con{w, MD.put_walk(t, Nat.sub(i, 32n), v)} == Con{w, SC.update(U32, t, B.wordix(Nat.sub(i, 32n)), B.word_put(v, nthw(t, B.wordix(Nat.sub(i, 32n))), _))} : List<&2, U32>}
70 Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{w, z},
71 MD.put_walk(t, Nat.sub(i, 32n), v),
72 SC.update(U32, t, B.wordix(Nat.sub(i, 32n)), B.word_put(v, nthw(t, B.wordix(Nat.sub(i, 32n))), B.bitix(Nat.sub(i, 32n)))),
73 ih)
74
75def put_index(ws: List<&2, U32>, +i: Nat, +v: Bool) -> {MD.put_walk(ws, i, v) == SC.update(U32, ws, B.wordix(i), B.word_put(v, nthw(ws, B.wordix(i)), B.bitix(i))) : List<&2, U32>}:
76 match ws:
77 case Nil{}:
78 {==}
79 case Con{+w, +t}:
80 put_case(v, w, t, i, Nat.is_lt(i, 32n), {==}, put_index(t, Nat.sub(i, 32n), v))
81
82# ---- nthw is nth in range ----
83
84def nthw_nth(ws: List<&2, U32>, q: Nat, +h: {Nat.is_lt(q, SC.length(U32, ws)) == True{} : Bool}) -> {SC.nth(U32, ws, q) == Some{nthw(ws, q)} : Maybe<&2, U32>}:
85 match ws q:
86 case Nil{} _:
87 Empty.absurd({SC.nth(U32, Nil{}, q) == Some{nthw(Nil{}, q)} : Maybe<&2, U32>}, N.lt_zero_absurd(q, h))
88 case Con{w, t} 0n:
89 {==}
90 case Con{w, t} 1n+p:
91 nthw_nth(t, p, h)