proofs/containers/intrusive_doubly_linked_list/links.bend
bend-collections-laws-containers@1.0.0.0 · 275 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
3import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/adapter.bend as A
4import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/programs.bend as Spec
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as LG
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as UA
10import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
11import bend-collections-laws-containers@1.0.0.0/src/containers/intrusive_links.bend as K
12
13# The ready-made link table src/containers/intrusive_links.bend meets the
14# adapter laws for EVERY size: 2^dn link slots per direction and 2^dr roots,
15# dn, dr < 32. This discharges, for arbitrary sizes, what array_adapter.bend
16# does for its four-node example: the exported remove and prepend are the
17# model graph's remove and prepend (adapter.remove_refines/prepend_refines).
18#
19# A model graph is realized by writing its bindings, oldest first, into
20# zeroed arrays (0 encodes "no entity"). The premises are exactly what an
21# array access needs: the ids written are in range, and a link that is READ
22# is not the reserved id 0 (it decodes back to itself).
23
24
25def ueq(a: U32, b: U32) -> Bool:
26 U32.is_eq(a, b)
27
28def tn(+d: Nat, bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>) -> AR.Tree<U32>:
29 match bs:
30 case Nil{}:
31 AR.trep(U32, d, 0)
32 case Con{G.Binding{k, v}, rest}:
33 AR.upd(U32, d, tn(d, rest), U32.to_nat(k), K.encode(v))
34
35# The graph's frame carries the table's sizes; no operation changes it.
36type Depth is Data:
37 Depth{nodes: Nat, roots: Nat}
38
39def 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:
40 match f:
41 case Depth{+dn, +dr}:
42 K.Links{AR.thaw(U32, tn(dn, ns)), AR.thaw(U32, tn(dn, ps)), AR.thaw(U32, tn(dr, rs))}
43
44def real(g: G.Graph<U32,U32,Depth>) -> K.Links:
45 G.Graph{ns, ps, rs, f} = g
46 real_at(ns, ps, rs, f)
47
48def dn_of(g: G.Graph<U32,U32,Depth>) -> Nat:
49 match g:
50 case G.Graph{ns, ps, rs, Depth{dn, dr}}:
51 dn
52
53def dr_of(g: G.Graph<U32,U32,Depth>) -> Nat:
54 match g:
55 case G.Graph{ns, ps, rs, Depth{dn, dr}}:
56 dr
57
58def bound(+d: Nat, +x: U32) -> Data:
59 {Nat.is_lt(U32.to_nat(x), SC.pow2(d)) == True{} : Bool}
60
61def keys_ok(+d: Nat, bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>) -> Data:
62 match bs:
63 case Nil{}:
64 Unit
65 case Con{G.Binding{k, v}, rest}:
66 G.both(bound(d, k), keys_ok(d, rest))
67
68def gok(g: G.Graph<U32,U32,Depth>) -> Data:
69 match g:
70 case G.Graph{ns, ps, rs, Depth{+dn, +dr}}:
71 G.both(keys_ok(dn, ns), G.both(keys_ok(dn, ps), keys_ok(dr, rs)))
72
73# A link that is read: absent, or a nonzero id.
74def nz(m: Maybe<&2,U32>) -> Data:
75 match m:
76 case None{}:
77 Unit
78 case Some{x}:
79 {U32.is_eq(x, 0) == False{} : Bool}
80
81# A link that is written through: absent, or an id in range.
82def inb(+d: Nat, m: Maybe<&2,U32>) -> Data:
83 match m:
84 case None{}:
85 Unit
86 case Some{x}:
87 bound(d, x)
88
89# ---- the realized trees ----
90
91def tn_perfect(+d: Nat, +bs: List<&2,G.Binding<U32,Maybe<&2,U32>>>) -> {AR.perfect(U32, d, tn(d, bs)) == True{} : Bool}:
92 match bs:
93 case Nil{}:
94 AR.trep_perfect(U32, d, 0)
95 case Con{G.Binding{+k, +v}, +rest}:
96 AR.upd_perfect(U32, d, tn(d, rest), U32.to_nat(k), K.encode(v), tn_perfect(d, rest))
97
98def 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>}:
99 match m i:
100 case 0n 0n:
101 Empty.absurd({SC.nth(U32, SC.replicate(U32, 0n, 0), 0n) == Some{0} : Maybe<&2,U32>}, LG.false_true(h))
102 case 0n 1n+j:
103 Empty.absurd({SC.nth(U32, SC.replicate(U32, 0n, 0), 1n+j) == Some{0} : Maybe<&2,U32>}, LG.false_true(h))
104 case 1n+p 0n:
105 {==}
106 case 1n+ +p 1n+ +j:
107 nth_rep(p, j, h)
108
109def eq_nat(+a: U32, +b: U32) -> {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}:
110 %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}
111 {==}
112
113def 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}:
114 %eq_nat(a, b) : {_ == False{} : Bool}
115 e
116
117
118def 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}:
119 %Equal.sym(Nat, SC.length(U32, xs), SC.pow2(d), hl) : {Nat.is_lt(U32.to_nat(n), _) == True{} : Bool}
120 hn
121
122# After a binding (k, v): the slot of n is v when k is n, else unchanged.
123def 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>}:
124 match b:
125 case True{}:
126 %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>}
127 LL.nth_update_same(U32, xs, U32.to_nat(n), K.encode(v), lt_len(d, n, xs, hl, hn))
128 case False{}:
129 %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>}
130 ih
131
132def 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}:
133 AR.slots_length(U32, d, tn(d, bs), tn_perfect(d, bs))
134
135# Reading slot n of a realized tree gives the model's value for n.
136def 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>}:
137 match bs hk:
138 case Nil{} _:
139 %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>}
140 nth_rep(SC.pow2(d), U32.to_nat(n), hn)
141 case Con{G.Binding{+k, +v}, +rest} Tuple{+hb, +hr}:
142 %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>}
143 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), {==})
144
145def dec_enc(+m: Maybe<&2,U32>, +hz: nz(m)) -> {K.decode(K.encode(m)) == m : Maybe<&2,U32>}:
146 match m:
147 case None{}:
148 {==}
149 case Some{+x}:
150 %Equal.sym(Bool, U32.is_eq(x, 0), False{}, hz) : {K.decode_pick(x, _) == Some{x} : Maybe<&2,U32>}
151 {==}
152
153# ---- reads (on a graph given by its components) ----
154
155
156def 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>}:
157 %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>}
158 %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>}
159 {==}
160
161def 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>}:
162 %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>}
163 %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>}
164 {==}
165
166
167def 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>}:
168 %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>}
169 %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>}
170 {==}
171
172# ---- writes ----
173
174def 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>}:
175 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))
176
177def 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}:
178 %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}
179 {==}
180
181def 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}:
182 %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}
183 {==}
184
185def 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}:
186 %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}
187 {==}
188
189# ---- the adapter laws, for every edit program with in-range targets ----
190
191
192def tgt(+dn: Nat, +dr: Nat, e: Spec.Edit<U32,U32>) -> Data:
193 match e:
194 case Spec.Next{n, m}:
195 bound(dn, n)
196 case Spec.Prev{n, m}:
197 bound(dn, n)
198 case Spec.Head{i, m}:
199 bound(dr, i)
200 case Spec.Nonempty{i, n}:
201 bound(dr, i)
202
203def tgts(+dn: Nat, +dr: Nat, es: List<&2,Spec.Edit<U32,U32>>) -> Data:
204 match es:
205 case Nil{}:
206 Unit
207 case Con{e, rest}:
208 G.both(tgt(dn, dr, e), tgts(dn, dr, rest))
209
210# Every edit program whose targets are in range is carried out exactly.
211def 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}}):
212 match es ht:
213 case Nil{} _:
214 Unit{}
215 case Con{Spec.Next{+n, +v}, +rest} Tuple{+he, +hr}:
216 (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))
217 case Con{Spec.Prev{+n, +v}, +rest} Tuple{+he, +hr}:
218 (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))
219 case Con{Spec.Head{+i, +v}, +rest} Tuple{+he, +hr}:
220 (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))
221 case Con{Spec.Nonempty{+i, +n}, +rest} Tuple{+he, +hr}:
222 (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))
223
224def 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)):
225 match p q:
226 case None{} None{}:
227 (hr, (hn, Unit{}))
228 case None{} Some{+y}:
229 (bq, (hr, (hn, Unit{})))
230 case Some{+x} None{}:
231 (bp, (hn, (hn, Unit{})))
232 case Some{+x} Some{+y}:
233 (bq, (bp, (hn, (hn, Unit{}))))
234
235def 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)):
236 match h:
237 case None{}:
238 (hn, (hr, Unit{}))
239 case Some{+x}:
240 (hn, (bh, (hr, Unit{})))
241
242# ---- the exported operations are the model's, for every size ----
243
244
245def 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}:
246 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)))
247
248def 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}:
249 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)))
250
251# ---- the same, stated on any model graph ----
252
253
254# The exported remove is the model's remove, for every table size.
255def 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}:
256 match g hk:
257 case G.Graph{+ns, +ps, +rs, Depth{+dn, +dr}} Tuple{+kn, Tuple{+kp, +kr}}:
258 remove_c(r, n, ns, ps, rs, dn, dr, hd, hdr, hn, hr, kn, kp, kr, zp, zq, bp, bq)
259
260# The exported prepend is the model's prepend, for every table size.
261def 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}:
262 match g hk:
263 case G.Graph{+ns, +ps, +rs, Depth{+dn, +dr}} Tuple{+kn, Tuple{+kp, +kr}}:
264 prepend_c(r, n, ns, ps, rs, dn, dr, hd, hdr, hn, hr, kn, kp, kr, zh, bh)
265
266# A fresh table is the empty model graph of its size.
267def new_real(+dn: Nat, +dr: Nat) -> {K.new(dn, dr) == real(G.Graph{Nil{}, Nil{}, Nil{}, Depth{dn, dr}}) : K.Links}:
268 %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}
269 %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}
270 %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}
271 {==}
272
273# The empty graph satisfies every premise about keys.
274def new_ok(+dn: Nat, +dr: Nat) -> gok(G.Graph{Nil{}, Nil{}, Nil{}, Depth{dn, dr}}):
275 (Unit{}, (Unit{}, Unit{}))