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 ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/deque.bend as S 7 import ../../../src/containers/deque.bend as DQ 8 import ../../../src/containers/types/deque.bend as E 9 import ./state.bend as ST 10 import ./stepok.bend as K 11 import ./rebalance.bend as RB 12 13 # Every public deque operation, including the errors (pop/peek on an empty 14 # deque: Fail{EmptyDeque}, deque unchanged), refines the spec step. 15 16 # the result of reading one end of a readied shadow 17 def Read(~T: Data, sh: ST.Shadow, r: DQ.Deque & E.Obs, spec: List<&2, T> & E.Obs) -> Type: 18 Sigma<&1, &1, ST.Shadow, sh2 => Sigma<&1, &1, E.Obs, o => {r == (ST.real(T, sh2), o) : DQ.Deque & E.Obs} & {(ST.model(T, sh2), o) == spec : List<&2, T> & E.Obs}>> 19 20 def pred1(-T: Data, +x: T, +t: List<&2, T>, +b: List<&2, T>) -> {DQ.DE{t, b, Nat.sub(SC.length(T, Con{x, t}), 1n), SC.length(T, b)} == ST.real(T, ST.Sh{t, b}) : DQ.Deque}: 21 Equal.cong(Nat, DQ.Deque, z => DQ.DE{t, b, z, SC.length(T, b)}, Nat.sub(1n+SC.length(T, t), 1n), SC.length(T, t), N.sub_zero(SC.length(T, t))) 22 23 def pred1b(-T: Data, +f: List<&2, T>, +x: T, +t: List<&2, T>) -> {DQ.DE{f, t, SC.length(T, f), Nat.sub(SC.length(T, Con{x, t}), 1n)} == ST.real(T, ST.Sh{f, t}) : DQ.Deque}: 24 Equal.cong(Nat, DQ.Deque, z => DQ.DE{f, t, SC.length(T, f), z}, Nat.sub(1n+SC.length(T, t), 1n), SC.length(T, t), N.sub_zero(SC.length(T, t))) 25 26 # the model with a nonempty back ends in the back's head 27 def model_back(-T: Data, +f: List<&2, T>, +x: T, +t: List<&2, T>) -> {ST.model(T, ST.Sh{f, Con{x, t}}) == SC.snoc(T, ST.model(T, ST.Sh{f, t}), x) : List<&2, T>}: 28 LL.append_snoc(T, f, SC.reverse(T, t), x) 29 30 def pop_back_snoc(-T: Data, +ys: List<&2, T>, +x: T) -> {S.pop_back(T, SC.snoc(T, ys, x)) == (ys, E.OItem{Done{x}}) : List<&2, T> & E.Obs}: 31 match ys: 32 case Nil{}: 33 {==} 34 case Con{h, t}: 35 %LL.init_snoc(T, Con{h, t}, x) : {S.pop_back(T, SC.snoc(T, Con{h, t}, x)) == (_, E.OItem{Done{x}}) : List<&2, T> & E.Obs} 36 %LL.last_snoc(T, Con{h, t}, x) : {S.pop_back(T, SC.snoc(T, Con{h, t}, x)) == (SC.init(T, SC.snoc(T, Con{h, t}, x)), E.OItem{S.item(T, _)}) : List<&2, T> & E.Obs} 37 {==} 38 39 def pop_front_ready(~T: Data, +sh: ST.Shadow, +hr: {RB.rdy_f(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, sh))), S.pop_front(T, ST.model(T, sh))): 40 match sh: 41 case ST.Sh{Con{x, t}, b}: 42 (ST.Sh{t, b}, (E.OItem{Done{x}}, (Equal.cong(DQ.Deque, DQ.Deque & E.Obs, d => (d, E.OItem{Done{x}}), DQ.DE{t, b, Nat.sub(SC.length(T, Con{x, t}), 1n), SC.length(T, b)}, ST.real(T, ST.Sh{t, b}), pred1(T, x, t, b)), {==}))) 43 case ST.Sh{Nil{}, Nil{}}: 44 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==}))) 45 case ST.Sh{Nil{}, Con{y, t}}: 46 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, ST.Sh{Nil{}, Con{y, t}}))), S.pop_front(T, ST.model(T, ST.Sh{Nil{}, Con{y, t}}))), L.false_true(hr)) 47 48 def peek_front_ready(~T: Data, +sh: ST.Shadow, +hr: {RB.rdy_f(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, sh))), (ST.model(T, sh), E.OItem{S.item(T, SC.head(T, ST.model(T, sh)))})): 49 match sh: 50 case ST.Sh{Con{x, t}, b}: 51 (ST.Sh{Con{x, t}, b}, (E.OItem{Done{x}}, ({==}, {==}))) 52 case ST.Sh{Nil{}, Nil{}}: 53 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==}))) 54 case ST.Sh{Nil{}, Con{y, t}}: 55 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, ST.Sh{Nil{}, Con{y, t}}))), (ST.model(T, ST.Sh{Nil{}, Con{y, t}}), E.OItem{S.item(T, SC.head(T, ST.model(T, ST.Sh{Nil{}, Con{y, t}})))})), L.false_true(hr)) 56 57 def pop_back_ready(~T: Data, +sh: ST.Shadow, +hr: {RB.rdy_b(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, sh))), S.pop_back(T, ST.model(T, sh))): 58 match sh: 59 case ST.Sh{f, Con{x, t}}: 60 +sp = Equal.trans(List<&2, T> & E.Obs, (ST.model(T, ST.Sh{f, t}), E.OItem{Done{x}}), S.pop_back(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), S.pop_back(T, ST.model(T, ST.Sh{f, Con{x, t}})), 61 Equal.sym(List<&2, T> & E.Obs, S.pop_back(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), (ST.model(T, ST.Sh{f, t}), E.OItem{Done{x}}), pop_back_snoc(T, ST.model(T, ST.Sh{f, t}), x)), 62 Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => S.pop_back(T, z), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), ST.model(T, ST.Sh{f, Con{x, t}}), Equal.sym(List<&2, T>, ST.model(T, ST.Sh{f, Con{x, t}}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), model_back(T, f, x, t)))) 63 (ST.Sh{f, t}, (E.OItem{Done{x}}, (Equal.cong(DQ.Deque, DQ.Deque & E.Obs, d => (d, E.OItem{Done{x}}), DQ.DE{f, t, SC.length(T, f), Nat.sub(SC.length(T, Con{x, t}), 1n)}, ST.real(T, ST.Sh{f, t}), pred1b(T, f, x, t)), sp))) 64 case ST.Sh{Nil{}, Nil{}}: 65 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==}))) 66 case ST.Sh{Con{y, t}, Nil{}}: 67 Empty.absurd(Read(~T, ST.Sh{Con{y, t}, Nil{}}, DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, ST.Sh{Con{y, t}, Nil{}}))), S.pop_back(T, ST.model(T, ST.Sh{Con{y, t}, Nil{}}))), L.false_true(hr)) 68 69 def peek_back_ready(~T: Data, +sh: ST.Shadow, +hr: {RB.rdy_b(T, sh) == True{} : Bool}) -> Read(~T, sh, DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, sh))), (ST.model(T, sh), E.OItem{S.item(T, SC.last(T, ST.model(T, sh)))})): 70 match sh: 71 case ST.Sh{f, Con{x, t}}: 72 +sp = Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => (z, E.OItem{S.item(T, SC.last(T, z))}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), ST.model(T, ST.Sh{f, Con{x, t}}), Equal.sym(List<&2, T>, ST.model(T, ST.Sh{f, Con{x, t}}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), model_back(T, f, x, t))) 73 +lx = Equal.cong(Maybe<&2, T>, List<&2, T> & E.Obs, m => (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, m)}), Some{x}, SC.last(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), Equal.sym(Maybe<&2, T>, SC.last(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)), Some{x}, LL.last_snoc(T, ST.model(T, ST.Sh{f, t}), x))) 74 (ST.Sh{f, Con{x, t}}, (E.OItem{Done{x}}, ({==}, Equal.trans(List<&2, T> & E.Obs, (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{Done{x}}), (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, SC.last(T, SC.snoc(T, ST.model(T, ST.Sh{f, t}), x)))}), (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, SC.last(T, ST.model(T, ST.Sh{f, Con{x, t}})))}), lx, 75 Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => (ST.model(T, ST.Sh{f, Con{x, t}}), E.OItem{S.item(T, SC.last(T, z))}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), ST.model(T, ST.Sh{f, Con{x, t}}), Equal.sym(List<&2, T>, ST.model(T, ST.Sh{f, Con{x, t}}), SC.snoc(T, ST.model(T, ST.Sh{f, t}), x), model_back(T, f, x, t))))))) 76 case ST.Sh{Nil{}, Nil{}}: 77 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyDeque{}}}, ({==}, {==}))) 78 case ST.Sh{Con{y, t}, Nil{}}: 79 Empty.absurd(Read(~T, ST.Sh{Con{y, t}, Nil{}}, DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, ST.Sh{Con{y, t}, Nil{}}))), (ST.model(T, ST.Sh{Con{y, t}, Nil{}}), E.OItem{S.item(T, SC.last(T, ST.model(T, ST.Sh{Con{y, t}, Nil{}})))})), L.false_true(hr)) 80 81 # ---- each operation ---- 82 83 def op_length(~T: Data, +sh: ST.Shadow) -> K.StepOK(~T, sh, E.Length{}): 84 match sh: 85 case ST.Sh{+f, +b}: 86 +n = Nat.add(SC.length(T, f), SC.length(T, b)) 87 +el = Equal.trans(Nat, n, Nat.add(SC.length(T, f), SC.length(T, SC.reverse(T, b))), SC.length(T, SC.append(T, f, SC.reverse(T, b))), Equal.cong(Nat, Nat, z => Nat.add(SC.length(T, f), z), SC.length(T, b), SC.length(T, SC.reverse(T, b)), Equal.sym(Nat, SC.length(T, SC.reverse(T, b)), SC.length(T, b), LL.length_rev(T, b))), Equal.sym(Nat, SC.length(T, SC.append(T, f, SC.reverse(T, b))), Nat.add(SC.length(T, f), SC.length(T, SC.reverse(T, b))), LL.length_append(T, f, SC.reverse(T, b)))) 88 K.mk(~T, ST.Sh{f, b}, E.Length{}, ST.Sh{f, b}, E.ONat{n}, {==}, Equal.cong(Nat, List<&2, T> & E.Obs, z => (ST.model(T, ST.Sh{f, b}), E.ONat{z}), n, SC.length(T, ST.model(T, ST.Sh{f, b})), el)) 89 90 def op_push_front(~T: Data, +sh: ST.Shadow, +x: T) -> K.StepOK(~T, sh, E.PushFront{x}): 91 match sh: 92 case ST.Sh{+f, +b}: 93 K.mk(~T, ST.Sh{f, b}, E.PushFront{x}, ST.Sh{Con{x, f}, b}, E.OUnit{}, {==}, {==}) 94 95 def op_push_back(~T: Data, +sh: ST.Shadow, +x: T) -> K.StepOK(~T, sh, E.PushBack{x}): 96 match sh: 97 case ST.Sh{+f, +b}: 98 K.mk(~T, ST.Sh{f, b}, E.PushBack{x}, ST.Sh{f, Con{x, b}}, E.OUnit{}, {==}, Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => (z, E.OUnit{}), ST.model(T, ST.Sh{f, Con{x, b}}), SC.snoc(T, ST.model(T, ST.Sh{f, b}), x), model_back(T, f, x, b))) 99 100 def op_to_list(~T: Data, +sh: ST.Shadow) -> K.StepOK(~T, sh, E.ToList{}): 101 match sh: 102 case ST.Sh{+f, +b}: 103 +el = Equal.trans(List<&2, T>, List.append(&2, T, f, List.reverse(&2, T, b)), List.append(&2, T, f, SC.reverse(T, b)), SC.append(T, f, SC.reverse(T, b)), Equal.cong(List<&2, T>, List<&2, T>, z => List.append(&2, T, f, z), List.reverse(&2, T, b), SC.reverse(T, b), LL.base_rev(T, b)), LL.base_append(T, f, SC.reverse(T, b))) 104 K.mk(~T, ST.Sh{f, b}, E.ToList{}, ST.Sh{f, b}, E.OList{List.append(&2, T, f, List.reverse(&2, T, b))}, {==}, Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => (ST.model(T, ST.Sh{f, b}), E.OList{z}), List.append(&2, T, f, List.reverse(&2, T, b)), ST.model(T, ST.Sh{f, b}), el)) 105 106 def pf_fin(~T: Data, +sh: ST.Shadow, +sh1: ST.Shadow, +e: {DQ.ready_front(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, sh1))), S.pop_front(T, ST.model(T, sh1)))) -> K.StepOK(~T, sh, E.PopFront{}): 107 match rd: 108 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}: 109 K.mk(~T, sh, E.PopFront{}, sh2, o, 110 Equal.trans(DQ.Deque & E.Obs, DQ.obs_item(~T, DQ.pop_front_ready(~T, DQ.ready_front(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.pop_front_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque, DQ.Deque & E.Obs, d => DQ.obs_item(~T, DQ.pop_front_ready(~T, d)), DQ.ready_front(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1), 111 Equal.trans(List<&2, T> & E.Obs, (ST.model(T, sh2), o), S.pop_front(T, ST.model(T, sh1)), S.pop_front(T, ST.model(T, sh)), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => S.pop_front(T, z), ST.model(T, sh1), ST.model(T, sh), em))) 112 113 def pf_rf(~T: Data, +sh: ST.Shadow, rf: RB.RF(~T, sh)) -> K.StepOK(~T, sh, E.PopFront{}): 114 match rf: 115 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}: 116 pf_fin(~T, sh, sh1, e, em, pop_front_ready(~T, sh1, hr)) 117 118 def kf_fin(~T: Data, +sh: ST.Shadow, +sh1: ST.Shadow, +e: {DQ.ready_front(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, sh1))), (ST.model(T, sh1), E.OItem{S.item(T, SC.head(T, ST.model(T, sh1)))}))) -> K.StepOK(~T, sh, E.PeekFront{}): 119 match rd: 120 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}: 121 K.mk(~T, sh, E.PeekFront{}, sh2, o, 122 Equal.trans(DQ.Deque & E.Obs, DQ.obs_item(~T, DQ.peek_front_ready(~T, DQ.ready_front(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.peek_front_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque, DQ.Deque & E.Obs, d => DQ.obs_item(~T, DQ.peek_front_ready(~T, d)), DQ.ready_front(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1), 123 Equal.trans(List<&2, T> & E.Obs, (ST.model(T, sh2), o), (ST.model(T, sh1), E.OItem{S.item(T, SC.head(T, ST.model(T, sh1)))}), (ST.model(T, sh), E.OItem{S.item(T, SC.head(T, ST.model(T, sh)))}), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => (z, E.OItem{S.item(T, SC.head(T, z))}), ST.model(T, sh1), ST.model(T, sh), em))) 124 125 def kf_rf(~T: Data, +sh: ST.Shadow, rf: RB.RF(~T, sh)) -> K.StepOK(~T, sh, E.PeekFront{}): 126 match rf: 127 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}: 128 kf_fin(~T, sh, sh1, e, em, peek_front_ready(~T, sh1, hr)) 129 130 def pb_fin(~T: Data, +sh: ST.Shadow, +sh1: ST.Shadow, +e: {DQ.ready_back(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, sh1))), S.pop_back(T, ST.model(T, sh1)))) -> K.StepOK(~T, sh, E.PopBack{}): 131 match rd: 132 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}: 133 K.mk(~T, sh, E.PopBack{}, sh2, o, 134 Equal.trans(DQ.Deque & E.Obs, DQ.obs_item(~T, DQ.pop_back_ready(~T, DQ.ready_back(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.pop_back_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque, DQ.Deque & E.Obs, d => DQ.obs_item(~T, DQ.pop_back_ready(~T, d)), DQ.ready_back(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1), 135 Equal.trans(List<&2, T> & E.Obs, (ST.model(T, sh2), o), S.pop_back(T, ST.model(T, sh1)), S.pop_back(T, ST.model(T, sh)), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => S.pop_back(T, z), ST.model(T, sh1), ST.model(T, sh), em))) 136 137 def pb_rb(~T: Data, +sh: ST.Shadow, rb: RB.RB(~T, sh)) -> K.StepOK(~T, sh, E.PopBack{}): 138 match rb: 139 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}: 140 pb_fin(~T, sh, sh1, e, em, pop_back_ready(~T, sh1, hr)) 141 142 def kb_fin(~T: Data, +sh: ST.Shadow, +sh1: ST.Shadow, +e: {DQ.ready_back(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, sh1))), (ST.model(T, sh1), E.OItem{S.item(T, SC.last(T, ST.model(T, sh1)))}))) -> K.StepOK(~T, sh, E.PeekBack{}): 143 match rd: 144 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}: 145 K.mk(~T, sh, E.PeekBack{}, sh2, o, 146 Equal.trans(DQ.Deque & E.Obs, DQ.obs_item(~T, DQ.peek_back_ready(~T, DQ.ready_back(~T, ST.real(T, sh)))), DQ.obs_item(~T, DQ.peek_back_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(DQ.Deque, DQ.Deque & E.Obs, d => DQ.obs_item(~T, DQ.peek_back_ready(~T, d)), DQ.ready_back(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1), 147 Equal.trans(List<&2, T> & E.Obs, (ST.model(T, sh2), o), (ST.model(T, sh1), E.OItem{S.item(T, SC.last(T, ST.model(T, sh1)))}), (ST.model(T, sh), E.OItem{S.item(T, SC.last(T, ST.model(T, sh)))}), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => (z, E.OItem{S.item(T, SC.last(T, z))}), ST.model(T, sh1), ST.model(T, sh), em))) 148 149 def kb_rb(~T: Data, +sh: ST.Shadow, rb: RB.RB(~T, sh)) -> K.StepOK(~T, sh, E.PeekBack{}): 150 match rb: 151 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}: 152 kb_fin(~T, sh, sh1, e, em, peek_back_ready(~T, sh1, hr)) 153 154 # every public operation refines the spec step 155 def step_ok(~T: Data, +sh: ST.Shadow, +op: E.Op) -> K.StepOK(~T, sh, op): 156 match op: 157 case E.Length{}: 158 op_length(~T, sh) 159 case E.PushFront{+x}: 160 op_push_front(~T, sh, x) 161 case E.PushBack{+x}: 162 op_push_back(~T, sh, x) 163 case E.PopFront{}: 164 pf_rf(~T, sh, RB.ready_front(~T, sh)) 165 case E.PopBack{}: 166 pb_rb(~T, sh, RB.ready_back(~T, sh)) 167 case E.PeekFront{}: 168 kf_rf(~T, sh, RB.ready_front(~T, sh)) 169 case E.PeekBack{}: 170 kb_rb(~T, sh, RB.ready_back(~T, sh)) 171 case E.ToList{}: 172 op_to_list(~T, sh)