src/HOL/IOA/NTP/Read_me

+Isabelle Verification of a protocol using IOA.
+
+------------------------------------------------------------------------------
+The theory structure looks like this picture:
+
+     Correctness
+
+        Impl
+
+Sender Receiver Channels Spec
+
+ Action    IOA      Multisets
+
+ Packet        List 
+
+         Arith
+
+------------------------------------------------------------------------------
+
+The System.
+
+The system being proved correct is a parallel composition of 4 processes:
+
+    Sender || Schannel || Receiver || Rchannel
+
+Accordingly, the system state is a 4-tuple:
+
+    (Sender_state, Schannel_state, Receiver_state, Rchannel_state)
+
+------------------------------------------------------------------------------
+Packets.
+
+The objects going over the medium from Sender to Receiver are modelled
+with the type
+
+    'm packet = bool * 'm
+
+This expresses that messages (modelled by polymorphic type "'m") are
+sent with a single header bit. Packet fields are accessed by
+
+    hdr<b,m> = b
+    mesg<b,m> = m
+------------------------------------------------------------------------------
+
+The Sender.
+
+The state of the process "Sender" is a 5-tuple:
+
+     1. messages : 'm list        (* sq *)
+     2. sent     : bool multiset  (* ssent *)
+     3. received : bool multiset  (* srcvd *)
+     4. header   : bool           (* sbit *)
+     5. mode     : bool           (* ssending *)
+
+
+The Receiver.
+
+The state of the process "Receiver" is a 5-tuple:
+
+     1. messages    : 'm list              (* rq *)
+     2. replies     : bool multiset        (* rsent *)
+     3. received    : 'm packet multiset   (* rrcvd *)
+     4. header      : bool                 (* rbit *)
+     5. mode        : bool                 (* rsending *)
+
+
+The Channels.
+
+The Sender and Receiver each have a proprietary channel, named
+"Schannel" and "Rchannel" respectively. The messages sent by the Sender
+and Receiver are never lost, but the channels may mix them
+up. Accordingly, multisets are used in modelling the state of the
+channels. The state of "Schannel" is modelled with the following type:
+
+    'm packet multiset
+
+The state of "Rchannel" is modelled with the following type:
+
+    bool multiset
+
+This expresses that replies from the Receiver are just one bit.
+
+Both Channels are instances of an abstract channel, that is modelled with
+the type 
+  
+    'a multiset.
+
+------------------------------------------------------------------------------
+
+The events.
+
+An `execution' of the system is modelled by a sequence of 
+
+    <system_state, action, system_state>
+
+transitions. The actions, or events, of the system are described by the
+following ML-style datatype declaration:
+
+    'm action = S_msg ('m)           (* Rqt for Sender to send mesg      *)
+              | R_msg ('m)           (* Mesg taken from Receiver's queue *)
+              | S_pkt_sr ('m packet) (* Packet arrives in Schannel       *)
+              | R_pkt_sr ('m packet) (* Packet leaves Schannel           *)
+              | S_pkt_rs (bool)      (* Packet arrives in Rchannel       *)
+              | R_pkt_rs (bool)      (* Packet leaves Rchannel           *)
+              | C_m_s                (* Change mode in Sender            *)
+              | C_m_r                (* Change mode in Receiver          *)
+              | C_r_s                (* Change round in Sender           *)
+              | C_r_r ('m)           (* Change round in Receiver         *)
+
+------------------------------------------------------------------------------
+
+The Specification.
+
+The abstract description of system behaviour is given by defining an
+IO/automaton named "Spec". The state of Spec is a message queue,
+modelled as an "'m list". The only actions performed in the abstract
+system are: "S_msg(m)" (putting message "m" at the end of the queue);
+and "R_msg(m)" (taking message "m" from the head of the queue).
+
+
+------------------------------------------------------------------------------
+
+The Verification.
+
+The verification proceeds by showing that a certain mapping ("hom") from
+the concrete system state to the abstract system state is a `weak
+possibilities map` from "Impl" to "Spec". 
+
+
+    hom : (S_state * Sch_state * R_state * Rch_state) -> queue
+
+The verification depends on several system invariants that relate the
+states of the 4 processes. These invariants must hold in all reachable
+states of the system. These invariants are difficult to make sense of;
+however, we attempt to give loose English paraphrases of them.
+
+Invariant 1.
+
+This expresses that no packets from the Receiver to the Sender are
+dropped by Rchannel. The analogous statement for Schannel is also true.
+
+    !b. R.replies b = S.received b + Rch b 
+    /\
+    !pkt. S.sent(hdr(pkt)) = R.received(hdr(b)) + Sch(pkt)
+
+
+Invariant 2.
+
+This expresses a complicated relationship about how many messages are
+sent and header bits.
+
+    R.header = S.header 
+    /\ S.mode = SENDING
+    /\ R.replies (flip S.header) <= S.sent (flip S.header)
+    /\ S.sent (flip S.header) <= R.replies header
+    OR
+    R.header = flip S.header
+    /\ R.mode = SENDING
+    /\ S.sent (flip S.header) <= R.replies S.header
+    /\ R.replies S.header <= S.sent S.header
+
+
+Invariant 3.
+
+The number of incoming messages in the Receiver plus the number of those
+messages in transit (in Schannel) is not greater than the number of
+replies, provided the message isn't current and the header bits agree.
+
+    let mesg = <S.header, m>
+    in
+    R.header = S.header
+    ==>
+    !m. (S.messages = [] \/ m ~= hd S.messages)
+        ==> R.received mesg + Sch mesg <= R.replies (flip S.header)
+
+
+Invariant 4.
+
+If the headers are opposite, then the Sender queue has a message in it.
+
+    R.header = flip S.header ==> S.messages ~= []
+