From 010ba7ecc2bde429592c0b8f4f709696cf067ff1 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 9 Sep 2024 18:54:13 +0200
Subject: [PATCH] assert builtins

---
 runtime/c/src/juvix/api.h                     | 15 ++++++++-----
 src/Juvix/Compiler/Asm/Extra/Recursors.hs     |  4 ++++
 src/Juvix/Compiler/Asm/Interpreter.hs         |  5 +++++
 src/Juvix/Compiler/Asm/Language.hs            |  3 +++
 src/Juvix/Compiler/Asm/Pretty/Base.hs         |  1 +
 .../Compiler/Asm/Translation/FromSource.hs    |  2 ++
 .../Compiler/Asm/Translation/FromTree.hs      |  1 +
 .../Compiler/Backend/C/Translation/FromReg.hs |  2 ++
 .../Backend/Cairo/Translation/FromCasm.hs     |  9 ++++++++
 .../Backend/Rust/Translation/FromReg.hs       |  2 ++
 src/Juvix/Compiler/Builtins/Assert.hs         | 22 +++++++++++++------
 src/Juvix/Compiler/Casm/Interpreter.hs        |  8 +++++++
 src/Juvix/Compiler/Casm/Keywords.hs           |  2 ++
 src/Juvix/Compiler/Casm/Language.hs           |  6 +++++
 src/Juvix/Compiler/Casm/Pretty/Base.hs        |  6 +++++
 .../Compiler/Casm/Translation/FromReg.hs      | 13 +++++++++++
 .../Compiler/Casm/Translation/FromSource.hs   |  7 ++++++
 src/Juvix/Compiler/Casm/Validate.hs           |  4 ++++
 src/Juvix/Compiler/Concrete/Data/Builtins.hs  |  4 +---
 src/Juvix/Compiler/Core/Evaluator.hs          | 16 ++++++++++++++
 src/Juvix/Compiler/Core/Keywords.hs           |  2 ++
 src/Juvix/Compiler/Core/Language/Builtins.hs  |  3 +++
 src/Juvix/Compiler/Core/Pretty/Base.hs        |  4 ++++
 .../Core/Transformation/ComputeTypeInfo.hs    |  3 +++
 .../Compiler/Core/Translation/FromInternal.hs |  5 +++++
 .../Compiler/Core/Translation/FromSource.hs   |  1 +
 .../Core/Translation/Stripped/FromCore.hs     |  2 +-
 .../Compiler/Nockma/Translation/FromTree.hs   |  5 +++++
 src/Juvix/Compiler/Reg/Extra/Base.hs          |  4 ++++
 src/Juvix/Compiler/Reg/Extra/Blocks.hs        |  4 ++++
 src/Juvix/Compiler/Reg/Extra/Info.hs          |  5 +++++
 src/Juvix/Compiler/Reg/Interpreter.hs         | 10 +++++++++
 src/Juvix/Compiler/Reg/Keywords.hs            |  2 ++
 src/Juvix/Compiler/Reg/Language.hs            |  3 ++-
 src/Juvix/Compiler/Reg/Language/Blocks.hs     |  1 +
 src/Juvix/Compiler/Reg/Language/Instrs.hs     |  6 +++++
 src/Juvix/Compiler/Reg/Pretty/Base.hs         |  6 +++++
 .../Reg/Translation/Blocks/FromReg.hs         |  1 +
 src/Juvix/Compiler/Reg/Translation/FromAsm.hs |  1 +
 .../Compiler/Reg/Translation/FromSource.hs    | 12 ++++++++++
 src/Juvix/Compiler/Tree/Evaluator.hs          |  6 +++++
 src/Juvix/Compiler/Tree/Keywords.hs           |  2 ++
 src/Juvix/Compiler/Tree/Language.hs           |  2 ++
 src/Juvix/Compiler/Tree/Pretty/Base.hs        |  1 +
 .../Compiler/Tree/Transformation/Validate.hs  |  1 +
 .../Compiler/Tree/Translation/FromAsm.hs      | 13 ++++++++---
 .../Compiler/Tree/Translation/FromCore.hs     | 10 +++++++++
 .../Compiler/Tree/Translation/FromSource.hs   |  1 +
 src/Juvix/Data/Keyword/All.hs                 |  3 +++
 src/Juvix/Extra/Strings.hs                    |  6 +++++
 50 files changed, 237 insertions(+), 20 deletions(-)

diff --git a/runtime/c/src/juvix/api.h b/runtime/c/src/juvix/api.h
index 07fa995336..940f0e82a0 100644
--- a/runtime/c/src/juvix/api.h
+++ b/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) \
diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
index f51515a925..6ef851bb38 100644
--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/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 ->
diff --git a/src/Juvix/Compiler/Asm/Interpreter.hs b/src/Juvix/Compiler/Asm/Interpreter.hs
index d445288a49..94686ab75d 100644
--- a/src/Juvix/Compiler/Asm/Interpreter.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Asm/Language.hs b/src/Juvix/Compiler/Asm/Language.hs
index a69f146c1c..63364f41fc 100644
--- a/src/Juvix/Compiler/Asm/Language.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Asm/Pretty/Base.hs b/src/Juvix/Compiler/Asm/Pretty/Base.hs
index b3fca036b6..0e630931c7 100644
--- a/src/Juvix/Compiler/Asm/Pretty/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Asm/Translation/FromSource.hs b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
index fa05a3d32c..17aae334b9 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromSource.hs
+++ b/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" ->
diff --git a/src/Juvix/Compiler/Asm/Translation/FromTree.hs b/src/Juvix/Compiler/Asm/Translation/FromTree.hs
index bbe1ab22fe..ea5f2d3b0d 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromTree.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
index 3b4424a6e6..6124aa9b4a 100644
--- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
+++ b/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 ->
diff --git a/src/Juvix/Compiler/Backend/Cairo/Translation/FromCasm.hs b/src/Juvix/Compiler/Backend/Cairo/Translation/FromCasm.hs
index d37f9f6325..9ba8104199 100644
--- a/src/Juvix/Compiler/Backend/Cairo/Translation/FromCasm.hs
+++ b/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 <> ")"))]
diff --git a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs
index a76a4c4f84..fd06b6affb 100644
--- a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs
+++ b/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 ->
diff --git a/src/Juvix/Compiler/Builtins/Assert.hs b/src/Juvix/Compiler/Builtins/Assert.hs
index 574491631f..de1570c47f 100644
--- a/src/Juvix/Compiler/Builtins/Assert.hs
+++ b/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 = []
+      }
diff --git a/src/Juvix/Compiler/Casm/Interpreter.hs b/src/Juvix/Compiler/Casm/Interpreter.hs
index 23fc58b2cb..02dbea97c5 100644
--- a/src/Juvix/Compiler/Casm/Interpreter.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Casm/Keywords.hs b/src/Juvix/Compiler/Casm/Keywords.hs
index 90352190fc..3bf2bbc812 100644
--- a/src/Juvix/Compiler/Casm/Keywords.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Casm/Language.hs b/src/Juvix/Compiler/Casm/Language.hs
index 6ac0404f04..6528927cc7 100644
--- a/src/Juvix/Compiler/Casm/Language.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Casm/Pretty/Base.hs b/src/Juvix/Compiler/Casm/Pretty/Base.hs
index 5a6cc8cf01..1645b7c95d 100644
--- a/src/Juvix/Compiler/Casm/Pretty/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs
index 90ea0f2b19..6cd31cb04d 100644
--- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Casm/Translation/FromSource.hs b/src/Juvix/Compiler/Casm/Translation/FromSource.hs
index a362d684c0..9568237d99 100644
--- a/src/Juvix/Compiler/Casm/Translation/FromSource.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Casm/Validate.hs b/src/Juvix/Compiler/Casm/Validate.hs
index 69f36dc8eb..43643356e1 100644
--- a/src/Juvix/Compiler/Casm/Validate.hs
+++ b/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 ()
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index abaf4f7c47..44fa3c32cd 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index cb79eb9b15..379410aa01 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs
index 3f5a522cdc..47683d3b3b 100644
--- a/src/Juvix/Compiler/Core/Keywords.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs
index c6c81a1bee..19d9f1a8a8 100644
--- a/src/Juvix/Compiler/Core/Language/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 8cb74a3aa4..f02d8e9283 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/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_
 
diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
index 812c60dcd6..c2be9aa0f2 100644
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/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"
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index b3578f015c..d5ea219095 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 3be6c2e31a..c3098036cd 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 3ce0bf2102..6982ee858d 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/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
@@ -54,7 +55,6 @@ fromCore fsize tab =
       BuiltinIntLt -> False
       BuiltinSeq -> False
       BuiltinMonadBind -> True -- TODO revise
-      BuiltinAssert -> True
       BuiltinFromNat -> True
       BuiltinFromInt -> True
 
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
index 08613b1619..2a752e58b8 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Reg/Extra/Base.hs b/src/Juvix/Compiler/Reg/Extra/Base.hs
index 34c590a0cc..ef485c27db 100644
--- a/src/Juvix/Compiler/Reg/Extra/Base.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Reg/Extra/Blocks.hs b/src/Juvix/Compiler/Reg/Extra/Blocks.hs
index b231a03303..dd3b010b82 100644
--- a/src/Juvix/Compiler/Reg/Extra/Blocks.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Reg/Extra/Info.hs b/src/Juvix/Compiler/Reg/Extra/Info.hs
index 7afa135f71..47113b5ede 100644
--- a/src/Juvix/Compiler/Reg/Extra/Info.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Reg/Interpreter.hs b/src/Juvix/Compiler/Reg/Interpreter.hs
index 682a0e8c66..0961c72f8b 100644
--- a/src/Juvix/Compiler/Reg/Interpreter.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Reg/Keywords.hs b/src/Juvix/Compiler/Reg/Keywords.hs
index 05fec6a66d..4fd7ae2bdb 100644
--- a/src/Juvix/Compiler/Reg/Keywords.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Reg/Language.hs b/src/Juvix/Compiler/Reg/Language.hs
index a13215578b..3244b6e131 100644
--- a/src/Juvix/Compiler/Reg/Language.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Reg/Language/Blocks.hs b/src/Juvix/Compiler/Reg/Language/Blocks.hs
index 3713e272cf..0ed1f9413a 100644
--- a/src/Juvix/Compiler/Reg/Language/Blocks.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Reg/Language/Instrs.hs b/src/Juvix/Compiler/Reg/Language/Instrs.hs
index 9b90493fd3..55da2a0387 100644
--- a/src/Juvix/Compiler/Reg/Language/Instrs.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Reg/Pretty/Base.hs b/src/Juvix/Compiler/Reg/Pretty/Base.hs
index fa11df91cc..67066ccd44 100644
--- a/src/Juvix/Compiler/Reg/Pretty/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Reg/Translation/Blocks/FromReg.hs b/src/Juvix/Compiler/Reg/Translation/Blocks/FromReg.hs
index 389126be35..5e4a380273 100644
--- a/src/Juvix/Compiler/Reg/Translation/Blocks/FromReg.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
index 571cdab915..8a10b8931e 100644
--- a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
+++ b/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))
diff --git a/src/Juvix/Compiler/Reg/Translation/FromSource.hs b/src/Juvix/Compiler/Reg/Translation/FromSource.hs
index 6314b26cfb..0432cbefa7 100644
--- a/src/Juvix/Compiler/Reg/Translation/FromSource.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Tree/Evaluator.hs b/src/Juvix/Compiler/Tree/Evaluator.hs
index 53f13f1f12..e8dc8797f0 100644
--- a/src/Juvix/Compiler/Tree/Evaluator.hs
+++ b/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)
 
diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs
index 989cdb9137..19b19e7611 100644
--- a/src/Juvix/Compiler/Tree/Keywords.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Tree/Language.hs b/src/Juvix/Compiler/Tree/Language.hs
index bbb9614910..deb476e696 100644
--- a/src/Juvix/Compiler/Tree/Language.hs
+++ b/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.
diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs
index 59433b8cdb..fa55322c84 100644
--- a/src/Juvix/Compiler/Tree/Pretty/Base.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Tree/Transformation/Validate.hs b/src/Juvix/Compiler/Tree/Transformation/Validate.hs
index c9ba84d41f..298e900d3a 100644
--- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Translation/FromAsm.hs b/src/Juvix/Compiler/Tree/Translation/FromAsm.hs
index 70f83829c8..0e01225130 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromAsm.hs
+++ b/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
-        goTrace = do
+        goSeqOp :: UnaryOpcode -> Sem r Node
+        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]
 
diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
index a5d578299a..a677ad506d 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs
+++ b/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] ->
diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
index 2a42f354d2..441b8df122 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs
+++ b/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)
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index 9f1d31e6de..71c54af014 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/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_
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 06725681ed..50e7387a74 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -485,6 +485,9 @@ sseq_ = "seq"
 eq :: (IsString s) => s
 eq = "eq"
 
+assert_ :: (IsString s) => s
+assert_ = "assert"
+
 trace_ :: (IsString s) => s
 trace_ = "trace"
 
@@ -848,6 +851,9 @@ instrPusht = "pusht"
 instrPopt :: (IsString s) => s
 instrPopt = "popt"
 
+instrAssert :: (IsString s) => s
+instrAssert = "assert"
+
 instrTrace :: (IsString s) => s
 instrTrace = "trace"