CASM serialization

.github/workflows/ci.yml

@@ -92,6 +92,7 @@ jobs:
 
       - name: Add ~/.local/bin to PATH
         run: |
+          mkdir -p "$HOME/.local/bin"
           echo "$HOME/.local/bin" >> $GITHUB_PATH
 
       - name: Install the latest Wasmer version
@@ -118,6 +119,19 @@ jobs:
         run: |
           vamp-ir --version
 
+      - name: Install Rust toolchain
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+
+      - name: Install Cairo VM
+        shell: bash
+        run: |
+          git clone https://github.com/lambdaclass/cairo-vm.git
+          cd cairo-vm
+          cargo build --release
+          cp target/release/cairo-vm-cli $HOME/.local/bin/cairo-vm-cli
+          cd -
+          cp main/scripts/run_cairo_vm.sh $HOME/.local/bin/run_cairo_vm.sh
+
       - name: Make runtime
         run: |
           cd main
@@ -274,6 +288,26 @@ jobs:
           echo "CC=$(brew --prefix llvm@15)/bin/clang" >> $GITHUB_ENV
           echo "LIBTOOL=$(brew --prefix llvm@15)/bin/llvm-ar" >> $GITHUB_ENV
 
+      - name: Add ~/.local/bin to PATH
+        run: |
+          mkdir -p "$HOME/.local/bin"
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+
+      - name: Install Rust toolchain
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+
+      - name: Install Cairo VM
+        shell: bash
+        run: |
+          git clone https://github.com/lambdaclass/cairo-vm.git
+          cd cairo-vm
+          cargo build --release
+          cp -a target/release/cairo-vm-cli $HOME/.local/bin/cairo-vm-cli
+          chmod a+x $HOME/.local/bin/cairo-vm-cli
+          cd -
+          cp -a main/scripts/run_cairo_vm.sh $HOME/.local/bin/run_cairo_vm.sh
+          chmod a+x $HOME/.local/bin/run_cairo_vm.sh
+
       - name: Make runtime
         run: |
           cd main
@@ -325,10 +359,6 @@ jobs:
           make CC=$CC LIBTOOL=$LIBTOOL install
           make CC=$CC LIBTOOL=$LIBTOOL test
 
-      - name: Add ~/.local/bin to PATH
-        run: |
-          echo "$HOME/.local/bin" >> $GITHUB_PATH
-
       - name: Typecheck and format Juvix examples
         if: ${{ success() }}
         shell: bash

app/Commands/Compile.hs

@@ -29,6 +29,7 @@ runCommand opts@CompileOptions {..} = do
     TargetReg -> Compile.runRegPipeline arg
     TargetAnoma -> Compile.runAnomaPipeline arg
     TargetCasm -> Compile.runCasmPipeline arg
+    TargetCairo -> Compile.runCairoPipeline arg
 
 writeCoreFile :: (Members '[EmbedIO, App, TaggedLock] r) => Compile.PipelineArg -> Sem r ()
 writeCoreFile [email protected] {..} = do

app/Commands/Dev/Asm/Compile.hs

@@ -3,6 +3,7 @@ module Commands.Dev.Asm.Compile where
 import Commands.Base
 import Commands.Dev.Asm.Compile.Options
 import Commands.Extra.Compile qualified as Compile
+import Data.Aeson qualified as JSON
 import Juvix.Compiler.Asm.Translation.FromSource qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
@@ -46,6 +47,15 @@ runCommand opts = do
               $ tab
           Casm.Result {..} <- getRight r
           writeFileEnsureLn casmFile (toPlainText $ Casm.ppProgram _resultCode)
+        TargetCairo -> do
+          cairoFile <- Compile.outputFile opts file
+          r <-
+            runReader entryPoint
+              . runError @JuvixError
+              . asmToCairo
+              $ tab
+          res <- getRight r
+          liftIO $ JSON.encodeFile (toFilePath cairoFile) res
         _ ->
           case run $ runReader entryPoint $ runError $ asmToMiniC tab of
             Left err -> exitJuvixError err
@@ -70,6 +80,7 @@ runCommand opts = do
       TargetNative64 -> return Backend.TargetCNative64
       TargetReg -> return Backend.TargetReg
       TargetCasm -> return Backend.TargetCairo
+      TargetCairo -> return Backend.TargetCairo
       TargetAnoma -> err "Anoma"
       TargetTree -> err "JuvixTree"
       TargetGeb -> err "GEB"

app/Commands/Dev/Asm/Compile/Options.hs

@@ -16,7 +16,8 @@ asmSupportedTargets =
     [ TargetWasm32Wasi,
       TargetNative64,
       TargetReg,
-      TargetCasm
+      TargetCasm,
+      TargetCairo
     ]
 
 parseAsmCompileOptions :: Parser AsmCompileOptions

app/Commands/Dev/Casm.hs

@@ -1,11 +1,13 @@
 module Commands.Dev.Casm where
 
 import Commands.Base
+import Commands.Dev.Casm.Compile as Compile
 import Commands.Dev.Casm.Options
 import Commands.Dev.Casm.Read as Read
 import Commands.Dev.Casm.Run as Run
 
 runCommand :: forall r. (Members '[EmbedIO, App, TaggedLock] r) => CasmCommand -> Sem r ()
 runCommand = \case
+  Compile opts -> Compile.runCommand opts
   Run opts -> Run.runCommand opts
   Read opts -> Read.runCommand opts

app/Commands/Dev/Casm/Compile.hs

@@ -0,0 +1,57 @@
+module Commands.Dev.Casm.Compile where
+
+import Commands.Base
+import Commands.Dev.Casm.Compile.Options
+import Commands.Extra.Compile qualified as Compile
+import Data.Aeson qualified as JSON
+import Juvix.Compiler.Backend qualified as Backend
+import Juvix.Compiler.Casm.Data.Result qualified as Casm
+import Juvix.Compiler.Casm.Translation.FromSource qualified as Casm
+import Juvix.Compiler.Casm.Validate qualified as Casm
+
+runCommand :: forall r. (Members '[EmbedIO, App, TaggedLock] r) => CompileOptions -> Sem r ()
+runCommand opts = do
+  file <- getFile
+  s <- readFile file
+  case Casm.runParser file s of
+    Left err -> exitJuvixError (JuvixError err)
+    Right (labi, code) ->
+      case Casm.validate labi code of
+        Left err -> exitJuvixError (JuvixError err)
+        Right () -> do
+          ep <- getEntryPoint (AppPath (preFileFromAbs file) True)
+          tgt <- getTarget (opts ^. compileTarget)
+          let entryPoint :: EntryPoint
+              entryPoint =
+                ep
+                  { _entryPointTarget = tgt,
+                    _entryPointDebug = opts ^. compileDebug
+                  }
+          cairoFile <- Compile.outputFile opts file
+          r <-
+            runReader entryPoint
+              . runError @JuvixError
+              . casmToCairo
+              $ Casm.Result labi code
+          res <- getRight r
+          liftIO $ JSON.encodeFile (toFilePath cairoFile) res
+  where
+    getFile :: Sem r (Path Abs File)
+    getFile = getMainFile (opts ^. compileInputFile)
+
+    getTarget :: CompileTarget -> Sem r Backend.Target
+    getTarget = \case
+      TargetCairo -> return Backend.TargetCairo
+      TargetWasm32Wasi -> err "WASM"
+      TargetNative64 -> err "native"
+      TargetCasm -> err "CASM"
+      TargetReg -> err "JuvixReg"
+      TargetAnoma -> err "Anoma"
+      TargetTree -> err "JuvixTree"
+      TargetGeb -> err "GEB"
+      TargetVampIR -> err "VampIR"
+      TargetCore -> err "JuvixCore"
+      TargetAsm -> err "JuvixAsm"
+      where
+        err :: Text -> Sem r a
+        err tgt = exitMsg (ExitFailure 1) ("error: " <> tgt <> " target not supported for CASM")

app/Commands/Dev/Casm/Compile/Options.hs

@@ -0,0 +1,21 @@
+module Commands.Dev.Casm.Compile.Options
+  ( module Commands.Dev.Casm.Compile.Options,
+    module Commands.Extra.Compile.Options,
+  )
+where
+
+import Commands.Extra.Compile.Options
+import CommonOptions
+import Data.List.NonEmpty qualified as NonEmpty
+
+casmSupportedTargets :: NonEmpty CompileTarget
+casmSupportedTargets =
+  NonEmpty.fromList
+    [ TargetCairo
+    ]
+
+parseCasmCompileOptions :: Parser CompileOptions
+parseCasmCompileOptions =
+  parseCompileOptions
+    casmSupportedTargets
+    (parseInputFile FileExtCasm)

app/Commands/Dev/Casm/Options.hs

@@ -1,28 +1,40 @@
 module Commands.Dev.Casm.Options where
 
+import Commands.Dev.Casm.Compile.Options
 import Commands.Dev.Casm.Read.Options
 import Commands.Dev.Casm.Run.Options
 import CommonOptions
 
 data CasmCommand
-  = Run CasmRunOptions
+  = Compile CompileOptions
+  | Run CasmRunOptions
   | Read CasmReadOptions
   deriving stock (Data)
 
 parseCasmCommand :: Parser CasmCommand
 parseCasmCommand =
   hsubparser $
     mconcat
-      [ commandRun,
+      [ commandCompile,
+        commandRun,
         commandRead
       ]
   where
+    commandCompile :: Mod CommandFields CasmCommand
+    commandCompile = command "compile" compileInfo
+
     commandRun :: Mod CommandFields CasmCommand
     commandRun = command "run" runInfo
 
     commandRead :: Mod CommandFields CasmCommand
     commandRead = command "read" readInfo
 
+    compileInfo :: ParserInfo CasmCommand
+    compileInfo =
+      info
+        (Compile <$> parseCasmCompileOptions)
+        (progDesc "Compile a CASM file")
+
     runInfo :: ParserInfo CasmCommand
     runInfo =
       info

app/Commands/Dev/Core/Compile.hs

@@ -23,6 +23,7 @@ runCommand opts = do
     TargetTree -> runTreePipeline arg
     TargetAnoma -> runAnomaPipeline arg
     TargetCasm -> runCasmPipeline arg
+    TargetCairo -> runCairoPipeline arg
   where
     getFile :: Sem r (Path Abs File)
     getFile = getMainFile (opts ^. compileInputFile)

app/Commands/Dev/Core/Compile/Base.hs

@@ -4,6 +4,7 @@ import Commands.Base
 import Commands.Dev.Core.Compile.Options
 import Commands.Dev.Tree.Compile.Base (outputAnomaResult)
 import Commands.Extra.Compile qualified as Compile
+import Data.Aeson qualified as JSON
 import Juvix.Compiler.Asm.Pretty qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
@@ -48,6 +49,7 @@ getEntry PipelineArg {..} = do
       TargetTree -> Backend.TargetTree
       TargetAnoma -> Backend.TargetAnoma
       TargetCasm -> Backend.TargetCairo
+      TargetCairo -> Backend.TargetCairo
 
     defaultOptLevel :: Int
     defaultOptLevel
@@ -169,3 +171,15 @@ runCasmPipeline pa@PipelineArg {..} = do
       $ _pipelineArgModule
   Casm.Result {..} <- getRight r
   writeFileEnsureLn casmFile (toPlainText $ Casm.ppProgram _resultCode)
+
+runCairoPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
+runCairoPipeline pa@PipelineArg {..} = do
+  entryPoint <- getEntry pa
+  cairoFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  r <-
+    runReader entryPoint
+      . runError @JuvixError
+      . coreToCairo
+      $ _pipelineArgModule
+  res <- getRight r
+  liftIO $ JSON.encodeFile (toFilePath cairoFile) res

app/Commands/Dev/Core/Compile/Options.hs

@@ -13,14 +13,15 @@ type CoreCompileOptions = CompileOptions
 coreSupportedTargets :: NonEmpty CompileTarget
 coreSupportedTargets =
   NonEmpty.fromList
-    [ TargetWasm32Wasi,
-      TargetNative64,
+    [ TargetNative64,
+      TargetWasm32Wasi,
       TargetGeb,
       TargetVampIR,
       TargetTree,
       TargetAsm,
       TargetReg,
-      TargetCasm
+      TargetCasm,
+      TargetCairo
     ]
 
 parseCoreCompileOptions :: Parser CoreCompileOptions

app/Commands/Dev/Reg/Compile.hs

@@ -3,6 +3,7 @@ module Commands.Dev.Reg.Compile where
 import Commands.Base
 import Commands.Dev.Reg.Compile.Options
 import Commands.Extra.Compile qualified as Compile
+import Data.Aeson qualified as JSON
 import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Casm.Data.Result qualified as Casm
@@ -35,6 +36,15 @@ runCommand opts = do
               $ tab
           Casm.Result {..} <- getRight r
           writeFileEnsureLn casmFile (toPlainText $ Casm.ppProgram _resultCode)
+        TargetCairo -> do
+          cairoFile <- Compile.outputFile opts file
+          r <-
+            runReader entryPoint
+              . runError @JuvixError
+              . regToCairo
+              $ tab
+          res <- getRight r
+          liftIO $ JSON.encodeFile (toFilePath cairoFile) res
         _ ->
           case run $ runReader entryPoint $ runError $ regToMiniC tab of
             Left err -> exitJuvixError err
@@ -58,6 +68,7 @@ runCommand opts = do
       TargetWasm32Wasi -> return Backend.TargetCWasm32Wasi
       TargetNative64 -> return Backend.TargetCNative64
       TargetCasm -> return Backend.TargetCairo
+      TargetCairo -> return Backend.TargetCairo
       TargetReg -> err "JuvixReg"
       TargetAnoma -> err "Anoma"
       TargetTree -> err "JuvixTree"

app/Commands/Dev/Reg/Compile/Options.hs

@@ -11,9 +11,10 @@ import Data.List.NonEmpty qualified as NonEmpty
 regSupportedTargets :: NonEmpty CompileTarget
 regSupportedTargets =
   NonEmpty.fromList
-    [ TargetWasm32Wasi,
-      TargetNative64,
-      TargetCasm
+    [ TargetNative64,
+      TargetWasm32Wasi,
+      TargetCasm,
+      TargetCairo
     ]
 
 parseRegCompileOptions :: Parser CompileOptions

app/Commands/Dev/Runtime/Options.hs

@@ -11,8 +11,8 @@ newtype RuntimeCommand
 runtimeSupportedTargets :: NonEmpty CompileTarget
 runtimeSupportedTargets =
   NonEmpty.fromList
-    [ TargetWasm32Wasi,
-      TargetNative64
+    [ TargetNative64,
+      TargetWasm32Wasi
     ]
 
 parseRuntimeOptions :: Parser CompileOptions

app/Commands/Dev/Tree/Compile.hs

@@ -22,6 +22,7 @@ runCommand opts = do
     TargetTree -> return ()
     TargetAnoma -> runAnomaPipeline arg
     TargetCasm -> runCasmPipeline arg
+    TargetCairo -> runCairoPipeline arg
   where
     getFile :: Sem r (Path Abs File)
     getFile = getMainFile (opts ^. compileInputFile)