1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/array.bend as AR
5	import ../../lib/list.bend as LL
6	import ../../../spec/lib/common.bend as SC
7	import ../../../src/containers/dynamic_array.bend as D
8	import ../../../src/containers/types/dynamic_array.bend as DE
9	import ../dynamic_array/layout.bend as LY
10	import ../dynamic_array/state.bend as DAS
11	import ../dynamic_array/steps.bend as DST
12	import ../dynamic_array/growth.bend as DGR
13	import ../dynamic_array/clear.bend as DCL
14	
15	# The dynamic array operations the TreeMap calls, over a good array shadow:
16	# the result is the realization of the updated shadow.
17	
18	
19	def item(-T: Data, m: Maybe<&2, T>) -> Result<&2, &2, DE.Error, T>:
20	  match m:
21	    case None{}:
22	      Fail{DE.IndexOutOfRange{}}
23	    case Some{x}:
24	      Done{x}
25	
26	def gf(~T: Data, +l: Nat, +d: Nat, +c: Nat, +n: Nat, -arr: Array<Maybe<&2, T>>, +x: Maybe<&2, T>) -> {D.get_found_at(~T, l, d, c, n, (arr, x)) == (D.DA{l, d, c, n, arr}, item(T, x)) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
27	  match x:
28	    case None{}:
29	      {==}
30	    case Some{v}:
31	      {==}
32	
33	def n_len(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}) -> {SC.length(T, LY.somes(T, AR.slots(Maybe<&2, T>, t))) == n : Nat}:
34	  LY.lay_len(T, AR.slots(Maybe<&2, T>, t), n, DAS.g_lay(T, l, d, n, t, g))
35	
36	def nth_hi(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +h: {Nat.is_lt(i, n) == False{} : Bool}) -> {SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i) == None{} : Maybe<&2, T>}:
37	  LL.nth_none(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i, L.subst(Nat, z => {Nat.is_le(z, i) == True{} : Bool}, n, SC.length(T, LY.somes(T, AR.slots(Maybe<&2, T>, t))), Equal.sym(Nat, SC.length(T, LY.somes(T, AR.slots(Maybe<&2, T>, t))), n, n_len(~T, l, d, n, t, g)), N.not_lt_le(i, n, h)))
38	
39	def lt_cap(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}:
40	  N.lt_le_trans(i, n, SC.pow2(d), h, DST.n_le_cap(T, l, d, n, t, g))
41	
42	def slot_at(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), i) == Some{SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i)} : Maybe<&2, Maybe<&2, T>>}:
43	  LY.lay_nth(T, AR.slots(Maybe<&2, T>, t), n, i, DAS.g_lay(T, l, d, n, t, g), h)
44	
45	def get_c(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, n) == b : Bool}) -> {D.get_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, b) == (DAS.real(T, DAS.Sh{l, d, n, t}), item(T, SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
46	  match b:
47	    case False{}:
48	      %Equal.sym(Maybe<&2, T>, SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i), None{}, nth_hi(~T, l, d, n, t, g, i, hb)) : {(D.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)}, Fail{DE.IndexOutOfRange{}}) == (DAS.real(T, DAS.Sh{l, d, n, t}), item(T, _)) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
49	      {==}
50	    case True{}:
51	      +x = SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i)
52	      +e = AR.get(Maybe<&2, T>, d, t, U32.from_nat(i), x, DAS.lt32(d, l, DAS.g_depth(T, l, d, n, t, g), DAS.g_limit(T, l, d, n, t, g)), DST.idx_lt(T, l, d, n, t, i, g, lt_cap(~T, l, d, n, t, g, i, hb)), DST.idx_slot(T, l, d, n, t, i, x, g, lt_cap(~T, l, d, n, t, g, i, hb), slot_at(~T, l, d, n, t, g, i, hb)), DAS.g_perfect(T, l, d, n, t, g))
53	      %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i)), (AR.thaw(Maybe<&2, T>, t), x), e) : {D.get_found_at(~T, l, d, SC.pow2(d), n, _) == (DAS.real(T, DAS.Sh{l, d, n, t}), item(T, x)) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
54	      gf(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), x)
55	
56	# get: the item at i, or out of range
57	def da_get(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat) -> {D.get_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), i) == (DAS.real(T, DAS.Sh{l, d, n, t}), item(T, SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
58	  get_c(~T, l, d, n, t, g, i, Nat.is_lt(i, n), {==})
59	
60	# set: the item at i replaced (i < n)
61	def da_set(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {D.set_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), i, v) == (DAS.real(T, DAS.Sh{l, d, n, AR.upd(Maybe<&2, T>, d, t, i, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
62	  +e = DST.set_arr(T, l, d, n, t, i, Some{v}, SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i), g, lt_cap(~T, l, d, n, t, g, i, h), slot_at(~T, l, d, n, t, g, i, h))
63	  %Equal.sym(Bool, Nat.is_lt(i, n), True{}, h) : {D.set_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _) == (DAS.real(T, DAS.Sh{l, d, n, AR.upd(Maybe<&2, T>, d, t, i, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
64	  %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), Some{v}), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, Some{v})), e) : {(D.DA{l, d, SC.pow2(d), n, _}, Done{Unit{}}) == (DAS.real(T, DAS.Sh{l, d, n, AR.upd(Maybe<&2, T>, d, t, i, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
65	  {==}
66	
67	def da_set_out(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, n) == False{} : Bool}) -> {D.set_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), i, v) == (DAS.real(T, DAS.Sh{l, d, n, t}), Fail{DE.IndexOutOfRange{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
68	  %Equal.sym(Bool, Nat.is_lt(i, n), False{}, h) : {D.set_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _) == (DAS.real(T, DAS.Sh{l, d, n, t}), Fail{DE.IndexOutOfRange{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
69	  {==}
70	
71	# swap: the item at i replaced, the old one returned (i < n)
72	def da_swap(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {D.swap_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), i, v) == (DAS.real(T, DAS.Sh{l, d, n, AR.upd(Maybe<&2, T>, d, t, i, Some{v})}), item(T, SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i))) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
73	  +x = SC.nth(T, LY.somes(T, AR.slots(Maybe<&2, T>, t)), i)
74	  +e = DST.swap_arr(T, l, d, n, t, i, Some{v}, x, g, lt_cap(~T, l, d, n, t, g, i, h), slot_at(~T, l, d, n, t, g, i, h))
75	  %Equal.sym(Bool, Nat.is_lt(i, n), True{}, h) : {D.swap_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _) == (DAS.real(T, DAS.Sh{l, d, n, AR.upd(Maybe<&2, T>, d, t, i, Some{v})}), item(T, x)) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
76	  %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(i), Some{v}), (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, Some{v})), x), e) : {D.get_found_at(~T, l, d, SC.pow2(d), n, _) == (DAS.real(T, DAS.Sh{l, d, n, AR.upd(Maybe<&2, T>, d, t, i, Some{v})}), item(T, x)) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
77	  gf(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, i, Some{v})), x)
78	
79	def da_swap_out(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +i: Nat, +v: T, +h: {Nat.is_lt(i, n) == False{} : Bool}) -> {D.swap_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), i, v) == (DAS.real(T, DAS.Sh{l, d, n, t}), Fail{DE.IndexOutOfRange{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}:
80	  %Equal.sym(Bool, Nat.is_lt(i, n), False{}, h) : {D.swap_checked_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), i, v, _) == (DAS.real(T, DAS.Sh{l, d, n, t}), Fail{DE.IndexOutOfRange{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, T>}
81	  {==}
82	
83	def da_len(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}) -> {D.length(T, DAS.real(T, DAS.Sh{l, d, n, t})) == (DAS.real(T, DAS.Sh{l, d, n, t}), n) : D.DynArray<&2, T> & Nat}:
84	  {==}
85	
86	def da_clear(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}) -> {D.clear_at(~T, DAS.real(T, DAS.Sh{l, d, n, t})) == DAS.real(T, DAS.Sh{l, d, 0n, AR.trep(Maybe<&2, T>, d, None{})}) : D.DynArray<&2, T>}:
87	  %Equal.sym(D.DynArray<&2, T>, D.clear_at(~T, DAS.real(T, DAS.Sh{l, d, n, t})), D.clear(T, DAS.real(T, DAS.Sh{l, d, n, t})), DCL.clear_eq(~T, l, d, n, t, g)) : {_ == DAS.real(T, DAS.Sh{l, d, 0n, AR.trep(Maybe<&2, T>, d, None{})}) : D.DynArray<&2, T>}
88	  %Equal.sym(Array<Maybe<&2, T>>, Array.new(Maybe<&2, T>, d, None{}), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), AR.new(Maybe<&2, T>, d, None{})) : {D.DA{l, d, SC.pow2(d), 0n, _} == DAS.real(T, DAS.Sh{l, d, 0n, AR.trep(Maybe<&2, T>, d, None{})}) : D.DynArray<&2, T>}
89	  {==}
90	
91	# push, with room in the block
92	def da_push_room(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +v: T, +hn: {Nat.is_lt(n, SC.pow2(d)) == True{} : Bool}) -> {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), v) == (DAS.real(T, DAS.Sh{l, d, 1n+n, AR.upd(Maybe<&2, T>, d, t, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
93	  %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), True{}, hn) : {D.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l)) == (DAS.real(T, DAS.Sh{l, d, 1n+n, AR.upd(Maybe<&2, T>, d, t, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
94	  %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(n), Some{v}), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, t, n, Some{v})), DST.pi_arr(T, l, d, n, t, v, g, hn)) : {(D.DA{l, d, SC.pow2(d), 1n+n, _}, Done{Unit{}}) == (DAS.real(T, DAS.Sh{l, d, 1n+n, AR.upd(Maybe<&2, T>, d, t, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
95	  {==}
96	
97	
98	# push into a full block below the limit: the block doubles
99	def da_push_grow(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +v: T, +hn: {Nat.is_lt(n, SC.pow2(d)) == False{} : Bool}, +hd: {Nat.is_lt(d, l) == True{} : Bool}) -> {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), v) == (DAS.real(T, DAS.Sh{l, 1n+d, 1n+n, AR.upd(Maybe<&2, T>, 1n+d, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
100	  +g1 = DGR.grow_good(T, l, d, n, t, g, hd)
101	  +hn1 = N.le_lt_trans(n, SC.pow2(d), SC.pow2(1n+d), DST.n_le_cap(T, l, d, n, t, g), N.pow2_lt_succ(d))
102	  %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, hn) : {D.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l)) == (DAS.real(T, DAS.Sh{l, 1n+d, 1n+n, AR.upd(Maybe<&2, T>, 1n+d, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
103	  %Equal.sym(Bool, Nat.is_lt(d, l), True{}, hd) : {D.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _) == (DAS.real(T, DAS.Sh{l, 1n+d, 1n+n, AR.upd(Maybe<&2, T>, 1n+d, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
104	  %Equal.sym(Array<Maybe<&2, T>>, Array.new(Maybe<&2, T>, d, None{}), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), AR.new(Maybe<&2, T>, d, None{})) : {(D.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, Array.set(Maybe<&2, T>, ANode{AR.thaw(Maybe<&2, T>, t), _}, U32.from_nat(n), Some{v})}, Done{Unit{}}) == (DAS.real(T, DAS.Sh{l, 1n+d, 1n+n, AR.upd(Maybe<&2, T>, 1n+d, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
105	  %Equal.sym(Array<Maybe<&2, T>>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), U32.from_nat(n), Some{v}), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+d, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, n, Some{v})), DST.pi_arr(T, l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, v, g1, hn1)) : {(D.DA{l, 1n+d, Nat.double(SC.pow2(d)), 1n+n, _}, Done{Unit{}}) == (DAS.real(T, DAS.Sh{l, 1n+d, 1n+n, AR.upd(Maybe<&2, T>, 1n+d, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, n, Some{v})}), Done{Unit{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
106	  {==}
107	
108	# push into a full block at the limit: rejected
109	def da_push_full(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {DAS.good(T, DAS.Sh{l, d, n, t}) == True{} : Bool}, +v: T, +hn: {Nat.is_lt(n, SC.pow2(d)) == False{} : Bool}, +hd: {Nat.is_lt(d, l) == False{} : Bool}) -> {D.push_at(~T, DAS.real(T, DAS.Sh{l, d, n, t}), v) == (DAS.real(T, DAS.Sh{l, d, n, t}), Fail{DE.CapacityExceeded{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}:
110	  %Equal.sym(Bool, Nat.is_lt(n, SC.pow2(d)), False{}, hn) : {D.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, _, Nat.is_lt(d, l)) == (DAS.real(T, DAS.Sh{l, d, n, t}), Fail{DE.CapacityExceeded{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
111	  %Equal.sym(Bool, Nat.is_lt(d, l), False{}, hd) : {D.push_room_at(~T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), v, False{}, _) == (DAS.real(T, DAS.Sh{l, d, n, t}), Fail{DE.CapacityExceeded{}}) : D.DynArray<&2, T> & Result<&2, &2, DE.Error, Unit>}
112	  {==}