%Patch files loaded: patch2 version 1.2.2.102 $$$sliding_window_liveness.pvs sliding_window_liveness : THEORY BEGIN IMPORTING sliding_window_safety %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % the goal of this theory is to prove the liveness property % main_liveness_property (at the bottom of the file) % The proof is devided in five steps. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % definition of the fair runs: the number of data obtained from % the source grows beyond any bound fair : PRED[(run)] = LAMBDA (r: (run)) : FORALL (m :nat) : EXISTS (n:nat) : r(n)`sourceIndex > m % definition of the live runs: the number of data delivered to % the target grows beyond any bound live : PRED[(run)] = LAMBDA (r: (run)) : FORALL (m :nat) : EXISTS (n:nat) : r(n)`targetIndex > m %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Step 1 : prove that if sourceIndex grows beyond any bound, % so does sndWinIndex. The invariant sndWinIndex = sourceIndex % (already proved in the safety properties) is used. fair_aux_1 : PRED[(run)] = LAMBDA (r: (run)) : FORALL (m :nat) : EXISTS (n:nat) : r(n)`sndWinIndex > m fairness_property_aux_1 : LEMMA FORALL (r:(run)) : fair(r) IMPLIES fair_aux_1(r) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Step 2 : prove that if sndWinIndex grows beyond any bound, % then so does sndLow. The invariant sndWinIndex <= sndLow+sw % is proved and used. fair_aux_2 : PRED[(run)] = LAMBDA (r: (run)) : FORALL (m :nat) : EXISTS (n:nat) : r(n)`sndLow > m %inductive safe_aux_2 : LEMMA invariant (LAMBDA (s:State) : s`sndWinIndex <= s`sndLow + sw) fairness_property_aux_2 : LEMMA FORALL (r:(run)) : fair_aux_1(r) IMPLIES fair_aux_2(r) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Step 3 : prove that if sndLow grows beyond any bound, % then so does rcvLow. The invariant sndLow <= rcvLow % is used. To prove it, one first has to prove FORALL i: % i < headAckChan IMPLIES ackChan(i) < rcvLow. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% fair_aux_3 : PRED[(run)] = LAMBDA (r: (run)) : FORALL (m :nat) : EXISTS (n:nat) : r(n)`rcvLow > m %inductive safe_aux_3bis : LEMMA invariant (LAMBDA (s:State) : FORALL (i:nat) : i < s`headAckChan IMPLIES s`ackChan(i) < s`rcvLow) safe_aux_3 : LEMMA invariant (LAMBDA (s:State): s`sndLow <= s`rcvLow) fairness_property_aux_3 : LEMMA FORALL (r:(run)) : fair_aux_2(r) IMPLIES fair_aux_3(r) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Step 4 : prove that if rcvLow grows beyond any bound, % then so does targetIndex. The invariant rcvLow = targetIndex % (already proved in the safety properties) is used fairness_property_aux_4 : LEMMA FORALL (r:(run)) : fair_aux_3(r) IMPLIES live(r) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Step 5: using lemmas fairness_property_aux_1 to 4, prove % the main safety property. main_fairness_property : THEOREM FORALL (r:(run)) : fair(r) IMPLIES live(r) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% END sliding_window_liveness $$$sliding_window_liveness.prf (|sliding_window_liveness| (|fairness_property_aux_1| "" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (FLATTEN) (("" (EXPAND "fair") (("" (EXPAND "fair_aux_1") (("" (SKOLEM 1 "p") (("" (INST -3 "p") (("" (LEMMA "source_equals_send_1") (("" (EXPAND "invariant") (("" (SKOLEM -4 "n") (("" (INST 1 "n") (("" (INSTANTIATE -1 ("r" "n")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|safe_aux_2| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (BETA) (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fairness_property_aux_2| "" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (FLATTEN) (("" (EXPAND "fair_aux_1") (("" (EXPAND "fair_aux_2") (("" (SKOLEM 1 "p") (("" (LEMMA "safe_aux_2") (("" (INST -4 "p+sw") (("" (SKOLEM -4 "n") (("" (INST 1 "n") (("" (HIDE -3) (("" (EXPAND "run_fragment") (("" (INST -2 "n") (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|safe_aux_3bis| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (BETA) (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|safe_aux_3| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (BETA) (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (GRIND) (("1" (COMMENT "will prove FORALL i: i < headAckChan IMPLIES ackChan(i) < rcvLow") (("1" (LEMMA "safe_aux_3bis") (("1" (GRIND) NIL NIL)) ";;;will prove FORALL i: i < headAckChan IMPLIES ackChan(i) < rcvLow")) NIL) ("2" (COMMENT "will prove FORALL i: i < headAckChan IMPLIES ackChan(i) < rcvLow") (("2" (LEMMA "safe_aux_3bis") (("2" (GRIND) NIL NIL)) ";;;will prove FORALL i: i < headAckChan IMPLIES ackChan(i) < rcvLow")) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fairness_property_aux_3| "" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (FLATTEN) (("" (HIDE -2) (("" (EXPAND "fair_aux_2") (("" (EXPAND "fair_aux_3") (("" (SKOLEM 1 "p") (("" (INST -2 "p") (("" (EXPAND "run_fragment") (("" (SKOLEM -2 "n") (("" (INST -1 "n") (("" (INST 1 "n") (("" (LEMMA "safe_aux_3") (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fairness_property_aux_4| "" (SKOLEM 1 "r") (("" (FLATTEN) (("" (TYPEPRED "r") (("" (HIDE -2) (("" (EXPAND "fair_aux_3") (("" (EXPAND "live") (("" (SKOLEM 1 "p") (("" (INST -2 "p") (("" (EXPAND "run_fragment") (("" (SKOLEM -2 "n") (("" (INST -1 "n") (("" (INST 1 "n") (("" (LEMMA "target_equals_receive") (("" (GRIND) (("1" (LEMMA "target_equals_receive_1") (("1" (GRIND) NIL NIL)) NIL) ("2" (LEMMA "target_equals_receive_1") (("2" (GRIND) NIL NIL)) NIL) ("3" (LEMMA "target_equals_receive_1") (("3" (GRIND) NIL NIL)) NIL) ("4" (LEMMA "target_equals_receive_1") (("4" (GRIND) NIL NIL)) NIL) ("5" (LEMMA "target_equals_receive_1") (("5" (GRIND) NIL NIL)) NIL) ("6" (LEMMA "target_equals_receive_1") (("6" (GRIND) NIL NIL)) NIL) ("7" (LEMMA "target_equals_receive_1") (("7" (GRIND) NIL NIL)) NIL) ("8" (LEMMA "target_equals_receive_1") (("8" (GRIND) NIL NIL)) NIL) ("9" (LEMMA "target_equals_receive_1") (("9" (GRIND) NIL NIL)) NIL) ("10" (LEMMA "target_equals_receive_1") (("10" (GRIND) NIL NIL)) NIL) ("11" (LEMMA "target_equals_receive_1") (("11" (GRIND) NIL NIL)) NIL) ("12" (LEMMA "target_equals_receive_1") (("12" (GRIND) NIL NIL)) NIL) ("13" (LEMMA "target_equals_receive_1") (("13" (GRIND) NIL NIL)) NIL) ("14" (LEMMA "target_equals_receive_1") (("14" (GRIND) NIL NIL)) NIL) ("15" (LEMMA "target_equals_receive_1") (("15" (GRIND) NIL NIL)) NIL) ("16" (LEMMA "target_equals_receive_1") (("16" (GRIND) NIL NIL)) NIL) ("17" (LEMMA "target_equals_receive_1") (("17" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|main_fairness_property| "" (LEMMA "fairness_property_aux_1") (("" (LEMMA "fairness_property_aux_2") (("" (LEMMA "fairness_property_aux_3") (("" (LEMMA "fairness_property_aux_4") (("" (SKOLEM 1 "r") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$runs.pvs runs[State : TYPE, initial : PRED[State], transition : [State, State -> bool]] : THEORY BEGIN %runs are infinite sequences of transition-related states, starting in an initial state run_fragment: pred[sequence[State]] = {r : sequence[State] | FORALL (n : nat): transition(r(n),r(n+1))} run : pred[(run_fragment)] = {r : (run_fragment) | initial(r(0))} r: VAR (run) p :VAR pred[State] invariant(p) : bool = FORALL (r : (run), n:nat ): p(r(n)) invariant_rule : LEMMA (FORALL (r : (run)) : p(r(0)) AND FORALL (n : nat) : p(r(n)) IMPLIES p(r(n+1))) IMPLIES invariant(p) END runs $$$runs.prf (|runs| (|invariant_rule| "" (SKOSIMP*) (("" (EXPAND "invariant") (("" (INDUCT-AND-SIMPLIFY "n") NIL NIL)) NIL)) NIL)) $$$Action.pvs Action : Theory BEGIN Data : TYPE = int Absent: int = -1 GoodData : TYPE = nat Ack: TYPE = int GoodAck : TYPE = nat Msg: TYPE = [#data: GoodData, index: nat #] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %declarations for the actions of the sliding window% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Action : DATATYPE BEGIN GET(d: GoodData) : GET? %get message m from data source SEND_MSG(m:Msg) : SEND_MSG? %send a message to the message channel RCV_ACK(a:Ack) :RCV_ACK? % receive ack from ack channel */ TIMEOUT : TIMEOUT? %sender receives a timeout after having send all messages in window */ RCV_MSG(m:Msg) : RCV_MSG? %receiver gets message from the message channel PUT(d: Data) : PUT? %deliver data d to the data destination SEND_ACK(a: Ack): SEND_ACK? %sender gets ack from ack channel LOSE_MSG: LOSE_MSG? LOSE_ACK : LOSE_ACK? END Action END Action $$$Action.prf (|Action| (|Absent_TCC1| "" (EXISTENCE-TCC)) (|notAbsent_TCC1| "" (LEMMA "GoodData_axiom") (("" (PROPAX) NIL NIL)) NIL)) $$$sliding_window.pvs %font-lock-mode %font-lock-fontify-buffer sliding_window: THEORY BEGIN IMPORTING Action sw : posnat % sender's window size rw : posnat % receiver's window size rcvControlType : TYPE = {receiving, flushing, sendingAck} State : TYPE = [# % variables for the data source source: [nat-> GoodData], sourceIndex : nat, % sender's variables sndWindow: [nat-> GoodData], sndLow, % bottom of sender's window sndWinIndex, % counts data received from data source sndIndex: nat, % counts data sent to message channel % receiver's variables rcvControl : rcvControlType, %controls what actions are allowed rcvWindow : [nat-> Data], %receiver's window rcvLow, % bottom of receiver's window % message channel headMsgChan, tailMsgChan : nat, msgChan : [nat->Msg], % ack channel headAckChan, tailAckChan : nat, ackChan : [nat->Ack], % data target target :[nat->Data], targetIndex : nat, % to distinguish actually reachable states actual : boolean #] %the initial states initial : setof[State] = {s: State | s`sndWinIndex = 0 AND s`sndIndex = 0 AND s`sndLow = 0 AND s`rcvLow = 0 AND s`rcvControl = receiving AND (FORALL (n: nat): s`rcvWindow(n) = Absent) AND s`headMsgChan = 0 AND s`tailMsgChan = 0 AND s`headAckChan = 0 AND s`tailAckChan = 0 AND s`sourceIndex = 0 AND s`targetIndex =0} % transition relation next(s: State, a: Action) : State = CASES a OF % sender's actions % obtain a data item from the data source, save it in the sender's window % (if there is space left) GET(d) : IF s`sndWinIndex < s`sndLow + sw AND d = s`source(s`sourceIndex) THEN s WITH [sndWindow := s`sndWindow WITH[(s`sndWinIndex) := d], sndWinIndex := s`sndWinIndex+1, sourceIndex := s`sourceIndex+1] ELSE s WITH [actual := false] ENDIF, %create a message with the next data item, send it on the message channel % a timer is started with each message (not explicitly modeled in this action) SEND_MSG(m): IF s`sndIndex < s`sndWinIndex AND m`data = s`sndWindow(s`sndIndex) AND m`index = s`sndIndex THEN s WITH [msgChan:= s`msgChan WITH [(s`headMsgChan):= m], headMsgChan := s`headMsgChan+1, sndIndex:= s`sndIndex+1] ELSE s WITH [actual := false] ENDIF, % if the timer has expired and there is no other action possible % (i.e., sender's window is full and all data has been sent to % message channel and no acknowledgments available), start resending % from current bottom of sender's window TIMEOUT: IF s`sndIndex = s`sndWinIndex AND s`sndWinIndex = s`sndLow +sw AND s`headAckChan = s`tailAckChan THEN s WITH [sndIndex := s`sndLow] ELSE s WITH [actual := false] ENDIF, %receive an acknowledgment from the acknowledgment channel (if available) % If it is in the range between bottom of sender's window and current top % of sender's window, set the bottom to the value of the ack+1, and modify the % index sndIndex (of the next data to be sent) to (max between itself % and the value of the ack)+1. This means that an ack also acknowledges all % messages before itself. RCV_ACK(a): IF s`headAckChan > s`tailAckChan AND a = s`ackChan(s`tailAckChan) THEN IF a >= s`sndLow AND a < s`sndWinIndex THEN s WITH[sndLow := a+1, sndIndex := (IF a > s`sndIndex THEN a ELSE s`sndIndex ENDIF)+1, tailAckChan := s`tailAckChan+1] ELSE s WITH[tailAckChan := s`tailAckChan+1] ENDIF ELSE s WITH [actual := false] ENDIF, % receiver's actions % receive a message from the message channel. The control has to allow %it (i.e., rcvControl = receiving), and there has to be a message in the %channel. If its index is in the current window of the receiver, it %is stored at the right position. RCV_MSG(m): IF s`rcvControl = receiving AND s`headMsgChan > s`tailMsgChan AND m = s`msgChan(s`tailMsgChan) THEN IF(m`index >= s`rcvLow AND m`index < s`rcvLow + rw) THEN s WITH[rcvWindow := s`rcvWindow WITH[(m`index) := m`data], tailMsgChan := s`tailMsgChan+1] ELSE s WITH [tailMsgChan := s`tailMsgChan+1] ENDIF ELSE s WITH [actual := false] ENDIF, % sending an item of data to the data target ("flushing" the receiver window). % The flushing starts ih the bottom of the receiver window contains an % actual item of data (not Absent), and continues until the first Absent data is met. % The rcvControl tag is used to control this process: % at the beginning, rcvControl = receiving, and if the bottom of the receiver % window contains an actual piece of data (not Absent), then control switches % to rcvControl = flushing. There, it stays until an Absent data is met, and % when this happens it goes to sending_ack, preparing for the last actual data % that was flushed to be acknowledged. However, if initially (when rcvControl = % receiving) the bottom of the receiver window contains Absent, then the state % is left unchanged. PUT(d) : IF (s`rcvControl = receiving OR s`rcvControl = flushing) AND d = s`rcvWindow(s`rcvLow) THEN IF d /= Absent THEN s WITH[rcvControl := flushing, target := s`target WITH[(s`targetIndex):= d], targetIndex:= s`targetIndex+1,rcvLow := s`rcvLow+1] ELSIF s`rcvControl =flushing THEN s WITH [rcvControl := sendingAck] ELSE s ENDIF ELSE s WITH [actual := false] ENDIF, %the last piece of data that was flushed to the data target is acknowledged, %then control goes back to receiving SEND_ACK(a): IF s`rcvControl = sendingAck AND a = s`rcvLow-1 THEN s WITH[ackChan := s`ackChan WITH[(s`headAckChan) := a], headAckChan := s`headAckChan+1, rcvControl := receiving] ELSE s WITH [actual := false] ENDIF, %environment's actions % lose a message, if any LOSE_MSG: IF s`headMsgChan > s`tailMsgChan THEN s WITH [tailMsgChan:= s`tailMsgChan+1] ELSE s WITH [actual := false] ENDIF, %lose an acknowledgment, if any LOSE_ACK: IF s`headAckChan > s`tailAckChan THEN s WITH [tailAckChan:= s`tailAckChan+1] ELSE s WITH [actual := false] ENDIF ENDCASES IMPORTING runs[State, initial, LAMBDA(s,s_: State): EXISTS (a: Action): s`actual AND s_`actual AND s_ = next(s,a)] END sliding_window $$$sliding_window.prf (|sliding_window| (|next_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|next_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|next_TCC3| "" (SUBTYPE-TCC) NIL NIL)) $$$sliding_window_safety.pvs sliding_window_safety : THEORY BEGIN IMPORTING sliding_window %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % the goal of this theory is to prove the safety property % main_safety_property (at the bottom of the file) % the proof is decomposed into five steps. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % step 1: proving that, up to the index sndWinIndex, the % data source and sender window are equal. %inductive source_equals_send_1 : LEMMA invariant(LAMBDA (s: State) : s`sndWinIndex = s`sourceIndex) %inductive in the context of source_equals_send_1 source_equals_send : LEMMA invariant(LAMBDA (s: State) : FORALL (i : nat) : i < s`sndWinIndex IMPLIES s`source(i) = s`sndWindow(i)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % step 2: proving that, up to the index rcvLow, the data % target and receiver window are equal. This is expressed % by lemma target_equals_receive. %inductive target_equals_receive_1 : LEMMA invariant(LAMBDA (s: State) : s`targetIndex = s`rcvLow) %inductive in the contex of target_equals_receive_1 target_equals_receive : LEMMA invariant(LAMBDA (s: State) : FORALL (i : nat) : i < s`rcvLow IMPLIES s`target(i) = s`rcvWindow(i)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % step 3: in order to make use of lemmas target_equals_receive and % source_equals_send, we need to prove that rcvLow <= sndWinIndex. % This is expressed as lemma rcvLow_leq_sndWinIndex. The other % lemmas are intermediary steps towards that result. They are % all suggested by a failure of the basic invariant-proving % strategy applied to some other (following) lemma. Some of the % results proved here are also useful in Step 4. rcvLow_leq_sndWinIndex_2: %inductive LEMMA invariant(LAMBDA(s: State) : FORALL (i: nat) : i < s`headMsgChan IMPLIES s`msgChan(i)`index < s`sndWinIndex) rcvLow_leq_sndWinIndex_1 : LEMMA invariant(LAMBDA(s: State) : FORALL (i:nat) : i >= s`sndWinIndex IMPLIES s`rcvWindow(i) = Absent) rcvLow_leq_sndWinIndex : LEMMA invariant(LAMBDA(s: State) : s`rcvLow <= s`sndWinIndex) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % step 4: prove that, up to rcvLow, the sender and receiver % windows coincide. This is expressed as lemma send_equals_receive. % All other lemmas are intermediary steps towards that result. They % are suggested by a failure of the basic invariant-proving % strategy applied to some other (following) lemma. send_equals_receive_2 : LEMMA invariant(LAMBDA(s: State): FORALL (i: nat) : i < s`headMsgChan IMPLIES s`msgChan(i)`data = s`sndWindow(s`msgChan(i)`index)) send_equals_receive_1 : LEMMA invariant(LAMBDA(s: State): FORALL (i: nat) : (i>= s`rcvLow AND s`rcvWindow(i) /= Absent) IMPLIES s`rcvWindow(i) = s`sndWindow(i)) send_equals_receive : LEMMA invariant(LAMBDA(s: State): FORALL (i : nat) : (i < s`rcvLow IMPLIES s`sndWindow(i) = s`rcvWindow(i))) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % step 5: using the lemmas proved in steps 1-4, prove the %main safety property. main_safety_property : THEOREM invariant(LAMBDA(s: State): FORALL (i : nat) : (i < s`rcvLow IMPLIES s`target(i) = s`source(i))) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% END sliding_window_safety $$$sliding_window_safety.prf (|sliding_window_safety| (|source_equals_send_1| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (BETA) (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|source_equals_send| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (BETA) (("2" (FLATTEN) (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) (("1" (COMMENT "suggests to prove sndWinIndex = sourceIndex") (("1" (LEMMA "source_equals_send_1") (("1" (GRIND) NIL NIL)) ";;;suggests to prove sndWinIndex = sourceIndex")) NIL) ("2" (LEMMA "source_equals_send_1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|target_equals_receive_1| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (BETA) (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|target_equals_receive| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (BETA) (("2" (FLATTEN) (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) (("1" (COMMENT "suggests to prove targetIndex = rcvLow") (("1" (LEMMA "target_equals_receive_1") (("1" (GRIND) NIL NIL)) ";;;suggests to prove targetIndex = rcvLow")) NIL) ("2" (COMMENT "suggests to prove targetIndex = rcvLow") (("2" (LEMMA "target_equals_receive_1") (("2" (GRIND) NIL NIL)) ";;;suggests to prove targetIndex = rcvLow")) NIL) ("3" (COMMENT "suggests to prove targetIndex = rcvLow") (("3" (LEMMA "target_equals_receive_1") (("3" (GRIND) NIL NIL)) ";;;suggests to prove targetIndex = rcvLow")) NIL) ("4" (COMMENT "suggests to prove targetIndex = rcvLow") (("4" (LEMMA "target_equals_receive_1") (("4" (GRIND) NIL NIL)) ";;;suggests to prove targetIndex = rcvLow")) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rcvLow_leq_sndWinIndex_2| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (BETA) (("2" (FLATTEN) (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rcvLow_leq_sndWinIndex_1| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (BETA) (("1" (EXPAND "run") (("1" (EXPAND "initial") (("1" (SKOLEM 1 "i") (("1" (GROUND) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM 1 "n") (("2" (HIDE -2) (("2" (FLATTEN) (("2" (BETA) (("2" (EXPAND "run_fragment") (("2" (INST -2 "n") (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) (("2" (COMMENT "will prove FORALL (i: nat) : i < headMsgChan IMPLIES msgChan(i)`index < sndWinIndex)") (("2" (LEMMA "rcvLow_leq_sndWinIndex_2") (("2" (GRIND) NIL NIL)) ";;;will prove FORALL (i: nat) : i < headMsgChan IMPLIES ;;;msgChan(i)`index < sndWinIndex)")) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rcvLow_leq_sndWinIndex| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (BETA) (("2" (GRIND) (("1" (COMMENT "suggests to prove FORALL (i:nat) : i >= sndWinIndex IMPLIES rcvWindow(i) = Absent") (("1" (LEMMA "rcvLow_leq_sndWinIndex_1") (("1" (GRIND) NIL NIL)) ";;;suggests to prove FORALL (i:nat) : i >= sndWinIndex IMPLIES ;;; rcvWindow(i) = Absent")) NIL) ("2" (LEMMA "rcvLow_leq_sndWinIndex_1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|send_equals_receive_2| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (BETA) (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) (("2" (COMMENT "suggests to prove FORALL i < headMsgChan msgChan(i)`index < sndWinIndex") (("2" (LEMMA "rcvLow_leq_sndWinIndex_2") (("2" (GRIND) NIL NIL)) ";;;suggests to prove FORALL i < headMsgChan msgChan(i)`index < sndWinIndex")) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|send_equals_receive_1| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (BETA) (("1" (EXPAND "run") (("1" (EXPAND "initial") (("1" (SKOLEM 1 "i") (("1" (GROUND) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM 1 "n") (("2" (HIDE -2) (("2" (FLATTEN) (("2" (BETA) (("2" (EXPAND "run_fragment") (("2" (INST -2 "n") (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) (("1" (COMMENT "suggests to prove rcvWindow(sndWinIndex) = Absent") (("1" (LEMMA "rcvLow_leq_sndWinIndex_1") (("1" (GRIND) NIL NIL)) ";;;suggests to prove rcvWindow(sndWinIndex) = Absent")) NIL) ("2" (COMMENT "will prove FORALL (j: nat) : j < headMsgChan IMPLIES msgChan(j)`data = sndWindow(msgChan(j)`index)") (("2" (LEMMA "send_equals_receive_2") (("2" (GRIND) NIL NIL)) ";;;will prove FORALL (j: nat) : j < headMsgChan IMPLIES msgChan(j)`data = sndWindow(msgChan(j)`index)")) NIL) ("3" (LEMMA "send_equals_receive_2") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|send_equals_receive| "" (LEMMA "invariant_rule") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOLEM 1 "r") (("" (TYPEPRED "r") (("" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (BETA) (("2" (SKOLEM 1 "i") (("2" (INST -1 "i") (("2" (GRIND) (("1" (COMMENT "will prove rcvLow <= sndWinIndex") (("1" (LEMMA "rcvLow_leq_sndWinIndex") (("1" (GRIND) NIL NIL)) ";;;will prove rcvLow <= sndWinIndex")) NIL) ("2" (COMMENT "suggests to prove FORALL (i: nat) : (i>= rcvLow AND rcvWindow(i) /= Absent) IMPLIES rcvWindow(i) = sndWindow(i))") (("2" (LEMMA "send_equals_receive_1") (("2" (GRIND) NIL NIL)) ";;;suggests to prove FORALL (i: nat) : ;;; (i>= rcvLow AND rcvWindow(i) /= Absent) IMPLIES rcvWindow(i) = sndWindow(i))")) NIL) ("3" (LEMMA "send_equals_receive_1") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|main_safety_property| "" (LEMMA "send_equals_receive") (("" (LEMMA "source_equals_send") (("" (LEMMA "target_equals_receive") (("" (LEMMA "rcvLow_leq_sndWinIndex") (("" (EXPAND "invariant") (("" (SKOLEM 1 ("r" "n")) (("" (INSTANTIATE -1 ("r" "n")) (("" (INSTANTIATE -2 ("r" "n")) (("" (INSTANTIATE -3 ("r" "n")) (("" (INSTANTIATE -4 ("r" "n")) (("" (FLATTEN) (("" (SKOLEM 1 "i") (("" (INST?) (("" (INST?) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))