1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../lib/array.bend as AR
6	import ../../../spec/lib/common.bend as SC
7	import ../../../src/containers/dynamic_array.bend as DA
8	import ./layout.bend as LY
9	import ./state.bend as ST
10	import ./steps.bend as SP
11	import ../../lib/array_ext.bend as AX
12	
13	# The executable clear (src/dynamic_array.bend clear_at) resets the occupied
14	# slots [0, n) to None, top down, in the block it already has; the parametric
15	# clear allocates a fresh all-None block of the same depth. On a good state
16	# the two agree: each reset is the in-place write pop makes (and keeps the
17	# layout good with one fewer element), and a good layout of length 0 is the
18	# all-None tree itself.
19	
20	# A list of Nones is the replication of None to its length.
21	def nones_rep_eq(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {LY.nones(T, xs) == True{} : Bool}) -> {xs == SC.replicate(Maybe<&2, T>, SC.length(Maybe<&2, T>, xs), None{}) : List<&2, Maybe<&2, T>>}:
22	  match xs:
23	    case Nil{}:
24	      {==}
25	    case Con{None{}, +r}:
26	      LL.cons_cong(Maybe<&2, T>, None{}, r, SC.replicate(Maybe<&2, T>, SC.length(Maybe<&2, T>, r), None{}), nones_rep_eq(T, r, h))
27	    case Con{Some{x}, r}:
28	      Empty.absurd({Con{Some{x}, r} == SC.replicate(Maybe<&2, T>, SC.length(Maybe<&2, T>, Con{Some{x}, r}), None{}) : List<&2, Maybe<&2, T>>}, L.false_true(h))
29	
30	# A layout of length 0 holds only Nones.
31	def lay0_nones(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {LY.lay(T, xs, 0n) == True{} : Bool}) -> {LY.nones(T, xs) == True{} : Bool}:
32	  match xs:
33	    case Nil{}:
34	      {==}
35	    case Con{None{}, r}:
36	      h
37	    case Con{Some{x}, r}:
38	      Empty.absurd({LY.nones(T, Con{Some{x}, r}) == True{} : Bool}, L.false_true(h))
39	
40	# The slots of a good empty shadow are those of the all-None tree.
41	def empty_slots_eq(-T: Data, +d: Nat, +t: AR.Tree<Maybe<&2, T>>, +pf: {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}, +h: {LY.lay(T, AR.slots(Maybe<&2, T>, t), 0n) == True{} : Bool}) -> {AR.slots(Maybe<&2, T>, t) == AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})) : List<&2, Maybe<&2, T>>}:
42	  +ss = AR.slots(Maybe<&2, T>, t)
43	  %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})) : {ss == _ : List<&2, Maybe<&2, T>>}
44	  %AR.slots_length(Maybe<&2, T>, d, t, pf) : {ss == SC.replicate(Maybe<&2, T>, _, None{}) : List<&2, Maybe<&2, T>>}
45	  nones_rep_eq(T, ss, lay0_nones(T, ss, h))
46	
47	# Resetting the k occupied slots of a good shadow gives the all-None block.
48	def clear_go_eq(~T: Data, +l: Nat, +d: Nat, +k: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, k, t}) == True{} : Bool}) -> {DA.clear_go_at(~T, k, AR.thaw(Maybe<&2, T>, t)) == DA.empty_slots(T, d) : Array<Maybe<&2, T>>}:
49	  match k:
50	    case 0n:
51	      +pf = ST.g_perfect(T, l, d, 0n, t, g)
52	      +te = AX.tree_ext(Maybe<&2, T>, d, t, AR.trep(Maybe<&2, T>, d, None{}), pf, AR.trep_perfect(Maybe<&2, T>, d, None{}), empty_slots_eq(T, d, t, pf, ST.g_lay(T, l, d, 0n, t, g)))
53	      %Equal.sym(Array<Maybe<&2, T>>, DA.empty_slots(T, d), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), ST.empty_eq(T, d)) : {AR.thaw(Maybe<&2, T>, t) == _ : Array<Maybe<&2, T>>}
54	      %te : {AR.thaw(Maybe<&2, T>, t) == AR.thaw(Maybe<&2, T>, _) : Array<Maybe<&2, T>>}
55	      {==}
56	    case 1n+ +m:
57	      +ss = AR.slots(Maybe<&2, T>, t)
58	      +x = SC.nth(T, LY.somes(T, ss), m)
59	      +hlay = ST.g_lay(T, l, d, 1n+m, t, g)
60	      +hm = N.lt_succ(m)
61	      +hi = N.lt_le_trans(m, 1n+m, SC.pow2(d), hm, SP.n_le_cap(T, l, d, 1n+m, t, g))
62	      +t2 = AR.upd(Maybe<&2, T>, d, t, m, None{})
63	      +hs = SP.upd_slots(T, l, d, 1n+m, t, m, None{}, g, hi)
64	      +g2 = ST.good_intro(T, l, d, m, t2, ST.g_limit(T, l, d, 1n+m, t, g), ST.g_depth(T, l, d, 1n+m, t, g), AR.upd_perfect(Maybe<&2, T>, d, t, m, None{}, ST.g_perfect(T, l, d, 1n+m, t, g)),
65	        L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, m) == True{} : Bool}, SC.update(Maybe<&2, T>, ss, m, None{}), AR.slots(Maybe<&2, T>, t2), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, t2), SC.update(Maybe<&2, T>, ss, m, None{}), hs), LY.lay_pop(T, ss, m, hlay)))
66	      %Equal.sym(Array<Maybe<&2, T>> & Maybe<&2, T>, Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t), U32.from_nat(m), None{}), (AR.thaw(Maybe<&2, T>, t2), x), SP.swap_arr(T, l, d, 1n+m, t, m, None{}, x, g, hi, LY.lay_nth(T, ss, 1n+m, m, hlay, hm))) : {DA.clear_go_at(~T, m, Array.set.fin(Maybe<&2, T>, _)) == DA.empty_slots(T, d) : Array<Maybe<&2, T>>}
67	      clear_go_eq(~T, l, d, m, t2, g2)
68	
69	def clear_eq(~T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}) -> {DA.clear_at(~T, ST.real(T, ST.Sh{l, d, n, t})) == DA.clear(T, ST.real(T, ST.Sh{l, d, n, t})) : DA.DynArray<&2, T>}:
70	  Equal.cong(Array<Maybe<&2, T>>, DA.DynArray<&2, T>, z => DA.DA{l, d, SC.pow2(d), 0n, z}, DA.clear_go_at(~T, n, AR.thaw(Maybe<&2, T>, t)), DA.empty_slots(T, d), clear_go_eq(~T, l, d, n, t, g))