Cairo: Support complex data types in program input (#2822)

* Types of arguments to `main` can now be field elements, numbers,
booleans and (nested) records and lists.
* Type of `main` result can now be a record of field elements, numbers
and booleans. Lists or nested records are not allowed for the result.
* Adds checks for the type of `main` in the Cairo pipeline.
* Requires updating
[juvix-cairo-vm](https://github.com/anoma/juvix-cairo-vm). The input can
be provided in a Json file via the `--program_input` option of
`juvix-cairo-vm`.

.github/workflows/ci.yml

@@ -26,7 +26,7 @@ env:
   SKIP: ormolu,format-juvix-files,typecheck-juvix-examples
   VAMPIRREPO: anoma/vamp-ir
   VAMPIRVERSION: v0.1.3
-  CAIRO_VM_VERSION: 6bb5330aede3fc8049b498012a6efbf12bc9432a
+  CAIRO_VM_VERSION: ec4e2547c201983595254efbe72d9b4cfa450ad9
   RISC0_VM_VERSION: v1.0.1
   JUST_ARGS: runtimeCcArg=$CC runtimeLibtoolArg=$LIBTOOL
   STACK_BUILD_ARGS: --pedantic -j4 --ghc-options=-j

app/Commands/Dev/Casm/Compile.hs

@@ -28,7 +28,12 @@ runCommand opts = do
     runReader entryPoint
       . runError @JuvixError
       . casmToCairo
-      $ Casm.Result labi code []
+      $ Casm.Result
+        { _resultLabelInfo = labi,
+          _resultCode = code,
+          _resultBuiltins = [],
+          _resultOutputSize = 1
+        }
   res <- getRight r
   liftIO $ JSON.encodeFile (toFilePath cairoFile) res
   where

cntlines.sh

@@ -9,7 +9,7 @@ function count_ext () {
 }
 
 RUNTIME_C=$(count runtime/c/src/juvix)
-RUNTIME_RUST=$(count runtime/rust/src)
+RUNTIME_RUST=$(count runtime/rust/juvix/src)
 RUNTIME_VAMPIR=$(count_ext '*.pir' runtime/vampir)
 RUNTIME_JVT=$(count_ext '*.jvt' runtime/tree)
 RUNTIME_CASM=$(count_ext '*.casm' runtime/casm)

runtime/casm/stdlib.casm

@@ -11,6 +11,13 @@
 -- sargs + argsnum = total numer of arguments for the function
 -- Maximum number of function arguments: 8
 
+-- Constructor layout: [ cid | arguments... ]
+--  cid -- constructor id: 2 * tag + 1, where tag is the 0-based index
+--         of the constructor within its inductive type
+-- Make sure this spec is followed by:
+-- * Juvix.Compiler.Casm.Translation.FromReg
+-- * get_cid() in juvix_hint_processor/hint_processor.rs in juvix-cairo-vm
+
 -- after calling juvix_get_regs:
 -- [ap - 4] = fp
 -- [ap - 3] = pc

src/Juvix/Compiler/Backend/Cairo/Extra/Serialization.hs

@@ -4,8 +4,8 @@ import Data.Bits
 import Juvix.Compiler.Backend.Cairo.Data.Result
 import Juvix.Compiler.Backend.Cairo.Language
 
-serialize :: [Text] -> [Element] -> Result
-serialize builtins elems =
+serialize :: Int -> [Text] -> [Element] -> Result
+serialize outputSize builtins elems =
   Result
     { _resultData =
         initializeBuiltins
@@ -48,17 +48,26 @@ serialize builtins elems =
 
     finalizeBuiltins :: [Text]
     finalizeBuiltins =
-      -- [[fp]] = [ap - 1] -- [output_ptr] = [ap - 1]
-      -- [ap] = [fp] + 1; ap++ -- output_ptr
-      [ "0x4002800080007fff",
-        "0x4826800180008000",
-        "0x1"
-      ]
+      -- [[fp] + i] = [ap - outputSize + i]
+      -- [output_ptr + i] = [ap - outputSize + i]
+      map
+        ( \i ->
+            toHexText (0x4002800080008000 - outputSize' + i + shift i 32)
+        )
+        [0 .. outputSize' - 1]
         ++
-        -- [ap] = [ap - builtinsNum - 2]; ap++
+        -- [ap] = [fp] + outputSize; ap++
+        -- output_ptr = output_ptr + outputSize
+        [ "0x4826800180008000",
+          toHexText outputSize'
+        ]
+        ++
+        -- [ap] = [ap - 1 - builtinsNum - outputSize]; ap++
         replicate
           builtinsNum
-          (toHexText (0x48107ffe7fff8000 - shift builtinsNum 32))
+          (toHexText (0x48107fff7fff8000 - shift (builtinsNum + outputSize') 32))
+      where
+        outputSize' = fromIntegral outputSize
 
     finalizeJump :: [Text]
     finalizeJump =

src/Juvix/Compiler/Casm/Data/Result.hs

@@ -7,7 +7,8 @@ import Juvix.Compiler.Casm.Language
 data Result = Result
   { _resultLabelInfo :: LabelInfo,
     _resultCode :: [Instruction],
-    _resultBuiltins :: [Builtin]
+    _resultBuiltins :: [Builtin],
+    _resultOutputSize :: Int
   }
 
 makeLenses ''Result

src/Juvix/Compiler/Casm/Translation/FromCairo.hs

@@ -9,7 +9,8 @@ fromCairo elems0 =
   Result
     { _resultLabelInfo = mempty,
       _resultCode = go 0 [] elems0,
-      _resultBuiltins = mempty
+      _resultBuiltins = mempty,
+      _resultOutputSize = 0
     }
   where
     errorMsg :: Address -> Text -> a

src/Juvix/Compiler/Casm/Translation/FromReg.hs

@@ -29,35 +29,38 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
   registerLabelName startSym startName
   registerLabelAddress startSym startAddr
   let mainSym = fromJust $ tab ^. Reg.infoMainFunction
-      mainInfo = fromJust (HashMap.lookup mainSym (tab ^. Reg.infoFunctions))
+      mainInfo = Reg.lookupFunInfo tab mainSym
       mainName = mainInfo ^. Reg.functionName
+      mainResultType = Reg.typeTarget (mainInfo ^. Reg.functionType)
       mainArgs = getInputArgs (mainInfo ^. Reg.functionArgsNum) (mainInfo ^. Reg.functionArgNames)
       bnum = toOffset builtinsNum
       callStartInstr = mkCallRel (Lab startLab)
       initBuiltinsInstr = mkAssignAp (Binop $ BinopValue FieldAdd (MemRef Fp (-2)) (Imm 1))
       callMainInstr = mkCallRel (Lab $ LabelRef mainSym (Just mainName))
       jmpEndInstr = mkJumpRel (Val $ Lab endLab)
-      margs = concat $ reverse $ map mkLoadInputArg mainArgs
+      loadInputArgsInstrs = concat $ reverse $ map mkLoadInputArg mainArgs
       -- [ap] = [[ap - 2 - k] + k]; ap++
       bltsRet = map (\k -> mkAssignAp (Load $ LoadValue (MemRef Ap (-2 - k)) k)) [0 .. bnum - 1]
-      resRetInstr = mkAssignAp (Val $ Ref $ MemRef Ap (-bnum - 1))
+      resRetInstrs = mkResultInstrs bnum mainResultType
       pinstrs =
         callStartInstr
           : jmpEndInstr
           : Label startLab
           : initBuiltinsInstr
-          : margs
+          : loadInputArgsInstrs
           ++ callMainInstr
           : bltsRet
-          ++ [resRetInstr, Return]
+          ++ resRetInstrs
+          ++ [Return]
   (blts, binstrs) <- addStdlibBuiltins (length pinstrs)
   let cinstrs = concatMap (mkFunCall . fst) $ sortOn snd $ HashMap.toList (info ^. Reg.extraInfoFUIDs)
   (addr, instrs) <- second (concat . reverse) <$> foldM (goFun blts endLab) (length pinstrs + length binstrs + length cinstrs, []) (tab ^. Reg.infoFunctions)
   eassert (addr == length instrs + length cinstrs + length binstrs + length pinstrs)
   registerLabelName endSym endName
   registerLabelAddress endSym addr
-  return $
-    ( allElements,
+  return
+    ( length resRetInstrs,
+      allElements,
       pinstrs
         ++ binstrs
         ++ cinstrs
@@ -65,8 +68,32 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
         ++ [Label endLab]
     )
   where
-    mkResult :: (LabelInfo, ([Builtin], Code)) -> Result
-    mkResult (labi, (blts, code)) = Result labi code blts
+    mkResult :: (LabelInfo, (Int, [Builtin], Code)) -> Result
+    mkResult (labi, (outSize, blts, code)) =
+      Result
+        { _resultLabelInfo = labi,
+          _resultCode = code,
+          _resultBuiltins = blts,
+          _resultOutputSize = outSize
+        }
+
+    mkResultInstrs :: Offset -> Reg.Type -> [Instruction]
+    mkResultInstrs off = \case
+      Reg.TyInductive Reg.TypeInductive {..} -> goRecord _typeInductiveSymbol
+      Reg.TyConstr Reg.TypeConstr {..} -> goRecord _typeConstrInductive
+      _ -> [mkAssignAp (Val $ Ref $ MemRef Ap (-off - 1))]
+      where
+        goRecord :: Symbol -> [Instruction]
+        goRecord sym = case indInfo ^. Reg.inductiveConstructors of
+          [tag] -> case Reg.lookupConstrInfo tab tag of
+            Reg.ConstructorInfo {..} ->
+              map mkOutInstr [1 .. toOffset _constructorArgsNum]
+              where
+                mkOutInstr :: Offset -> Instruction
+                mkOutInstr i = mkAssignAp (Load $ LoadValue (MemRef Ap (-off - i)) i)
+          _ -> impossible
+          where
+            indInfo = Reg.lookupInductiveInfo tab sym
 
     mkLoadInputArg :: Text -> [Instruction]
     mkLoadInputArg arg = [Hint (HintInput arg), mkAssignAp (Val $ Ref $ MemRef Ap 0)]
@@ -87,6 +114,10 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
         Nop
       ]
 
+    -- To make it convenient with relative jumps, Cairo constructor tag is `2 *
+    -- tag + 1` where `tag` is the 0-based constructor number within the
+    -- inductive type. Make sure this corresponds with the relative jump code in
+    -- `goCase`.
     getTagId :: Tag -> Int
     getTagId tag =
       1 + 2 * fromJust (HashMap.lookup tag (info ^. Reg.extraInfoCIDs))
@@ -170,7 +201,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
 
         goCallBlock :: Bool -> Maybe Reg.VarRef -> HashSet Reg.VarRef -> Sem r ()
         goCallBlock updatedBuiltins outVar liveVars = do
-          let liveVars' = toList (maybe liveVars (flip HashSet.delete liveVars) outVar)
+          let liveVars' = toList (maybe liveVars (`HashSet.delete` liveVars) outVar)
               n = length liveVars'
               bltOff =
                 if
@@ -578,7 +609,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
           syms <- replicateM (length tags) freshSymbol
           symEnd <- freshSymbol
           let symMap = HashMap.fromList $ zip tags syms
-              labs = map (flip LabelRef Nothing) syms
+              labs = map (`LabelRef` Nothing) syms
               labEnd = LabelRef symEnd Nothing
               jmps = map (mkJumpRel . Val . Lab) labs
               -- we need the Nop instructions to ensure that the relative jump

src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs

@@ -2,9 +2,9 @@ module Juvix.Compiler.Core.Transformation.Check.Cairo where
 
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation.Check.Base
-import Juvix.Data.PPOutput
 
 checkCairo :: forall r. (Member (Error CoreError) r) => Module -> Sem r Module
 checkCairo md = do
@@ -19,7 +19,7 @@ checkCairo md = do
       unless (checkType (ii ^. identifierType)) $
         throw
           CoreError
-            { _coreErrorMsg = ppOutput "for this target the arguments and the result of the `main` function must be numbers or field elements",
+            { _coreErrorMsg = ppOutput "for this target the arguments the `main` function need to be field elements, numbers, booleans, records or lists, and the result needs to be a field element, number, boolean or a record of field elements, numbers and booleans",
               _coreErrorLoc = fromMaybe defaultLoc (ii ^. identifierLocation),
               _coreErrorNode = Nothing
             }
@@ -29,7 +29,69 @@ checkCairo md = do
     checkType :: Node -> Bool
     checkType ty =
       let (tyargs, tgt) = unfoldPi' ty
-       in all isPrimIntegerOrField (tgt : tyargs)
+       in all isArgType tyargs && isTargetType tgt
       where
-        isPrimIntegerOrField ty' =
-          isTypeInteger ty' || isTypeField ty' || isDynamic ty'
+        isArgType :: Node -> Bool
+        isArgType = \case
+          NPi {} -> False
+          NUniv {} -> False
+          NTyp x -> isRecordOrList x
+          NPrim x -> isAllowedPrim x
+          NDyn {} -> True
+          _ -> False
+
+        isTargetType :: Node -> Bool
+        isTargetType = \case
+          NPi {} -> False
+          NUniv {} -> False
+          NTyp x -> isFlatRecord x
+          NPrim x -> isAllowedPrim x
+          NDyn {} -> True
+          _ -> False
+
+        isPrimType :: Node -> Bool
+        isPrimType = \case
+          NPrim x -> isAllowedPrim x
+          _ -> False
+
+        isAllowedPrim :: TypePrim -> Bool
+        isAllowedPrim TypePrim {..} = case _typePrimPrimitive of
+          PrimInteger {} -> True
+          PrimBool {} -> True
+          PrimField {} -> True
+          PrimString {} -> False
+
+        isRecordOrList :: TypeConstr -> Bool
+        isRecordOrList TypeConstr {..} = case ii ^. inductiveBuiltin of
+          Just (BuiltinTypeInductive BuiltinList) ->
+            all isArgType _typeConstrArgs
+          Just {} ->
+            False
+          Nothing ->
+            case ii ^. inductiveConstructors of
+              [tag] ->
+                all isArgType tyargs
+                where
+                  ci = lookupConstructorInfo md tag
+                  cty = ci ^. constructorType
+                  nParams = length _typeConstrArgs
+                  tyargs =
+                    map (substs _typeConstrArgs)
+                      . drop nParams
+                      . typeArgs
+                      $ cty
+              _ -> False
+          where
+            ii = lookupInductiveInfo md _typeConstrSymbol
+
+        isFlatRecord :: TypeConstr -> Bool
+        isFlatRecord TypeConstr {..} =
+          case ii ^. inductiveConstructors of
+            [tag]
+              | null _typeConstrArgs ->
+                  all isPrimType (typeArgs (ci ^. constructorType))
+              where
+                ci = lookupConstructorInfo md tag
+            _ -> False
+          where
+            ii = lookupInductiveInfo md _typeConstrSymbol

src/Juvix/Compiler/Pipeline.hs

@@ -364,7 +364,7 @@ regToCasm = Reg.toCasm >=> return . Casm.fromReg
 casmToCairo :: Casm.Result -> Sem r Cairo.Result
 casmToCairo Casm.Result {..} =
   return
-    . Cairo.serialize (map Casm.builtinName _resultBuiltins)
+    . Cairo.serialize _resultOutputSize (map Casm.builtinName _resultBuiltins)
     $ Cairo.fromCasm _resultCode
 
 regToCairo :: Reg.InfoTable -> Sem r Cairo.Result

test/Casm/Compilation.hs

@@ -1,7 +1,8 @@
 module Casm.Compilation where
 
 import Base
+import Casm.Compilation.Negative qualified as N
 import Casm.Compilation.Positive qualified as P
 
 allTests :: TestTree
-allTests = testGroup "Juvix to CASM compilation" [P.allTests, P.allTestsNoOptimize]
+allTests = testGroup "Juvix to CASM compilation" [P.allTests, P.allTestsNoOptimize, N.allTests]

test/Casm/Compilation/Base.hs

@@ -14,6 +14,7 @@ compileAssertion ::
   Bool ->
   Int ->
   Path Abs File ->
+  Maybe (Path Abs File) ->
   Path Abs File ->
   (String -> IO ()) ->
   Assertion
@@ -26,10 +27,11 @@ compileAssertionEntry ::
   Bool ->
   Int ->
   Path Abs File ->
+  Maybe (Path Abs File) ->
   Path Abs File ->
   (String -> IO ()) ->
   Assertion
-compileAssertionEntry adjustEntry root' bInterp bRunVM optLevel mainFile expectedFile step = do
+compileAssertionEntry adjustEntry root' bInterp bRunVM optLevel mainFile inputFile expectedFile step = do
   step "Translate to JuvixCore"
   entryPoint <- adjustEntry <$> testDefaultEntryPointIO root' mainFile
   PipelineResult {..} <- snd <$> testRunIO entryPoint upToStoredCore
@@ -44,4 +46,15 @@ compileAssertionEntry adjustEntry root' bInterp bRunVM optLevel mainFile expecte
             step "Pretty print"
             writeFileEnsureLn tmpFile (toPlainText $ ppProgram _resultCode)
         )
-      casmRunAssertion' bInterp bRunVM _resultLabelInfo _resultCode _resultBuiltins Nothing expectedFile step
+      casmRunAssertion' bInterp bRunVM _resultLabelInfo _resultCode _resultBuiltins _resultOutputSize inputFile expectedFile step
+
+compileErrorAssertion :: Path Abs Dir -> Path Abs File -> (String -> IO ()) -> Assertion
+compileErrorAssertion root' mainFile step = do
+  step "Translate to JuvixCore"
+  entryPoint <- testDefaultEntryPointIO root' mainFile
+  let entryPoint' = entryPoint {_entryPointFieldSize = cairoFieldSize}
+  PipelineResult {..} <- snd <$> testRunIO entryPoint' upToStoredCore
+  step "Translate to CASM"
+  case run $ runError @JuvixError $ runReader entryPoint $ storedCoreToCasm (_pipelineResult ^. Core.coreResultModule) of
+    Left {} -> assertBool "" True
+    Right {} -> assertFailure "no error"

test/Casm/Compilation/Negative.hs

@@ -0,0 +1,41 @@
+module Casm.Compilation.Negative where
+
+import Base
+import Casm.Compilation.Base
+
+data NegTest = NegTest
+  { _name :: String,
+    _relDir :: Path Rel Dir,
+    _file :: Path Rel File
+  }
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/Casm/Compilation/negative")
+
+testDescr :: NegTest -> TestDescr
+testDescr NegTest {..} =
+  let tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ compileErrorAssertion tRoot file'
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Juvix to CASM negative tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [NegTest]
+tests =
+  [ NegTest
+      "Test001: Wrong `main` argument type"
+      $(mkRelDir ".")
+      $(mkRelFile "test001.juvix"),
+    NegTest
+      "Test002: Wrong `main` result type"
+      $(mkRelDir ".")
+      $(mkRelFile "test002.juvix")
+  ]

test/Casm/Compilation/Positive.hs

@@ -10,7 +10,8 @@ data PosTest = PosTest
     _name :: String,
     _dir :: Path Abs Dir,
     _file :: Path Abs File,
-    _expectedFile :: Path Abs File
+    _expectedFile :: Path Abs File,
+    _inputFile :: Maybe (Path Abs File)
   }
 
 makeLenses ''PosTest
@@ -23,10 +24,11 @@ toTestDescr optLevel PosTest {..} =
   let tRoot = _dir
       file' = _file
       expected' = _expectedFile
+      input' = _inputFile
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ compileAssertion _dir _interp _runVM optLevel file' expected'
+          _testAssertion = Steps $ compileAssertion _dir _interp _runVM optLevel file' input' expected'
         }
 
 allTests :: TestTree
@@ -41,11 +43,12 @@ allTestsNoOptimize =
     "Juvix to CASM positive tests (no optimization)"
     (map (mkTest . toTestDescr 0) tests)
 
-posTest :: String -> Bool -> Bool -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
-posTest _name _interp _runVM rdir rfile routfile =
+posTest :: String -> Bool -> Bool -> Path Rel Dir -> Path Rel File -> Maybe (Path Rel File) -> Path Rel File -> PosTest
+posTest _name _interp _runVM rdir rfile rinfile routfile =
   let _dir = root <//> rdir
       _file = _dir <//> rfile
       _expectedFile = root <//> routfile
+      _inputFile = fmap (root <//>) rinfile
    in PosTest {..}
 
 isIgnored :: PosTest -> Bool
@@ -68,6 +71,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test001.juvix")
+        Nothing
         $(mkRelFile "out/test001.out"),
       posTest
         "Test002: Arithmetic operators inside lambdas"
@@ -75,6 +79,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test002.juvix")
+        Nothing
         $(mkRelFile "out/test002.out"),
       posTest
         "Test003: Integer arithmetic"
@@ -82,6 +87,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test003.juvix")
+        Nothing
         $(mkRelFile "out/test003.out"),
       posTest
         "Test005: Higher-order functions"
@@ -89,6 +95,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test005.juvix")
+        Nothing
         $(mkRelFile "out/test005.out"),
       posTest
         "Test006: If-then-else and lazy boolean operators"
@@ -96,6 +103,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test006.juvix")
+        Nothing
         $(mkRelFile "out/test006.out"),
       posTest
         "Test007: Pattern matching and lambda-case"
@@ -103,6 +111,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test007.juvix")
+        Nothing
         $(mkRelFile "out/test007.out"),
       posTest
         "Test008: Recursion"
@@ -110,6 +119,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test008.juvix")
+        Nothing
         $(mkRelFile "out/test008.out"),
       posTest
         "Test009: Tail recursion"
@@ -117,6 +127,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test009.juvix")
+        Nothing
         $(mkRelFile "out/test009.out"),
       posTest
         "Test010: Let"
@@ -124,6 +135,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test010.juvix")
+        Nothing
         $(mkRelFile "out/test010.out"),
       posTest
         "Test013: Functions returning functions with variable capture"
@@ -131,6 +143,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test013.juvix")
+        Nothing
         $(mkRelFile "out/test013.out"),
       posTest
         "Test014: Arithmetic"
@@ -138,6 +151,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test014.juvix")
+        Nothing
         $(mkRelFile "out/test014.out"),
       posTest
         "Test015: Local functions with free variables"
@@ -145,6 +159,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test015.juvix")
+        Nothing
         $(mkRelFile "out/test015.out"),
       posTest
         "Test016: Recursion through higher-order functions"
@@ -152,6 +167,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test016.juvix")
+        Nothing
         $(mkRelFile "out/test016.out"),
       posTest
         "Test017: Tail recursion through higher-order functions"
@@ -159,6 +175,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test017.juvix")
+        Nothing
         $(mkRelFile "out/test017.out"),
       posTest
         "Test018: Higher-order functions and recursion"
@@ -166,6 +183,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test018.juvix")
+        Nothing
         $(mkRelFile "out/test018.out"),
       posTest
         "Test019: Self-application"
@@ -173,6 +191,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test019.juvix")
+        Nothing
         $(mkRelFile "out/test019.out"),
       posTest
         "Test020: Recursive functions: McCarthy's 91 function, subtraction by increments"
@@ -180,6 +199,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test020.juvix")
+        Nothing
         $(mkRelFile "out/test020.out"),
       posTest
         "Test021: Fast exponentiation"
@@ -187,6 +207,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test021.juvix")
+        Nothing
         $(mkRelFile "out/test021.out"),
       posTest
         "Test022: Lists"
@@ -194,6 +215,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test022.juvix")
+        Nothing
         $(mkRelFile "out/test022.out"),
       posTest
         "Test023: Mutual recursion"
@@ -201,6 +223,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test023.juvix")
+        Nothing
         $(mkRelFile "out/test023.out"),
       posTest
         "Test024: Nested binders with variable capture"
@@ -208,6 +231,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test024.juvix")
+        Nothing
         $(mkRelFile "out/test024.out"),
       posTest
         "Test025: Euclid's algorithm"
@@ -215,6 +239,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test025.juvix")
+        Nothing
         $(mkRelFile "out/test025.out"),
       posTest
         "Test026: Functional queues"
@@ -222,6 +247,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test026.juvix")
+        Nothing
         $(mkRelFile "out/test026.out"),
       posTest
         "Test028: Streams without memoization"
@@ -229,6 +255,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test028.juvix")
+        Nothing
         $(mkRelFile "out/test028.out"),
       posTest
         "Test029: Ackermann function"
@@ -236,6 +263,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test029.juvix")
+        Nothing
         $(mkRelFile "out/test029.out"),
       posTest
         "Test030: Ackermann function (higher-order definition)"
@@ -243,6 +271,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test030.juvix")
+        Nothing
         $(mkRelFile "out/test030.out"),
       posTest
         "Test032: Merge sort"
@@ -250,6 +279,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test032.juvix")
+        Nothing
         $(mkRelFile "out/test032.out"),
       posTest
         "Test033: Eta-expansion of builtins and constructors"
@@ -257,6 +287,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test033.juvix")
+        Nothing
         $(mkRelFile "out/test033.out"),
       posTest
         "Test034: Recursive let"
@@ -264,6 +295,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test034.juvix")
+        Nothing
         $(mkRelFile "out/test034.out"),
       posTest
         "Test035: Pattern matching"
@@ -271,6 +303,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test035.juvix")
+        Nothing
         $(mkRelFile "out/test035.out"),
       posTest
         "Test036: Eta-expansion"
@@ -278,6 +311,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test036.juvix")
+        Nothing
         $(mkRelFile "out/test036.out"),
       posTest
         "Test037: Applications with lets and cases in function position"
@@ -285,6 +319,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test037.juvix")
+        Nothing
         $(mkRelFile "out/test037.out"),
       posTest
         "Test038: Simple case expression"
@@ -292,6 +327,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test038.juvix")
+        Nothing
         $(mkRelFile "out/test038.out"),
       posTest
         "Test039: Mutually recursive let expression"
@@ -299,6 +335,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test039.juvix")
+        Nothing
         $(mkRelFile "out/test039.out"),
       posTest
         "Test040: Pattern matching nullary constructor"
@@ -306,6 +343,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test040.juvix")
+        Nothing
         $(mkRelFile "out/test040.out"),
       posTest
         "Test045: Implicit builtin bool"
@@ -313,6 +351,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test045.juvix")
+        Nothing
         $(mkRelFile "out/test045.out"),
       posTest
         "Test046: Polymorphic type arguments"
@@ -320,6 +359,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test046.juvix")
+        Nothing
         $(mkRelFile "out/test046.out"),
       posTest
         "Test047: Local Modules"
@@ -327,6 +367,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test047.juvix")
+        Nothing
         $(mkRelFile "out/test047.out"),
       posTest
         "Test050: Pattern matching with integers"
@@ -334,6 +375,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test050.juvix")
+        Nothing
         $(mkRelFile "out/test050.out"),
       posTest
         "Test053: Inlining"
@@ -341,6 +383,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test053.juvix")
+        Nothing
         $(mkRelFile "out/test053.out"),
       posTest
         "Test054: Iterators"
@@ -348,6 +391,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test054.juvix")
+        Nothing
         $(mkRelFile "out/test054.out"),
       posTest
         "Test056: Argument specialization"
@@ -355,6 +399,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test056.juvix")
+        Nothing
         $(mkRelFile "out/test056.out"),
       posTest
         "Test057: Case folding"
@@ -362,6 +407,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test057.juvix")
+        Nothing
         $(mkRelFile "out/test057.out"),
       posTest
         "Test058: Ranges"
@@ -369,6 +415,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test058.juvix")
+        Nothing
         $(mkRelFile "out/test058.out"),
       posTest
         "Test059: Builtin list"
@@ -376,6 +423,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test059.juvix")
+        Nothing
         $(mkRelFile "out/test059.out"),
       posTest
         "Test060: Record update"
@@ -383,6 +431,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test060.juvix")
+        Nothing
         $(mkRelFile "out/test060.out"),
       posTest
         "Test062: Overapplication"
@@ -390,6 +439,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test062.juvix")
+        Nothing
         $(mkRelFile "out/test062.out"),
       posTest
         "Test064: Constant folding"
@@ -397,6 +447,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test064.juvix")
+        Nothing
         $(mkRelFile "out/test064.out"),
       posTest
         "Test065: Arithmetic simplification"
@@ -404,6 +455,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test065.juvix")
+        Nothing
         $(mkRelFile "out/test065.out"),
       posTest
         "Test066: Import function with a function call in default argument"
@@ -411,6 +463,7 @@ tests =
         True
         $(mkRelDir "test066")
         $(mkRelFile "M.juvix")
+        Nothing
         $(mkRelFile "out/test066.out"),
       posTest
         "Test067: Dependent default values inserted during translation FromConcrete"
@@ -418,6 +471,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test067.juvix")
+        Nothing
         $(mkRelFile "out/test067.out"),
       posTest
         "Test068: Dependent default values inserted in the arity checker"
@@ -425,6 +479,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test068.juvix")
+        Nothing
         $(mkRelFile "out/test068.out"),
       posTest
         "Test069: Dependent default values for Ord trait"
@@ -432,6 +487,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test069.juvix")
+        Nothing
         $(mkRelFile "out/test069.out"),
       posTest
         "Test070: Nested default values and named arguments"
@@ -439,6 +495,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test070.juvix")
+        Nothing
         $(mkRelFile "out/test070.out"),
       posTest
         "Test071: Named application (Ord instance with default cmp)"
@@ -446,6 +503,7 @@ tests =
         False
         $(mkRelDir ".")
         $(mkRelFile "test071.juvix")
+        Nothing
         $(mkRelFile "out/test071.out"),
       posTest
         "Test072: Monad transformers (ReaderT + StateT + Identity)"
@@ -453,6 +511,7 @@ tests =
         True
         $(mkRelDir "test072")
         $(mkRelFile "ReaderT.juvix")
+        Nothing
         $(mkRelFile "out/test072.out"),
       posTest
         "Test073: Import and use a syntax alias"
@@ -460,6 +519,7 @@ tests =
         True
         $(mkRelDir "test073")
         $(mkRelFile "test073.juvix")
+        Nothing
         $(mkRelFile "out/test073.out"),
       posTest
         "Test074: Fields"
@@ -467,6 +527,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test074.juvix")
+        Nothing
         $(mkRelFile "out/test074.out"),
       posTest
         "Test075: Poseidon hash"
@@ -474,6 +535,7 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test075.juvix")
+        Nothing
         $(mkRelFile "out/test075.out"),
       posTest
         "Test076: Elliptic Curve builtin"
@@ -481,5 +543,14 @@ tests =
         True
         $(mkRelDir ".")
         $(mkRelFile "test076.juvix")
-        $(mkRelFile "out/test076.out")
+        Nothing
+        $(mkRelFile "out/test076.out"),
+      posTest
+        "Test077: Input and output"
+        False
+        True
+        $(mkRelDir ".")
+        $(mkRelFile "test077.juvix")
+        (Just $(mkRelFile "in/test077.json"))
+        $(mkRelFile "out/test077.out")
     ]

test/Casm/Reg/Positive.hs

@@ -27,7 +27,7 @@ testDescr PosTest {..} =
         }
 
 filterOutTests :: [String] -> [PosTest] -> [PosTest]
-filterOutTests incl = filter (\PosTest {..} -> not (_name `elem` incl))
+filterOutTests incl = filter (\PosTest {..} -> _name `notElem` incl)
 
 allTests :: TestTree
 allTests =

test/Casm/Run/Base.hs

@@ -18,14 +18,23 @@ casmRunVM' dirPath outputFile inputFile = do
   let args = maybe [] (\f -> ["--program_input", toFilePath f]) inputFile
   readProcessCwd (toFilePath dirPath) "run_cairo_vm.sh" (toFilePath outputFile : args) ""
 
-casmRunVM :: LabelInfo -> Code -> [Builtin] -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
-casmRunVM labi instrs blts inputFile expectedFile step = do
+casmRunVM :: LabelInfo -> Code -> [Builtin] -> Int -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
+casmRunVM labi instrs blts outputSize inputFile expectedFile step = do
   step "Check run_cairo_vm.sh is on path"
   assertCmdExists $(mkRelFile "run_cairo_vm.sh")
   withTempDir'
     ( \dirPath -> do
         step "Serialize to Cairo bytecode"
-        let res = run $ casmToCairo (Casm.Result labi instrs blts)
+        let res =
+              run $
+                casmToCairo
+                  ( Casm.Result
+                      { _resultLabelInfo = labi,
+                        _resultCode = instrs,
+                        _resultBuiltins = blts,
+                        _resultOutputSize = outputSize
+                      }
+                  )
             outputFile = dirPath <//> $(mkRelFile "out.json")
         encodeFile (toFilePath outputFile) res
         step "Run Cairo VM"
@@ -56,8 +65,8 @@ casmInterpret labi instrs inputFile expectedFile step =
             assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
     )
 
-casmRunAssertion' :: Bool -> Bool -> LabelInfo -> Code -> [Builtin] -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
-casmRunAssertion' bInterp bRunVM labi instrs blts inputFile expectedFile step =
+casmRunAssertion' :: Bool -> Bool -> LabelInfo -> Code -> [Builtin] -> Int -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
+casmRunAssertion' bInterp bRunVM labi instrs blts outputSize inputFile expectedFile step =
   case validate labi instrs of
     Left err -> do
       assertFailure (prettyString err)
@@ -65,7 +74,7 @@ casmRunAssertion' bInterp bRunVM labi instrs blts inputFile expectedFile step =
       when bInterp $
         casmInterpret labi instrs inputFile expectedFile step
       when bRunVM $
-        casmRunVM labi instrs blts inputFile expectedFile step
+        casmRunVM labi instrs blts outputSize inputFile expectedFile step
 
 casmRunAssertion :: Bool -> Bool -> Path Abs File -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
 casmRunAssertion bInterp bRunVM mainFile inputFile expectedFile step = do
@@ -73,7 +82,7 @@ casmRunAssertion bInterp bRunVM mainFile inputFile expectedFile step = do
   r <- parseFile mainFile
   case r of
     Left err -> assertFailure (prettyString err)
-    Right (labi, instrs) -> casmRunAssertion' bInterp bRunVM labi instrs [] inputFile expectedFile step
+    Right (labi, instrs) -> casmRunAssertion' bInterp bRunVM labi instrs [] 1 inputFile expectedFile step
 
 casmRunErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
 casmRunErrorAssertion mainFile step = do

test/Casm/Run/Positive.hs

@@ -5,6 +5,7 @@ import Casm.Run.Base
 
 data PosTest = PosTest
   { _name :: String,
+    _interp :: Bool,
     _runVM :: Bool,
     _relDir :: Path Rel Dir,
     _file :: Path Rel File,
@@ -24,7 +25,7 @@ testDescr PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ casmRunAssertion True _runVM file' input' expected'
+          _testAssertion = Steps $ casmRunAssertion _interp _runVM file' input' expected'
         }
 
 filterTests :: [String] -> [PosTest] -> [PosTest]
@@ -41,6 +42,7 @@ tests =
   [ PosTest
       "Test001: Sum of numbers"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test001.casm")
       $(mkRelFile "out/test001.out")
@@ -48,6 +50,7 @@ tests =
     PosTest
       "Test002: Factorial"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test002.casm")
       $(mkRelFile "out/test002.out")
@@ -55,6 +58,7 @@ tests =
     PosTest
       "Test003: Direct call"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test003.casm")
       $(mkRelFile "out/test003.out")
@@ -62,6 +66,7 @@ tests =
     PosTest
       "Test004: Indirect call"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test004.casm")
       $(mkRelFile "out/test004.out")
@@ -69,6 +74,7 @@ tests =
     PosTest
       "Test005: Exp function"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test005.casm")
       $(mkRelFile "out/test005.out")
@@ -76,6 +82,7 @@ tests =
     PosTest
       "Test006: Branch"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test006.casm")
       $(mkRelFile "out/test006.out")
@@ -83,12 +90,14 @@ tests =
     PosTest
       "Test007: Closure extension"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test007.casm")
       $(mkRelFile "out/test007.out")
       Nothing,
     PosTest
       "Test008: Integer arithmetic"
+      True
       False -- integer division not yet supported
       $(mkRelDir ".")
       $(mkRelFile "test008.casm")
@@ -97,6 +106,7 @@ tests =
     PosTest
       "Test009: Recursion"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test009.casm")
       $(mkRelFile "out/test009.out")
@@ -104,6 +114,7 @@ tests =
     PosTest
       "Test010: Functions returning functions"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test010.casm")
       $(mkRelFile "out/test010.out")
@@ -111,6 +122,7 @@ tests =
     PosTest
       "Test011: Lists"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test011.casm")
       $(mkRelFile "out/test011.out")
@@ -118,6 +130,7 @@ tests =
     PosTest
       "Test012: Recursion through higher-order functions"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test012.casm")
       $(mkRelFile "out/test012.out")
@@ -125,6 +138,7 @@ tests =
     PosTest
       "Test013: Currying and uncurrying"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test013.casm")
       $(mkRelFile "out/test013.out")
@@ -132,6 +146,7 @@ tests =
     PosTest
       "Test014: Field arithmetic"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test014.casm")
       $(mkRelFile "out/test014.out")
@@ -139,8 +154,17 @@ tests =
     PosTest
       "Test015: Input"
       True
+      True
       $(mkRelDir ".")
       $(mkRelFile "test015.casm")
       $(mkRelFile "out/test015.out")
-      (Just $(mkRelFile "in/test015.json"))
+      (Just $(mkRelFile "in/test015.json")),
+    PosTest
+      "Test016: Complex input"
+      False
+      True
+      $(mkRelDir ".")
+      $(mkRelFile "test016.casm")
+      $(mkRelFile "out/test016.out")
+      (Just $(mkRelFile "in/test016.json"))
   ]

tests/Casm/Compilation/negative/test001.juvix

@@ -0,0 +1,12 @@
+module test001;
+
+import Stdlib.Prelude open;
+
+type T :=
+  | T1 {
+      x : Field;
+      y : Field
+    }
+  | T2;
+
+main (x : Field) (_ : T) : Field := x + 1;

tests/Casm/Compilation/negative/test002.juvix

@@ -0,0 +1,5 @@
+module test002;
+
+import Stdlib.Prelude open;
+
+main (x : Field) : List Field := [x + 1];

tests/Casm/Compilation/positive/in/test077.json

@@ -0,0 +1,21 @@
+{
+  "input": {
+    "fld0": 7,
+    "fld1": 9,
+    "eph": true
+  },
+  "path": [
+    {
+      "fst": 1,
+      "snd": true
+    },
+    {
+      "fst": 2,
+      "snd": false
+    },
+    {
+      "fst": 3,
+      "snd": true
+    }
+  ]
+}

tests/Casm/Compilation/positive/out/test077.out

@@ -0,0 +1,3 @@
+4
+16
+9

tests/Casm/Compilation/positive/test077.juvix

@@ -0,0 +1,50 @@
+-- Complex input and output
+module test077;
+
+import Stdlib.Prelude open;
+
+type Resource :=
+  mkResource {
+    fld0 : Field;
+    fld1 : Field;
+    eph : Bool
+  };
+
+type Point :=
+  mkPoint {
+    x : Field;
+    y : Field
+  };
+
+type ComplianceResult :=
+  mkResult {
+    cnt : Field;
+    x : Field;
+    y : Field
+  };
+
+count : List (Field × Bool) -> Field
+  | [] := 0
+  | ((h, b) :: t) := if b (h + count t) (count t);
+
+main
+  (input : Resource)
+  (path : List (Field × Bool))
+  : ComplianceResult :=
+  mkResult@{
+    cnt := count path;
+    x :=
+      if
+        | Resource.eph input :=
+          Resource.fld0 input + Resource.fld1 input
+        | else := Resource.fld0 input;
+    y := Resource.fld1 input
+  };
+
+{-
+main
+  (input : Resource)
+  (path : List (Field × Bool))
+  : Field :=
+  count path;
+-}

tests/Casm/positive/in/test016.json

@@ -0,0 +1,7 @@
+{
+  "X": {
+    "A": 5,
+    "B": 7
+  },
+  "Y": [1, 2, 3]
+}

tests/Casm/positive/out/test016.out

@@ -0,0 +1 @@
+14

tests/Casm/positive/test016.casm

@@ -0,0 +1,22 @@
+-- complex input hints
+
+call main
+jmp end
+
+main:
+%{ Input(X) %}
+[ap] = [ap]; ap++
+%{ Input(Y) %}
+[ap] = [ap]; ap++
+[ap] = [[fp + 1] + 2]; ap++
+-- [fp + 3]
+[ap] = [[fp + 2] + 1]; ap++
+-- [fp + 4]
+[ap] = [[fp] + 1]; ap++
+-- [fp + 5]
+[ap] = [[fp] + 2]; ap++
+[ap] = [fp + 3] + [fp + 4]; ap++
+[ap] = [ap - 1] + [fp + 5]; ap++
+ret
+
+end: