/* Copyright © 2010 The Crowfoot Team (Billiejoe Charlton, Ben Horsfall, Bernhard Reus) */


/* Now we program in an update, which adds logging, as in the
  "Formalizing Dynamic Software Updating" paper (Bierman, Hicks, Sewell, Stoyle). */


const version;


/* Modules: */

const serverOne;
const handlersOne;

const logOne;    /* These two modules will be added in the update. */
const serverTwo;

const serverLatest;
const handlersLatest;
const logLatest;


/* Offsets */

/* Server module */

const getevent = 0;
const handle = 1;
const loop = 2;
const loopPrime = 3;

/* Handlers module */

const handleGet = 0;
const handlePost = 1;
const handleUpdate = 2;

/* Log module */

const emptyLog = 0;
const logevent = 1;


/* 'Abstract' (universally quantified) predicates for request data, queues and logs. */

forall $GetRequest(_).
forall $PostRequest(_).

forall $Queue(_,_).
forall $NonEmptyQueue(_,_). 

forall $Log(_,_).  /* Second argument counts number of log entries */




/* Three different kinds of event can happen. */

const evGet = 0;
const evPost = 1;
const evUpdate = 2;

recdef $Event(e) :=

      e |-> evGet *  $GetRequest(e+1)
    | e |-> evPost * $PostRequest(e+1)
    | e |-> evUpdate;
    

/* Now there are predicates $CodeOne and $CodeTwo. $Code1 describes the behaviour of the code for version 1 
   of webserver (i.e. the initial program) and $Code2 describes the behaviour of the extra code added onto
   the heap in the update to give version 2. */

recdef $CodeOne() :=

handlersOne+handleGet |->
forall q,req,n.
  { $GetRequest(req) * $Queue(q,n) }
  _(q,req)
  { $Queue(q,n) }

*

handlersOne+handlePost |->
forall q,req,n.
  { $PostRequest(req) * $Queue(q,n) }
  _(q,req)
  { $Queue(q,n) }

*
  
handlersOne+handleUpdate |->
forall ver.
  { $Code(ver) }
  _()
  { $Code(ver+1) * ver != 2 | $Code(ver) * ver=2 }  

*

serverOne+getevent |->
forall q,n.
  { $Queue(q,n) }
  _(q)
  { $NonEmptyQueue(q,n) }

*

serverOne+handle |->
forall q,n.
  { $Code(1) * $NonEmptyQueue(q,n) }
  _(q)
  { $Code(1) * $Queue(q,n+1)  |  $Code(2) * $Queue(q,n+1) }  

*

serverOne+loop |->
forall q.  
  { exists n. $Code(1) * $Queue(q,n) }
  _(q)
  { false }
;


recdef $CodeTwo() := 

logOne+emptyLog |->
forall logPtr.
  {logPtr |-> _}
  _(logPtr)
  {exists l. logPtr |-> l * $Log(l,0)}

* 

logOne+logevent |->
  forall l,e,n.
  {$Log(l,n) * $Event(e)}
  _(l,e)
  {$Log(l,n+1) * $Event(e)}

* 

serverTwo+getevent |->
forall q,n.
  { $Queue(q,n) }
  _(q)
  { $NonEmptyQueue(q,n) }
  
*

serverTwo+handle |->
forall l,q,n.
  { $Code(2) * $NonEmptyQueue(q,n) * $Log(l,n) }
  _(l,q)
  { $Code(2) * $Queue(q,n+1) * $Log(l,n+1) }

  /*  Note how this triple states that 'handle' maintains an INVARIANT:
      that there are as many log entries as there are dequeued messages. */

*

serverTwo+loop |->
forall q.
  { exists n. $Code(2) * $Queue(q,n) }
  _(q)
  { false }

* 

serverTwo+loopPrime |->
forall l,q.
  {exists n. $Code(2) * $Queue(q,n) * $Log(l,n) }   /* INVARIANT holds at loop start */
  _(l,q)
  { false }
;


/* The $Code(v) predicate describes version v of the system (in this file, version 1 or 2)
   with code stored on the heap, and the pointers to the latest versions. */ 

recdef $Code(v) :=

/* First there is "version 1" (initial program): */

v = 1  * version |-> 1

*

$CodeOne()

  * handlersLatest |-> handlersOne
  * serverLatest |-> serverOne

  /* Things that will appear in first update: */

  * logLatest |-> 0
 
  * logOne+emptyLog |-> 0
  * logOne+logevent |-> 0

  * serverTwo+getevent |-> 0
  * serverTwo+handle |-> 0
  * serverTwo+loop |-> 0
  * serverTwo+loopPrime |-> 0


/* Then there is "version 2" (after the update) */

|

v = 2  * version |-> 2

*

$CodeOne()

  * handlersLatest |-> handlersOne

  /* Things that changed in the update: */

* 

$CodeTwo()

  * logLatest |-> logOne

  * serverLatest |-> serverTwo
;


/* All the code for the initial program is still here. */

proc abstract handleGet(q,req)
  forall n.
  pre:  $GetRequest(req) * $Queue(q,n);
  post: $Queue(q,n);

proc abstract handlePost(q,req)
  forall n.
  pre:  $PostRequest(req) * $Queue(q,n);
  post: $Queue(q,n);


proc handleUpdate()

forall ver.
  pre:  $Code(ver);
  post: $Code(ver+1) * ver != 2 | $Code(ver) * ver=2;
  
  {
  	call update()
  }


/* The body of update has changed to now implement a particular update step, to add logging. */

proc update()

forall ver.
  pre:  $Code(ver);
  post: $Code(ver+1) * ver != 2 | $Code(ver) * ver=2;
  
  {
  	locals v;
  	
  	ghost "unfold $Code(?)";
  	
  	v := [version];
  	
  	if v = 1 then
  	  {  	  	
  	  	/* If the system is still at version 1, perform the update. */
  	
  		/* Load to the heap the procedures for the new Log module, and the updated Server module. */
  		  		  	
	    [logOne+emptyLog] := mk_empty_log(_);
	    [logOne+logevent] := logevent(_,_);
	    [serverTwo+getevent] := getevent(_);  
		[serverTwo+handle] := handle2(_,_);
		[serverTwo+loop] := loop2(_);
		[serverTwo+loopPrime] := loopPrime(_,_);
	
		ghost "fold $CodeTwo()";
		
		/* Now update the latest pointers. */
	
	    [logLatest] := logOne;
	    [serverLatest] := serverTwo;

		[version] := 2
  	  } 

	else  /* If the system has already reached version 2, do nothing. */
	  {
	  	skip
	  };
	  
	ghost "fold $Code(?)"
  }


proc abstract getevent(q)
 forall n.
  pre:  $Queue(q,n);
  post: $NonEmptyQueue(q,n);


proc handle(q)
 forall n.
  pre:  $Code(1) * $NonEmptyQueue(q,n);
  post:  $Code(1) * $Queue(q,n+1)  |  $Code(2) * $Queue(q,n+1); 
  
  /* This postcondition has changed to reflect the fact that within 'handle' the system may
     transition from one version to the next. */
  
  {
  	locals ePtr, event, eventType, req;
  	
  	ePtr := new 0;
  	call dequeue(q,ePtr);
  	event := [ePtr];
	dispose ePtr;
	
	ghost "unfold $Event(?)";
	
	eventType := [event];
	req := event+1;
	
	if eventType = evGet then
	  {
	  	eval [handlersOne+handleGet](q,req)
	  }
	else
	  {
	  	if eventType = evPost then
	  	  {
	  	  	eval [handlersOne+handlePost](q,req)
	  	  }
	  	else
	  	  {
	  	  	eval [handlersOne+handleUpdate]()
	  	  }
	  };
	 
  	dispose event 
  }


proc loop(q)

  pre:  exists n. $Code(1) * $Queue(q,n);
  post: false;

  {
    locals tmp;

    ghost "unfold $Code(1)";
    tmp := [serverLatest];
    ghost "fold $Code(1)";
    eval [tmp+getevent](q);

    ghost "unfold $Code(1)";
    tmp := [serverLatest];
    ghost "fold $Code(?)";
    eval [tmp+handle](q);

    ghost "unfold $Code(?)";
    tmp := [serverLatest];
    ghost "fold $Code(?)";
    eval [tmp+loop](q)
  }


proc main()

  pre:
      version |-> _
      
    /* For the initial program: */

    * handlersOne |-> 0,0,0 /* handleGet, handlePost, handleUpdate */
    * serverOne |-> 0,0,0 /* getevent, handle, loop */
    
    /* For the update: */
    
	* logOne |-> 0,0 /* emptyLog, logevent */
	* serverTwo |-> 0,0,0,0 /* ..., loop' */
	
	/* These will hold pointers to the latest versions */
	* handlersLatest |-> 0
	* serverLatest |-> 0
	* logLatest |-> 0;

  post: false;
    
  {
    locals qPtr,q;
  	
  	[version] := 1;
  	
    /* We begin by writing all the procedures for the intial program onto the heap. */

    [serverOne+getevent] := getevent(_);
    [serverOne+handle] := handle(_);
    [serverOne+loop] := loop(_);

    [handlersOne+handleGet] := handleGet(_,_);
    [handlersOne+handlePost] := handlePost(_,_);
    [handlersOne+handleUpdate] := handleUpdate();

	ghost "fold $CodeOne()";

    /* Then we set up all the "latest" pointers to point to version 1. */

    [serverLatest] := serverOne;
    [handlersLatest] := handlersOne;
    
    ghost "fold $Code(1)";
    
    /* We create an empty queue, and then call 'loop' to start the server. */
   	
    qPtr := new 0;
    call mk_empty_queue(qPtr);
    q := [qPtr];
    dispose qPtr;

    eval [serverOne+loop](q)
  }



/* =========================
        CODE FOR UPDATE
   ========================= */

/* Here are the commands for the new Log module. */

proc abstract mk_empty_log(logPtr)
  pre:  logPtr |-> _;
  post: exists l. logPtr |-> l * $Log(l,0);
  
 
proc abstract logevent(l,e)
 forall n.
  pre:  $Log(l,n) * $Event(e);
  post: $Log(l,n+1) * $Event(e);
  
  
/* Here are the commands for the replacement Server module. */

proc handle2(l,q)
 forall n.
  pre:  $Code(2) * $NonEmptyQueue(q,n) * $Log(l,n);
  post: $Code(2) * $Queue(q,n+1) * $Log(l,n+1);
  
  {
	locals ePtr, event, eventType, req, tmp;

  	ePtr := new 0;
  	call dequeue(q,ePtr);
  	event := [ePtr];
	dispose ePtr;
	
	
	/* Here is the new behaviour: we log the event. */
	
	ghost "unfold $Code(2)";
	tmp := [logLatest];
	ghost "fold $Code(2)";
	eval [tmp+logevent](l,event);
	
	
	ghost "unfold $Event(?)";
	
	eventType := [event];
	req := event+1;
		
	if eventType = evGet then
	  {
	  	eval [handlersOne+handleGet](q,req)
	  }
	else
	  {
	  	if eventType = evPost then
	  	  {
	  	  	eval [handlersOne+handlePost](q,req)
	  	  }
	  	else
	  	  {
	  	  	eval [handlersOne+handleUpdate]()
	  	  }
	  };
	 
  	dispose event
  }

proc loop2(q)  /* This is the "transitional" function which creates an empty log. */
  pre:  exists n. $Code(2) * $Queue(q,n);
  post: false;
  
  {
	locals logPtr, log;
	
	logPtr := new 0;
	eval [logOne+emptyLog](logPtr);
	log := [logPtr];
	dispose logPtr;
	
	/* Before we start logging we need to reset the counter for the dequeued messages. */
	
	call reset(q);
	
	eval [serverTwo+loopPrime](log,q)
  }

proc loopPrime(l,q)
  pre:  exists n. $Code(2) * $Queue(q,n) * $Log(l,n);
  post: false;
  
  {
	locals tmp;

    ghost "unfold $Code(2)";
    tmp := [serverLatest];
    ghost "fold $Code(2)";
    eval [tmp+getevent](q);

    ghost "unfold $Code(2)";
    tmp := [serverLatest];
    ghost "fold $Code(2)";
    eval [tmp+handle](l,q);

    ghost "unfold $Code(?)";
    tmp := [serverLatest];
    ghost "fold $Code(?)";
    eval [tmp+loopPrime](l,q)
  }



/* =========================
   Abstract queue operations
   ========================= */
    

proc abstract mk_empty_queue(qPtr)
  pre:  qPtr |-> _;
  post: exists q. qPtr |-> q * $Queue(q,0);


proc abstract dequeue(q,ePtr)
forall n.
  pre:  $NonEmptyQueue(q,n) * ePtr |-> _;
  post: exists e. $Queue(q,n+1) * ePtr |-> e * $Event(e);


proc abstract reset(q) /* This operations resets the internal dequeued messages counter */
pre:  exists n. $Queue(q,n);
post: $Queue(q,0);