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 ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/bitset.bend as S 7 import ../../../src/containers/bitset.bend as B 8 import ../../lib/array.bend as A 9 import ./model.bend as MD 10 import ./arr.bend as AR 11 import ./depth.bend as DP 12 import ./lists.bend as BL 13 import ./word.bend as W 14 15 # Abstraction and invariant of the packed representation. 16 # flat(ws) all stored bits, word by word, bit 0 first 17 # abs the first `len` stored bits 18 # inv len <= |flat| < len + 32 (exactly ceil(len/32) words) and 19 # every stored bit at position >= len is zero (masked tail) 20 21 def flat(ws: List<&2, U32>) -> List<&2, Bool>: 22 match ws: 23 case Nil{}: 24 Nil{} 25 case Con{w, t}: 26 SC.append(Bool, W.ubits(w), flat(t)) 27 28 def invf(+n: Nat, +xs: List<&2, Bool>) -> Bool: 29 Bool.and(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n))) 30 31 def inv_le(+n: Nat, +xs: List<&2, Bool>, +g: {invf(n, xs) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}: 32 L.and_left(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n)), g) 33 34 def inv_tail(+n: Nat, +xs: List<&2, Bool>, +g: {invf(n, xs) == True{} : Bool}) -> {BL.allf(SC.drop(Bool, xs, n)) == True{} : Bool}: 35 L.and_right(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n)), g) 36 37 def inv_mk(+n: Nat, +xs: List<&2, Bool>, +a: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}, +c: {BL.allf(SC.drop(Bool, xs, n)) == True{} : Bool}) -> {invf(n, xs) == True{} : Bool}: 38 L.and_intro(Nat.is_le(n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, n)), a, c) 39 40 # The logical length is len. 41 def length_abs(+n: Nat, +xs: List<&2, Bool>, +g: {invf(n, xs) == True{} : Bool}) -> {SC.length(Bool, SC.take(Bool, xs, n)) == n : Nat}: 42 BL.length_take(xs, n, inv_le(n, xs, g)) 43 44 # The stored bits are the logical bits followed by the zero tail. 45 def split(+n: Nat, +xs: List<&2, Bool>) -> {xs == SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)) : List<&2, Bool>}: 46 Equal.sym(List<&2, Bool>, SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)), xs, BL.take_drop(xs, n)) 47 48 def take32(+w: U32) -> {SC.take(Bool, W.ubits(w), 32n) == W.ubits(w) : List<&2, Bool>}: 49 L.subst(Nat, k => {SC.take(Bool, W.ubits(w), k) == W.ubits(w) : List<&2, Bool>}, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w), BL.take_all(W.ubits(w))) 50 51 def length_flat_cons(+w: U32, +t: List<&2, U32>) -> {SC.length(Bool, flat(Con{w, t})) == Nat.add(32n, SC.length(Bool, flat(t))) : Nat}: 52 %Equal.sym(Nat, SC.length(Bool, SC.append(Bool, W.ubits(w), flat(t))), Nat.add(SC.length(Bool, W.ubits(w)), SC.length(Bool, flat(t))), LL.length_append(Bool, W.ubits(w), flat(t))) : {_ == Nat.add(32n, SC.length(Bool, flat(t))) : Nat} 53 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {Nat.add(_, SC.length(Bool, flat(t))) == Nat.add(32n, SC.length(Bool, flat(t))) : Nat} 54 {==} 55 56 # ---- word-list walks ---- 57 58 def get_case(+w: U32, +t: List<&2, U32>, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +h: {Nat.is_lt(i, Nat.add(32n, SC.length(Bool, flat(t)))) == True{} : Bool}, ih: @+h2: {Nat.is_lt(Nat.sub(i, 32n), SC.length(Bool, flat(t))) == True{} : Bool} -> {Some{MD.get_walk(t, Nat.sub(i, 32n))} == SC.nth(Bool, flat(t), Nat.sub(i, 32n)) : Maybe<&2, Bool>}) -> {Some{MD.get_pick(b, w, i, MD.get_walk(t, Nat.sub(i, 32n)))} == SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i) : Maybe<&2, Bool>}: 59 match b: 60 case True{}: 61 +hl = L.subst(Nat, k => {Nat.is_lt(i, k) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), eb) 62 Equal.trans(Maybe<&2, Bool>, Some{B.word_get(w, i)}, SC.nth(Bool, W.ubits(w), i), SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i), 63 W.word_get(w, i, eb), 64 Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i), SC.nth(Bool, W.ubits(w), i), LL.nth_append_left(Bool, W.ubits(w), flat(t), i, hl))) 65 case False{}: 66 +le = N.not_lt_le(i, 32n, eb) 67 +hr = L.subst(Nat, k => {Nat.is_le(k, i) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), le) 68 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.append(Bool, W.ubits(w), flat(t)), i), SC.nth(Bool, flat(t), Nat.sub(i, SC.length(Bool, W.ubits(w)))), LL.nth_append_right(Bool, W.ubits(w), flat(t), i, hr)) : {Some{MD.get_walk(t, Nat.sub(i, 32n))} == _ : Maybe<&2, Bool>} 69 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {Some{MD.get_walk(t, Nat.sub(i, 32n))} == SC.nth(Bool, flat(t), Nat.sub(i, _)) : Maybe<&2, Bool>} 70 ih(N.sub_lt(i, 32n, SC.length(Bool, flat(t)), le, h)) 71 72 def get_walk(+ws: List<&2, U32>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, flat(ws))) == True{} : Bool}) -> {Some{MD.get_walk(ws, i)} == SC.nth(Bool, flat(ws), i) : Maybe<&2, Bool>}: 73 match ws: 74 case Nil{}: 75 Empty.absurd({Some{MD.get_walk(Nil{}, i)} == SC.nth(Bool, flat(Nil{}), i) : Maybe<&2, Bool>}, N.lt_zero_absurd(i, h)) 76 case Con{w, t}: 77 get_case(w, t, i, Nat.is_lt(i, 32n), {==}, L.subst(Nat, k => {Nat.is_lt(i, k) == True{} : Bool}, SC.length(Bool, flat(Con{w, t})), Nat.add(32n, SC.length(Bool, flat(t))), length_flat_cons(w, t), h), h2 => get_walk(t, Nat.sub(i, 32n), h2)) 78 79 def put_case(+v: Bool, +w: U32, +i: Nat, +t: List<&2, U32>, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +ih: {flat(MD.put_walk(t, Nat.sub(i, 32n), v)) == SC.update(Bool, flat(t), Nat.sub(i, 32n), v) : List<&2, Bool>}) -> {flat(MD.put_pick(b, v, w, i, t, MD.put_walk(t, Nat.sub(i, 32n), v))) == SC.update(Bool, SC.append(Bool, W.ubits(w), flat(t)), i, v) : List<&2, Bool>}: 80 match b: 81 case True{}: 82 +hl = L.subst(Nat, k => {Nat.is_lt(i, k) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), eb) 83 %Equal.sym(List<&2, Bool>, SC.update(Bool, SC.append(Bool, W.ubits(w), flat(t)), i, v), SC.append(Bool, SC.update(Bool, W.ubits(w), i, v), flat(t)), LL.update_append_left(Bool, W.ubits(w), flat(t), i, v, hl)) : {SC.append(Bool, W.ubits(B.word_put(v, w, i)), flat(t)) == _ : List<&2, Bool>} 84 %Equal.sym(List<&2, Bool>, W.ubits(B.word_put(v, w, i)), SC.update(Bool, W.ubits(w), i, v), W.word_put(v, w, i, eb)) : {SC.append(Bool, _, flat(t)) == SC.append(Bool, SC.update(Bool, W.ubits(w), i, v), flat(t)) : List<&2, Bool>} 85 {==} 86 case False{}: 87 +le = N.not_lt_le(i, 32n, eb) 88 +hr = L.subst(Nat, k => {Nat.is_le(k, i) == True{} : Bool}, 32n, SC.length(Bool, W.ubits(w)), Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)), le) 89 %Equal.sym(List<&2, Bool>, SC.update(Bool, SC.append(Bool, W.ubits(w), flat(t)), i, v), SC.append(Bool, W.ubits(w), SC.update(Bool, flat(t), Nat.sub(i, SC.length(Bool, W.ubits(w))), v)), LL.update_append_right(Bool, W.ubits(w), flat(t), i, v, hr)) : {SC.append(Bool, W.ubits(w), flat(MD.put_walk(t, Nat.sub(i, 32n), v))) == _ : List<&2, Bool>} 90 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {SC.append(Bool, W.ubits(w), flat(MD.put_walk(t, Nat.sub(i, 32n), v))) == SC.append(Bool, W.ubits(w), SC.update(Bool, flat(t), Nat.sub(i, _), v)) : List<&2, Bool>} 91 %Equal.sym(List<&2, Bool>, flat(MD.put_walk(t, Nat.sub(i, 32n), v)), SC.update(Bool, flat(t), Nat.sub(i, 32n), v), ih) : {SC.append(Bool, W.ubits(w), _) == SC.append(Bool, W.ubits(w), SC.update(Bool, flat(t), Nat.sub(i, 32n), v)) : List<&2, Bool>} 92 {==} 93 94 def put_walk(+ws: List<&2, U32>, +i: Nat, +v: Bool) -> {flat(MD.put_walk(ws, i, v)) == SC.update(Bool, flat(ws), i, v) : List<&2, Bool>}: 95 match ws: 96 case Nil{}: 97 {==} 98 case Con{w, t}: 99 put_case(v, w, i, t, Nat.is_lt(i, 32n), {==}, put_walk(t, Nat.sub(i, 32n), v)) 100 101 def zip_words(+k: B.WordOp, +ws: List<&2, U32>, +vs: List<&2, U32>) -> {flat(MD.zip_words(k, ws, vs)) == BL.zipk(k, flat(ws), flat(vs)) : List<&2, Bool>}: 102 match ws vs: 103 case Nil{} _: 104 {==} 105 case Con{a, s} Nil{}: 106 Equal.sym(List<&2, Bool>, BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), Nil{}), Nil{}, BL.zipk_nil_r(k, SC.append(Bool, W.ubits(a), flat(s)))) 107 case Con{a, s} Con{b, t}: 108 %Equal.sym(List<&2, Bool>, W.ubits(B.word_op(k, a, b)), BL.zipk(k, W.ubits(a), W.ubits(b)), W.u_op(k, a, b)) : {SC.append(Bool, _, flat(MD.zip_words(k, s, t))) == BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), SC.append(Bool, W.ubits(b), flat(t))) : List<&2, Bool>} 109 %Equal.sym(List<&2, Bool>, flat(MD.zip_words(k, s, t)), BL.zipk(k, flat(s), flat(t)), zip_words(k, s, t)) : {SC.append(Bool, BL.zipk(k, W.ubits(a), W.ubits(b)), _) == BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), SC.append(Bool, W.ubits(b), flat(t))) : List<&2, Bool>} 110 Equal.sym(List<&2, Bool>, BL.zipk(k, SC.append(Bool, W.ubits(a), flat(s)), SC.append(Bool, W.ubits(b), flat(t))), SC.append(Bool, BL.zipk(k, W.ubits(a), W.ubits(b)), BL.zipk(k, flat(s), flat(t))), 111 BL.zipk_append(k, W.ubits(a), W.ubits(b), flat(s), flat(t), Equal.trans(Nat, SC.length(Bool, W.ubits(a)), 32n, SC.length(Bool, W.ubits(b)), W.ulen(a), Equal.sym(Nat, SC.length(Bool, W.ubits(b)), 32n, W.ulen(b))))) 112 113 def count_words(+ws: List<&2, U32>) -> {MD.count_words(ws) == S.count(flat(ws)) : Nat}: 114 match ws: 115 case Nil{}: 116 {==} 117 case Con{w, t}: 118 %Equal.sym(Nat, B.word_count(32n, w), S.count(SC.take(Bool, W.ubits(w), 32n)), W.word_count(32n, w)) : {Nat.add(_, MD.count_words(t)) == S.count(SC.append(Bool, W.ubits(w), flat(t))) : Nat} 119 %Equal.sym(List<&2, Bool>, SC.take(Bool, W.ubits(w), 32n), W.ubits(w), take32(w)) : {Nat.add(S.count(_), MD.count_words(t)) == S.count(SC.append(Bool, W.ubits(w), flat(t))) : Nat} 120 %Equal.sym(Nat, MD.count_words(t), S.count(flat(t)), count_words(t)) : {Nat.add(S.count(W.ubits(w)), _) == S.count(SC.append(Bool, W.ubits(w), flat(t))) : Nat} 121 Equal.sym(Nat, S.count(SC.append(Bool, W.ubits(w), flat(t))), Nat.add(S.count(W.ubits(w)), S.count(flat(t))), BL.count_append(W.ubits(w), flat(t))) 122 123 def members_words(+ws: List<&2, U32>, +off: Nat) -> {MD.members_words(ws, off) == S.members(flat(ws), off) : List<&2, Nat>}: 124 match ws: 125 case Nil{}: 126 {==} 127 case Con{w, t}: 128 %Equal.sym(List<&2, Nat>, B.word_members(32n, w, off, MD.members_words(t, Nat.add(32n, off))), SC.append(Nat, S.members(SC.take(Bool, W.ubits(w), 32n), off), MD.members_words(t, Nat.add(32n, off))), W.word_members(32n, w, off, MD.members_words(t, Nat.add(32n, off)))) : {_ == S.members(SC.append(Bool, W.ubits(w), flat(t)), off) : List<&2, Nat>} 129 %Equal.sym(List<&2, Bool>, SC.take(Bool, W.ubits(w), 32n), W.ubits(w), take32(w)) : {SC.append(Nat, S.members(_, off), MD.members_words(t, Nat.add(32n, off))) == S.members(SC.append(Bool, W.ubits(w), flat(t)), off) : List<&2, Nat>} 130 %Equal.sym(List<&2, Nat>, MD.members_words(t, Nat.add(32n, off)), S.members(flat(t), Nat.add(32n, off)), members_words(t, Nat.add(32n, off))) : {SC.append(Nat, S.members(W.ubits(w), off), _) == S.members(SC.append(Bool, W.ubits(w), flat(t)), off) : List<&2, Nat>} 131 %Equal.sym(List<&2, Nat>, S.members(SC.append(Bool, W.ubits(w), flat(t)), off), SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(SC.length(Bool, W.ubits(w)), off))), BL.members_append(W.ubits(w), flat(t), off)) : {SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(32n, off))) == _ : List<&2, Nat>} 132 %Equal.sym(Nat, SC.length(Bool, W.ubits(w)), 32n, W.ulen(w)) : {SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(32n, off))) == SC.append(Nat, S.members(W.ubits(w), off), S.members(flat(t), Nat.add(_, off))) : List<&2, Nat>} 133 {==} 134 135 # ---- invariant preservation facts ---- 136 137 def invf_update(+n: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, n) == True{} : Bool}, +g: {invf(n, xs) == True{} : Bool}) -> {invf(n, SC.update(Bool, xs, i, v)) == True{} : Bool}: 138 +el = Equal.sym(Nat, SC.length(Bool, SC.update(Bool, xs, i, v)), SC.length(Bool, xs), LL.length_update(Bool, xs, i, v)) 139 inv_mk(n, SC.update(Bool, xs, i, v), 140 L.subst(Nat, k => {Nat.is_le(n, k) == True{} : Bool}, SC.length(Bool, xs), SC.length(Bool, SC.update(Bool, xs, i, v)), el, inv_le(n, xs, g)), 141 L.subst(List<&2, Bool>, d => {BL.allf(d) == True{} : Bool}, SC.drop(Bool, xs, n), SC.drop(Bool, SC.update(Bool, xs, i, v), n), Equal.sym(List<&2, Bool>, SC.drop(Bool, SC.update(Bool, xs, i, v), n), SC.drop(Bool, xs, n), BL.drop_update(xs, i, v, n, h)), inv_tail(n, xs, g))) 142 143 def invf_zipk(+k: B.WordOp, +n: Nat, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +gx: {invf(n, xs) == True{} : Bool}, +gy: {invf(n, ys) == True{} : Bool}) -> {invf(n, BL.zipk(k, xs, ys)) == True{} : Bool}: 144 inv_mk(n, BL.zipk(k, xs, ys), 145 BL.le_length_zipk(k, n, xs, ys, inv_le(n, xs, gx), inv_le(n, ys, gy)), 146 %Equal.sym(List<&2, Bool>, SC.drop(Bool, BL.zipk(k, xs, ys), n), BL.zipk(k, SC.drop(Bool, xs, n), SC.drop(Bool, ys, n)), BL.drop_zipk(k, xs, ys, n)) : {BL.allf(_) == True{} : Bool} 147 BL.allf_zipk(k, SC.drop(Bool, xs, n), SC.drop(Bool, ys, n), inv_tail(n, xs, gx), inv_tail(n, ys, gy))) 148 149 # put_walk as seen through the abstraction. 150 def put_abs(+n: Nat, +ws: List<&2, U32>, +i: Nat, +v: Bool) -> {SC.take(Bool, flat(MD.put_walk(ws, i, v)), n) == SC.update(Bool, SC.take(Bool, flat(ws), n), i, v) : List<&2, Bool>}: 151 %Equal.sym(List<&2, Bool>, flat(MD.put_walk(ws, i, v)), SC.update(Bool, flat(ws), i, v), put_walk(ws, i, v)) : {SC.take(Bool, _, n) == SC.update(Bool, SC.take(Bool, flat(ws), n), i, v) : List<&2, Bool>} 152 BL.take_update(flat(ws), i, v, n) 153 154 def put_inv(+n: Nat, +ws: List<&2, U32>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, n) == True{} : Bool}, +g: {invf(n, flat(ws)) == True{} : Bool}) -> {invf(n, flat(MD.put_walk(ws, i, v))) == True{} : Bool}: 155 L.subst(List<&2, Bool>, x => {invf(n, x) == True{} : Bool}, SC.update(Bool, flat(ws), i, v), flat(MD.put_walk(ws, i, v)), Equal.sym(List<&2, Bool>, flat(MD.put_walk(ws, i, v)), SC.update(Bool, flat(ws), i, v), put_walk(ws, i, v)), invf_update(n, flat(ws), i, v, h, g)) 156 157 # ---- the representation: a word array of depth d holding n logical bits ---- 158 # 159 # Base.Array is linear, so (exactly as in proofs/dynamic_array) the statements 160 # are about `A.thaw(t)`, the array built from the Data mirror tree t. 161 162 def rep(+n: Nat, +d: Nat, +t: A.Tree) -> Bool: 163 Bool.and(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t))))) 164 165 def abs(+n: Nat, +t: A.Tree) -> List<&2, Bool>: 166 SC.take(Bool, flat(AR.ws(t)), n) 167 168 def rep_depth(+n: Nat, +d: Nat, +t: A.Tree, +g: {rep(n, d, t) == True{} : Bool}) -> {Nat.is_eq(d, B.depth_for(n)) == True{} : Bool}: 169 L.and_left(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), g) 170 171 def rep_perfect(+n: Nat, +d: Nat, +t: A.Tree, +g: {rep(n, d, t) == True{} : Bool}) -> {A.perfect(B.Wd, d, t) == True{} : Bool}: 172 L.and_left(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t))), 173 L.and_right(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), g)) 174 175 def rep_invf(+n: Nat, +d: Nat, +t: A.Tree, +g: {rep(n, d, t) == True{} : Bool}) -> {invf(n, flat(AR.ws(t))) == True{} : Bool}: 176 L.and_right(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t))), 177 L.and_right(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), g)) 178 179 def rep_mk(+n: Nat, +d: Nat, +t: A.Tree, +a: {Nat.is_eq(d, B.depth_for(n)) == True{} : Bool}, +b: {A.perfect(B.Wd, d, t) == True{} : Bool}, +c: {invf(n, flat(AR.ws(t))) == True{} : Bool}) -> {rep(n, d, t) == True{} : Bool}: 180 L.and_intro(Nat.is_eq(d, B.depth_for(n)), Bool.and(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t)))), a, 181 L.and_intro(A.perfect(B.Wd, d, t), invf(n, flat(AR.ws(t))), b, c)) 182 183 def rep_lt(+n: Nat, +d: Nat, +t: A.Tree, +g: {rep(n, d, t) == True{} : Bool}) -> {Nat.is_lt(d, 32n) == True{} : Bool}: 184 L.subst(Nat, z => {Nat.is_lt(z, 32n) == True{} : Bool}, B.depth_for(n), d, 185 Equal.sym(Nat, d, B.depth_for(n), N.eq_from_is_eq(d, B.depth_for(n), rep_depth(n, d, t, g))), 186 DP.depth_lt(n)) 187 188 # ---- the all-zero array ---- 189 190 def length_flat(ws: List<&2, U32>) -> {SC.length(Bool, flat(ws)) == Nat.mul(SC.length(U32, ws), 32n) : Nat}: 191 match ws: 192 case Nil{}: 193 {==} 194 case Con{+w, +t}: 195 %Equal.sym(Nat, SC.length(Bool, flat(Con{w, t})), Nat.add(32n, SC.length(Bool, flat(t))), length_flat_cons(w, t)) : {_ == Nat.mul(SC.length(U32, Con{w, t}), 32n) : Nat} 196 Equal.cong(Nat, Nat, z => Nat.add(32n, z), SC.length(Bool, flat(t)), Nat.mul(SC.length(U32, t), 32n), length_flat(t)) 197 198 def flat_zeros(+m: Nat) -> {BL.allf(flat(SC.replicate(U32, m, 0))) == True{} : Bool}: 199 match m: 200 case 0n: 201 {==} 202 case 1n+p: 203 BL.allf_append(W.ubits(0), flat(SC.replicate(U32, p, 0)), {==}, flat_zeros(p)) 204 205 def zero_length(+d: Nat) -> {SC.length(Bool, flat(AR.ws(A.trep(B.Wd, d, B.W{0})))) == Nat.mul(SC.pow2(d), 32n) : Nat}: 206 %Equal.sym(List<&2, U32>, AR.ws(A.trep(B.Wd, d, B.W{0})), SC.replicate(U32, SC.pow2(d), 0), AR.ws_trep(d, 0)) : {SC.length(Bool, flat(_)) == Nat.mul(SC.pow2(d), 32n) : Nat} 207 %LL.length_replicate(U32, SC.pow2(d), 0) : {SC.length(Bool, flat(SC.replicate(U32, SC.pow2(d), 0))) == Nat.mul(_, 32n) : Nat} 208 length_flat(SC.replicate(U32, SC.pow2(d), 0)) 209 210 def zero_allf(+d: Nat) -> {BL.allf(flat(AR.ws(A.trep(B.Wd, d, B.W{0})))) == True{} : Bool}: 211 %Equal.sym(List<&2, U32>, AR.ws(A.trep(B.Wd, d, B.W{0})), SC.replicate(U32, SC.pow2(d), 0), AR.ws_trep(d, 0)) : {BL.allf(flat(_)) == True{} : Bool} 212 flat_zeros(SC.pow2(d)) 213 214 # `fits` is the documented capacity condition: the depth the representation is 215 # allowed to reach (2^31 words = 2^36 bits) must cover n. 216 def new_le(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Bool, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))))) == True{} : Bool}: 217 L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, Nat.mul(SC.pow2(B.depth_for(n)), 32n), SC.length(Bool, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0})))), 218 Equal.sym(Nat, SC.length(Bool, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0})))), Nat.mul(SC.pow2(B.depth_for(n)), 32n), zero_length(B.depth_for(n))), h) 219 220 def new_rep(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {rep(n, B.depth_for(n), A.trep(B.Wd, B.depth_for(n), B.W{0})) == True{} : Bool}: 221 rep_mk(n, B.depth_for(n), A.trep(B.Wd, B.depth_for(n), B.W{0}), 222 N.is_eq_refl(B.depth_for(n)), 223 A.trep_perfect(B.Wd, B.depth_for(n), B.W{0}), 224 inv_mk(n, flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))), new_le(n, h), 225 BL.drop_allf(flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))), n, zero_allf(B.depth_for(n))))) 226 227 def new_abs(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {abs(n, A.trep(B.Wd, B.depth_for(n), B.W{0})) == S.new(n) : List<&2, Bool>}: 228 BL.take_allf(flat(AR.ws(A.trep(B.Wd, B.depth_for(n), B.W{0}))), n, zero_allf(B.depth_for(n)), new_le(n, h)) 229 230 # `new(n)` is that array, thawed. 231 def new_form(+n: Nat) -> {B.new(n) == B.BS{n, B.depth_for(n), A.thaw(B.Wd, A.trep(B.Wd, B.depth_for(n), B.W{0}))} : B.Bitset}: 232 Equal.cong(Array, B.Bitset, a => B.BS{n, B.depth_for(n), a}, 233 Array.new(B.Wd, B.depth_for(n), B.W{0}), A.thaw(B.Wd, A.trep(B.Wd, B.depth_for(n), B.W{0})), 234 A.new(B.Wd, B.depth_for(n), B.W{0})) 235 236 # ---- the shadow: the Data mirror of a live bitset ---- 237 238 type Sh is Data: 239 Sh{len: Nat, depth: Nat, tree: A.Tree} 240 241 def real(sh: Sh) -> B.Bitset: 242 match sh: 243 case Sh{n, d, t}: 244 B.BS{n, d, A.thaw(B.Wd, t)} 245 246 def good(sh: Sh) -> Bool: 247 match sh: 248 case Sh{n, d, t}: 249 rep(n, d, t) 250 251 def model(sh: Sh) -> List<&2, Bool>: 252 match sh: 253 case Sh{n, d, t}: 254 abs(n, t) 255 256 # The stored bit count is 32 per word. 257 def flat_len(+d: Nat, +t: A.Tree, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {SC.length(Bool, flat(AR.ws(t))) == Nat.mul(SC.pow2(d), 32n) : Nat}: 258 %AR.ws_length(d, t, pf) : {SC.length(Bool, flat(AR.ws(t))) == Nat.mul(_, 32n) : Nat} 259 length_flat(AR.ws(t)) 260 261 # Any bitset satisfying the invariant is within the capacity. 262 def rep_fits(+n: Nat, +d: Nat, +t: A.Tree, +g: {rep(n, d, t) == True{} : Bool}) -> {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}: 263 L.subst(Nat, z => {Nat.is_le(n, Nat.mul(SC.pow2(z), 32n)) == True{} : Bool}, d, B.depth_for(n), 264 N.eq_from_is_eq(d, B.depth_for(n), rep_depth(n, d, t, g)), 265 L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, SC.length(Bool, flat(AR.ws(t))), Nat.mul(SC.pow2(d), 32n), 266 flat_len(d, t, rep_perfect(n, d, t, g)), inv_le(n, flat(AR.ws(t)), rep_invf(n, d, t, g)))) 267 268 # A bit index below the logical size addresses a word inside the array. 269 def wordix_go(m: Nat, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +h: {Nat.is_lt(i, Nat.mul(m, 32n)) == True{} : Bool}) -> {Nat.is_lt(B.wordix(i), m) == True{} : Bool}: 270 match m b: 271 case 0n _: 272 Empty.absurd({Nat.is_lt(B.wordix(i), 0n) == True{} : Bool}, N.lt_zero_absurd(i, h)) 273 case 1n+ +p True{}: 274 %Equal.sym(Nat, B.wordix(i), 0n, DP.wordix_small_alias(i, eb)) : {Nat.is_lt(_, 1n+p) == True{} : Bool} 275 {==} 276 case 1n+ +p False{}: 277 %Equal.sym(Nat, B.wordix(i), 1n+B.wordix(Nat.sub(i, 32n)), DP.wordix_step_alias(i, eb)) : {Nat.is_lt(_, 1n+p) == True{} : Bool} 278 wordix_go(p, Nat.sub(i, 32n), Nat.is_lt(Nat.sub(i, 32n), 32n), {==}, 279 N.sub_lt(i, 32n, Nat.mul(p, 32n), N.not_lt_le(i, 32n, eb), h)) 280 281 def wordix_lt(+i: Nat, +m: Nat, +h: {Nat.is_lt(i, Nat.mul(m, 32n)) == True{} : Bool}) -> {Nat.is_lt(B.wordix(i), m) == True{} : Bool}: 282 wordix_go(m, i, Nat.is_lt(i, 32n), {==}, h) 283 284 # Releasing a bitset is the unit: `burn_list` consumes any finite list. 285 def burn_any(xs: List) -> {B.burn_list(xs) == Unit{} : Unit}: 286 match xs: 287 case Nil{}: 288 {==} 289 case Con{x, t}: 290 burn_any(t) 291 292 def dispose_ok(+n: Nat, +d: Nat, t: A.Tree) -> {B.dispose(B.BS{n, d, A.thaw(B.Wd, t)}) == Unit{} : Unit}: 293 {==} 294 295 # ---- the shadow of a live bitset is unique ---- 296 # 297 # Every law about an operation says "the real operation lands on the array of 298 # THIS shadow", and then states the model and the invariant of that shadow. 299 # That is only meaningful if a runtime bitset determines its shadow, i.e. if 300 # `real` is injective - otherwise a proof could name a different shadow that 301 # happens to have the same `real` and claim its model. It is. 302 303 def blen_go(+n: Nat, u: Unit) -> Nat: 304 match u: 305 case Unit{}: 306 n 307 308 def blen(s: B.Bitset) -> Nat: 309 match s: 310 case B.BS{+n, d, a}: 311 blen_go(n, B.burn(a)) 312 313 def bdepth(s: B.Bitset) -> Nat: 314 match s: 315 case B.BS{n, +d, a}: 316 blen_go(d, B.burn(a)) 317 318 def btree(s: B.Bitset) -> A.Tree: 319 match s: 320 case B.BS{n, d, a}: 321 A.freeze(B.Wd, a) 322 323 def sh_len(sh: Sh) -> Nat: 324 match sh: 325 case Sh{n, d, t}: 326 n 327 328 def sh_depth(sh: Sh) -> Nat: 329 match sh: 330 case Sh{n, d, t}: 331 d 332 333 def sh_tree(sh: Sh) -> A.Tree: 334 match sh: 335 case Sh{n, d, t}: 336 t 337 338 def real_len(+sh: Sh) -> {blen(real(sh)) == sh_len(sh) : Nat}: 339 match sh: 340 case Sh{+n, d, t}: 341 {==} 342 343 def real_depth(+sh: Sh) -> {bdepth(real(sh)) == sh_depth(sh) : Nat}: 344 match sh: 345 case Sh{n, +d, t}: 346 {==} 347 348 def real_tree(+sh: Sh) -> {btree(real(sh)) == sh_tree(sh) : A.Tree}: 349 match sh: 350 case Sh{n, d, +t}: 351 A.freeze_thaw(B.Wd, t) 352 353 def sh_eta(+sh: Sh) -> {sh == Sh{sh_len(sh), sh_depth(sh), sh_tree(sh)} : Sh}: 354 match sh: 355 case Sh{n, d, t}: 356 {==} 357 358 def real_inj_parts(+a: Sh, +b: Sh, +e: {real(a) == real(b) : B.Bitset}) -> {Sh{sh_len(a), sh_depth(a), sh_tree(a)} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh}: 359 %real_len(a) : {Sh{_, sh_depth(a), sh_tree(a)} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh} 360 %real_depth(a) : {Sh{blen(real(a)), _, sh_tree(a)} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh} 361 %real_tree(a) : {Sh{blen(real(a)), bdepth(real(a)), _} == Sh{sh_len(b), sh_depth(b), sh_tree(b)} : Sh} 362 %real_len(b) : {Sh{blen(real(a)), bdepth(real(a)), btree(real(a))} == Sh{_, sh_depth(b), sh_tree(b)} : Sh} 363 %real_depth(b) : {Sh{blen(real(a)), bdepth(real(a)), btree(real(a))} == Sh{blen(real(b)), _, sh_tree(b)} : Sh} 364 %real_tree(b) : {Sh{blen(real(a)), bdepth(real(a)), btree(real(a))} == Sh{blen(real(b)), bdepth(real(b)), _} : Sh} 365 Equal.cong(B.Bitset, Sh, s => Sh{blen(s), bdepth(s), btree(s)}, real(a), real(b), e) 366 367 def real_inj(+a: Sh, +b: Sh, +e: {real(a) == real(b) : B.Bitset}) -> {a == b : Sh}: 368 Equal.trans(Sh, a, Sh{sh_len(a), sh_depth(a), sh_tree(a)}, b, 369 sh_eta(a), 370 Equal.trans(Sh, Sh{sh_len(a), sh_depth(a), sh_tree(a)}, Sh{sh_len(b), sh_depth(b), sh_tree(b)}, b, 371 real_inj_parts(a, b, e), 372 Equal.sym(Sh, b, Sh{sh_len(b), sh_depth(b), sh_tree(b)}, sh_eta(b))))