module Certifier (runCertifier) where

import FFI.AgdaUnparse (agdaUnparse)
import FFI.SimplifierTrace (mkFfiSimplifierTrace)
import FFI.Untyped (UTerm)

import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Transform.Simplifier

import MAlonzo.Code.VerifiedCompilation (runCertifierMain)

-- | Run the Agda certifier on the simplification trace, if requested
runCertifier
  :: Maybe String
  -- ^ Should we run the Agda certifier? If so, what should the certificate file be called?
  -> SimplifierTrace UPLC.Name UPLC.DefaultUni UPLC.DefaultFun a
  -- ^ The trace produced by the simplification process
  -> IO ()
runCertifier :: forall a.
Maybe String
-> SimplifierTrace Name DefaultUni DefaultFun a -> IO ()
runCertifier (Just String
certName) SimplifierTrace Name DefaultUni DefaultFun a
simplTrace = do
  let rawAgdaTrace :: [(SimplifierStage, (UTerm, UTerm))]
rawAgdaTrace = SimplifierTrace Name DefaultUni DefaultFun a
-> [(SimplifierStage, (UTerm, UTerm))]
forall a.
SimplifierTrace Name DefaultUni DefaultFun a
-> [(SimplifierStage, (UTerm, UTerm))]
mkFfiSimplifierTrace SimplifierTrace Name DefaultUni DefaultFun a
simplTrace
  case [(SimplifierStage, (UTerm, UTerm))] -> T_Maybe_10 () Bool
runCertifierMain [(SimplifierStage, (UTerm, UTerm))]
rawAgdaTrace of
    Just Bool
True ->
      String -> IO ()
putStrLn String
"The compilation was successfully certified."
    Just Bool
False ->
      String -> IO ()
putStrLn
        String
"The compilation was not successfully certified. \
        \Please open a bug report at https://www.github.com/IntersectMBO/plutus \
        \and attach the faulty certificate."
    T_Maybe_10 () Bool
Nothing ->
      String -> IO ()
putStrLn
        String
"The certifier was unable to check the compilation. \
        \Please open a bug report at https://www.github.com/IntersectMBO/plutus."
  String -> String -> IO ()
writeFile (String
certName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".agda") (String -> [(SimplifierStage, (UTerm, UTerm))] -> String
rawCertificate String
certName [(SimplifierStage, (UTerm, UTerm))]
rawAgdaTrace)
runCertifier Maybe String
Nothing SimplifierTrace Name DefaultUni DefaultFun a
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

rawCertificate :: String -> [(SimplifierStage, (UTerm, UTerm))] -> String
rawCertificate :: String -> [(SimplifierStage, (UTerm, UTerm))] -> String
rawCertificate String
certName [(SimplifierStage, (UTerm, UTerm))]
rawTrace =
  String
"module " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
certName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" where\
  \\n\
  \\nopen import VerifiedCompilation\
  \\nopen import VerifiedCompilation.Certificate\
  \\nopen import Untyped\
  \\nopen import RawU\
  \\nopen import Builtin\
  \\nopen import Data.Unit\
  \\nopen import Data.Nat\
  \\nopen import Data.Integer\
  \\nopen import Utils\
  \\nimport Agda.Builtin.Bool\
  \\nimport Relation.Nullary\
  \\nimport VerifiedCompilation.UntypedTranslation\
  \\nopen import Agda.Builtin.Maybe\
  \\nopen import Data.Empty using (⊥)\
  \\nopen import Data.Bool.Base using (Bool; false; true)\
  \\nopen import Agda.Builtin.Equality using (_≡_; refl)\
  \\n\
  \\nasts : List (SimplifierTag × Untyped × Untyped)\
  \\nasts = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [(SimplifierStage, (UTerm, UTerm))] -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse [(SimplifierStage, (UTerm, UTerm))]
rawTrace String -> String -> String
forall a. Semigroup a => a -> a -> a
<>
  String
"\n\
  \\ncertificate : passed? (runCertifier asts) ≡ true\
  \\ncertificate = refl\
  \\n"