1  
  2  -- | See <https://docs.circom.io/circom-language/basic-operators> for the official
  3  -- semantics of the operations
  4  
  5  {-# LANGUAGE StrictData, DeriveFunctor #-}
  6  module Semantics where
  7  
  8  --------------------------------------------------------------------------------
  9  
 10  import Data.Bits
 11  
 12  import BN254
 13  import Misc
 14  
 15  --------------------------------------------------------------------------------
 16  
 17  data PrimOp a
 18    -- unary
 19    = Neg  a
 20    | Id   a
 21    | Lnot a
 22    | Bnot a
 23    -- binary
 24    | Mul  a a
 25    | Div  a a
 26    | Add  a a
 27    | Sub  a a
 28    | Pow  a a
 29    | Idiv a a
 30    | Mod  a a
 31    | Eq_  a a
 32    | Neq  a a
 33    | Lt   a a
 34    | Gt   a a
 35    | Leq  a a
 36    | Geq  a a
 37    | Land a a
 38    | Lor  a a
 39    | Shl  a a
 40    | Shr  a a
 41    | Bor  a a
 42    | Band a a
 43    | Bxor a a
 44    -- ternary
 45    | Cond a a a
 46    deriving (Show,Functor)
 47  
 48  --------------------------------------------------------------------------------
 49  
 50  evalPrimOp :: PrimOp F -> F
 51  evalPrimOp prim = case prim of
 52    Neg  x     -> neg x
 53    Id   x     -> x
 54    Lnot x     -> fromBool (not (toBool x))
 55    Bnot x     -> toF (fieldMask .&. (negate (fromF x) - 1)) 
 56    Mul  x y   -> mul x y
 57    Div  x y   -> BN254.div x y
 58    Add  x y   -> add x y
 59    Sub  x y   -> sub x y
 60    Pow  x y   -> pow x (fromF y)
 61    Idiv x y   -> if isZero y then 0 else toF $ Prelude.div (fromF x) (fromF y)
 62    Mod  x y   -> if isZero y then 0 else toF $ Prelude.mod (fromF x) (fromF y)
 63    Eq_  x y   -> fromBool (x == y)
 64    Neq  x y   -> fromBool (x /= y)
 65    Lt   x y   -> fromBool (signedFromF x <  signedFromF y)
 66    Gt   x y   -> fromBool (signedFromF x >  signedFromF y)
 67    Leq  x y   -> fromBool (signedFromF x <= signedFromF y)
 68    Geq  x y   -> fromBool (signedFromF x >= signedFromF y)
 69    Land x y   -> fromBool (toBool x && toBool y)
 70    Lor  x y   -> fromBool (toBool x || toBool y)
 71    Shl  x y   -> shiftLeft  x (fromF y)
 72    Shr  x y   -> shiftRight x (fromF y)
 73    Bor  x y   -> toF (fromF x  .|.  fromF y)
 74    Band x y   -> toF (fromF x  .&.  fromF y)
 75    Bxor x y   -> toF (fromF x `xor` fromF y) 
 76    Cond b x y -> if toBool b then x else y
 77  
 78  --------------------------------------------------------------------------------
 79  
 80  fieldMask :: Integer
 81  fieldMask = shiftL 1 fieldBits - 1
 82  
 83  fieldBits :: Int
 84  fieldBits = ceilingLog2 fieldPrime
 85  
 86  shiftRight :: F -> Integer -> F
 87  shiftRight (MkF x) k = if k < halfPrimePlus1
 88    then if k > fromIntegral fieldBits 
 89      then 0 
 90      else MkF (shiftR x (fromInteger k))
 91    else shiftLeft (MkF x) (fieldPrime - k)
 92  
 93  shiftLeft :: F -> Integer -> F
 94  shiftLeft (MkF x) k = if k < halfPrimePlus1
 95    then if k > fromIntegral fieldBits
 96      then 0
 97      else toF (shiftL x (fromIntegral k) .&. fieldMask)
 98    else shiftRight (MkF x) (fieldPrime - k)
 99  
100  --------------------------------------------------------------------------------
101  
102  {-
103  notYet :: a
104  notYet = error "not yet implemented"
105  -}