1  
  2  {-# LANGUAGE BlockArguments #-}
  3  module Semantics where
  4  
  5  --------------------------------------------------------------------------------
  6  
  7  import Prelude hiding (div)
  8  import Control.Monad
  9  import System.Random
 10  
 11  --------------------------------------------------------------------------------
 12  
 13  type F    = Int
 14  type FExt = (F,F)
 15  
 16  fieldPrime :: Int
 17  fieldPrime = 2^8 - 2^4 + 1
 18  
 19  modp :: Int -> F
 20  modp x = mod x fieldPrime
 21  
 22  --------------------------------------------------------------------------------
 23  
 24  neg :: F -> F
 25  neg 0 = 0
 26  neg x = fieldPrime - x
 27  
 28  add :: F -> F -> F
 29  add x y = modp (x + y)
 30  
 31  sub :: F -> F -> F
 32  sub x y = modp (x - y)
 33  
 34  mul :: F -> F -> F
 35  mul x y = modp (x * y)
 36  
 37  sqr :: F -> F 
 38  sqr x = mul x x
 39  
 40  mul3 :: F -> F -> F -> F
 41  mul3 x y z = mul (mul x y) z
 42  
 43  pow :: F -> Int -> F
 44  pow x0 expo
 45    | expo < 0  = error "pow: negative exponent"
 46    | expo == 0 = 1
 47    | otherwise = go 1 x0 expo
 48    where
 49      go acc s 0 = acc
 50      go acc s e = case divMod e 2 of
 51        (e', 0) -> go      acc    (sqr s) e'
 52        (e' ,1) -> go (mul acc s) (sqr s) e'
 53  
 54  inv :: F -> F
 55  inv x = pow x (fieldPrime - 2)      
 56  
 57  div :: F -> F -> F
 58  div x y = mul x (inv y)
 59  
 60  --------------------------------------------------------------------------------
 61  
 62  negExt :: FExt -> FExt
 63  negExt (r,i) = (neg r, neg i)
 64  
 65  addExt :: FExt -> FExt -> FExt
 66  addExt (r1,i1) (r2,i2) = (add r1 r2, add i1 i2)
 67  
 68  subExt :: FExt -> FExt -> FExt
 69  subExt (r1,i1) (r2,i2) = (sub r1 r2, sub i1 i2)
 70  
 71  mulExt :: FExt -> FExt -> FExt
 72  mulExt (r1,i1) (r2,i2) = (r3,i3) where
 73    r3 = (mul r1 r2) `add` (mul3 7 i1 i2) 
 74    i3 = (mul r1 i2) `add` (mul i1 r2)
 75  
 76  sqrExt :: FExt -> FExt 
 77  sqrExt x = mulExt x x
 78  
 79  powExt :: FExt -> Int -> FExt
 80  powExt x0 expo
 81    | expo < 0  = error "pow: negative exponent"
 82    | expo == 0 = (1,0)
 83    | otherwise = go (1,0) x0 expo
 84    where
 85      go acc s 0 = acc
 86      go acc s e = case divMod e 2 of
 87        (e', 0) -> go         acc    (sqrExt s) e'
 88        (e' ,1) -> go (mulExt acc s) (sqrExt s) e'
 89  
 90  invExt :: FExt -> FExt
 91  invExt (r,i) = (r `mul` z , neg i `mul` z) where 
 92    denom = (sqr r) `sub` (mul3 7 i i)
 93    z = inv denom
 94  
 95  divExt :: FExt -> FExt -> FExt
 96  divExt x y = mulExt x (invExt y)
 97  
 98  --------------------------------------------------------------------------------
 99  -- some quick & dirty testing
100  
101  data Prop a 
102    = Prop1 String (a -> Bool)
103    | Prop2 String (a -> a -> Bool)
104    | Prop3 String (a -> a -> a -> Bool)
105  
106  propName :: Prop a -> String
107  propName prop = case prop of
108    Prop1 name _ -> name
109    Prop2 name _ -> name
110    Prop3 name _ -> name
111  
112  some_properties :: [Prop F]
113  some_properties = 
114    [ Prop2 "add-sub" \x y   -> add (sub x y) y == x 
115    , Prop2 "add-neg" \x y   -> sub x y == add x (neg y)
116    , Prop1 "inv-mul" \x     -> x == 0 || inv x `mul` x == 1
117    , Prop1 "inv-pow" \x     -> inv x == pow x (fieldPrime - 2)
118    , Prop2 "mul-div" \x y   -> y == 0 || mul (div x y) y == x 
119    , Prop3 "mul-add" \x y z -> mul (add x y) z == mul x z `add` mul y z 
120    , Prop1 "mul-pow" \x     -> mul (mul x x) x == pow x 3
121    ]
122  
123  some_ext_properties :: [Prop FExt]
124  some_ext_properties = 
125    [ Prop2 "add-sub" \x y   -> addExt (subExt x y) y == x 
126    , Prop2 "add-neg" \x y   -> subExt x y == addExt x (negExt y)
127    , Prop1 "inv-mul" \x     -> x == (0,0) || invExt x `mulExt` x == (1,0)
128    , Prop1 "inv-pow" \x     -> invExt x == powExt x (fieldPrime^2 - 2)
129    , Prop2 "mul-div" \x y   -> y == (0,0) || mulExt (divExt x y) y == x 
130    , Prop3 "mul-add" \x y z -> mulExt (addExt x y) z == mulExt x z `addExt` mulExt y z 
131    , Prop1 "mul-pow" \x     -> mulExt (mulExt x x) x == powExt x 3
132    ]
133  
134  --------------------------------------------------------------------------------
135  
136  runTests :: IO ()
137  runTests = do
138    let n = 1000
139    runTestsBase n
140    runTestsExt  n
141  
142  runTestsBase :: Int -> IO ()
143  runTestsBase n = do
144    putStrLn $ "\nbase field properties"
145    forM_ some_properties $ \prop -> do
146      oks <- replicateM n (runPropF prop) 
147      let good = length (filter id oks)
148      let bad  = if good < n then " - FAILED!" else " - OK."
149      putStrLn $ "  - " ++ propName prop ++ ": " ++ show good ++ " / " ++ show n ++ " passed. " ++ bad 
150  
151  runTestsExt :: Int -> IO ()
152  runTestsExt n = do
153    putStrLn $ "\nextension field properties"
154    forM_ some_ext_properties $ \prop -> do
155      oks <- replicateM n (runPropFExt prop) 
156      let good = length (filter id oks)
157      let bad  = if good < n then " - FAILED!" else " - OK."
158      putStrLn $ "  - " ++ propName prop ++ ": " ++ show good ++ " / " ++ show n ++ " passed. " ++ bad
159  
160  ----------------------------------------
161  
162  rndF :: IO F
163  rndF = randomRIO (0,fieldPrime-1)
164  
165  rndFExt :: IO FExt
166  rndFExt = (,) <$> rndF <*> rndF
167  
168  runPropF :: Prop F -> IO Bool
169  runPropF prop = case prop of
170    Prop1 _ f1 -> f1 <$> rndF
171    Prop2 _ f2 -> f2 <$> rndF <*> rndF
172    Prop3 _ f3 -> f3 <$> rndF <*> rndF <*> rndF
173  
174  runPropFExt :: Prop FExt -> IO Bool
175  runPropFExt prop = case prop of
176    Prop1 _ f1 -> f1 <$> rndFExt
177    Prop2 _ f2 -> f2 <$> rndFExt <*> rndFExt
178    Prop3 _ f3 -> f3 <$> rndFExt <*> rndFExt <*> rndFExt
179  
180  --------------------------------------------------------------------------------