proofs/containers/queue/proof.bend
bend-collections-laws-containers@1.0.0.0 · 111 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/queue.bend as S
3import bend-collections-laws-containers@1.0.0.0/src/containers/queue.bend as Q
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/queue.bend as E
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/state.bend as ST
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/steps.bend as PS
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/trace.bend as FT
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
10import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as VL
12
13# FIFO queue (two lists, src/containers/queue.bend): public proof entry point.
14# shadow ST.Sh{front, back}: the queue QU{front, back, |front| +
15# |back|}
16# abstraction ST.model(sh) = front ++ reverse(back), oldest first
17# ready PS.ready: reversing the back into an empty front keeps the
18# model and leaves the front nonempty unless the queue is empty
19# operations PS.step_ok: every public operation, errors included
20# (dequeue or peek on an empty queue is Fail{EmptyQueue}, queue
21# unchanged)
22# traces trace_from / trace_new: any finite operation list, no
23# premise on its length or on the queue's size
24
25def new_abs(~T: Data) -> {ST.model(T, ST.initial(T)) == Nil{} : List<&2, T>}:
26 {==}
27
28def new_real(~T: Data) -> {Q.new(~T) == ST.real(T, ST.initial(T)) : Q.Queue<T>}:
29 {==}
30
31def step_ok(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>) -> PS.StepOK(~T, sh, op):
32 PS.step_ok(~T, sh, op)
33
34# a queue determines its shadow
35def shadow_unique(~T: Data, +a: ST.Shadow<T>, +b: ST.Shadow<T>, +e: {ST.real(T, a) == ST.real(T, b) : Q.Queue<T>}) -> {a == b : ST.Shadow<T>}:
36 ST.real_inj(T, a, b, e)
37
38def trace_from(~T: Data, +ops: List<&2, E.Op<T>>, +sh0: ST.Shadow<T>) -> FT.TraceOK(~T, ops, sh0):
39 FT.trace_from(~T, ops, sh0)
40
41# arbitrary finite operation traces from the real constructor
42def trace_new(~T: Data, +ops: List<&2, E.Op<T>>) -> FT.TraceOK(~T, ops, ST.initial(T)):
43 FT.trace_from(~T, ops, ST.initial(T))
44
45# ==== the contract of queue (stated in spec/containers/queue.bend) ====================
46
47# ---- the implementation ----
48def Impl(~T: Data, sh: ST.Shadow<T>, op: E.Op<T>, Post: (List<&2, T> & E.Obs<T>) -> Type) -> Type:
49 Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {Q.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : Q.Queue<T> & E.Obs<T>} & Post((ST.model(T, sh2), o))>>
50
51def impl_of(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, -Post: (List<&2, T> & E.Obs<T>) -> Type, k: PS.StepOK(~T, sh, op), pf: Post(S.step(T, ST.model(T, sh), op))) -> Impl(~T, sh, op, Post):
52 match k:
53 case Tuple{sh2, Tuple{o, Tuple{e1, e2}}}:
54 (sh2, (o, (e1, L.subst(List<&2, T> & E.Obs<T>, Post, S.step(T, ST.model(T, sh), op), (ST.model(T, sh2), o), Equal.sym(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), S.step(T, ST.model(T, sh), op), e2), pf))))
55
56def impl(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, -Post: (List<&2, T> & E.Obs<T>) -> Type, pf: Post(S.step(T, ST.model(T, sh), op))) -> Impl(~T, sh, op, Post):
57 impl_of(~T, sh, op, Post, step_ok(~T, sh, op), pf)
58
59# ---- Length, iteration ----
60def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs):
61 {==}
62
63def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs):
64 {==}
65
66def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs):
67 {==}
68
69def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs):
70 {==}
71
72# ---- Empty_Vector ----
73def new_empty(~T: Data) -> {SC.length(T, ST.model(T, ST.initial(T))) == 0n : Nat}:
74 %Equal.sym(List<&2, T>, ST.model(T, ST.initial(T)), Nil{}, new_abs(~T)) : {SC.length(T, _) == 0n : Nat}
75 {==}
76
77def new_impl(~T: Data) -> {Q.new(~T) == ST.real(T, ST.initial(T)) : Q.Queue<T>}:
78 new_real(~T)
79
80# ---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last'Old + 1) = New_Item ----
81def enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_length(T, xs, v):
82 VL.snoc_length(T, xs, v)
83
84def enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_prefix(T, xs, v):
85 VL.snoc_prefix(T, xs, v)
86
87def enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_element(T, xs, v):
88 VL.snoc_last(T, xs, v)
89
90# ---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); dequeue returns First_Element'Old ----
91def dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_length(T, h, t):
92 {==}
93
94def dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_shifted(T, h, t):
95 VL.tail_shifted(T, h, t)
96
97def dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_result(T, h, t):
98 {==}
99
100def dequeue_empty(-T: Data) -> S.Delete_First.dequeue_empty(T):
101 {==}
102
103# ---- First_Element: Element (Model, First); nothing changes ----
104def peek_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_first(T, h, t):
105 ({==}, {==})
106
107def peek_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_frame(T, xs):
108 {==}
109
110def peek_empty(-T: Data) -> S.First_Element.peek_empty(T):
111 {==}