1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32alg.bend as A 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/doubly_linked_list.bend as S 8 import ../../lib/u32div.bend as UD 9 import ../../../src/containers/internal/dlist_storage.bend as R 10 import ./state.bend as ST 11 import ./rel.bend as RL 12 import ./link.bend as LN 13 import ../../lib/nat_list.bend as NL 14 import ../../lib/links.bend as LK 15 import ../../lib/words32.bend as W32 16 import ../../lib/u32_tree.bend as UT 17 18 # to_list: the walk back from the tail along the prev links. 19 20 21 # every id of back is below fr and live, and its prev is the next id of back 22 def rok(~T: Data, +pl: List<&2, U32>, back: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>) -> Bool: 23 match back: 24 case Nil{}: 25 True{} 26 case Con{+x, +r}: 27 Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), Bool.and(U32.is_eq(W32.nth0(pl, x), LK.fst_or(r, 0)), rok(~T, pl, r, fr, vl))) 28 29 # the values of back prepended to acc, one by one 30 def racc(-T: Data, +vl: List<&2, Maybe<&2, T>>, back: List<&2, Nat>, acc: List<&2, T>) -> List<&2, T>: 31 match back: 32 case Nil{}: 33 acc 34 case Con{+x, r}: 35 racc(T, vl, r, S.cons_some(T, S.val_of(T, vl, x), acc)) 36 37 def cs_app(-T: Data, +m: Maybe<&2, T>, +xs: List<&2, T>, +acc: List<&2, T>) -> {SC.append(T, S.cons_some(T, m, xs), acc) == S.cons_some(T, m, SC.append(T, xs, acc)) : List<&2, T>}: 38 match m: 39 case None{}: 40 {==} 41 case Some{v}: 42 {==} 43 44 def ra_rapp(-T: Data, +vl: List<&2, Maybe<&2, T>>, +l: List<&2, Nat>, +b: List<&2, Nat>, +acc: List<&2, T>) -> {racc(T, vl, NL.rapp(l, b), acc) == racc(T, vl, b, SC.append(T, S.values(T, vl, l), acc)) : List<&2, T>}: 45 match l: 46 case Nil{}: 47 {==} 48 case Con{+x, +r}: 49 Equal.trans(List<&2, T>, racc(T, vl, NL.rapp(r, Con{x, b}), acc), racc(T, vl, b, S.cons_some(T, S.val_of(T, vl, x), SC.append(T, S.values(T, vl, r), acc))), racc(T, vl, b, SC.append(T, S.cons_some(T, S.val_of(T, vl, x), S.values(T, vl, r)), acc)), ra_rapp(T, vl, r, Con{x, b}, acc), Equal.cong(List<&2, T>, List<&2, T>, z => racc(T, vl, b, z), S.cons_some(T, S.val_of(T, vl, x), SC.append(T, S.values(T, vl, r), acc)), SC.append(T, S.cons_some(T, S.val_of(T, vl, x), S.values(T, vl, r)), acc), Equal.sym(List<&2, T>, SC.append(T, S.cons_some(T, S.val_of(T, vl, x), S.values(T, vl, r)), acc), S.cons_some(T, S.val_of(T, vl, x), SC.append(T, S.values(T, vl, r), acc)), cs_app(T, S.val_of(T, vl, x), S.values(T, vl, r), acc)))) 50 51 # a linked live list, reversed onto a back list, keeps its links backwards 52 def rok_app(~T: Data, +pl: List<&2, U32>, +nl: List<&2, U32>, +vl: List<&2, Maybe<&2, T>>, +l: List<&2, Nat>, +b: List<&2, Nat>, +fr: Nat, +p: U32, +q: U32, +hs: {ST.seg(pl, nl, l, p, q) == True{} : Bool}, +hl: {ST.slok(~T, l, fr, vl) == True{} : Bool}, +hb: {rok(~T, pl, b, fr, vl) == True{} : Bool}, +hp: {U32.is_eq(p, LK.fst_or(b, 0)) == True{} : Bool}) -> {rok(~T, pl, NL.rapp(l, b), fr, vl) == True{} : Bool}: 53 match l: 54 case Nil{}: 55 hb 56 case Con{+x, +r}: 57 +ha = L.and_left(U32.is_eq(W32.nth0(pl, x), p), Bool.and(U32.is_eq(W32.nth0(nl, x), LK.fst_or(r, q)), ST.seg(pl, nl, r, LK.lnk(x), q)), hs) 58 +hc = L.and_right(U32.is_eq(W32.nth0(nl, x), LK.fst_or(r, q)), ST.seg(pl, nl, r, LK.lnk(x), q), L.and_right(U32.is_eq(W32.nth0(pl, x), p), Bool.and(U32.is_eq(W32.nth0(nl, x), LK.fst_or(r, q)), ST.seg(pl, nl, r, LK.lnk(x), q)), hs)) 59 +hx = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, r, fr, vl), hl) 60 +hlr = L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, r, fr, vl), hl) 61 +e0 = A.eq_of(W32.nth0(pl, x), p, ha) 62 +hq = L.subst(U32, z => {U32.is_eq(z, LK.fst_or(b, 0)) == True{} : Bool}, p, W32.nth0(pl, x), Equal.sym(U32, W32.nth0(pl, x), p, e0), hp) 63 +hb2 = L.and_intro(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), Bool.and(U32.is_eq(W32.nth0(pl, x), LK.fst_or(b, 0)), rok(~T, pl, b, fr, vl)), hx, L.and_intro(U32.is_eq(W32.nth0(pl, x), LK.fst_or(b, 0)), rok(~T, pl, b, fr, vl), hq, hb)) 64 rok_app(~T, pl, nl, vl, r, Con{x, b}, fr, LK.lnk(x), q, hc, hlr, hb2, A.eq_refl(LK.lnk(x))) 65 66 # ---- the walk ---- 67 68 69 70 def step_live(-T: Data, +acc: List<&2, T>, +at: U32, +m: Maybe<&2, T>, +hm: {ST.some_b(T, m) == True{} : Bool}, -vals: Array>, -prevs: Array) -> {R.step_m(~T, vals, prevs, acc, at, m) == R.step_p(~T, vals, S.cons_some(T, m, acc), Array.get(U32, prevs, R.slot(at))) : R.Cur}: 71 match m: 72 case None{}: 73 Empty.absurd({R.step_m(~T, vals, prevs, acc, at, None{}) == R.step_p(~T, vals, acc, Array.get(U32, prevs, R.slot(at))) : R.Cur}, L.false_true(hm)) 74 case Some{v}: 75 {==} 76 77 # one step: the value of x is prepended and the walk moves to x's prev 78 def wstep(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +vT: AR.Tree>, +pT: AR.Tree, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +fr: Nat, +hfr: {Nat.is_le(fr, SC.pow2(d)) == True{} : Bool}, +x: Nat, +r: List<&2, Nat>, +acc: List<&2, T>, +hx: {Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, AR.slots(Maybe<&2, T>, vT), x)), Bool.and(U32.is_eq(W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0)), rok(~T, AR.slots(U32, pT), r, fr, AR.slots(Maybe<&2, T>, vT)))) == True{} : Bool}) -> {R.step_back(~T, R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), acc, LK.lnk(x)}) == R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), LK.fst_or(r, 0)} : R.Cur}: 79 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, AR.slots(Maybe<&2, T>, vT), x)), Bool.and(U32.is_eq(W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0)), rok(~T, AR.slots(U32, pT), r, fr, AR.slots(Maybe<&2, T>, vT))), hx) 80 +h2 = L.and_left(U32.is_eq(W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0)), rok(~T, AR.slots(U32, pT), r, fr, AR.slots(Maybe<&2, T>, vT)), L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, AR.slots(Maybe<&2, T>, vT), x)), Bool.and(U32.is_eq(W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0)), rok(~T, AR.slots(U32, pT), r, fr, AR.slots(Maybe<&2, T>, vT))), hx)) 81 +hn = N.lt_le_trans(x, fr, SC.pow2(d), L.and_left(Nat.is_lt(x, fr), ST.live(T, AR.slots(Maybe<&2, T>, vT), x), h0), hfr) 82 +es = RL.slot_lnk(one, h1, x, d, hd, hn) 83 +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, x, UD.v(R.slot(LK.lnk(x))), Equal.sym(Nat, UD.v(R.slot(LK.lnk(x))), x, es), hn) 84 +e1 = Equal.cong(Array> & Maybe<&2, T>, R.Cur, rr => R.step_v(~T, AR.thaw(U32, pT), acc, LK.lnk(x), rr), Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), R.slot(LK.lnk(x))), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), x)), Equal.trans(Array> & Maybe<&2, T>, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), R.slot(LK.lnk(x))), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(R.slot(LK.lnk(x))))), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), x)), LN.vget(T, d, hd, vT, pv, R.slot(LK.lnk(x)), hi), Equal.cong(Nat, Array> & Maybe<&2, T>, z => (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), z)), UD.v(R.slot(LK.lnk(x))), x, es))) 85 +e2 = step_live(T, acc, LK.lnk(x), S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), L.and_right(Nat.is_lt(x, fr), ST.live(T, AR.slots(Maybe<&2, T>, vT), x), h0), AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT)) 86 +e3 = Equal.cong(Array & U32, R.Cur, rr => R.step_p(~T, AR.thaw(Maybe<&2, T>, vT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), rr), Array.get(U32, AR.thaw(U32, pT), R.slot(LK.lnk(x))), (AR.thaw(U32, pT), W32.nth0(AR.slots(U32, pT), x)), Equal.trans(Array & U32, Array.get(U32, AR.thaw(U32, pT), R.slot(LK.lnk(x))), (AR.thaw(U32, pT), W32.nth0(AR.slots(U32, pT), UD.v(R.slot(LK.lnk(x))))), (AR.thaw(U32, pT), W32.nth0(AR.slots(U32, pT), x)), UT.uget(d, RL.hd0(d, hd), pT, pp, R.slot(LK.lnk(x)), hi), Equal.cong(Nat, Array & U32, z => (AR.thaw(U32, pT), W32.nth0(AR.slots(U32, pT), z)), UD.v(R.slot(LK.lnk(x))), x, es))) 87 +e4 = Equal.cong(U32, R.Cur, z => R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), z}, W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0), A.eq_of(W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0), h2)) 88 Equal.trans(R.Cur, R.step_back(~T, R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), acc, LK.lnk(x)}), R.step_v(~T, AR.thaw(U32, pT), acc, LK.lnk(x), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), x))), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), LK.fst_or(r, 0)}, e1, Equal.trans(R.Cur, R.step_m(~T, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), acc, LK.lnk(x), S.val_of(T, AR.slots(Maybe<&2, T>, vT), x)), R.step_p(~T, AR.thaw(Maybe<&2, T>, vT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), Array.get(U32, AR.thaw(U32, pT), R.slot(LK.lnk(x)))), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), LK.fst_or(r, 0)}, e2, Equal.trans(R.Cur, R.step_p(~T, AR.thaw(Maybe<&2, T>, vT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), Array.get(U32, AR.thaw(U32, pT), R.slot(LK.lnk(x)))), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), W32.nth0(AR.slots(U32, pT), x)}, R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), LK.fst_or(r, 0)}, e3, e4))) 89 90 # THEOREM: the walk from the first id of back, for its length, prepends the 91 # values of back one by one 92 def walk(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +vT: AR.Tree>, +pT: AR.Tree, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +fr: Nat, +hfr: {Nat.is_le(fr, SC.pow2(d)) == True{} : Bool}, +back: List<&2, Nat>, +acc: List<&2, T>, +hr: {rok(~T, AR.slots(U32, pT), back, fr, AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}) -> {R.walk(~T, SC.length(Nat, back), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), acc, LK.fst_or(back, 0)}) == R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), racc(T, AR.slots(Maybe<&2, T>, vT), back, acc), 0} : R.Cur}: 93 match back: 94 case Nil{}: 95 {==} 96 case Con{+x, +r}: 97 +ih = walk(~T, one, h1, d, hd, vT, pT, pv, pp, fr, hfr, r, S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), L.and_right(U32.is_eq(W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0)), rok(~T, AR.slots(U32, pT), r, fr, AR.slots(Maybe<&2, T>, vT)), L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, AR.slots(Maybe<&2, T>, vT), x)), Bool.and(U32.is_eq(W32.nth0(AR.slots(U32, pT), x), LK.fst_or(r, 0)), rok(~T, AR.slots(U32, pT), r, fr, AR.slots(Maybe<&2, T>, vT))), hr))) 98 Equal.trans(R.Cur, R.walk(~T, SC.length(Nat, r), R.step_back(~T, R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), acc, LK.lnk(x)})), R.walk(~T, SC.length(Nat, r), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), LK.fst_or(r, 0)}), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), racc(T, AR.slots(Maybe<&2, T>, vT), r, S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc)), 0}, Equal.cong(R.Cur, R.Cur, c => R.walk(~T, SC.length(Nat, r), c), R.step_back(~T, R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), acc, LK.lnk(x)}), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), S.cons_some(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), x), acc), LK.fst_or(r, 0)}, wstep(~T, one, h1, d, hd, vT, pT, pv, pp, fr, hfr, x, r, acc, hr)), ih)