assert builtins

runtime/c/src/juvix/api.h

@@ -33,9 +33,10 @@
     DECL_TAIL_APPLY_3;                              \
     juvix_program_start:
 
-#define JUVIX_EPILOGUE              \
-    juvix_program_end : STACK_POPT; \
-    IO_INTERPRET;                   \
+#define JUVIX_EPILOGUE \
+    juvix_program_end: \
+    STACK_POPT;        \
+    IO_INTERPRET;      \
     io_print_toplevel(juvix_result);
 
 // Temporary / local vars
@@ -44,7 +45,9 @@
 
 // Begin a function definition. `max_stack` is the maximum stack allocation in
 // the function.
-#define JUVIX_FUNCTION(label, max_stack) label : STACK_ENTER((max_stack))
+#define JUVIX_FUNCTION(label, max_stack) \
+    label:                               \
+    STACK_ENTER((max_stack))
 
 /*
     Macro sequence for function definition:
@@ -64,7 +67,8 @@
 */
 
 // Begin a function with no stack allocation.
-#define JUVIX_FUNCTION_NS(label) label:
+#define JUVIX_FUNCTION_NS(label) \
+    label:
 
 #define JUVIX_INT_ADD(var0, var1, var2) (var0 = smallint_add(var1, var2))
 #define JUVIX_INT_SUB(var0, var1, var2) (var0 = smallint_sub(var1, var2))
@@ -104,6 +108,7 @@
 #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

@@ -6,11 +6,19 @@ import Juvix.Prelude
 
 checkAssert :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
 checkAssert f = do
-  let ftype = f ^. funDefType
-      u = ExpressionUniverse smallUniverseNoLoc
-      l = getLoc f
   bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
-  valueT <- freshVar l "valueT"
-  let freeVars = hashSet [valueT]
-  unless ((ftype ==% (u <>--> bool_ --> valueT --> valueT)) freeVars) $
-    builtinsErrorText (getLoc f) "assert must be of type {Value : Type} -> Bool -> Value -> Value"
+  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

@@ -468,7 +468,6 @@ isIgnoredBuiltin f
         .&&. (not . isIntBuiltin)
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
-        .&&. (/= BuiltinAssert)
         $ f
 
     explicit :: Bool
@@ -501,9 +500,8 @@ isIgnoredBuiltin f
       BuiltinNatEq -> False
       -- Monad
       BuiltinMonadBind -> False
-      -- Assert
-      BuiltinAssert -> 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/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,