1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/array.bend as A 6 import ../../../spec/lib/common.bend as SC 7 import ../../../src/containers/bitset.bend as B 8 import ./model.bend as MD 9 import ./walk.bend as WK 10 import ./listx.bend as LX 11 import ./arr.bend as AR 12 import ./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 20 def ztree(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree, +tb: A.Tree, +q: Nat) -> A.Tree: 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 27 def 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 36 def zip_go_ok(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree, +tb: A.Tree, +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 & Array}: 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 & 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 & Array} 44 %Equal.sym(Array & 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 & Array} 45 %Equal.sym(Array, 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 & Array} 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 50 def ztree_ws(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree, +tb: A.Tree, +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 60 def ztree_perfect(m: Nat, +k: B.WordOp, +d: Nat, +ta: A.Tree, +tb: A.Tree, +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 70 def 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 98 def 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 104 def 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))