{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}

module Evaluation.Builtins.BLS12_381.Utils
where

import Evaluation.Builtins.Common

import PlutusCore qualified as PLC
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultBuiltinCostModelForTesting)
import PlutusCore.MkPlc (builtin, mkConstant, mkIterAppNoAnn)
import PlutusPrelude (def)
import UntypedPlutusCore qualified as UPLC

import Data.Bits (complement, xor, (.&.), (.|.))
import Data.ByteString as BS (ByteString, cons, uncons)
import Data.Word (Word8)

-- PLC utilities

-- Evaluating PLC terms

type PlcTerm = PLC.Term PLC.TyName PLC.Name PLC.DefaultUni PLC.DefaultFun ()
type PlcError = PLC.Error PLC.DefaultUni PLC.DefaultFun ()
type UplcTerm = UPLC.Term PLC.Name PLC.DefaultUni PLC.DefaultFun ()

data CekResult =
    TypeCheckError PlcError
  | CekError
  | CekSuccess UplcTerm
    deriving stock (CekResult -> CekResult -> Bool
(CekResult -> CekResult -> Bool)
-> (CekResult -> CekResult -> Bool) -> Eq CekResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CekResult -> CekResult -> Bool
== :: CekResult -> CekResult -> Bool
$c/= :: CekResult -> CekResult -> Bool
/= :: CekResult -> CekResult -> Bool
Eq, Int -> CekResult -> ShowS
[CekResult] -> ShowS
CekResult -> String
(Int -> CekResult -> ShowS)
-> (CekResult -> String)
-> ([CekResult] -> ShowS)
-> Show CekResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CekResult -> ShowS
showsPrec :: Int -> CekResult -> ShowS
$cshow :: CekResult -> String
show :: CekResult -> String
$cshowList :: [CekResult] -> ShowS
showList :: [CekResult] -> ShowS
Show)

evalTerm :: PlcTerm -> CekResult
evalTerm :: PlcTerm -> CekResult
evalTerm PlcTerm
term =
    case BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> PlcTerm
-> Either
     (Error DefaultUni DefaultFun ()) (EvaluationResult UplcTerm)
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
typecheckEvaluateCekNoEmit BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def BuiltinCostModel
CostingPart DefaultUni DefaultFun
defaultBuiltinCostModelForTesting PlcTerm
term
    of Left Error DefaultUni DefaultFun ()
e -> Error DefaultUni DefaultFun () -> CekResult
TypeCheckError Error DefaultUni DefaultFun ()
e
       Right EvaluationResult UplcTerm
x  ->
           case EvaluationResult UplcTerm
x of
             EvaluationResult UplcTerm
PLC.EvaluationFailure   -> CekResult
CekError
             PLC.EvaluationSuccess UplcTerm
s -> UplcTerm -> CekResult
CekSuccess UplcTerm
s

-- Constructing PLC constants and applications

uplcTrue :: CekResult
uplcTrue :: CekResult
uplcTrue = UplcTerm -> CekResult
CekSuccess (UplcTerm -> CekResult) -> UplcTerm -> CekResult
forall a b. (a -> b) -> a -> b
$ () -> Bool -> UplcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Bool
True

uplcFalse :: CekResult
uplcFalse :: CekResult
uplcFalse = UplcTerm -> CekResult
CekSuccess (UplcTerm -> CekResult) -> UplcTerm -> CekResult
forall a b. (a -> b) -> a -> b
$ () -> Bool -> UplcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Bool
False

integer :: Integer -> PlcTerm
integer :: Integer -> PlcTerm
integer = () -> Integer -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant ()

bytestring :: ByteString -> PlcTerm
bytestring :: ByteString -> PlcTerm
bytestring = () -> ByteString -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant ()

mkApp1 :: PLC.DefaultFun -> PlcTerm -> PlcTerm
mkApp1 :: DefaultFun -> PlcTerm -> PlcTerm
mkApp1 DefaultFun
b PlcTerm
x = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
b) [PlcTerm
x]

mkApp2 :: PLC.DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 :: DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
b PlcTerm
x PlcTerm
y = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
b) [PlcTerm
x,PlcTerm
y]

{- | ByteString utilities.  These are used in tests to check that the format of
   compressed points conforms to the specification at
   https://github.com/supranational/blst#serialization-format . -}

-- The most signiificant bit of a serialised curve point is set if the
-- serialised point is in compressed form (x-coordinate only)
compressionBit :: Word8
compressionBit :: Word8
compressionBit = Word8
0x80

-- The second most significant bit is set if and only if the point is the point
-- at infinity (the zero of the group); if it is set, all other bits should be zero.
infinityBit :: Word8
infinityBit :: Word8
infinityBit = Word8
0x40

-- The third most significant bit of a compressed point denotes the "sign" of
-- the y-coordinate of the associated point: it is set if and only if the point
-- is not the point at infinity and the y-coordinate is the lexicographically
-- larger one with the given x coordinate.
signBit :: Word8
signBit :: Word8
signBit = Word8
0x20

unsafeUnconsBS :: ByteString -> (Word8, ByteString)
unsafeUnconsBS :: ByteString -> (Word8, ByteString)
unsafeUnconsBS ByteString
b =
    case ByteString -> Maybe (Word8, ByteString)
BS.uncons ByteString
b of
      Maybe (Word8, ByteString)
Nothing -> String -> (Word8, ByteString)
forall a. HasCallStack => String -> a
error String
"Tried to uncons empty bytestring"
      Just (Word8, ByteString)
p  -> (Word8, ByteString)
p

-- | Apply some function to the most significant byte of a bytestring
modifyMSB :: (Word8 -> Word8) -> ByteString -> ByteString
modifyMSB :: (Word8 -> Word8) -> ByteString -> ByteString
modifyMSB Word8 -> Word8
f ByteString
s =
    let (Word8
w,ByteString
rest) = ByteString -> (Word8, ByteString)
unsafeUnconsBS ByteString
s
    in Word8 -> ByteString -> ByteString
BS.cons (Word8 -> Word8
f Word8
w) ByteString
rest

-- | Flip a specified set of bits in the most significant byte of a bytestring.
flipBits :: Word8 -> ByteString -> ByteString
flipBits :: Word8 -> ByteString -> ByteString
flipBits Word8
mask = (Word8 -> Word8) -> ByteString -> ByteString
modifyMSB (Word8
mask Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
`xor`)

-- | Clear a specified set of bits in the most significant byte of a bytestring.
clearBits :: Word8 -> ByteString -> ByteString
clearBits :: Word8 -> ByteString -> ByteString
clearBits Word8
mask = (Word8 -> Word8) -> ByteString -> ByteString
modifyMSB ((Word8 -> Word8
forall a. Bits a => a -> a
complement Word8
mask) Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.&.)

-- | Set a specified set of bits in the most significant byte of a bytestring.
setBits :: Word8 -> ByteString -> ByteString
setBits :: Word8 -> ByteString -> ByteString
setBits Word8
mask = (Word8 -> Word8) -> ByteString -> ByteString
modifyMSB (Word8
mask Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|.)

-- | Check that a specified set of bits is set in the most significant byte of a
-- bytestring.
isSet :: Word8 -> ByteString -> Bool
isSet :: Word8 -> ByteString -> Bool
isSet Word8
mask ByteString
s =
    let (Word8
w,ByteString
_) = ByteString -> (Word8, ByteString)
unsafeUnconsBS ByteString
s
    in Word8
w Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.&. Word8
mask Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
mask