proofs/containers/bitset/steps.bend
bend-collections-laws-containers@1.0.0.0 · 520 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as P2
3import bend-collections-laws-containers@1.0.0.0/proofs/math/pow2/pow2.bend as PT
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as A
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as S
10import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
11import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitset.bend as E
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/lists.bend as BL
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as MD
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/walk.bend as WK
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/arr.bend as AR
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/loops.bend as LP
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/zip.bend as ZP
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/depth.bend as DP
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/state.bend as ST
20
21# Every public operation (errors included) refines the spec step and keeps the
22# representation invariant; from_bools builds exactly the requested bit
23# sequence.
24#
25# Base.Array is linear, so a step is stated as: the real operation on the
26# array of a good shadow produces the array of another good shadow, whose
27# model and observation are the spec step of the first shadow's model.
28
29def StepOK(sh: ST.Sh, op: E.Op) -> Type:
30 Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, E.Obs, o => {B.step(ST.real(sh), op) == (ST.real(sh2), o) : B.Bitset & E.Obs} & ({ST.good(sh2) == True{} : Bool} & {(ST.model(sh2), o) == S.step(ST.model(sh), op) : List<&2, Bool> & E.Obs})>>
31
32# ---- shared index facts ----
33
34def n_le_cap(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {ST.rep(n, d, t) == True{} : Bool}) -> {Nat.is_le(n, Nat.mul(SC.pow2(d), 32n)) == True{} : Bool}:
35 L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, SC.length(Bool, ST.flat(AR.ws(t))), Nat.mul(SC.pow2(d), 32n),
36 ST.flat_len(d, t, ST.rep_perfect(n, d, t, g)), ST.inv_le(n, ST.flat(AR.ws(t)), ST.rep_invf(n, d, t, g)))
37
38def wix(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +g: {ST.rep(n, d, t) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {Nat.is_lt(B.wordix(i), SC.pow2(d)) == True{} : Bool}:
39 ST.wordix_lt(i, SC.pow2(d), N.lt_le_trans(i, n, Nat.mul(SC.pow2(d), 32n), hi, n_le_cap(n, d, t, g)))
40
41# ---- length ----
42
43def length_ok(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {ST.rep(n, d, t) == True{} : Bool}) -> StepOK(ST.Sh{n, d, t}, E.Length{}):
44 (ST.Sh{n, d, t}, (E.ONat{n}, ({==}, (g,
45 %Equal.sym(Nat, SC.length(Bool, ST.abs(n, t)), n, ST.length_abs(n, ST.flat(AR.ws(t)), ST.rep_invf(n, d, t, g))) : {(ST.abs(n, t), E.ONat{n}) == (ST.abs(n, t), E.ONat{_}) : List<&2, Bool> & E.Obs}
46 {==}))))
47
48# ---- get ----
49
50def nth_in(+n: Nat, +ws: List<&2, U32>, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}, +g: {ST.invf(n, ST.flat(ws)) == True{} : Bool}) -> {Some{MD.get_walk(ws, i)} == SC.nth(Bool, SC.take(Bool, ST.flat(ws), n), i) : Maybe<&2, Bool>}:
51 Equal.trans(Maybe<&2, Bool>, Some{MD.get_walk(ws, i)}, SC.nth(Bool, ST.flat(ws), i), SC.nth(Bool, SC.take(Bool, ST.flat(ws), n), i),
52 ST.get_walk(ws, i, N.lt_le_trans(i, n, SC.length(Bool, ST.flat(ws)), h, ST.inv_le(n, ST.flat(ws), g))),
53 Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.take(Bool, ST.flat(ws), n), i), SC.nth(Bool, ST.flat(ws), i), BL.nth_take(ST.flat(ws), n, i, h)))
54
55def nth_out(+n: Nat, +ws: List<&2, U32>, +i: Nat, +h: {Nat.is_lt(i, n) == False{} : Bool}, +g: {ST.invf(n, ST.flat(ws)) == True{} : Bool}) -> {None{} == SC.nth(Bool, SC.take(Bool, ST.flat(ws), n), i) : Maybe<&2, Bool>}:
56 Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.take(Bool, ST.flat(ws), n), i), None{},
57 LL.nth_none(Bool, SC.take(Bool, ST.flat(ws), n), i, L.subst(Nat, k => {Nat.is_le(k, i) == True{} : Bool}, n, SC.length(Bool, SC.take(Bool, ST.flat(ws), n)), Equal.sym(Nat, SC.length(Bool, SC.take(Bool, ST.flat(ws), n)), n, ST.length_abs(n, ST.flat(ws), g)), N.not_lt_le(i, n, h))))
58
59def get_case(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}, +g: {ST.rep(n, d, t) == True{} : Bool}) -> StepOK(ST.Sh{n, d, t}, E.Get{i}):
60 match b:
61 case True{}:
62 (ST.Sh{n, d, t}, (E.OBit{Done{MD.get_walk(AR.ws(t), i)}}, (
63 %Equal.sym(Bool, Nat.is_lt(i, n), True{}, eb) : {B.obs_bit(B.get_if(_, n, d, A.thaw(B.Wd, t), i)) == (ST.real(ST.Sh{n, d, t}), E.OBit{Done{MD.get_walk(AR.ws(t), i)}}) : B.Bitset & E.Obs}
64 %Equal.sym(Array<B.Wd> & U32, B.read(A.thaw(B.Wd, t), d, B.wordix(i)), (A.thaw(B.Wd, t), WK.nthw(AR.ws(t), B.wordix(i))), AR.read_ok(d, t, B.wordix(i), ST.rep_lt(n, d, t, g), wix(n, d, t, i, g, eb), ST.rep_perfect(n, d, t, g))) : {B.obs_bit(B.get_read(_, n, d, B.bitix(i))) == (ST.real(ST.Sh{n, d, t}), E.OBit{Done{MD.get_walk(AR.ws(t), i)}}) : B.Bitset & E.Obs}
65 %WK.get_index(AR.ws(t), i) : {(B.BS{n, d, A.thaw(B.Wd, t)}, E.OBit{Done{_}}) == (ST.real(ST.Sh{n, d, t}), E.OBit{Done{MD.get_walk(AR.ws(t), i)}}) : B.Bitset & E.Obs}
66 {==},
67 (g,
68 %nth_in(n, AR.ws(t), i, eb, ST.rep_invf(n, d, t, g)) : {(ST.abs(n, t), E.OBit{Done{MD.get_walk(AR.ws(t), i)}}) == (ST.abs(n, t), E.OBit{S.bit(_)}) : List<&2, Bool> & E.Obs}
69 {==}))))
70 case False{}:
71 (ST.Sh{n, d, t}, (E.OBit{Fail{E.IndexOutOfRange{}}}, (
72 %Equal.sym(Bool, Nat.is_lt(i, n), False{}, eb) : {B.obs_bit(B.get_if(_, n, d, A.thaw(B.Wd, t), i)) == (ST.real(ST.Sh{n, d, t}), E.OBit{Fail{E.IndexOutOfRange{}}}) : B.Bitset & E.Obs}
73 {==},
74 (g,
75 %nth_out(n, AR.ws(t), i, eb, ST.rep_invf(n, d, t, g)) : {(ST.abs(n, t), E.OBit{Fail{E.IndexOutOfRange{}}}) == (ST.abs(n, t), E.OBit{S.bit(_)}) : List<&2, Bool> & E.Obs}
76 {==}))))
77
78# ---- set / clear ----
79
80def upd_tree(+d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +v: Bool) -> A.Tree<B.Wd>:
81 A.upd(B.Wd, d, t, B.wordix(i), B.W{B.word_put(v, WK.nthw(AR.ws(t), B.wordix(i)), B.bitix(i))})
82
83def upd_ws(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +v: Bool, +g: {ST.rep(n, d, t) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {AR.ws(upd_tree(d, t, i, v)) == MD.put_walk(AR.ws(t), i, v) : List<&2, U32>}:
84 Equal.trans(List<&2, U32>, AR.ws(upd_tree(d, t, i, v)), SC.update(U32, AR.ws(t), B.wordix(i), B.word_put(v, WK.nthw(AR.ws(t), B.wordix(i)), B.bitix(i))), MD.put_walk(AR.ws(t), i, v),
85 AR.ws_upd(d, t, B.wordix(i), B.word_put(v, WK.nthw(AR.ws(t), B.wordix(i)), B.bitix(i)), wix(n, d, t, i, g, hi), ST.rep_perfect(n, d, t, g)),
86 Equal.sym(List<&2, U32>, MD.put_walk(AR.ws(t), i, v), SC.update(U32, AR.ws(t), B.wordix(i), B.word_put(v, WK.nthw(AR.ws(t), B.wordix(i)), B.bitix(i))), WK.put_index(AR.ws(t), i, v)))
87
88def upd_rep(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +v: Bool, +g: {ST.rep(n, d, t) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {ST.rep(n, d, upd_tree(d, t, i, v)) == True{} : Bool}:
89 ST.rep_mk(n, d, upd_tree(d, t, i, v),
90 ST.rep_depth(n, d, t, g),
91 AR.upd_perfect(d, t, B.wordix(i), B.word_put(v, WK.nthw(AR.ws(t), B.wordix(i)), B.bitix(i)), ST.rep_perfect(n, d, t, g)),
92 L.subst(List<&2, U32>, z => {ST.invf(n, ST.flat(z)) == True{} : Bool}, MD.put_walk(AR.ws(t), i, v), AR.ws(upd_tree(d, t, i, v)),
93 Equal.sym(List<&2, U32>, AR.ws(upd_tree(d, t, i, v)), MD.put_walk(AR.ws(t), i, v), upd_ws(n, d, t, i, v, g, hi)),
94 ST.put_inv(n, AR.ws(t), i, v, hi, ST.rep_invf(n, d, t, g))))
95
96def upd_abs(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +v: Bool, +g: {ST.rep(n, d, t) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {ST.abs(n, upd_tree(d, t, i, v)) == SC.update(Bool, ST.abs(n, t), i, v) : List<&2, Bool>}:
97 L.subst(List<&2, U32>, z => {SC.take(Bool, ST.flat(z), n) == SC.update(Bool, ST.abs(n, t), i, v) : List<&2, Bool>}, MD.put_walk(AR.ws(t), i, v), AR.ws(upd_tree(d, t, i, v)),
98 Equal.sym(List<&2, U32>, AR.ws(upd_tree(d, t, i, v)), MD.put_walk(AR.ws(t), i, v), upd_ws(n, d, t, i, v, g, hi)),
99 ST.put_abs(n, AR.ws(t), i, v))
100
101def AssignOK(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +v: Bool, b: Bool) -> Type:
102 Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, Result<&2, &2, E.Error, Unit>, x => {B.assign_if(b, n, d, A.thaw(B.Wd, t), i, v) == (ST.real(sh2), x) : B.Bitset & Result<&2, &2, E.Error, Unit>} & ({ST.good(sh2) == True{} : Bool} & {(ST.model(sh2), E.OUnit{x}) == S.assign(ST.abs(n, t), i, v) : List<&2, Bool> & E.Obs})>>
103
104def assign_case(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +v: Bool, b: Bool, +eb: {Nat.is_lt(i, n) == b : Bool}, +g: {ST.rep(n, d, t) == True{} : Bool}) -> AssignOK(n, d, t, i, v, b):
105 match b:
106 case True{}:
107 (ST.Sh{n, d, upd_tree(d, t, i, v)}, (Done{Unit{}}, (
108 %Equal.sym(Array<B.Wd> & U32, B.read(A.thaw(B.Wd, t), d, B.wordix(i)), (A.thaw(B.Wd, t), WK.nthw(AR.ws(t), B.wordix(i))), AR.read_ok(d, t, B.wordix(i), ST.rep_lt(n, d, t, g), wix(n, d, t, i, g, eb), ST.rep_perfect(n, d, t, g))) : {B.assign_read(_, n, d, B.wordix(i), B.bitix(i), v) == (ST.real(ST.Sh{n, d, upd_tree(d, t, i, v)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
109 %Equal.sym(Array<B.Wd>, B.write(A.thaw(B.Wd, t), d, B.wordix(i), B.word_put(v, WK.nthw(AR.ws(t), B.wordix(i)), B.bitix(i))), A.thaw(B.Wd, upd_tree(d, t, i, v)), AR.write_ok(d, t, B.wordix(i), B.word_put(v, WK.nthw(AR.ws(t), B.wordix(i)), B.bitix(i)), ST.rep_lt(n, d, t, g), wix(n, d, t, i, g, eb), ST.rep_perfect(n, d, t, g))) : {(B.BS{n, d, _}, Done{Unit{}}) == (ST.real(ST.Sh{n, d, upd_tree(d, t, i, v)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
110 {==},
111 (upd_rep(n, d, t, i, v, g, eb),
112 %nth_in(n, AR.ws(t), i, eb, ST.rep_invf(n, d, t, g)) : {(ST.abs(n, upd_tree(d, t, i, v)), E.OUnit{Done{Unit{}}}) == S.assign_at(_, ST.abs(n, t), i, v) : List<&2, Bool> & E.Obs}
113 %Equal.sym(List<&2, Bool>, ST.abs(n, upd_tree(d, t, i, v)), SC.update(Bool, ST.abs(n, t), i, v), upd_abs(n, d, t, i, v, g, eb)) : {(_, E.OUnit{Done{Unit{}}}) == S.assign_at(Some{MD.get_walk(AR.ws(t), i)}, ST.abs(n, t), i, v) : List<&2, Bool> & E.Obs}
114 {==}))))
115 case False{}:
116 (ST.Sh{n, d, t}, (Fail{E.IndexOutOfRange{}}, ({==},
117 (g,
118 %nth_out(n, AR.ws(t), i, eb, ST.rep_invf(n, d, t, g)) : {(ST.abs(n, t), E.OUnit{Fail{E.IndexOutOfRange{}}}) == S.assign_at(_, ST.abs(n, t), i, v) : List<&2, Bool> & E.Obs}
119 {==}))))
120
121# ---- count and enumeration see only the logical bits ----
122
123def count_abs(+n: Nat, +xs: List<&2, Bool>, +g: {ST.invf(n, xs) == True{} : Bool}) -> {S.count(xs) == S.count(SC.take(Bool, xs, n)) : Nat}:
124 Equal.trans(Nat, S.count(xs), S.count(SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n))), S.count(SC.take(Bool, xs, n)),
125 Equal.cong(List<&2, Bool>, Nat, z => S.count(z), xs, SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)), ST.split(n, xs)),
126 %Equal.sym(Nat, S.count(SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n))), Nat.add(S.count(SC.take(Bool, xs, n)), S.count(SC.drop(Bool, xs, n))), BL.count_append(SC.take(Bool, xs, n), SC.drop(Bool, xs, n))) : {_ == S.count(SC.take(Bool, xs, n)) : Nat}
127 %Equal.sym(Nat, S.count(SC.drop(Bool, xs, n)), 0n, BL.count_allf(SC.drop(Bool, xs, n), ST.inv_tail(n, xs, g))) : {Nat.add(S.count(SC.take(Bool, xs, n)), _) == S.count(SC.take(Bool, xs, n)) : Nat}
128 N.add_zero(S.count(SC.take(Bool, xs, n))))
129
130def members_abs(+n: Nat, +xs: List<&2, Bool>, +g: {ST.invf(n, xs) == True{} : Bool}) -> {S.members(xs, 0n) == S.members(SC.take(Bool, xs, n), 0n) : List<&2, Nat>}:
131 Equal.trans(List<&2, Nat>, S.members(xs, 0n), S.members(SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)), 0n), S.members(SC.take(Bool, xs, n), 0n),
132 Equal.cong(List<&2, Bool>, List<&2, Nat>, z => S.members(z, 0n), xs, SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)), ST.split(n, xs)),
133 %Equal.sym(List<&2, Nat>, S.members(SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)), 0n), SC.append(Nat, S.members(SC.take(Bool, xs, n), 0n), S.members(SC.drop(Bool, xs, n), Nat.add(SC.length(Bool, SC.take(Bool, xs, n)), 0n))), BL.members_append(SC.take(Bool, xs, n), SC.drop(Bool, xs, n), 0n)) : {_ == S.members(SC.take(Bool, xs, n), 0n) : List<&2, Nat>}
134 %Equal.sym(List<&2, Nat>, S.members(SC.drop(Bool, xs, n), Nat.add(SC.length(Bool, SC.take(Bool, xs, n)), 0n)), Nil{}, BL.members_allf(SC.drop(Bool, xs, n), Nat.add(SC.length(Bool, SC.take(Bool, xs, n)), 0n), ST.inv_tail(n, xs, g))) : {SC.append(Nat, S.members(SC.take(Bool, xs, n), 0n), _) == S.members(SC.take(Bool, xs, n), 0n) : List<&2, Nat>}
135 LL.append_nil(Nat, S.members(SC.take(Bool, xs, n), 0n)))
136
137def count_ok(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {ST.rep(n, d, t) == True{} : Bool}) -> StepOK(ST.Sh{n, d, t}, E.Count{}):
138 (ST.Sh{n, d, t}, (E.ONat{MD.count_words(AR.ws(t))}, (
139 %Equal.sym(Nat, P2.pow2t(d), SC.pow2(d), PT.same(d)) : {B.obs_nat(B.count_fin(B.count_go(_, (A.thaw(B.Wd, t), 0n), d, 0n), n, d)) == (ST.real(ST.Sh{n, d, t}), E.ONat{MD.count_words(AR.ws(t))}) : B.Bitset & E.Obs}
140 %Equal.sym(Array<B.Wd> & Nat, B.count_go(SC.pow2(d), (A.thaw(B.Wd, t), 0n), d, 0n), (A.thaw(B.Wd, t), MD.count_words(AR.ws(t))), LP.count_ok(d, t, ST.rep_lt(n, d, t, g), ST.rep_perfect(n, d, t, g))) : {B.obs_nat(B.count_fin(_, n, d)) == (ST.real(ST.Sh{n, d, t}), E.ONat{MD.count_words(AR.ws(t))}) : B.Bitset & E.Obs}
141 {==},
142 (g,
143 %Equal.sym(Nat, MD.count_words(AR.ws(t)), S.count(ST.flat(AR.ws(t))), ST.count_words(AR.ws(t))) : {(ST.abs(n, t), E.ONat{_}) == (ST.abs(n, t), E.ONat{S.count(ST.abs(n, t))}) : List<&2, Bool> & E.Obs}
144 %Equal.sym(Nat, S.count(ST.flat(AR.ws(t))), S.count(ST.abs(n, t)), count_abs(n, ST.flat(AR.ws(t)), ST.rep_invf(n, d, t, g))) : {(ST.abs(n, t), E.ONat{_}) == (ST.abs(n, t), E.ONat{S.count(ST.abs(n, t))}) : List<&2, Bool> & E.Obs}
145 {==}))))
146
147def tolist_ok(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +g: {ST.rep(n, d, t) == True{} : Bool}) -> StepOK(ST.Sh{n, d, t}, E.ToList{}):
148 (ST.Sh{n, d, t}, (E.OList{MD.members_words(AR.ws(t), 0n)}, (
149 %Equal.sym(Nat, P2.pow2t(d), SC.pow2(d), PT.same(d)) : {B.obs_list(B.members_fin(B.members_go(_, (A.thaw(B.Wd, t), Nil{}), d), n, d)) == (ST.real(ST.Sh{n, d, t}), E.OList{MD.members_words(AR.ws(t), 0n)}) : B.Bitset & E.Obs}
150 %Equal.sym(Array<B.Wd> & List<&2, Nat>, B.members_go(SC.pow2(d), (A.thaw(B.Wd, t), Nil{}), d), (A.thaw(B.Wd, t), MD.members_words(AR.ws(t), 0n)), LP.to_list_ok(d, t, ST.rep_lt(n, d, t, g), ST.rep_perfect(n, d, t, g))) : {B.obs_list(B.members_fin(_, n, d)) == (ST.real(ST.Sh{n, d, t}), E.OList{MD.members_words(AR.ws(t), 0n)}) : B.Bitset & E.Obs}
151 {==},
152 (g,
153 %Equal.sym(List<&2, Nat>, MD.members_words(AR.ws(t), 0n), S.members(ST.flat(AR.ws(t)), 0n), ST.members_words(AR.ws(t), 0n)) : {(ST.abs(n, t), E.OList{_}) == (ST.abs(n, t), E.OList{S.members(ST.abs(n, t), 0n)}) : List<&2, Bool> & E.Obs}
154 %Equal.sym(List<&2, Nat>, S.members(ST.flat(AR.ws(t)), 0n), S.members(ST.abs(n, t), 0n), members_abs(n, ST.flat(AR.ws(t)), ST.rep_invf(n, d, t, g))) : {(ST.abs(n, t), E.OList{_}) == (ST.abs(n, t), E.OList{S.members(ST.abs(n, t), 0n)}) : List<&2, Bool> & E.Obs}
155 {==}))))
156
157# ---- from_bools builds the requested sequence ----
158
159def ao_sh(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -i: Nat, -v: Bool, -b: Bool, r: AssignOK(n, d, t, i, v, b)) -> ST.Sh:
160 match r:
161 case Tuple{sh2, x}:
162 sh2
163
164def ao_res(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -i: Nat, -v: Bool, -b: Bool, r: AssignOK(n, d, t, i, v, b)) -> Result<&2, &2, E.Error, Unit>:
165 match r:
166 case Tuple{sh2, Tuple{x, y}}:
167 x
168
169def ao_eq(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -i: Nat, -v: Bool, -b: Bool, r: AssignOK(n, d, t, i, v, b)) -> {B.assign_if(b, n, d, A.thaw(B.Wd, t), i, v) == (ST.real(ao_sh(n, d, t, i, v, b, r)), ao_res(n, d, t, i, v, b, r)) : B.Bitset & Result<&2, &2, E.Error, Unit>}:
170 match r:
171 case Tuple{sh2, Tuple{x, Tuple{e, y}}}:
172 e
173
174def ao_good(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -i: Nat, -v: Bool, -b: Bool, r: AssignOK(n, d, t, i, v, b)) -> {ST.good(ao_sh(n, d, t, i, v, b, r)) == True{} : Bool}:
175 match r:
176 case Tuple{sh2, Tuple{x, Tuple{e, Tuple{g, y}}}}:
177 g
178
179def ao_spec(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -i: Nat, -v: Bool, -b: Bool, r: AssignOK(n, d, t, i, v, b)) -> {(ST.model(ao_sh(n, d, t, i, v, b, r)), E.OUnit{ao_res(n, d, t, i, v, b, r)}) == S.assign(ST.abs(n, t), i, v) : List<&2, Bool> & E.Obs}:
180 match r:
181 case Tuple{sh2, Tuple{x, Tuple{e, Tuple{g, s}}}}:
182 s
183
184def assign_some(+n: Nat, +ws: List<&2, U32>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, n) == True{} : Bool}, +g: {ST.invf(n, ST.flat(ws)) == True{} : Bool}) -> {S.assign(SC.take(Bool, ST.flat(ws), n), i, v) == (SC.update(Bool, SC.take(Bool, ST.flat(ws), n), i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}:
185 %nth_in(n, ws, i, h, g) : {S.assign_at(_, SC.take(Bool, ST.flat(ws), n), i, v) == (SC.update(Bool, SC.take(Bool, ST.flat(ws), n), i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}
186 {==}
187
188def lt_add_succ(+a: Nat, +x: Nat) -> {Nat.is_lt(a, Nat.add(a, 1n+x)) == True{} : Bool}:
189 %Equal.sym(Nat, Nat.add(a, 1n+x), 1n+Nat.add(a, x), N.add_succ(a, x)) : {Nat.is_lt(a, _) == True{} : Bool}
190 N.le_lt_succ(a, Nat.add(a, x), N.le_add_right(a, x))
191
192def upd_snoc(+p: List<&2, Bool>, +r: List<&2, Bool>, +xs: List<&2, Bool>, +ea: {xs == SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}) : List<&2, Bool>}) -> {SC.update(Bool, xs, SC.length(Bool, p), True{}) == SC.append(Bool, SC.snoc(Bool, p, True{}), BL.rep(SC.length(Bool, r))) : List<&2, Bool>}:
193 %Equal.sym(List<&2, Bool>, xs, SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}), ea) : {SC.update(Bool, _, SC.length(Bool, p), True{}) == SC.append(Bool, SC.snoc(Bool, p, True{}), BL.rep(SC.length(Bool, r))) : List<&2, Bool>}
194 %Equal.sym(List<&2, Bool>, SC.update(Bool, SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}), SC.length(Bool, p), True{}), SC.append(Bool, p, SC.update(Bool, Con{False{}, BL.rep(SC.length(Bool, r))}, Nat.sub(SC.length(Bool, p), SC.length(Bool, p)), True{})), LL.update_append_right(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}, SC.length(Bool, p), True{}, N.le_refl(SC.length(Bool, p)))) : {_ == SC.append(Bool, SC.snoc(Bool, p, True{}), BL.rep(SC.length(Bool, r))) : List<&2, Bool>}
195 %Equal.sym(Nat, Nat.sub(SC.length(Bool, p), SC.length(Bool, p)), 0n, N.sub_self(SC.length(Bool, p))) : {SC.append(Bool, p, SC.update(Bool, Con{False{}, BL.rep(SC.length(Bool, r))}, _, True{})) == SC.append(Bool, SC.snoc(Bool, p, True{}), BL.rep(SC.length(Bool, r))) : List<&2, Bool>}
196 Equal.sym(List<&2, Bool>, SC.append(Bool, SC.snoc(Bool, p, True{}), BL.rep(SC.length(Bool, r))), SC.append(Bool, p, Con{True{}, BL.rep(SC.length(Bool, r))}), LL.snoc_append_cons(Bool, p, True{}, BL.rep(SC.length(Bool, r))))
197
198# The index the next bit goes to is inside the bitset.
199def pick_lt(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +p: List<&2, Bool>, +r: List<&2, Bool>, +g: {ST.rep(n, d, t) == True{} : Bool}, +ea: {ST.abs(n, t) == SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}) : List<&2, Bool>}) -> {Nat.is_lt(SC.length(Bool, p), n) == True{} : Bool}:
200 +el = Equal.trans(Nat, n, SC.length(Bool, ST.abs(n, t)), SC.length(Bool, SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))})),
201 Equal.sym(Nat, SC.length(Bool, ST.abs(n, t)), n, ST.length_abs(n, ST.flat(AR.ws(t)), ST.rep_invf(n, d, t, g))),
202 Equal.cong(List<&2, Bool>, Nat, z => SC.length(Bool, z), ST.abs(n, t), SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}), ea))
203 +el2 = Equal.trans(Nat, n, SC.length(Bool, SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))})), Nat.add(SC.length(Bool, p), 1n+SC.length(Bool, BL.rep(SC.length(Bool, r)))), el, LL.length_append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}))
204 L.subst(Nat, q => {Nat.is_lt(SC.length(Bool, p), q) == True{} : Bool}, Nat.add(SC.length(Bool, p), 1n+SC.length(Bool, BL.rep(SC.length(Bool, r)))), n, Equal.sym(Nat, n, Nat.add(SC.length(Bool, p), 1n+SC.length(Bool, BL.rep(SC.length(Bool, r)))), el2), lt_add_succ(SC.length(Bool, p), SC.length(Bool, BL.rep(SC.length(Bool, r)))))
205
206def PickOK(b: Bool, sh: ST.Sh, +p: List<&2, Bool>, +r: List<&2, Bool>) -> Type:
207 Sigma<&1, &1, ST.Sh, sh2 => {B.fill_pick(b, ST.real(sh), SC.length(Bool, p)) == ST.real(sh2) : B.Bitset} & ({ST.good(sh2) == True{} : Bool} & {ST.model(sh2) == SC.append(Bool, SC.snoc(Bool, p, b), BL.rep(SC.length(Bool, r))) : List<&2, Bool>})>
208
209def fill_drop_id(-s: B.Bitset, x: Result<&2, &2, E.Error, Unit>) -> {B.fill_drop(s, x) == s : B.Bitset}:
210 match x:
211 case Fail{e}:
212 {==}
213 case Done{u}:
214 {==}
215
216def AC(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +p: List<&2, Bool>, +g: {ST.rep(n, d, t) == True{} : Bool}) -> AssignOK(n, d, t, SC.length(Bool, p), True{}, Nat.is_lt(SC.length(Bool, p), n)):
217 assign_case(n, d, t, SC.length(Bool, p), True{}, Nat.is_lt(SC.length(Bool, p), n), {==}, g)
218
219def pick_ok(b: Bool, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +p: List<&2, Bool>, +r: List<&2, Bool>, +g: {ST.rep(n, d, t) == True{} : Bool}, +ea: {ST.abs(n, t) == SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}) : List<&2, Bool>}) -> PickOK(b, ST.Sh{n, d, t}, p, r):
220 match b:
221 case True{}:
222 +h = pick_lt(n, d, t, p, r, g, ea)
223 +sh2 = ao_sh(n, d, t, SC.length(Bool, p), True{}, Nat.is_lt(SC.length(Bool, p), n), AC(n, d, t, p, g))
224 +x = ao_res(n, d, t, SC.length(Bool, p), True{}, Nat.is_lt(SC.length(Bool, p), n), AC(n, d, t, p, g))
225 +em = Equal.trans(List<&2, Bool> & E.Obs, (ST.model(sh2), E.OUnit{x}), S.assign(ST.abs(n, t), SC.length(Bool, p), True{}), (SC.update(Bool, ST.abs(n, t), SC.length(Bool, p), True{}), E.OUnit{Done{Unit{}}}),
226 ao_spec(n, d, t, SC.length(Bool, p), True{}, Nat.is_lt(SC.length(Bool, p), n), AC(n, d, t, p, g)),
227 assign_some(n, AR.ws(t), SC.length(Bool, p), True{}, h, ST.rep_invf(n, d, t, g)))
228 (sh2, (
229 %Equal.sym(B.Bitset & Result<&2, &2, E.Error, Unit>, B.assign_if(Nat.is_lt(SC.length(Bool, p), n), n, d, A.thaw(B.Wd, t), SC.length(Bool, p), True{}), (ST.real(sh2), x), ao_eq(n, d, t, SC.length(Bool, p), True{}, Nat.is_lt(SC.length(Bool, p), n), AC(n, d, t, p, g))) : {B.fill_set(_) == ST.real(sh2) : B.Bitset}
230 fill_drop_id(ST.real(sh2), x),
231 (ao_good(n, d, t, SC.length(Bool, p), True{}, Nat.is_lt(SC.length(Bool, p), n), AC(n, d, t, p, g)),
232 Equal.trans(List<&2, Bool>, ST.model(sh2), SC.update(Bool, ST.abs(n, t), SC.length(Bool, p), True{}), SC.append(Bool, SC.snoc(Bool, p, True{}), BL.rep(SC.length(Bool, r))),
233 Equal.cong(List<&2, Bool> & E.Obs, List<&2, Bool>, z => Pair.fst(List<&2, Bool>, E.Obs, z), (ST.model(sh2), E.OUnit{x}), (SC.update(Bool, ST.abs(n, t), SC.length(Bool, p), True{}), E.OUnit{Done{Unit{}}}), em),
234 upd_snoc(p, r, ST.abs(n, t), ea)))))
235 case False{}:
236 (ST.Sh{n, d, t}, ({==},
237 (g,
238 Equal.trans(List<&2, Bool>, ST.abs(n, t), SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}), SC.append(Bool, SC.snoc(Bool, p, False{}), BL.rep(SC.length(Bool, r))), ea,
239 Equal.sym(List<&2, Bool>, SC.append(Bool, SC.snoc(Bool, p, False{}), BL.rep(SC.length(Bool, r))), SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}), LL.snoc_append_cons(Bool, p, False{}, BL.rep(SC.length(Bool, r))))))))
240
241def po_sh(-b: Bool, -sh: ST.Sh, -p: List<&2, Bool>, -r: List<&2, Bool>, z: PickOK(b, sh, p, r)) -> ST.Sh:
242 match z:
243 case Tuple{sh2, y}:
244 sh2
245
246def po_eq(-b: Bool, -sh: ST.Sh, -p: List<&2, Bool>, -r: List<&2, Bool>, z: PickOK(b, sh, p, r)) -> {B.fill_pick(b, ST.real(sh), SC.length(Bool, p)) == ST.real(po_sh(b, sh, p, r, z)) : B.Bitset}:
247 match z:
248 case Tuple{sh2, Tuple{e, y}}:
249 e
250
251def po_good(-b: Bool, -sh: ST.Sh, -p: List<&2, Bool>, -r: List<&2, Bool>, z: PickOK(b, sh, p, r)) -> {ST.good(po_sh(b, sh, p, r, z)) == True{} : Bool}:
252 match z:
253 case Tuple{sh2, Tuple{e, Tuple{gg, m}}}:
254 gg
255
256def po_model(-b: Bool, -sh: ST.Sh, -p: List<&2, Bool>, -r: List<&2, Bool>, z: PickOK(b, sh, p, r)) -> {ST.model(po_sh(b, sh, p, r, z)) == SC.append(Bool, SC.snoc(Bool, p, b), BL.rep(SC.length(Bool, r))) : List<&2, Bool>}:
257 match z:
258 case Tuple{sh2, Tuple{e, Tuple{gg, m}}}:
259 m
260
261def pick_sh(b: Bool, sh: ST.Sh, +p: List<&2, Bool>, +r: List<&2, Bool>, +g: {ST.good(sh) == True{} : Bool}, +ea: {ST.model(sh) == SC.append(Bool, p, Con{False{}, BL.rep(SC.length(Bool, r))}) : List<&2, Bool>}) -> PickOK(b, sh, p, r):
262 match sh:
263 case ST.Sh{+n, +d, +t}:
264 pick_ok(b, n, d, t, p, r, g, ea)
265
266def FillOK(zs: List<&2, Bool>, +p: List<&2, Bool>, sh: ST.Sh) -> Type:
267 Sigma<&1, &1, ST.Sh, sh2 => {B.fill(zs, SC.length(Bool, p), ST.real(sh)) == ST.real(sh2) : B.Bitset} & ({ST.good(sh2) == True{} : Bool} & {ST.model(sh2) == SC.append(Bool, p, zs) : List<&2, Bool>})>
268
269def fo_sh(-zs: List<&2, Bool>, -p: List<&2, Bool>, -sh: ST.Sh, z: FillOK(zs, p, sh)) -> ST.Sh:
270 match z:
271 case Tuple{sh2, y}:
272 sh2
273
274def fo_eq(-zs: List<&2, Bool>, -p: List<&2, Bool>, -sh: ST.Sh, z: FillOK(zs, p, sh)) -> {B.fill(zs, SC.length(Bool, p), ST.real(sh)) == ST.real(fo_sh(zs, p, sh, z)) : B.Bitset}:
275 match z:
276 case Tuple{sh2, Tuple{e, y}}:
277 e
278
279def fo_good(-zs: List<&2, Bool>, -p: List<&2, Bool>, -sh: ST.Sh, z: FillOK(zs, p, sh)) -> {ST.good(fo_sh(zs, p, sh, z)) == True{} : Bool}:
280 match z:
281 case Tuple{sh2, Tuple{e, Tuple{gg, m}}}:
282 gg
283
284def fo_model(-zs: List<&2, Bool>, -p: List<&2, Bool>, -sh: ST.Sh, z: FillOK(zs, p, sh)) -> {ST.model(fo_sh(zs, p, sh, z)) == SC.append(Bool, p, zs) : List<&2, Bool>}:
285 match z:
286 case Tuple{sh2, Tuple{e, Tuple{gg, m}}}:
287 m
288
289def fill_ok(zs: List<&2, Bool>, +p: List<&2, Bool>, +sh: ST.Sh, +g: {ST.good(sh) == True{} : Bool}, +ea: {ST.model(sh) == SC.append(Bool, p, BL.rep(SC.length(Bool, zs))) : List<&2, Bool>}) -> FillOK(zs, p, sh):
290 match zs:
291 case Nil{}:
292 (sh, ({==}, (g, ea)))
293 case Con{+b, +r}:
294 +sh1 = po_sh(b, sh, p, r, pick_sh(b, sh, p, r, g, ea))
295 +g1 = po_good(b, sh, p, r, pick_sh(b, sh, p, r, g, ea))
296 +ea1 = po_model(b, sh, p, r, pick_sh(b, sh, p, r, g, ea))
297 +sh2 = fo_sh(r, SC.snoc(Bool, p, b), sh1, fill_ok(r, SC.snoc(Bool, p, b), sh1, g1, ea1))
298 (sh2, (
299 %Equal.sym(B.Bitset, B.fill_pick(b, ST.real(sh), SC.length(Bool, p)), ST.real(sh1), po_eq(b, sh, p, r, pick_sh(b, sh, p, r, g, ea))) : {B.fill(r, 1n+SC.length(Bool, p), _) == ST.real(sh2) : B.Bitset}
300 %LL.length_snoc(Bool, p, b) : {B.fill(r, _, ST.real(sh1)) == ST.real(sh2) : B.Bitset}
301 fo_eq(r, SC.snoc(Bool, p, b), sh1, fill_ok(r, SC.snoc(Bool, p, b), sh1, g1, ea1)),
302 (fo_good(r, SC.snoc(Bool, p, b), sh1, fill_ok(r, SC.snoc(Bool, p, b), sh1, g1, ea1)),
303 Equal.trans(List<&2, Bool>, ST.model(sh2), SC.append(Bool, SC.snoc(Bool, p, b), r), SC.append(Bool, p, Con{b, r}),
304 fo_model(r, SC.snoc(Bool, p, b), sh1, fill_ok(r, SC.snoc(Bool, p, b), sh1, g1, ea1)),
305 LL.snoc_append_cons(Bool, p, b, r)))))
306
307def bool_count_len(+ys: List<&2, Bool>) -> {B.bool_count(ys) == SC.length(Bool, ys) : Nat}:
308 match ys:
309 case Nil{}:
310 {==}
311 case Con{b, +t}:
312 N.succ_cong(B.bool_count(t), SC.length(Bool, t), bool_count_len(t))
313
314def FromOK(ys: List<&2, Bool>) -> Type:
315 Sigma<&1, &1, ST.Sh, sh2 => {B.from_bools(ys) == ST.real(sh2) : B.Bitset} & ({ST.good(sh2) == True{} : Bool} & {ST.model(sh2) == ys : List<&2, Bool>})>
316
317def from_ok(+ys: List<&2, Bool>, +hf: {Nat.is_le(B.bool_count(ys), Nat.mul(SC.pow2(B.depth_for(B.bool_count(ys))), 32n)) == True{} : Bool}) -> FromOK(ys):
318 +c = B.bool_count(ys)
319 +sh0 = {ST.Sh{c, B.depth_for(c), A.trep(B.Wd, B.depth_for(c), B.W{0})} : ST.Sh}
320 +ea0 = L.subst(Nat, q => {ST.model(sh0) == BL.rep(q) : List<&2, Bool>}, c, SC.length(Bool, ys), bool_count_len(ys), ST.new_abs(c, hf))
321 +sh2 = fo_sh(ys, Nil{}, sh0, fill_ok(ys, Nil{}, sh0, ST.new_rep(c, hf), ea0))
322 (sh2, (
323 %Equal.sym(B.Bitset, B.new(c), ST.real(sh0), ST.new_form(c)) : {B.fill(ys, 0n, _) == ST.real(sh2) : B.Bitset}
324 fo_eq(ys, Nil{}, sh0, fill_ok(ys, Nil{}, sh0, ST.new_rep(c, hf), ea0)),
325 (fo_good(ys, Nil{}, sh0, fill_ok(ys, Nil{}, sh0, ST.new_rep(c, hf), ea0)),
326 fo_model(ys, Nil{}, sh0, fill_ok(ys, Nil{}, sh0, ST.new_rep(c, hf), ea0)))))
327
328# ---- binary operations ----
329
330def ws_len_eq(+d: Nat, +t: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +pa: {A.perfect(B.Wd, d, t) == True{} : Bool}, +pb: {A.perfect(B.Wd, d, tb) == True{} : Bool}) -> {SC.length(U32, AR.ws(tb)) == SC.length(U32, AR.ws(t)) : Nat}:
331 Equal.trans(Nat, SC.length(U32, AR.ws(tb)), SC.pow2(d), SC.length(U32, AR.ws(t)),
332 AR.ws_length(d, tb, pb),
333 Equal.sym(Nat, SC.length(U32, AR.ws(t)), SC.pow2(d), AR.ws_length(d, t, pa)))
334
335def ztz(+k: B.WordOp, +d: Nat, +t: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>) -> A.Tree<B.Wd>:
336 ZP.ztree(SC.pow2(d), k, d, t, tb, 0n)
337
338def ws_zip(+k: B.WordOp, +d: Nat, +t: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +pa: {A.perfect(B.Wd, d, t) == True{} : Bool}, +pb: {A.perfect(B.Wd, d, tb) == True{} : Bool}) -> {AR.ws(ztz(k, d, t, tb)) == MD.zip_words(k, AR.ws(t), AR.ws(tb)) : List<&2, U32>}:
339 Equal.trans(List<&2, U32>, AR.ws(ztz(k, d, t, tb)), ZP.zl(SC.pow2(d), k, 0n, AR.ws(t), AR.ws(tb)), MD.zip_words(k, AR.ws(t), AR.ws(tb)),
340 ZP.ztree_ws(SC.pow2(d), k, d, t, tb, 0n, pa, N.le_refl(SC.pow2(d))),
341 L.subst(Nat, z => {ZP.zl(z, k, 0n, AR.ws(t), AR.ws(tb)) == MD.zip_words(k, AR.ws(t), AR.ws(tb)) : List<&2, U32>},
342 SC.length(U32, AR.ws(t)), SC.pow2(d), AR.ws_length(d, t, pa),
343 ZP.zl_full(k, AR.ws(t), AR.ws(tb), ws_len_eq(d, t, tb, pa, pb))))
344
345def zip_flat(+k: B.WordOp, +d: Nat, +t: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +pa: {A.perfect(B.Wd, d, t) == True{} : Bool}, +pb: {A.perfect(B.Wd, d, tb) == True{} : Bool}) -> {ST.flat(AR.ws(ztz(k, d, t, tb))) == BL.zipk(k, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb))) : List<&2, Bool>}:
346 Equal.trans(List<&2, Bool>, ST.flat(AR.ws(ztz(k, d, t, tb))), ST.flat(MD.zip_words(k, AR.ws(t), AR.ws(tb))), BL.zipk(k, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb))),
347 Equal.cong(List<&2, U32>, List<&2, Bool>, ST.flat, AR.ws(ztz(k, d, t, tb)), MD.zip_words(k, AR.ws(t), AR.ws(tb)), ws_zip(k, d, t, tb, pa, pb)),
348 ST.zip_words(k, AR.ws(t), AR.ws(tb)))
349
350def zip_rep(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +g: {ST.rep(n, d, t) == True{} : Bool}, +gb: {ST.rep(n, d, tb) == True{} : Bool}) -> {ST.rep(n, d, ztz(k, d, t, tb)) == True{} : Bool}:
351 ST.rep_mk(n, d, ztz(k, d, t, tb),
352 ST.rep_depth(n, d, t, g),
353 ZP.ztree_perfect(SC.pow2(d), k, d, t, tb, 0n, ST.rep_perfect(n, d, t, g)),
354 L.subst(List<&2, Bool>, z => {ST.invf(n, z) == True{} : Bool}, BL.zipk(k, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb))), ST.flat(AR.ws(ztz(k, d, t, tb))),
355 Equal.sym(List<&2, Bool>, ST.flat(AR.ws(ztz(k, d, t, tb))), BL.zipk(k, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb))), zip_flat(k, d, t, tb, ST.rep_perfect(n, d, t, g), ST.rep_perfect(n, d, tb, gb))),
356 ST.invf_zipk(k, n, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb)), ST.rep_invf(n, d, t, g), ST.rep_invf(n, d, tb, gb))))
357
358def zip_abs(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +pa: {A.perfect(B.Wd, d, t) == True{} : Bool}, +pb: {A.perfect(B.Wd, d, tb) == True{} : Bool}) -> {ST.abs(n, ztz(k, d, t, tb)) == BL.zipk(k, ST.abs(n, t), ST.abs(n, tb)) : List<&2, Bool>}:
359 Equal.trans(List<&2, Bool>, SC.take(Bool, ST.flat(AR.ws(ztz(k, d, t, tb))), n), SC.take(Bool, BL.zipk(k, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb))), n), BL.zipk(k, ST.abs(n, t), ST.abs(n, tb)),
360 Equal.cong(List<&2, Bool>, List<&2, Bool>, z => SC.take(Bool, z, n), ST.flat(AR.ws(ztz(k, d, t, tb))), BL.zipk(k, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb))), zip_flat(k, d, t, tb, pa, pb)),
361 BL.take_zipk(k, ST.flat(AR.ws(t)), ST.flat(AR.ws(tb)), n))
362
363def CombOK(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +k: B.WordOp, +ys: List<&2, Bool>, +z: List<&2, Bool>) -> Type:
364 Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, Result<&2, &2, E.Error, Unit>, x => {B.comb_bits(k, ST.real(ST.Sh{n, d, t}), ys) == (ST.real(sh2), x) : B.Bitset & Result<&2, &2, E.Error, Unit>} & ({ST.good(sh2) == True{} : Bool} & {(ST.model(sh2), E.OUnit{x}) == S.combine(ST.abs(n, t), ys, z) : List<&2, Bool> & E.Obs})>>
365
366def comb_at(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +tb: A.Tree<B.Wd>, +ys: List<&2, Bool>, +z: List<&2, Bool>, +ez: {BL.zipk(k, ST.abs(n, t), ys) == z : List<&2, Bool>}, +g: {ST.rep(n, d, t) == True{} : Bool}, +gb: {ST.rep(n, d, tb) == True{} : Bool}, +eab: {ST.abs(n, tb) == ys : List<&2, Bool>}, +etrue: {Nat.is_eq(n, B.bool_count(ys)) == True{} : Bool}, +efb: {B.from_bools(ys) == ST.real(ST.Sh{n, d, tb}) : B.Bitset}) -> CombOK(n, d, t, k, ys, z):
367 (ST.Sh{n, d, ztz(k, d, t, tb)}, (Done{Unit{}}, (
368 %Equal.sym(Bool, Nat.is_eq(n, B.bool_count(ys)), True{}, etrue) : {B.comb_go(_, k, n, d, A.thaw(B.Wd, t), ys) == (ST.real(ST.Sh{n, d, ztz(k, d, t, tb)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
369 %Equal.sym(B.Bitset, B.from_bools(ys), ST.real(ST.Sh{n, d, tb}), efb) : {B.drop_right(B.combine(k, B.BS{n, d, A.thaw(B.Wd, t)}, _)) == (ST.real(ST.Sh{n, d, ztz(k, d, t, tb)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
370 %Equal.sym(Bool, Nat.is_eq(n, n), True{}, N.is_eq_refl(n)) : {B.drop_right(B.combine_if(Bool.and(_, Nat.is_eq(d, d)), k, n, d, A.thaw(B.Wd, t), n, d, A.thaw(B.Wd, tb))) == (ST.real(ST.Sh{n, d, ztz(k, d, t, tb)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
371 %Equal.sym(Bool, Nat.is_eq(d, d), True{}, N.is_eq_refl(d)) : {B.drop_right(B.combine_if(Bool.and(True{}, _), k, n, d, A.thaw(B.Wd, t), n, d, A.thaw(B.Wd, tb))) == (ST.real(ST.Sh{n, d, ztz(k, d, t, tb)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
372 %Equal.sym(Nat, P2.pow2t(d), SC.pow2(d), PT.same(d)) : {B.drop_right(B.zip_fin(B.zip_go(_, (A.thaw(B.Wd, t), A.thaw(B.Wd, tb)), k, d, 0n), n, d, n, d)) == (ST.real(ST.Sh{n, d, ztz(k, d, t, tb)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
373 %Equal.sym(Array<B.Wd> & Array<B.Wd>, B.zip_go(SC.pow2(d), (A.thaw(B.Wd, t), A.thaw(B.Wd, tb)), k, d, 0n), (A.thaw(B.Wd, ztz(k, d, t, tb)), A.thaw(B.Wd, tb)), ZP.zip_go_ok(SC.pow2(d), k, d, t, tb, 0n, ST.rep_lt(n, d, t, g), ST.rep_perfect(n, d, t, g), ST.rep_perfect(n, d, tb, gb), N.le_refl(SC.pow2(d)))) : {B.drop_right(B.zip_fin(_, n, d, n, d)) == (ST.real(ST.Sh{n, d, ztz(k, d, t, tb)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
374 %Equal.sym(Unit, B.dispose(B.BS{n, d, A.thaw(B.Wd, tb)}), Unit{}, ST.dispose_ok(n, d, tb)) : {B.drop_right_go(B.BS{n, d, A.thaw(B.Wd, ztz(k, d, t, tb))}, _, Done{Unit{}}) == (ST.real(ST.Sh{n, d, ztz(k, d, t, tb)}), Done{Unit{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
375 {==},
376 (zip_rep(k, n, d, t, tb, g, gb),
377 %Equal.sym(Nat, SC.length(Bool, ST.abs(n, t)), n, ST.length_abs(n, ST.flat(AR.ws(t)), ST.rep_invf(n, d, t, g))) : {(ST.abs(n, ztz(k, d, t, tb)), E.OUnit{Done{Unit{}}}) == S.combine_if(Nat.is_eq(_, SC.length(Bool, ys)), ST.abs(n, t), z) : List<&2, Bool> & E.Obs}
378 %bool_count_len(ys) : {(ST.abs(n, ztz(k, d, t, tb)), E.OUnit{Done{Unit{}}}) == S.combine_if(Nat.is_eq(n, _), ST.abs(n, t), z) : List<&2, Bool> & E.Obs}
379 %Equal.sym(Bool, Nat.is_eq(n, B.bool_count(ys)), True{}, etrue) : {(ST.abs(n, ztz(k, d, t, tb)), E.OUnit{Done{Unit{}}}) == S.combine_if(_, ST.abs(n, t), z) : List<&2, Bool> & E.Obs}
380 Equal.cong(List<&2, Bool>, List<&2, Bool> & E.Obs, w => (w, E.OUnit{Done{Unit{}}}), ST.abs(n, ztz(k, d, t, tb)), z,
381 Equal.trans(List<&2, Bool>, ST.abs(n, ztz(k, d, t, tb)), BL.zipk(k, ST.abs(n, t), ys), z,
382 Equal.trans(List<&2, Bool>, ST.abs(n, ztz(k, d, t, tb)), BL.zipk(k, ST.abs(n, t), ST.abs(n, tb)), BL.zipk(k, ST.abs(n, t), ys),
383 zip_abs(k, n, d, t, tb, ST.rep_perfect(n, d, t, g), ST.rep_perfect(n, d, tb, gb)),
384 Equal.cong(List<&2, Bool>, List<&2, Bool>, w => BL.zipk(k, ST.abs(n, t), w), ST.abs(n, tb), ys, eab)),
385 ez))))))
386
387def fr_sh(-ys: List<&2, Bool>, z: FromOK(ys)) -> ST.Sh:
388 match z:
389 case Tuple{sh2, y}:
390 sh2
391
392def fr_eq(-ys: List<&2, Bool>, z: FromOK(ys)) -> {B.from_bools(ys) == ST.real(fr_sh(ys, z)) : B.Bitset}:
393 match z:
394 case Tuple{sh2, Tuple{e, y}}:
395 e
396
397def fr_good(-ys: List<&2, Bool>, z: FromOK(ys)) -> {ST.good(fr_sh(ys, z)) == True{} : Bool}:
398 match z:
399 case Tuple{sh2, Tuple{e, Tuple{gg, m}}}:
400 gg
401
402def fr_model(-ys: List<&2, Bool>, z: FromOK(ys)) -> {ST.model(fr_sh(ys, z)) == ys : List<&2, Bool>}:
403 match z:
404 case Tuple{sh2, Tuple{e, Tuple{gg, m}}}:
405 m
406
407def comb_sh(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, shf: ST.Sh, +ys: List<&2, Bool>, +z: List<&2, Bool>, +ez: {BL.zipk(k, ST.abs(n, t), ys) == z : List<&2, Bool>}, +g: {ST.rep(n, d, t) == True{} : Bool}, +gf: {ST.good(shf) == True{} : Bool}, +eaf: {ST.model(shf) == ys : List<&2, Bool>}, +etrue: {Nat.is_eq(n, B.bool_count(ys)) == True{} : Bool}, +efb: {B.from_bools(ys) == ST.real(shf) : B.Bitset}) -> CombOK(n, d, t, k, ys, z):
408 match shf:
409 case ST.Sh{+m, +e, +tb}:
410 +eyn = Equal.trans(Nat, SC.length(Bool, ys), B.bool_count(ys), n,
411 Equal.sym(Nat, B.bool_count(ys), SC.length(Bool, ys), bool_count_len(ys)),
412 Equal.sym(Nat, n, B.bool_count(ys), N.eq_from_is_eq(n, B.bool_count(ys), etrue)))
413 +em = Equal.trans(Nat, m, SC.length(Bool, ys), n,
414 Equal.trans(Nat, m, SC.length(Bool, ST.abs(m, tb)), SC.length(Bool, ys),
415 Equal.sym(Nat, SC.length(Bool, ST.abs(m, tb)), m, ST.length_abs(m, ST.flat(AR.ws(tb)), ST.rep_invf(m, e, tb, gf))),
416 Equal.cong(List<&2, Bool>, Nat, w => SC.length(Bool, w), ST.abs(m, tb), ys, eaf)),
417 eyn)
418 +ee = Equal.trans(Nat, e, B.depth_for(n), d,
419 Equal.trans(Nat, e, B.depth_for(m), B.depth_for(n),
420 N.eq_from_is_eq(e, B.depth_for(m), ST.rep_depth(m, e, tb, gf)),
421 Equal.cong(Nat, Nat, w => B.depth_for(w), m, n, em)),
422 Equal.sym(Nat, d, B.depth_for(n), N.eq_from_is_eq(d, B.depth_for(n), ST.rep_depth(n, d, t, g))))
423 comb_at(k, n, d, t, tb, ys, z, ez, g,
424 L.subst(Nat, x => {ST.rep(n, x, tb) == True{} : Bool}, e, d, ee,
425 L.subst(Nat, x => {ST.rep(x, e, tb) == True{} : Bool}, m, n, em, gf)),
426 L.subst(Nat, x => {ST.abs(x, tb) == ys : List<&2, Bool>}, m, n, em, eaf),
427 etrue,
428 L.subst(Nat, x => {B.from_bools(ys) == ST.real(ST.Sh{n, x, tb}) : B.Bitset}, e, d, ee,
429 L.subst(Nat, x => {B.from_bools(ys) == ST.real(ST.Sh{x, e, tb}) : B.Bitset}, m, n, em, efb)))
430
431def comb_false(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +ys: List<&2, Bool>, +z: List<&2, Bool>, +g: {ST.rep(n, d, t) == True{} : Bool}, +efalse: {Nat.is_eq(n, B.bool_count(ys)) == False{} : Bool}) -> CombOK(n, d, t, k, ys, z):
432 (ST.Sh{n, d, t}, (Fail{E.LengthMismatch{}}, (
433 %Equal.sym(Bool, Nat.is_eq(n, B.bool_count(ys)), False{}, efalse) : {B.comb_go(_, k, n, d, A.thaw(B.Wd, t), ys) == (ST.real(ST.Sh{n, d, t}), Fail{E.LengthMismatch{}}) : B.Bitset & Result<&2, &2, E.Error, Unit>}
434 {==},
435 (g,
436 %Equal.sym(Nat, SC.length(Bool, ST.abs(n, t)), n, ST.length_abs(n, ST.flat(AR.ws(t)), ST.rep_invf(n, d, t, g))) : {(ST.abs(n, t), E.OUnit{Fail{E.LengthMismatch{}}}) == S.combine_if(Nat.is_eq(_, SC.length(Bool, ys)), ST.abs(n, t), z) : List<&2, Bool> & E.Obs}
437 %bool_count_len(ys) : {(ST.abs(n, t), E.OUnit{Fail{E.LengthMismatch{}}}) == S.combine_if(Nat.is_eq(n, _), ST.abs(n, t), z) : List<&2, Bool> & E.Obs}
438 %Equal.sym(Bool, Nat.is_eq(n, B.bool_count(ys)), False{}, efalse) : {(ST.abs(n, t), E.OUnit{Fail{E.LengthMismatch{}}}) == S.combine_if(_, ST.abs(n, t), z) : List<&2, Bool> & E.Obs}
439 {==}))))
440
441def comb_case(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +ys: List<&2, Bool>, +z: List<&2, Bool>, +ez: {BL.zipk(k, ST.abs(n, t), ys) == z : List<&2, Bool>}, +g: {ST.rep(n, d, t) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(n, B.bool_count(ys)) == b : Bool}) -> CombOK(n, d, t, k, ys, z):
442 match b:
443 case True{}:
444 +hf = L.subst(Nat, x => {Nat.is_le(x, Nat.mul(SC.pow2(B.depth_for(x)), 32n)) == True{} : Bool}, n, B.bool_count(ys), N.eq_from_is_eq(n, B.bool_count(ys), eb), ST.rep_fits(n, d, t, g))
445 comb_sh(k, n, d, t, fr_sh(ys, from_ok(ys, hf)), ys, z, ez, g,
446 fr_good(ys, from_ok(ys, hf)), fr_model(ys, from_ok(ys, hf)), eb, fr_eq(ys, from_ok(ys, hf)))
447 case False{}:
448 comb_false(k, n, d, t, ys, z, g, eb)
449
450def co_sh(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -k: B.WordOp, -ys: List<&2, Bool>, -z: List<&2, Bool>, c: CombOK(n, d, t, k, ys, z)) -> ST.Sh:
451 match c:
452 case Tuple{sh2, y}:
453 sh2
454
455def co_res(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -k: B.WordOp, -ys: List<&2, Bool>, -z: List<&2, Bool>, c: CombOK(n, d, t, k, ys, z)) -> Result<&2, &2, E.Error, Unit>:
456 match c:
457 case Tuple{sh2, Tuple{x, y}}:
458 x
459
460def co_eq(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -k: B.WordOp, -ys: List<&2, Bool>, -z: List<&2, Bool>, c: CombOK(n, d, t, k, ys, z)) -> {B.comb_bits(k, ST.real(ST.Sh{n, d, t}), ys) == (ST.real(co_sh(n, d, t, k, ys, z, c)), co_res(n, d, t, k, ys, z, c)) : B.Bitset & Result<&2, &2, E.Error, Unit>}:
461 match c:
462 case Tuple{sh2, Tuple{x, Tuple{e, y}}}:
463 e
464
465def co_good(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -k: B.WordOp, -ys: List<&2, Bool>, -z: List<&2, Bool>, c: CombOK(n, d, t, k, ys, z)) -> {ST.good(co_sh(n, d, t, k, ys, z, c)) == True{} : Bool}:
466 match c:
467 case Tuple{sh2, Tuple{x, Tuple{e, Tuple{gg, s}}}}:
468 gg
469
470def co_spec(-n: Nat, -d: Nat, -t: A.Tree<B.Wd>, -k: B.WordOp, -ys: List<&2, Bool>, -z: List<&2, Bool>, c: CombOK(n, d, t, k, ys, z)) -> {(ST.model(co_sh(n, d, t, k, ys, z, c)), E.OUnit{co_res(n, d, t, k, ys, z, c)}) == S.combine(ST.abs(n, t), ys, z) : List<&2, Bool> & E.Obs}:
471 match c:
472 case Tuple{sh2, Tuple{x, Tuple{e, Tuple{gg, s}}}}:
473 s
474
475def CC(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +ys: List<&2, Bool>, +z: List<&2, Bool>, +ez: {BL.zipk(k, ST.abs(n, t), ys) == z : List<&2, Bool>}, +g: {ST.rep(n, d, t) == True{} : Bool}) -> CombOK(n, d, t, k, ys, z):
476 comb_case(k, n, d, t, ys, z, ez, g, Nat.is_eq(n, B.bool_count(ys)), {==})
477
478def comb_step(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +ys: List<&2, Bool>, +z: List<&2, Bool>, +ez: {BL.zipk(k, ST.abs(n, t), ys) == z : List<&2, Bool>}, +g: {ST.rep(n, d, t) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, E.Obs, o => {B.obs_unit(B.comb_bits(k, ST.real(ST.Sh{n, d, t}), ys)) == (ST.real(sh2), o) : B.Bitset & E.Obs} & ({ST.good(sh2) == True{} : Bool} & {(ST.model(sh2), o) == S.combine(ST.abs(n, t), ys, z) : List<&2, Bool> & E.Obs})>>:
479 (co_sh(n, d, t, k, ys, z, CC(k, n, d, t, ys, z, ez, g)), (E.OUnit{co_res(n, d, t, k, ys, z, CC(k, n, d, t, ys, z, ez, g))}, (
480 Equal.cong(B.Bitset & Result<&2, &2, E.Error, Unit>, B.Bitset & E.Obs, w => B.obs_unit(w),
481 B.comb_bits(k, ST.real(ST.Sh{n, d, t}), ys),
482 (ST.real(co_sh(n, d, t, k, ys, z, CC(k, n, d, t, ys, z, ez, g))), co_res(n, d, t, k, ys, z, CC(k, n, d, t, ys, z, ez, g))),
483 co_eq(n, d, t, k, ys, z, CC(k, n, d, t, ys, z, ez, g))),
484 (co_good(n, d, t, k, ys, z, CC(k, n, d, t, ys, z, ez, g)),
485 co_spec(n, d, t, k, ys, z, CC(k, n, d, t, ys, z, ez, g))))))
486
487def assign_step(+n: Nat, +d: Nat, +t: A.Tree<B.Wd>, +i: Nat, +v: Bool, +g: {ST.rep(n, d, t) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, E.Obs, o => {B.obs_unit(B.assign(B.BS{n, d, A.thaw(B.Wd, t)}, i, v)) == (ST.real(sh2), o) : B.Bitset & E.Obs} & ({ST.good(sh2) == True{} : Bool} & {(ST.model(sh2), o) == S.assign(ST.abs(n, t), i, v) : List<&2, Bool> & E.Obs})>>:
488 (ao_sh(n, d, t, i, v, Nat.is_lt(i, n), assign_case(n, d, t, i, v, Nat.is_lt(i, n), {==}, g)),
489 (E.OUnit{ao_res(n, d, t, i, v, Nat.is_lt(i, n), assign_case(n, d, t, i, v, Nat.is_lt(i, n), {==}, g))}, (
490 Equal.cong(B.Bitset & Result<&2, &2, E.Error, Unit>, B.Bitset & E.Obs, w => B.obs_unit(w),
491 B.assign_if(Nat.is_lt(i, n), n, d, A.thaw(B.Wd, t), i, v),
492 (ST.real(ao_sh(n, d, t, i, v, Nat.is_lt(i, n), assign_case(n, d, t, i, v, Nat.is_lt(i, n), {==}, g))), ao_res(n, d, t, i, v, Nat.is_lt(i, n), assign_case(n, d, t, i, v, Nat.is_lt(i, n), {==}, g))),
493 ao_eq(n, d, t, i, v, Nat.is_lt(i, n), assign_case(n, d, t, i, v, Nat.is_lt(i, n), {==}, g))),
494 (ao_good(n, d, t, i, v, Nat.is_lt(i, n), assign_case(n, d, t, i, v, Nat.is_lt(i, n), {==}, g)),
495 ao_spec(n, d, t, i, v, Nat.is_lt(i, n), assign_case(n, d, t, i, v, Nat.is_lt(i, n), {==}, g))))))
496
497# ---- every operation ----
498
499def step_ok(sh: ST.Sh, op: E.Op, +g: {ST.good(sh) == True{} : Bool}) -> StepOK(sh, op):
500 match sh op:
501 case ST.Sh{+n, +d, +t} E.Length{}:
502 length_ok(n, d, t, g)
503 case ST.Sh{+n, +d, +t} E.Get{+i}:
504 get_case(n, d, t, i, Nat.is_lt(i, n), {==}, g)
505 case ST.Sh{+n, +d, +t} E.Set{+i}:
506 assign_step(n, d, t, i, True{}, g)
507 case ST.Sh{+n, +d, +t} E.Clear{+i}:
508 assign_step(n, d, t, i, False{}, g)
509 case ST.Sh{+n, +d, +t} E.Count{}:
510 count_ok(n, d, t, g)
511 case ST.Sh{+n, +d, +t} E.Union{+ys}:
512 comb_step(B.KOr{}, n, d, t, ys, S.zip_or(ST.abs(n, t), ys), Equal.sym(List<&2, Bool>, S.zip_or(ST.abs(n, t), ys), BL.zipk(B.KOr{}, ST.abs(n, t), ys), BL.spec_or(ST.abs(n, t), ys)), g)
513 case ST.Sh{+n, +d, +t} E.Intersection{+ys}:
514 comb_step(B.KAnd{}, n, d, t, ys, S.zip_and(ST.abs(n, t), ys), Equal.sym(List<&2, Bool>, S.zip_and(ST.abs(n, t), ys), BL.zipk(B.KAnd{}, ST.abs(n, t), ys), BL.spec_and(ST.abs(n, t), ys)), g)
515 case ST.Sh{+n, +d, +t} E.Difference{+ys}:
516 comb_step(B.KDiff{}, n, d, t, ys, S.zip_diff(ST.abs(n, t), ys), Equal.sym(List<&2, Bool>, S.zip_diff(ST.abs(n, t), ys), BL.zipk(B.KDiff{}, ST.abs(n, t), ys), BL.spec_diff(ST.abs(n, t), ys)), g)
517 case ST.Sh{+n, +d, +t} E.Xor{+ys}:
518 comb_step(B.KXor{}, n, d, t, ys, S.zip_xor(ST.abs(n, t), ys), Equal.sym(List<&2, Bool>, S.zip_xor(ST.abs(n, t), ys), BL.zipk(B.KXor{}, ST.abs(n, t), ys), BL.spec_xor(ST.abs(n, t), ys)), g)
519 case ST.Sh{+n, +d, +t} E.ToList{}:
520 tolist_ok(n, d, t, g)