proofs/containers/bitset/arr.bend
bend-collections-laws-containers@1.0.0.0 · 131 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/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as A
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as MD
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/walk.bend as WK
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/listx.bend as LX
12
13# The bridge between src/bitset.bend's native Base.Array of words and the
14# word list the rest of the proof talks about.
15#
16# Arrays are linear, so (exactly as in proofs/dynamic_array) every statement
17# is about `A.thaw(t)`, the array built from a Data mirror tree `t` of the
18# same shape; `ws(t)` is the list of the words it holds.
19
20def wmap(xs: List<&2, B.Wd>) -> List<&2, U32>:
21 match xs:
22 case Nil{}:
23 Nil{}
24 case Con{x, t}:
25 Con{B.wval(x), wmap(t)}
26
27def ws(t: A.Tree<B.Wd>) -> List<&2, U32>:
28 wmap(A.slots(B.Wd, t))
29
30# Slot q of a word list (the callers always stay in range; the default keeps
31# the function total and agrees with WK.nthw's default).
32def nths(xs: List<&2, B.Wd>, q: Nat) -> B.Wd:
33 match xs q:
34 case Nil{} _:
35 B.W{0}
36 case Con{x, t} 0n:
37 x
38 case Con{x, t} 1n+p:
39 nths(t, p)
40
41# ---- wmap ----
42
43def wmap_length(xs: List<&2, B.Wd>) -> {SC.length(U32, wmap(xs)) == SC.length(B.Wd, xs) : Nat}:
44 match xs:
45 case Nil{}:
46 {==}
47 case Con{x, +t}:
48 N.succ_cong(SC.length(U32, wmap(t)), SC.length(B.Wd, t), wmap_length(t))
49
50def wmap_update(xs: List<&2, B.Wd>, q: Nat, +v: U32) -> {wmap(SC.update(B.Wd, xs, q, B.W{v})) == SC.update(U32, wmap(xs), q, v) : List<&2, U32>}:
51 match xs q:
52 case Nil{} _:
53 {==}
54 case Con{x, t} 0n:
55 {==}
56 case Con{+x, +t} 1n+p:
57 Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{B.wval(x), z},
58 wmap(SC.update(B.Wd, t, p, B.W{v})), SC.update(U32, wmap(t), p, v), wmap_update(t, p, v))
59
60def wval_nths(xs: List<&2, B.Wd>, q: Nat) -> {B.wval(nths(xs, q)) == WK.nthw(wmap(xs), q) : U32}:
61 match xs q:
62 case Nil{} _:
63 {==}
64 case Con{x, t} 0n:
65 {==}
66 case Con{x, t} 1n+p:
67 wval_nths(t, p)
68
69def nths_nth(xs: List<&2, B.Wd>, q: Nat, +h: {Nat.is_lt(q, SC.length(B.Wd, xs)) == True{} : Bool}) -> {SC.nth(B.Wd, xs, q) == Some{nths(xs, q)} : Maybe<&2, B.Wd>}:
70 match xs q:
71 case Nil{} _:
72 Empty.absurd({SC.nth(B.Wd, Nil{}, q) == Some{nths(Nil{}, q)} : Maybe<&2, B.Wd>}, N.lt_zero_absurd(q, h))
73 case Con{x, t} 0n:
74 {==}
75 case Con{x, t} 1n+p:
76 nths_nth(t, p, h)
77
78# ---- shape ----
79
80def ws_length(+d: Nat, +t: A.Tree<B.Wd>, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {SC.length(U32, ws(t)) == SC.pow2(d) : Nat}:
81 Equal.trans(Nat, SC.length(U32, wmap(A.slots(B.Wd, t))), SC.length(B.Wd, A.slots(B.Wd, t)), SC.pow2(d),
82 wmap_length(A.slots(B.Wd, t)), A.slots_length(B.Wd, d, t, pf))
83
84def slots_lt(+d: Nat, +t: A.Tree<B.Wd>, +q: Nat, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(q, SC.length(B.Wd, A.slots(B.Wd, t))) == True{} : Bool}:
85 L.subst(Nat, k => {Nat.is_lt(q, k) == True{} : Bool}, SC.pow2(d), SC.length(B.Wd, A.slots(B.Wd, t)),
86 Equal.sym(Nat, SC.length(B.Wd, A.slots(B.Wd, t)), SC.pow2(d), A.slots_length(B.Wd, d, t, pf)), hq)
87
88def idx_ok(+d: Nat, +q: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(q)) == q : Nat}:
89 U.to_nat_from_nat(q, d, N.lt_le(d, 32n, hd), hq)
90
91# ---- read ----
92
93def read_ok(+d: Nat, +t: A.Tree<B.Wd>, +q: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {B.read(A.thaw(B.Wd, t), d, q) == (A.thaw(B.Wd, t), WK.nthw(ws(t), q)) : Array<B.Wd> & U32}:
94 %wval_nths(A.slots(B.Wd, t), q) : {B.read(A.thaw(B.Wd, t), d, q) == (A.thaw(B.Wd, t), _) : Array<B.Wd> & U32}
95 Equal.cong(Array<B.Wd> & B.Wd, Array<B.Wd> & U32, B.read_fin,
96 Array.get(B.Wd, A.thaw(B.Wd, t), U32.from_nat(q)),
97 (A.thaw(B.Wd, t), nths(A.slots(B.Wd, t), q)),
98 A.get(B.Wd, d, t, U32.from_nat(q), nths(A.slots(B.Wd, t), q), hd,
99 L.subst(Nat, j => {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), hq),
100 L.subst(Nat, j => {SC.nth(B.Wd, A.slots(B.Wd, t), j) == Some{nths(A.slots(B.Wd, t), q)} : Maybe<&2, B.Wd>}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), nths_nth(A.slots(B.Wd, t), q, slots_lt(d, t, q, pf, hq))),
101 pf))
102
103# ---- write ----
104
105def write_ok(+d: Nat, +t: A.Tree<B.Wd>, +q: Nat, +v: U32, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {B.write(A.thaw(B.Wd, t), d, q, v) == A.thaw(B.Wd, A.upd(B.Wd, d, t, q, B.W{v})) : Array<B.Wd>}:
106 %idx_ok(d, q, hd, hq) : {B.write(A.thaw(B.Wd, t), d, q, v) == A.thaw(B.Wd, A.upd(B.Wd, d, t, _, B.W{v})) : Array<B.Wd>}
107 A.set(B.Wd, d, t, U32.from_nat(q), B.W{v}, nths(A.slots(B.Wd, t), q), hd,
108 L.subst(Nat, j => {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), hq),
109 L.subst(Nat, j => {SC.nth(B.Wd, A.slots(B.Wd, t), j) == Some{nths(A.slots(B.Wd, t), q)} : Maybe<&2, B.Wd>}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), nths_nth(A.slots(B.Wd, t), q, slots_lt(d, t, q, pf, hq))),
110 pf)
111
112def ws_upd(+d: Nat, +t: A.Tree<B.Wd>, +q: Nat, +v: U32, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {ws(A.upd(B.Wd, d, t, q, B.W{v})) == SC.update(U32, ws(t), q, v) : List<&2, U32>}:
113 Equal.trans(List<&2, U32>, wmap(A.slots(B.Wd, A.upd(B.Wd, d, t, q, B.W{v}))), wmap(SC.update(B.Wd, A.slots(B.Wd, t), q, B.W{v})), SC.update(U32, wmap(A.slots(B.Wd, t)), q, v),
114 Equal.cong(List<&2, B.Wd>, List<&2, U32>, wmap, A.slots(B.Wd, A.upd(B.Wd, d, t, q, B.W{v})), SC.update(B.Wd, A.slots(B.Wd, t), q, B.W{v}), A.upd_slots(B.Wd, d, t, q, B.W{v}, hq, pf)),
115 wmap_update(A.slots(B.Wd, t), q, v))
116
117def upd_perfect(+d: Nat, +t: A.Tree<B.Wd>, +q: Nat, +v: U32, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {A.perfect(B.Wd, d, A.upd(B.Wd, d, t, q, B.W{v})) == True{} : Bool}:
118 A.upd_perfect(B.Wd, d, t, q, B.W{v}, pf)
119
120def wmap_replicate(+m: Nat, +v: U32) -> {wmap(SC.replicate(B.Wd, m, B.W{v})) == SC.replicate(U32, m, v) : List<&2, U32>}:
121 match m:
122 case 0n:
123 {==}
124 case 1n+p:
125 Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{v, z},
126 wmap(SC.replicate(B.Wd, p, B.W{v})), SC.replicate(U32, p, v), wmap_replicate(p, v))
127
128def ws_trep(+d: Nat, +v: U32) -> {ws(A.trep(B.Wd, d, B.W{v})) == SC.replicate(U32, SC.pow2(d), v) : List<&2, U32>}:
129 Equal.trans(List<&2, U32>, wmap(A.slots(B.Wd, A.trep(B.Wd, d, B.W{v}))), wmap(SC.replicate(B.Wd, SC.pow2(d), B.W{v})), SC.replicate(U32, SC.pow2(d), v),
130 Equal.cong(List<&2, B.Wd>, List<&2, U32>, wmap, A.slots(B.Wd, A.trep(B.Wd, d, B.W{v})), SC.replicate(B.Wd, SC.pow2(d), B.W{v}), A.trep_slots(B.Wd, d, B.W{v})),
131 wmap_replicate(SC.pow2(d), v))