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


/* Finally we add in also a second update, to change the type of events. We use the "convert"
   strategy to deal with events already in the queue. */

const version;


/* Modules: */

const serverOne;
const handlersOne;

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

const serverThree;   /* These three modules will be added in the second update. */
const handlersTwo;
const logTwo;

const serverLatest;
const handlersLatest;
const logLatest;


/* Offsets */

/* Server module */

const getevent = 0;
const handle = 1;
const loop = 2;
const loopPrime = 3;
const loopPrimePrime = 4;
const convertevent = 5;
const convert = 6;

/* 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(_,_).


/* Now there are also predicates to represent the new event type, used after the second update. */

forall $GetRequestNew(_).
forall $PostRequestNew(_).

forall $QueueNew(_,_).
forall $NonEmptyQueueNew(_,_).


/* 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;

recdef $EventNew(e) :=

      e |-> evGet *  $GetRequestNew(e+1)
    | e |-> evPost * $PostRequestNew(e+1)
    | e |-> evUpdate;



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 != 3 | $Code(ver) * ver=3 }  

*

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) |  $Code(3) * $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 }
;


/* Now there is a new predicate $CodeThree, which describes the behaviour of the extra code added onto the heap
 * in the second upate, to give version 3. */

recdef $CodeThree() :=

serverThree+convertevent |-> 
 forall e,newePtr.
  { newePtr |-> _ * $Event(e) }
  _(e,newePtr)
  { exists x. newePtr |-> x * $EventNew(x) }

*

serverThree+convert |-> 
forall q, newqPtr, n.
  { newqPtr |-> _ * $Queue(q,n) }
  _(q, newqPtr)
  { exists q. newqPtr |-> q * $QueueNew(q,n) }

*

serverThree+getevent |-> 
forall q,n.
  { $QueueNew(q,n) }
  _(q)
  { $NonEmptyQueueNew(q,n) }

*

serverThree+handle |-> 
forall l,q,n. 
  { $Code(3) * $NonEmptyQueueNew(q,n) * $Log(l,n) }
  _(l,q)
  { $Code(3) * $QueueNew(q,n+1) * $Log(l,n+1) }
 /*  Note how this triple states that handle maintains an INVARIANT:
   *  that  are as many log entries as there are dequeued messages */

*  

serverThree+loop |-> _  /* loop isn't needed anymore in serverThree */

*

serverThree+loopPrime |-> 
forall l,q. 
  { exists n. $Code(3) * $Queue(q,n) * $Log(l,n) }   /* assumes the INVARIANT */
  _(l,q)
  { false }
 
 *
 
serverThree+loopPrimePrime |-> 
forall l,q. 
  { exists n. $Code(3) * $QueueNew(q,n) * $Log(l,n) }   /* assumes the INVARIANT */
  _(l,q)
  { false }

*

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


*

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

*

handlersTwo+handleGet |->  
forall q,req,n.
  { $GetRequestNew(req) * $QueueNew(q,n) }
  _(q,req)
  { $QueueNew(q,n) }

*
  
handlersTwo+handlePost |-> 
forall q,req,n. 
  { $PostRequestNew(req) * $QueueNew(q,n) }
  _(q,req)
  { $QueueNew(q,n) }

* 

handlersTwo+handleUpdate |->
forall ver.
  { $Code(ver) }
  _()
  { $Code(ver+1) * ver != 3 | $Code(ver) * ver=3 }  
;


/* The $Code(v) predicate describes version v of the system (here, version 1, 2 or 3)
   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

  /* Things that will appear in second update. */

  * serverThree+getevent |-> 0
  * serverThree+handle |-> 0
  * serverThree+loop |-> 0
  * serverThree+loopPrime |-> 0
  * serverThree+loopPrimePrime |-> 0
  * serverThree+convertevent |-> 0
  * serverThree+convert |-> 0

  * logTwo+emptyLog |-> 0
  * logTwo+logevent |-> 0
    
  * handlersTwo+handleGet |-> 0
  * handlersTwo+handlePost |-> 0
  * handlersTwo+handleUpdate |-> 0 
    

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

|

v = 2  * version |-> 2

*

$CodeOne()

  * handlersLatest |-> handlersOne

  /* Things that changed in the first update: */

* 

$CodeTwo()

  * logLatest |-> logOne

  * serverLatest |-> serverTwo

  /* Things that will appear in the second update. */

  * serverThree+getevent |-> 0
  * serverThree+handle |-> 0
  * serverThree+loop |-> 0
  * serverThree+loopPrime |-> 0
  * serverThree+loopPrimePrime |-> 0
  * serverThree+convertevent |-> 0
  * serverThree+convert |-> 0

  * logTwo+emptyLog |-> 0
  * logTwo+logevent |-> 0
    
  * handlersTwo+handleGet |-> 0
  * handlersTwo+handlePost |-> 0
  * handlersTwo+handleUpdate |-> 0 


/* Finally there is "version 3" (after both updates) */

|

v = 3  * version |-> 3

*

$CodeOne()

*

$CodeTwo()

/* Things that changed in 3rd update: */

* $CodeThree()
  
  * serverLatest |-> serverThree
  * handlersLatest |-> handlersTwo
  * logLatest |-> logTwo
;
  

/* All the code for the initial program and the first update 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 != 3 | $Code(ver) * ver=3;
  
  {
  	call update()
  }


/* The body of update has changed again: it now implements a sequence of two update steps. */

proc update()

forall ver.
  pre:  $Code(ver);
  post: $Code(ver+1) * ver != 3 | $Code(ver) * ver=3;
  
  {
  	locals v;
  	
  	ghost "unfold $Code(?)";
  	
  	v := [version];
  	
  	if v = 1 then
  	  {  	  	
  	  	/* If the system is still at version 1, perform the first 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()";
	
	    [logLatest] := logOne;
	    [serverLatest] := serverTwo;
		
		[version] := 2
  	  } 

	else
	  {
	  	if v = 2 then
	  	  {
	  	  	/* If the system is still at version 2, perform the second update. */
  	
  			/* Load to the heap the procedures for the new Log, Handlers and Server modules. */

			/* Server module: */
			
	  	  	[serverThree+convertevent] := convertevent(_,_);
			[serverThree+convert] := convert(_,_);
			[serverThree+getevent] := getevent3(_);
			[serverThree+handle] := handle3(_,_);
			[serverThree+loopPrime] := loopPrime3(_,_);
			[serverThree+loopPrimePrime] := loopPrimePrime(_,_);
 
			[serverLatest] := serverThree; 

			/* Log module: */
			
			[logTwo+emptyLog] := mk_empty_log(_);
			[logTwo+logevent] := logevent2(_,_);
			
			[logLatest] := logTwo;

			/* Handlers module: */
			
			[handlersTwo+handleGet] := handleGet2(_,_);
			[handlersTwo+handlePost] := handlePost2(_,_);
			[handlersTwo+handleUpdate] := handleUpdate();

			[handlersLatest] := handlersTwo;

			ghost "fold $CodeThree()";

			[version] := 3
	  	  }
	  	else  /* If the system has already reached version 3, 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);
  
  {
  	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 first update: */
    
	* logOne |-> 0,0 /* emptyLog, logevent */
	* serverTwo |-> 0,0,0,0 /* ..., loop' */

	/* For the second update: */
	
	* serverThree |-> 0,0,0,0,0,0,0 /* ... ,loop'', convertevent, convert */
	* logTwo |-> 0,0
	* handlersTwo |-> 0,0,0
	
	/* 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 FIRST UPDATE
   =============================== */

/* 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);
  
  
/* 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) |  $Code(3) * $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)
  }

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

/* For the replacement Server module. */

 proc abstract convertevent(e,newePtr)
  pre:  newePtr |-> _ * $Event(e);
  post: exists x. newePtr |-> x * $EventNew(x);


proc abstract convert(q, newqPtr)
  forall n.
  pre:  newqPtr |-> _ * $Queue(q,n);
  post: exists q. newqPtr |-> q * $QueueNew(q,n);


proc abstract getevent3(q)
  forall n.
  pre:  $QueueNew(q,n);
  post: $NonEmptyQueueNew(q,n);

proc handle3(l,q)
 forall n.
  pre:  $Code(3) * $NonEmptyQueueNew(q,n) * $Log(l,n);
  post: $Code(3) * $QueueNew(q,n+1) * $Log(l,n+1);
  
  {
	locals ePtr, event, eventType, req, tmp;

  	ePtr := new 0;
  	call dequeue(q,ePtr);
  	event := [ePtr];
	dispose ePtr;
	
	ghost "unfold $Code(3)";
	tmp := [logLatest];
	ghost "fold $Code(3)";
	eval [tmp+logevent](l,event);
	
	ghost "unfold $EventNew(?)";
	
	eventType := [event];
	req := event+1;
		
	if eventType = evGet then
	  {
	  	eval [handlersTwo+handleGet](q,req)
	  }
	else
	  {
	  	if eventType = evPost then
	  	  {
	  	  	eval [handlersTwo+handlePost](q,req)
	  	  }
	  	else
	  	  {
	  	  	eval [handlersTwo+handleUpdate]()
	  	  }
	  };
	 
  	dispose event
  }


proc loopPrime3(l,q)
  pre:  exists n. $Code(3) * $Queue(q,n) * $Log(l,n);
  post: false;
  
  {
  	locals newq, newqPtr, tmp;
  	
  	/* Convert the existing queued events to the new type. */
  	
  	newqPtr := new 0;
  	ghost "unfold $Code(3)";
  	tmp := [serverLatest];
  	ghost "fold $Code(3)";
  	
  	eval [tmp+convert](q, newqPtr);
  	newq := [newqPtr];
  	dispose newqPtr; 
  	
	eval [serverThree+loopPrimePrime](l,newq)
  }
 
proc loopPrimePrime(l,q)
  pre: exists n. $Code(3) * $QueueNew(q,n) * $Log(l,n);
  post: false;
  
  {
	locals tmp;

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

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

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


/* For the replacement Log module. */

proc abstract logevent2(l,e)
 forall n.
  pre:  $Log(l,n) * $EventNew(e);
  post: $Log(l,n+1) * $EventNew(e);


/* For the Handlers module. */

proc abstract handleGet2(q,req)
  forall n.
  pre:  $GetRequestNew(req) * $QueueNew(q,n);
  post: $QueueNew(q,n);
  
proc abstract handlePost2(q,req)
  forall n.
  pre:  $PostRequestNew(req) * $QueueNew(q,n);
  post: $QueueNew(q,n);


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

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


/* The queues used in the "Formalizing Dynamic Software Updating" are polymorphic and can be used
   with event queues at both the old and new event types. Here we get this effect by using a standard
   trick to conjoin two specifications into a single one. */

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


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