mirror of
https://github.com/anoma/juvix.git
synced 2024-09-11 08:15:41 +03:00
parent
b0fb240219
commit
75b5228258
@ -1 +1 @@
|
||||
Subproject commit e2efe4e6fe8e8bf1766050a7fa7ad8ff4e8c69fc
|
||||
Subproject commit b3768d2654e55fb7c8772592918b27e321a273b2
|
@ -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++
|
||||
|
@ -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
|
||||
|
@ -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" ->
|
||||
|
@ -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 {..} =
|
||||
|
@ -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
|
||||
|
32
src/Juvix/Compiler/Builtins/Cairo.hs
Normal file
32
src/Juvix/Compiler/Builtins/Cairo.hs
Normal file
@ -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)
|
@ -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)
|
||||
|
@ -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 ()
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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_
|
||||
|
||||
|
@ -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)
|
||||
|
@ -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 {}
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
|
@ -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) =>
|
||||
|
@ -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]
|
||||
|
@ -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
|
||||
]
|
||||
|
@ -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) =>
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
]
|
||||
|
@ -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)
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -289,6 +289,7 @@ genCode infoTable fi =
|
||||
Core.OpTrace -> OpTrace
|
||||
Core.OpFail -> OpFail
|
||||
Core.OpAnomaGet -> OpAnomaGet
|
||||
Core.OpPoseidonHash -> PrimUnop OpCairoPoseidon
|
||||
_ -> impossible
|
||||
|
||||
getArgsNum :: Symbol -> Int
|
||||
|
@ -106,6 +106,7 @@ parseUnop =
|
||||
<|> parseUnaryOp kwTrace OpTrace
|
||||
<|> parseUnaryOp kwFail OpFail
|
||||
<|> parseUnaryOp kwArgsNum (PrimUnop OpArgsNum)
|
||||
<|> parseUnaryOp kwPoseidon (PrimUnop OpCairoPoseidon)
|
||||
<|> parseUnaryOp kwAnomaGet (OpAnomaGet)
|
||||
|
||||
parseUnaryOp ::
|
||||
|
@ -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
|
||||
|
||||
|
@ -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"
|
||||
|
@ -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
|
||||
|
@ -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")
|
||||
]
|
||||
|
@ -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
|
||||
]
|
||||
|
@ -36,12 +36,8 @@ 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 =
|
||||
case validate labi instrs of
|
||||
Left err -> do
|
||||
assertFailure (prettyString err)
|
||||
Right () -> do
|
||||
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")
|
||||
@ -60,16 +56,25 @@ casmRunAssertion' bRunVM labi instrs blts inputFile expectedFile step =
|
||||
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
|
||||
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
|
||||
|
@ -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]
|
||||
|
13
tests/Casm/Cairo/reference/README.md
Normal file
13
tests/Casm/Cairo/reference/README.md
Normal file
@ -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
|
||||
```
|
71
tests/Casm/Cairo/reference/poseidon.cairo
Normal file
71
tests/Casm/Cairo/reference/poseidon.cairo
Normal file
@ -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 ();
|
||||
}
|
1
tests/Casm/Compilation/positive/out/test075.out
Normal file
1
tests/Casm/Compilation/positive/out/test075.out
Normal file
@ -0,0 +1 @@
|
||||
1725896553192394782543714999351211125700806599592244002323760583399227747069
|
8
tests/Casm/Compilation/positive/test075.juvix
Normal file
8
tests/Casm/Compilation/positive/test075.juvix
Normal file
@ -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];
|
1
tests/Casm/Reg/positive/out/test041.out
Normal file
1
tests/Casm/Reg/positive/out/test041.out
Normal file
@ -0,0 +1 @@
|
||||
960520245973031731151539114206112032362948660473336226878218924279221851535
|
17
tests/Casm/Reg/positive/test041.jvr
Normal file
17
tests/Casm/Reg/positive/test041.jvr
Normal file
@ -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];
|
||||
}
|
Loading…
Reference in New Issue
Block a user