1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/u32.bend as U 6 import ../../lib/array.bend as A 7 import ../../../spec/lib/common.bend as SC 8 import ../../../src/containers/bitset.bend as B 9 import ./model.bend as MD 10 import ./walk.bend as WK 11 import ./listx.bend as LX 12 13 # The bridge between src/bitset.bend's native Base.Array of words and the 14 # word list the rest of the proof talks about. 15 # 16 # Arrays are linear, so (exactly as in proofs/dynamic_array) every statement 17 # is about `A.thaw(t)`, the array built from a Data mirror tree `t` of the 18 # same shape; `ws(t)` is the list of the words it holds. 19 20 def wmap(xs: List<&2, B.Wd>) -> List<&2, U32>: 21 match xs: 22 case Nil{}: 23 Nil{} 24 case Con{x, t}: 25 Con{B.wval(x), wmap(t)} 26 27 def ws(t: A.Tree) -> List<&2, U32>: 28 wmap(A.slots(B.Wd, t)) 29 30 # Slot q of a word list (the callers always stay in range; the default keeps 31 # the function total and agrees with WK.nthw's default). 32 def nths(xs: List<&2, B.Wd>, q: Nat) -> B.Wd: 33 match xs q: 34 case Nil{} _: 35 B.W{0} 36 case Con{x, t} 0n: 37 x 38 case Con{x, t} 1n+p: 39 nths(t, p) 40 41 # ---- wmap ---- 42 43 def wmap_length(xs: List<&2, B.Wd>) -> {SC.length(U32, wmap(xs)) == SC.length(B.Wd, xs) : Nat}: 44 match xs: 45 case Nil{}: 46 {==} 47 case Con{x, +t}: 48 N.succ_cong(SC.length(U32, wmap(t)), SC.length(B.Wd, t), wmap_length(t)) 49 50 def wmap_update(xs: List<&2, B.Wd>, q: Nat, +v: U32) -> {wmap(SC.update(B.Wd, xs, q, B.W{v})) == SC.update(U32, wmap(xs), q, v) : List<&2, U32>}: 51 match xs q: 52 case Nil{} _: 53 {==} 54 case Con{x, t} 0n: 55 {==} 56 case Con{+x, +t} 1n+p: 57 Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{B.wval(x), z}, 58 wmap(SC.update(B.Wd, t, p, B.W{v})), SC.update(U32, wmap(t), p, v), wmap_update(t, p, v)) 59 60 def wval_nths(xs: List<&2, B.Wd>, q: Nat) -> {B.wval(nths(xs, q)) == WK.nthw(wmap(xs), q) : U32}: 61 match xs q: 62 case Nil{} _: 63 {==} 64 case Con{x, t} 0n: 65 {==} 66 case Con{x, t} 1n+p: 67 wval_nths(t, p) 68 69 def nths_nth(xs: List<&2, B.Wd>, q: Nat, +h: {Nat.is_lt(q, SC.length(B.Wd, xs)) == True{} : Bool}) -> {SC.nth(B.Wd, xs, q) == Some{nths(xs, q)} : Maybe<&2, B.Wd>}: 70 match xs q: 71 case Nil{} _: 72 Empty.absurd({SC.nth(B.Wd, Nil{}, q) == Some{nths(Nil{}, q)} : Maybe<&2, B.Wd>}, N.lt_zero_absurd(q, h)) 73 case Con{x, t} 0n: 74 {==} 75 case Con{x, t} 1n+p: 76 nths_nth(t, p, h) 77 78 # ---- shape ---- 79 80 def ws_length(+d: Nat, +t: A.Tree, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {SC.length(U32, ws(t)) == SC.pow2(d) : Nat}: 81 Equal.trans(Nat, SC.length(U32, wmap(A.slots(B.Wd, t))), SC.length(B.Wd, A.slots(B.Wd, t)), SC.pow2(d), 82 wmap_length(A.slots(B.Wd, t)), A.slots_length(B.Wd, d, t, pf)) 83 84 def slots_lt(+d: Nat, +t: A.Tree, +q: Nat, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(q, SC.length(B.Wd, A.slots(B.Wd, t))) == True{} : Bool}: 85 L.subst(Nat, k => {Nat.is_lt(q, k) == True{} : Bool}, SC.pow2(d), SC.length(B.Wd, A.slots(B.Wd, t)), 86 Equal.sym(Nat, SC.length(B.Wd, A.slots(B.Wd, t)), SC.pow2(d), A.slots_length(B.Wd, d, t, pf)), hq) 87 88 def idx_ok(+d: Nat, +q: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(q)) == q : Nat}: 89 U.to_nat_from_nat(q, d, N.lt_le(d, 32n, hd), hq) 90 91 # ---- read ---- 92 93 def read_ok(+d: Nat, +t: A.Tree, +q: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {B.read(A.thaw(B.Wd, t), d, q) == (A.thaw(B.Wd, t), WK.nthw(ws(t), q)) : Array & U32}: 94 %wval_nths(A.slots(B.Wd, t), q) : {B.read(A.thaw(B.Wd, t), d, q) == (A.thaw(B.Wd, t), _) : Array & U32} 95 Equal.cong(Array & B.Wd, Array & U32, B.read_fin, 96 Array.get(B.Wd, A.thaw(B.Wd, t), U32.from_nat(q)), 97 (A.thaw(B.Wd, t), nths(A.slots(B.Wd, t), q)), 98 A.get(B.Wd, d, t, U32.from_nat(q), nths(A.slots(B.Wd, t), q), hd, 99 L.subst(Nat, j => {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), hq), 100 L.subst(Nat, j => {SC.nth(B.Wd, A.slots(B.Wd, t), j) == Some{nths(A.slots(B.Wd, t), q)} : Maybe<&2, B.Wd>}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), nths_nth(A.slots(B.Wd, t), q, slots_lt(d, t, q, pf, hq))), 101 pf)) 102 103 # ---- write ---- 104 105 def write_ok(+d: Nat, +t: A.Tree, +q: Nat, +v: U32, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {B.write(A.thaw(B.Wd, t), d, q, v) == A.thaw(B.Wd, A.upd(B.Wd, d, t, q, B.W{v})) : Array}: 106 %idx_ok(d, q, hd, hq) : {B.write(A.thaw(B.Wd, t), d, q, v) == A.thaw(B.Wd, A.upd(B.Wd, d, t, _, B.W{v})) : Array} 107 A.set(B.Wd, d, t, U32.from_nat(q), B.W{v}, nths(A.slots(B.Wd, t), q), hd, 108 L.subst(Nat, j => {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), hq), 109 L.subst(Nat, j => {SC.nth(B.Wd, A.slots(B.Wd, t), j) == Some{nths(A.slots(B.Wd, t), q)} : Maybe<&2, B.Wd>}, q, U32.to_nat(U32.from_nat(q)), Equal.sym(Nat, U32.to_nat(U32.from_nat(q)), q, idx_ok(d, q, hd, hq)), nths_nth(A.slots(B.Wd, t), q, slots_lt(d, t, q, pf, hq))), 110 pf) 111 112 def ws_upd(+d: Nat, +t: A.Tree, +q: Nat, +v: U32, +hq: {Nat.is_lt(q, SC.pow2(d)) == True{} : Bool}, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {ws(A.upd(B.Wd, d, t, q, B.W{v})) == SC.update(U32, ws(t), q, v) : List<&2, U32>}: 113 Equal.trans(List<&2, U32>, wmap(A.slots(B.Wd, A.upd(B.Wd, d, t, q, B.W{v}))), wmap(SC.update(B.Wd, A.slots(B.Wd, t), q, B.W{v})), SC.update(U32, wmap(A.slots(B.Wd, t)), q, v), 114 Equal.cong(List<&2, B.Wd>, List<&2, U32>, wmap, A.slots(B.Wd, A.upd(B.Wd, d, t, q, B.W{v})), SC.update(B.Wd, A.slots(B.Wd, t), q, B.W{v}), A.upd_slots(B.Wd, d, t, q, B.W{v}, hq, pf)), 115 wmap_update(A.slots(B.Wd, t), q, v)) 116 117 def upd_perfect(+d: Nat, +t: A.Tree, +q: Nat, +v: U32, +pf: {A.perfect(B.Wd, d, t) == True{} : Bool}) -> {A.perfect(B.Wd, d, A.upd(B.Wd, d, t, q, B.W{v})) == True{} : Bool}: 118 A.upd_perfect(B.Wd, d, t, q, B.W{v}, pf) 119 120 def wmap_replicate(+m: Nat, +v: U32) -> {wmap(SC.replicate(B.Wd, m, B.W{v})) == SC.replicate(U32, m, v) : List<&2, U32>}: 121 match m: 122 case 0n: 123 {==} 124 case 1n+p: 125 Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{v, z}, 126 wmap(SC.replicate(B.Wd, p, B.W{v})), SC.replicate(U32, p, v), wmap_replicate(p, v)) 127 128 def ws_trep(+d: Nat, +v: U32) -> {ws(A.trep(B.Wd, d, B.W{v})) == SC.replicate(U32, SC.pow2(d), v) : List<&2, U32>}: 129 Equal.trans(List<&2, U32>, wmap(A.slots(B.Wd, A.trep(B.Wd, d, B.W{v}))), wmap(SC.replicate(B.Wd, SC.pow2(d), B.W{v})), SC.replicate(U32, SC.pow2(d), v), 130 Equal.cong(List<&2, B.Wd>, List<&2, U32>, wmap, A.slots(B.Wd, A.trep(B.Wd, d, B.W{v})), SC.replicate(B.Wd, SC.pow2(d), B.W{v}), A.trep_slots(B.Wd, d, B.W{v})), 131 wmap_replicate(SC.pow2(d), v))