proofs/containers/binary_heap/state.bend
bend-collections-laws-containers@1.0.0.0 · 123 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
10import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as H
11import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as E
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as IX
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/slots.bend as SL
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as V
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/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
22type Shadow<-A: Data> is Data:
23 Sh{size: Nat, depth: Nat, tree: AR.Tree<Maybe<&2, A>>}
24
25def 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.
32def 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.
43def 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).
50def 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
55def 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.
62def 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
67def 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
70def 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
73def 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
76def 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
79def 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
82def 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
85def 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
88def 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
91def 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
97def sh_depth(~A: Data, sh: Shadow<A>) -> Nat:
98 match sh:
99 case Sh{+size, +depth, +t}:
100 depth
101
102def 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
108def 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
113def initial(~A: Data) -> Shadow<A>:
114 Sh{0n, 0n, AR.TLeaf{None{}}}
115
116def 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
119def new_good(~A: Data, ~cmp: A -> A -> Cmp) -> {good(~A, ~cmp, initial(~A)) == True{} : Bool}:
120 {==}
121
122def new_model(~A: Data, ~cmp: A -> A -> Cmp) -> {model(~A, ~cmp, initial(~A)) == Nil{} : List<&2, A>}:
123 {==}