~/bend-docscommunity

proofs/containers/doubly_linked_list/links.bend source

proofs/containers/doubly_linked_list/links.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../../spec/lib/common.bend as SCimport ./state.bend as STimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32# Segments of the two link lists: writes off a segment leave it, a segment# splits at an append, and its ends can be re-targeted.def seg_c(+pl1: List<&2, U32>, +nl1: List<&2, U32>, +pl2: List<&2, U32>, +nl2: List<&2, U32>, +s: Nat, +t: List<&2, Nat>, +p: U32, +q: U32, +e0: {W32.nth0(pl1, s) == W32.nth0(pl2, s) : U32}, +e1: {W32.nth0(nl1, s) == W32.nth0(nl2, s) : U32}, +ec: {ST.seg(pl1, nl1, t, LK.lnk(s), q) == ST.seg(pl2, nl2, t, LK.lnk(s), q) : Bool}) -> {ST.seg(pl1, nl1, Con{s, t}, p, q) == ST.seg(pl2, nl2, Con{s, t}, p, q) : Bool}:  +r1 = L.subst(U32, z => {Bool.and(U32.is_eq(z, p), Bool.and(U32.is_eq(W32.nth0(nl2, s), LK.fst_or(t, q)), ST.seg(pl2, nl2, t, LK.lnk(s), q))) == ST.seg(pl2, nl2, Con{s, t}, p, q) : Bool}, W32.nth0(pl2, s), W32.nth0(pl1, s), Equal.sym(U32, W32.nth0(pl1, s), W32.nth0(pl2, s), e0), {==})  +r2 = L.subst(U32, z => {Bool.and(U32.is_eq(W32.nth0(pl1, s), p), Bool.and(U32.is_eq(z, LK.fst_or(t, q)), ST.seg(pl2, nl2, t, LK.lnk(s), q))) == ST.seg(pl2, nl2, Con{s, t}, p, q) : Bool}, W32.nth0(nl2, s), W32.nth0(nl1, s), Equal.sym(U32, W32.nth0(nl1, s), W32.nth0(nl2, s), e1), r1)  L.subst(Bool, z => {Bool.and(U32.is_eq(W32.nth0(pl1, s), p), Bool.and(U32.is_eq(W32.nth0(nl1, s), LK.fst_or(t, q)), z)) == ST.seg(pl2, nl2, Con{s, t}, p, q) : Bool}, ST.seg(pl2, nl2, t, LK.lnk(s), q), ST.seg(pl1, nl1, t, LK.lnk(s), q), Equal.sym(Bool, ST.seg(pl1, nl1, t, LK.lnk(s), q), ST.seg(pl2, nl2, t, LK.lnk(s), q), ec), r2)# a write to the prev list off the segment leaves itdef seg_fp(+pl: List<&2, U32>, +nl: List<&2, U32>, +y: Nat, +v: U32, +xs: List<&2, Nat>, +p: U32, +q: U32, +hy: {NL.memn(y, xs) == False{} : Bool}) -> {ST.seg(SC.update(U32, pl, y, v), nl, xs, p, q) == ST.seg(pl, nl, xs, p, q) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+s, +t}:      seg_c(SC.update(U32, pl, y, v), nl, pl, nl, s, t, p, q, W32.nth0_upd_other(pl, y, s, v, NL.ne_sym(s, y, NL.or_ff_l(Nat.is_eq(s, y), NL.memn(y, t), hy))), {==}, seg_fp(pl, nl, y, v, t, LK.lnk(s), q, NL.or_ff_r(Nat.is_eq(s, y), NL.memn(y, t), hy)))# a write to the next list off the segment leaves itdef seg_fn(+pl: List<&2, U32>, +nl: List<&2, U32>, +y: Nat, +v: U32, +xs: List<&2, Nat>, +p: U32, +q: U32, +hy: {NL.memn(y, xs) == False{} : Bool}) -> {ST.seg(pl, SC.update(U32, nl, y, v), xs, p, q) == ST.seg(pl, nl, xs, p, q) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+s, +t}:      seg_c(pl, SC.update(U32, nl, y, v), pl, nl, s, t, p, q, {==}, W32.nth0_upd_other(nl, y, s, v, NL.ne_sym(s, y, NL.or_ff_l(Nat.is_eq(s, y), NL.memn(y, t), hy))), seg_fn(pl, nl, y, v, t, LK.lnk(s), q, NL.or_ff_r(Nat.is_eq(s, y), NL.memn(y, t), hy)))# a write to the next list off the free stack leaves itdef fll_fn(+nl: List<&2, U32>, +y: Nat, +v: U32, +fl: List<&2, Nat>, +hy: {NL.memn(y, fl) == False{} : Bool}) -> {ST.fll(SC.update(U32, nl, y, v), fl) == ST.fll(nl, fl) : Bool}:  match fl:    case Nil{}:      {==}    case Con{+s, +t}:      +e1 = W32.nth0_upd_other(nl, y, s, v, NL.ne_sym(s, y, NL.or_ff_l(Nat.is_eq(s, y), NL.memn(y, t), hy)))      +ih = fll_fn(nl, y, v, t, NL.or_ff_r(Nat.is_eq(s, y), NL.memn(y, t), hy))      +r1 = L.subst(U32, z => {Bool.and(U32.is_eq(z, LK.fst_or(t, 0)), ST.fll(nl, t)) == ST.fll(nl, Con{s, t}) : Bool}, W32.nth0(nl, s), W32.nth0(SC.update(U32, nl, y, v), s), Equal.sym(U32, W32.nth0(SC.update(U32, nl, y, v), s), W32.nth0(nl, s), e1), {==})      L.subst(Bool, z => {Bool.and(U32.is_eq(W32.nth0(SC.update(U32, nl, y, v), s), LK.fst_or(t, 0)), z) == ST.fll(nl, Con{s, t}) : Bool}, ST.fll(nl, t), ST.fll(SC.update(U32, nl, y, v), t), Equal.sym(Bool, ST.fll(SC.update(U32, nl, y, v), t), ST.fll(nl, t), ih), r1)# a segment splits at an appenddef seg_app(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +p: U32, +q: U32) -> {ST.seg(pl, nl, SC.append(Nat, a, b), p, q) == Bool.and(ST.seg(pl, nl, a, p, LK.fst_or(b, q)), ST.seg(pl, nl, b, LK.last_or(a, p), q)) : Bool}:  match a:    case Nil{}:      {==}    case Con{+h, +t}:      +E0 = U32.is_eq(W32.nth0(pl, h), p)      +F = LK.fst_or(b, q)      +Y = ST.seg(pl, nl, t, LK.lnk(h), F)      +Z = ST.seg(pl, nl, b, LK.last_or(t, LK.lnk(h)), q)      +e1 = Equal.cong(U32, Bool, z => Bool.and(E0, Bool.and(U32.is_eq(W32.nth0(nl, h), z), ST.seg(pl, nl, SC.append(Nat, t, b), LK.lnk(h), q))), LK.fst_or(SC.append(Nat, t, b), q), LK.fst_or(t, F), LK.fst_app(t, b, q))      +e2 = Equal.cong(Bool, Bool, z => Bool.and(E0, Bool.and(U32.is_eq(W32.nth0(nl, h), LK.fst_or(t, F)), z)), ST.seg(pl, nl, SC.append(Nat, t, b), LK.lnk(h), q), Bool.and(Y, Z), seg_app(pl, nl, t, b, LK.lnk(h), q))      Equal.trans(Bool, ST.seg(pl, nl, SC.append(Nat, Con{h, t}, b), p, q), Bool.and(E0, Bool.and(U32.is_eq(W32.nth0(nl, h), LK.fst_or(t, F)), ST.seg(pl, nl, SC.append(Nat, t, b), LK.lnk(h), q))), Bool.and(Bool.and(E0, Bool.and(U32.is_eq(W32.nth0(nl, h), LK.fst_or(t, F)), Y)), Z), e1, Equal.trans(Bool, Bool.and(E0, Bool.and(U32.is_eq(W32.nth0(nl, h), LK.fst_or(t, F)), ST.seg(pl, nl, SC.append(Nat, t, b), LK.lnk(h), q))), Bool.and(E0, Bool.and(U32.is_eq(W32.nth0(nl, h), LK.fst_or(t, F)), Bool.and(Y, Z))), Bool.and(Bool.and(E0, Bool.and(U32.is_eq(W32.nth0(nl, h), LK.fst_or(t, F)), Y)), Z), e2, NL.and3(E0, U32.is_eq(W32.nth0(nl, h), LK.fst_or(t, F)), Y, Z)))# re-target the last id's nextdef segq(+pl: List<&2, U32>, +nl: List<&2, U32>, +t: List<&2, Nat>, +a: Nat, +p: U32, +x: U32, +y: U32, +hs: {ST.seg(pl, nl, Con{a, t}, p, x) == True{} : Bool}, +hn: {NL.nodupn(Con{a, t}) == True{} : Bool}, +hl: {Nat.is_lt(NL.lastn(t, a), SC.length(U32, nl)) == True{} : Bool}) -> {ST.seg(pl, SC.update(U32, nl, NL.lastn(t, a), y), Con{a, t}, p, y) == True{} : Bool}:  match t:    case Nil{}:      +h0 = L.and_left(U32.is_eq(W32.nth0(pl, a), p), Bool.and(U32.is_eq(W32.nth0(nl, a), x), True{}), hs)      +h1b = L.subst(U32, z => {U32.is_eq(z, y) == True{} : Bool}, y, W32.nth0(SC.update(U32, nl, a, y), a), Equal.sym(U32, W32.nth0(SC.update(U32, nl, a, y), a), y, W32.nth0_upd_same(nl, a, y, hl)), LK.u_refl(y))      L.and_intro(U32.is_eq(W32.nth0(pl, a), p), Bool.and(U32.is_eq(W32.nth0(SC.update(U32, nl, a, y), a), y), True{}), h0, L.and_intro(U32.is_eq(W32.nth0(SC.update(U32, nl, a, y), a), y), True{}, h1b, {==}))    case Con{+b, +t2}:      +z = NL.lastn(t2, b)      +hna = L.and_left(Bool.not(NL.memn(a, Con{b, t2})), NL.nodupn(Con{b, t2}), hn)      +hza = NL.ne_mem(a, z, Con{b, t2}, hna, NL.lastn_mem(t2, b))      +e1 = W32.nth0_upd_other(nl, z, a, y, hza)      +h0 = L.and_left(U32.is_eq(W32.nth0(pl, a), p), Bool.and(U32.is_eq(W32.nth0(nl, a), LK.lnk(b)), ST.seg(pl, nl, Con{b, t2}, LK.lnk(a), x)), hs)      +hr = L.and_right(U32.is_eq(W32.nth0(pl, a), p), Bool.and(U32.is_eq(W32.nth0(nl, a), LK.lnk(b)), ST.seg(pl, nl, Con{b, t2}, LK.lnk(a), x)), hs)      +h1 = L.and_left(U32.is_eq(W32.nth0(nl, a), LK.lnk(b)), ST.seg(pl, nl, Con{b, t2}, LK.lnk(a), x), hr)      +hst = L.and_right(U32.is_eq(W32.nth0(nl, a), LK.lnk(b)), ST.seg(pl, nl, Con{b, t2}, LK.lnk(a), x), hr)      +h1b = L.subst(U32, w => {U32.is_eq(w, LK.lnk(b)) == True{} : Bool}, W32.nth0(nl, a), W32.nth0(SC.update(U32, nl, z, y), a), Equal.sym(U32, W32.nth0(SC.update(U32, nl, z, y), a), W32.nth0(nl, a), e1), h1)      L.and_intro(U32.is_eq(W32.nth0(pl, a), p), Bool.and(U32.is_eq(W32.nth0(SC.update(U32, nl, z, y), a), LK.lnk(b)), ST.seg(pl, SC.update(U32, nl, z, y), Con{b, t2}, LK.lnk(a), y)), h0, L.and_intro(U32.is_eq(W32.nth0(SC.update(U32, nl, z, y), a), LK.lnk(b)), ST.seg(pl, SC.update(U32, nl, z, y), Con{b, t2}, LK.lnk(a), y), h1b, segq(pl, nl, t2, b, LK.lnk(a), x, y, hst, L.and_right(Bool.not(NL.memn(a, Con{b, t2})), NL.nodupn(Con{b, t2}), hn), hl)))# re-target the first id's prevdef segp(+pl: List<&2, U32>, +nl: List<&2, U32>, +b: Nat, +t: List<&2, Nat>, +x: U32, +q: U32, +y: U32, +hs: {ST.seg(pl, nl, Con{b, t}, x, q) == True{} : Bool}, +hn: {NL.nodupn(Con{b, t}) == True{} : Bool}, +hl: {Nat.is_lt(b, SC.length(U32, pl)) == True{} : Bool}) -> {ST.seg(SC.update(U32, pl, b, y), nl, Con{b, t}, y, q) == True{} : Bool}:  +p2 = SC.update(U32, pl, b, y)  +hr = L.and_right(U32.is_eq(W32.nth0(pl, b), x), Bool.and(U32.is_eq(W32.nth0(nl, b), LK.fst_or(t, q)), ST.seg(pl, nl, t, LK.lnk(b), q)), hs)  +h1 = L.and_left(U32.is_eq(W32.nth0(nl, b), LK.fst_or(t, q)), ST.seg(pl, nl, t, LK.lnk(b), q), hr)  +hst = L.and_right(U32.is_eq(W32.nth0(nl, b), LK.fst_or(t, q)), ST.seg(pl, nl, t, LK.lnk(b), q), hr)  +hbt = NL.not_t_f(NL.memn(b, t), L.and_left(Bool.not(NL.memn(b, t)), NL.nodupn(t), hn))  +h0b = L.subst(U32, w => {U32.is_eq(w, y) == True{} : Bool}, y, W32.nth0(p2, b), Equal.sym(U32, W32.nth0(p2, b), y, W32.nth0_upd_same(pl, b, y, hl)), LK.u_refl(y))  +hstb = L.subst(Bool, w => {w == True{} : Bool}, ST.seg(pl, nl, t, LK.lnk(b), q), ST.seg(p2, nl, t, LK.lnk(b), q), Equal.sym(Bool, ST.seg(p2, nl, t, LK.lnk(b), q), ST.seg(pl, nl, t, LK.lnk(b), q), seg_fp(pl, nl, b, y, t, LK.lnk(b), q, hbt)), hst)  L.and_intro(U32.is_eq(W32.nth0(p2, b), y), Bool.and(U32.is_eq(W32.nth0(nl, b), LK.fst_or(t, q)), ST.seg(p2, nl, t, LK.lnk(b), q)), h0b, L.and_intro(U32.is_eq(W32.nth0(nl, b), LK.fst_or(t, q)), ST.seg(p2, nl, t, LK.lnk(b), q), h1, hstb))