proofs/containers/intrusive_doubly_linked_list/links.bend source

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

import Baseimport ../../../spec/containers/intrusive_doubly_linked_list/model.bend as Gimport ./adapter.bend as Aimport ../../../spec/containers/intrusive_doubly_linked_list/programs.bend as Specimport ../../lib/array.bend as ARimport ../../lib/logic.bend as LGimport ../../lib/list.bend as LLimport ../../lib/u32.bend as Uimport ../../lib/u32alg.bend as UAimport ../../../spec/lib/common.bend as SCimport ../../../src/containers/intrusive_links.bend as K# The ready-made link table src/containers/intrusive_links.bend meets the# adapter laws for EVERY size: 2^dn link slots per direction and 2^dr roots,# dn, dr < 32. This discharges, for arbitrary sizes, what array_adapter.bend# does for its four-node example: the exported remove and prepend are the# model graph's remove and prepend (adapter.remove_refines/prepend_refines).## A model graph is realized by writing its bindings, oldest first, into# zeroed arrays (0 encodes "no entity"). The premises are exactly what an# array access needs: the ids written are in range, and a link that is READ# is not the reserved id 0 (it decodes back to itself).def ueq(a: U32, b: U32) -> Bool:  U32.is_eq(a, b)def tn(+d: Nat, bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>) -> AR.Tree<U32>:  match bs:    case Nil{}:      AR.trep(U32, d, 0)    case Con{G.Binding{k, v}, rest}:      AR.upd(U32, d, tn(d, rest), U32.to_nat(k), K.encode(v))# The graph's frame carries the table's sizes; no operation changes it.type Depth is Data:  Depth{nodes: Nat, roots: Nat}def real_at(ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, f: Depth) -> K.Links:  match f:    case Depth{+dn, +dr}:      K.Links{AR.thaw(U32, tn(dn, ns)), AR.thaw(U32, tn(dn, ps)), AR.thaw(U32, tn(dr, rs))}def real(g: G.Graph<U32,U32,Depth>) -> K.Links:  G.Graph{ns, ps, rs, f} = g  real_at(ns, ps, rs, f)def dn_of(g: G.Graph<U32,U32,Depth>) -> Nat:  match g:    case G.Graph{ns, ps, rs, Depth{dn, dr}}:      dndef dr_of(g: G.Graph<U32,U32,Depth>) -> Nat:  match g:    case G.Graph{ns, ps, rs, Depth{dn, dr}}:      drdef bound(+d: Nat, +x: U32) -> Data:  {Nat.is_lt(U32.to_nat(x), SC.pow2(d)) == True{} : Bool}def keys_ok(+d: Nat, bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>) -> Data:  match bs:    case Nil{}:      Unit    case Con{G.Binding{k, v}, rest}:      G.both(bound(d, k), keys_ok(d, rest))def gok(g: G.Graph<U32,U32,Depth>) -> Data:  match g:    case G.Graph{ns, ps, rs, Depth{+dn, +dr}}:      G.both(keys_ok(dn, ns), G.both(keys_ok(dn, ps), keys_ok(dr, rs)))# A link that is read: absent, or a nonzero id.def nz(m: Maybe<&2,U32>) -> Data:  match m:    case None{}:      Unit    case Some{x}:      {U32.is_eq(x, 0) == False{} : Bool}# A link that is written through: absent, or an id in range.def inb(+d: Nat, m: Maybe<&2,U32>) -> Data:  match m:    case None{}:      Unit    case Some{x}:      bound(d, x)# ---- the realized trees ----def tn_perfect(+d: Nat, +bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>) -> {AR.perfect(U32, d, tn(d, bs)) == True{} : Bool}:  match bs:    case Nil{}:      AR.trep_perfect(U32, d, 0)    case Con{G.Binding{+k, +v}, +rest}:      AR.upd_perfect(U32, d, tn(d, rest), U32.to_nat(k), K.encode(v), tn_perfect(d, rest))def nth_rep(+m: Nat, +i: Nat, +h: {Nat.is_lt(i, m) == True{} : Bool}) -> {SC.nth(U32, SC.replicate(U32, m, 0), i) == Some{0} : Maybe<&2,U32>}:  match m i:    case 0n 0n:      Empty.absurd({SC.nth(U32, SC.replicate(U32, 0n, 0), 0n) == Some{0} : Maybe<&2,U32>}, LG.false_true(h))    case 0n 1n+j:      Empty.absurd({SC.nth(U32, SC.replicate(U32, 0n, 0), 1n+j) == Some{0} : Maybe<&2,U32>}, LG.false_true(h))    case 1n+p 0n:      {==}    case 1n+ +p 1n+ +j:      nth_rep(p, j, h)def eq_nat(+a: U32, +b: U32) -> {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}:  %Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b)) : {Cmp.is_eq(_) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}  {==}def ne_nat(+a: U32, +b: U32, +e: {U32.is_eq(a, b) == False{} : Bool}) -> {Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) == False{} : Bool}:  %eq_nat(a, b) : {_ == False{} : Bool}  edef lt_len(+d: Nat, +n: U32, +xs: List<&2,U32>, +hl: {SC.length(U32, xs) == SC.pow2(d) : Nat}, +hn: bound(d, n)) -> {Nat.is_lt(U32.to_nat(n), SC.length(U32, xs)) == True{} : Bool}:  %Equal.sym(Nat, SC.length(U32, xs), SC.pow2(d), hl) : {Nat.is_lt(U32.to_nat(n), _) == True{} : Bool}  hn# After a binding (k, v): the slot of n is v when k is n, else unchanged.def nth_bind(+d: Nat, +k: U32, +v: Maybe<&2,U32>, +rest: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +n: U32, +xs: List<&2,U32>, +hl: {SC.length(U32, xs) == SC.pow2(d) : Nat}, +hn: bound(d, n), +ih: {SC.nth(U32, xs, U32.to_nat(n)) == Some{K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, rest, None{}))} : Maybe<&2,U32>}, +b: Bool, +eb: {U32.is_eq(k, n) == b : Bool}) -> {SC.nth(U32, SC.update(U32, xs, U32.to_nat(k), K.encode(v)), U32.to_nat(n)) == Some{K.encode(G.choose(~Maybe<&2,U32>, b, v, G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, rest, None{})))} : Maybe<&2,U32>}:  match b:    case True{}:      %Equal.sym(U32, k, n, UA.eq_of(k, n, eb)) : {SC.nth(U32, SC.update(U32, xs, U32.to_nat(_), K.encode(v)), U32.to_nat(n)) == Some{K.encode(v)} : Maybe<&2,U32>}      LL.nth_update_same(U32, xs, U32.to_nat(n), K.encode(v), lt_len(d, n, xs, hl, hn))    case False{}:      %Equal.sym(Maybe<&2,U32>, SC.nth(U32, SC.update(U32, xs, U32.to_nat(k), K.encode(v)), U32.to_nat(n)), SC.nth(U32, xs, U32.to_nat(n)), LL.nth_update_other(U32, xs, U32.to_nat(k), U32.to_nat(n), K.encode(v), ne_nat(k, n, eb))) : {_ == Some{K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, rest, None{}))} : Maybe<&2,U32>}      ihdef tn_len(+d: Nat, +bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>) -> {SC.length(U32, AR.slots(U32, tn(d, bs))) == SC.pow2(d) : Nat}:  AR.slots_length(U32, d, tn(d, bs), tn_perfect(d, bs))# Reading slot n of a realized tree gives the model's value for n.def tn_nth(+d: Nat, +bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +n: U32, +hn: bound(d, n), +hk: keys_ok(d, bs)) -> {SC.nth(U32, AR.slots(U32, tn(d, bs)), U32.to_nat(n)) == Some{K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, bs, None{}))} : Maybe<&2,U32>}:  match bs hk:    case Nil{} _:      %Equal.sym(List<&2,U32>, AR.slots(U32, AR.trep(U32, d, 0)), SC.replicate(U32, SC.pow2(d), 0), AR.trep_slots(U32, d, 0)) : {SC.nth(U32, _, U32.to_nat(n)) == Some{0} : Maybe<&2,U32>}      nth_rep(SC.pow2(d), U32.to_nat(n), hn)    case Con{G.Binding{+k, +v}, +rest} Tuple{+hb, +hr}:      %Equal.sym(List<&2,U32>, AR.slots(U32, AR.upd(U32, d, tn(d, rest), U32.to_nat(k), K.encode(v))), SC.update(U32, AR.slots(U32, tn(d, rest)), U32.to_nat(k), K.encode(v)), AR.upd_slots(U32, d, tn(d, rest), U32.to_nat(k), K.encode(v), hb, tn_perfect(d, rest))) : {SC.nth(U32, _, U32.to_nat(n)) == Some{K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, Con{G.Binding{k, v}, rest}, None{}))} : Maybe<&2,U32>}      nth_bind(d, k, v, rest, n, AR.slots(U32, tn(d, rest)), tn_len(d, rest), hn, tn_nth(d, rest, n, hn, hr), U32.is_eq(k, n), {==})def dec_enc(+m: Maybe<&2,U32>, +hz: nz(m)) -> {K.decode(K.encode(m)) == m : Maybe<&2,U32>}:  match m:    case None{}:      {==}    case Some{+x}:      %Equal.sym(Bool, U32.is_eq(x, 0), False{}, hz) : {K.decode_pick(x, _) == Some{x} : Maybe<&2,U32>}      {==}# ---- reads (on a graph given by its components) ----def next_read(+n: U32, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hn: bound(dn, n), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs), +hz: nz(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{}))) -> {K.next(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), n) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{})) : K.Links & Maybe<&2,U32>}:  %Equal.sym(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tn(dn, ns)), n), (AR.thaw(U32, tn(dn, ns)), K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{}))), AR.get(U32, dn, tn(dn, ns), n, K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{})), hd, hn, tn_nth(dn, ns, n, hn, kn), tn_perfect(dn, ns))) : {K.next_got(AR.thaw(U32, tn(dn, ps)), AR.thaw(U32, tn(dr, rs)), _) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{})) : K.Links & Maybe<&2,U32>}  %Equal.sym(Maybe<&2,U32>, K.decode(K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{}))), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{}), dec_enc(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{}), hz)) : {(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), _) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ns, None{})) : K.Links & Maybe<&2,U32>}  {==}def prev_read(+n: U32, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hn: bound(dn, n), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs), +hz: nz(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{}))) -> {K.prev(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), n) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{})) : K.Links & Maybe<&2,U32>}:  %Equal.sym(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tn(dn, ps)), n), (AR.thaw(U32, tn(dn, ps)), K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{}))), AR.get(U32, dn, tn(dn, ps), n, K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{})), hd, hn, tn_nth(dn, ps, n, hn, kp), tn_perfect(dn, ps))) : {K.prev_got(AR.thaw(U32, tn(dn, ns)), AR.thaw(U32, tn(dr, rs)), _) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{})) : K.Links & Maybe<&2,U32>}  %Equal.sym(Maybe<&2,U32>, K.decode(K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{}))), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{}), dec_enc(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{}), hz)) : {(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), _) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, n, ps, None{})) : K.Links & Maybe<&2,U32>}  {==}def head_read(+r: U32, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hr: bound(dr, r), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs), +hz: nz(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{}))) -> {K.get_head(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), r) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{})) : K.Links & Maybe<&2,U32>}:  %Equal.sym(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tn(dr, rs)), r), (AR.thaw(U32, tn(dr, rs)), K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{}))), AR.get(U32, dr, tn(dr, rs), r, K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{})), hdr, hr, tn_nth(dr, rs, r, hr, kr), tn_perfect(dr, rs))) : {K.head_got(AR.thaw(U32, tn(dn, ns)), AR.thaw(U32, tn(dn, ps)), _) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{})) : K.Links & Maybe<&2,U32>}  %Equal.sym(Maybe<&2,U32>, K.decode(K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{}))), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{}), dec_enc(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{}), hz)) : {(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), _) == (real(G.Graph{ns, ps, rs, Depth{dn, dr}}), G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, r, rs, None{})) : K.Links & Maybe<&2,U32>}  {==}# ---- writes ----def set_tree(+d: Nat, +bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +x: U32, +v: Maybe<&2,U32>, +hd0: {Nat.is_lt(d, 32n) == True{} : Bool}, +hx: bound(d, x), +kb: keys_ok(d, bs)) -> {Array.set(U32, AR.thaw(U32, tn(d, bs)), x, K.encode(v)) == AR.thaw(U32, tn(d, Con{G.Binding{x, v}, bs})) : Array<U32>}:  AR.set(U32, d, tn(d, bs), x, K.encode(v), K.encode(G.lookup(~U32, ~Maybe<&2,U32>, ~ueq, x, bs, None{})), hd0, hx, tn_nth(d, bs, x, hx, kb), tn_perfect(d, bs))def sn_law(+n: U32, +v: Maybe<&2,U32>, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hn: bound(dn, n), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs)) -> {K.set_next(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), n, v) == real(G.sn(~U32, ~U32, ~Depth, G.Graph{ns, ps, rs, Depth{dn, dr}}, n, v)) : K.Links}:  %Equal.sym(Array<U32>, Array.set(U32, AR.thaw(U32, tn(dn, ns)), n, K.encode(v)), AR.thaw(U32, tn(dn, Con{G.Binding{n, v}, ns})), set_tree(dn, ns, n, v, hd, hn, kn)) : {K.Links{_, AR.thaw(U32, tn(dn, ps)), AR.thaw(U32, tn(dr, rs))} == real(G.Graph{Con{G.Binding{n, v}, ns}, ps, rs, Depth{dn, dr}}) : K.Links}  {==}def sp_law(+n: U32, +v: Maybe<&2,U32>, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hn: bound(dn, n), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs)) -> {K.set_prev(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), n, v) == real(G.sp(~U32, ~U32, ~Depth, G.Graph{ns, ps, rs, Depth{dn, dr}}, n, v)) : K.Links}:  %Equal.sym(Array<U32>, Array.set(U32, AR.thaw(U32, tn(dn, ps)), n, K.encode(v)), AR.thaw(U32, tn(dn, Con{G.Binding{n, v}, ps})), set_tree(dn, ps, n, v, hd, hn, kp)) : {K.Links{AR.thaw(U32, tn(dn, ns)), _, AR.thaw(U32, tn(dr, rs))} == real(G.Graph{ns, Con{G.Binding{n, v}, ps}, rs, Depth{dn, dr}}) : K.Links}  {==}def sh_law(+r: U32, +v: Maybe<&2,U32>, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hr: bound(dr, r), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs)) -> {K.set_head(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), r, v) == real(G.sh(~U32, ~U32, ~Depth, G.Graph{ns, ps, rs, Depth{dn, dr}}, r, v)) : K.Links}:  %Equal.sym(Array<U32>, Array.set(U32, AR.thaw(U32, tn(dr, rs)), r, K.encode(v)), AR.thaw(U32, tn(dr, Con{G.Binding{r, v}, rs})), set_tree(dr, rs, r, v, hdr, hr, kr)) : {K.Links{AR.thaw(U32, tn(dn, ns)), AR.thaw(U32, tn(dn, ps)), _} == real(G.Graph{ns, ps, Con{G.Binding{r, v}, rs}, Depth{dn, dr}}) : K.Links}  {==}# ---- the adapter laws, for every edit program with in-range targets ----def tgt(+dn: Nat, +dr: Nat, e: Spec.Edit<U32,U32>) -> Data:  match e:    case Spec.Next{n, m}:      bound(dn, n)    case Spec.Prev{n, m}:      bound(dn, n)    case Spec.Head{i, m}:      bound(dr, i)    case Spec.Nonempty{i, n}:      bound(dr, i)def tgts(+dn: Nat, +dr: Nat, es: List<&2,Spec.Edit<U32,U32>>) -> Data:  match es:    case Nil{}:      Unit    case Con{e, rest}:      G.both(tgt(dn, dr, e), tgts(dn, dr, rest))# Every edit program whose targets are in range is carried out exactly.def laws_of(+es: List<&2,Spec.Edit<U32,U32>>, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs), +ht: tgts(dn, dr, es)) -> A.laws(~K.Links, ~U32, ~U32, ~Depth, ~U32, ~real, ~(i => i), ~K.set_next, ~K.set_prev, ~K.set_head, ~K.set_head_nonempty, es, G.Graph{ns, ps, rs, Depth{dn, dr}}):  match es ht:    case Nil{} _:      Unit{}    case Con{Spec.Next{+n, +v}, +rest} Tuple{+he, +hr}:      (sn_law(n, v, ns, ps, rs, dn, dr, hd, hdr, he, kn, kp, kr), laws_of(rest, Con{G.Binding{n, v}, ns}, ps, rs, dn, dr, hd, hdr, (he, kn), kp, kr, hr))    case Con{Spec.Prev{+n, +v}, +rest} Tuple{+he, +hr}:      (sp_law(n, v, ns, ps, rs, dn, dr, hd, hdr, he, kn, kp, kr), laws_of(rest, ns, Con{G.Binding{n, v}, ps}, rs, dn, dr, hd, hdr, kn, (he, kp), kr, hr))    case Con{Spec.Head{+i, +v}, +rest} Tuple{+he, +hr}:      (sh_law(i, v, ns, ps, rs, dn, dr, hd, hdr, he, kn, kp, kr), laws_of(rest, ns, ps, Con{G.Binding{i, v}, rs}, dn, dr, hd, hdr, kn, kp, (he, kr), hr))    case Con{Spec.Nonempty{+i, +n}, +rest} Tuple{+he, +hr}:      (sh_law(i, Some{n}, ns, ps, rs, dn, dr, hd, hdr, he, kn, kp, kr), laws_of(rest, ns, ps, Con{G.Binding{i, Some{n}}, rs}, dn, dr, hd, hdr, kn, kp, (he, kr), hr))def rm_tgts(+dn: Nat, +dr: Nat, +r: U32, +n: U32, +p: Maybe<&2,U32>, +q: Maybe<&2,U32>, +hn: bound(dn, n), +hr: bound(dr, r), +bp: inb(dn, p), +bq: inb(dn, q)) -> tgts(dn, dr, Spec.remove(U32, U32, r, n, p, q)):  match p q:    case None{} None{}:      (hr, (hn, Unit{}))    case None{} Some{+y}:      (bq, (hr, (hn, Unit{})))    case Some{+x} None{}:      (bp, (hn, (hn, Unit{})))    case Some{+x} Some{+y}:      (bq, (bp, (hn, (hn, Unit{}))))def pp_tgts(+dn: Nat, +dr: Nat, +r: U32, +n: U32, +h: Maybe<&2,U32>, +hn: bound(dn, n), +hr: bound(dr, r), +bh: inb(dn, h)) -> tgts(dn, dr, Spec.prepend(U32, U32, r, n, h)):  match h:    case None{}:      (hn, (hr, Unit{}))    case Some{+x}:      (hn, (bh, (hr, Unit{})))# ---- the exported operations are the model's, for every size ----def remove_c(+r: U32, +n: U32, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hn: bound(dn, n), +hr: bound(dr, r), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs), +zp: nz(G.prev(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n)), +zq: nz(G.next(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n)), +bp: inb(dn, G.prev(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n)), +bq: inb(dn, G.next(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n))) -> {K.remove(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), r, n) == real(G.remove(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, r, n)) : K.Links}:  A.remove_refines(~K.Links, ~U32, ~U32, ~Depth, ~U32, ~real, ~(i => i), ~K.set_next, ~K.set_prev, ~K.set_head, ~K.set_head_nonempty, ~ueq, ~K.next, ~K.prev, G.Graph{ns, ps, rs, Depth{dn, dr}}, r, n, next_read(n, ns, ps, rs, dn, dr, hd, hdr, hn, kn, kp, kr, zq), prev_read(n, ns, ps, rs, dn, dr, hd, hdr, hn, kn, kp, kr, zp), laws_of(Spec.remove(U32, U32, r, n, G.prev(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n), G.next(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n)), ns, ps, rs, dn, dr, hd, hdr, kn, kp, kr, rm_tgts(dn, dr, r, n, G.prev(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n), G.next(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, n), hn, hr, bp, bq)))def prepend_c(+r: U32, +n: U32, +ns: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +ps: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +rs: List<&2,G.Binding<U32,Maybe<&2,U32>>>, +dn: Nat, +dr: Nat, +hd: {Nat.is_lt(dn, 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr, 32n) == True{} : Bool}, +hn: bound(dn, n), +hr: bound(dr, r), +kn: keys_ok(dn, ns), +kp: keys_ok(dn, ps), +kr: keys_ok(dr, rs), +zh: nz(G.head(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, r)), +bh: inb(dn, G.head(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, r))) -> {K.prepend(real(G.Graph{ns, ps, rs, Depth{dn, dr}}), r, n) == real(G.prepend(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, r, n)) : K.Links}:  A.prepend_refines(~K.Links, ~U32, ~U32, ~Depth, ~U32, ~real, ~(i => i), ~K.set_next, ~K.set_prev, ~K.set_head, ~K.set_head_nonempty, ~U32, ~ueq, ~K.get_head, G.Graph{ns, ps, rs, Depth{dn, dr}}, r, r, n, head_read(r, ns, ps, rs, dn, dr, hd, hdr, hr, kn, kp, kr, zh), laws_of(Spec.prepend(U32, U32, r, n, G.head(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, r)), ns, ps, rs, dn, dr, hd, hdr, kn, kp, kr, pp_tgts(dn, dr, r, n, G.head(~U32, ~U32, ~Depth, ~ueq, G.Graph{ns, ps, rs, Depth{dn, dr}}, r), hn, hr, bh)))# ---- the same, stated on any model graph ----# The exported remove is the model's remove, for every table size.def remove_refines(+r: U32, +n: U32, +g: G.Graph<U32,U32,Depth>, +hd: {Nat.is_lt(dn_of(g), 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr_of(g), 32n) == True{} : Bool}, +hk: gok(g), +hn: bound(dn_of(g), n), +hr: bound(dr_of(g), r), +zp: nz(G.prev(~U32, ~U32, ~Depth, ~ueq, g, n)), +zq: nz(G.next(~U32, ~U32, ~Depth, ~ueq, g, n)), +bp: inb(dn_of(g), G.prev(~U32, ~U32, ~Depth, ~ueq, g, n)), +bq: inb(dn_of(g), G.next(~U32, ~U32, ~Depth, ~ueq, g, n))) -> {K.remove(real(g), r, n) == real(G.remove(~U32, ~U32, ~Depth, ~ueq, g, r, n)) : K.Links}:  match g hk:    case G.Graph{+ns, +ps, +rs, Depth{+dn, +dr}} Tuple{+kn, Tuple{+kp, +kr}}:      remove_c(r, n, ns, ps, rs, dn, dr, hd, hdr, hn, hr, kn, kp, kr, zp, zq, bp, bq)# The exported prepend is the model's prepend, for every table size.def prepend_refines(+r: U32, +n: U32, +g: G.Graph<U32,U32,Depth>, +hd: {Nat.is_lt(dn_of(g), 32n) == True{} : Bool}, +hdr: {Nat.is_lt(dr_of(g), 32n) == True{} : Bool}, +hk: gok(g), +hn: bound(dn_of(g), n), +hr: bound(dr_of(g), r), +zh: nz(G.head(~U32, ~U32, ~Depth, ~ueq, g, r)), +bh: inb(dn_of(g), G.head(~U32, ~U32, ~Depth, ~ueq, g, r))) -> {K.prepend(real(g), r, n) == real(G.prepend(~U32, ~U32, ~Depth, ~ueq, g, r, n)) : K.Links}:  match g hk:    case G.Graph{+ns, +ps, +rs, Depth{+dn, +dr}} Tuple{+kn, Tuple{+kp, +kr}}:      prepend_c(r, n, ns, ps, rs, dn, dr, hd, hdr, hn, hr, kn, kp, kr, zh, bh)# A fresh table is the empty model graph of its size.def new_real(+dn: Nat, +dr: Nat) -> {K.new(dn, dr) == real(G.Graph{Nil{}, Nil{}, Nil{}, Depth{dn, dr}}) : K.Links}:  %Equal.sym(Array<U32>, Array.new(U32, dn, 0), AR.thaw(U32, AR.trep(U32, dn, 0)), AR.new(U32, dn, 0)) : {K.Links{_, Array.new(U32, dn, 0), Array.new(U32, dr, 0)} == real(G.Graph{Nil{}, Nil{}, Nil{}, Depth{dn, dr}}) : K.Links}  %Equal.sym(Array<U32>, Array.new(U32, dn, 0), AR.thaw(U32, AR.trep(U32, dn, 0)), AR.new(U32, dn, 0)) : {K.Links{AR.thaw(U32, AR.trep(U32, dn, 0)), _, Array.new(U32, dr, 0)} == real(G.Graph{Nil{}, Nil{}, Nil{}, Depth{dn, dr}}) : K.Links}  %Equal.sym(Array<U32>, Array.new(U32, dr, 0), AR.thaw(U32, AR.trep(U32, dr, 0)), AR.new(U32, dr, 0)) : {K.Links{AR.thaw(U32, AR.trep(U32, dn, 0)), AR.thaw(U32, AR.trep(U32, dn, 0)), _} == real(G.Graph{Nil{}, Nil{}, Nil{}, Depth{dn, dr}}) : K.Links}  {==}# The empty graph satisfies every premise about keys.def new_ok(+dn: Nat, +dr: Nat) -> gok(G.Graph{Nil{}, Nil{}, Nil{}, Depth{dn, dr}}):  (Unit{}, (Unit{}, Unit{}))