The assert builtin (#3014)

* Requires #3015

examples/milestone/Bank/Bank.juvix

@@ -70,10 +70,6 @@ calculateInterest : Nat -> Nat -> Nat -> Nat
       incrAmount (a : Nat) : Nat := div (a * rate) 10000;
     in iterate (min 100 periods) incrAmount amount;
 
---- Asserts some ;Bool; condition.
-assert : {A : Type} -> Bool -> A -> A
-  | c a := ite c a (failwith "assertion failed");
-
 --- Returns a new ;Token;. Arguments are:
 ---
 --- `owner`: The address of the account to issue the token to
@@ -82,7 +78,7 @@ assert : {A : Type} -> Bool -> A -> A
 ---
 --- `caller`: Who is creating the transaction. It must be the bank.
 issue : Address -> Address -> Nat -> Token
-  | caller owner amount := assert (caller == bankAddress) (mkToken owner 0 amount);
+  | caller owner amount := assert (caller == bankAddress) >-> mkToken owner 0 amount;
 
 --- Deposits some amount of money into the bank.
 deposit (bal : Balances) (token : Token) (amount : Nat) : Token :=
@@ -102,11 +98,10 @@ withdraw
   (rate : Nat)
   (periods : Nat)
   : Token :=
-  assert
+  assert (caller == bankAddress)
-    (caller == bankAddress)
+    >-> let
-    (let
+          hash : Field := hashAddress recipient;
-      hash : Field := hashAddress recipient;
+          total : Nat := calculateInterest amount rate periods;
-      total : Nat := calculateInterest amount rate periods;
+          token : Token := mkToken recipient 0 total;
-      token : Token := mkToken recipient 0 total;
+          bal' : Balances := decrement hash amount bal;
-      bal' : Balances := decrement hash amount bal;
+        in runOnChain (commitBalances bal') token;
-    in runOnChain (commitBalances bal') token);

juvix-stdlib

@@ -1 +1 @@
-Subproject commit 615a02c8107076ca9661c5234d41792be91a5104
+Subproject commit 6010ad32f80498432b9a14752a0b7b50e9b36763

runtime/c/src/juvix/api.h

@@ -104,6 +104,7 @@ closure_label:
 #define JUVIX_INT_TO_UINT8(var0, var1) \
     (var0 = make_smallint((word_t)((uint8_t)(get_unboxed_int(var1) & 0xFF))))
 
+#define JUVIX_ASSERT(val) (assert(is_true(val)))
 #define JUVIX_TRACE(val) (io_trace(val))
 #define JUVIX_DUMP (stacktrace_dump())
 #define JUVIX_FAILURE(val) \

src/Juvix/Compiler/Asm/Extra/Recursors.hs

@@ -92,6 +92,8 @@ recurse' sig = go True
                 throw $
                   AsmError loc "popping empty value stack"
               return (popValueStack 1 mem)
+            Assert ->
+              return mem
             Trace ->
               return mem
             Dump ->
@@ -412,6 +414,8 @@ recurseS' sig = go True
               return (stackInfoPushValueStack 1 si)
             Pop -> do
               return (stackInfoPopValueStack 1 si)
+            Assert ->
+              return si
             Trace ->
               return si
             Dump ->

src/Juvix/Compiler/Asm/Interpreter.hs

@@ -82,6 +82,11 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
         goCode cont
       Pop ->
         popValueStack >> goCode cont
+      Assert -> do
+        v <- topValueStack
+        unless (v == ValBool True) $
+          runtimeError "assertion failed"
+        goCode cont
       Trace -> do
         v <- topValueStack
         logMessage (printValue infoTable v)

src/Juvix/Compiler/Asm/Language.hs

@@ -49,6 +49,9 @@ data Instruction
     Push Value
   | -- | Pop the stack. JVA opcode: 'pop'.
     Pop
+  | -- | Assert a boolean on top of the stack. Does not pop the stack. JVA
+    -- opcode: 'assert'.
+    Assert
   | -- | Print a debug log of the object on top of the stack. Does not pop the
     -- stack. JVA opcode: 'trace'.
     Trace

src/Juvix/Compiler/Asm/Pretty/Base.hs

@@ -98,6 +98,7 @@ instance PrettyCode Instruction where
     Cairo op -> Tree.ppCode op
     Push val -> (primitive Str.instrPush <+>) <$> ppCode val
     Pop -> return $ primitive Str.instrPop
+    Assert -> return $ primitive Str.instrAssert
     Trace -> return $ primitive Str.instrTrace
     Dump -> return $ primitive Str.instrDump
     Failure -> return $ primitive Str.instrFailure

src/Juvix/Compiler/Asm/Translation/FromSource.hs

@@ -91,6 +91,8 @@ command = do
       mkInstr' loc . Push <$> value
     "pop" ->
       return $ mkInstr' loc Pop
+    "assert" ->
+      return $ mkInstr' loc Assert
     "trace" ->
       return $ mkInstr' loc Trace
     "dump" ->

src/Juvix/Compiler/Asm/Translation/FromTree.hs

@@ -233,6 +233,7 @@ genCode fi =
     genUnOp :: Tree.UnaryOpcode -> Command
     genUnOp op = case op of
       Tree.PrimUnop op' -> mkUnop op'
+      Tree.OpAssert -> mkInstr Assert
       Tree.OpTrace -> mkInstr Trace
       Tree.OpFail -> mkInstr Failure
 

src/Juvix/Compiler/Backend/C/Translation/FromReg.hs

@@ -227,6 +227,8 @@ fromRegInstr bNoStack info = \case
     unsupported "Cairo builtin"
   Reg.Assign Reg.InstrAssign {..} ->
     return $ stmtsAssign (fromVarRef _instrAssignResult) (fromValue _instrAssignValue)
+  Reg.Assert Reg.InstrAssert {..} ->
+    return [StatementExpr $ macroCall "JUVIX_ASSERT" [fromValue _instrAssertValue]]
   Reg.Trace Reg.InstrTrace {..} ->
     return [StatementExpr $ macroCall "JUVIX_TRACE" [fromValue _instrTraceValue]]
   Reg.Dump ->

src/Juvix/Compiler/Backend/Cairo/Translation/FromCasm.hs

@@ -43,6 +43,7 @@ fromCasm instrs0 =
       Casm.Return -> goReturn
       Casm.Alloc x -> goAlloc x
       Casm.Hint x -> goHint x
+      Casm.Assert x -> goAssert x
       Casm.Trace {} -> []
       Casm.Label {} -> []
       Casm.Nop -> []
@@ -230,6 +231,14 @@ fromCasm instrs0 =
             . set instrApUpdate ApUpdateAdd
             $ defaultInstruction
 
+        goAssert :: Casm.InstrAssert -> [Element]
+        goAssert Casm.InstrAssert {..} =
+          toElems
+            . updateOps False (Casm.Val (Casm.Imm 0))
+            . updateDst _instrAssertValue
+            . set instrOpcode AssertEq
+            $ defaultInstruction
+
         goHint :: Casm.Hint -> [Element]
         goHint = \case
           Casm.HintInput var -> [ElementHint (Hint ("Input(" <> var <> ")"))]

src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs

@@ -130,6 +130,8 @@ fromRegInstr info = \case
     unsupported "Cairo builtin"
   Reg.Assign Reg.InstrAssign {..} ->
     stmtsAssign (mkVarRef _instrAssignResult) (fromValue _instrAssignValue)
+  Reg.Assert {} ->
+    unsupported "assert"
   Reg.Trace {} ->
     unsupported "trace"
   Reg.Dump ->

src/Juvix/Compiler/Builtins/Assert.hs

@@ -0,0 +1,24 @@
+module Juvix.Compiler.Builtins.Assert where
+
+import Juvix.Compiler.Internal.Builtins
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+checkAssert :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkAssert f = do
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
+  let assert_ = f ^. funDefName
+      l = getLoc f
+  varx <- freshVar l "x"
+  let x = toExpression varx
+      assertClauses :: [(Expression, Expression)]
+      assertClauses = [(assert_ @@ x, x)]
+  checkBuiltinFunctionInfo
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinAssert,
+        _funInfoSignature = bool_ --> bool_,
+        _funInfoClauses = assertClauses,
+        _funInfoFreeVars = [varx],
+        _funInfoFreeTypeVars = []
+      }

src/Juvix/Compiler/Casm/Interpreter.hs

@@ -64,6 +64,7 @@ hRunCode hout inputInfo (LabelInfo labelInfo) instrs0 = runST goCode
             Call x -> goCall x pc ap fp mem
             Return -> goReturn pc ap fp mem
             Alloc x -> goAlloc x pc ap fp mem
+            Assert x -> goAssert x pc ap fp mem
             Trace x -> goTrace x pc ap fp mem
             Hint x -> goHint x pc ap fp mem
             Label {} -> go (pc + 1) ap fp mem
@@ -244,6 +245,13 @@ hRunCode hout inputInfo (LabelInfo labelInfo) instrs0 = runST goCode
       v <- readRValue ap fp mem _instrAllocSize
       go (pc + 1) (ap + fromInteger (fieldToInteger v)) fp mem
 
+    goAssert :: InstrAssert -> Address -> Address -> Address -> Memory s -> ST s FField
+    goAssert InstrAssert {..} pc ap fp mem = do
+      v <- readMemRef ap fp mem _instrAssertValue
+      when (fieldToInteger v /= 0) $
+        throwRunError "assertion failed"
+      go (pc + 1) ap fp mem
+
     goTrace :: InstrTrace -> Address -> Address -> Address -> Memory s -> ST s FField
     goTrace InstrTrace {..} pc ap fp mem = do
       v <- readRValue ap fp mem _instrTraceValue

src/Juvix/Compiler/Casm/Keywords.hs

@@ -11,6 +11,7 @@ import Juvix.Data.Keyword.All
     kwAbs,
     kwAp,
     kwApPlusPlus,
+    kwAssert,
     kwCall,
     kwColon,
     kwDiv,
@@ -45,6 +46,7 @@ allKeywords =
     kwAbs,
     kwAp,
     kwApPlusPlus,
+    kwAssert,
     kwCall,
     kwColon,
     kwDiv,

src/Juvix/Compiler/Casm/Language.hs

@@ -90,6 +90,7 @@ data Instruction
   | Call InstrCall
   | Return
   | Alloc InstrAlloc
+  | Assert InstrAssert
   | Trace InstrTrace
   | Hint Hint
   | Label LabelRef
@@ -132,6 +133,10 @@ newtype InstrAlloc = InstrAlloc
   { _instrAllocSize :: RValue
   }
 
+newtype InstrAssert = InstrAssert
+  { _instrAssertValue :: MemRef
+  }
+
 newtype InstrTrace = InstrTrace
   { _instrTraceValue :: RValue
   }
@@ -148,4 +153,5 @@ makeLenses ''InstrJump
 makeLenses ''InstrJumpIf
 makeLenses ''InstrCall
 makeLenses ''InstrAlloc
+makeLenses ''InstrAssert
 makeLenses ''InstrTrace

src/Juvix/Compiler/Casm/Pretty/Base.hs

@@ -171,6 +171,11 @@ instance PrettyCode InstrAlloc where
     s <- ppCode _instrAllocSize
     return $ Str.ap <+> Str.plusequal <+> s
 
+instance PrettyCode InstrAssert where
+  ppCode InstrAssert {..} = do
+    v <- ppCode _instrAssertValue
+    return $ Str.assert_ <+> v
+
 instance PrettyCode InstrTrace where
   ppCode InstrTrace {..} = do
     v <- ppCode _instrTraceValue
@@ -185,6 +190,7 @@ instance PrettyCode Instruction where
     Call x -> ppCode x
     Return -> return Str.ret
     Alloc x -> ppCode x
+    Assert x -> ppCode x
     Trace x -> ppCode x
     Hint x -> ppCode x
     Label x -> (<> colon) <$> ppCode x

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

@@ -286,6 +286,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
           Reg.Assign x -> goAssign x
           Reg.Alloc x -> goAlloc x
           Reg.AllocClosure x -> goAllocClosure x
+          Reg.Assert x -> goAssert x
           Reg.Trace x -> goTrace x
           Reg.Dump -> unsupported "dump"
           Reg.Failure x -> goFail x
@@ -512,6 +513,18 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
             storedArgsNum = length _instrAllocClosureArgs
             leftArgsNum = _instrAllocClosureExpectedArgsNum - storedArgsNum
 
+        goAssert :: Reg.InstrAssert -> Sem r ()
+        goAssert Reg.InstrAssert {..} = do
+          v <- goValue _instrAssertValue
+          case v of
+            Imm c
+              | c == 0 -> return ()
+              | otherwise ->
+                  output' 0 $ mkAssign (MemRef Ap 0) (Binop $ BinopValue FieldAdd (MemRef Ap 0) (Imm 1))
+            Ref r ->
+              output' 0 $ Assert (InstrAssert r)
+            Lab {} -> unsupported "assert label"
+
         goTrace :: Reg.InstrTrace -> Sem r ()
         goTrace Reg.InstrTrace {..} = do
           v <- mkRValue _instrTraceValue

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

@@ -74,6 +74,7 @@ instruction =
     <|> parseJump
     <|> parseCall
     <|> parseReturn
+    <|> parseAssert
     <|> parseTrace
     <|> parseAssign
 
@@ -249,6 +250,12 @@ parseReturn = do
   kw kwRet
   return Return
 
+parseAssert :: ParsecS r Instruction
+parseAssert = do
+  kw kwAssert
+  r <- parseMemRef
+  return $ Assert $ InstrAssert {_instrAssertValue = r}
+
 parseTrace :: (Member LabelInfoBuilder r) => ParsecS r Instruction
 parseTrace = do
   kw kwTrace

src/Juvix/Compiler/Casm/Validate.hs

@@ -18,6 +18,7 @@ validate labi instrs = mapM_ go instrs
       Call x -> goCall x
       Return -> return ()
       Alloc x -> goAlloc x
+      Assert x -> goAssert x
       Trace x -> goTrace x
       Hint {} -> return ()
       Label {} -> return ()
@@ -66,3 +67,6 @@ validate labi instrs = mapM_ go instrs
 
     goTrace :: InstrTrace -> Either CasmError ()
     goTrace InstrTrace {..} = goRValue _instrTraceValue
+
+    goAssert :: InstrAssert -> Either CasmError ()
+    goAssert InstrAssert {} = return ()

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -125,7 +125,8 @@ instance Serialize BuiltinConstructor
 instance NFData BuiltinConstructor
 
 data BuiltinFunction
-  = BuiltinNatPlus
+  = BuiltinAssert
+  | BuiltinNatPlus
   | BuiltinNatSub
   | BuiltinNatMul
   | BuiltinNatUDiv
@@ -163,6 +164,7 @@ instance NFData BuiltinFunction
 
 instance Pretty BuiltinFunction where
   pretty = \case
+    BuiltinAssert -> Str.assert
     BuiltinNatPlus -> Str.natPlus
     BuiltinNatSub -> Str.natSub
     BuiltinNatMul -> Str.natMul
@@ -368,6 +370,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
+  BuiltinAssert -> False
   BuiltinBoolIf -> False
   BuiltinBoolOr -> False
   BuiltinBoolAnd -> False
@@ -403,6 +406,7 @@ isIntBuiltin = \case
   BuiltinIntLe -> True
   BuiltinIntLt -> True
   --
+  BuiltinAssert -> False
   BuiltinNatPlus -> False
   BuiltinNatSub -> False
   BuiltinNatMul -> False
@@ -425,6 +429,7 @@ isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
+  BuiltinAssert -> False
   BuiltinIntEq -> False
   BuiltinIntPlus -> False
   BuiltinIntSubNat -> False
@@ -496,6 +501,7 @@ isIgnoredBuiltin f
       -- Monad
       BuiltinMonadBind -> False
       -- Ignored
+      BuiltinAssert -> True
       BuiltinBoolIf -> True
       BuiltinBoolOr -> True
       BuiltinBoolAnd -> True

src/Juvix/Compiler/Core/Evaluator.hs

@@ -217,6 +217,7 @@ geval opts herr tab env0 = eval' env0
       OpSeq -> seqOp
       OpFail -> failOp
       OpTrace -> traceOp
+      OpAssert -> assertOp
       OpAnomaGet -> anomaGetOp
       OpAnomaEncode -> anomaEncodeOp
       OpAnomaDecode -> anomaDecodeOp
@@ -367,6 +368,21 @@ geval opts herr tab env0 = eval' env0
                       unsafePerformIO (hPutStrLn herr (printNode v) >> return v)
         {-# INLINE traceOp #-}
 
+        assertOp :: [Node] -> Node
+        assertOp = unary $ \val ->
+          let !v = eval' env val
+           in if
+                  | opts ^. evalOptionsSilent ->
+                      v
+                  | otherwise ->
+                      case v of
+                        NCtr Constr {..}
+                          | _constrTag == BuiltinTag TagTrue ->
+                              v
+                        _ ->
+                          Exception.throw (EvalError ("assertion failed: " <> printNode val) Nothing)
+        {-# INLINE assertOp #-}
+
         anomaGetOp :: [Node] -> Node
         anomaGetOp = unary $ \arg ->
           if

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -188,6 +188,7 @@ containsDebugOperations = ufold (\x xs -> x || or xs) isDebugOp
           OpTrace -> True
           OpFail -> True
           OpSeq -> True
+          OpAssert -> False
           OpAnomaByteArrayFromAnomaContents -> False
           OpAnomaByteArrayToAnomaContents -> False
           OpAnomaDecode -> False
@@ -466,6 +467,7 @@ builtinOpArgTypes = \case
   OpShow -> [mkDynamic']
   OpStrConcat -> [mkTypeString', mkTypeString']
   OpStrToInt -> [mkTypeString']
+  OpAssert -> [mkTypeBool']
   OpSeq -> [mkDynamic', mkDynamic']
   OpTrace -> [mkDynamic']
   OpFail -> [mkTypeString']

src/Juvix/Compiler/Core/Keywords.hs

@@ -15,6 +15,7 @@ import Juvix.Data.Keyword.All
     kwAnomaVerifyDetached,
     kwAnomaVerifyWithMessage,
     kwAny,
+    kwAssert,
     kwAssign,
     kwBindOperator,
     kwBottom,
@@ -72,6 +73,7 @@ allKeywordStrings = keywordsStrings allKeywords
 allKeywords :: [Keyword]
 allKeywords =
   [ delimSemicolon,
+    kwAssert,
     kwAssign,
     kwBottom,
     kwBuiltin,

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -24,6 +24,7 @@ data BuiltinOp
   | OpStrConcat
   | OpStrToInt
   | OpSeq
+  | OpAssert
   | OpTrace
   | OpFail
   | OpAnomaGet
@@ -84,6 +85,7 @@ builtinOpArgsNum = \case
   OpStrConcat -> 2
   OpStrToInt -> 1
   OpSeq -> 2
+  OpAssert -> 1
   OpTrace -> 1
   OpFail -> 1
   OpAnomaGet -> 1
@@ -133,6 +135,7 @@ builtinIsFoldable = \case
   OpStrConcat -> True
   OpStrToInt -> True
   OpSeq -> False
+  OpAssert -> False
   OpTrace -> False
   OpFail -> False
   OpAnomaGet -> False

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -50,6 +50,7 @@ instance PrettyCode BuiltinOp where
     OpShow -> return primShow
     OpStrConcat -> return primStrConcat
     OpStrToInt -> return primStrToInt
+    OpAssert -> return primAssert
     OpSeq -> return primSeq
     OpTrace -> return primTrace
     OpFail -> return primFail
@@ -867,6 +868,9 @@ kwPi = keyword Str.piUnicode
 kwDef :: Doc Ann
 kwDef = keyword Str.def
 
+primAssert :: Doc Ann
+primAssert = primitive Str.assert_
+
 primSeq :: Doc Ann
 primSeq = primitive Str.seqq_
 

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -64,6 +64,9 @@ computeNodeTypeInfo md = umapL go
           OpSeq -> case _builtinAppArgs of
             [_, arg2] -> Info.getNodeType arg2
             _ -> error "incorrect seq builtin application"
+          OpAssert -> case _builtinAppArgs of
+            [arg] -> Info.getNodeType arg
+            _ -> error "incorrect assert builtin application"
           OpTrace -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect trace builtin application"

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -1309,6 +1309,11 @@ goApplication a = do
             (_ : _ : arg1 : arg2 : xs) ->
               return (mkApps' (mkBuiltinApp' OpSeq [arg1, arg2]) xs)
             _ -> error "internal to core: seq must be called with 2 arguments"
+        Just Internal.BuiltinAssert -> do
+          as <- exprArgs
+          case as of
+            (x : xs) -> return (mkApps' (mkBuiltinApp' OpAssert [x]) xs)
+            _ -> error "internal to core: assert must be called with 1 argument"
         _ -> app
     _ -> app
 

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -569,6 +569,7 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwShow $> OpShow)
       <|> (kw kwStrConcat $> OpStrConcat)
       <|> (kw kwStrToInt $> OpStrToInt)
+      <|> (kw kwAssert $> OpAssert)
       <|> (kw kwSeqq $> OpSeq)
       <|> (kw kwTrace $> OpTrace)
       <|> (kw kwFail $> OpFail)

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -28,6 +28,7 @@ fromCore fsize tab =
 
     shouldKeepFunction :: BuiltinFunction -> Bool
     shouldKeepFunction = \case
+      BuiltinAssert -> False
       BuiltinNatPlus -> False
       BuiltinNatSub -> False
       BuiltinNatMul -> False

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -14,6 +14,7 @@ import Data.HashSet qualified as HashSet
 import Data.IntMap.Strict qualified as IntMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Builtins
+import Juvix.Compiler.Builtins.Assert
 import Juvix.Compiler.Builtins.Pair
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra qualified as Concrete
@@ -537,6 +538,7 @@ checkBuiltinFunction ::
   BuiltinFunction ->
   Sem r ()
 checkBuiltinFunction d f = localBuiltins $ case f of
+  BuiltinAssert -> checkAssert d
   BuiltinNatPlus -> checkNatPlus d
   BuiltinNatSub -> checkNatSub d
   BuiltinNatMul -> checkNatMul d

src/Juvix/Compiler/Nockma/Translation/FromTree.hs

@@ -517,6 +517,9 @@ compile = \case
       arg <- compile _nodeUnopArg
       case _nodeUnopOpcode of
         Tree.PrimUnop op -> return $ goPrimUnop op arg
+        Tree.OpAssert ->
+          -- TODO: remove duplication of `arg` here
+          return (branch arg arg crash)
         Tree.OpFail -> return crash
         Tree.OpTrace -> goTrace arg
 
@@ -525,6 +528,7 @@ compile = \case
       Tree.OpShow -> stringsErr "show"
       Tree.OpStrToInt -> stringsErr "strToInt"
       Tree.OpArgsNum ->
+        -- TODO: remove duplication of `arg` here!!!
         let getF f = getClosureField f arg
          in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum)
       Tree.OpIntToField -> fieldErr
@@ -651,6 +655,7 @@ compile = \case
       enabled <- asks (^. compilerOptions . compilerOptionsEnableTrace)
       return $
         if
+            -- TODO: remove duplication of `arg` here
             | enabled -> OpTrace # arg # arg
             | otherwise -> arg
 

src/Juvix/Compiler/Reg/Extra/Base.hs

@@ -53,6 +53,7 @@ overValueRefs'' f = \case
   If x -> If <$> goIf x
   Branch x -> Branch <$> goBranch x
   Case x -> Case <$> goCase x
+  Assert x -> Assert <$> goAssert x
   Trace x -> Trace <$> goTrace x
   Dump -> return Dump
   Failure x -> Failure <$> goFailure x
@@ -174,6 +175,9 @@ overValueRefs'' f = \case
     goCase :: InstrCase -> m InstrCase
     goCase = overM instrCaseValue goValue
 
+    goAssert :: InstrAssert -> m InstrAssert
+    goAssert = overM instrAssertValue goValue
+
     goTrace :: InstrTrace -> m InstrTrace
     goTrace = overM instrTraceValue goValue
 

src/Juvix/Compiler/Reg/Extra/Blocks.hs

@@ -79,6 +79,7 @@ getValueRefs = \case
   Assign x -> goAssign x
   Alloc x -> goAlloc x
   AllocClosure x -> goAllocClosure x
+  Assert x -> goAssert x
   Trace x -> goTrace x
   Dump -> []
   Failure x -> goFailure x
@@ -103,6 +104,9 @@ getValueRefs = \case
     goAllocClosure :: InstrAllocClosure -> [VarRef]
     goAllocClosure InstrAllocClosure {..} = concatMap getValueRefs'' _instrAllocClosureArgs
 
+    goAssert :: InstrAssert -> [VarRef]
+    goAssert InstrAssert {..} = getValueRefs'' _instrAssertValue
+
     goTrace :: InstrTrace -> [VarRef]
     goTrace InstrTrace {..} = getValueRefs'' _instrTraceValue
 

src/Juvix/Compiler/Reg/Extra/Info.hs

@@ -21,6 +21,7 @@ computeMaxStackHeight lims = maximum . map go
       Unop {} -> 0
       Cairo {} -> 0
       Assign {} -> 0
+      Assert {} -> 0
       Trace {} -> 0
       Dump -> 0
       Failure {} -> 0
@@ -73,6 +74,7 @@ computeMaxCallClosuresArgsNum = maximum . map go
       Unop {} -> 0
       Cairo {} -> 0
       Assign {} -> 0
+      Assert {} -> 0
       Trace {} -> 0
       Dump -> 0
       Failure {} -> 0
@@ -121,6 +123,8 @@ computeStringMap strs = snd . run . execState (HashMap.size strs, strs) . mapM g
         mapM_ goVal _instrCairoArgs
       Assign InstrAssign {..} ->
         goVal _instrAssignValue
+      Assert InstrAssert {..} ->
+        goVal _instrAssertValue
       Trace InstrTrace {..} ->
         goVal _instrTraceValue
       Dump -> return ()
@@ -180,6 +184,7 @@ computeLocalVarsNum = maximum . map go
       Unop InstrUnop {..} -> goVarRef _instrUnopResult
       Cairo InstrCairo {..} -> goVarRef _instrCairoResult
       Assign InstrAssign {..} -> goVarRef _instrAssignResult
+      Assert {} -> 0
       Trace {} -> 0
       Dump -> 0
       Failure {} -> 0

src/Juvix/Compiler/Reg/Interpreter.hs

@@ -48,6 +48,7 @@ runFunction hout infoTable args0 info0 = do
         Unop x -> goUnop args tmps instrs x
         Cairo {} -> throwRunError "unsupported: Cairo builtin" Nothing
         Assign x -> goAssign args tmps instrs x
+        Assert x -> goAssert args tmps instrs x
         Trace x -> goTrace args tmps instrs x
         Dump -> goDump args tmps instrs
         Failure x -> goFailure args tmps instrs x
@@ -130,6 +131,15 @@ runFunction hout infoTable args0 info0 = do
       writeVarRef args tmps _instrAssignResult val
       go args tmps instrs
 
+    goAssert :: Args -> Vars s -> Code -> InstrAssert -> ST s Val
+    goAssert args tmps instrs InstrAssert {..} = do
+      val <- readValue args tmps _instrAssertValue
+      case val of
+        ValBool True ->
+          go args tmps instrs
+        _ ->
+          throwRunError "assertion failed" Nothing
+
     goTrace :: Args -> Vars s -> Code -> InstrTrace -> ST s Val
     goTrace args tmps instrs InstrTrace {..} = do
       val <- readValue args tmps _instrTraceValue

src/Juvix/Compiler/Reg/Keywords.hs

@@ -10,6 +10,7 @@ import Juvix.Data.Keyword.All
   ( kwAdd_,
     kwAlloc,
     kwArgsNum,
+    kwAssert,
     kwAtoi,
     kwBr,
     kwCAlloc,
@@ -74,6 +75,7 @@ allKeywords =
          kwIf,
          kwShow,
          kwAtoi,
+         kwAssert,
          kwTrace,
          kwDump,
          kwPrealloc,

src/Juvix/Compiler/Reg/Language.hs

@@ -25,7 +25,8 @@ data Instruction
   | Branch InstrBranch
   | Case InstrCase
   | ----
-    Trace InstrTrace
+    Assert InstrAssert
+  | Trace InstrTrace
   | Dump
   | Failure InstrFailure
   | Prealloc InstrPrealloc

src/Juvix/Compiler/Reg/Language/Blocks.hs

@@ -20,6 +20,7 @@ data Instruction
   | Assign InstrAssign
   | Alloc InstrAlloc
   | AllocClosure InstrAllocClosure
+  | Assert InstrAssert
   | Trace InstrTrace
   | Dump
   | Failure InstrFailure

src/Juvix/Compiler/Reg/Language/Instrs.hs

@@ -80,6 +80,11 @@ data InstrAssign = InstrAssign
   }
   deriving stock (Eq)
 
+newtype InstrAssert = InstrAssert
+  { _instrAssertValue :: Value
+  }
+  deriving stock (Eq)
+
 newtype InstrTrace = InstrTrace
   { _instrTraceValue :: Value
   }
@@ -184,6 +189,7 @@ makeLenses ''InstrBinop
 makeLenses ''InstrUnop
 makeLenses ''InstrCairo
 makeLenses ''InstrAssign
+makeLenses ''InstrAssert
 makeLenses ''InstrTrace
 makeLenses ''InstrFailure
 makeLenses ''InstrAlloc

src/Juvix/Compiler/Reg/Pretty/Base.hs

@@ -75,6 +75,11 @@ instance PrettyCode InstrAssign where
     val <- ppCode _instrAssignValue
     return $ res <+> primitive Str.equal <+> val
 
+instance PrettyCode InstrAssert where
+  ppCode InstrAssert {..} = do
+    val <- ppCode _instrAssertValue
+    return $ primitive Str.assert_ <+> val
+
 instance PrettyCode InstrTrace where
   ppCode InstrTrace {..} = do
     val <- ppCode _instrTraceValue
@@ -271,6 +276,7 @@ instance PrettyCode Instruction where
     Unop x -> ppCode x
     Cairo x -> ppCode x
     Assign x -> ppCode x
+    Assert x -> ppCode x
     Trace x -> ppCode x
     Dump -> return $ primitive Str.dump
     Failure x -> ppCode x

src/Juvix/Compiler/Reg/Translation/Blocks/FromReg.hs

@@ -30,6 +30,7 @@ fromReg = over infoFunctions (fmap (over functionCode goCode))
         Reg.Case x -> mkBlock (Case (fmap goCode x))
         Reg.CallClosures {} -> impossible
         Reg.TailCallClosures {} -> impossible
+        Reg.Assert x -> over blockBody (Assert x :) (goCode is)
         Reg.Trace x -> over blockBody (Trace x :) (goCode is)
         Reg.Dump -> over blockBody (Dump :) (goCode is)
         Reg.Failure x -> over blockBody (Failure x :) (goCode is)

src/Juvix/Compiler/Reg/Translation/FromAsm.hs

@@ -69,6 +69,7 @@ fromAsmInstr funInfo tab si Asm.CmdInstr {..} =
     Asm.Cairo op -> return $ mkCairo op
     Asm.Push val -> return $ mkAssign (mkVarRef VarGroupLocal (ntmps + n + 1)) (mkValue val)
     Asm.Pop -> return Nop
+    Asm.Assert -> return $ Assert $ InstrAssert (VRef $ mkVarRef VarGroupLocal (ntmps + n))
     Asm.Trace -> return $ Trace $ InstrTrace (VRef $ mkVarRef VarGroupLocal (ntmps + n))
     Asm.Dump -> return Dump
     Asm.Failure -> return $ Failure $ InstrFailure (VRef $ mkVarRef VarGroupLocal (ntmps + n))

src/Juvix/Compiler/Reg/Translation/FromSource.hs

@@ -53,6 +53,7 @@ instruction ::
   ParsecS r Instruction
 instruction =
   (instrNop >> return Nop)
+    <|> (Assert <$> instrAssert)
     <|> (Trace <$> instrTrace)
     <|> (instrDump >> return Dump)
     <|> (Failure <$> instrFailure)
@@ -195,6 +196,17 @@ instrTrace = do
       { _instrTraceValue = val
       }
 
+instrAssert ::
+  (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) =>
+  ParsecS r InstrAssert
+instrAssert = do
+  kw kwAssert
+  val <- value
+  return
+    InstrAssert
+      { _instrAssertValue = val
+      }
+
 instrDump :: ParsecS r ()
 instrDump = kw kwDump
 

src/Juvix/Compiler/Tree/Evaluator.hs

@@ -75,6 +75,7 @@ hEval hout tab = eval' [] mempty
           let !v = eval' args temps _nodeUnopArg
            in case _nodeUnopOpcode of
                 PrimUnop op -> eitherToError $ evalUnop tab op v
+                OpAssert -> goAssert v
                 OpTrace -> goTrace v
                 OpFail -> goFail v
 
@@ -105,6 +106,11 @@ hEval hout tab = eval' [] mempty
                     _ -> evalError "expected either a nullary or a binary constructor"
                   _ -> evalError "expected a constructor"
 
+        goAssert :: Value -> Value
+        goAssert = \case
+          ValBool True -> ValBool True
+          _ -> evalError "assertion failed"
+
         goFail :: Value -> Value
         goFail v = evalError ("failure: " <> printValue tab v)
 

src/Juvix/Compiler/Tree/EvaluatorEff.hs

@@ -70,6 +70,7 @@ eval tab = runReader emptyEvalCtx . eval'
           v <- eval' _nodeUnopArg
           case _nodeUnopOpcode of
             PrimUnop op -> eitherToError $ evalUnop tab op v
+            OpAssert -> goAssert v
             OpTrace -> goTrace v
             OpFail -> goFail v
 
@@ -100,6 +101,12 @@ eval tab = runReader emptyEvalCtx . eval'
                     _ -> evalError "expected either a nullary or a binary constructor"
                   _ -> evalError "expected a constructor"
 
+        goAssert :: Value -> Sem r' Value
+        goAssert = \case
+          ValBool True -> return $ ValBool True
+          ValBool False -> evalError "assertion failed"
+          v -> evalError ("expected a boolean: " <> printValue tab v)
+
         goFail :: Value -> Sem r' Value
         goFail v = evalError ("failure: " <> printValue tab v)
 

src/Juvix/Compiler/Tree/Keywords.hs

@@ -17,6 +17,7 @@ import Juvix.Data.Keyword.All
     kwAnomaVerifyDetached,
     kwAnomaVerifyWithMessage,
     kwArgsNum,
+    kwAssert,
     kwAtoi,
     kwBr,
     kwByteArrayFromListUInt8,
@@ -70,6 +71,7 @@ allKeywords =
          kwStrcat,
          kwShow,
          kwAtoi,
+         kwAssert,
          kwTrace,
          kwFail,
          kwArgsNum,

src/Juvix/Compiler/Tree/Language.hs

@@ -65,6 +65,8 @@ data BinaryOpcode
 
 data UnaryOpcode
   = PrimUnop UnaryOp
+  | -- | Assert a boolean and return it
+    OpAssert
   | -- | Print a debug log of the argument and return it.
     OpTrace
   | -- | Interrupt execution with a runtime error printing the argument.

src/Juvix/Compiler/Tree/Pretty/Base.hs

@@ -297,6 +297,7 @@ instance PrettyCode AnomaOp where
 instance PrettyCode UnaryOpcode where
   ppCode = \case
     PrimUnop x -> ppCode x
+    OpAssert -> return $ primitive Str.instrAssert
     OpTrace -> return $ primitive Str.instrTrace
     OpFail -> return $ primitive Str.instrFailure
 

src/Juvix/Compiler/Tree/Transformation/Validate.hs

@@ -65,6 +65,7 @@ inferType tab funInfo = goInfer mempty
     goUnop :: BinderList Type -> NodeUnop -> Sem r Type
     goUnop bl NodeUnop {..} = case _nodeUnopOpcode of
       PrimUnop x -> checkPrimUnop x
+      OpAssert -> goInfer bl _nodeUnopArg
       OpTrace -> goInfer bl _nodeUnopArg
       OpFail -> checkUnop TyDynamic TyDynamic
       where

src/Juvix/Compiler/Tree/Translation/FromAsm.hs

@@ -92,6 +92,7 @@ goFunction infoTab fi = do
           Asm.Push (Asm.Constant c) -> return (mkConst c)
           Asm.Push (Asm.Ref r) -> return (mkMemRef r)
           Asm.Pop -> goPop
+          Asm.Assert -> goAssert
           Asm.Trace -> goTrace
           Asm.Dump -> unsupported (_cmdInstrInfo ^. Asm.commandInfoLocation)
           Asm.Failure -> goUnop OpFail
@@ -244,8 +245,8 @@ goFunction infoTab fi = do
                   _nodeBinopArg2 = arg2
                 }
 
-        goTrace :: Sem r Node
+        goSeqOp :: UnaryOpcode -> Sem r Node
-        goTrace = do
+        goSeqOp op = do
           arg <- goCode
           off <- asks (^. tempSize)
           let ref = mkMemRef $ DRef $ mkTempRef $ OffsetRef off Nothing
@@ -264,13 +265,19 @@ goFunction infoTab fi = do
                             Unop
                               NodeUnop
                                 { _nodeUnopInfo = mempty,
-                                  _nodeUnopOpcode = OpTrace,
+                                  _nodeUnopOpcode = op,
                                   _nodeUnopArg = ref
                                 },
                           _nodeBinopArg2 = ref
                         }
                 }
 
+        goAssert :: Sem r Node
+        goAssert = goSeqOp OpAssert
+
+        goTrace :: Sem r Node
+        goTrace = goSeqOp OpTrace
+
         goArgs :: Int -> Sem r [Node]
         goArgs n = mapM (const goCode) [1 .. n]
 

src/Juvix/Compiler/Tree/Translation/FromCore.hs

@@ -163,6 +163,16 @@ genCode infoTable fi =
                 _nodeAnomaOpcode = genAnomaOp _builtinAppOp,
                 _nodeAnomaArgs = args
               }
+      | _builtinAppOp == Core.OpAssert =
+          case args of
+            [arg] ->
+              Unop $
+                NodeUnop
+                  { _nodeUnopInfo = mempty,
+                    _nodeUnopOpcode = OpAssert,
+                    _nodeUnopArg = arg
+                  }
+            _ -> impossible
       | otherwise =
           case args of
             [arg] ->

src/Juvix/Compiler/Tree/Translation/FromSource.hs

@@ -106,6 +106,7 @@ parseUnop ::
 parseUnop =
   parseUnaryOp kwShow (PrimUnop OpShow)
     <|> parseUnaryOp kwAtoi (PrimUnop OpStrToInt)
+    <|> parseUnaryOp kwAssert OpAssert
     <|> parseUnaryOp kwTrace OpTrace
     <|> parseUnaryOp kwFail OpFail
     <|> parseUnaryOp kwArgsNum (PrimUnop OpArgsNum)

src/Juvix/Data/Keyword/All.hs

@@ -265,6 +265,9 @@ kwSeqq = asciiKw Str.seqq_
 kwSSeq :: Keyword
 kwSSeq = asciiKw Str.sseq_
 
+kwAssert :: Keyword
+kwAssert = asciiKw Str.assert_
+
 kwTrace :: Keyword
 kwTrace = asciiKw Str.trace_
 

src/Juvix/Extra/Strings.hs

@@ -260,6 +260,9 @@ ioSequence = "IO-sequence"
 ioReadline :: (IsString s) => s
 ioReadline = "IO-readline"
 
+assert :: (IsString s) => s
+assert = "assert"
+
 natPrint :: (IsString s) => s
 natPrint = "nat-print"
 
@@ -482,6 +485,9 @@ sseq_ = "seq"
 eq :: (IsString s) => s
 eq = "eq"
 
+assert_ :: (IsString s) => s
+assert_ = "assert"
+
 trace_ :: (IsString s) => s
 trace_ = "trace"
 
@@ -845,6 +851,9 @@ instrPusht = "pusht"
 instrPopt :: (IsString s) => s
 instrPopt = "popt"
 
+instrAssert :: (IsString s) => s
+instrAssert = "assert"
+
 instrTrace :: (IsString s) => s
 instrTrace = "trace"
 

test/Casm/Compilation/Positive.hs

@@ -557,5 +557,13 @@ tests =
         $(mkRelDir ".")
         $(mkRelFile "test077.juvix")
         (Just $(mkRelFile "in/test077.json"))
-        $(mkRelFile "out/test077.out")
+        $(mkRelFile "out/test077.out"),
+      posTest
+        "Test078: Assertions"
+        True
+        True
+        $(mkRelDir ".")
+        $(mkRelFile "test078.juvix")
+        Nothing
+        $(mkRelFile "out/test078.out")
     ]

test/Casm/Run/Positive.hs

@@ -178,5 +178,13 @@ tests =
       $(mkRelDir ".")
       $(mkRelFile "test017.casm")
       $(mkRelFile "out/test017.out")
+      Nothing,
+    PosTest
+      "Test018: Assertions"
+      True
+      True
+      $(mkRelDir ".")
+      $(mkRelFile "test018.casm")
+      $(mkRelFile "out/test018.out")
       Nothing
   ]

tests/Casm/Compilation/positive/out/test078.out

@@ -0,0 +1 @@
+482630520

tests/Casm/Compilation/positive/test077.juvix

@@ -40,11 +40,3 @@ main
         | else := Resource.fld0 input;
     y := Resource.fld1 input
   };
-
-{-
-main
-  (input : Resource)
-  (path : List (Pair Field Bool))
-  : Field :=
-  count path;
--}

tests/Casm/Compilation/positive/test078.juvix

@@ -0,0 +1,11 @@
+module test078;
+
+import Stdlib.Prelude open;
+
+fact' (acc : Nat) : Nat → Nat
+  | zero := acc
+  | (suc x) := assert (acc /= 0) >-> fact' (acc * suc x) x;
+
+fact : Nat → Nat := fact' 1;
+
+main : Nat := assert (fact 10 == 10 * fact 9) >-> fact 5 + fact 10 + fact 12;

tests/Casm/positive/out/test018.out

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

tests/Casm/positive/test018.casm

@@ -0,0 +1,13 @@
+-- assertions
+
+start:
+  [ap] = 10
+  [ap + 1] = 1
+  ap += 2
+loop:
+  [ap] = [ap - 2] - 1
+  [ap + 1] = [ap - 1] * [ap - 2]
+  ap += 2
+  jmp loop if [ap - 2] != 0
+  [ap] = [ap - 1] - 3628800; ap++
+  assert [ap - 1]