]> Git — Sourcephile - majurity.git/blob - hjugement-protocol/Protocol/Election.hs
protocol: change F to be a Natural, not an Integer.
[majurity.git] / hjugement-protocol / Protocol / Election.hs
1 {-# LANGUAGE GADTs #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE OverloadedStrings #-}
4 module Protocol.Election where
5
6 import Control.Monad (Monad(..), mapM, forM, join, sequence)
7 import Data.Bool
8 import Data.Eq (Eq(..))
9 import Data.Foldable (Foldable, foldMap, and, toList)
10 import Data.Function (($), (.))
11 import Data.Functor (Functor(..), (<$>))
12 import Data.Int (Int)
13 import Data.Map.Strict (Map)
14 import Data.Maybe (Maybe(..), fromJust)
15 import Data.Monoid (Monoid(..))
16 import Data.Ord (Ord(..), Ordering(..))
17 import Data.Proxy (Proxy(..))
18 import Data.Semigroup (Semigroup(..))
19 import Data.String (IsString(..))
20 import Data.Text (Text)
21 import Data.Tuple (fst, snd, curry)
22 import GHC.TypeNats
23 import Numeric.Natural (Natural)
24 import Prelude (Integral, fromIntegral, undefined, error, min)
25 import Text.Show (Show(..))
26 import qualified Control.Monad.Trans.State.Strict as S
27 import qualified Data.ByteString as BS
28 import qualified Data.List as List
29 import qualified Data.Map.Strict as Map
30 import qualified Data.Text.Encoding as Text
31
32 import Protocol.Arithmetic
33 import Utils.MeasuredList as ML
34 import qualified Utils.Natural as Nat
35 import qualified Utils.Constraint as Constraint
36
37 -- * Type 'Encryption'
38 -- | ElGamal-like encryption.
39 data Encryption q = Encryption
40 { encryption_nonce :: G q
41 -- ^ Public part of the random 'secNonce': @('groupGen''^'r)@
42 , encryption_vault :: G q
43 -- ^ Encrypted opinion: @('pubKey''^'r '*' 'groupGen''^'opinion)@
44 } deriving (Eq,Show)
45
46 -- | Additive homomorphism.
47 -- Using the fact that: @'groupGen''^'x '*' 'groupGen''^'y '==' 'groupGen''^'(x'+'y)@.
48 instance SubGroup q => Additive (Encryption q) where
49 zero = Encryption one one
50 x+y = Encryption
51 (encryption_nonce x * encryption_nonce y)
52 (encryption_vault x * encryption_vault y)
53
54 type PublicKey = G
55 type SecretKey = E
56 type SecretNonce = E
57 type ZKP = BS.ByteString
58
59 -- ** Type 'Opinion'
60 -- | Index of a 'Disjunction' within a 'ML.MeasuredList' of them.
61 -- It is encoded as an 'E'xponent in 'encrypt'.
62 type Opinion = Nat.Index
63
64 -- | @(encrypt pubKey opinion)@ returns an ElGamal-like 'Encryption'.
65 --
66 -- WARNING: the secret nonce is returned alongside the 'Encryption'
67 -- in order to prove the validity of the encrypted content in 'nizkProof',
68 -- but this secret nonce MUST be forgotten after that,
69 -- as it may be used to decipher the 'Encryption'
70 -- without the secret key associated with 'pubKey'.
71 encrypt ::
72 Monad m => RandomGen r => SubGroup q =>
73 PublicKey q -> Opinion ds ->
74 S.StateT r m (SecretNonce q, Encryption q)
75 encrypt pubKey (Nat.Index o) = do
76 let opinion = inE (natVal o)
77 secNonce <- random
78 -- NOTE: preserve the 'secNonce' for 'nizkProof'.
79 return $ (secNonce,)
80 Encryption
81 { encryption_nonce = groupGen^secNonce
82 , encryption_vault = pubKey ^secNonce * groupGen^opinion
83 -- NOTE: pubKey == groupGen ^ secKey
84 -- NOTE: 'opinion' is put as exponent in order
85 -- to make an additive homomorphism
86 -- instead of a multiplicative homomorphism.
87 }
88
89 -- * Type 'Signature'
90 type Signature q = (PublicKey q, Proof q)
91
92 -- * Type 'Proof'
93 data Proof q = Proof
94 { proof_challenge :: Challenge q
95 , proof_response :: E q
96 } deriving (Eq,Show)
97
98 -- ** Type 'Challenge'
99 type Challenge = E
100 -- ** Type 'Oracle'
101 type Oracle q = [Commitment q] -> Challenge q
102
103 -- | Fiat-Shamir transformation
104 -- of an interactive zero-knowledge (IZK) proof
105 -- into a non-interactive zero-knowledge (NIZK) proof.
106 nizkProof ::
107 Monad m => RandomGen r => SubGroup q =>
108 SecretNonce q -> [Commitment q] -> Oracle q -> S.StateT r m (Proof q)
109 nizkProof secNonce commits oracle = do
110 nonce <- random
111 let commitments = (^ nonce) <$> commits
112 let proof_challenge = oracle commitments
113 return Proof
114 { proof_challenge
115 , proof_response = nonce + secNonce*proof_challenge
116 }
117
118 -- ** Type 'Commitment'
119 type Commitment = G
120
121 -- ** Type 'Disjunction'
122 -- | A 'Disjunction' is an 'inv'ersed @'groupGen''^'opinion@
123 -- it's used in 'proveEncryption' to generate a 'Proof'
124 -- that an 'encryption_vault' contains a given @'groupGen''^'opinion@,
125 type Disjunction = G
126
127 validBool :: SubGroup q => ML.MeasuredList 2 (Disjunction q)
128 validBool = fromJust $ ML.fromList $ List.take 2 groupGenInverses
129
130 validRange ::
131 forall q mini maxi proxy.
132 SubGroup q =>
133 Bounds mini maxi ->
134 ML.MeasuredList (maxi-mini) (Disjunction q)
135 validRange Bounds{}
136 | Constraint.Proof <- (Nat.<=) @mini @maxi =
137 fromJust $
138 ML.fromList $
139 List.genericTake (Nat.nat @(maxi-mini)) $
140 List.genericDrop (Nat.nat @mini) $
141 groupGenInverses
142
143 -- ** Type 'ValidityProof'
144 -- | A list of 'Proof' to prove that the 'Opinion' within an 'Encryption'
145 -- is indexing a 'Disjunction' within a list of them,
146 -- without knowing which 'Opinion' it is.
147 newtype ValidityProof n q = ValidityProof (ML.MeasuredList n (Proof q))
148 deriving (Eq,Show)
149
150 encryptionStatement :: SubGroup q => ZKP -> Encryption q -> BS.ByteString
151 encryptionStatement zkp Encryption{..} =
152 "prove|"<>zkp<>"|"<>
153 fromString (show (natG encryption_nonce))<>","<>
154 fromString (show (natG encryption_vault))<>"|"
155
156 proveEncryption ::
157 forall ds m r q.
158 Nat.Known ds =>
159 Monad m => RandomGen r => SubGroup q =>
160 PublicKey q -> ZKP ->
161 ML.MeasuredList ds (Disjunction q) -> Opinion ds ->
162 (SecretNonce q, Encryption q) ->
163 S.StateT r m (ValidityProof ds q)
164 proveEncryption pubKey zkp valids
165 (Nat.Index (o::Proxy o))
166 (secNonce, enc@Encryption{..})
167 -- NOTE: the 'Constraint.Proof's below are needed to prove
168 -- that the returned 'ValidityProof' has the same length
169 -- than the given list of 'Disjunction's.
170 | Constraint.Proof <- (Nat.+<=) @o @1 @ds -- prove that o+1<=ds implies 1<=ds-o and o<=ds
171 , Constraint.Proof <- (Nat.<=) @o @ds -- prove that o<=ds implies ds-o is a Natural and o+(ds-o) ~ ds
172 , Constraint.Proof <- (Nat.<=) @1 @(ds-o) -- prove that ((ds-o)-1)+1 ~ ds-o
173 = do
174 let (prevDisjs, _indexedDisj:#nextDisjs) = ML.splitAt o valids
175 prevFakes <- fakeProof `mapM` prevDisjs
176 nextFakes <- fakeProof `mapM` nextDisjs
177 let challengeSum =
178 neg $
179 sum (proof_challenge . fst <$> prevFakes) +
180 sum (proof_challenge . fst <$> nextFakes)
181 genuineProof <- nizkProof secNonce [groupGen, pubKey] $
182 -- | 'Oracle'
183 \nizkCommitments ->
184 let commitments =
185 foldMap snd prevFakes <>
186 nizkCommitments <>
187 foldMap snd nextFakes in
188 -- NOTE: this is a so-called strong Fiat-Shamir transformation (not a weak):
189 -- because the statement is included in the hash (not only the commitments).
190 hash (encryptionStatement zkp enc) commitments + challengeSum
191 return $
192 ValidityProof $
193 ML.concat
194 (fst <$> prevFakes)
195 (ML.cons genuineProof (fst <$> nextFakes))
196 where
197 fakeProof :: Disjunction q -> S.StateT r m (Proof q, [Commitment q])
198 fakeProof disj = do
199 proof_challenge <- random
200 proof_response <- random
201 let commitments =
202 [ groupGen^proof_response / encryption_nonce ^proof_challenge
203 , pubKey ^proof_response / (encryption_vault*disj)^proof_challenge
204 ]
205 return (Proof{..}, commitments)
206
207 validateEncryption ::
208 SubGroup q =>
209 PublicKey q -> ZKP ->
210 ML.MeasuredList n (Disjunction q) ->
211 (Encryption q, ValidityProof n q) -> Bool
212 validateEncryption pubKey zkp disjs (enc@Encryption{..}, ValidityProof proofs) =
213 hash (encryptionStatement zkp enc) commitments == challengeSum
214 where
215 challengeSum = sum (proof_challenge <$> proofs)
216 commitments = foldMap commitment (ML.zip disjs proofs)
217 where commitment (disj, Proof{..}) =
218 -- g = groupGen
219 -- h = pubKey
220 -- y1 = encryption_nonce
221 -- y2 = (encryption_vault * disj)
222 -- com1 = g^res / y1 ^ ch
223 -- com2 = h^res / y2 ^ ch
224 [ groupGen^proof_response / encryption_nonce ^proof_challenge
225 , pubKey ^proof_response / (encryption_vault*disj)^proof_challenge
226 ]
227
228 -- * Type 'Question'
229 data Question choices (mini::Nat) (maxi::Nat) q =
230 Question
231 { question_text :: Text
232 , question_answers :: ML.MeasuredList choices Text
233 , question_bounds :: Bounds mini maxi
234 -- , question_blank :: Maybe Bool
235 } deriving (Eq, Show)
236
237 -- ** Type 'Bounds'
238 data Bounds mini maxi =
239 ((mini<=maxi), Nat.Known mini, Nat.Known maxi) =>
240 Bounds (Proxy mini) (Proxy maxi)
241 instance Show (Bounds mini maxi)
242 instance Eq (Bounds mini maxi)
243
244 -- * Type 'Answer'
245 data Answer choices mini maxi q = Answer
246 { answer_opinions :: ML.MeasuredList choices (Encryption q, ValidityProof 2 q)
247 -- ^ Encrypted 'Opinion' for each 'question_answers'
248 -- with a 'ValidityProof' that they belong to [0,1].
249 , answer_sumProof :: ValidityProof (maxi-mini) q
250 -- ^ Proofs that the sum of the 'Opinon's encrypted in 'answer_opinions'
251 -- is an element of ['mini'..'maxi'].
252 -- , answer_blankProof ::
253 } deriving (Eq,Show)
254
255 -- | @(answer pubKey zkp quest opinions)@
256 -- returns a validable 'Answer',
257 -- unless the given 'opinions' do not respect 'question_bounds'.
258 answer ::
259 forall m r q mini maxi choices.
260 Monad m => RandomGen r => SubGroup q =>
261 PublicKey q -> ZKP ->
262 Question choices mini maxi q ->
263 ML.MeasuredList choices (Opinion 2) ->
264 S.StateT r m (Maybe (Answer choices mini maxi q))
265 answer pubKey zkp Question{..} opinions
266 | Bounds{} <- question_bounds
267 , SomeNat (opinionsSum::Proxy opinionsSum) <-
268 someNatVal $ sum $ (\(Nat.Index o) -> natVal o) <$> opinions
269 -- prove that opinionsSum-mini is a Natural
270 , Just Constraint.Proof <- (Nat.<=?) @mini @opinionsSum
271 -- prove that (opinionsSum-mini)+1 is a Natural
272 , Constraint.Proof <- (Nat.+) @(opinionsSum-mini) @1
273 -- prove that maxi-mini is a Natural
274 , Constraint.Proof <- (Nat.<=) @mini @maxi
275 -- prove that (opinionsSum-mini)+1 <= maxi-mini
276 , Just Constraint.Proof <- (Nat.<=?) @((opinionsSum-mini)+1) @(maxi-mini)
277 = do
278 encryptions <- encrypt pubKey `mapM` opinions
279 individualProofs <-
280 sequence $ ML.zipWith
281 (proveEncryption pubKey zkp validBool)
282 opinions encryptions
283 sumProof <-
284 proveEncryption pubKey zkp
285 (validRange question_bounds)
286 (Nat.Index $ Proxy @(opinionsSum-mini))
287 ( sum (fst <$> encryptions)
288 , sum (snd <$> encryptions) )
289 return $ Just Answer
290 { answer_opinions = ML.zip
291 (snd <$> encryptions) -- NOTE: drop secNonce
292 individualProofs
293 , answer_sumProof = sumProof
294 }
295 | otherwise = return Nothing
296
297 validateAnswer ::
298 SubGroup q =>
299 PublicKey q -> ZKP ->
300 Question choices mini maxi q ->
301 Answer choices mini maxi q -> Bool
302 validateAnswer pubKey zkp Question{..} Answer{..} =
303 and (validateEncryption pubKey zkp validBool <$> answer_opinions) &&
304 validateEncryption pubKey zkp
305 (validRange question_bounds)
306 ( sum (fst <$> answer_opinions)
307 , answer_sumProof )
308
309 -- * Type 'Election'
310 data Election quests choices mini maxi q = Election
311 { election_name :: Text
312 , election_description :: Text
313 , election_publicKey :: PublicKey q
314 , election_questions :: ML.MeasuredList quests (Question choices mini maxi q)
315 , election_uuid :: UUID
316 , election_hash :: Hash
317 } deriving (Eq,Show)
318
319 -- ** Type 'UUID'
320 newtype UUID = UUID Text
321 deriving (Eq,Ord,Show)
322
323 -- ** Type 'Hash'
324 newtype Hash = Hash Text
325 deriving (Eq,Ord,Show)
326
327 -- * Type 'Ballot'
328 data Ballot quests choices mini maxi q = Ballot
329 { ballot_answers :: ML.MeasuredList quests (Answer choices mini maxi q)
330 , ballot_signature :: Maybe (Signature q)
331 , ballot_election_uuid :: UUID
332 , ballot_election_hash :: Text
333 }