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 AR 7 import ../../../spec/lib/common.bend as SC 8 import ../../../src/containers/dynamic_array.bend as DA 9 import ./layout.bend as LY 10 import ./state.bend as ST 11 12 # `to_list_at` reads the `length` occupied slots by index, last one first, and 13 # conses them. This file proves that this indexed read walk produces exactly 14 # `LY.somes` of the slot list -- the same list the parametric `to_list` 15 # produces by cloning and flattening -- without cloning the array and without 16 # a structural traversal. 17 18 def unwrap(-T: Data, m: Maybe<&2, Maybe<&2, T>>) -> Maybe<&2, T>: 19 match m: 20 case None{}: 21 None{} 22 case Some{s}: 23 s 24 25 # the content of slot j 26 def slot(-T: Data, +xs: List<&2, Maybe<&2, T>>, +j: Nat) -> Maybe<&2, T>: 27 unwrap(T, SC.nth(Maybe<&2, T>, xs, j)) 28 29 def nth_slot(-T: Data, +xs: List<&2, Maybe<&2, T>>, +j: Nat, +hj: {Nat.is_lt(j, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, xs, j) == Some{slot(T, xs, j)} : Maybe<&2, Maybe<&2, T>>}: 30 match xs j: 31 case Nil{} _: 32 Empty.absurd({None{} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, N.lt_zero_absurd(j, hj)) 33 case Con{x, r} 0n: 34 {==} 35 case Con{x, +r} 1n+k: 36 nth_slot(T, r, k, hj) 37 38 def get_slot(-T: Data, +l: Nat, +d: Nat, +t: AR.Tree>, +j: Nat, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}) -> {Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(j)) == (AR.thaw(Maybe<&2, T>, t), slot(T, AR.slots(Maybe<&2, T>, t), j)) : Array> & Maybe<&2, T>}: 39 +ss = AR.slots(Maybe<&2, T>, t) 40 +ej = U.to_nat_from_nat(j, d, ST.le32(d, l, hd, hl), hj) 41 AR.get(Maybe<&2, T>, d, t, U32.from_nat(j), slot(T, ss, j), ST.lt32(d, l, hd, hl), 42 L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, j, U32.to_nat(U32.from_nat(j)), Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, ej), hj), 43 L.subst(Nat, z => {SC.nth(Maybe<&2, T>, ss, z) == Some{slot(T, ss, j)} : Maybe<&2, Maybe<&2, T>>}, j, U32.to_nat(U32.from_nat(j)), Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, ej), 44 nth_slot(T, ss, j, L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, T>, ss), Equal.sym(Nat, SC.length(Maybe<&2, T>, ss), SC.pow2(d), AR.slots_length(Maybe<&2, T>, d, t, pf)), hj))), 45 pf) 46 47 # ---- the walk on the slot list ---- 48 49 def tvals(k: Nat, -T: Data, +xs: List<&2, Maybe<&2, T>>, acc: List<&2, T>) -> List<&2, T>: 50 match k: 51 case 0n: 52 acc 53 case 1n+ +m: 54 tvals(m, T, xs, DA.cons_some(T, slot(T, xs, m), acc)) 55 56 def dec1_le(+m: Nat) -> {Nat.is_le(DA.dec1(m), m) == True{} : Bool}: 57 match m: 58 case 0n: 59 {==} 60 case 1n+p: 61 N.le_succ(p) 62 63 def tl_thaw(k: Nat, -T: Data, +l: Nat, +d: Nat, +t: AR.Tree>, acc: List<&2, T>, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hb: {Nat.is_lt(DA.dec1(k), SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}) -> {DA.tl_go(k, T, acc, (AR.thaw(Maybe<&2, T>, t), slot(T, AR.slots(Maybe<&2, T>, t), DA.dec1(k)))) == (AR.thaw(Maybe<&2, T>, t), tvals(k, T, AR.slots(Maybe<&2, T>, t), acc)) : Array> & List<&2, T>}: 64 match k: 65 case 0n: 66 {==} 67 case 1n+ +m: 68 +ss = AR.slots(Maybe<&2, T>, t) 69 +hj = N.le_lt_trans(DA.dec1(m), m, SC.pow2(d), dec1_le(m), hb) 70 %Equal.sym(Array> & Maybe<&2, T>, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(DA.dec1(m))), (AR.thaw(Maybe<&2, T>, t), slot(T, ss, DA.dec1(m))), get_slot(T, l, d, t, DA.dec1(m), hd, hl, hj, pf)) : {DA.tl_go(m, T, DA.cons_some(T, slot(T, ss, m), acc), _) == (AR.thaw(Maybe<&2, T>, t), tvals(1n+m, T, ss, acc)) : Array> & List<&2, T>} 71 tl_thaw(m, T, l, d, t, DA.cons_some(T, slot(T, ss, m), acc), hd, hl, hj, pf) 72 73 # ---- the walk on the slot list is the model ---- 74 75 def take_all(-T: Data, +ys: List<&2, T>, +n: Nat, +h: {SC.length(T, ys) == n : Nat}) -> {SC.take(T, ys, n) == ys : List<&2, T>}: 76 match ys n: 77 case Nil{} 0n: 78 {==} 79 case Nil{} 1n+m: 80 Empty.absurd({Nil{} == Nil{} : List<&2, T>}, N.zero_succ(m, h)) 81 case Con{y, r} 0n: 82 Empty.absurd({Nil{} == Con{y, r} : List<&2, T>}, N.succ_zero(SC.length(T, r), h)) 83 case Con{+y, +r} 1n+m: 84 LL.cons_cong(T, y, SC.take(T, r, m), r, take_all(T, r, m, N.succ_inj(SC.length(T, r), m, h))) 85 86 def take_cons_some(-T: Data, +ys: List<&2, T>, +m: Nat, +acc: List<&2, T>, +hm: {Nat.is_lt(m, SC.length(T, ys)) == True{} : Bool}) -> {SC.append(T, SC.take(T, ys, m), DA.cons_some(T, SC.nth(T, ys, m), acc)) == SC.append(T, SC.take(T, ys, 1n+m), acc) : List<&2, T>}: 87 match ys m: 88 case Nil{} _: 89 Empty.absurd({DA.cons_some(T, None{}, acc) == acc : List<&2, T>}, N.lt_zero_absurd(m, hm)) 90 case Con{y, +r} 0n: 91 %Equal.sym(List<&2, T>, SC.take(T, r, 0n), Nil{}, LL.sc_take_zero(T, r)) : {Con{y, acc} == SC.append(T, Con{y, _}, acc) : List<&2, T>} 92 {==} 93 case Con{+y, +r} 1n+k: 94 LL.cons_cong(T, y, SC.append(T, SC.take(T, r, k), DA.cons_some(T, SC.nth(T, r, k), acc)), SC.append(T, SC.take(T, r, 1n+k), acc), take_cons_some(T, r, k, acc, hm)) 95 96 def slot_nth(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +m: Nat, +h: {LY.lay(T, xs, n) == True{} : Bool}, +hm: {Nat.is_lt(m, n) == True{} : Bool}) -> {slot(T, xs, m) == SC.nth(T, LY.somes(T, xs), m) : Maybe<&2, T>}: 97 %Equal.sym(Maybe<&2, Maybe<&2, T>>, SC.nth(Maybe<&2, T>, xs, m), Some{SC.nth(T, LY.somes(T, xs), m)}, LY.lay_nth(T, xs, n, m, h, hm)) : {unwrap(T, _) == SC.nth(T, LY.somes(T, xs), m) : Maybe<&2, T>} 98 {==} 99 100 def tvals_take(k: Nat, -T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +acc: List<&2, T>, +h: {LY.lay(T, xs, n) == True{} : Bool}, +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {tvals(k, T, xs, acc) == SC.append(T, SC.take(T, LY.somes(T, xs), k), acc) : List<&2, T>}: 101 match k: 102 case 0n: 103 %Equal.sym(List<&2, T>, SC.take(T, LY.somes(T, xs), 0n), Nil{}, LL.sc_take_zero(T, LY.somes(T, xs))) : {acc == SC.append(T, _, acc) : List<&2, T>} 104 {==} 105 case 1n+ +m: 106 +ys = LY.somes(T, xs) 107 +hm = N.succ_le_lt(m, n, hk) 108 +hlen = N.lt_le_trans(m, n, SC.length(T, ys), hm, N.eq_le(n, SC.length(T, ys), Equal.sym(Nat, SC.length(T, ys), n, LY.lay_len(T, xs, n, h)))) 109 %Equal.sym(Maybe<&2, T>, slot(T, xs, m), SC.nth(T, ys, m), slot_nth(T, xs, n, m, h, hm)) : {tvals(m, T, xs, DA.cons_some(T, _, acc)) == SC.append(T, SC.take(T, ys, 1n+m), acc) : List<&2, T>} 110 %take_cons_some(T, ys, m, acc, hlen) : {tvals(m, T, xs, DA.cons_some(T, SC.nth(T, ys, m), acc)) == _ : List<&2, T>} 111 tvals_take(m, T, xs, n, DA.cons_some(T, SC.nth(T, ys, m), acc), h, N.lt_le(m, n, hm)) 112 113 def tvals_model(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +h: {LY.lay(T, xs, n) == True{} : Bool}) -> {tvals(n, T, xs, Nil{}) == LY.somes(T, xs) : List<&2, T>}: 114 %take_all(T, LY.somes(T, xs), n, LY.lay_len(T, xs, n, h)) : {tvals(n, T, xs, Nil{}) == _ : List<&2, T>} 115 %LL.append_nil(T, SC.take(T, LY.somes(T, xs), n)) : {tvals(n, T, xs, Nil{}) == _ : List<&2, T>} 116 tvals_take(n, T, xs, n, Nil{}, h, N.le_refl(n))