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/order.bend as O
6	import ../../lib/u32.bend as U
7	import ../../lib/array.bend as AR
8	import ../../../spec/lib/common.bend as SC
9	import ../../../spec/containers/binary_heap.bend as S
10	import ../../../src/containers/binary_heap.bend as H
11	import ../../../src/containers/types/binary_heap.bend as E
12	import ./idx.bend as IX
13	import ./slots.bend as SL
14	import ./vals.bend as V
15	import ./root.bend as RT
16	
17	# Shadow (Data) description of a reachable heap: the number of elements, the
18	# depth of the block and the mirror tree of its Base.Array. The array itself
19	# is linear, so -- exactly as in proofs/dynamic_array and proofs/bitset --
20	# every law is stated about the heap BUILT from a Data mirror tree.
21	
22	type Shadow<-A: Data> is Data:
23	  Sh{size: Nat, depth: Nat, tree: AR.Tree<Maybe<&2, A>>}
24	
25	def real(~A: Data, sh: Shadow<A>) -> H.Heap<A>:
26	  match sh:
27	    case Sh{+size, +depth, t}:
28	      H.BH{size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t)}
29	
30	# Representation invariant: the block is a perfect tree of `depth` levels, the
31	# elements occupy exactly the slots [0, size), and heap order holds over them.
32	def good(~A: Data, ~cmp: A -> A -> Cmp, sh: Shadow<A>) -> Bool:
33	  match sh:
34	    case Sh{+size, +depth, +t}:
35	      Bool.and(Nat.is_le(depth, 31n),
36	        Bool.and(AR.perfect(Maybe<&2, A>, depth, t),
37	          Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size),
38	            Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size),
39	              Nat.is_le(size, SC.pow2(depth))))))
40	
41	# Abstraction: the multiset of the occupied slots, sorted -- which is what
42	# the specification calls a priority queue.
43	def model(~A: Data, ~cmp: A -> A -> Cmp, sh: Shadow<A>) -> List<&2, A>:
44	  match sh:
45	    case Sh{+size, +depth, +t}:
46	      V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t), size))
47	
48	# Abstraction of an actual heap (proof level; reads the Base.Array through
49	# AR.freeze).
50	def abs(~A: Data, ~cmp: A -> A -> Cmp, h: H.Heap<A>) -> List<&2, A>:
51	  match h:
52	    case H.BH{+size, n, depth, cap, arr}:
53	      V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, AR.freeze(Maybe<&2, A>, arr)), size))
54	
55	def abs_real(~A: Data, ~cmp: A -> A -> Cmp, +sh: Shadow<A>) -> {abs(~A, ~cmp, real(~A, sh)) == model(~A, ~cmp, sh) : List<&2, A>}:
56	  match sh:
57	    case Sh{+size, +depth, +t}:
58	      %Equal.sym(AR.Tree<Maybe<&2, A>>, AR.freeze(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t)), t, AR.freeze_thaw(Maybe<&2, A>, t)) : {V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, _), size)) == V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t), size)) : List<&2, A>}
59	      {==}
60	
61	# Invariant of an actual heap: it is the realization of a good shadow.
62	def Inv(~A: Data, ~cmp: A -> A -> Cmp, h: H.Heap<A>) -> Type:
63	  Sigma<&1, &1, Shadow<A>, sh => {h == real(~A, sh) : H.Heap<A>} & {good(~A, ~cmp, sh) == True{} : Bool}>
64	
65	# ---- projections ----
66	
67	def g_depth(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {Nat.is_le(depth, 31n) == True{} : Bool}:
68	  L.and_left(Nat.is_le(depth, 31n), Bool.and(AR.perfect(Maybe<&2, A>, depth, t), Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))))), g)
69	
70	def g_rest1(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {Bool.and(AR.perfect(Maybe<&2, A>, depth, t), Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))))) == True{} : Bool}:
71	  L.and_right(Nat.is_le(depth, 31n), Bool.and(AR.perfect(Maybe<&2, A>, depth, t), Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))))), g)
72	
73	def g_perfect(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {AR.perfect(Maybe<&2, A>, depth, t) == True{} : Bool}:
74	  L.and_left(AR.perfect(Maybe<&2, A>, depth, t), Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth)))), g_rest1(~A, ~cmp, size, depth, t, g))
75	
76	def g_rest2(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth)))) == True{} : Bool}:
77	  L.and_right(AR.perfect(Maybe<&2, A>, depth, t), Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth)))), g_rest1(~A, ~cmp, size, depth, t, g))
78	
79	def g_lay(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {SL.lay(~A, AR.slots(Maybe<&2, A>, t), size) == True{} : Bool}:
80	  L.and_left(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))), g_rest2(~A, ~cmp, size, depth, t, g))
81	
82	def g_rest3(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))) == True{} : Bool}:
83	  L.and_right(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))), g_rest2(~A, ~cmp, size, depth, t, g))
84	
85	def g_ho(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size) == True{} : Bool}:
86	  L.and_left(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth)), g_rest3(~A, ~cmp, size, depth, t, g))
87	
88	def g_size(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +g: {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}) -> {Nat.is_le(size, SC.pow2(depth)) == True{} : Bool}:
89	  L.and_right(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth)), g_rest3(~A, ~cmp, size, depth, t, g))
90	
91	def good_intro(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +hd: {Nat.is_le(depth, 31n) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, depth, t) == True{} : Bool}, +hlay: {SL.lay(~A, AR.slots(Maybe<&2, A>, t), size) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size) == True{} : Bool}, +hs: {Nat.is_le(size, SC.pow2(depth)) == True{} : Bool}) -> {good(~A, ~cmp, Sh{size, depth, t}) == True{} : Bool}:
92	  L.and_intro(Nat.is_le(depth, 31n), Bool.and(AR.perfect(Maybe<&2, A>, depth, t), Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))))), hd,
93	    L.and_intro(AR.perfect(Maybe<&2, A>, depth, t), Bool.and(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth)))), pf,
94	      L.and_intro(SL.lay(~A, AR.slots(Maybe<&2, A>, t), size), Bool.and(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth))), hlay,
95	        L.and_intro(SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size), Nat.is_le(size, SC.pow2(depth)), hho, hs))))
96	
97	def sh_depth(~A: Data, sh: Shadow<A>) -> Nat:
98	  match sh:
99	    case Sh{+size, +depth, +t}:
100	      depth
101	
102	def sh_size(~A: Data, sh: Shadow<A>) -> Nat:
103	  match sh:
104	    case Sh{+size, +depth, +t}:
105	      size
106	
107	# depth <= 31 in the form the U32 bridges want it
108	def depth_lt32(+depth: Nat, +hd: {Nat.is_le(depth, 31n) == True{} : Bool}) -> {Nat.is_lt(depth, 32n) == True{} : Bool}:
109	  N.le_lt_succ(depth, 31n, hd)
110	
111	# ---- the constructor ----
112	
113	def initial(~A: Data) -> Shadow<A>:
114	  Sh{0n, 0n, AR.TLeaf{None{}}}
115	
116	def new_real(~A: Data) -> {H.new(~A) == real(~A, initial(~A)) : H.Heap<A>}:
117	  Equal.cong(Array<Maybe<&2, A>>, H.Heap<A>, a => H.BH{0n, 0, 0n, 1, a}, H.empty_slots(~A, 0n), AR.thaw(Maybe<&2, A>, AR.TLeaf{None{}}), AR.new(Maybe<&2, A>, 0n, None{}))
118	
119	def new_good(~A: Data, ~cmp: A -> A -> Cmp) -> {good(~A, ~cmp, initial(~A)) == True{} : Bool}:
120	  {==}
121	
122	def new_model(~A: Data, ~cmp: A -> A -> Cmp) -> {model(~A, ~cmp, initial(~A)) == Nil{} : List<&2, A>}:
123	  {==}