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/u32.bend as U
6	import ../../lib/array.bend as AR
7	import ../../../spec/lib/common.bend as SC
8	import ../../../spec/containers/dynamic_array.bend as S
9	import ../../../src/containers/dynamic_array.bend as DA
10	import ./layout.bend as LY
11	import ../../../src/containers/types/dynamic_array.bend as E
12	
13	# Shadow (Data) description of a reachable dynamic array: limit, depth,
14	# length and the mirror tree t of its Base.Array (the array is thaw(t)).
15	
16	type Shadow<-T: Data> is Data:
17	  Sh{limit: Nat, depth: Nat, len: Nat, tree: AR.Tree<Maybe<&2, T>>}
18	
19	def real(-T: Data, sh: Shadow<T>) -> DA.DynArray<&2, T>:
20	  match sh:
21	    case Sh{l, +d, n, t}:
22	      DA.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)}
23	
24	# Representation invariant.
25	def good(-T: Data, sh: Shadow<T>) -> Bool:
26	  match sh:
27	    case Sh{+l, +d, +n, +t}:
28	      Bool.and(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))))
29	
30	def model(-T: Data, sh: Shadow<T>) -> S.Model<T>:
31	  match sh:
32	    case Sh{l, d, n, t}:
33	      S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, t))}
34	
35	# Abstraction of an actual dynamic array (proof-level; reads the Base.Array
36	# tree through AR.freeze).
37	def abs(-T: Data, da: DA.DynArray<&2, T>) -> S.Model<T>:
38	  match da:
39	    case DA.DA{l, d, c, n, arr}:
40	      S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, AR.freeze(Maybe<&2, T>, arr)))}
41	
42	def abs_real(-T: Data, +sh: Shadow<T>) -> {abs(T, real(T, sh)) == model(T, sh) : S.Model<T>}:
43	  match sh:
44	    case Sh{+l, +d, +n, +t}:
45	      %Equal.sym(AR.Tree<Maybe<&2, T>>, AR.freeze(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t)), t, AR.freeze_thaw(Maybe<&2, T>, t)) : {S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, _))} == S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, t))} : S.Model<T>}
46	      {==}
47	
48	# Invariant of an actual array: it is the realization of a good shadow.
49	def Inv(-T: Data, da: DA.DynArray<&2, T>) -> Type:
50	  Sigma<&1, &1, Shadow<T>, sh => {da == real(T, sh) : DA.DynArray<&2, T>} & {good(T, sh) == True{} : Bool}>
51	
52	# ---- projections of good ----
53	
54	def g_limit(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Nat.is_le(l, 31n) == True{} : Bool}:
55	  L.and_left(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))), g)
56	
57	def g_rest1(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))) == True{} : Bool}:
58	  L.and_right(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))), g)
59	
60	def g_depth(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Nat.is_le(d, l) == True{} : Bool}:
61	  L.and_left(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)), g_rest1(T, l, d, n, t, g))
62	
63	def g_rest2(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)) == True{} : Bool}:
64	  L.and_right(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)), g_rest1(T, l, d, n, t, g))
65	
66	def g_perfect(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}:
67	  L.and_left(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n), g_rest2(T, l, d, n, t, g))
68	
69	def g_lay(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {LY.lay(T, AR.slots(Maybe<&2, T>, t), n) == True{} : Bool}:
70	  L.and_right(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n), g_rest2(T, l, d, n, t, g))
71	
72	def good_intro(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +a: {Nat.is_le(l, 31n) == True{} : Bool}, +b: {Nat.is_le(d, l) == True{} : Bool}, +c: {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}, +e: {LY.lay(T, AR.slots(Maybe<&2, T>, t), n) == True{} : Bool}) -> {good(T, Sh{l, d, n, t}) == True{} : Bool}:
73	  L.and_intro(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))), a,
74	    L.and_intro(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)), b,
75	      L.and_intro(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n), c, e)))
76	
77	# ---- derived facts ----
78	
79	def lt32(+d: Nat, +l: Nat, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hl: {Nat.is_le(l, 31n) == True{} : Bool}) -> {Nat.is_lt(d, 32n) == True{} : Bool}:
80	  N.le_lt_succ(d, 31n, N.le_trans(d, l, 31n, hd, hl))
81	
82	def le32(+d: Nat, +l: Nat, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hl: {Nat.is_le(l, 31n) == True{} : Bool}) -> {Nat.is_le(d, 32n) == True{} : Bool}:
83	  N.lt_le(d, 32n, lt32(d, l, hd, hl))
84	
85	def pow2_src(+d: Nat) -> {DA.pow2(d) == SC.pow2(d) : Nat}:
86	  match d:
87	    case 0n:
88	      {==}
89	    case 1n+p:
90	      Equal.cong(Nat, Nat, Nat.double, DA.pow2(p), SC.pow2(p), pow2_src(p))
91	
92	def slot_item(-T: Data, +m: Maybe<&2, T>) -> {DA.slot_result(T, m) == S.item_result(T, m) : Result<&2, &2, E.Error, T>}:
93	  match m:
94	    case None{}:
95	      {==}
96	    case Some{x}:
97	      {==}
98	
99	def empty_eq(-T: Data, +d: Nat) -> {DA.empty_slots(T, d) == AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})) : Array<Maybe<&2, T>>}:
100	  AR.new(Maybe<&2, T>, d, None{})
101	
102	def grown_eq(-T: Data, +d: Nat, +t: AR.Tree<Maybe<&2, T>>) -> {DA.grown(T, d, AR.thaw(Maybe<&2, T>, t)) == AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}) : Array<Maybe<&2, T>>}:
103	  %Equal.sym(Array<Maybe<&2, T>>, DA.empty_slots(T, d), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), empty_eq(T, d)) : {ANode{AR.thaw(Maybe<&2, T>, t), _} == ANode{AR.thaw(Maybe<&2, T>, t), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{}))} : Array<Maybe<&2, T>>}
104	  {==}
105	
106	def slots_grown(-T: Data, +d: Nat, +t: AR.Tree<Maybe<&2, T>>) -> {AR.slots(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}) == SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})) : List<&2, Maybe<&2, T>>}:
107	  %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{})) : {SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), _) == SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})) : List<&2, Maybe<&2, T>>}
108	  {==}