HOL CASE STUDY

The Specification and Verification of a

Sliding Window Protocol

Author

Rachel Cardell-Oliver Computer Laboratory Corn Exchange Street Cambridge CB2 3QG, UK. Telephone: +44 223 334733

Email: rco@cl.cam.ac.uk

Concepts illustrated

Communication protocol specification and verification

Prerequisites

Good working knowledge of HOL and some experience using the HOL system. Some familiarity with the built in tactics and the theories of lists and arithmetic. Ability to tackle proofs using steps containing several tactics.

Supporting files

On the directory hol/Training/studies/protocols.

Abstract

This case study describes the specification and verification of a sliding window protocol. It presents some ideas about modelling software systems with HOL and a feel for the work involved in performing a medium sized verification proof in HOL.

Contents

1 Introduction 3 2 Files 3 3 Informal specification 4 4 Specification 7 5 Verification 13

5.1 Safety theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 5.2 Liveness theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.3 Total correctness theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

6 References 36 A Supporting theories 37

A Sliding Window Protocol

1 Introduction

The following document describes the specification and verification of a sliding window protocol in HOL. It is proved that a model for implementations of the protocol logically implies safety and liveness invariants and that these invariants in turn imply an abstract specification of the protocol. The specification states that a sequence of data is transferred from one computer in a network to another after some elapsed time. The implementation model is an interpretation of the behaviour, over time, of the variables of a Pascal program for a sliding window protocol. Real time is modelled explicitly. This means that timeouts, channel delays, response times and retransmission limits can be expressed directly and real protocol implementations can be modelled. All levels of the protocol model and proof are expressed in higher order logic, and proofs are checked by the HOL proof assistant.

I shall first describe the files used in this case study and then informally describe the sliding window protocol which is verified in this example. The specification and verification of this sliding window protocol in HOL is then described, following the order in which definitions and theorems are introduced when building this theory. The theorems were actually developed in a different order, usually starting from the theorems at the end of each section which were proved by assuming any supporting theorems. This process was continued, top down, until no assumed theorems remained to be proved. Of course, there was also a lot of sideways development (that is rewriting definitions and theorems) since the problems of modelling protocols at this level of detail were new to me, and I was also learning to use HOL at the same time. I changed aspects of the protocol’s specification and the organization of the proof several times during the development stages. Details of the development of this proof may be found in Reference [2]. Reference [1] is an introductory text book on computer networks which includes a section on sliding window protocols.

2 Files

The case study is supported by the files in the directory protocols in the HOL distribution directory. These files are :

READ-ME
casestudy.tex sect1.tex  sect2.tex sect3.tex appendix.tex
casestudy.dvi
SWnew.ml SW.th
hdi_tli.ml plusm_subm.ml int.ml mod.ml da.ml
hdi_tli.th plusm_subm.th int.th mod.th da.th

arith.ml arith.th myarith.ml myarith.th
tacticsSW.ml mytactics.ml
startSW.ml restartSW.ml tydefsSW.ml
MakeSW MakeEverything

The file READ-ME contains this explanation. The .tex files are needed to print the case study document which appears in printable form in casestudy.dvi. SWnew.ml contains the HOL sessions from the case study document and SW.th contains a copy of the theory which is created by executing SWnew.ml.

The remaining .ml and .th files support the main sliding window protocol theory which will be described later. MakeSW automatically performs the HOL session described in the case study, and MakeEverything rebuilds the complete supporting theory as well. MakeEverything should not be used if it can be avoided, as the sessions involved will take a very long time.

3 Informal specification

A sliding window protocol is a concurrent program for transferring an ordered stream of data from one computer in a network to another via an unreliable channel. There is a large family of such protocols of which the protocol described here, called the go-back-n sliding window protocol, is one example.

At the highest level of specification the family of sliding window protocols may be represented by an input stream of data, called the source, and an output stream, the sink. The protocol itself is a black box which effects the transfer of data from source to sink.

source

SLIDING WINDOW PROTOCOL

sink

The input stream, source, is available on one computer and the output sequence, sink, is eventually produced on another computer. The sink data list is dynamic since it will not be available until some time after the protocol has begun. It is modelled as a function from time to finite output data lists. Time starts at time 0 and extends infinitely into the future in discrete time steps. Thus sink(t) refers to the value of the ouput sequence, sink, at time t where t ≥ 0. The source data list is static: its value is determined outside the protocol model and never changed by the model. source is modelled as a finite list of data messages. The specification for a sliding window protocol using these variables is

∃t : time. sink(t) = source

This specification encapsulates the total correctness of the protocol. That is, it says that the protocol program will terminate and, on termination, will satisfy its specification. In this case, termination means reaching a stable state. Properties stating that progress will be made are called liveness properties. Properties which are always satisfied by the system are called safety properties or system invariants.

The implementation of a sliding window protocol is described by the structure and behaviour of the black box, SLIDING WINDOW PROTOCOL, of the specification. A sliding window protocol uses three physical devices: SENDER and RECEIVER computer programs running concurrently on different computers in a network, and a CHANNEL, a physical wire, between the computers. The channel provides the only means of communication between the two computers. The implementation structure of a sliding window protocol can be represented by

[figure: source; SENDER; CHANNEL; RECEIVER; sink]

The CHANNEL device provides unreliable message delivery. Messages may be correctly delivered, detectably garbled or lost completely. To reliably transmit data in such an environment, the SENDER takes a window or buffer of messages from the source stream and transmits each message with a unique label. The RECEIVER accepts these messages and outputs them to the sink in their original order. The original order of the messages must be deduced from their labels. The RECEIVER also sends messages, called acknowledgements, to the SENDER expressing the current state of the RECEIVER in terms of which messages it has received. The SENDER uses the information contained in the acknowledgements to retransmit any messages which may not have been received. This process continues until all the messages from the source have been received and output to the sink.

An example of the sort of program code which would be used for the SENDER and RECEIVER programs of this sliding window protocol is given in Figure 1. The code is written in a language like Pascal. The HOL specification verified in this case study is an informal translation of the program code of Figure 1. However, the HOL specification is more general than the code in that it describes a family of protocols. For example, window size is a parameter of the HOL specification, so the alternating bit protocol (with window size 1) and the HDLC protocol (with window size 7 or 127) are both described by the HOL model. Also, the sender’s retransmission strategy is not fully specified in the HOL model so a range of protocols using different strategies are possible.

The protocol model presented in this case study is based on a number of simplistic assumptions. For example, it is assumed that the time taken to deliver a message (channel delay) is 0 and that the receiver does not buffer any received packets. These restrictions are removed in [3].

program SENDER;                            program RECEIVER;
{external variables}                       {external variables}
  source : input list of data                sink  : output list of data
  ackS   : input from channel via ackR       ackR  : output to channel
  dataS  : output to channel                 dataR : input from channel via dataS
const maxseq = 8; {for example}             {constants and types as SENDER}
      SW = 7;     {SENDER window}             RW = 1;     {RECEIVER window}
type data = num;    {or char or integer or record etc.}
     sequence = [0..maxseq-1]  {message labels}
var rem : list of data;                    var r : sequence;
    s, stop, i: sequence;                      dummy : data;
begin                                      begin
  rem:=source;                               sink:=[];
  s:=0;                                      r:=0;
  while not(NULL rem) do begin               while TRUE do begin
{receive ack packet}                       {receive data packet}
    RECV( ackS ) ;                            RECV( dataR ) ;
    if IN_WINDOW(ackS,s,SW,maxseq)            if IN_WINDOW(dataR,r,RW,maxseq)
    then begin                                then begin
      stop:=(label(ackS)+1) MOD maxseq;
      while s<>stop do begin
        rem:=tail(rem);                         sink:=append(sink, dataR);
        s:= (s+1) MOD maxseq;                   r:= (r+1) MOD maxseq;
      end; {while}
    end {if};                                 end {if};
{transmit data}                            {transmit ack}
    i:=choosei(SW);
    dataS:=((s+i) MOD maxseq,                ackR:=((r-1) MOD maxseq, dummy);
            headi(i,rem));
    SEND( dataS )                            SEND( ackR )
  end {while};                               end {while};
end {program}.                              end {program}.

Figure 1: Pascal Programs for a Sliding Window Protocol

CHANNEL (ack)

ABORT

SENDER

DataTrans s rem

AckRecv RECEIVER

DataRecv r

AckTrans INIT

CHANNEL (data)

source = rem 0

sink

[figure]

dataS dataR

[figure] [figure]

ackS ackR

[figure] [figure] [figure]

Figure 2: HOL Sliding Window Protocol Model

4 Specification

This case study describes the definitions and theorems needed to build a complete sliding window protocol theory. The files needed to do this are in the directory:

    hol/Training/studies/protocols.

All the input commands which are given in boxes can be found in the file SWnew.ml. To work through this case study in HOL edit the file SWnew.ml while running HOL and read through this document, entering commands as they appear in the text.

To build the sliding window protocol theory, first enter HOL and set up the sliding window theory :

1

 loadf`startSW`;;

This command will open a new theory and load its parent theories. The parent theories for this sliding window protocol theory are, myarith which contains some necessary arithmetic theorems, plusm_subm which contains a theory of modular arithmetic and hdi_tli which contains definitions and theorems for operations on sections of lists. A summary of the theories hdi_tli and plusm_subm can be found in Appendix A.

The structure of the HOL model to be specified is illustrated in Figure 2. The boxes in the diagram represent HOL predicates and the arrows represent the flow of information or data in the system.

To describe this model in HOL we must first define some types. Enter the following definitions in HOL :

2

let  time = ":num"
and  data = ":*"
and  sequence = ":num"
and  non_packet = ":one" ;;
let  packet = ":(^sequence # ^data) + ^non_packet" ;;
let  channel = ":^time -> ^packet" ;;
let  seqtime = ":^time->^sequence" ;;
let  datatime = ":^time->^data list" ;;

The packet type is made up of either a sequence number, data message pair, or a nonpacket which represents a message lost or garbled by the channel or a time at which no message is being transmitted. The following operators are used for creating, reading and writing variables of the packet type.

3

let set_non_packet = new_definition(
  `set_non_packet`,
  "set_non_packet:^packet = INR(one)");;
let good_packet = new_definition(
 `good_packet`,
  "good_packet (p:^packet) = (ISL p)");;
let new_packet = new_definition(
 `new_packet`,
 "(new_packet (ss:^sequence) (dd:^data)):^packet = (INL(ss,dd))");;
let label = new_definition(
 `label`,
 "label (p:^packet) = FST(OUTL p)");;
let message = new_definition(
 `message`,
 "message (p:^packet) = SND(OUTL p)");;

The INIT predicate describes the initial values of the main program variables and a condition for the range of sequence numbers, maxseq.

4

let INIT = new_definition(
  `INIT`,
  "INIT (source:^data list) (maxseq:^sequence)
        (rem :^datatime)  (s:^seqtime)
        (sink:^datatime)  (r:^seqtime)  =
   ( ( 1 < maxseq )    /\
     (rem 0 = source)  /\  (s 0 = 0) /\
     (sink 0 = NIL)    /\  (r 0 = 0))");;

A channel is modelled by two streams, one for packets input to the channel and one for those output by the channel over time. The relationship between the two streams at any instant of time is that the packet on the output stream is either a copy of the packet on the input stream or is a non-packet. The assumption that packets can be output in the same time granule in which they are input is unrealistic and eventually a channel model including message delivery delay will be used instead.

5

 let CHANNEL = new_definition(
    `CHANNEL`,
    "CHANNEL (inC:^channel) (outC:^channel) =
       (!t:^time. (outC t = inC t) \/ (outC t = set_non_packet))" );;

The predicate DATA_TRANS represents the data transmission parts of the SENDER program. Any packet from the SENDER window is chosen for transmission. The sender’s window consists of the first SW elements of (rem t). The message chosen is the i-th element of rem, HDI (i t) (rem t), for (i t) < SW. Its sequence number is

                         plusm(s t, i t, maxseq)

where s t is the true sequence number of the first element of rem t. The functions plusm and subm perform addition and subtraction modulo maxseq. The choice function, p, guarantees that i t is within the window and that there are at least i t data messages available in rem t. If p t is false then a non-packet is transmitted instead. With the intention of making this implementation model as general as possible, only the minimum information needed about p, its type, is given at this stage. Later, different implementations can be defined by more fully defining such parameters. The conjunct ~(NULL rem t) is included in DATA_TRANS so that, after all data has been transmitted, non-packets are transmitted forever. That is, the program never exits, but the protocol will reach a stable state once transmission of source data has been completed.

6

  let DATA_TRANS = new_definition(
    `DATA_TRANS`,
    "DATA_TRANS
       (rem:^datatime) (s:^seqtime) (SW:^sequence)
       (maxseq:^sequence)
       (p:^time->^sequence->bool) (i:^seqtime)
       (dataS:^channel) =
       ( (SW = (maxseq-1)) /\
       (!t:^time.
         ( ((p t (i t)) ==>
               ((~NULL(TLI (i t) (rem t))) /\ ((i t) < SW) )) /\
            ( ((p t (i t)) /\ ~(NULL(rem t)))
                    => (dataS t = new_packet
                                    (plusm(s t,i t,maxseq))
                                    (HDI (i t) (rem t)) )
                    |  (dataS t = set_non_packet ) ) ))) ");;

For any packet, p, (IN_WINDOW p b ws maxseq) tests whether p is within the sender or receiver’s window by testing whether label p is less than window-size, ws, sequence numbers from the bottom edge of the window, b.

7

 let IN_WINDOW = new_definition(
   `IN_WINDOW`,
   "IN_WINDOW (p:^packet) (b:^sequence) (ws:^sequence) (maxseq:^sequence) =
     ( (good_packet p) /\
       ( subm(label p,b,maxseq) < ws ) )");;

The predicate DATA_RECV represents the part of RECEIVER program which accepts incoming packets and outputs them to the sink if necessary. This particular predicate uses a receiver window size of one which means only packets which can be output immediately are accepted. If the incoming packet, dataR t is acceptable, then its message part is appended to the sink list, otherwise DATA_RECV makes no changes.

8

 let DATA_RECV = new_definition(
   `DATA_RECV`,
   "DATA_RECV (dataR:^channel)
              (RW:^sequence) (maxseq:^sequence)
              (sink:^datatime) (r:^seqtime)  =
   ( (RW = 1) /\
     (!t:^time.
       (IN_WINDOW (dataR t) (r t) RW maxseq )
           => ( (r (t+1) = plusm(r t,1,maxseq)) /\
                (sink (t+1) = (APPEND (sink t) [message(dataR t)] ) ))
           |  ( (r (t+1) = (r t)) /\
                (sink (t+1) = (sink t)) )))" );;

The RECEIVER program is also required to transmit information about its current state to the SENDER in the form of acknowledgement packets. The variables updated in DATA_RECV are used in the next acknowledgement packet. Since r is the value of the next sequence number expected, the acknowledgement sequence is one less than r to represent the sequence number of the last message correctly received. This strategy is chosen so that the model generalizes for all window sizes from one upwards. The boolean function q is like p in DATA_TRANS. An acknowledgement packet is only transmitted at times when q t is true. The data field of an acknowledgement packet is never used, and can be filled with any dummy data message.

9

  let ACK_TRANS = new_definition(
    `ACK_TRANS`,
    "ACK_TRANS (r:^seqtime)
               (maxseq:^sequence)
               (q:^time->bool)
               (ackR:^channel) =
     ( !t:^time. !dummy:^data.
       ( (q t) => (ackR t = new_packet (subm((r t),1,maxseq)) dummy )
               |  (ackR t = set_non_packet) ) )");;

Acknowledgement packets received by the SENDER program are checked by ACK_RECV. If the acknowledgement represents the correct reception of a packet within the SENDER’s window then a new window is chosen starting from the first packet from the source stream which is as yet unacknowledged. That is, the sequence number s t represents the sender’s knowledge of the latest message correctly delivered to the sink. The first message not known to be correctly delivered has sequence number s t.

10

 let ACK_RECV = new_definition(
    `ACK_RECV`,
    "ACK_RECV (ackS:^channel)
              (SW:^sequence)
              (maxseq:^sequence)
              (rem:^datatime)
              (s:^seqtime) =
     (!t:^time.
         (IN_WINDOW (ackS t) (s t) SW maxseq)
            => ( (s (t+1) = plusm(label(ackS t),1,maxseq) ) /\
                 (rem (t+1) =
                      (TLI (subm (plusm(label(ackS t),1,maxseq),s t,maxseq))
                           (rem t)) ) )
            |  ( (s (t+1) = (s t)) /\
                 (rem (t+1) = (rem t)) ) )");;

The SENDER predicate contains all those sections of the above specification which would be part of the sender program in an implementation. The conjunction of predicates represents their concurrent execution (this is an abstraction of their real sequential execution).

11

 let SENDER = new_definition(
   `SENDER`,
   "SENDER (maxseq:^sequence)
           (SW:^sequence)
           (rem:^datatime)
           (s:^seqtime)
           (p:^time->^sequence->bool) (i:^seqtime)
           (dataS:^channel)
           (ackS:^channel) =
     ( (DATA_TRANS rem s SW maxseq p i dataS) /\
       (ACK_RECV ackS SW maxseq rem s) )");;

The liveness, or progress, of the sliding window protocol is monitored by the ABORT predicate which would also be part of the sender’s program code in an implementation. This predicate counts the lengths of times during which no valid acknowledgement arrives. If any such waiting period exceeds maxT then aborted is set to true and remains so. Such a specification of liveness is called real-time liveness and is based on the solution used in most implementations. It is up to the program which is using the protocol to decide what action to take when the aborted signal has been set. The aborted variable is used in the verification of liveness because it can be proved that the protocol will eventually deliver all its data as long as aborted remains false. Note that aborted will be always false once all the source data, contained in rem, has been delivered. Throughout this specification termination is represented by a predicate reaching and remaining in a stable state rather than actually exiting a program.

12

let ABORT = new_definition(
`ABORT`,
"ABORT (c:^time->num) (aborted:^time->bool) (maxT:num)
       (maxseq:^sequence) (SW:^sequence)
       (s:^seqtime) (rem:^datatime) (ackS:^channel) =
  (!t:^time.
    (c 0 = 0 ) /\
    (c (t+1) = ( (IN_WINDOW (ackS t) (s t) SW maxseq) => 0 | ((c t)+1) )) /\
    (aborted 0 = F) /\
    (aborted(t+1) = (((c t >= maxT) \/ (aborted t)) /\ ~(NULL(rem t)))))");;

The RECEIVER predicate, like SENDER, represents all the functions of the receiver program of an implementation.

13

let RECEIVER = new_definition(
`RECEIVER`,
"RECEIVER (maxseq:^sequence)
          (RW:^sequence)
          (sink:^datatime)
          (r:^seqtime)
          (q:^time->bool)
          (ackR:^channel)
          (dataR:^channel) =
  ( (ACK_TRANS r maxseq q ackR) /\
    (DATA_RECV dataR RW maxseq sink r) )");;

Finally, all the implementation predicates described above are included in a single predicate, IMPL. A sliding window protocol implementation is a system satisfying the behaviour of each of its parts.

14

let IMPL = new_definition(
`IMPL`,
"IMPL (source:^data list)
      (maxseq:^sequence)
      (rem:^datatime)  (s:^seqtime) (SW:^sequence)
      (p:^time->^sequence->bool) (i:^seqtime)
      (c:^time->num) (aborted:^time->bool) (maxT:num)
      (sink:^datatime) (r:^seqtime) (RW:^sequence)
      (q:^time->bool)
      (dataS:^channel) (dataR:^channel) (ackS:^channel) (ackR:^channel) =
( (INIT source maxseq rem s sink r) /\
  (SENDER maxseq SW rem s p i dataS ackS) /\
  (ABORT c aborted maxT maxseq SW s rem ackS) /\
  (CHANNEL dataS dataR) /\
  (RECEIVER maxseq RW sink r q ackR dataR) /\
  (CHANNEL ackR ackS) )");;

5 Verification

This section presents the proofs that the implementation described in the last section satisfies its total correctness specification. Executing this session in HOL will create the complete sliding window theory. Because the number of proofs in the theory is reasonably large, some of the proof steps have been saved in a set of tactics which are stored in the file tacticsSW.ml. Load these tactic files first.

15

 loadf`tacticsSW`;;

Alternatively, if you have been working on these proofs earlier and wish to return to the latest state, start HOL and load the following file, which will set up the new session.

16

 loadf`restartSW`;;

The first theorem to be proved states that the receiver’s sequence counter is always less than maxseq. It will be used in the proofs of theorems involving plusm, subm and the receiver’s sequence counter, r.

17

 g("!source:^data list. !maxseq:^sequence.
    !rem:^datatime.  !s:^seqtime.
    !sink:^datatime. !r:^seqtime. !RW:^sequence.
    !dataR:^channel.
   (INIT source maxseq rem s sink r) /\
   (DATA_RECV dataR RW maxseq sink r)
  ==>
   ( !t:^time. (r t) < maxseq )");;

The first step of the proof is to expand the definitions INIT and DATA_RECV and to include the conclusion of the theorem ONE_LESS_0_LESS |- !m. 1 < m ==> 0 < m in the assumption list. These steps are combined in tactic2. An edited version of the result of executing tactic2 is shown below. To save space “… ” are used to indicate parts of the assumption list which have not been shown.

18

 #expand tactic2;;
 OK..
 "!t. (r t) < maxseq"
   ...
     [ "r 0 = 0" ]
   ...
     [ "!t.
         (IN_WINDOW(dataR t)(r t)RW maxseq =>
          ((r(t + 1) = plusm(r t,1,maxseq)) /\
           (sink(t + 1) = APPEND(sink t)[message(dataR t)])) |
          ((r(t + 1) = r t) /\ (sink(t + 1) = sink t)))" ]
     [ "0 < maxseq" ]

This goal is solved using induction. The basis case is proved by rewriting with the assumption (r 0 = 0). The induction step examines the two cases for the value of r(t+1) given by the second assumption of the above list. In addition to these assumptions, a specialization of the theorem plusm_less_m is used :

|- 0 < maxseq ==> (plusm(r t,1,maxseq)) < maxseq

These steps, contained in tactic3, complete the proof. The newly proved theorem is then saved in the theory.

19

 expand tactic3;;
 let r_in_range = save_top_thm `r_in_range`;;

Expanding the definition of INIT is all that is needed to prove the next theorem.

20

 let INIT_maxseq_1 =
 prove_thm(
   `INIT_maxseq_1`,
   "!source:^data list. !maxseq:^sequence.
    !rem sink :^datatime.  !s r :^seqtime.
   (INIT source maxseq rem s sink r) ==> (1 < maxseq)",
   REWRITE_TAC[INIT] THEN REPEAT STRIP_TAC THEN
   FIRST_ASSUM ACCEPT_TAC );;

In the next theorem, it is shown that INIT also implies that 0 < maxseq, since we know

1 < maxseq. Use INIT_maxseq_1 to show 1<maxseq, then resolve with ONE_LESS_0_LESS.

The last result satisfies the original goal and completes the proof.

21

 let INIT_maxseq_0 = prove_thm(
   `INIT_maxseq_0`,
   "!source:^data list. !maxseq:^sequence.
    !rem sink :^datatime.  !s r :^seqtime.
    (INIT source maxseq rem s sink r) ==> (0 < maxseq)",
    REPEAT STRIP_TAC THEN IMP_RES_TAC INIT_maxseq_1 THEN
    IMP_RES_TAC ONE_LESS_0_LESS );;

5.1 Safety theorems

The lemma Lemma1A states that if a non-garbled packet is received at any time then it must be a copy of the packet input to the channel at that time.

22

 g("!inC outC :^channel. !t:^time.
    (CHANNEL inC outC) /\
     good_packet (outC t)
  ==>
    ( (outC t) = (inC t) )");;

The proof is set up using tactic5 which expands the CHANNEL definition and strips the goal.

23

#expand tactic5;;
OK..
"outC t = inC t"
    [ "!t. (outC t = inC t) \/ (outC t = set_non_packet)" ]
    [ "good_packet(outC t)" ]

We perform cases on the disjunctive assumption (after specializing !t).

24

#expand( POP_ASSUM MP_TAC THEN POP_ASSUM(DISJ_CASES_TAC o SPEC_ALL));;
OK..
2 subgoals
"outC t = inC t"
    [ "!t. (outC t = inC t) \/ (outC t = set_non_packet)" ]
    [ "good_packet(outC t)" ]
    [ "outC t = set_non_packet" ]
"outC t = inC t"
    [ "!t. (outC t = inC t) \/ (outC t = set_non_packet)" ]
    [ "good_packet(outC t)" ]
    [ "outC t = inC t" ]

It can now be seen that the first goal (the lowest one above), can be solved since the first assumption is the same as the goal. In the second goal, the assumption that outC t is a good packet contradicts the assumption outC t = set_non_packet. Undischarging the former and rewriting with assumptions and definitions yields a theorem of the form |- F ==> term which is true for any term, term. This completes the proof of the goal in box 22 which is saved as Lemma1A.

25

expand( ASM_REWRITE_TAC[] );;
expand( ASM_REWRITE_TAC [good_packet;set_non_packet;ISL]);;
let Lemma1A = save_top_thm`Lemma1A`;;

Lemma1 gives the label values of acknowledgements received by the sender.

26

g("!r s :^seqtime.
   !q:^time->bool. !SW maxseq :^sequence.
   !ackS ackR :^channel.
   !t:^time.
     ACK_TRANS r maxseq q ackR /\
     CHANNEL ackR ackS /\
     IN_WINDOW (ackS t) (s t) SW maxseq
    ==>
     (label(ackS t) = subm(r t,1,maxseq))" );;

The definition of ACK_TRANS contains a conditional statement for assigning values to ackR t. This proof analyses each of these cases. The first case states that a good acknowledgement was transmitted, and second that a non-packet was transmitted. The cases are set up by tactic6 which expands the definition of IN_WINDOW so as to resolve with Lemma1A and then expands the definition of ACK_TRANS and breaks the main goal into two goals, one for each case.

27

 #expand(tactic6 Lemma1A);;
 OK..
 2 subgoals
 "label(ackS t) = subm(r t,1,maxseq)"
  ...
     [ "good_packet(ackS t)" ]
  ...
     [ "ackS t = ackR t" ]
  ...
     [ "ackR t = set_non_packet" ]

 "label(ackS t) = subm(r t,1,maxseq)"
   ...
     [ "ackS t = ackR t" ]
   ...
     [ "ackR t = new_packet(subm(r t,1,maxseq))dummy" ]

The first of these goals can be solved by rewriting with the assumptions and with definitions. The second case is solved by contradiction.

28

 expand( ASM_REWRITE_TAC[label;new_packet;OUTL;FST] );;
 expand(
       UNDISCH_TAC "good_packet((ackS:^channel) t)" THEN
       ASM_REWRITE_TAC[good_packet;set_non_packet;ISL] );;
 let Lemma1 = save_top_thm`Lemma1`;;

The following lemmas, 2A,2B,2C and 2, relate the contents of data packets received by the receiver, through DATA_RECV, to the sender’s and receiver’s sequence numbers.

The sender’s view of the values which are transmitted in its data packets is expressed in Lemma2A. This lemma will be used later with Lemma1A to prove properties of data packets received by DATA_RECV.

29

 g("!dataS:^channel.
    !maxseq:^sequence. !s:^seqtime.
    !p:^time->^sequence->bool. !i:^seqtime. !rem:^datatime.
    !t:^time.
    (DATA_TRANS rem s SW maxseq p i dataS) /\
     good_packet(dataS t) /\
     (0 < maxseq)
   ==>
    ((label(dataS t) = plusm(s t,i t,maxseq)) /\
     (message(dataS t) = (HDI (i t) (rem t))) /\
     ( ((i t)+1) < maxseq ) /\
     ( ~NULL(TLI (i t) (rem t)) ) )" );;

The first step in the proof is to break down the goal into the two cases for dataS t values in DATA_TRANS. This step is performed by tactic7.

30

 expand tactic7;;

The parts of the goal which concern the values of the label and message of a packet are solved by rewriting using the following tactic.

31

 #expand( ASM_REWRITE_TAC[label;new_packet;OUTL;FST;message;SND] );;
 OK..
 "((i t) + 1) < maxseq /\ ~NULL(TLI(i t)(rem t))"
     [ "SW = maxseq - 1" ]
 ...
     [ "0 < maxseq" ]
     [ "p t(i t) ==> ~NULL(TLI(i t)(rem t)) /\ (i t) < SW" ]
 ...
     [ "p t(i t) /\ ~NULL(rem t)" ]
 ...

The remaining goal can be solved by extracting the conclusion of the second assumption from the bottom in the list above and using the assumption SW = maxseq - 1 and the theorem

PRE_LESS_LESS_SUC = |- !i m. i < (m - 1) /\ 0 < m ==> (i + 1) < m

to deduce that ((i t) + 1) < maxseq). The steps are performed by tactic8 which completes the first case of the proof.

32

 expand tactic8;;

To complete the proof, prove that transmitting and receiving a non-packet contradicts the assumption that dataS t is a good packet as before. The proved theorem is saved as

Lemma2A.

33

expand(
  UNDISCH_TAC "good_packet ((dataS:^channel) t)" THEN
  ASM_REWRITE_TAC [good_packet;set_non_packet;ISL] );;
let Lemma2A = save_top_thm`Lemma2A`;;

Lemma2B shows that, for a window size of 1, packets are only accepted if the difference between the incoming sequence number and the base marker for the window is zero.

34

g("!dataR:^channel.
  !r:^seqtime. !RW:^sequence. !maxseq:^sequence.
  !t:^time.
     ((IN_WINDOW (dataR t) (r t) RW maxseq) /\ (RW=1))
    ==>
     ( subm(label(dataR t),r t,maxseq) = 0 )");;

The proof involves expanding the definition of IN_WINDOW and then showing that if the difference between the label of dataR t and r t is less than RW, which is 1, then the difference must be equal to 0. This is a specialization of the theorem

less_than_one_is_0 = |- !a. a < 1 = (a = 0)

The theorem is proved by tactic10 and saved as Lemma2B.

35

expand tactic10 ;;
let Lemma2B = save_top_thm `Lemma2B`;;

The relationship between the window markers of the sender and receiver when the receiver accepts a packet is expressed by Lemma2C.

36

g("!dataR dataS :^channel.
   !maxseq  SW  RW :^sequence.
   !rem sink :^datatime. !s r :^seqtime.
   !p:^time->^sequence->bool. !i:^seqtime.
   !t:^time.
  ( (DATA_TRANS rem s SW maxseq p i dataS ) /\
    (CHANNEL dataS dataR) /\
    (RW=1) /\
    (IN_WINDOW (dataR t) (r t) RW maxseq) /\
    ( 0 < maxseq ) )
  ==>
    ( i t = (subm(r t,s t,maxseq)) )" );;

First move all assumptions to the assumption list and resolve with Lemma2B.

37

expand( REPEAT STRIP_TAC THEN
        IMP_RES_TAC Lemma2B THEN
        POP_ASSUM MP_TAC);;

Then use tactic11A and tactic11B which expand the goal and its assumption list using the results of Lemma1A and Lemma2B.

38

#expand( tactic11A Lemma1A THEN tactic11B Lemma2A );;
OK..
"(subm(plusm(s t,i t,maxseq),r t,maxseq) = 0) ==>
 (i t = subm(r t,s t,maxseq))"
...
    [ "0 < maxseq" ]
...
    [ "(i t) < maxseq" ]

The final goal and its assumptions match the theorem change_sides from the theory

plusm_subm.
change_sides = |- !a b c m.
  b < m /\ 0 < m /\ (subm(plusm(a,b,m),c,m) = 0) ==> (b = subm(c,a,m))

Resolving the assumptions with this lemma proves the theorem which is then saved in the theory.

39

expand(
  DISCH_TAC THEN
  IMP_RES_TAC (SPECL
      ["(s:^seqtime) t";"(i:^seqtime) t";"(r:^seqtime) t";"maxseq:num"]
      change_sides) );;
let Lemma2C = save_top_thm`Lemma2C`;;

Lemma2 combines the results of lemmas 1A, 2A and 2C to express the relationship between data messages received by DATA_RECV and those transmitted by DATA_TRANS.

40

g("!dataR dataS :^channel.
   !maxseq SW RW :^sequence.
   !rem sink :^datatime. !s r :^seqtime.
   !p:^time->^sequence->bool. !i:^seqtime.
   !t:^time.
  ( (DATA_TRANS rem s SW maxseq p i dataS ) /\
    (CHANNEL dataS dataR) /\
    (RW=1) /\
    (IN_WINDOW (dataR t) (r t) RW maxseq) /\
    ( 0 < maxseq ) )
  ==>
  ( ((HDI (subm(r t,s t,maxseq)) (rem t)) = message(dataR t) ) /\
    (~NULL(TLI (subm(r t,s t,maxseq)) (rem t))) /\
     ( (subm(r t,s t,maxseq)+1) < maxseq) )" );;

To prove this lemma use tactic12 to strip the goal and add the conclusions of Lemma1A, Lemma2A and Lemma2C to the assumption list. Rewriting with this assumption list proves the goal which is then saved as Lemma2.

41

expand (tactic12 Lemma1A Lemma2A Lemma2C);;
let Lemma2 = save_top_thm`Lemma2`;;

Lemmas 3 and 4 state the results of all earlier lemmas in a form suitable for the case analysis which will be performed in the proof of the SAFETY_THM

42

g("!source:^data list. !rem sink:^datatime.
 !SW:^sequence. !maxseq:^sequence.
 !s r:^seqtime.  !q:^time->bool.
 !ackS ackR dataR:^channel.
    ACK_TRANS r maxseq q ackR /\
    CHANNEL ackR ackS /\
    ACK_RECV ackS SW maxseq rem s /\
    INIT source maxseq rem s sink r /\
    DATA_RECV dataR RW maxseq sink r
   ==>
    (!t:^time.
      (IN_WINDOW(ackS t)(s t)SW maxseq =>
         ((s(t + 1) = r t) /\
          (rem(t + 1) = TLI(subm(r t,s t,maxseq))(rem t))) |
         ((s(t + 1) = s t) /\ (rem(t + 1) = rem t))))" );;

The proof uses the results of some earlier lemmas, INIT_maxseq_0 and r_in_range and then rewrites the definition of ACK_RECV with the results of Lemma1, saving the theorem as Lemma3.

43

expand(
REPEAT STRIP_TAC THEN IMP_RES_TAC INIT_maxseq_0 THEN
IMP_RES_TAC r_in_range THEN
POP_ASSUM (ASSUME_TAC o SPEC_ALL) THEN
IMP_RES_TAC (SPECL ["(r:^seqtime) t";"1";"maxseq:num"] plusm_subm) THEN
UNDISCH_TAC "ACK_RECV (ackS:^channel) SW maxseq rem s" THEN
REWRITE_TAC[ACK_RECV] THEN REPEAT STRIP_TAC THEN
POP_ASSUM (MP_TAC o SPEC_ALL) THEN COND_CASES_TAC
  REPEAT STRIP_TAC THEN IMP_RES_TAC Lemma1 THEN ASM_REWRITE_TAC[]);;
let Lemma3=save_top_thm`Lemma3`;;

Lemma4 is similar to Lemma3. It rewrites the definition of ACK_RECV using Lemma2.

44

g("!dataR dataS:^channel.
!maxseq:^sequence.  !source:^data list.
!rem sink:^datatime. !s r:^seqtime. !SW RW:^sequence.
!p:^time->^sequence->bool. !i:^seqtime.
  INIT source maxseq rem s sink r  /\
  DATA_TRANS rem s SW maxseq p i dataS  /\
  CHANNEL dataS dataR  /\
  DATA_RECV dataR RW maxseq sink r
==>
(!t:^time.
  (IN_WINDOW (dataR t) (r t) RW maxseq)
    => ((r(t+1)=plusm(r t,1,maxseq)) /\
        (sink(t+1)=
         (APPEND (sink t) [HDI (subm(r t,s t,maxseq)) (rem t)])) /\
        (~NULL(TLI (subm(r t,s t,maxseq)) (rem t))) /\
        ( (subm(r t,s t,maxseq)+1) < maxseq) )
    |  ((r(t+1)=(r t)) /\
        (sink(t+1)=(sink t)) ))" );;

45

expand(
REPEAT STRIP_TAC THEN IMP_RES_TAC INIT_maxseq_0 THEN
UNDISCH_TAC "DATA_RECV (dataR:^channel) RW maxseq sink r" THEN
REWRITE_TAC[DATA_RECV] THEN DISCH_TAC THEN POP_ASSUM STRIP_ASSUME_TAC THEN
POP_ASSUM (MP_TAC o SPEC_ALL) THEN
COND_CASES_TAC THEN
  REPEAT STRIP_TAC THEN IMP_RES_TAC Lemma2 THEN ASM_REWRITE_TAC[]);;
let Lemma4 =save_top_thm`Lemma4`;;

All the lemmas required to prove the main safety theorem are now in place. The idea of the safety proof is quite straightforward: the required invariant is proved by induction over time. The base case can be proved by rewriting with the initial values given in INIT. The induction step is proved by analysing the cases for updated variables which have been set up in Lemma3 and Lemma4. The goal of the SAFETY_THM is :

46

g("!source:^data list. !maxseq:^sequence.
 !rem:^datatime.  !s:^seqtime. !SW:^sequence.
 !p:^time->^sequence->bool. !i:^seqtime.
 !c:^time->num. !aborted:^time->bool. !maxT:num.
 !sink:^datatime. !r:^seqtime. !RW:^sequence. !q:^time->bool.
 !dataS dataR ackS ackR:^channel.
 (IMPL source maxseq rem s SW p i c aborted maxT sink r RW q
      dataS dataR ackS ackR)
==>
 ( !t:^time.
    ( (APPEND (sink t) (TLI (subm(r t,s t,maxseq)) (rem t))) = source) )");;

The proof is begun by setting up the induction as usual and expanding the definitions

of IMPL, SENDER and RECEIVER using tactic15.

47

 #expand( tactic15 [IMPL;SENDER;RECEIVER] );;
 OK..
 2 subgoals
 "APPEND(sink(SUC t))(TLI(subm(r(SUC t),s(SUC t),maxseq))(rem(SUC t))) =
  source"
 ...
     [ "APPEND(sink t)(TLI(subm(r t,s t,maxseq))(rem t)) = source" ]

 "APPEND(sink 0)(TLI(subm(r 0,s 0,maxseq))(rem 0)) = source"
     [ "INIT source maxseq rem s sink r" ]
 ...

The base case is solved by the list of tactics below. The first task is to resolve with the

theorems INIT_maxseq_0 and

subm_self = |- !m. 0 < m ==> (!r. subm(r,r,m) = 0)

from the theory plusm_subm. Next, specialize subm_self using maxseq for m. Then expand the definition of INIT. Rewrite the goal with these assumptions and the basis cases of the recursive list definition APPEND [] l = l and the primitive recursive definition TLI 0 l = l. These steps prove the basis case of the SAFETY_THM.

48

 expand(
    IMP_RES_TAC INIT_maxseq_0 THEN
    IMP_RES_TAC (SPEC "maxseq:num" subm_self) THEN
    UNDISCH_TAC "INIT (source:^data list) maxseq rem s sink r" THEN
    REWRITE_TAC[INIT] THEN REPEAT STRIP_TAC THEN
    ASM_REWRITE_TAC[APPEND;TLI] );;

The cases for the induction step are now set up. We use MP_TAC instead of IMP_RES_TAC to avoid an explosion of theorems on the assumption list.

49

 #expand( MP_TAC (SPEC_ALL Lemma3) THEN ASM_REWRITE_TAC[] THEN
         DISCH_TAC THEN POP_ASSUM (MP_TAC o SPEC_ALL) THEN
         COND_CASES_TAC THEN REPEAT STRIP_TAC );;

50

#expand( MP_TAC (SPEC_ALL Lemma4) THEN ASM_REWRITE_TAC[] THEN
        DISCH_TAC THEN POP_ASSUM (MP_TAC o SPEC_ALL) THEN
        COND_CASES_TAC THEN REPEAT STRIP_TAC );;
OK..
...
"APPEND(sink(SUC t))(TLI(subm(r(SUC t),s(SUC t),maxseq))(rem(SUC t))) =
 source"
...
    [ "IN_WINDOW(ackS t)(s t)SW maxseq" ]
    [ "(s(t + 1) = r t) /\
       (rem(t + 1) = TLI(subm(r t,s t,maxseq))(rem t))" ]
...
    [ "IN_WINDOW(dataR t)(r t)RW maxseq" ]
    [ "(r(t + 1) = plusm(r t,1,maxseq)) /\
       (sink(t + 1) = APPEND(sink t)[HDI(subm(r t,s t,maxseq))(rem t)]) /\
       ~NULL(TLI(subm(r t,s t,maxseq))(rem t)) /\
       ((subm(r t,s t,maxseq)) + 1) < maxseq" ]
 To show that (subm(plusm(r t,1,maxseq),r t,maxseq))=1 use a specialisation of

the theorem plus_1_sub which states

   |- 1 < maxseq ==> (subm(plusm(r t,1,maxseq),r t,maxseq) = 1)

51

#expand(
  IMP_RES_TAC INIT_maxseq_1 THEN
  IMP_RES_TAC (SPECL ["(r:^seqtime) t";"maxseq:num"] plus_1_sub) THEN
  ASM_REWRITE_TAC[ADD1] );;
OK..
"APPEND
 (APPEND(sink t)[HDI(subm(r t,s t,maxseq))(rem t)])
 (TLI 1(TLI(subm(r t,s t,maxseq))(rem t))) =
 source"
...
    [ "~NULL(TLI(subm(r t,s t,maxseq))(rem t))" ]
...

Two theorems from the hdi_tli theory (see Appendix A) are used to finish the proof. The first

HDI_TLI_2 = |- !x y l. TLI x(TLI y l) = TLI(x + y) l

is used to rewrite the goal in a form suitable for rewriting with the conclusion of the second theorem,

HDI_TLI_1 =
  |- !x l. ~NULL(TLI x l) ==> (APPEND[HDI x l](TLI(x + 1)l) = TLI x l)

The rewriting is completed using associativity of the list APPEND operation.

52

expand(
  IMP_RES_TAC HDI_TLI_1 THEN
  POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [ADD_SYM]) THEN
  ASM_REWRITE_TAC[(SYM (SPEC_ALL APPEND_ASSOC));HDI_TLI_2]);;

This concludes the proof for the first case. In the second case, rewriting with the assumption list yields :

53

#expand( ASM_REWRITE_TAC[ADD1] );;
OK..
"APPEND
 (sink t)
 (TLI(subm(r t,r t,maxseq))(TLI(subm(r t,s t,maxseq))(rem t))) =
 source"
...

This goal can be solved with the theorem

subm_self = |- !m. 0 < m ==> (!r. subm(r,r,m) = 0)

and the base case for TLI, which is TLI 0 l = l.

54

expand(
  IMP_RES_TAC INIT_maxseq_0 THEN
  IMP_RES_TAC (SPEC "maxseq:num" subm_self) THEN
  POP_ASSUM (ASSUME_TAC o SPEC "(r:^seqtime) t") THEN
  ASM_REWRITE_TAC[ADD1; TLI ] );;

Set up the second half of the proof in the same way as the first.

55

#expand( MP_TAC (SPEC_ALL Lemma4) THEN ASM_REWRITE_TAC[] THEN
        DISCH_TAC THEN POP_ASSUM (MP_TAC o SPEC_ALL) THEN
        COND_CASES_TAC THEN REPEAT STRIP_TAC );;
OK..
"APPEND
 (APPEND(sink t)[HDI(subm(r t,s t,maxseq))(rem t)])
 (TLI(subm(plusm(r t,1,maxseq),s t,maxseq))(rem t)) =
 source"
...

It can be seen that it is necessary to show

subm(plusm(r t,1,maxseq),s t,maxseq)) = 1 + subm(r t,s t,maxseq)

and then use the theorem HDI_TLI_2 as in the first case of the proof. The theorem

plusm_eq_plus =
   |- !a b m. 0 < m /\ (a + b) < m ==> (plusm(a,b,m) = a + b)

will be used for the former task. The tactics which prove this are contained in tactic16.

56

#expand( tactic16 INIT_maxseq_0 r_in_range );;
OK..
goal proved
...
Previous subproof:
"APPEND(sink(SUC t))(TLI(subm(r(SUC t),s(SUC t),maxseq))(rem(SUC t))) =
 source"
...
    [ "(s(t + 1) = s t) /\ (rem(t + 1) = rem t)" ]
...
    [ "(r(t + 1) = r t) /\ (sink(t + 1) = sink t)" ]

It can be seen from the last result that the final case can be proved by simply rewriting with the assumption list and ADD1. The completed theorem is saved in SAFETY_THM.

57

expand( ASM_REWRITE_TAC[ADD1] );;
let SAFETY_THM = save_top_thm`SAFETY_THM`;;

5.2 Liveness theorems

These theorems form the second set of those needed to prove the total correctness of this sliding window protocol implementation. First, a theorem which extracts the necessary predicates from the IMPL definition and one which extracts the size of the sender’s sliding window are proved by rewriting with the obvious definitions using tactic17 and tactic18.

58

let IMPL_LIVE_PARTS =
prove_thm(
  `IMPL_LIVE_PARTS`,
  "!source:^data list. !maxseq SW RW :^sequence.
   !rem sink :^datatime.  !s r :^seqtime.
   !p:^time->^sequence->bool. !i:^seqtime. !q:^time->bool.
   !c:^time->num. !aborted:^time->bool. !maxT:num.
   !dataS dataR ackS ackR :^channel.
  (IMPL source maxseq rem s SW p i c aborted maxT sink r RW q
        dataS dataR ackS ackR)
  ==>
  ((INIT source maxseq rem s sink r ) /\
   (SENDER maxseq SW rem s p i dataS ackS ) /\
   (ABORT c aborted maxT maxseq SW s rem ackS))" ,
 tactic17 );;

59

let SW_value =
prove_thm(
`SW_value`,
"!rem:^datatime. !s:^seqtime. !SW maxseq:^sequence.
!p:^time->^sequence->bool. !i:^seqtime.
!dataS:^channel.
( DATA_TRANS rem s SW maxseq p i dataS ) ==> ( SW = maxseq-1 )",
tactic18 );;

The lemma Liveness_1 states that for any time, t, the list of messages remaining to be transmitted at time t+1, (rem t+1), is either the same as in the last time interval, (rem t), or is entirely contained by the tail of the last list. That is, there has either been progress made towards the termination of the protocol (when (rem t)=NIL) or there has been no progress. In the first case the abort counter will be reset to 0 and in the second case the value of the abort counter is incremented by 1.

60

g("!maxseq:^sequence.
!rem sink:^datatime.  !s r:^seqtime. !SW :^sequence.
!c:^time->num. !aborted:^time->bool. !maxT:num.
!p:^time->^sequence->bool. !i:^seqtime.
!ackS dataS :^channel.
!source:^data list.
(INIT source maxseq rem s sink r ) /\
(SENDER maxseq SW rem s p i dataS ackS ) /\
(ABORT c aborted maxT maxseq SW s rem ackS)
==>
!t:^time.
  ( (?x:num. ( rem(t+1) = (TLI x (rem t))) /\ (0<x)) /\ (c(t+1)=0) ) \/
    (( rem(t+1) = (rem t) ) /\ (c(t+1)=((c t)+1)) )");;

To prove this goal, use tactic19 to strip the goal as usual and perform case analysis on the sender’s actions when it receives an acknowledgement packet.

61

 #expand tactic19;;
 OK..
 2 subgoals
 ...
 "(?x. (rem(t + 1) = TLI x(rem t)) /\ 0 < x) /\ (c(t + 1) = 0) \/
  (rem(t + 1) = rem t) /\ (c(t + 1) = (c t) + 1)"
 ...
     [ "!t.
         (c 0 = 0) /\
         (c(t + 1) = (IN_WINDOW(ackS t)(s t)SW maxseq => 0 | (c t) + 1)) /\
         ~aborted 0 /\
         (aborted(t + 1) = ((c t) >= maxT \/ aborted t) /\ ~NULL(rem t))" ]
     [ "IN_WINDOW(ackS t)(s t)SW maxseq" ]
     [ "(s(t + 1) = plusm(label(ackS t),1,maxseq)) /\
        (rem(t + 1) =
         TLI(subm(plusm(label(ackS t),1,maxseq),s t,maxseq))(rem t))" ]

We choose to prove the first disjunct of the current goal.

62

 #expand( DISJ1_TAC THEN ASM_REWRITE_TAC[]);;

Now choose a value of x which will satisfy the goal. It can be seen that a suitable choice for x is,

   SUC(subm(label((ackS:^channel) t),s t,maxseq))

Some rewriting using the following theorems is performed by tactic20 to make the value for rem t+1 in the first assumption match this choice of x in the goal. The main theorems used in tactic20 are:

subm_plusm =
    |- !m. 0 < m ==>
           (!a b c. subm(plusm(a,b,m),c,m) = plusm(subm(a,c,m),b,m))
plusm_eq_plus =
    |- !a b m. 0 < m /\ (a + b) < m ==> (plusm(a,b,m) = a + b)

63

 expand( tactic20 INIT_maxseq_0 SW_value );;

In the case we have c (t+1) = (c t) + 1 and rem (t+1) = rem t in the assumptions. Rewriting satisfies the second disjunct, and the theorem is proved. The theorem is

saved as Liveness_1.

64

 expand( DISJ2_TAC THEN ASM_REWRITE_TAC[] );;
 let Liveness_1 = save_top_thm`Liveness_1`;;

The theorem Liveness_2 extracts the expression for the aborted variable from the ABORT predicate, by expanding its definition and rewriting using tactic21.

65

let Liveness_2 =
prove_thm(
`Liveness_2`,
"!maxseq:^sequence.
!rem sink:^datatime.  !s:^seqtime. !SW:^sequence.
!c:^time->num. !aborted:^time->bool. !maxT:num.
!ackS:^channel.
(ABORT c aborted maxT maxseq SW s rem ackS)
==>
!t:^time.
( (((c t >= maxT) \/ (aborted t)) /\ ~(NULL(rem t)))
 = aborted(t+1) )",
tactic21 );;

The theorem Liveness_3 is a generalized version of Liveness_1, relating the current value of rem at any time, t, to its value n time steps into the future.

66

g("!maxseq:^sequence.
!rem sink:^datatime.  !s r:^seqtime. !SW :^sequence.
!c:^time->num. !aborted:^time->bool. !maxT:num.
!p:^time->^sequence->bool. !i:^seqtime.
!ackS dataS :^channel.
!source:^data list.
(INIT source maxseq rem s sink r ) /\
(SENDER maxseq SW rem s p i dataS ackS ) /\
(ABORT c aborted maxT maxseq SW s rem ackS)
==>
!n:num. !t:^time.
( ?x:num. ( rem(t+n) = (TLI x (rem t)) ) /\ (0<x)  ) \/
(         ( rem(t+n) = (rem t)) /\ (n <= c(t+n)) )");;

The proof uses induction on n and the theorem Liveness_1. Set up the proof using the following tactic,

67

#expand(
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  POP_ASSUM (ASSUME_TAC o ( MP (SPEC_ALL Liveness_1) )) THEN
  INDUCT_TAC );;
OK..
2 subgoals
"!t.
  (?x. (rem(t + (SUC n)) = TLI x(rem t)) /\ 0 < x) \/
  (rem(t + (SUC n)) = rem t) /\ (SUC n) <= (c(t + (SUC n)))"
    [ "!t.
        (?x. (rem(t + 1) = TLI x(rem t)) /\ 0 < x) /\ (c(t + 1) = 0) \/
        (rem(t + 1) = rem t) /\ (c(t + 1) = (c t) + 1)" ]
    [ "!t.
        (?x. (rem(t + n) = TLI x(rem t)) /\ 0 < x) \/
        (rem(t + n) = rem t) /\ n <= (c(t + n))" ]
"!t.
  (?x. (rem(t + 0) = TLI x(rem t)) /\ 0 < x) \/
  (rem(t + 0) = rem t) /\ 0 <= (c(t + 0))"
...

The base case is trivially satisfied by rewriting with standard arithmetic theorems.

68

expand( REWRITE_TAC[ADD_CLAUSES;LESS_OR_EQ_0] );;

To prove the induction step, analyse each disjunct of each of the two assumptions in turn. There are two cases relating rem t+n to rem t (from the induction assumption) and two relating rem t' to rem t'+1 (from Liveness_1). Use tactic21A and tactic21B to set up these cases. The box below shows the first of the four goals to be proved.

69

#expand tactic21A ;;
#expand tactic21B ;;
OK..
...
"(?x. (rem(SUC(t + n)) = TLI x(rem t)) /\ 0 < x) \/
 (rem(SUC(t + n)) = rem t) /\ (SUC n) <= (c(SUC(t + n)))"
...
    [ "rem(t + n) = TLI(@x. (rem(t + n) = TLI x(rem t)) /\ 0 < x)(rem t)" ]
    [ "0 < (@x. (rem(t + n) = TLI x(rem t)) /\ 0 < x)" ]
    [ "(?x. (rem((t + n) + 1) = TLI x(rem(t + n))) /\ 0 < x) /\
       (c((t + n) + 1) = 0)" ]

In the first case the goal can be solved by rewriting the first disjunct of the goal with a suitable choice of x. This value will be the sum of the x which satisfy the 2nd and 3rd assumptions, and the x which satisfies the first conjunct of the first assumption in the list above.

The second, much simpler, case is solved in a similar manner using tactic23.

70

expand tactic22;;
expand tactic23;;

The third and fourth cases of the four are set up by tactic23A.

71

 #expand tactic21B;;
 OK..
 ...
 "(?x. (rem(SUC(t + n)) = TLI x(rem t)) /\ 0 < x) \/
  (rem(SUC(t + n)) = rem t) /\ (SUC n) <= (c(SUC(t + n)))"
 ...
     [ "(rem(t + n) = rem t) /\ n <= (c(t + n))" ]
     [ "(?x. (rem((t + n) + 1) = TLI x(rem(t + n))) /\ 0 < x) /\
        (c((t + n) + 1) = 0)" ]

This time the x needed is that from the first assumption. The necessary selection and rewriting is performed by tactic23, leaving one last case.

72

 #expand tactic23;;
 OK..
 goal proved
 ...
 Previous subproof:
 "(?x. (rem(SUC(t + n)) = TLI x(rem t)) /\ 0 < x) \/
  (rem(SUC(t + n)) = rem t) /\ (SUC n) <= (c(SUC(t + n)))"
 ...
     [ "(rem(t + n) = rem t) /\ n <= (c(t + n))" ]
     [ "(rem((t + n) + 1) = rem(t + n)) /\
        (c((t + n) + 1) = (c(t + n)) + 1)" ]

This case is easily satisfied by rewriting with the assumptions to satisfy the second disjunct.

73

 expand(
   DISJ2_TAC THEN
   ASM_REWRITE_TAC[ADD1;REWRITE_RULE [ADD1] LESS_EQ_MONO_EQ] );;
 let Liveness_3=save_top_thm `Liveness_3`;;

The theorem Liveness identifies three possible outcomes related to the progress of this sliding window protocol. The theorem states that if the list of remaining data, (rem t), has not been exhausted by time t+maxT then either rem (t+maxT) is shorter than it was at time, t or aborted will be set to true by time t+maxT+1. This theorem is used later to show that if it is assumed that the protocol is never aborted then it must make progress in the sense that rem t will eventually be the empty list.

74

g("!maxseq:^sequence.
!rem sink:^datatime.  !s r:^seqtime. !SW:^sequence.
!c:^time->num. !aborted:^time->bool. !maxT:num.
!p:^time->^sequence->bool. !i:^seqtime.
!ackS dataS :^channel.
!source:^data list.
(INIT source maxseq rem s sink r ) /\
(SENDER maxseq SW rem s p i dataS ackS ) /\
(ABORT c aborted maxT maxseq SW s rem ackS)
==>
!t:^time.
(~NULL (rem (t+maxT)) )
==>
( ( ?x:num. ( rem(t+maxT) = (TLI x (rem t)) ) /\ (0<x)  ) \/
  ( aborted(t+maxT+1) ) )");;

To begin the proof we perform case analysis on the conclusion of Liveness_3 with maxT for n.

75

expand( REPEAT GEN_TAC THEN DISCH_TAC THEN
     POP_ASSUM STRIP_ASSUME_TAC THEN IMP_RES_TAC Liveness_3);;
expand( GEN_TAC THEN
     POP_ASSUM (DISJ_CASES_TAC o SPECL ["t:num";"maxT:num"]) );;
OK..
2 subgoals
"(?x. (rem(t + maxT) = TLI x(rem t)) /\ 0 < x) \/
aborted(t + (maxT + 1))"
...
 [ "!t. ((c t) >= maxT \/ aborted t) /\ ~NULL(rem t) = aborted(t + 1)" ]
 [ "!n t.
     (?x. (rem(t + n) = TLI x(rem t)) /\ 0 < x) \/
     (rem(t + n) = rem t) /\ n <= (c(t + n))" ]
 [ "~NULL(rem(t + maxT))" ]
 [ "(rem(t + maxT) = rem t) /\ maxT <= (c(t + maxT))" ]

"(?x. (rem(t + maxT) = TLI x(rem t)) /\ 0 < x) \/
aborted(t + (maxT + 1))"
...
 [ "?x. (rem(t + maxT) = TLI x(rem t)) /\ 0 < x" ]

We use Liveness_2 to complete this proof.

76

expand( DISCH_TAC THEN DISJ1_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC);;
expand( POP_ASSUM STRIP_ASSUME_TAC THEN DISCH_TAC THEN DISJ2_TAC THEN
        IMP_RES_TAC Liveness_2);;
expand( UNDISCH_TAC "(c(t + maxT)) >= maxT ==> aborted((t + maxT) + 1)" THEN
        REWRITE_TAC[GREATER_OR_EQ_LESS_OR_EQ] THEN
        ASM_REWRITE_TAC[ADD_ASSOC]);;
let Liveness = save_top_thm`Liveness`;;

To prove the total correctness of the sliding window protocol we need to make some assumptions about its behaviour. Consider what happens if the protocol is not aborted, that is either rem is NIL or rem is still decreasing. In this case the length of rem at the end of each interval of length maxT is at least one less than its length at the beginning of the interval. Generalising this result, the length of rem at the end of n intervals of length maxT is at least n less than the original length of rem. This lemma is called the

decreasing_rem_lemma.

77

g("!rem:^datatime. !maxT:num.
   (!t:^time.
     ( NULL(rem (t+maxT))) \/
     ( ?x:num. (rem(t+maxT) = (TLI x (rem t)) ) /\ (0<x)) )
  ==>
   ( !n:num. LENGTH(rem(maxT * n)) <= (LENGTH(rem 0) - n ) )" );;

This theorem is proved by induction which is set up in the usual way.

78

#expand(
 REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC );;
OK..
2 subgoals
"(LENGTH(rem(maxT * (SUC n)))) <= ((LENGTH(rem 0)) - (SUC n))"
    [ "!t.
        NULL(rem(t + maxT)) \/
        (?x. (rem(t + maxT) = TLI x(rem t)) /\ 0 < x)" ]
    [ "(LENGTH(rem(maxT * n))) <= ((LENGTH(rem 0)) - n)" ]
"(LENGTH(rem(maxT * 0))) <= ((LENGTH(rem 0)) - 0)"
...

The base case is solved by rewriting with a number of arithmetic theorems.

79

expand( REWRITE_TAC[MULT_CLAUSES;SUB_0;LESS_EQ_REFL] );;

The proof of the induction step will use cases from its second assumption, in which t is specialized by maxT*n.

80

 #expand( UNDISCH_TAC "!t.
         NULL((rem:^datatime)(t + maxT)) \/
         (?x. (rem(t + maxT) = TLI x(rem t)) /\ 0 < x)" THEN
         DISCH_TAC THEN POP_ASSUM(DISJ_CASES_TAC o (SPEC "maxT*n")) );;
 OK..
 2 subgoals
 "(LENGTH(rem(maxT * (SUC n)))) <= ((LENGTH(rem 0)) - (SUC n))"
 ...
     [ "(LENGTH(rem(maxT * n))) <= ((LENGTH(rem 0)) - n)" ]
     [ "?x. (rem((maxT * n) + maxT) = TLI x(rem(maxT * n))) /\ 0 < x" ]
 "(LENGTH(rem(maxT * (SUC n)))) <= ((LENGTH(rem 0)) - (SUC n))"
 ...
     [ "(LENGTH(rem(maxT * n))) <= ((LENGTH(rem 0)) - n)" ]
     [ "NULL(rem((maxT * n) + maxT))" ]

For the first case, tactic28 proves that the goal must be satisfied because the length of a NULL list is 0, the tail of a NULL list is also NULL, and every number is greater than or equal to 0.

For the second case, tactic29 proves that since 0<x the length of TLI x of any list is at least 1 less than the length of the original list. The proof uses a useful lemma,

useful_lemma =
  |- !a b c n. 0 < c /\ a <= (b - n) ==> (a - c) <= (b - (SUC n))

Rewriting with these deductions and the induction assumption proves the goal.

81

 expand tactic28;;
 expand tactic29;;
 let decreasing_rem_lemma = save_top_thm`decreasing_rem_lemma`;;

The theorem just proved, decreasing_rem_lemma, and the assumption that the protocol is never aborted are combined in the theorem LIVENESS which gives a worst case for the time by which the protocol must have satisfied ?t. sink t = source.

Here is the definition intended to capture the assumption that the protocol is never aborted.

82

 let LIVE_ASSUM = new_definition(
   `LIVE_ASSUM`,
   "LIVE_ASSUM (aborted:^time->bool) (maxT:num) =
     ( !t:^time. ~(aborted (t + maxT + 1)) )" );;

and a statment of the last liveness theorem, LIVENESS.

83

 g( "!maxseq:^sequence.
     !rem sink:^datatime.  !s r:^seqtime. !SW:^sequence.
     !c:^time->num. !aborted:^time->bool. !maxT:num.
     !p:^time->^sequence->bool. !i:^seqtime.
     !ackS dataS :^channel.
     !source:^data list.
     (LIVE_ASSUM aborted maxT) /\
     (INIT source maxseq rem s sink r ) /\
     (SENDER maxseq SW rem s p i dataS ackS ) /\
     (ABORT c aborted maxT maxseq SW s rem ackS)
    ==>
     (rem (maxT * LENGTH(rem 0)) = [] )" );;

The first part of the proof is completed using tactic30. First add the conclusion of the Liveness theorem. Use IMP_DISJ_THM to rewrite the implication of this conclusion as a disjunction and then LIVE_ASSUM to show that the disjunct for aborting the protocol cannot be satisfied. All this rewriting has provided the premise of decreasing_rem_lemma as an assumption, so using IMP_RES_TAC adds the required conclusion to the assumption list.

84

 #expand( tactic30 Liveness LIVE_ASSUM decreasing_rem_lemma);;
 OK..
 "rem(maxT * (LENGTH(rem 0))) = []"
 ...
     [ "(LENGTH(rem(maxT * (LENGTH(rem 0))))) <=
        ((LENGTH(rem 0)) - (LENGTH(rem 0)))" ]

Rewrite the first assumption with a number of list and arithmetic lemmas to put it in the same form as the goal, and rewrite to solve the goal.

85

 expand(
   POP_ASSUM (ASSUME_TAC o REWRITE_RULE
      [SUB_SELF;LESS_OR_EQ;NOT_LESS_0;LENGTH_NIL]) THEN
   ASM_REWRITE_TAC[]  );;
 let LIVENESS = save_top_thm`LIVENESS`;;

5.3 Total correctness theorem

The theorems SAFETY and LIVENESS can now be combined to prove the total correctness of the sliding window protocol as expressed in the original informal specification. That is, that the implementation of the protocol and the assumption that the protocol is not aborted together satisfy the specification that there is a time at which the sink list is a copy of the source list.

86

g("!source:^data list. !maxseq:^sequence.
 !rem sink : ^datatime. !s r :^seqtime. !SW RW :^sequence.
 !p:^time->^sequence->bool. !i:^seqtime.  !q:^time->bool.
 !c:^time->num. !aborted:^time->bool. !maxT:num.
 !dataS dataR ackS ackR : ^channel.
(IMPL source maxseq rem s SW p i c aborted maxT sink r RW q
      dataS dataR ackS ackR) /\
(LIVE_ASSUM aborted maxT)
==>
( ?t :^time. (sink t) = source )" );;

The proof is straightforward. First add the conclusions of the theorems, SAFETY_THM, IMPL_LIVE_PARTS and LIVENESS and specialize the safety theorem to the time at which rem is guaranteed to be NIL.

87

expand(
REPEAT STRIP_TAC THEN
IMP_RES_TAC IMPL_LIVE_PARTS THEN
IMP_RES_TAC LIVENESS THEN
IMP_RES_TAC SAFETY_THM THEN
POP_ASSUM (ASSUME_TAC o (SPEC "maxT*LENGTH((rem:^datatime) 0)")) );;

Now rewrite this version of the safety theorem using the assumption

 rem(maxT * (LENGTH(rem 0))) = []

and use rewriting to get an assumption in the correct form to match the goal.

88

#expand(
POP_ASSUM MP_TAC THEN
ASM_REWRITE_TAC[TLI_NIL;APPEND_NIL] THEN
DISCH_TAC);;
OK..
"?t. sink t = source"
...
  [ "rem(maxT * (LENGTH(rem 0))) = []" ]
  [ "APPEND
     (sink(maxT * (LENGTH(rem 0))))
     (TLI
      (subm
       (r(maxT * (LENGTH(rem 0))),s(maxT * (LENGTH(rem 0))),maxseq))
      (rem(maxT * (LENGTH(rem 0))))) =
     source" ]
  [ "sink(maxT * (LENGTH(rem 0))) = source" ]

The last steps of the proof are to choose a value for t in the goal using EXISTS_TAC and to match the result to the first assumption in the list using FIRST_ASSUM and ACCEPT_TAC. After saving this proof, close the newly created sliding window theory. You may also end your HOL session by typing quit();;.

89

expand(
EXISTS_TAC "maxT * LENGTH((rem:^datatime) 0)" THEN
FIRST_ASSUM ACCEPT_TAC);;
let TOTAL_CORRECTNESS_THM = save_top_thm`TOTAL_CORRECTNESS_THM`;;
close_theory();;

6 References

[1] Dimitri Bertsekas and Robert Gallagher. Data Networks. Prentice-Hall International, Englewood Cliffs, NJ, 1987.

[2] Rachel Cardell-Oliver. The Specification and Verification of Sliding Window Protocols. Computer Laboratory Technical Report 183, The University of Cambridge, October 1989.

[3] Rachel Cardell-Oliver. Using higher order logic for modelling real-time protocols. In TAPSOFT ’91, number 494 in Lecture Notes in Computer Science, pages 259-282. Springer Verlag, April 1991.

A Supporting theories

The Theory plusm_subm
Parents --  HOL     int     myarith
Definitions --
plusm
  |- !a b m.
      plusm(a,b,m) =
      abs((((Int a) MODI m) plus ((Int b) MODI m)) MODI m)
N
  |- (!m. N 0 m = 0) /\
     (!n m.
       N(SUC n)m = ((N n m = 0) => (N n m) + (m - 1) | (N n m) - 1))
subm  |- !a b m. subm(a,b,m) = plusm(a,N b m,m)
Theorems -- are quoted in the case study text as necessary.
******************** plusm_subm ********************
The Theory hdi_tli
Parents --  HOL     myarith
Definitions --
TLo  |- !l. TLo l = ((~NULL l) => TL l | [])
TLI  |- (!l. TLI 0 l = l) /\ (!n l. TLI(SUC n)l = TLo(TLI n l))
HDI  |- !n l. HDI n l = HD(TLI n l)
Theorems --
LENGTH_TL  |- !l. ~NULL l ==> (LENGTH(TL l) = (LENGTH l) - 1)
NULL_LENGTH_0  |- !l. NULL l ==> (LENGTH l = 0)
APPEND_NIL  |- !l. APPEND l[] = l
TLI_NIL  |- !n. TLI n[] = []
HDI_TLI_1
  |- !x l. ~NULL(TLI x l) ==> (APPEND[HDI x l](TLI(x + 1)l) = TLI x l)
HDI_TLI_2  |- !x y l. TLI x(TLI y l) = TLI(x + y)l
HDI_TLI_3  |- !x l. LENGTH(TLI x l) = (LENGTH l) - x
******************** hdi_tli ********************