1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../src/containers/balanced_search_tree.bend as M
6	import ../../../src/containers/dynamic_array.bend as D
7	import ../../../src/containers/types/dynamic_array.bend as DE
8	import ./state.bend as ST
9	import ./da.bend as DA
10	import ./arr.bend as AB
11	import ./nsl.bend as NSL
12	
13	# The TreeMap's node and payload accesses over the shadow: a read returns
14	# the list's node, a write or exchange updates the list in range.
15	
16	
17	def or_else(-X: Data, m: Maybe<&2, X>, +dv: X) -> X:
18	  match m:
19	    case None{}:
20	      dv
21	    case Some{x}:
22	      x
23	
24	def nth_or_nth(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X) -> {ST.nth_or(X, xs, i, dv) == or_else(X, SC.nth(X, xs, i), dv) : X}:
25	  match xs i:
26	    case Nil{} _:
27	      {==}
28	    case Con{x, t} 0n:
29	      {==}
30	    case Con{x, +t} 1n+p:
31	      nth_or_nth(X, t, p, dv)
32	
33	def pl_cap(~K: Data, ~V: Data, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {Nat.is_le(SC.length(Maybe<&2, V>, pl), SC.pow2(d)) == True{} : Bool}:
34	  L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, pl), Equal.sym(Nat, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), N.eq_from_is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hp)), hc)
35	
36	def nth_hi(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X, +h: {Nat.is_lt(i, SC.length(X, xs)) == False{} : Bool}) -> {ST.nth_or(X, xs, i, dv) == dv : X}:
37	  match xs i:
38	    case Nil{} _:
39	      {==}
40	    case Con{x, t} 0n:
41	      Empty.absurd({x == dv : X}, L.true_false(h))
42	    case Con{x, +t} 1n+p:
43	      nth_hi(X, t, p, dv, h)
44	
45	# ---- read ----
46	
47	def rf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +m: Maybe<&2, M.Node<K>>) -> {M.read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), (ST.nodes(~K, l, d, nl), DA.item(M.Node<K>, m))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), or_else(M.Node<K>, m, M.Free{0n})) : M.TreeMap<K, V, cmp> & M.Node<K>}:
48	  match m:
49	    case None{}:
50	      {==}
51	    case Some{x}:
52	      {==}
53	
54	
55	def read_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat) -> {M.read(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.nd(K, nl, id)) : M.TreeMap<K, V, cmp> & M.Node<K>}:
56	  match id:
57	    case 0n:
58	      {==}
59	    case 1n+i:
60	      %Equal.sym(M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>, M.ns_get(~K, ST.nodes(~K, l, d, nl), i), (ST.nodes(~K, l, d, nl), DA.item(M.Node<K>, SC.nth(M.Node<K>, nl, i))), NSL.ns_get_ok(~K, l, d, nl, hl, hd, hc, i)) : {M.read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.nd(K, nl, 1n+i)) : M.TreeMap<K, V, cmp> & M.Node<K>}
61	      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, nl, i, M.Free{0n}), or_else(M.Node<K>, SC.nth(M.Node<K>, nl, i), M.Free{0n}), nth_or_nth(M.Node<K>, nl, i, M.Free{0n})) : {M.read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), (ST.nodes(~K, l, d, nl), DA.item(M.Node<K>, SC.nth(M.Node<K>, nl, i)))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), _) : M.TreeMap<K, V, cmp> & M.Node<K>}
62	      rf(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, SC.nth(M.Node<K>, nl, i))
63	
64	# ---- the payload read ----
65	
66	def gf2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +m: Maybe<&2, Maybe<&2, V>>) -> {M.get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, pl), DA.item(Maybe<&2, V>, m))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), or_else(Maybe<&2, V>, m, None{})) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
67	  match m:
68	    case None{}:
69	      {==}
70	    case Some{x}:
71	      {==}
72	
73	def get_id_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat) -> {M.get_id(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.pv(V, pl, id)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
74	  match id:
75	    case 0n:
76	      {==}
77	    case 1n+i:
78	      %Equal.sym(D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>, D.get_at(~Maybe<&2, V>, ST.pays(~V, l, d, pl), i), (ST.pays(~V, l, d, pl), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i))), AB.blk_get(~Maybe<&2, V>, l, d, pl, hl, hd, pl_cap(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp), i)) : {M.get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
79	      %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, pl, i, None{}), or_else(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i), None{}), nth_or_nth(Maybe<&2, V>, pl, i, None{})) : {M.get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, pl), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i)))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), _) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
80	      gf2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, SC.nth(Maybe<&2, V>, pl, i))
81	
82	# ---- write ----
83	
84	# the shadow's write: the node of id replaced when id names a slot
85	def wr_nl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +x: M.Node<K>) -> List<&2, M.Node<K>>:
86	  match id:
87	    case 0n:
88	      nl
89	    case 1n+i:
90	      ST.pk(List<&2, M.Node<K>>, Nat.is_lt(i, SC.length(M.Node<K>, nl)), SC.update(M.Node<K>, nl, i, x), nl)
91	
92	def wr_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +i: Nat, +x: M.Node<K>, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == b : Bool}) -> {M.write(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), 1n+i, x) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, ST.pk(List<&2, M.Node<K>>, b, SC.update(M.Node<K>, nl, i, x), nl), pl, t, fl}) : M.TreeMap<K, V, cmp>}:
93	  match b:
94	    case True{}:
95	      %Equal.sym(M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, M.ns_set(~K, ST.nodes(~K, l, d, nl), i, x), (ST.nodes(~K, l, d, SC.update(M.Node<K>, nl, i, x)), Done{Unit{}}), NSL.ns_set_in(~K, l, d, nl, hl, hd, hc, i, x, hb)) : {M.write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), _) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SC.update(M.Node<K>, nl, i, x), pl, t, fl}) : M.TreeMap<K, V, cmp>}
96	      {==}
97	    case False{}:
98	      %Equal.sym(M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, M.ns_set(~K, ST.nodes(~K, l, d, nl), i, x), (ST.nodes(~K, l, d, nl), Fail{DE.IndexOutOfRange{}}), NSL.ns_set_out(~K, l, d, nl, hl, hd, hc, i, x, hb)) : {M.write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), _) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}) : M.TreeMap<K, V, cmp>}
99	      {==}
100	
101	def write_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat, +x: M.Node<K>) -> {M.write(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id, x) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, wr_nl(K, nl, id, x), pl, t, fl}) : M.TreeMap<K, V, cmp>}:
102	  match id:
103	    case 0n:
104	      {==}
105	    case 1n+i:
106	      wr_c2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp, i, x, Nat.is_lt(i, SC.length(M.Node<K>, nl)), {==})
107	
108	# ---- exchange ----
109	
110	def ex_pl(-V: Data, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Maybe<&2, V>) -> List<&2, Maybe<&2, V>>:
111	  match id:
112	    case 0n:
113	      pl
114	    case 1n+i:
115	      ST.pk(List<&2, Maybe<&2, V>>, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)), SC.update(Maybe<&2, V>, pl, i, v), pl)
116	
117	def ef(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +pl2: List<&2, Maybe<&2, V>>, +m: Maybe<&2, Maybe<&2, V>>) -> {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, pl2), DA.item(Maybe<&2, V>, m))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl2, t, fl}), or_else(Maybe<&2, V>, m, None{})) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
118	  match m:
119	    case None{}:
120	      {==}
121	    case Some{x}:
122	      {==}
123	
124	def ex_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +i: Nat, +v: Maybe<&2, V>, +b: Bool, +hb: {Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)) == b : Bool}) -> {M.exchange(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), 1n+i, v) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, ST.pk(List<&2, Maybe<&2, V>>, b, SC.update(Maybe<&2, V>, pl, i, v), pl), t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
125	  match b:
126	    case True{}:
127	      %Equal.sym(D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>, D.swap_at(~Maybe<&2, V>, ST.pays(~V, l, d, pl), i, v), (ST.pays(~V, l, d, SC.update(Maybe<&2, V>, pl, i, v)), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i))), AB.blk_swap(~Maybe<&2, V>, l, d, pl, hl, hd, pl_cap(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp), i, v, hb)) : {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, SC.update(Maybe<&2, V>, pl, i, v), t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
128	      %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, pl, i, None{}), or_else(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i), None{}), nth_or_nth(Maybe<&2, V>, pl, i, None{})) : {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, SC.update(Maybe<&2, V>, pl, i, v)), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i)))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, SC.update(Maybe<&2, V>, pl, i, v), t, fl}), _) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
129	      ef(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, SC.update(Maybe<&2, V>, pl, i, v), SC.nth(Maybe<&2, V>, pl, i))
130	    case False{}:
131	      %Equal.sym(D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>, D.swap_at(~Maybe<&2, V>, ST.pays(~V, l, d, pl), i, v), (ST.pays(~V, l, d, pl), Fail{DE.IndexOutOfRange{}}), AB.blk_swap_out(~Maybe<&2, V>, l, d, pl, hl, hd, pl_cap(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp), i, v, hb)) : {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
132	      %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, pl, i, None{}), None{}, nth_hi(Maybe<&2, V>, pl, i, None{}, hb)) : {(ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), None{}) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), _) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
133	      {==}
134	
135	def exchange_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat, +v: Maybe<&2, V>) -> {M.exchange(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id, v) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, ex_pl(V, pl, id, v), t, fl}), ST.pv(V, pl, id)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
136	  match id:
137	    case 0n:
138	      {==}
139	    case 1n+i:
140	      ex_c2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp, i, v, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)), {==})