proofs/containers/bitset/zip.bend
bend-collections-laws-containers@1.0.0.0 · 110 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/array.bend as A
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as MD
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/walk.bend as WK
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/listx.bend as LX
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/arr.bend as AR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/loops.bend as LP
13
14# The word-wise combination loop `zip_go` of src/bitset.bend writes
15# `word_op(k, a[q], b[q])` into a[q] for every q, leaving b alone. Three
16# steps: the loop follows the mirror tree `ztree`, the slot list of that tree
17# is the list-level `zl`, and `zl` over the whole array is exactly
18# `MD.zip_words`.
19
20def ztree(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +q: Nat) -> A.Tree<B.Wd>:
21 match m:
22 case 0n:
23 ta
24 case 1n+ +r:
25 ztree(r, k, d, A.upd(B.Wd, d, ta, q, B.W{B.word_op(k, WK.nthw(AR.ws(ta), q), WK.nthw(AR.ws(tb), q))}), tb, 1n+q)
26
27def zl(m: Nat, +k: B.WordOp, +q: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>) -> List<&2, U32>:
28 match m:
29 case 0n:
30 xs
31 case 1n+ +r:
32 zl(r, k, 1n+q, SC.update(U32, xs, q, B.word_op(k, WK.nthw(xs, q), WK.nthw(ys, q))), ys)
33
34# ---- the loop follows the mirror tree ----
35
36def zip_go_ok(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +q: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +pa: {A.perfect(B.Wd, d, ta) == True{} : Bool}, +pb: {A.perfect(B.Wd, d, tb) == True{} : Bool}, +hm: {Nat.is_le(Nat.add(q, m), SC.pow2(d)) == True{} : Bool}) -> {B.zip_go(m, (A.thaw(B.Wd, ta), A.thaw(B.Wd, tb)), k, d, q) == (A.thaw(B.Wd, ztree(m, k, d, ta, tb, q)), A.thaw(B.Wd, tb)) : Array<B.Wd> & Array<B.Wd>}:
37 match m:
38 case 0n:
39 {==}
40 case 1n+ +r:
41 +hq = LP.lt_of_sum(q, r, SC.pow2(d), hm)
42 +w = B.word_op(k, WK.nthw(AR.ws(ta), q), WK.nthw(AR.ws(tb), q))
43 %Equal.sym(Array<B.Wd> & U32, B.read(A.thaw(B.Wd, ta), d, q), (A.thaw(B.Wd, ta), WK.nthw(AR.ws(ta), q)), AR.read_ok(d, ta, q, hd, hq, pa)) : {B.zip_go(r, B.zip_write(_, B.read(A.thaw(B.Wd, tb), d, q), k, d, q), k, d, 1n+q) == (A.thaw(B.Wd, ztree(1n+r, k, d, ta, tb, q)), A.thaw(B.Wd, tb)) : Array<B.Wd> & Array<B.Wd>}
44 %Equal.sym(Array<B.Wd> & U32, B.read(A.thaw(B.Wd, tb), d, q), (A.thaw(B.Wd, tb), WK.nthw(AR.ws(tb), q)), AR.read_ok(d, tb, q, hd, hq, pb)) : {B.zip_go(r, B.zip_write((A.thaw(B.Wd, ta), WK.nthw(AR.ws(ta), q)), _, k, d, q), k, d, 1n+q) == (A.thaw(B.Wd, ztree(1n+r, k, d, ta, tb, q)), A.thaw(B.Wd, tb)) : Array<B.Wd> & Array<B.Wd>}
45 %Equal.sym(Array<B.Wd>, B.write(A.thaw(B.Wd, ta), d, q, w), A.thaw(B.Wd, A.upd(B.Wd, d, ta, q, B.W{w})), AR.write_ok(d, ta, q, w, hd, hq, pa)) : {B.zip_go(r, (_, A.thaw(B.Wd, tb)), k, d, 1n+q) == (A.thaw(B.Wd, ztree(1n+r, k, d, ta, tb, q)), A.thaw(B.Wd, tb)) : Array<B.Wd> & Array<B.Wd>}
46 zip_go_ok(r, k, d, A.upd(B.Wd, d, ta, q, B.W{w}), tb, 1n+q, hd, AR.upd_perfect(d, ta, q, w, pa), pb, LP.le_of_sum(q, r, SC.pow2(d), hm))
47
48# ---- the slots of the mirror tree are the list-level zl ----
49
50def ztree_ws(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +q: Nat, +pa: {A.perfect(B.Wd, d, ta) == True{} : Bool}, +hm: {Nat.is_le(Nat.add(q, m), SC.pow2(d)) == True{} : Bool}) -> {AR.ws(ztree(m, k, d, ta, tb, q)) == zl(m, k, q, AR.ws(ta), AR.ws(tb)) : List<&2, U32>}:
51 match m:
52 case 0n:
53 {==}
54 case 1n+ +r:
55 +hq = LP.lt_of_sum(q, r, SC.pow2(d), hm)
56 +w = B.word_op(k, WK.nthw(AR.ws(ta), q), WK.nthw(AR.ws(tb), q))
57 %AR.ws_upd(d, ta, q, w, hq, pa) : {AR.ws(ztree(r, k, d, A.upd(B.Wd, d, ta, q, B.W{w}), tb, 1n+q)) == zl(r, k, 1n+q, _, AR.ws(tb)) : List<&2, U32>}
58 ztree_ws(r, k, d, A.upd(B.Wd, d, ta, q, B.W{w}), tb, 1n+q, AR.upd_perfect(d, ta, q, w, pa), LP.le_of_sum(q, r, SC.pow2(d), hm))
59
60def ztree_perfect(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +q: Nat, +pa: {A.perfect(B.Wd, d, ta) == True{} : Bool}) -> {A.perfect(B.Wd, d, ztree(m, k, d, ta, tb, q)) == True{} : Bool}:
61 match m:
62 case 0n:
63 pa
64 case 1n+ +r:
65 +w = B.word_op(k, WK.nthw(AR.ws(ta), q), WK.nthw(AR.ws(tb), q))
66 ztree_perfect(r, k, d, A.upd(B.Wd, d, ta, q, B.W{w}), tb, 1n+q, AR.upd_perfect(d, ta, q, w, pa))
67
68# ---- zl is zip_words on the whole list ----
69
70def zl_spec(m: Nat, +k: B.WordOp, +q: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +hx: {Nat.add(q, m) == SC.length(U32, xs) : Nat}, +hy: {SC.length(U32, ys) == SC.length(U32, xs) : Nat}) -> {zl(m, k, q, xs, ys) == SC.append(U32, SC.take(U32, xs, q), MD.zip_words(k, SC.drop(U32, xs, q), SC.drop(U32, ys, q))) : List<&2, U32>}:
71 match m:
72 case 0n:
73 +eq = Equal.trans(Nat, q, Nat.add(q, 0n), SC.length(U32, xs), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q)), hx)
74 %Equal.sym(Nat, q, SC.length(U32, xs), eq) : {xs == SC.append(U32, SC.take(U32, xs, _), MD.zip_words(k, SC.drop(U32, xs, _), SC.drop(U32, ys, _))) : List<&2, U32>}
75 %Equal.sym(List<&2, U32>, SC.drop(U32, xs, SC.length(U32, xs)), Nil{}, LX.drop_all(U32, xs)) : {xs == SC.append(U32, SC.take(U32, xs, SC.length(U32, xs)), MD.zip_words(k, _, SC.drop(U32, ys, SC.length(U32, xs)))) : List<&2, U32>}
76 %Equal.sym(List<&2, U32>, SC.take(U32, xs, SC.length(U32, xs)), xs, LX.take_all(U32, xs)) : {xs == SC.append(U32, _, Nil{}) : List<&2, U32>}
77 Equal.sym(List<&2, U32>, SC.append(U32, xs, Nil{}), xs, LL.append_nil(U32, xs))
78 case 1n+ +r:
79 +hq = LP.lt_of_sum(q, r, SC.length(U32, xs), N.eq_le(Nat.add(q, 1n+r), SC.length(U32, xs), hx))
80 +hqy = L.subst(Nat, z => {Nat.is_lt(q, z) == True{} : Bool}, SC.length(U32, xs), SC.length(U32, ys), Equal.sym(Nat, SC.length(U32, ys), SC.length(U32, xs), hy), hq)
81 +a = WK.nthw(xs, q)
82 +b = WK.nthw(ys, q)
83 +w = B.word_op(k, a, b)
84 +ex = Equal.sym(List<&2, U32>, SC.drop(U32, xs, q), Con{a, SC.drop(U32, xs, 1n+q)}, LX.drop_cons(U32, xs, q, a, WK.nthw_nth(xs, q, hq)))
85 +ey = Equal.sym(List<&2, U32>, SC.drop(U32, ys, q), Con{b, SC.drop(U32, ys, 1n+q)}, LX.drop_cons(U32, ys, q, b, WK.nthw_nth(ys, q, hqy)))
86 +len2 = Equal.trans(Nat, SC.length(U32, SC.update(U32, xs, q, w)), SC.length(U32, xs), Nat.add(1n+q, r),
87 LL.length_update(U32, xs, q, w),
88 Equal.sym(Nat, Nat.add(1n+q, r), SC.length(U32, xs), Equal.trans(Nat, Nat.add(1n+q, r), Nat.add(q, 1n+r), SC.length(U32, xs), Equal.sym(Nat, Nat.add(q, 1n+r), Nat.add(1n+q, r), N.add_succ(q, r)), hx)))
89 +ih = zl_spec(r, k, 1n+q, SC.update(U32, xs, q, w), ys, Equal.sym(Nat, SC.length(U32, SC.update(U32, xs, q, w)), Nat.add(1n+q, r), len2),
90 Equal.trans(Nat, SC.length(U32, ys), SC.length(U32, xs), SC.length(U32, SC.update(U32, xs, q, w)), hy, Equal.sym(Nat, SC.length(U32, SC.update(U32, xs, q, w)), SC.length(U32, xs), LL.length_update(U32, xs, q, w))))
91 %ex : {zl(1n+r, k, q, xs, ys) == SC.append(U32, SC.take(U32, xs, q), MD.zip_words(k, _, SC.drop(U32, ys, q))) : List<&2, U32>}
92 %ey : {zl(1n+r, k, q, xs, ys) == SC.append(U32, SC.take(U32, xs, q), MD.zip_words(k, Con{a, SC.drop(U32, xs, 1n+q)}, _)) : List<&2, U32>}
93 %LL.snoc_append_cons(U32, SC.take(U32, xs, q), w, MD.zip_words(k, SC.drop(U32, xs, 1n+q), SC.drop(U32, ys, 1n+q))) : {zl(1n+r, k, q, xs, ys) == _ : List<&2, U32>}
94 %LX.take_update_succ(U32, xs, q, w, hq) : {zl(1n+r, k, q, xs, ys) == SC.append(U32, _, MD.zip_words(k, SC.drop(U32, xs, 1n+q), SC.drop(U32, ys, 1n+q))) : List<&2, U32>}
95 %LX.drop_update(U32, xs, q, w) : {zl(1n+r, k, q, xs, ys) == SC.append(U32, SC.take(U32, SC.update(U32, xs, q, w), 1n+q), MD.zip_words(k, _, SC.drop(U32, ys, 1n+q))) : List<&2, U32>}
96 ih
97
98def zl_edges(+k: B.WordOp, +xs: List<&2, U32>, +ys: List<&2, U32>) -> {SC.append(U32, SC.take(U32, xs, 0n), MD.zip_words(k, SC.drop(U32, xs, 0n), SC.drop(U32, ys, 0n))) == MD.zip_words(k, xs, ys) : List<&2, U32>}:
99 %Equal.sym(List<&2, U32>, SC.take(U32, xs, 0n), Nil{}, LX.take_zero(U32, xs)) : {SC.append(U32, _, MD.zip_words(k, SC.drop(U32, xs, 0n), SC.drop(U32, ys, 0n))) == MD.zip_words(k, xs, ys) : List<&2, U32>}
100 %Equal.sym(List<&2, U32>, SC.drop(U32, xs, 0n), xs, LX.drop_zero(U32, xs)) : {MD.zip_words(k, _, SC.drop(U32, ys, 0n)) == MD.zip_words(k, xs, ys) : List<&2, U32>}
101 %Equal.sym(List<&2, U32>, SC.drop(U32, ys, 0n), ys, LX.drop_zero(U32, ys)) : {MD.zip_words(k, xs, _) == MD.zip_words(k, xs, ys) : List<&2, U32>}
102 {==}
103
104def zl_full(+k: B.WordOp, +xs: List<&2, U32>, +ys: List<&2, U32>, +hy: {SC.length(U32, ys) == SC.length(U32, xs) : Nat}) -> {zl(SC.length(U32, xs), k, 0n, xs, ys) == MD.zip_words(k, xs, ys) : List<&2, U32>}:
105 Equal.trans(List<&2, U32>,
106 zl(SC.length(U32, xs), k, 0n, xs, ys),
107 SC.append(U32, SC.take(U32, xs, 0n), MD.zip_words(k, SC.drop(U32, xs, 0n), SC.drop(U32, ys, 0n))),
108 MD.zip_words(k, xs, ys),
109 zl_spec(SC.length(U32, xs), k, 0n, xs, ys, {==}, hy),
110 zl_edges(k, xs, ys))