1 module Voting.Protocol.Arithmetic where
3 import Control.Monad (bind)
4 import Data.Argonaut.Core as JSON
5 import Data.Argonaut.Decode (class DecodeJson, decodeJson)
6 import Data.Argonaut.Encode (class EncodeJson, encodeJson)
7 import Data.Argonaut.Parser as JSON
8 import Data.BigInt (BigInt)
9 import Data.BigInt as BigInt
10 import Data.Boolean (otherwise)
11 import Data.Bounded (class Bounded, top)
12 import Data.Either (Either(..))
13 import Data.Eq (class Eq, (==), (/=))
14 import Data.EuclideanRing (class EuclideanRing, (/), mod)
15 import Data.Foldable (all)
16 import Data.Function (($), identity, (<<<))
17 import Data.Functor ((<$>))
18 import Data.HeytingAlgebra ((&&))
19 import Data.List (List, (:))
20 import Data.List.Lazy as LL
21 import Data.Maybe (Maybe(..), maybe)
22 import Data.Monoid (class Monoid, mempty, (<>))
23 import Data.Newtype (class Newtype, wrap, unwrap)
24 import Data.Ord (class Ord, (<), (<=))
25 import Data.Reflection (class Reifies, reflect)
26 import Data.Ring (class Ring, (-), negate)
27 import Data.Semiring (class Semiring, zero, (+), one, (*))
28 import Data.Show (class Show, show)
29 import Data.String.CodeUnits as String
30 import Effect.Exception.Unsafe (unsafeThrow)
31 import Type.Proxy (Proxy(..))
34 newtype Natural = Natural BigInt
35 instance newtypeNatural :: Newtype Natural BigInt where
37 unwrap (Natural x) = x
38 derive newtype instance eqNatural :: Eq Natural
39 derive newtype instance ordNatural :: Ord Natural
40 derive newtype instance showNatural :: Show Natural
41 derive newtype instance semiringNatural :: Semiring Natural
42 derive newtype instance euclideanRingNatural :: EuclideanRing Natural
44 -- * Class 'FromNatural'
45 class FromNatural a where
46 fromNatural :: Natural -> a
48 -- * Class 'ToNatural'
49 class ToNatural a where
51 instance toNaturalBigInt :: ToNatural Natural where
53 instance toNaturalInt :: ToNatural Int where
54 nat x | 0 <= x = wrap (BigInt.fromInt x)
55 | otherwise = unsafeThrow "nat: given Int is negative"
59 -- | An additive semigroup.
60 class Additive a where
63 instance additiveBigInt :: Additive BigInt where
66 instance additiveNatural :: Additive Natural where
70 -- | `('power' b e)` returns the modular exponentiation of base `b` by exponent `e`.
71 power :: forall crypto c a. Semiring a => a -> E crypto c -> a
72 power x = go <<< unwrap
80 | p `mod` two == zero = let x' = go (p / two) in x' * x'
81 | otherwise = let x' = go (p / two) in x' * x' * x
84 -- * Class 'CryptoParams' where
86 ( EuclideanRing (G crypto c)
87 , FromNatural (G crypto c)
88 , ToNatural (G crypto c)
92 , DecodeJson (G crypto c)
93 , EncodeJson (G crypto c)
95 ) <= CryptoParams crypto c where
96 -- | A generator of the subgroup.
97 groupGen :: G crypto c
98 -- | The order of the subgroup.
99 groupOrder :: Proxy crypto -> Proxy c -> Natural
101 -- | 'groupGenPowers' returns the infinite list
102 -- of powers of 'groupGen'.
103 groupGenPowers :: forall crypto c. CryptoParams crypto c => LL.List (G crypto c)
104 groupGenPowers = go one
105 where go g = g LL.: go (g * groupGen)
107 -- | 'groupGenInverses' returns the infinite list
108 -- of 'inverse' powers of 'groupGen':
109 -- @['groupGen' '^' 'negate' i | i <- [0..]]@,
110 -- but by computing each value from the previous one.
112 -- Used by 'intervalDisjunctions'.
113 groupGenInverses :: forall crypto c. CryptoParams crypto c => LL.List (G crypto c)
114 groupGenInverses = go one
116 invGen = inverse groupGen
117 go g = g LL.: go (g * invGen)
119 inverse :: forall a. EuclideanRing a => a -> a
122 -- ** Class 'ReifyCrypto'
123 class ReifyCrypto crypto where
124 -- | Like 'reify' but augmented with the 'CryptoParams' constraint.
125 reifyCrypto :: forall r. crypto -> (forall c. Reifies c crypto => CryptoParams crypto c => Proxy c -> r) -> r
128 -- | The type of the elements of a subgroup of a field.
129 newtype G crypto c = G Natural
132 -- | An exponent of a (cyclic) subgroup of a field.
133 -- The value is always in @[0..'groupOrder'-1]@.
134 newtype E crypto c = E Natural
135 -- deriving (Eq,Ord,Show)
136 -- deriving newtype NFData
137 derive newtype instance eqE :: Eq (E crypto c)
138 derive newtype instance ordE :: Ord (E crypto c)
139 derive newtype instance showE :: Show (E crypto c)
140 instance newtypeE :: Newtype (E crypto c) Natural where
143 instance additiveE :: CryptoParams crypto c => Additive (E crypto c) where
146 instance semiringE :: CryptoParams crypto c => Semiring (E crypto c) where
148 add (E x) (E y) = E ((x + y) `mod` groupOrder (Proxy::Proxy crypto) (Proxy::Proxy c))
150 mul (E x) (E y) = E ((x * y) `mod` groupOrder (Proxy::Proxy crypto) (Proxy::Proxy c))
151 instance ringE :: CryptoParams crypto c => Ring (E crypto c) where
152 sub (E x) (E y) = E (x + wrap (unwrap (groupOrder (Proxy::Proxy crypto) (Proxy::Proxy c)) - unwrap y))
153 instance fromNaturalE :: CryptoParams crypto c => FromNatural (E crypto c) where
154 fromNatural n = E (n `mod` groupOrder (Proxy::Proxy crypto) (Proxy::Proxy c))
155 instance toNaturalE :: ToNatural (E crypto c) where
157 instance boundedE :: CryptoParams crypto c => Bounded (E crypto c) where
159 top = E $ wrap (unwrap (groupOrder (Proxy::Proxy crypto) (Proxy::Proxy c)) - one)
161 instance enumE :: Reifies c crypto => Enum (E crypto c) where
162 succ z = let z' = z + one in if z' > z then Just z' else Nothing
163 pred z = let z' = z - one in if z' < z then Just z' else Nothing
164 instance boundedEnumE :: Reifies c crypto => BoundedEnum (E crypto c) where
165 cardinality = Cardinality (toInt (undefined :: m) - 1)
166 toEnum x = let z = mkE x in if runE z == x then Just z else Nothing
169 instance encodeJsonE :: EncodeJson (E crypto c) where
170 encodeJson (E n) = encodeJson (show n)
171 instance decodeJsonE :: CryptoParams crypto c => DecodeJson (E crypto c) where
172 decodeJson = JSON.caseJsonString (Left "String") $ \s ->
173 maybe (Left "Exponent") Right $ do
174 {head:c0} <- String.uncons s
175 if c0 /= '0' && all isDigit (String.toCharArray s)
177 n <- Natural <$> BigInt.fromString s
178 if n < groupOrder (Proxy::Proxy crypto) (Proxy::Proxy c)
183 isDigit :: Char -> Boolean
184 isDigit c = case c of