diff --git a/nix/agda.nix b/nix/agda.nix index 9c13969464f..a8599cf41a1 100644 --- a/nix/agda.nix +++ b/nix/agda.nix @@ -124,7 +124,7 @@ rec { agda-project = pkgs.haskell-nix.hackage-project { name = "Agda"; - version = "2.7.0"; + version = "2.7.0.1"; compiler-nix-name = "ghc96"; cabalProjectLocal = "extra-packages: ieee754, filemanip"; modules = [ agda-project-module-patch-default ]; diff --git a/plutus-executables/executables/uplc/Main.hs b/plutus-executables/executables/uplc/Main.hs index fbb24673d01..bb0376958b3 100644 --- a/plutus-executables/executables/uplc/Main.hs +++ b/plutus-executables/executables/uplc/Main.hs @@ -1,9 +1,11 @@ -- editorconfig-checker-disable +{-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -Wno-orphans #-} module Main (main) where +import Control.Exception qualified as E import PlutusCore qualified as PLC import PlutusCore.Annotation (SrcSpan) import PlutusCore.Data (Data) @@ -19,6 +21,8 @@ import PlutusPrelude import Untyped qualified as AgdaFFI +import Data.FileEmbed qualified as FileEmbed +import Debug.Trace (traceM) import UntypedPlutusCore.Evaluation.Machine.SteppableCek.DebugDriver qualified as D import UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal qualified as D @@ -28,14 +32,17 @@ import UntypedPlutusCore.Evaluation.Machine.Cek qualified as Cek import UntypedPlutusCore.Transform.Simplifier import Control.DeepSeq (force) -import Control.Monad.Except (runExcept) +import Control.Monad.Except (catchError, runExcept, throwError) import Control.Monad.IO.Class (liftIO) import Criterion (benchmarkWith, whnf) import Criterion.Main (defaultConfig) import Criterion.Types (Config (..)) +import Data.ByteString.Lazy (ByteString) import Data.ByteString.Lazy as BSL (readFile) import Data.Foldable import Data.List.Split (splitOn) +import Data.Maybe (fromJust) +import Data.Strict.Maybe qualified as Maybe.Strict import Data.Text qualified as T import Flat (unflat) import Options.Applicative @@ -45,6 +52,14 @@ import System.FilePath (()) import System.IO (hPrint, stderr) import Text.Read (readMaybe) +-- import Data.ByteString qualified as BS +-- import Data.ByteString.Lazy qualified as BSL +-- import Data.ByteString.Char8 qualified as BSL8 + +import Data.ByteString qualified as BS +import Data.ByteString.Char8 qualified as BS8 +import Data.ByteString.Lazy qualified as BSL + import Control.Monad.ST (RealWorld) import System.Console.Haskeline qualified as Repl @@ -52,17 +67,36 @@ import Agda.Interaction.Base (ComputeMode (DefaultCompute)) import Agda.Interaction.FindFile qualified as HAgda.File import Agda.Interaction.Imports qualified as HAgda.Imp import Agda.Interaction.Options (CommandLineOptions (optIncludePaths), defaultOptions) +import Agda.Interaction.Options qualified as HAgda.Options import Agda.Syntax.Parser qualified as HAgda.Parser +import Agda.TypeChecking.Serialise qualified as HAgda.Serialise +import Agda.Utils.Trie qualified as HAgda.Trie -import Agda.Compiler.Backend (crInterface, iInsideScope, setCommandLineOptions, setScope) +import Agda.Benchmarking (Phase (Deserialization), billToPure) +import Agda.Compiler.Backend (Interface, TCErr (..), TCM, crInterface, iInsideScope, iScope, + setCommandLineOptions, setScope) import Agda.Interaction.BasicOps (evalInCurrent) import Agda.Main (runTCMPrettyErrors) +import Agda.Syntax.Scope.Base (publicModules) import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract)) import Agda.TypeChecking.Pretty (PrettyTCM (..)) +import Agda.TypeChecking.Serialise.Base +import Agda.TypeChecking.Serialise.Base (runGetState) +import Agda.TypeChecking.Serialise.Instances () import Agda.Utils.FileName qualified as HAgda.File +import Agda.Utils.IO.Binary (readBinaryFile') +import Agda.Utils.Null qualified as Agda.Null import AgdaUnparse (agdaUnparse) +import Codec.Compression.Zlib.Internal qualified as Z +import Data.Binary qualified as B +import Data.Binary.Get qualified as B +import Data.Binary.Put qualified as B +import Data.ByteString.Builder (byteString, toLazyByteString) +import Data.Word +import Debug.Trace (traceShowM) import System.Environment (getEnv) + uplcHelpText :: String uplcHelpText = helpText "Untyped Plutus Core" @@ -136,7 +170,7 @@ benchmarkOpts = ( long "time-limit" <> short 'T' <> metavar "TIME LIMIT" - <> value 5.0 + <> Options.Applicative.value 5.0 <> showDefault <> help "Time limit (in seconds) for benchmarking.") @@ -318,25 +352,114 @@ runAgda certName rawTrace = do Left err -> error $ show err stdlibPath <- getEnv "AGDA_STDLIB_SRC" metatheoryPath <- getEnv "PLUTUS_METHATHEORY_SRC" - inputFile <- HAgda.File.absolute (metatheoryPath "Certifier.agda") + -- let ifacePath = "/home/ana/Workspace/IOG/plutus/plutus-metatheory/_build/2.7.0.1/agda/src" + inputFile <- HAgda.File.absolute ("/home/ana/Workspace/IOG/plutus/agda-interfaces/src/Certifier.agdai") + interfaceDir <- HAgda.File.absolute ("/home/ana/Workspace/IOG/plutus/agda-interfaces/src") + Just ifaceFile <- HAgda.File.mkInterfaceFile inputFile + -- let ifaceFile = HAgda.File.InterfaceFile "/home/ana/Workspace/IOG/plutus/plutus-metatheory/_build/2.7.0.1/agda/src/Certifier.agdai" + -- let embeddedInterfaceFile :: BS.ByteString + -- let embeddedInterfaceFile = BS8.fromStrict $(FileEmbed.embedFile "/home/ana/Workspace/IOG/plutus/plutus-metatheory/_build/2.7.0.1/agda/src/Certifier.agdai") runTCMPrettyErrors $ do let opts = + -- defaultOptions + -- { HAgda.Options.optTraceImports = 42 + -- , HAgda.Options.optPragmaOptions = HAgda.Options.defaultPragmaOptions + -- { HAgda.Options._optVerbose = Maybe.Strict.Just (HAgda.Trie.singleton [] 0) + -- } + -- } defaultOptions - { optIncludePaths = - [ metatheoryPath - , stdlibPath - ] + { HAgda.Options.optAbsoluteIncludePaths = [interfaceDir] + -- [ metatheoryPath "_build/2.7.0.1/agda/src" + -- , stdlibPath "../_build/2.7.0.1/agda/src" + -- ] } + -- traceShowM opts setCommandLineOptions opts - result <- HAgda.Imp.typeCheckMain HAgda.Imp.TypeCheck =<< HAgda.Imp.parseSource (HAgda.File.SourceFile inputFile) - let interface = crInterface result - insideScope = iInsideScope interface + -- aaaa <- HAgda.Imp.parseSource (HAgda.File.SourceFile inputFile) + -- traceM "asasdads" + -- result <- HAgda.Imp.typeCheckMain HAgda.Imp.TypeCheck aaaa + -- let interface = crInterface result + Just interface <- readInterface ifaceFile + -- interface <- HAgda.Serialise.decodeInterface embeddedInterfaceFile + -- traceShowM interface + let insideScope = iInsideScope interface + -- let insideScope = iInsideScope (fromJust interface) setScope insideScope internalisedTrace <- toAbstract parsedTrace decisionProcedureResult <- evalInCurrent DefaultCompute internalisedTrace final <- prettyTCM decisionProcedureResult liftIO $ writeFile (certName ++ ".agda") (show final) +readInterface :: HAgda.File.InterfaceFile -> TCM (Maybe Agda.Compiler.Backend.Interface) +readInterface file = do + let ifp = HAgda.File.filePath $ HAgda.File.intFilePath file + -- Decode the interface file + (s, close) <- liftIO $ readBinaryFile' ifp + do mi <- liftIO . E.evaluate =<< decodeInterface s + + -- Close the file. Note + -- ⑴ that evaluate ensures that i is evaluated to WHNF (before + -- the next IO operation is executed), and + -- ⑵ that decode returns Nothing if an error is encountered, + -- so it is safe to close the file here. + liftIO close + + res <- return $ constructIScope <$> mi + return res + -- Catch exceptions and close + `catchError` \e -> liftIO close >> handler e + -- Catch exceptions + `catchError` handler + where + handler = \case + IOException _ _ e -> do + -- alwaysReportSLn "" 0 $ "IO exception: " ++ show e + return Nothing -- Work-around for file locking bug. + -- TODO: What does this refer to? Please + -- document. + e -> throwError e + +constructIScope :: Interface -> Interface +constructIScope i = billToPure [ Deserialization ] $ + i{ iScope = publicModules $ iInsideScope i } + +currentInterfaceVersion :: B.Word64 +currentInterfaceVersion = 20240629 * 10 + 0 + +decodeInterface :: ByteString -> TCM (Maybe Interface) +decodeInterface s = do + + -- Note that runGetState and the decompression code below can raise + -- errors if the input is malformed. The decoder is (intended to be) + -- strict enough to ensure that all such errors can be caught by the + -- handler here or the one in decode. + + s <- liftIO $ + E.handle (\(E.ErrorCall s) -> return (Left s)) $ + E.evaluate $ + let (ver, s', _) = runGetState B.get (BSL.drop 16 s) 0 in + if ver /= currentInterfaceVersion + then Left "Wrong interface version." + else Right $ + toLazyByteString $ + Z.foldDecompressStreamWithInput + (\s -> (byteString s <>)) + (\s -> if Agda.Null.null s + then mempty + else error "Garbage at end.") + (\err -> error (show err)) + (Z.decompressST Z.gzipFormat Z.defaultDecompressParams) + s' + + case s of + Right s -> do + traceM "hello" + HAgda.Serialise.decode s + Left err -> do + -- reportSLn "import.iface" 5 $ + -- "Error when decoding interface file: " ++ err + return Nothing + ---------------- Script application ---------------- -- | Apply one script to a list of others and output the result. All of the diff --git a/plutus-executables/plutus-executables.cabal b/plutus-executables/plutus-executables.cabal index 9f606005956..9ca95c67a9f 100644 --- a/plutus-executables/plutus-executables.cabal +++ b/plutus-executables/plutus-executables.cabal @@ -103,11 +103,13 @@ executable uplc main-is: uplc/Main.hs hs-source-dirs: executables build-depends: - , Agda ==2.7.0 - , base >=4.9 && <5 - , bytestring + , Agda ==2.7.0.1 + , base >=4.9 && <5 + , binary >=0.8.6.0 && <0.9 + , bytestring >=0.10.8.2 && <0.13 , criterion , deepseq + , file-embed , filepath , flat ^>=0.6 , haskeline @@ -119,7 +121,9 @@ executable uplc , plutus-metatheory , prettyprinter , split + , strict , text + , zlib >=0.6 && <0.8 -- build-tool-depends: Agda:agda diff --git a/plutus-metatheory/src/Main.lagda.md b/plutus-metatheory/src/Main.lagda.md index c091fe80ed1..1ebe41d768c 100644 --- a/plutus-metatheory/src/Main.lagda.md +++ b/plutus-metatheory/src/Main.lagda.md @@ -6,6 +6,7 @@ layout: page module Main where import VerifiedCompilation +import Certifier open import Agda.Builtin.IO using (IO) import IO.Primitive.Core as IO using (return;_>>=_) open import Agda.Builtin.Unit using (⊤;tt)