{-|
Module      : ExampleDiningCryptographers
Description : Implementation  of Chaum's Dining Cryptographers algorithm

@n@ agents dine at a round table [Chaum, 1988]. 
The dinner may have been paid by their employer (the NSA), or by one of the agents. 
They execute a protocol to reveal whether one of the agents paid, but without revealing which one. 
The protocol supplies each pair of adjacent agents with a random coin, which can be observed only by that pair. Each agent announces the result of XORing three Booleans: the two coins observable by her and the status of whether she paid for the dinner. The XOR of all announcements is proven to be equal to the disjunction of whether any agent paid.

-}
module ExampleDiningCryptographers where
import Data.Map (Map, fromList, (!))
import Data.SBV
import Data.List
import Logics
import Translation
import ToSBV
import Data.Maybe

-- | @ag i@ characterised by its identity @i@ and its nonobservable variables
ag :: Int -> Agent
ag i = Agent {identity=i, nonobs=(allVars\\(obs i))} 

-- | all variables
allVars :: [Var]
allVars = [varx] ++ concat [[varc i, varp i] | i <- [0 .. (n-1)]] 

-- | observability function, \(ag_i\) observes \(x, p_i, c_i, c_{i+1 \mod n}\), 
obs :: Int -> [Var]
obs i = [varx, varp i, varc i, varc $ (i+1) `mod` n] 

-- | boolean variable \(x\)
varx :: Var
varx = BVar "x" 

-- | boolean expression x
x :: BExpr
x = BValue varx

-- | boolean variable \(c_i\) coin flip between agent i and agent i-1
varc :: Int -> Var
varc i = BVar ("c" ++ show i) 

-- | boolean variable \(p_i\) agent i paid
varp :: Int -> Var
varp i = BVar ("p" ++ show i) 

-- | boolean expression \(p_i\)
p :: Int -> BExpr
p i = BValue $ varp i
 
-- | boolean expression \(c_i\)
c :: Int -> BExpr
c i = BValue $ varc i


-- | \(\phi\) or \(I\) the constraint on the inital states: "that all agents knows that at most one agent paid"
phi :: ModalFormula
phi = Conj [ Imp (Atom (p i)) (Conj [ Neg (Atom (p j)) | j <- ([0 .. i-1] ++ [i+1 ..  (n-1)])]) | i <- [0 .. (n-1)] ] 

-- | the boolean expression to be assigned to \(x\) in the algorithm
bexprDC :: BExpr
bexprDC = Xor [Xor [p i, c i, c $ (i+1) `mod` n] | i <- [0 .. (n-1)]]

-- | the DC algorithm as an assignment to \(x\)
progDC :: Prog              
progDC = BAssign varx bexprDC 

-- | the number of agents
n :: Int 
n = 5 

alpha1 :: ModalFormula
alpha1 = Neg (Atom (p 0)) ⇒ (K (ag 0) (Conj [Neg (Atom (p i)) | i <- [0 .. (n-1)]])   
                            ∨  (Conj [Neg (K (ag 0) (Atom (p i))) | i <- [1 .. (n-1)]])
                            )

-- | an example of Modal Formula to be verified at the end of the DC algorithm
alpha2 :: ModalFormula
alpha2 = K (ag 0) (Atom x ⇔ Disj [Atom (p i) | i <- [0 .. (n-1) ]])

-- | an example of Modal Formula to be verified at the end of the DC algorithm
alpha3 :: ModalFormula
alpha3 = K (ag 0) (Atom (p 1))  

alpha4 :: ModalFormula
alpha4 = K (ag 0) (Atom (p 1) ∨ Atom (p 2))  

dcAlpha1   = toSBV allVars phi (Neg (tau phi (Box progDC alpha1)))
dcAlpha1SP = toSBV allVars (sp phi progDC) (Neg (tau (sp phi progDC) alpha1))

-- | proving \([progDC] \alpha_2\)
dcAlpha2   = toSBV allVars phi (Neg (tau phi (Box progDC alpha2)))
dcAlpha2SP = toSBV allVars (sp phi progDC) (Neg (tau (sp phi progDC) alpha2))
-- -- ^
-- DC with \(\alpha_2\) as in IJCAI paper
--
-- >>> sat dcAlpha2

dcAlpha2'   = toSBV allVars phi (Neg (tau phi (K (ag 0) (Box progDC (Atom x ⇔ Disj [Atom (p i) | i <- [0 .. (n-1) ]])))))


-- | proving \([progDC] \alpha_3\) (should be falsified) 
dcAlpha3    = toSBV allVars phi (Neg (tau phi (Box progDC alpha3)))
dcAlpha3SP  = toSBV allVars (sp phi progDC) (Neg (tau (sp phi progDC) alpha3))
-- ^
-- DC with \(\alpha_3\) as in IJCAI paper
--
-- >>> sat dcAlpha3