module native/a
open native/common

-- 2006-07-07 DONE 

-- State definitions

sig AbWorld {
	abAuthPurse : set AbPurse
}

sig AbPurse in Purse {
	abBalance, abLost : Coin -> AbWorld
}

pred Abstract (s : AbWorld) {
	no s.abAuthPurse.abBalance.s & s.abAuthPurse.abLost.s
-- the following does not pass through the parser.
--	(s.abAuthPurse <: (abBalance + abLost).s) : AbPurse lone -> Coin
-- so rewrite it
	all c : Coin | lone (abBalance + abLost).s.c & s.abAuthPurse
}

pred XiAbPurse (s, s' : AbWorld, a : set AbPurse) {
	a <: abBalance.s = a <: abBalance.s'
	a <: abLost.s = a <: abLost.s'
}

-- Security properties

fun totalBalance (s : AbWorld) : set Coin {
	s.abAuthPurse.abBalance.s
}

fun totalLost (s : AbWorld) : set Coin {
	s.abAuthPurse.abLost.s
}

pred NoValueCreation (s, s' : AbWorld) {
	totalBalance <s'> in totalBalance <s>
}

pred AllValueAccounted (s, s' : AbWorld) {
	totalBalance <s'> + totalLost <s'> = totalBalance <s> + totalLost <s>
}

-- Messages have to be included.

one sig aNullIn {}

sig AIN in aNullIn + TransferDetails {}

fact ain_constr {
     one  aNullIn
	AIN = aNullIn + TransferDetails
}

pred XiAbIn (a, g : AIN) {
	(a + g) in aNullIn or (a + g) in TransferDetails
	(a + g) in TransferDetails implies XiTransfer (a, g)
}

abstract sig AOUT {}
one sig aNullOut extends AOUT {}

-- Operations

pred Authentic (s : AbWorld, p : AbPurse) {
	p in s.abAuthPurse
}

pred SufficientFundsProperty (s : AbWorld, t  :TransferDetails) {
	t.value in t.from.abBalance.s
}

pred AbOp (a_out  : AOUT) {
	a_out = aNullOut
}

pred AbIgnore (s, s' : AbWorld, a_out : AOUT) {
	AbOp (a_out)
	s.abAuthPurse = s'.abAuthPurse
	XiAbPurse (s, s', s.abAuthPurse)
}

pred AbWorldSecureOp (s, s' : AbWorld, a_in : AIN, a_out : AOUT) {
	AbOp (a_out)
	a_in in TransferDetails
	s.abAuthPurse - a_in.from - a_in.to = s'.abAuthPurse - a_in.from - a_in.to
	XiAbPurse (s, s', s.abAuthPurse - a_in.from - a_in.to)
}

pred AbTransferOkay (s, s' : AbWorld, a_in : AIN, a_out : AOUT) {
	AbWorldSecureOp (s, s', a_in, a_out)
	Authentic (s, a_in.from)
	Authentic (s, a_in.to)
	SufficientFundsProperty (s, a_in)
	no a_in.from & a_in.to
	a_in.from.abBalance.s' = a_in.from.abBalance.s - a_in.value
	a_in.from.abLost.s' = a_in.from.abLost.s
	a_in.to.abBalance.s' = a_in.to.abBalance.s + a_in.value
	a_in.to.abLost.s' = a_in.to.abLost.s

	-- ADDED :
	Authentic (s', a_in.from)
	Authentic (s', a_in.to)
}

pred AbTransferLost (s, s' : AbWorld, a_in : AIN, a_out : AOUT) {
	AbWorldSecureOp (s, s', a_in, a_out)
	Authentic (s, a_in.from)
	Authentic (s, a_in.to)
	SufficientFundsProperty (s, a_in)
	no a_in.from & a_in.to
	a_in.from.abBalance.s'  = a_in.from.abBalance.s - a_in.value
	a_in.from.abLost.s' = a_in.from.abLost.s + a_in.value
	XiAbPurse (s, s', a_in.to)

	-- ADDED :
	Authentic (s', a_in.from)
	Authentic (s', a_in.to)
}

pred AbTransfer (s, s' : AbWorld, a_in : AIN, a_out : AOUT) {
	AbTransferOkay (s, s', a_in, a_out) or AbTransferLost (s, s', a_in, a_out) or AbIgnore (s, s', a_out)
}

pred AbInitState (s : AbWorld) {
	Abstract (s)
}

pred AbInitIn (a, g : AIN) {
	XiAbIn (a, g)
}

pred AbFinState (a, g : AbWorld) {
	g.abAuthPurse = a.abAuthPurse
	XiAbPurse (g, a, g.abAuthPurse)
}

pred AbFinOut (a, g : AOUT) {
	a = g
}