diff --git a/juvix-stdlib b/juvix-stdlib
index e2efe4e6f..b3768d265 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit e2efe4e6fe8e8bf1766050a7fa7ad8ff4e8c69fc
+Subproject commit b3768d2654e55fb7c8772592918b27e321a273b2
diff --git a/runtime/src/casm/stdlib.casm b/runtime/src/casm/stdlib.casm
index a6e46a45b..71d8f90bd 100644
--- a/runtime/src/casm/stdlib.casm
+++ b/runtime/src/casm/stdlib.casm
@@ -1,5 +1,8 @@
 -- Juvix runtime for Cairo assembly
 
+-- Make sure Juvix.Compiler.Casm.Extra.Stdlib is kept up to date with
+-- this file.
+
 -- Closure layout: [ fuid | 9 - sargs | 9 - argsnum | arguments... ]
 --  fuid -- function id which also indicates the relative jump
 --          offset for closure call (see juvix_call_closure below)
@@ -12,12 +15,45 @@
 -- [ap - 4] = fp
 -- [ap - 3] = pc
 -- [ap - 2] = ap - 2
+-- ap offset: 4
 juvix_get_regs:
   call juvix_get_ap_reg
   ret
 juvix_get_ap_reg:
   ret
 
+-- [fp - 3]: poseidon state ptr
+-- [fp - 4]: builtins ptr
+-- On return:
+-- [ap - 1]: new poseidon state ptr
+-- [ap - 2]: new builtins ptr
+-- Poseidon ap offset: 13 + 4 + 2
+juvix_poseidon:
+  -- [fp] = poseidon builtin ptr
+  [ap] = [[fp - 4] + 2]; ap++
+  -- transfer poseidon state to builtin memory
+  [ap] = [[fp - 3] + 1]; ap++
+  [ap - 1] = [[fp]]
+  [ap] = [[fp - 3] + 2]; ap++
+  [ap - 1] = [[fp] + 1]
+  [ap] = [[fp - 3] + 3]; ap++
+  [ap - 1] = [[fp] + 2]
+  call juvix_get_regs
+  -- alloc new poseidon state
+  [ap] = 1; ap++
+  [ap] = [[fp] + 3]; ap++
+  [ap] = [[fp] + 4]; ap++
+  [ap] = [[fp] + 5]; ap++
+  -- alloc new builtins
+  [ap] = [[fp - 4]]; ap++
+  [ap] = [[fp - 4] + 1]; ap++
+  [ap] = [fp] + 6; ap++
+  -- new builtins ptr
+  [ap] = [ap - 9] + 6; ap++
+  -- new poseidon state ptr
+  [ap] = [ap - 10] + 2; ap++
+  ret
+
 -- [fp - 3]: closure
 -- [fp - 4]: n = the number of arguments to extend with
 -- [fp - 4 - k]: argument n - k - 1 (reverse order!) (k is 0-based)
@@ -37,7 +73,7 @@ juvix_extend_closure:
   [ap] = [[fp - 3] + 4]; ap++
   [ap] = [[fp - 3] + 3]; ap++
   -- the following ensures continuous memory use
-  -- with a compile-time contant offset for local
+  -- with a compile-time constant offset for local
   -- variables
   [ap] = 10; ap++
   [ap] = [[fp - 3] + 1]; ap++
diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
index 0151dd492..20ddcb2eb 100644
--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
@@ -187,6 +187,8 @@ recurse' sig = go True
             checkUnop mkTypeInteger TyField
           OpFieldToInt ->
             checkUnop TyField mkTypeInteger
+          OpCairoPoseidon ->
+            checkUnop TyDynamic TyDynamic
           where
             checkUnop :: Type -> Type -> Sem r Memory
             checkUnop ty1 ty2 = do
diff --git a/src/Juvix/Compiler/Asm/Translation/FromSource.hs b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
index e513fa308..dd73028d1 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
@@ -99,6 +99,8 @@ command = do
       return $ mkInstr' loc Failure
     "argsnum" ->
       return $ mkUnop' loc OpArgsNum
+    "poseidon" ->
+      return $ mkUnop' loc OpCairoPoseidon
     "alloc" ->
       mkInstr' loc . AllocConstr <$> constrTag @Code @(Maybe FunctionInfoExtra) @DirectRef
     "calloc" ->
diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
index 145559d24..945885723 100644
--- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
+++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
@@ -301,6 +301,7 @@ fromRegInstr bNoStack info = \case
       Reg.OpArgsNum -> "JUVIX_ARGS_NUM"
       Reg.OpFieldToInt -> unsupported "field type"
       Reg.OpIntToField -> unsupported "field type"
+      Reg.OpCairoPoseidon -> unsupported "Cairo builtins"
 
     fromVarRef :: Reg.VarRef -> Expression
     fromVarRef Reg.VarRef {..} =
diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs
index afcc1f7ac..20c154d9e 100644
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/src/Juvix/Compiler/Builtins.hs
@@ -10,11 +10,13 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.Debug,
     module Juvix.Compiler.Builtins.Control,
     module Juvix.Compiler.Builtins.Anoma,
+    module Juvix.Compiler.Builtins.Cairo,
   )
 where
 
 import Juvix.Compiler.Builtins.Anoma
 import Juvix.Compiler.Builtins.Bool
+import Juvix.Compiler.Builtins.Cairo
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug
 import Juvix.Compiler.Builtins.Effect
diff --git a/src/Juvix/Compiler/Builtins/Cairo.hs b/src/Juvix/Compiler/Builtins/Cairo.hs
new file mode 100644
index 000000000..c962cd4fa
--- /dev/null
+++ b/src/Juvix/Compiler/Builtins/Cairo.hs
@@ -0,0 +1,32 @@
+module Juvix.Compiler.Builtins.Cairo where
+
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+registerPoseidonStateDef :: (Member Builtins r) => InductiveDef -> Sem r ()
+registerPoseidonStateDef d = do
+  unless (null (d ^. inductiveParameters)) (error "PoseidonState should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (error "PoseidonState should be in the small universe")
+  registerBuiltin BuiltinPoseidonState (d ^. inductiveName)
+  case d ^. inductiveConstructors of
+    [c] -> registerMkPoseidonState c
+    _ -> error "PoseidonState should have exactly one constructor"
+
+registerMkPoseidonState :: (Member Builtins r) => ConstructorDef -> Sem r ()
+registerMkPoseidonState d@ConstructorDef {..} = do
+  let mkps = _inductiveConstructorName
+      ty = _inductiveConstructorType
+  field_ <- getBuiltinName (getLoc d) BuiltinField
+  ps <- getBuiltinName (getLoc d) BuiltinPoseidonState
+  unless (ty === (field_ --> field_ --> field_ --> ps)) (error "mkPoseidonState has the wrong type")
+  registerBuiltin BuiltinMkPoseidonState mkps
+
+registerPoseidon :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerPoseidon f = do
+  let ftype = f ^. axiomType
+  ps <- getBuiltinName (getLoc f) BuiltinPoseidonState
+  unless
+    (ftype === (ps --> ps))
+    (error "poseidon must be of type PoseidonState -> PoseidonState")
+  registerBuiltin BuiltinPoseidon (f ^. axiomName)
diff --git a/src/Juvix/Compiler/Casm/Extra/Stdlib.hs b/src/Juvix/Compiler/Casm/Extra/Stdlib.hs
index c15593281..6ee90b525 100644
--- a/src/Juvix/Compiler/Casm/Extra/Stdlib.hs
+++ b/src/Juvix/Compiler/Casm/Extra/Stdlib.hs
@@ -10,9 +10,14 @@ data StdlibBuiltins = StdlibBuiltins
   { _stdlibGetRegs :: Symbol,
     _stdlibCallClosure :: Symbol,
     _stdlibExtendClosure :: Symbol,
+    _stdlibPoseidon :: Symbol,
     _stdlibGetRegsName :: Text,
     _stdlibCallClosureName :: Text,
-    _stdlibExtendClosureName :: Text
+    _stdlibExtendClosureName :: Text,
+    _stdlibPoseidonName :: Text,
+    -- The Ap offsets include the 2 cells for function call
+    _stdlibGetRegsApOffset :: Int,
+    _stdlibPoseidonApOffset :: Int
   }
 
 makeLenses ''StdlibBuiltins
@@ -26,7 +31,12 @@ addStdlibBuiltins addr = do
   let _stdlibGetRegsName :: Text = "juvix_get_regs"
       _stdlibCallClosureName :: Text = "juvix_call_closure"
       _stdlibExtendClosureName :: Text = "juvix_extend_closure"
+      _stdlibPoseidonName :: Text = "juvix_poseidon"
+      -- Make sure the Ap offsets correspond to the runtime
+      _stdlibGetRegsApOffset :: Int = 4
+      _stdlibPoseidonApOffset :: Int = 19
   _stdlibGetRegs <- fromJust <$> getIdent _stdlibGetRegsName
   _stdlibCallClosure <- fromJust <$> getIdent _stdlibCallClosureName
   _stdlibExtendClosure <- fromJust <$> getIdent _stdlibExtendClosureName
+  _stdlibPoseidon <- fromJust <$> getIdent _stdlibPoseidonName
   return (StdlibBuiltins {..}, instrs)
diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs
index cdfd321c0..e5060f6f4 100644
--- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs
+++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs
@@ -268,6 +268,8 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
         goAssignApBuiltins :: Sem r ()
         goAssignApBuiltins = mkBuiltinRef >>= goAssignAp . Val . Ref
 
+        -- Warning: the result may depend on Ap. Use adjust_ap when changing ap
+        -- afterwards.
         goValue :: Reg.Value -> Sem r Value
         goValue = \case
           Reg.ValConst c -> return $ Imm $ mkConst c
@@ -336,6 +338,16 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
           goAssignAp (Load $ LoadValue (adjustAp 1 v) casmClosureArgsNumOffset)
           goExtraBinop FieldSub res (MemRef Ap (-2)) (Ref $ MemRef Ap (-1))
 
+        goOpPoseidon :: Reg.VarRef -> Reg.Value -> Sem r ()
+        goOpPoseidon res v = do
+          goAssignApBuiltins
+          goAssignApValue v
+          output' (blts ^. stdlibPoseidonApOffset) $
+            mkCallRel (Lab (LabelRef (blts ^. stdlibPoseidon) (Just (blts ^. stdlibPoseidonName))))
+          off <- getAP
+          insertVar res (off - 1)
+          setBuiltinOffset (off - 2)
+
         goBinop' :: Reg.BinaryOp -> Reg.VarRef -> MemRef -> Value -> Sem r ()
         goBinop' op res arg1 arg2 = case op of
           Reg.OpIntAdd ->
@@ -392,19 +404,23 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
             v2 <- goValue _instrBinopArg2
             goBinop' _instrBinopOpcode _instrBinopResult ref v2
 
+        goUnop' :: (Reg.VarRef -> MemRef -> Sem r ()) -> Reg.VarRef -> Reg.Value -> Sem r ()
+        goUnop' f res val = do
+          v <- goValue val
+          case v of
+            Ref mr -> do
+              f res mr
+            Imm {} -> impossible
+            Lab {} -> impossible
+
         goUnop :: Reg.InstrUnop -> Sem r ()
         goUnop Reg.InstrUnop {..} = case _instrUnopOpcode of
           Reg.OpShow -> unsupported "strings"
           Reg.OpStrToInt -> unsupported "strings"
           Reg.OpFieldToInt -> goAssignValue _instrUnopResult _instrUnopArg
           Reg.OpIntToField -> goAssignValue _instrUnopResult _instrUnopArg
-          Reg.OpArgsNum -> do
-            v <- goValue _instrUnopArg
-            case v of
-              Ref mr -> do
-                goOpArgsNum _instrUnopResult mr
-              Imm {} -> impossible
-              Lab {} -> impossible
+          Reg.OpArgsNum -> goUnop' goOpArgsNum _instrUnopResult _instrUnopArg
+          Reg.OpCairoPoseidon -> goOpPoseidon _instrUnopResult _instrUnopArg
 
         goAssign :: Reg.InstrAssign -> Sem r ()
         goAssign Reg.InstrAssign {..} =
@@ -412,7 +428,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
 
         goAllocCall :: Reg.VarRef -> Sem r ()
         goAllocCall res = do
-          output' 4 $ mkCallRel $ Lab $ LabelRef (blts ^. stdlibGetRegs) (Just (blts ^. stdlibGetRegsName))
+          output' (blts ^. stdlibGetRegsApOffset) $ mkCallRel $ Lab $ LabelRef (blts ^. stdlibGetRegs) (Just (blts ^. stdlibGetRegsName))
           goNativeBinop FieldAdd res (MemRef Ap (-2)) (Imm 3)
 
         goAlloc :: Reg.InstrAlloc -> Sem r ()
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index b84e95ac9..8df343a17 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -44,12 +44,14 @@ builtinConstructors = \case
   BuiltinBool -> [BuiltinBoolTrue, BuiltinBoolFalse]
   BuiltinInt -> [BuiltinIntOfNat, BuiltinIntNegSuc]
   BuiltinList -> [BuiltinListNil, BuiltinListCons]
+  BuiltinPoseidonState -> [BuiltinMkPoseidonState]
 
 data BuiltinInductive
   = BuiltinNat
   | BuiltinBool
   | BuiltinInt
   | BuiltinList
+  | BuiltinPoseidonState
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinInductive
@@ -62,6 +64,7 @@ instance Pretty BuiltinInductive where
     BuiltinBool -> Str.bool_
     BuiltinInt -> Str.int_
     BuiltinList -> Str.list
+    BuiltinPoseidonState -> Str.cairoPoseidonState
 
 instance Pretty BuiltinConstructor where
   pretty = \case
@@ -73,6 +76,7 @@ instance Pretty BuiltinConstructor where
     BuiltinIntNegSuc -> Str.negSuc
     BuiltinListNil -> Str.nil
     BuiltinListCons -> Str.cons
+    BuiltinMkPoseidonState -> Str.cairoMkPoseidonState
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -83,6 +87,7 @@ data BuiltinConstructor
   | BuiltinIntNegSuc
   | BuiltinListNil
   | BuiltinListCons
+  | BuiltinMkPoseidonState
   deriving stock (Show, Eq, Ord, Generic, Data)
 
 instance Hashable BuiltinConstructor
@@ -178,6 +183,7 @@ data BuiltinAxiom
   | BuiltinIntToString
   | BuiltinIntPrint
   | BuiltinAnomaGet
+  | BuiltinPoseidon
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinAxiom
@@ -210,6 +216,7 @@ instance Pretty BuiltinAxiom where
     BuiltinIntToString -> Str.intToString
     BuiltinIntPrint -> Str.intPrint
     BuiltinAnomaGet -> Str.anomaGet
+    BuiltinPoseidon -> Str.cairoPoseidon
 
 data BuiltinType
   = BuiltinTypeInductive BuiltinInductive
diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
index fc2975043..aa9369591 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@@ -60,6 +60,9 @@ getNatSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinNat
 getIntSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
 getIntSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinInt
 
+getPoseidonStateSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getPoseidonStateSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinPoseidonState
+
 checkSymbolDefined :: (Member InfoTableBuilder r) => Symbol -> Sem r Bool
 checkSymbolDefined sym = do
   m <- getModule
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 30082de5e..54163c643 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -187,7 +187,8 @@ geval opts herr ctx env0 = eval' env0
       OpSeq -> seqOp
       OpFail -> failOp
       OpTrace -> traceOp
-      OpAnomaGet -> err "unsupported op: OpAnomaGet"
+      OpAnomaGet -> err "unsupported builtin operation: OpAnomaGet"
+      OpPoseidonHash -> err "unsupported builtin operation: OpPoseidonHash"
       where
         err :: Text -> a
         err msg = evalError msg n
diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
index d89d747bb..120b5e44e 100644
--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/src/Juvix/Compiler/Core/Extra/Utils.hs
@@ -424,6 +424,7 @@ builtinOpArgTypes = \case
   OpTrace -> [mkDynamic']
   OpFail -> [mkTypeString']
   OpAnomaGet -> [mkDynamic']
+  OpPoseidonHash -> [mkDynamic']
 
 translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a
 translateCase translateIfFun dflt Case {..} = case _caseBranches of
diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs
index f4a955661..091f16fa2 100644
--- a/src/Juvix/Compiler/Core/Language/Builtins.hs
+++ b/src/Juvix/Compiler/Core/Language/Builtins.hs
@@ -27,6 +27,7 @@ data BuiltinOp
   | OpTrace
   | OpFail
   | OpAnomaGet
+  | OpPoseidonHash
   deriving stock (Eq, Generic)
 
 instance Serialize BuiltinOp
@@ -68,6 +69,7 @@ builtinOpArgsNum = \case
   OpTrace -> 1
   OpFail -> 1
   OpAnomaGet -> 1
+  OpPoseidonHash -> 1
 
 builtinConstrArgsNum :: BuiltinDataTag -> Int
 builtinConstrArgsNum = \case
@@ -77,3 +79,29 @@ builtinConstrArgsNum = \case
   TagBind -> 2
   TagWrite -> 1
   TagReadLn -> 0
+
+-- | True if the builtin can be evaluated away during constant folding
+builtinIsFoldable :: BuiltinOp -> Bool
+builtinIsFoldable = \case
+  OpIntAdd -> True
+  OpIntSub -> True
+  OpIntMul -> True
+  OpIntDiv -> True
+  OpIntMod -> True
+  OpIntLt -> True
+  OpIntLe -> True
+  OpFieldAdd -> True
+  OpFieldSub -> True
+  OpFieldMul -> True
+  OpFieldDiv -> True
+  OpFieldFromInt -> True
+  OpFieldToInt -> True
+  OpEq -> True
+  OpShow -> True
+  OpStrConcat -> True
+  OpStrToInt -> True
+  OpSeq -> False
+  OpTrace -> False
+  OpFail -> False
+  OpAnomaGet -> False
+  OpPoseidonHash -> False
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 62a1caae9..60bd0ed6d 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -53,6 +53,7 @@ instance PrettyCode BuiltinOp where
     OpTrace -> return primTrace
     OpFail -> return primFail
     OpAnomaGet -> return primAnomaGet
+    OpPoseidonHash -> return primPoseidonHash
 
 instance PrettyCode BuiltinDataTag where
   ppCode = \case
@@ -798,6 +799,9 @@ primFail = primitive Str.fail_
 primAnomaGet :: Doc Ann
 primAnomaGet = primitive Str.anomaGet
 
+primPoseidonHash :: Doc Ann
+primPoseidonHash = primitive Str.cairoPoseidon
+
 primTrace :: Doc Ann
 primTrace = primitive Str.trace_
 
diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
index ffb64429b..ef0b4db16 100644
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
@@ -67,6 +67,9 @@ computeNodeTypeInfo md = umapL go
             _ -> error "incorrect trace builtin application"
           OpFail -> Info.getNodeType node
           OpAnomaGet -> Info.getNodeType node
+          OpPoseidonHash -> case _builtinAppArgs of
+            [arg] -> Info.getNodeType arg
+            _ -> error "incorrect poseidon builtin application"
       NCtr Constr {..} ->
         let ci = lookupConstructorInfo md _constrTag
             ii = lookupInductiveInfo md (ci ^. constructorInductive)
diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs
index fc86c5804..41896cd50 100644
--- a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs
@@ -15,9 +15,7 @@ convertNode opts nonRecSyms tab md = umap go
     go node = case node of
       NBlt BuiltinApp {..}
         | Info.isClosed node
-            && _builtinAppOp /= OpFail
-            && _builtinAppOp /= OpTrace
-            && _builtinAppOp /= OpSeq
+            && builtinIsFoldable _builtinAppOp
             && all isNonRecValue _builtinAppArgs ->
             doEval' node
       NApp {}
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index 7aa39821d..1cff14a48 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -209,6 +209,7 @@ goConstructor sym ctor = do
       Just Internal.BuiltinIntNegSuc -> freshTag
       Just Internal.BuiltinListNil -> freshTag
       Just Internal.BuiltinListCons -> freshTag
+      Just Internal.BuiltinMkPoseidonState -> freshTag
       Nothing -> freshTag
 
     ctorType :: Sem r Type
@@ -578,6 +579,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinFieldFromInt -> return ()
       Internal.BuiltinFieldToNat -> return ()
       Internal.BuiltinAnomaGet -> return ()
+      Internal.BuiltinPoseidon -> return ()
 
     registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
     registerInductiveAxiom ax ctrs = do
@@ -695,6 +697,11 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaGet [mkVar' 0]))
               )
           )
+      Internal.BuiltinPoseidon -> do
+        psName <- getPoseidonStateName
+        psSym <- getPoseidonStateSymbol
+        let ty = mkTypeConstr (setInfoName psName mempty) psSym []
+        registerAxiomDef (mkLambda' ty (mkBuiltinApp' OpPoseidonHash [mkVar' 0]))
 
     axiomType' :: Sem r Type
     axiomType' = fromTopIndex (goType (a ^. Internal.axiomType))
@@ -708,6 +715,9 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
     getIntName :: Sem r Text
     getIntName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinInt
 
+    getPoseidonStateName :: Sem r Text
+    getPoseidonStateName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinPoseidonState
+
     registerAxiomDef :: Node -> Sem r ()
     registerAxiomDef body = do
       let name = a ^. Internal.axiomName
@@ -1071,6 +1081,7 @@ goApplication a = do
             _ -> app
         Just Internal.BuiltinFieldToNat -> app
         Just Internal.BuiltinAnomaGet -> app
+        Just Internal.BuiltinPoseidon -> app
         Nothing -> app
     Internal.ExpressionIden (Internal.IdenFunction n) -> do
       funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index ecccaa562..72f61e966 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -60,6 +60,7 @@ fromCore fsize tab =
     shouldKeepConstructor = \case
       BuiltinListNil -> True
       BuiltinListCons -> True
+      BuiltinMkPoseidonState -> True
       BuiltinNatZero -> False
       BuiltinNatSuc -> False
       BuiltinBoolTrue -> False
@@ -94,8 +95,10 @@ fromCore fsize tab =
         BuiltinIntToString -> False
         BuiltinIntPrint -> False
         BuiltinAnomaGet -> False
+        BuiltinPoseidon -> False
       BuiltinTypeInductive i -> case i of
         BuiltinList -> True
+        BuiltinPoseidonState -> True
         BuiltinNat -> False
         BuiltinInt -> False
         BuiltinBool -> False
diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
index c1b2b5c35..00b6be91b 100644
--- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
+++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
@@ -194,6 +194,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
         modify (set builderStateInt (Just (i ^. inductiveName)))
         addInductiveStartNode
       BuiltinList -> return ()
+      BuiltinPoseidonState -> return ()
 
     addInductiveStartNode :: Sem r ()
     addInductiveStartNode = addStartNode (i ^. inductiveName)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 7feebb8a9..f91137ad9 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -523,6 +523,7 @@ registerBuiltinInductive d = \case
   BuiltinBool -> registerBoolDef d
   BuiltinInt -> registerIntDef d
   BuiltinList -> registerListDef d
+  BuiltinPoseidonState -> registerPoseidonStateDef d
 
 registerBuiltinFunction ::
   (Members '[Error ScoperError, Builtins, NameIdGen] r) =>
@@ -588,6 +589,7 @@ registerBuiltinAxiom d = \case
   BuiltinIntToString -> registerIntToString d
   BuiltinIntPrint -> registerIntPrint d
   BuiltinAnomaGet -> registerAnomaGet d
+  BuiltinPoseidon -> registerPoseidon d
 
 goInductive ::
   (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Reader Pragmas, Builtins, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) =>
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
index 5e4ad70f7..759ee0b94 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
@@ -435,6 +435,7 @@ compile = \case
          in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum)
       Tree.OpIntToField -> fieldErr
       Tree.OpFieldToInt -> fieldErr
+      Tree.OpCairoPoseidon -> cairoErr
 
     goAnomaGet :: Term Natural -> Sem r (Term Natural)
     goAnomaGet key = do
@@ -691,6 +692,9 @@ stringsErr = unsupported "strings"
 fieldErr :: a
 fieldErr = unsupported "the field type"
 
+cairoErr :: a
+cairoErr = unsupported "cairo builtins"
+
 -- | Computes a - b
 sub :: Term Natural -> Term Natural -> Term Natural
 sub a b = callStdlib StdlibSub [a, b]
diff --git a/src/Juvix/Compiler/Reg/Keywords.hs b/src/Juvix/Compiler/Reg/Keywords.hs
index 0f2310127..5f22f8e85 100644
--- a/src/Juvix/Compiler/Reg/Keywords.hs
+++ b/src/Juvix/Compiler/Reg/Keywords.hs
@@ -36,6 +36,7 @@ import Juvix.Data.Keyword.All
     kwMod_,
     kwMul_,
     kwNop,
+    kwPoseidon,
     kwPrealloc,
     kwRet,
     kwShow,
@@ -83,5 +84,6 @@ allKeywords =
          kwBr,
          kwCase,
          kwFail,
-         kwArgsNum
+         kwArgsNum,
+         kwPoseidon
        ]
diff --git a/src/Juvix/Compiler/Reg/Translation/FromSource.hs b/src/Juvix/Compiler/Reg/Translation/FromSource.hs
index 6d2c60a92..b793411ec 100644
--- a/src/Juvix/Compiler/Reg/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Reg/Translation/FromSource.hs
@@ -128,6 +128,7 @@ instrUnop vref =
   parseUnaryOp kwShow OpShow vref
     <|> parseUnaryOp kwAtoi OpStrToInt vref
     <|> parseUnaryOp kwArgsNum OpArgsNum vref
+    <|> parseUnaryOp kwPoseidon OpCairoPoseidon vref
 
 parseUnaryOp ::
   (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) =>
diff --git a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs
index 6c73426c6..4d7a74977 100644
--- a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs
+++ b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs
@@ -63,6 +63,7 @@ evalUnop tab op v = case op of
   OpFieldToInt -> goFieldToInt v
   OpIntToField -> goIntToField v
   OpArgsNum -> goArgsNum v
+  OpCairoPoseidon -> Left "unsupported: Poseidon hash"
   where
     strToInt :: Text -> Either ErrorMsg Value
     strToInt s = case T.readMaybe (fromText s) of
diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs
index 900df036b..83d3ff7b3 100644
--- a/src/Juvix/Compiler/Tree/Keywords.hs
+++ b/src/Juvix/Compiler/Tree/Keywords.hs
@@ -29,6 +29,7 @@ import Juvix.Data.Keyword.All
     kwLt_,
     kwMod_,
     kwMul_,
+    kwPoseidon,
     kwSave,
     kwSeq_,
     kwShow,
@@ -70,5 +71,6 @@ allKeywords =
          kwBr,
          kwCase,
          kwSave,
-         kwAnomaGet
+         kwAnomaGet,
+         kwPoseidon
        ]
diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs
index 54f84f276..4bf1a242d 100644
--- a/src/Juvix/Compiler/Tree/Language/Builtins.hs
+++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs
@@ -30,4 +30,6 @@ data UnaryOp
   | -- | Compute the number of expected arguments for the given closure. JV*
     -- opcode: `argsnum`.
     OpArgsNum
+  | -- | Cairo Poseidon hash builtin. Implemented only in the Cairo backend.
+    OpCairoPoseidon
   deriving stock (Eq)
diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs
index 9e143f619..e8fe36186 100644
--- a/src/Juvix/Compiler/Tree/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs
@@ -233,6 +233,7 @@ instance PrettyCode UnaryOp where
     OpFieldToInt -> Str.instrFieldToInt
     OpIntToField -> Str.instrIntToField
     OpArgsNum -> Str.instrArgsNum
+    OpCairoPoseidon -> Str.instrPoseidon
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case
diff --git a/src/Juvix/Compiler/Tree/Transformation/Validate.hs b/src/Juvix/Compiler/Tree/Transformation/Validate.hs
index ca95afe38..a9648a5db 100644
--- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs
+++ b/src/Juvix/Compiler/Tree/Transformation/Validate.hs
@@ -81,6 +81,7 @@ inferType tab funInfo = goInfer mempty
           OpArgsNum -> checkUnop TyDynamic mkTypeInteger
           OpIntToField -> checkUnop mkTypeInteger TyField
           OpFieldToInt -> checkUnop TyField mkTypeInteger
+          OpCairoPoseidon -> checkUnop TyDynamic TyDynamic
 
     goConst :: BinderList Type -> NodeConstant -> Sem r Type
     goConst _ NodeConstant {..} = case _nodeConstant of
diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
index 220f1f7ff..5576b39a7 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
@@ -289,6 +289,7 @@ genCode infoTable fi =
       Core.OpTrace -> OpTrace
       Core.OpFail -> OpFail
       Core.OpAnomaGet -> OpAnomaGet
+      Core.OpPoseidonHash -> PrimUnop OpCairoPoseidon
       _ -> impossible
 
     getArgsNum :: Symbol -> Int
diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
index 199e6f57b..7ddab6535 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
@@ -106,6 +106,7 @@ parseUnop =
     <|> parseUnaryOp kwTrace OpTrace
     <|> parseUnaryOp kwFail OpFail
     <|> parseUnaryOp kwArgsNum (PrimUnop OpArgsNum)
+    <|> parseUnaryOp kwPoseidon (PrimUnop OpCairoPoseidon)
     <|> parseUnaryOp kwAnomaGet (OpAnomaGet)
 
 parseUnaryOp ::
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index 9e7a7b7fd..56b786630 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@@ -277,6 +277,9 @@ kwPrealloc = asciiKw Str.prealloc
 kwArgsNum :: Keyword
 kwArgsNum = asciiKw Str.instrArgsNum
 
+kwPoseidon :: Keyword
+kwPoseidon = asciiKw Str.instrPoseidon
+
 kwAlloc :: Keyword
 kwAlloc = asciiKw Str.instrAlloc
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index dc76c4f90..b849544d6 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -755,6 +755,9 @@ instrFailure = "fail"
 instrArgsNum :: (IsString s) => s
 instrArgsNum = "argsnum"
 
+instrPoseidon :: (IsString s) => s
+instrPoseidon = "poseidon"
+
 instrPrealloc :: (IsString s) => s
 instrPrealloc = "prealloc"
 
@@ -1000,3 +1003,9 @@ cairoPoseidon = "poseidon"
 
 cairoEcOp :: (IsString s) => s
 cairoEcOp = "ec_op"
+
+cairoPoseidonState :: (IsString s) => s
+cairoPoseidonState = "poseidon_state"
+
+cairoMkPoseidonState :: (IsString s) => s
+cairoMkPoseidonState = "mkPoseidonState"
diff --git a/test/Casm/Compilation/Base.hs b/test/Casm/Compilation/Base.hs
index 6fc13a684..04dbbc328 100644
--- a/test/Casm/Compilation/Base.hs
+++ b/test/Casm/Compilation/Base.hs
@@ -11,6 +11,7 @@ import Juvix.Data.PPOutput
 compileAssertion ::
   Path Abs Dir ->
   Bool ->
+  Bool ->
   Int ->
   Path Abs File ->
   Path Abs File ->
@@ -22,12 +23,13 @@ compileAssertionEntry ::
   (EntryPoint -> EntryPoint) ->
   Path Abs Dir ->
   Bool ->
+  Bool ->
   Int ->
   Path Abs File ->
   Path Abs File ->
   (String -> IO ()) ->
   Assertion
-compileAssertionEntry adjustEntry root' bRunVM optLevel mainFile expectedFile step = do
+compileAssertionEntry adjustEntry root' bInterp bRunVM optLevel mainFile expectedFile step = do
   step "Translate to JuvixCore"
   entryPoint <- adjustEntry <$> testDefaultEntryPointIO root' mainFile
   PipelineResult {..} <- snd <$> testRunIO entryPoint upToStoredCore
@@ -42,4 +44,4 @@ compileAssertionEntry adjustEntry root' bRunVM optLevel mainFile expectedFile st
             step "Pretty print"
             writeFileEnsureLn tmpFile (toPlainText $ ppProgram _resultCode)
         )
-      casmRunAssertion' bRunVM _resultLabelInfo _resultCode _resultBuiltins Nothing expectedFile step
+      casmRunAssertion' bInterp bRunVM _resultLabelInfo _resultCode _resultBuiltins Nothing expectedFile step
diff --git a/test/Casm/Compilation/Positive.hs b/test/Casm/Compilation/Positive.hs
index 34e131542..7fcfada82 100644
--- a/test/Casm/Compilation/Positive.hs
+++ b/test/Casm/Compilation/Positive.hs
@@ -5,7 +5,8 @@ import Casm.Compilation.Base
 import Data.HashSet qualified as HashSet
 
 data PosTest = PosTest
-  { _runVM :: Bool,
+  { _interp :: Bool,
+    _runVM :: Bool,
     _name :: String,
     _dir :: Path Abs Dir,
     _file :: Path Abs File,
@@ -25,7 +26,7 @@ toTestDescr optLevel PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ compileAssertion _dir _runVM optLevel file' expected'
+          _testAssertion = Steps $ compileAssertion _dir _interp _runVM optLevel file' expected'
         }
 
 allTests :: TestTree
@@ -40,8 +41,8 @@ allTestsNoOptimize =
     "Juvix to CASM positive tests (no optimization)"
     (map (mkTest . toTestDescr 0) tests)
 
-posTest :: String -> Bool -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
-posTest _name _runVM rdir rfile routfile =
+posTest :: String -> Bool -> Bool -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
+posTest _name _interp _runVM rdir rfile routfile =
   let _dir = root <//> rdir
       _file = _dir <//> rfile
       _expectedFile = root <//> routfile
@@ -64,17 +65,20 @@ tests =
     [ posTest
         "Test001: Arithmetic operators"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test001.juvix")
         $(mkRelFile "out/test001.out"),
       posTest
         "Test002: Arithmetic operators inside lambdas"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test002.juvix")
         $(mkRelFile "out/test002.out"),
       posTest
         "Test003: Integer arithmetic"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test003.juvix")
@@ -82,11 +86,13 @@ tests =
       posTest
         "Test005: Higher-order functions"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test005.juvix")
         $(mkRelFile "out/test005.out"),
       posTest
         "Test006: If-then-else and lazy boolean operators"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test006.juvix")
@@ -94,41 +100,48 @@ tests =
       posTest
         "Test007: Pattern matching and lambda-case"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test007.juvix")
         $(mkRelFile "out/test007.out"),
       posTest
         "Test008: Recursion"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test008.juvix")
         $(mkRelFile "out/test008.out"),
       posTest
         "Test009: Tail recursion"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test009.juvix")
         $(mkRelFile "out/test009.out"),
       posTest
         "Test010: Let"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test010.juvix")
         $(mkRelFile "out/test010.out"),
       posTest
         "Test013: Functions returning functions with variable capture"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test013.juvix")
         $(mkRelFile "out/test013.out"),
       posTest
         "Test014: Arithmetic"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test014.juvix")
         $(mkRelFile "out/test014.out"),
       posTest
         "Test015: Local functions with free variables"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test015.juvix")
@@ -136,35 +149,41 @@ tests =
       posTest
         "Test016: Recursion through higher-order functions"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test016.juvix")
         $(mkRelFile "out/test016.out"),
       posTest
         "Test017: Tail recursion through higher-order functions"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test017.juvix")
         $(mkRelFile "out/test017.out"),
       posTest
         "Test018: Higher-order functions and recursion"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test018.juvix")
         $(mkRelFile "out/test018.out"),
       posTest
         "Test019: Self-application"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test019.juvix")
         $(mkRelFile "out/test019.out"),
       posTest
         "Test020: Recursive functions: McCarthy's 91 function, subtraction by increments"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test020.juvix")
         $(mkRelFile "out/test020.out"),
       posTest
         "Test021: Fast exponentiation"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test021.juvix")
@@ -172,11 +191,13 @@ tests =
       posTest
         "Test022: Lists"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test022.juvix")
         $(mkRelFile "out/test022.out"),
       posTest
         "Test023: Mutual recursion"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test023.juvix")
@@ -184,11 +205,13 @@ tests =
       posTest
         "Test024: Nested binders with variable capture"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test024.juvix")
         $(mkRelFile "out/test024.out"),
       posTest
         "Test025: Euclid's algorithm"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test025.juvix")
@@ -196,11 +219,13 @@ tests =
       posTest
         "Test026: Functional queues"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test026.juvix")
         $(mkRelFile "out/test026.out"),
       posTest
         "Test028: Streams without memoization"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test028.juvix")
@@ -208,41 +233,48 @@ tests =
       posTest
         "Test029: Ackermann function"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test029.juvix")
         $(mkRelFile "out/test029.out"),
       posTest
         "Test030: Ackermann function (higher-order definition)"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test030.juvix")
         $(mkRelFile "out/test030.out"),
       posTest
         "Test032: Merge sort"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test032.juvix")
         $(mkRelFile "out/test032.out"),
       posTest
         "Test033: Eta-expansion of builtins and constructors"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test033.juvix")
         $(mkRelFile "out/test033.out"),
       posTest
         "Test034: Recursive let"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test034.juvix")
         $(mkRelFile "out/test034.out"),
       posTest
         "Test035: Pattern matching"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test035.juvix")
         $(mkRelFile "out/test035.out"),
       posTest
         "Test036: Eta-expansion"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test036.juvix")
@@ -250,47 +282,55 @@ tests =
       posTest
         "Test037: Applications with lets and cases in function position"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test037.juvix")
         $(mkRelFile "out/test037.out"),
       posTest
         "Test038: Simple case expression"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test038.juvix")
         $(mkRelFile "out/test038.out"),
       posTest
         "Test039: Mutually recursive let expression"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test039.juvix")
         $(mkRelFile "out/test039.out"),
       posTest
         "Test040: Pattern matching nullary constructor"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test040.juvix")
         $(mkRelFile "out/test040.out"),
       posTest
         "Test045: Implicit builtin bool"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test045.juvix")
         $(mkRelFile "out/test045.out"),
       posTest
         "Test046: Polymorphic type arguments"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test046.juvix")
         $(mkRelFile "out/test046.out"),
       posTest
         "Test047: Local Modules"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test047.juvix")
         $(mkRelFile "out/test047.out"),
       posTest
         "Test050: Pattern matching with integers"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test050.juvix")
@@ -298,29 +338,34 @@ tests =
       posTest
         "Test053: Inlining"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test053.juvix")
         $(mkRelFile "out/test053.out"),
       posTest
         "Test054: Iterators"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test054.juvix")
         $(mkRelFile "out/test054.out"),
       posTest
         "Test056: Argument specialization"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test056.juvix")
         $(mkRelFile "out/test056.out"),
       posTest
         "Test057: Case folding"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test057.juvix")
         $(mkRelFile "out/test057.out"),
       posTest
         "Test058: Ranges"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test058.juvix")
@@ -328,53 +373,62 @@ tests =
       posTest
         "Test059: Builtin list"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test059.juvix")
         $(mkRelFile "out/test059.out"),
       posTest
         "Test060: Record update"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test060.juvix")
         $(mkRelFile "out/test060.out"),
       posTest
         "Test062: Overapplication"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test062.juvix")
         $(mkRelFile "out/test062.out"),
       posTest
         "Test064: Constant folding"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test064.juvix")
         $(mkRelFile "out/test064.out"),
       posTest
         "Test065: Arithmetic simplification"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test065.juvix")
         $(mkRelFile "out/test065.out"),
       posTest
         "Test066: Import function with a function call in default argument"
         True
+        True
         $(mkRelDir "test066")
         $(mkRelFile "M.juvix")
         $(mkRelFile "out/test066.out"),
       posTest
         "Test067: Dependent default values inserted during translation FromConcrete"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test067.juvix")
         $(mkRelFile "out/test067.out"),
       posTest
         "Test068: Dependent default values inserted in the arity checker"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test068.juvix")
         $(mkRelFile "out/test068.out"),
       posTest
         "Test069: Dependent default values for Ord trait"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test069.juvix")
@@ -382,11 +436,13 @@ tests =
       posTest
         "Test070: Nested default values and named arguments"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test070.juvix")
         $(mkRelFile "out/test070.out"),
       posTest
         "Test071: Named application (Ord instance with default cmp)"
+        True
         False
         $(mkRelDir ".")
         $(mkRelFile "test071.juvix")
@@ -394,19 +450,29 @@ tests =
       posTest
         "Test072: Monad transformers (ReaderT + StateT + Identity)"
         True
+        True
         $(mkRelDir "test072")
         $(mkRelFile "ReaderT.juvix")
         $(mkRelFile "out/test072.out"),
       posTest
         "Test073: Import and use a syntax alias"
         True
+        True
         $(mkRelDir "test073")
         $(mkRelFile "test073.juvix")
         $(mkRelFile "out/test073.out"),
       posTest
         "Test074: Fields"
         True
+        True
         $(mkRelDir ".")
         $(mkRelFile "test074.juvix")
-        $(mkRelFile "out/test074.out")
+        $(mkRelFile "out/test074.out"),
+      posTest
+        "Test075: Poseidon hash"
+        False
+        True
+        $(mkRelDir ".")
+        $(mkRelFile "test075.juvix")
+        $(mkRelFile "out/test075.out")
     ]
diff --git a/test/Casm/Reg/Cairo.hs b/test/Casm/Reg/Cairo.hs
index 31e363933..e9e4ce51a 100644
--- a/test/Casm/Reg/Cairo.hs
+++ b/test/Casm/Reg/Cairo.hs
@@ -35,4 +35,15 @@ allTests =
             "Test036: Streams without memoization"
           ]
           P.tests
+          ++ cairoTests
     )
+
+cairoTests :: [P.PosTest]
+cairoTests =
+  [ P.PosTest
+      "Test041: Poseidon hash"
+      $(mkRelDir ".")
+      $(mkRelFile "test041.jvr")
+      $(mkRelFile "out/test041.out")
+      Nothing
+  ]
diff --git a/test/Casm/Run/Base.hs b/test/Casm/Run/Base.hs
index 16f76ed10..fa56192b1 100644
--- a/test/Casm/Run/Base.hs
+++ b/test/Casm/Run/Base.hs
@@ -36,40 +36,45 @@ casmRunVM labi instrs blts inputFile expectedFile step = do
         assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
     )
 
-casmRunAssertion' :: Bool -> LabelInfo -> Code -> [Builtin] -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
-casmRunAssertion' bRunVM labi instrs blts inputFile expectedFile step =
+casmInterpret :: LabelInfo -> Code -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
+casmInterpret labi instrs inputFile expectedFile step =
+  withTempDir'
+    ( \dirPath -> do
+        let outputFile = dirPath <//> $(mkRelFile "out.out")
+        step "Interpret"
+        hout <- openFile (toFilePath outputFile) WriteMode
+        r' <- doRun hout labi instrs inputFile
+        case r' of
+          Left err -> do
+            hClose hout
+            assertFailure (prettyString err)
+          Right value' -> do
+            hPrint hout value'
+            hClose hout
+            actualOutput <- readFile outputFile
+            step "Compare expected and actual program output"
+            expected <- readFile expectedFile
+            assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
+    )
+
+casmRunAssertion' :: Bool -> Bool -> LabelInfo -> Code -> [Builtin] -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
+casmRunAssertion' bInterp bRunVM labi instrs blts inputFile expectedFile step =
   case validate labi instrs of
     Left err -> do
       assertFailure (prettyString err)
     Right () -> do
-      withTempDir'
-        ( \dirPath -> do
-            let outputFile = dirPath <//> $(mkRelFile "out.out")
-            step "Interpret"
-            hout <- openFile (toFilePath outputFile) WriteMode
-            r' <- doRun hout labi instrs inputFile
-            case r' of
-              Left err -> do
-                hClose hout
-                assertFailure (prettyString err)
-              Right value' -> do
-                hPrint hout value'
-                hClose hout
-                actualOutput <- readFile outputFile
-                step "Compare expected and actual program output"
-                expected <- readFile expectedFile
-                assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
-        )
+      when bInterp $
+        casmInterpret labi instrs inputFile expectedFile step
       when bRunVM $
         casmRunVM labi instrs blts inputFile expectedFile step
 
-casmRunAssertion :: Bool -> Path Abs File -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
-casmRunAssertion bRunVM mainFile inputFile expectedFile step = do
+casmRunAssertion :: Bool -> Bool -> Path Abs File -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion
+casmRunAssertion bInterp bRunVM mainFile inputFile expectedFile step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
     Left err -> assertFailure (prettyString err)
-    Right (labi, instrs) -> casmRunAssertion' bRunVM labi instrs [] inputFile expectedFile step
+    Right (labi, instrs) -> casmRunAssertion' bInterp bRunVM labi instrs [] inputFile expectedFile step
 
 casmRunErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
 casmRunErrorAssertion mainFile step = do
diff --git a/test/Casm/Run/Positive.hs b/test/Casm/Run/Positive.hs
index 70ced320a..9cdcae7b4 100644
--- a/test/Casm/Run/Positive.hs
+++ b/test/Casm/Run/Positive.hs
@@ -24,7 +24,7 @@ testDescr PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ casmRunAssertion _runVM file' input' expected'
+          _testAssertion = Steps $ casmRunAssertion True _runVM file' input' expected'
         }
 
 filterTests :: [String] -> [PosTest] -> [PosTest]
diff --git a/tests/Casm/Cairo/reference/README.md b/tests/Casm/Cairo/reference/README.md
new file mode 100644
index 000000000..e4f9ccdad
--- /dev/null
+++ b/tests/Casm/Cairo/reference/README.md
@@ -0,0 +1,13 @@
+This directory contains reference Cairo0 programs used to obtain the
+output values for corresponding Juvix programs.
+
+The programs should be compiled with
+```
+cairo-compile --proof_mode program.cairo > program.json
+```
+where `cairo-compile` is the Cairo0 compiler (the Python version).
+
+Then run with:
+```
+run_cairo_vm.sh program.json
+```
diff --git a/tests/Casm/Cairo/reference/poseidon.cairo b/tests/Casm/Cairo/reference/poseidon.cairo
new file mode 100644
index 000000000..37c81a92e
--- /dev/null
+++ b/tests/Casm/Cairo/reference/poseidon.cairo
@@ -0,0 +1,71 @@
+%builtins output poseidon
+
+from starkware.cairo.common.cairo_builtins import PoseidonBuiltin
+from starkware.cairo.common.poseidon_state import PoseidonBuiltinState
+
+// Hashes two elements and retrieves a single field element output.
+func poseidon_hash{poseidon_ptr: PoseidonBuiltin*}(x: felt, y: felt) -> (res: felt) {
+    // To distinguish between the use cases the capacity element is initialized to 2.
+    assert poseidon_ptr.input = PoseidonBuiltinState(s0=x, s1=y, s2=2);
+
+    let res = poseidon_ptr.output.s0;
+    let poseidon_ptr = poseidon_ptr + PoseidonBuiltin.SIZE;
+
+    return (res=res);
+}
+
+// Hashes n elements and retrieves a single field element output.
+func poseidon_hash_many{poseidon_ptr: PoseidonBuiltin*}(n: felt, elements: felt*) -> (res: felt) {
+    let elements_end = &elements[n];
+    // Apply the sponge construction to digest many elements.
+    // To distinguish between the use cases the capacity element is initialized to 0.
+    // To distinguish between different input sizes always pad with 1 and possibly with another 0 to
+    // complete to an even sized input.
+    tempvar state = PoseidonBuiltinState(s0=0, s1=0, s2=0);
+    tempvar elements = elements;
+    tempvar poseidon_ptr = poseidon_ptr;
+
+        assert poseidon_ptr.input = PoseidonBuiltinState(
+            s0=state.s0 + elements[0], s1=state.s1 + elements[1], s2=state.s2
+        );
+        let state = poseidon_ptr.output;
+        let poseidon_ptr = poseidon_ptr + PoseidonBuiltin.SIZE;
+
+
+
+        tempvar state = state;
+        tempvar elements = &elements[2];
+        tempvar poseidon_ptr = poseidon_ptr;
+        tempvar n = elements_end - elements;
+
+    if (n == 0) {
+        // Pad input with [1, 0].
+        assert poseidon_ptr.input = PoseidonBuiltinState(s0=state.s0 + 1, s1=state.s1, s2=state.s2);
+        let res = poseidon_ptr.output.s0;
+        let poseidon_ptr = poseidon_ptr + PoseidonBuiltin.SIZE;
+        return (res=res);
+    }
+
+    assert n = 1;
+    // Pad input with [1].
+    assert poseidon_ptr.input = PoseidonBuiltinState(
+        s0=state.s0 + elements[0], s1=state.s1 + 1, s2=state.s2
+    );
+    let res = poseidon_ptr.output.s0;
+    let poseidon_ptr = poseidon_ptr + PoseidonBuiltin.SIZE;
+    return (res=res);
+}
+
+func main{output_ptr, poseidon_ptr: PoseidonBuiltin*}() {
+  alloc_locals;
+  let x = 7;
+  let y = 10;
+  let (z) = poseidon_hash(x, y);
+  local h1 = z;
+  tempvar arr: felt* = new (3, 5, 7);
+  let (h2) = poseidon_hash_many(3, arr);
+  assert [output_ptr] = h1;
+  assert [output_ptr + 1] = h1 + h2;
+  let output_ptr = output_ptr + 2;
+  return ();
+}
diff --git a/tests/Casm/Compilation/positive/out/test075.out b/tests/Casm/Compilation/positive/out/test075.out
new file mode 100644
index 000000000..b2823ee52
--- /dev/null
+++ b/tests/Casm/Compilation/positive/out/test075.out
@@ -0,0 +1 @@
+1725896553192394782543714999351211125700806599592244002323760583399227747069
diff --git a/tests/Casm/Compilation/positive/test075.juvix b/tests/Casm/Compilation/positive/test075.juvix
new file mode 100644
index 000000000..72137a4d4
--- /dev/null
+++ b/tests/Casm/Compilation/positive/test075.juvix
@@ -0,0 +1,8 @@
+-- Poseidon hash
+module test075;
+
+import Stdlib.Prelude open;
+import Stdlib.Cairo.Poseidon open;
+
+main : Field :=
+  poseidonHash2 7 10 + poseidonHashList [3; 5; 7];
diff --git a/tests/Casm/Reg/positive/out/test041.out b/tests/Casm/Reg/positive/out/test041.out
new file mode 100644
index 000000000..fb6a5833b
--- /dev/null
+++ b/tests/Casm/Reg/positive/out/test041.out
@@ -0,0 +1 @@
+960520245973031731151539114206112032362948660473336226878218924279221851535
diff --git a/tests/Casm/Reg/positive/test041.jvr b/tests/Casm/Reg/positive/test041.jvr
new file mode 100644
index 000000000..face2d87b
--- /dev/null
+++ b/tests/Casm/Reg/positive/test041.jvr
@@ -0,0 +1,17 @@
+-- Poseidon hash
+
+type PoseidonState {
+  poseidon_state : (field, field, field) -> PoseidonState;
+}
+
+function poseidon_hash(field, field) : field {
+  tmp[0] = alloc poseidon_state (arg[0], arg[1], 2);
+  tmp[1] = poseidon tmp[0];
+  ret tmp[1].poseidon_state[0];
+}
+
+function main() : field {
+  tmp[0] = call poseidon_hash (7, 10);
+  tmp[1] = fadd tmp[0] 5;
+  ret tmp[1];
+}