-- ABSTRACT/BETWEEN ABSTRACTION RELATION

module mondex/rab
open mondex/a
open mondex/c
open mondex/b
open util/ordering [mondex/c/SEQNO] as seqord
open mondex/op


-- The abstraction relation depends on a set of "chosen lost"
-- transactions. That is, the way of counting the "balance" and "lost"
-- values of the Abstract purses.

pred AbstractBetween (a : AbWorld0, b : ConWorld) {
	Between (b)
	a.abAuthPurse.AbPurse = b.conAuthPurse.ConPurse
}

sig ChosenLost {
	pd : set PayDetails
}
fact {
	no disj c1, c2 : ChosenLost | c1.pd = c2.pd
}

-- Given a Between world and a set of "chosen lost" transaction, we'll
-- consider that the following predicate actually constructs an AbWorld0 -
-- that is, an unconstrained (but functional) relation from
-- NAMEs to unconstrained Abstract Purse records.

pred RabCl (a : AbWorld0, b : ConWorld, cl : set PayDetails) {
	AbstractBetween (a, b)
	cl in maybeLost (b)
	all n : NAME | n in a.abAuthPurse.AbPurse implies {
		n.(a.abAuthPurse).lost = ((definitelyLost (b) + cl) & {pd : PayDetails | pd.from = n}).value
		n.(a.abAuthPurse).balance = n.(b.conAuthPurse).balance + ((maybeLost(b) - cl) & {pd : PayDetails | pd.to = n}).value
	}
        -- We have to enforce the functionality of the
	-- abPurse relatio of the AbWorld0.
	all n : NAME | lone n.(a.abAuthPurse)
}

-- I have to show that the record "constructed" by RabCl is actually an
-- AbWorld, that is its relation and its purses verify the constraint.

assert rab_ex {
	all b : ConWorld, cl : ChosenLost, a : AbWorld0 |
	RabCl (a, b, cl.pd) implies Abstract (a.abAuthPurse)
}

-- There are also abstract relations between Abstract and Between messages

pred RabIn (a_in : AIN, m_in : MESSAGE, name_in : NAME) {
	InitIn (a_in, m_in, name_in)
}

pred RabOut (a_out : AOUT, m_out : MESSAGE) {
	FinOut (a_out, m_out)
}

-- Check the initialization and the finalization.

assert rab_init {
	all b : ConWorld, cl : ChosenLost, a : AbWorld | {
		BetweenInitState (b)
		RabCl (a, b, cl.pd)
	}
	implies AbInitState (a)
}

assert rab_initIn {
	all g_in, a_in : AIN, m_in : MESSAGE, name_in : NAME | {
		InitIn (g_in, m_in, name_in)
		RabIn (a_in, m_in, name_in)
	}
	implies AbInitIn (a_in, g_in)
}

assert rab_fin {
	all g : GlobalWorld, b : ConWorld, cl : ChosenLost, a : AbWorld | {
		FinState (b, g)
		RabCl (a, b, maybeLost (b))
	}
	implies AbFinState (a, g)
}

assert rab_finOut {
	all a_out, g_out : AOUT, m_out : MESSAGE | {
		FinOut (g_out, m_out)
		RabOut (a_out, m_out)
	}
	implies AbFinOut (a_out, g_out)
}



-- Now I may check the Backwards simulation. That is, given the Between
-- operation, the post "chosen lost" transfer set and the Abstract
-- post-state, I've to calculate a pre "chosen lost" transfer set and check
-- that the AbWorld deduced from that value is a valid pre-state for the
-- corresponding Abstract operation.

assert rab_ignore {
	all a, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a, b, cl'.pd)
	}
	implies AbIgnore (a, a', a_in, a_out)
}

-- As I know that the Between operations can do nothing, I eliminate this
-- case by adding the hypothesis "not Ignore", to try to make the proof
-- faster...

assert rab_abort {
	all a1, a2, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		Abort (b, b', name_in, m_in, m_out)
		not Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a1, b, cl'.pd)
		RabCl (a2, b, cl'.pd + name_in.(b.conAuthPurse).pdAuth)
	}
	implies (
		AbIgnore (a1, a', a_in, a_out) or AbIgnore (a2, a', a_in, a_out)
	)
}

assert rab_increase {
	all a, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		Increase (b, b', name_in, m_in, m_out)
		not Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a, b, cl'.pd)
	}
	implies AbIgnore (a, a', a_in, a_out)
}

assert rab_startFrom {
	all a1, a2, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		StartFrom (b, b', name_in, m_in, m_out)
		not Abort (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a1, b, cl'.pd)
		RabCl (a2, b, cl'.pd + name_in.(b.conAuthPurse).pdAuth)
	}
	implies (
		AbIgnore (a1, a', a_in, a_out) or AbIgnore (a2, a', a_in, a_out)
	)
}

assert rab_startTo {
	all a1, a2, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		StartTo (b, b', name_in, m_in, m_out)
		not Abort (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a1, b, cl'.pd)
		RabCl (a2, b, cl'.pd + name_in.(b.conAuthPurse).pdAuth)
	}
	implies (
		AbIgnore (a1, a', a_in, a_out) or AbIgnore (a2, a', a_in, a_out)
	)
}

-- Only Req makes a transfer. But, as I know that AbTransfer can abstractly
-- do nothing, it is also valid to eliminate the between Ignore case (which
-- I showed corresponds to the AbIgnore operation).

assert rab_req {
	all a1, a2, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		Req (b, b', name_in, m_in, m_out)
		not Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a1, b, cl'.pd)
		RabCl (a2, b, cl'.pd - (m_in :> req).details)
	}
	implies AbTransfer (a1, a', a_in, a_out) or AbTransfer (a2, a', a_in, a_out)
}

assert rab_val {
	all a, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		Val (b, b', name_in, m_in, m_out)
		not Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a, b, cl'.pd)
	}
	implies AbIgnore (a, a', a_in, a_out)
}

assert rab_ack {
	all a, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		Ack (b, b', name_in, m_in, m_out)
		not Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a, b, cl'.pd)
	}
	implies AbIgnore (a, a', a_in, a_out)
}

assert rab_readExceptionLog {
	all a1, a2, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		ReadExceptionLog (b, b', name_in, m_in, m_out)
		not Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a1, b, cl'.pd)
                RabCl (a2, b, cl'.pd + name_in.(b.conAuthPurse).pdAuth)
	}
	implies AbIgnore (a1, a', a_in, a_out) or AbIgnore (a2, a', a_in, a_out)
}

assert rab_clearExceptionLog {
	all a, a2, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		ClearExceptionLog (b, b', name_in, m_in, m_out)
		not Abort (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a, b, cl'.pd)
                RabCl (a2, b, cl'.pd + name_in.(b.conAuthPurse).pdAuth)
	}
	implies AbIgnore (a, a', a_in, a_out) or AbIgnore (a2, a', a_in, a_out)
}

assert rab_authorizeExLogClear {
	all a, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		AuthorizeExLogClear (b, b', name_in, m_in, m_out)
		not Ignore (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a, b, cl'.pd)
	}
	implies AbIgnore (a, a', a_in, a_out)
}

assert rab_archive {
	all a, a' : AbWorld, b, b' : ConWorld, cl' : ChosenLost, a_in : AIN, m_in : MESSAGE, name_in : NAME, a_out : AOUT, m_out : MESSAGE | {
		Archive (b, b', name_in, m_in, m_out)
		RabIn (a_in, m_in, name_in)
		RabOut (a_out, m_out)
		RabCl (a', b', cl'.pd)
		RabCl (a, b, cl'.pd)
	}
	implies AbIgnore (a, a', a_in, a_out)
}

check rab_ex for 10 but 1 ConWorld, 1 ChosenLost, 1 AbWorld0
check rab_init for 10
check rab_initIn for 10
check rab_fin for 10 but 1 GlobalWorld, 1 ChosenLost, 1 ConWorld, 1 AbWorld0
check rab_finOut for 10
check rab_ignore for 8 but 2 ConWorld, 1 ChosenLost, 2 AbWorld0 
check rab_increase for 8 but 2 ConWorld, 1 ChosenLost, 3 AbWorld0 
check rab_abort for 8 but 2 ConWorld, 1 ChosenLost, 3 AbWorld0 
check rab_startFrom for 8 but 2 ConWorld, 1 ChosenLost, 3 AbWorld0 
check rab_startTo for 8 but 2 ConWorld, 1 ChosenLost, 3 AbWorld0 
check rab_req for 8 but 2 ConWorld, 1 ChosenLost, 3 AbWorld0 
check rab_val for 8 but 2 ConWorld, 1 ChosenLost, 2 AbWorld0 
check rab_ack for 8 but 2 ConWorld, 1 ChosenLost, 2 AbWorld0 
check rab_readExceptionLog for 8 but 2 ConWorld, 1 ChosenLost, 2 AbWorld0 
check rab_clearExceptionLog for 8 but 2 ConWorld, 1 ChosenLost, 2 AbWorld0 
check rab_archive for 8 but 2 ConWorld, 1 ChosenLost, 2 AbWorld0