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/queue.bend as S 7 import ../../../src/containers/queue.bend as Q 8 import ../../../src/containers/types/queue.bend as E 9 import ./state.bend as ST 10 11 # Every public queue operation, including the errors (dequeue/peek on an 12 # empty queue: Fail{EmptyQueue}, queue unchanged), refines the spec step. 13 14 def StepOK(~T: Data, sh: ST.Shadow, op: E.Op) -> Type: 15 Sigma<&1, &1, ST.Shadow, sh2 => Sigma<&1, &1, E.Obs, o => {Q.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : Q.Queue & E.Obs} & {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : List<&2, T> & E.Obs}>> 16 17 def mk(~T: Data, -sh: ST.Shadow, -op: E.Op, sh2: ST.Shadow, o: E.Obs, e1: {Q.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : Q.Queue & E.Obs}, e2: {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : List<&2, T> & E.Obs}) -> StepOK(~T, sh, op): 18 (sh2, (o, (e1, e2))) 19 20 # ---- ready: reverse the back into an empty front ---- 21 22 def is_nil(-T: Data, xs: List<&2, T>) -> Bool: 23 match xs: 24 case Nil{}: 25 True{} 26 case Con{h, t}: 27 False{} 28 29 # the front can be read: nonempty, or the queue is empty 30 def rdy(-T: Data, sh: ST.Shadow) -> Bool: 31 match sh: 32 case ST.Sh{Nil{}, b}: 33 is_nil(T, b) 34 case ST.Sh{Con{x, f}, b}: 35 True{} 36 37 def rdy_nil_back(-T: Data, +m: List<&2, T>) -> {rdy(T, ST.Sh{m, Nil{}}) == True{} : Bool}: 38 match m: 39 case Nil{}: 40 {==} 41 case Con{x, t}: 42 {==} 43 44 def Ready(~T: Data, sh: ST.Shadow) -> Type: 45 Sigma<&1, &1, ST.Shadow, sh1 => {Q.ready(~T, ST.real(T, sh)) == ST.real(T, sh1) : Q.Queue} & ({ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>} & {rdy(T, sh1) == True{} : Bool})> 46 47 def ready(~T: Data, +sh: ST.Shadow) -> Ready(~T, sh): 48 match sh: 49 case ST.Sh{Con{x, f}, b}: 50 (ST.Sh{Con{x, f}, b}, ({==}, ({==}, {==}))) 51 case ST.Sh{Nil{}, +b}: 52 +rb = SC.reverse(T, b) 53 +en = Equal.sym(Nat, Nat.add(SC.length(T, rb), 0n), SC.length(T, b), Equal.trans(Nat, Nat.add(SC.length(T, rb), 0n), SC.length(T, rb), SC.length(T, b), N.add_zero(SC.length(T, rb)), LL.length_rev(T, b))) 54 +e1 = Equal.cong(List<&2, T>, Q.Queue, z => Q.QU{z, Nil{}, SC.length(T, b)}, List.reverse(&2, T, b), rb, LL.base_rev(T, b)) 55 +e2 = Equal.cong(Nat, Q.Queue, z => Q.QU{rb, Nil{}, z}, SC.length(T, b), Nat.add(SC.length(T, rb), 0n), en) 56 (ST.Sh{rb, Nil{}}, (Equal.trans(Q.Queue, Q.QU{List.reverse(&2, T, b), Nil{}, SC.length(T, b)}, Q.QU{rb, Nil{}, SC.length(T, b)}, ST.real(T, ST.Sh{rb, Nil{}}), e1, e2), (LL.append_nil(T, rb), rdy_nil_back(T, rb)))) 57 58 # ---- reading the front of a readied shadow ---- 59 60 def Read(~T: Data, sh: ST.Shadow, r: Q.Queue & E.Obs, spec: List<&2, T> & E.Obs) -> Type: 61 Sigma<&1, &1, ST.Shadow, sh2 => Sigma<&1, &1, E.Obs, o => {r == (ST.real(T, sh2), o) : Q.Queue & E.Obs} & {(ST.model(T, sh2), o) == spec : List<&2, T> & E.Obs}>> 62 63 def dequeue_ready(~T: Data, +sh: ST.Shadow, +hr: {rdy(T, sh) == True{} : Bool}) -> Read(~T, sh, Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, sh))), S.dequeue(T, ST.model(T, sh))): 64 match sh: 65 case ST.Sh{Con{+x, +t}, +b}: 66 +e = Equal.cong(Nat, Q.Queue, z => Q.QU{t, b, z}, Nat.sub(Nat.add(SC.length(T, Con{x, t}), SC.length(T, b)), 1n), Nat.add(SC.length(T, t), SC.length(T, b)), N.sub_zero(Nat.add(SC.length(T, t), SC.length(T, b)))) 67 (ST.Sh{t, b}, (E.OItem{Done{x}}, (Equal.cong(Q.Queue, Q.Queue & E.Obs, q => (q, E.OItem{Done{x}}), Q.QU{t, b, Nat.sub(Nat.add(SC.length(T, Con{x, t}), SC.length(T, b)), 1n)}, ST.real(T, ST.Sh{t, b}), e), {==}))) 68 case ST.Sh{Nil{}, Nil{}}: 69 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyQueue{}}}, ({==}, {==}))) 70 case ST.Sh{Nil{}, Con{y, t}}: 71 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, ST.Sh{Nil{}, Con{y, t}}))), S.dequeue(T, ST.model(T, ST.Sh{Nil{}, Con{y, t}}))), L.false_true(hr)) 72 73 def peek_ready(~T: Data, +sh: ST.Shadow, +hr: {rdy(T, sh) == True{} : Bool}) -> Read(~T, sh, Q.obs_item(~T, Q.peek_ready(~T, ST.real(T, sh))), (ST.model(T, sh), E.OItem{S.item(T, SC.head(T, ST.model(T, sh)))})): 74 match sh: 75 case ST.Sh{Con{x, t}, b}: 76 (ST.Sh{Con{x, t}, b}, (E.OItem{Done{x}}, ({==}, {==}))) 77 case ST.Sh{Nil{}, Nil{}}: 78 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyQueue{}}}, ({==}, {==}))) 79 case ST.Sh{Nil{}, Con{y, t}}: 80 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, Q.obs_item(~T, Q.peek_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)) 81 82 def dq_fin(~T: Data, +sh: ST.Shadow, +sh1: ST.Shadow, +e: {Q.ready(~T, ST.real(T, sh)) == ST.real(T, sh1) : Q.Queue}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, sh1))), S.dequeue(T, ST.model(T, sh1)))) -> StepOK(~T, sh, E.Dequeue{}): 83 match rd: 84 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}: 85 mk(~T, sh, E.Dequeue{}, sh2, o, 86 Equal.trans(Q.Queue & E.Obs, Q.obs_item(~T, Q.dequeue_ready(~T, Q.ready(~T, ST.real(T, sh)))), Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(Q.Queue, Q.Queue & E.Obs, d => Q.obs_item(~T, Q.dequeue_ready(~T, d)), Q.ready(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1), 87 Equal.trans(List<&2, T> & E.Obs, (ST.model(T, sh2), o), S.dequeue(T, ST.model(T, sh1)), S.dequeue(T, ST.model(T, sh)), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs, z => S.dequeue(T, z), ST.model(T, sh1), ST.model(T, sh), em))) 88 89 def dq_rd(~T: Data, +sh: ST.Shadow, r: Ready(~T, sh)) -> StepOK(~T, sh, E.Dequeue{}): 90 match r: 91 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}: 92 dq_fin(~T, sh, sh1, e, em, dequeue_ready(~T, sh1, hr)) 93 94 def pk_fin(~T: Data, +sh: ST.Shadow, +sh1: ST.Shadow, +e: {Q.ready(~T, ST.real(T, sh)) == ST.real(T, sh1) : Q.Queue}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, Q.obs_item(~T, Q.peek_ready(~T, ST.real(T, sh1))), (ST.model(T, sh1), E.OItem{S.item(T, SC.head(T, ST.model(T, sh1)))}))) -> StepOK(~T, sh, E.Peek{}): 95 match rd: 96 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}: 97 mk(~T, sh, E.Peek{}, sh2, o, 98 Equal.trans(Q.Queue & E.Obs, Q.obs_item(~T, Q.peek_ready(~T, Q.ready(~T, ST.real(T, sh)))), Q.obs_item(~T, Q.peek_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(Q.Queue, Q.Queue & E.Obs, d => Q.obs_item(~T, Q.peek_ready(~T, d)), Q.ready(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1), 99 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))) 100 101 def pk_rd(~T: Data, +sh: ST.Shadow, r: Ready(~T, sh)) -> StepOK(~T, sh, E.Peek{}): 102 match r: 103 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}: 104 pk_fin(~T, sh, sh1, e, em, peek_ready(~T, sh1, hr)) 105 106 # ---- each operation ---- 107 108 def op_length(~T: Data, +sh: ST.Shadow) -> StepOK(~T, sh, E.Length{}): 109 match sh: 110 case ST.Sh{+f, +b}: 111 +n = Nat.add(SC.length(T, f), SC.length(T, b)) 112 +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)))) 113 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)) 114 115 def op_enqueue(~T: Data, +sh: ST.Shadow, +x: T) -> StepOK(~T, sh, E.Enqueue{x}): 116 match sh: 117 case ST.Sh{+f, +b}: 118 +en = Equal.sym(Nat, Nat.add(SC.length(T, f), 1n+SC.length(T, b)), 1n+Nat.add(SC.length(T, f), SC.length(T, b)), N.add_succ(SC.length(T, f), SC.length(T, b))) 119 +e1 = Equal.cong(Nat, Q.Queue & E.Obs, z => (Q.QU{f, Con{x, b}, z}, E.OUnit{}), 1n+Nat.add(SC.length(T, f), SC.length(T, b)), Nat.add(SC.length(T, f), 1n+SC.length(T, b)), en) 120 mk(~T, ST.Sh{f, b}, E.Enqueue{x}, ST.Sh{f, Con{x, b}}, E.OUnit{}, e1, 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), LL.append_snoc(T, f, SC.reverse(T, b), x))) 121 122 def op_to_list(~T: Data, +sh: ST.Shadow) -> StepOK(~T, sh, E.ToList{}): 123 match sh: 124 case ST.Sh{+f, +b}: 125 +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))) 126 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)) 127 128 # every public operation refines the spec step 129 def step_ok(~T: Data, +sh: ST.Shadow, +op: E.Op) -> StepOK(~T, sh, op): 130 match op: 131 case E.Length{}: 132 op_length(~T, sh) 133 case E.Enqueue{+x}: 134 op_enqueue(~T, sh, x) 135 case E.Dequeue{}: 136 dq_rd(~T, sh, ready(~T, sh)) 137 case E.Peek{}: 138 pk_rd(~T, sh, ready(~T, sh)) 139 case E.ToList{}: 140 op_to_list(~T, sh)