1 import Base 2 import ../../../spec/containers/deque.bend as S 3 import ../../../src/containers/deque.bend as DQ 4 import ../../../src/containers/types/deque.bend as E 5 import ./state.bend as ST 6 import ./stepok.bend as K 7 import ./steps.bend as PS 8 import ./trace.bend as FT 9 import ../../lib/logic.bend as L 10 import ../../../spec/lib/common.bend as SC 11 import ../../../spec/lib/sequence.bend as V 12 import ../../lib/sequence.bend as VL 13 14 # Deque (two lists, src/containers/deque.bend): public proof entry point. 15 # shadow ST.Sh{front, back}: the deque DE{front, back, |front|, 16 # |back|} (the counts are the list lengths by construction) 17 # abstraction ST.model(sh) = front ++ reverse(back), front first 18 # rebalance proofs/deque/rebalance.bend: ready_front / ready_back move 19 # half of the other list over, keep the model, and leave the 20 # requested end nonempty unless the deque is empty 21 # operations PS.step_ok: every public operation, errors included (pop or 22 # peek on an empty deque is Fail{EmptyDeque}, deque unchanged) 23 # traces trace_from / trace_new: any finite operation list, no 24 # premise on its length or on the deque's size 25 # 26 # Every law is a template in the element type; END_TO_END.bend instantiates 27 # them at U32 and String. 28 29 def new_abs(~T: Data) -> {ST.model(T, ST.initial(T)) == Nil{} : List<&2, T>}: 30 {==} 31 32 def new_real(~T: Data) -> {DQ.new(~T) == ST.real(T, ST.initial(T)) : DQ.Deque}: 33 {==} 34 35 def step_ok(~T: Data, +sh: ST.Shadow, +op: E.Op) -> K.StepOK(~T, sh, op): 36 PS.step_ok(~T, sh, op) 37 38 # a deque determines its shadow 39 def shadow_unique(~T: Data, +a: ST.Shadow, +b: ST.Shadow, +e: {ST.real(T, a) == ST.real(T, b) : DQ.Deque}) -> {a == b : ST.Shadow}: 40 ST.real_inj(T, a, b, e) 41 42 def trace_from(~T: Data, +ops: List<&2, E.Op>, +sh0: ST.Shadow) -> FT.TraceOK(~T, ops, sh0): 43 FT.trace_from(~T, ops, sh0) 44 45 # arbitrary finite operation traces from the real constructor 46 def trace_new(~T: Data, +ops: List<&2, E.Op>) -> FT.TraceOK(~T, ops, ST.initial(T)): 47 FT.trace_from(~T, ops, ST.initial(T)) 48 49 # ==== the contract of deque (stated in spec/containers/deque.bend) ==================== 50 51 # ---- the implementation ---- 52 def Impl(~T: Data, sh: ST.Shadow, op: E.Op, Post: (List<&2, T> & E.Obs) -> Type) -> Type: 53 Sigma<&1, &1, ST.Shadow, sh2 => Sigma<&1, &1, E.Obs, o => {DQ.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : DQ.Deque & E.Obs} & Post((ST.model(T, sh2), o))>> 54 55 def impl_of(~T: Data, -sh: ST.Shadow, -op: E.Op, -Post: (List<&2, T> & E.Obs) -> Type, k: K.StepOK(~T, sh, op), pf: Post(S.step(T, ST.model(T, sh), op))) -> Impl(~T, sh, op, Post): 56 match k: 57 case Tuple{sh2, Tuple{o, Tuple{e1, e2}}}: 58 (sh2, (o, (e1, L.subst(List<&2, T> & E.Obs, Post, S.step(T, ST.model(T, sh), op), (ST.model(T, sh2), o), Equal.sym(List<&2, T> & E.Obs, (ST.model(T, sh2), o), S.step(T, ST.model(T, sh), op), e2), pf)))) 59 60 def impl(~T: Data, +sh: ST.Shadow, +op: E.Op, -Post: (List<&2, T> & E.Obs) -> Type, pf: Post(S.step(T, ST.model(T, sh), op))) -> Impl(~T, sh, op, Post): 61 impl_of(~T, sh, op, Post, step_ok(~T, sh, op), pf) 62 63 # ---- Length, iteration ---- 64 def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs): 65 {==} 66 67 def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs): 68 {==} 69 70 def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs): 71 {==} 72 73 def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs): 74 {==} 75 76 # ---- Empty_Vector ---- 77 def new_empty(~T: Data) -> {SC.length(T, ST.model(T, ST.initial(T))) == 0n : Nat}: 78 %Equal.sym(List<&2, T>, ST.model(T, ST.initial(T)), Nil{}, new_abs(~T)) : {SC.length(T, _) == 0n : Nat} 79 {==} 80 81 def new_impl(~T: Data) -> {DQ.new(~T) == ST.real(T, ST.initial(T)) : DQ.Deque}: 82 new_real(~T) 83 84 # ---- Prepend: Length + 1, Element (First) = New_Item, Range_Shifted (Old, New, First, Last'Old, 1) ---- 85 def push_front_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_front_length(T, xs, v): 86 {==} 87 88 def push_front_first(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_front_first(T, xs, v): 89 {==} 90 91 def push_front_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_front_shifted(T, xs, v): 92 VL.cons_shifted(T, xs, v) 93 94 # ---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last'Old + 1) = New_Item ---- 95 def push_back_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.push_back_length(T, xs, v): 96 VL.snoc_length(T, xs, v) 97 98 def push_back_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.push_back_prefix(T, xs, v): 99 VL.snoc_prefix(T, xs, v) 100 101 def push_back_element(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.push_back_element(T, xs, v): 102 VL.snoc_last(T, xs, v) 103 104 # ---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); pop_front returns First_Element'Old ---- 105 def pop_front_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_front_length(T, h, t): 106 {==} 107 108 def pop_front_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_front_shifted(T, h, t): 109 VL.tail_shifted(T, h, t) 110 111 def pop_front_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_front_result(T, h, t): 112 {==} 113 114 def pop_front_empty(-T: Data) -> S.Delete_First.pop_front_empty(T): 115 {==} 116 117 # ---- Delete_Last: Length - 1, Equal_Prefix (Model, Model'Old); pop_back returns Last_Element'Old ---- 118 def pop_back_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_back_length(T, h, t): 119 VL.init_length(T, t, h) 120 121 def pop_back_prefix(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_back_prefix(T, h, t): 122 VL.init_prefix(T, t, h) 123 124 def pop_back_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_back_result(T, h, t): 125 %Equal.sym(Maybe<&2, T>, SC.last(T, Con{h, t}), V.last_elem(T, Con{h, t}), VL.last_is_elem(T, t, h)) : {E.OItem{S.item(T, _)} == E.OItem{S.item(T, V.last_elem(T, Con{h, t}))} : E.Obs} 126 {==} 127 128 def pop_back_empty(-T: Data) -> S.Delete_Last.pop_back_empty(T): 129 {==} 130 131 # ---- First_Element / Last_Element: the end elements; nothing changes ---- 132 def peek_front_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_front_first(T, h, t): 133 ({==}, {==}) 134 135 def peek_front_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_front_frame(T, xs): 136 {==} 137 138 def peek_front_empty(-T: Data) -> S.First_Element.peek_front_empty(T): 139 {==} 140 141 def peek_back_last(-T: Data, +h: T, +t: List<&2, T>) -> S.Last_Element.peek_back_last(T, h, t): 142 %Equal.sym(Maybe<&2, T>, SC.last(T, Con{h, t}), V.last_elem(T, Con{h, t}), VL.last_is_elem(T, t, h)) : {E.OItem{S.item(T, _)} == E.OItem{S.item(T, V.last_elem(T, Con{h, t}))} : E.Obs} 143 {==} 144 145 def peek_back_frame(-T: Data, +xs: List<&2, T>) -> S.Last_Element.peek_back_frame(T, xs): 146 {==} 147 148 def peek_back_empty(-T: Data) -> S.Last_Element.peek_back_empty(T): 149 {==}