1 import Base 2 import ../../../src/math/pow2.bend as P2 3 import ../../math/pow2/pow2.bend as PT 4 import ../../lib/logic.bend as L 5 import ../../lib/nat.bend as N 6 import ../../lib/list.bend as LL 7 import ../../lib/array.bend as A 8 import ../../../spec/lib/common.bend as SC 9 import ../../../spec/containers/bitset.bend as S 10 import ../../../src/containers/bitset.bend as B 11 import ../../../src/containers/types/bitset.bend as E 12 import ./lists.bend as BL 13 import ./model.bend as MD 14 import ./walk.bend as WK 15 import ./arr.bend as AR 16 import ./loops.bend as LP 17 import ./zip.bend as ZP 18 import ./depth.bend as DP 19 import ./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 29 def 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 34 def n_le_cap(+n: Nat, +d: Nat, +t: A.Tree, +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 38 def wix(+n: Nat, +d: Nat, +t: A.Tree, +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 43 def length_ok(+n: Nat, +d: Nat, +t: A.Tree, +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 50 def 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 55 def 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 59 def get_case(+n: Nat, +d: Nat, +t: A.Tree, +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 & 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 80 def upd_tree(+d: Nat, +t: A.Tree, +i: Nat, +v: Bool) -> A.Tree: 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 83 def upd_ws(+n: Nat, +d: Nat, +t: A.Tree, +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 88 def upd_rep(+n: Nat, +d: Nat, +t: A.Tree, +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 96 def upd_abs(+n: Nat, +d: Nat, +t: A.Tree, +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 101 def AssignOK(+n: Nat, +d: Nat, +t: A.Tree, +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 104 def assign_case(+n: Nat, +d: Nat, +t: A.Tree, +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 & 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.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 123 def 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 130 def 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 137 def count_ok(+n: Nat, +d: Nat, +t: A.Tree, +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 & 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 147 def tolist_ok(+n: Nat, +d: Nat, +t: A.Tree, +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 & 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 159 def ao_sh(-n: Nat, -d: Nat, -t: A.Tree, -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 164 def ao_res(-n: Nat, -d: Nat, -t: A.Tree, -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 169 def ao_eq(-n: Nat, -d: Nat, -t: A.Tree, -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 174 def ao_good(-n: Nat, -d: Nat, -t: A.Tree, -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 179 def ao_spec(-n: Nat, -d: Nat, -t: A.Tree, -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 184 def 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 188 def 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 192 def 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. 199 def pick_lt(+n: Nat, +d: Nat, +t: A.Tree, +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 206 def 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 209 def 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 216 def AC(+n: Nat, +d: Nat, +t: A.Tree, +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 219 def pick_ok(b: Bool, +n: Nat, +d: Nat, +t: A.Tree, +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 241 def 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 246 def 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 251 def 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 256 def 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 261 def 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 266 def 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 269 def 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 274 def 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 279 def 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 284 def 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 289 def 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 307 def 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 314 def 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 317 def 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 330 def ws_len_eq(+d: Nat, +t: A.Tree, +tb: A.Tree, +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 335 def ztz(+k: B.WordOp, +d: Nat, +t: A.Tree, +tb: A.Tree) -> A.Tree: 336 ZP.ztree(SC.pow2(d), k, d, t, tb, 0n) 337 338 def ws_zip(+k: B.WordOp, +d: Nat, +t: A.Tree, +tb: A.Tree, +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 345 def zip_flat(+k: B.WordOp, +d: Nat, +t: A.Tree, +tb: A.Tree, +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 350 def zip_rep(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, +tb: A.Tree, +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 358 def zip_abs(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, +tb: A.Tree, +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 363 def CombOK(+n: Nat, +d: Nat, +t: A.Tree, +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 366 def comb_at(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, +tb: A.Tree, +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 & Array, 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 387 def fr_sh(-ys: List<&2, Bool>, z: FromOK(ys)) -> ST.Sh: 388 match z: 389 case Tuple{sh2, y}: 390 sh2 391 392 def 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 397 def 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 402 def 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 407 def comb_sh(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, 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 431 def comb_false(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, +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 441 def comb_case(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, +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 450 def co_sh(-n: Nat, -d: Nat, -t: A.Tree, -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 455 def co_res(-n: Nat, -d: Nat, -t: A.Tree, -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 460 def co_eq(-n: Nat, -d: Nat, -t: A.Tree, -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 465 def co_good(-n: Nat, -d: Nat, -t: A.Tree, -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 470 def co_spec(-n: Nat, -d: Nat, -t: A.Tree, -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 475 def CC(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, +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 478 def comb_step(+k: B.WordOp, +n: Nat, +d: Nat, +t: A.Tree, +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 487 def assign_step(+n: Nat, +d: Nat, +t: A.Tree, +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 499 def 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)