anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-04 05:33:27 +03:00
Code Issues Projects Releases Wiki Activity

Add frontend support for Anoma Resource Machine builtins (#3113)

Browse Source 
This PR adds frontend builtin support for the Anoma Resource machine
functions provided in
[resource-machine.hoon](4897751366/hoon/resource-machine.hoon),
*except* for the `prove-logic` function which still needs some
discussion.

Users must now mark the Anoma `Resource` type with
`builtin-anoma-resource` and the Anoma `Action` type with
`builtin-anoma-action`. This is required because the resource machine
functions use these types.

The compiler does not check that the constructors of `Resource` and
`Action` match the RM spec. I made this decision because the Anoma types
are sill in flux and it's easier to change if correctness is delegated
to the RM library for now. We can add the constructor checks when the
Anoma RM interface is stable.

The test file
[test085.juvix](47ba3e2746/tests/Anoma/Compilation/positive/test085.juvix)
demonstrates how each builtin should be used.

### Core Evaluator

The Core evaluator does not support these builtin functions in normal
mode. When used for normalisation (e.g when used in the constant folding
pass) the Core evaluator leaves the builtin functions unchanged.

### Nock Evaluator

The Nock evaluator does not intercept the Anoma lib functions that the
builtins correspond to in the Nock backend. It executes the underlying
Nock code instead. This means that several of the functions cannot be
tested because they're either too slow (e.g commitment) or do not have
an implementation in the Nock code (e.g addDelta).

* Closes: https://github.com/anoma/juvix/issues/3084
This commit is contained in:
Paul Cadman 2024-10-22 12:10:08 +01:00 committed by GitHub
parent 8fb5ae77ba
commit 18cca89296
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
26 changed files with 765 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

103
src/Juvix/Compiler/Builtins/Anoma.hs
View File

@ -117,3 +117,106 @@ checkAnomaSha256 f = do
unless
(ftype == (nat_ --> byteArray))
$ builtinsErrorText l "anomaSha256 must be of type Nat -> ByteArray"
checkResource :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
checkResource d = do
let err = builtinsErrorText (getLoc d)
unless (null (d ^. inductiveParameters)) (err "AnomaResource should have no type parameters")
unless (isSmallUniverse' (d ^. inductiveType)) (err "AnomaResource should be in the small universe")
unless (length (d ^. inductiveConstructors) == 1) (err "AnomaResource should have exactly one constructor")
checkAction :: (Members '[Error ScoperError] r) => InductiveDef -> Sem r ()
checkAction d = do
let err = builtinsErrorText (getLoc d)
unless (null (d ^. inductiveParameters)) (err "AnomaAction should have no type parameters")
unless (isSmallUniverse' (d ^. inductiveType)) (err "AnomaAction should be in the small universe")
unless (length (d ^. inductiveConstructors) == 1) (err "AnomaAction should have exactly one constructor")
checkDelta :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
checkDelta d =
unless (isSmallUniverse' (d ^. axiomType)) $
builtinsErrorText (getLoc d) "AnomaDelta should be in the small universe"
checkKind :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
checkKind d =
unless (isSmallUniverse' (d ^. axiomType)) $
builtinsErrorText (getLoc d) "AnomaDelta should be in the small universe"
checkResourceCommitment :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkResourceCommitment f = do
let l = getLoc f
resource <- getBuiltinNameScoper (getLoc f) BuiltinAnomaResource
nat_ <- getBuiltinNameScoper l BuiltinNat
unless (f ^. axiomType === (resource --> nat_)) $
builtinsErrorText (getLoc f) "resourceCommitment must be of type AnomaResource -> Nat"
checkResourceNullifier :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkResourceNullifier f = do
let l = getLoc f
resource <- getBuiltinNameScoper l BuiltinAnomaResource
nat_ <- getBuiltinNameScoper l BuiltinNat
unless (f ^. axiomType === (resource --> nat_)) $
builtinsErrorText l "resourceNullifier must be of type AnomaResource -> Nat"
checkResourceKind :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkResourceKind f = do
let l = getLoc f
resource <- getBuiltinNameScoper l BuiltinAnomaResource
kind <- getBuiltinNameScoper l BuiltinAnomaKind
unless (f ^. axiomType === (resource --> kind)) $
builtinsErrorText l "resourceNullifier must be of type AnomaResource -> Nat"
checkResourceDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkResourceDelta f = do
let l = getLoc f
resource <- getBuiltinNameScoper l BuiltinAnomaResource
delta <- getBuiltinNameScoper l BuiltinAnomaDelta
unless (f ^. axiomType === (resource --> delta)) $
builtinsErrorText l "resourceDelta must be of type AnomaResource -> AnomaDelta"
checkProveAction :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkProveAction f = do
let l = getLoc f
action <- getBuiltinNameScoper l BuiltinAnomaAction
nat_ <- getBuiltinNameScoper l BuiltinNat
unless (f ^. axiomType === (action --> nat_)) $
builtinsErrorText l "proveAction must be of type AnomaAction -> Nat"
checkProveDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkProveDelta f = do
let l = getLoc f
delta <- getBuiltinNameScoper l BuiltinAnomaDelta
nat_ <- getBuiltinNameScoper l BuiltinNat
unless (f ^. axiomType === (delta --> nat_)) $
builtinsErrorText l "proveDelta must be of type AnomaDelta -> Nat"
checkActionDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkActionDelta f = do
let l = getLoc f
action <- getBuiltinNameScoper l BuiltinAnomaAction
delta <- getBuiltinNameScoper l BuiltinAnomaDelta
unless (f ^. axiomType === (action --> delta)) $
builtinsErrorText l "actionDelta must be of type AnomaAction -> AnomaDelta"
checkActionsDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkActionsDelta f = do
let l = getLoc f
action <- getBuiltinNameScoper l BuiltinAnomaAction
delta <- getBuiltinNameScoper l BuiltinAnomaDelta
list_ <- getBuiltinNameScoper l BuiltinList
unless (f ^. axiomType === (list_ @@ action --> delta)) $
builtinsErrorText l "actionsDelta must be of type List AnomaAction -> AnomaDelta"
checkDeltaBinaryOp :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkDeltaBinaryOp f = do
let l = getLoc f
delta <- getBuiltinNameScoper l BuiltinAnomaDelta
unless (f ^. axiomType === (delta --> delta --> delta)) $
builtinsErrorText l "deltaAdd must be of type AnomaDelta -> AnomaDelta -> AnomaDelta"
checkZeroDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
checkZeroDelta f = do
let l = getLoc f
delta <- getBuiltinNameScoper l BuiltinAnomaDelta
unless (f ^. axiomType === delta) $
builtinsErrorText (getLoc f) "zeroDelta must be of Delta"

49
src/Juvix/Compiler/Concrete/Data/Builtins.hs
View File

@ -57,6 +57,8 @@ builtinConstructors = \case
BuiltinPair -> [BuiltinPairConstr]
BuiltinPoseidonState -> [BuiltinMkPoseidonState]
BuiltinEcPoint -> [BuiltinMkEcPoint]
BuiltinAnomaResource -> [BuiltinMkAnomaResource]
BuiltinAnomaAction -> [BuiltinMkAnomaAction]
data BuiltinInductive
= BuiltinNat
@ -67,6 +69,8 @@ data BuiltinInductive
| BuiltinPair
| BuiltinPoseidonState
| BuiltinEcPoint
| BuiltinAnomaResource
| BuiltinAnomaAction
deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
instance Hashable BuiltinInductive
@ -85,6 +89,8 @@ instance Pretty BuiltinInductive where
BuiltinPair -> Str.pair
BuiltinPoseidonState -> Str.cairoPoseidonState
BuiltinEcPoint -> Str.cairoEcPoint
BuiltinAnomaResource -> Str.anomaResource
BuiltinAnomaAction -> Str.anomaAction
instance Pretty BuiltinConstructor where
pretty = \case
@ -101,6 +107,8 @@ instance Pretty BuiltinConstructor where
BuiltinPairConstr -> Str.pair
BuiltinMkPoseidonState -> Str.cairoMkPoseidonState
BuiltinMkEcPoint -> Str.cairoMkEcPoint
BuiltinMkAnomaResource -> Str.anomaMkResource
BuiltinMkAnomaAction -> Str.anomaMkAction
data BuiltinConstructor
= BuiltinNatZero
@ -116,6 +124,8 @@ data BuiltinConstructor
| BuiltinPairConstr
| BuiltinMkPoseidonState
| BuiltinMkEcPoint
| BuiltinMkAnomaResource
| BuiltinMkAnomaAction
deriving stock (Show, Eq, Ord, Generic, Data)
instance Hashable BuiltinConstructor
@ -228,6 +238,19 @@ data BuiltinAxiom
| BuiltinAnomaByteArrayToAnomaContents
| BuiltinAnomaByteArrayFromAnomaContents
| BuiltinAnomaSha256
| BuiltinAnomaDelta
| BuiltinAnomaKind
| BuiltinAnomaResourceCommitment
| BuiltinAnomaResourceNullifier
| BuiltinAnomaResourceKind
| BuiltinAnomaResourceDelta
| BuiltinAnomaActionDelta
| BuiltinAnomaActionsDelta
| BuiltinAnomaZeroDelta
| BuiltinAnomaAddDelta
| BuiltinAnomaSubDelta
| BuiltinAnomaProveAction
| BuiltinAnomaProveDelta
| BuiltinPoseidon
| BuiltinEcOp
| BuiltinRandomEcPoint
@ -275,6 +298,19 @@ instance HasNameKind BuiltinAxiom where
BuiltinAnomaByteArrayToAnomaContents -> KNameFunction
BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction
BuiltinAnomaSha256 -> KNameFunction
BuiltinAnomaDelta -> KNameInductive
BuiltinAnomaKind -> KNameInductive
BuiltinAnomaResourceCommitment -> KNameFunction
BuiltinAnomaResourceNullifier -> KNameFunction
BuiltinAnomaResourceKind -> KNameFunction
BuiltinAnomaResourceDelta -> KNameFunction
BuiltinAnomaActionDelta -> KNameFunction
BuiltinAnomaActionsDelta -> KNameFunction
BuiltinAnomaZeroDelta -> KNameFunction
BuiltinAnomaAddDelta -> KNameFunction
BuiltinAnomaSubDelta -> KNameFunction
BuiltinAnomaProveAction -> KNameFunction
BuiltinAnomaProveDelta -> KNameFunction
BuiltinPoseidon -> KNameFunction
BuiltinEcOp -> KNameFunction
BuiltinRandomEcPoint -> KNameFunction
@ -329,6 +365,19 @@ instance Pretty BuiltinAxiom where
BuiltinAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
BuiltinAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
BuiltinAnomaSha256 -> Str.anomaSha256
BuiltinAnomaDelta -> Str.anomaDelta
BuiltinAnomaKind -> Str.anomaKind
BuiltinAnomaResourceCommitment -> Str.anomaResourceCommitment
BuiltinAnomaResourceNullifier -> Str.anomaResourceNullifier
BuiltinAnomaResourceKind -> Str.anomaResourceKind
BuiltinAnomaResourceDelta -> Str.anomaResourceDelta
BuiltinAnomaActionDelta -> Str.anomaActionDelta
BuiltinAnomaActionsDelta -> Str.anomaActionsDelta
BuiltinAnomaZeroDelta -> Str.anomaZeroDelta
BuiltinAnomaAddDelta -> Str.anomaAddDelta
BuiltinAnomaSubDelta -> Str.anomaSubDelta
BuiltinAnomaProveDelta -> Str.anomaProveDelta
BuiltinAnomaProveAction -> Str.anomaProveAction
BuiltinPoseidon -> Str.cairoPoseidon
BuiltinEcOp -> Str.cairoEcOp
BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

6
src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
View File

@ -63,6 +63,12 @@ getIntSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinInt
getPoseidonStateSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
getPoseidonStateSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinPoseidonState
getAnomaResourceSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
getAnomaResourceSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinAnomaResource
getAnomaActionSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
getAnomaActionSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinAnomaAction
getEcPointSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
getEcPointSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinEcPoint

20
src/Juvix/Compiler/Core/Evaluator.hs
View File

@ -228,6 +228,17 @@ geval opts herr tab env0 = eval' env0
OpAnomaByteArrayToAnomaContents -> anomaByteArrayToAnomaContents
OpAnomaByteArrayFromAnomaContents -> anomaByteArrayFromAnomaContents
OpAnomaSha256 -> anomaSha256
OpAnomaResourceCommitment -> normalizeOrUnsupported opcode
OpAnomaResourceNullifier -> normalizeOrUnsupported opcode
OpAnomaResourceKind -> normalizeOrUnsupported opcode
OpAnomaResourceDelta -> normalizeOrUnsupported opcode
OpAnomaActionDelta -> normalizeOrUnsupported opcode
OpAnomaActionsDelta -> normalizeOrUnsupported opcode
OpAnomaProveAction -> normalizeOrUnsupported opcode
OpAnomaProveDelta -> normalizeOrUnsupported opcode
OpAnomaZeroDelta -> normalizeOrUnsupported opcode
OpAnomaAddDelta -> normalizeOrUnsupported opcode
OpAnomaSubDelta -> normalizeOrUnsupported opcode
OpPoseidonHash -> poseidonHashOp
OpEc -> ecOp
OpRandomEcPoint -> randomEcPointOp
@ -384,6 +395,15 @@ geval opts herr tab env0 = eval' env0
Exception.throw (EvalError ("assertion failed: " <> printNode val) Nothing)
{-# INLINE assertOp #-}
normalizeOrUnsupported :: BuiltinOp -> [Node] -> Node
normalizeOrUnsupported op args =
if
| opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
mkBuiltinApp' op (eval' env <$> args)
| otherwise ->
err ("unsupported builtin operation: " <> show op)
{-# INLINE normalizeOrUnsupported #-}
anomaGetOp :: [Node] -> Node
anomaGetOp = unary $ \arg ->
if

22
src/Juvix/Compiler/Core/Extra/Utils.hs
View File

@ -195,6 +195,17 @@ isDebugOp = \case
OpAnomaSignDetached -> False
OpAnomaVerifyDetached -> False
OpAnomaVerifyWithMessage -> False
OpAnomaResourceCommitment -> False
OpAnomaResourceNullifier -> False
OpAnomaResourceKind -> False
OpAnomaResourceDelta -> False
OpAnomaActionDelta -> False
OpAnomaActionsDelta -> False
OpAnomaProveAction -> False
OpAnomaProveDelta -> False
OpAnomaZeroDelta -> False
OpAnomaAddDelta -> False
OpAnomaSubDelta -> False
OpEc -> False
OpFieldAdd -> False
OpFieldDiv -> False
@ -482,6 +493,17 @@ builtinOpArgTypes = \case
OpAnomaByteArrayToAnomaContents -> [mkDynamic']
OpAnomaByteArrayFromAnomaContents -> [mkTypeInteger', mkTypeInteger']
OpAnomaSha256 -> [mkTypeInteger']
OpAnomaResourceCommitment -> [mkDynamic']
OpAnomaResourceNullifier -> [mkDynamic']
OpAnomaResourceKind -> [mkDynamic']
OpAnomaResourceDelta -> [mkDynamic']
OpAnomaActionDelta -> [mkDynamic']
OpAnomaActionsDelta -> [mkDynamic']
OpAnomaProveAction -> [mkDynamic']
OpAnomaProveDelta -> [mkDynamic']
OpAnomaZeroDelta -> []
OpAnomaAddDelta -> [mkDynamic', mkDynamic']
OpAnomaSubDelta -> [mkDynamic', mkDynamic']
OpPoseidonHash -> [mkDynamic']
OpEc -> [mkDynamic', mkTypeField', mkDynamic']
OpRandomEcPoint -> []

11
src/Juvix/Compiler/Core/Keywords.hs
View File

@ -8,13 +8,24 @@ where
import Juvix.Data.Keyword
import Juvix.Data.Keyword.All
( delimSemicolon,
kwAnomaActionDelta,
kwAnomaActionsDelta,
kwAnomaAddDelta,
kwAnomaDecode,
kwAnomaEncode,
kwAnomaProveAction,
kwAnomaProveDelta,
kwAnomaResourceCommitment,
kwAnomaResourceDelta,
kwAnomaResourceKind,
kwAnomaResourceNullifier,
kwAnomaSha256,
kwAnomaSign,
kwAnomaSignDetached,
kwAnomaSubDelta,
kwAnomaVerifyDetached,
kwAnomaVerifyWithMessage,
kwAnomaZeroDelta,
kwAny,
kwAssert,
kwAssign,

48
src/Juvix/Compiler/Core/Language/Builtins.hs
View File

@ -40,6 +40,17 @@ data BuiltinOp
| OpAnomaByteArrayToAnomaContents
| OpAnomaByteArrayFromAnomaContents
| OpAnomaSha256
| OpAnomaResourceCommitment
| OpAnomaResourceNullifier
| OpAnomaResourceKind
| OpAnomaResourceDelta
| OpAnomaActionDelta
| OpAnomaActionsDelta
| OpAnomaProveAction
| OpAnomaProveDelta
| OpAnomaZeroDelta
| OpAnomaAddDelta
| OpAnomaSubDelta
| OpPoseidonHash
| OpEc
| OpRandomEcPoint
@ -47,7 +58,7 @@ data BuiltinOp
| OpUInt8FromInt
| OpByteArrayFromListByte
| OpByteArrayLength
deriving stock (Eq, Generic)
deriving stock (Eq, Generic, Show)
instance Serialize BuiltinOp
@ -114,6 +125,17 @@ builtinOpArgsNum = \case
OpAnomaByteArrayToAnomaContents -> 1
OpAnomaByteArrayFromAnomaContents -> 2
OpAnomaSha256 -> 1
OpAnomaResourceCommitment -> 1
OpAnomaResourceNullifier -> 1
OpAnomaResourceKind -> 1
OpAnomaResourceDelta -> 1
OpAnomaActionDelta -> 1
OpAnomaActionsDelta -> 1
OpAnomaProveAction -> 1
OpAnomaProveDelta -> 1
OpAnomaZeroDelta -> 0
OpAnomaAddDelta -> 2
OpAnomaSubDelta -> 2
OpPoseidonHash -> 1
OpEc -> 3
OpRandomEcPoint -> 0
@ -164,6 +186,17 @@ builtinIsFoldable = \case
OpAnomaVerifyWithMessage -> False
OpAnomaByteArrayToAnomaContents -> False
OpAnomaByteArrayFromAnomaContents -> False
OpAnomaResourceCommitment -> False
OpAnomaResourceNullifier -> False
OpAnomaResourceKind -> False
OpAnomaResourceDelta -> False
OpAnomaActionDelta -> False
OpAnomaActionsDelta -> False
OpAnomaProveAction -> False
OpAnomaProveDelta -> False
OpAnomaZeroDelta -> False
OpAnomaAddDelta -> False
OpAnomaSubDelta -> False
OpAnomaSha256 -> False
OpPoseidonHash -> False
OpEc -> False
@ -199,7 +232,18 @@ builtinsAnoma =
OpAnomaSignDetached,
OpAnomaByteArrayToAnomaContents,
OpAnomaByteArrayFromAnomaContents,
OpAnomaSha256
OpAnomaSha256,
OpAnomaResourceCommitment,
OpAnomaResourceNullifier,
OpAnomaResourceKind,
OpAnomaResourceDelta,
OpAnomaActionDelta,
OpAnomaActionsDelta,
OpAnomaProveAction,
OpAnomaProveDelta,
OpAnomaZeroDelta,
OpAnomaAddDelta,
OpAnomaSubDelta
]
builtinsUInt8 :: [BuiltinOp]

46
src/Juvix/Compiler/Core/Pretty/Base.hs
View File

@ -64,6 +64,17 @@ instance PrettyCode BuiltinOp where
OpAnomaByteArrayToAnomaContents -> return primAnomaByteArrayToAnomaContents
OpAnomaByteArrayFromAnomaContents -> return primAnomaByteArrayFromAnomaContents
OpAnomaSha256 -> return primAnomaSha256
OpAnomaResourceCommitment -> return primResourceCommitment
OpAnomaResourceNullifier -> return primResourceNullifier
OpAnomaResourceKind -> return primResourceKind
OpAnomaResourceDelta -> return primResourceDelta
OpAnomaActionDelta -> return primActionDelta
OpAnomaActionsDelta -> return primActionsDelta
OpAnomaProveAction -> return primProveAction
OpAnomaProveDelta -> return primProveDelta
OpAnomaZeroDelta -> return primZeroDelta
OpAnomaAddDelta -> return primAddDelta
OpAnomaSubDelta -> return primSubDelta
OpPoseidonHash -> return primPoseidonHash
OpEc -> return primEc
OpRandomEcPoint -> return primRandomEcPoint
@ -601,6 +612,8 @@ instance PrettyCode InfoTable where
BuiltinNat -> False
BuiltinInt -> False
BuiltinBool -> False
BuiltinAnomaResource -> True
BuiltinAnomaAction -> True
Just _ -> False
Nothing -> True
@ -908,6 +921,39 @@ primAnomaByteArrayFromAnomaContents = primitive Str.anomaByteArrayFromAnomaConte
primAnomaSha256 :: Doc Ann
primAnomaSha256 = primitive Str.anomaSha256
primResourceCommitment :: Doc Ann
primResourceCommitment = primitive Str.anomaResourceCommitment
primResourceNullifier :: Doc Ann
primResourceNullifier = primitive Str.anomaResourceNullifier
primResourceKind :: Doc Ann
primResourceKind = primitive Str.anomaResourceKind
primResourceDelta :: Doc Ann
primResourceDelta = primitive Str.anomaResourceDelta
primActionDelta :: Doc Ann
primActionDelta = primitive Str.anomaActionDelta
primActionsDelta :: Doc Ann
primActionsDelta = primitive Str.anomaActionsDelta
primProveDelta :: Doc Ann
primProveDelta = primitive Str.anomaProveDelta
primProveAction :: Doc Ann
primProveAction = primitive Str.anomaProveAction
primZeroDelta :: Doc Ann
primZeroDelta = primitive Str.anomaZeroDelta
primAddDelta :: Doc Ann
primAddDelta = primitive Str.anomaAddDelta
primSubDelta :: Doc Ann
primSubDelta = primitive Str.anomaSubDelta
primPoseidonHash :: Doc Ann
primPoseidonHash = primitive Str.cairoPoseidon

11
src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
View File

@ -81,6 +81,17 @@ computeNodeTypeInfo md = umapL go
OpAnomaByteArrayFromAnomaContents -> Info.getNodeType node
OpAnomaByteArrayToAnomaContents -> mkTypeInteger'
OpAnomaSha256 -> mkTypeByteArray'
OpAnomaResourceCommitment -> mkTypeInteger'
OpAnomaResourceNullifier -> mkTypeInteger'
OpAnomaResourceKind -> mkDynamic'
OpAnomaResourceDelta -> mkDynamic'
OpAnomaActionDelta -> mkDynamic'
OpAnomaActionsDelta -> mkDynamic'
OpAnomaProveAction -> mkTypeInteger'
OpAnomaProveDelta -> mkTypeInteger'
OpAnomaZeroDelta -> mkDynamic'
OpAnomaAddDelta -> mkDynamic'
OpAnomaSubDelta -> mkDynamic'
OpPoseidonHash -> case _builtinAppArgs of
[arg] -> Info.getNodeType arg
_ -> error "incorrect poseidon builtin application"

122
src/Juvix/Compiler/Core/Translation/FromInternal.hs
View File

@ -228,6 +228,8 @@ goConstructor sym ctor = do
Just Internal.BuiltinPairConstr -> freshTag
Just Internal.BuiltinMkPoseidonState -> freshTag
Just Internal.BuiltinMkEcPoint -> freshTag
Just Internal.BuiltinMkAnomaAction -> freshTag
Just Internal.BuiltinMkAnomaResource -> freshTag
Nothing -> freshTag
ctorType :: Sem r Type
@ -647,6 +649,19 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
Internal.BuiltinAnomaByteArrayToAnomaContents -> return ()
Internal.BuiltinAnomaByteArrayFromAnomaContents -> return ()
Internal.BuiltinAnomaSha256 -> return ()
Internal.BuiltinAnomaDelta -> registerInductiveAxiom (Just BuiltinAnomaDelta) []
Internal.BuiltinAnomaKind -> registerInductiveAxiom (Just BuiltinAnomaKind) []
Internal.BuiltinAnomaResourceCommitment -> return ()
Internal.BuiltinAnomaResourceNullifier -> return ()
Internal.BuiltinAnomaResourceDelta -> return ()
Internal.BuiltinAnomaResourceKind -> return ()
Internal.BuiltinAnomaActionDelta -> return ()
Internal.BuiltinAnomaActionsDelta -> return ()
Internal.BuiltinAnomaProveDelta -> return ()
Internal.BuiltinAnomaProveAction -> return ()
Internal.BuiltinAnomaZeroDelta -> return ()
Internal.BuiltinAnomaAddDelta -> return ()
Internal.BuiltinAnomaSubDelta -> return ()
Internal.BuiltinPoseidon -> return ()
Internal.BuiltinEcOp -> return ()
Internal.BuiltinRandomEcPoint -> return ()
@ -861,6 +876,82 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
natType
(mkBuiltinApp' OpAnomaSha256 [mkVar' 0])
)
Internal.BuiltinAnomaDelta -> return ()
Internal.BuiltinAnomaKind -> return ()
Internal.BuiltinAnomaResourceCommitment -> do
resourceType <- getAnomaResourceType
registerAxiomDef
( mkLambda'
resourceType
(mkBuiltinApp' OpAnomaResourceCommitment [mkVar' 0])
)
Internal.BuiltinAnomaResourceNullifier -> do
resourceType <- getAnomaResourceType
registerAxiomDef
( mkLambda'
resourceType
(mkBuiltinApp' OpAnomaResourceNullifier [mkVar' 0])
)
Internal.BuiltinAnomaResourceKind -> do
resourceType <- getAnomaResourceType
registerAxiomDef
( mkLambda'
resourceType
(mkBuiltinApp' OpAnomaResourceKind [mkVar' 0])
)
Internal.BuiltinAnomaResourceDelta -> do
resourceType <- getAnomaResourceType
registerAxiomDef
( mkLambda'
resourceType
(mkBuiltinApp' OpAnomaResourceDelta [mkVar' 0])
)
Internal.BuiltinAnomaActionDelta -> do
actionType <- getAnomaActionType
registerAxiomDef
( mkLambda'
actionType
(mkBuiltinApp' OpAnomaActionDelta [mkVar' 0])
)
Internal.BuiltinAnomaActionsDelta -> do
registerAxiomDef
( mkLambda'
mkDynamic'
(mkBuiltinApp' OpAnomaActionsDelta [mkVar' 0])
)
Internal.BuiltinAnomaProveAction -> do
actionType <- getAnomaActionType
registerAxiomDef
( mkLambda'
actionType
(mkBuiltinApp' OpAnomaProveAction [mkVar' 0])
)
Internal.BuiltinAnomaProveDelta -> do
registerAxiomDef
( mkLambda'
mkDynamic'
(mkBuiltinApp' OpAnomaProveDelta [mkVar' 0])
)
Internal.BuiltinAnomaZeroDelta -> do
registerAxiomDef (mkBuiltinApp' OpAnomaZeroDelta [])
Internal.BuiltinAnomaAddDelta -> do
registerAxiomDef
( mkLambda'
mkDynamic'
( mkLambda'
mkDynamic'
(mkBuiltinApp' OpAnomaAddDelta [mkVar' 1, mkVar' 0])
)
)
Internal.BuiltinAnomaSubDelta -> do
registerAxiomDef
( mkLambda'
mkDynamic'
( mkLambda'
mkDynamic'
(mkBuiltinApp' OpAnomaSubDelta [mkVar' 1, mkVar' 0])
)
)
Internal.BuiltinPoseidon -> do
psName <- getPoseidonStateName
psSym <- getPoseidonStateSymbol
@ -914,6 +1005,24 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
getEcPointName :: Sem r Text
getEcPointName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinEcPoint
getAnomaResourceName :: Sem r Text
getAnomaResourceName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinAnomaResource
getAnomaActionName :: Sem r Text
getAnomaActionName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinAnomaAction
getAnomaResourceType :: Sem r Type
getAnomaResourceType = do
resourceName <- getAnomaResourceName
resourceSymbol <- getAnomaResourceSymbol
return (mkTypeConstr (setInfoName resourceName mempty) resourceSymbol [])
getAnomaActionType :: Sem r Type
getAnomaActionType = do
actionName <- getAnomaActionName
actionSymbol <- getAnomaActionSymbol
return (mkTypeConstr (setInfoName actionName mempty) actionSymbol [])
registerAxiomDef :: Node -> Sem r ()
registerAxiomDef body = do
let name = a ^. Internal.axiomName
@ -1285,6 +1394,19 @@ goApplication a = do
Just Internal.BuiltinAnomaByteArrayToAnomaContents -> app
Just Internal.BuiltinAnomaByteArrayFromAnomaContents -> app
Just Internal.BuiltinAnomaSha256 -> app
Just Internal.BuiltinAnomaDelta -> app
Just Internal.BuiltinAnomaKind -> app
Just Internal.BuiltinAnomaResourceCommitment -> app
Just Internal.BuiltinAnomaResourceNullifier -> app
Just Internal.BuiltinAnomaResourceDelta -> app
Just Internal.BuiltinAnomaResourceKind -> app
Just Internal.BuiltinAnomaActionDelta -> app
Just Internal.BuiltinAnomaActionsDelta -> app
Just Internal.BuiltinAnomaZeroDelta -> app
Just Internal.BuiltinAnomaAddDelta -> app
Just Internal.BuiltinAnomaSubDelta -> app
Just Internal.BuiltinAnomaProveAction -> app
Just Internal.BuiltinAnomaProveDelta -> app
Just Internal.BuiltinPoseidon -> app
Just Internal.BuiltinEcOp -> app
Just Internal.BuiltinRandomEcPoint -> app

12
src/Juvix/Compiler/Core/Translation/FromSource.hs
View File

@ -585,6 +585,18 @@ builtinAppExpr varsNum vars = do
<|> (kw kwByteArrayFromListByte $> OpByteArrayFromListByte)
<|> (kw kwByteArrayLength $> OpByteArrayLength)
<|> (kw kwAnomaSha256 $> OpAnomaSha256)
<|> (kw kwAnomaResourceCommitment $> OpAnomaResourceCommitment)
<|> (kw kwAnomaResourceNullifier $> OpAnomaResourceNullifier)
<|> (kw kwAnomaResourceKind $> OpAnomaResourceKind)
<|> (kw kwAnomaResourceDelta $> OpAnomaResourceDelta)
<|> (kw kwAnomaActionDelta $> OpAnomaActionDelta)
<|> (kw kwAnomaActionsDelta $> OpAnomaActionsDelta)
<|> (kw kwAnomaProveAction $> OpAnomaProveAction)
<|> (kw kwAnomaProveDelta $> OpAnomaProveDelta)
<|> (kw kwAnomaZeroDelta $> OpAnomaZeroDelta)
<|> (kw kwAnomaAddDelta $> OpAnomaAddDelta)
<|> (kw kwAnomaSubDelta $> OpAnomaSubDelta)
args <- P.many (atom varsNum vars)
return $ mkBuiltinApp' op args

17
src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
View File

@ -73,6 +73,8 @@ fromCore fsize tab =
BuiltinBoolFalse -> False
BuiltinIntOfNat -> False
BuiltinIntNegSuc -> False
BuiltinMkAnomaResource -> True
BuiltinMkAnomaAction -> True
shouldKeepType :: BuiltinType -> Bool
shouldKeepType = \case
@ -110,6 +112,19 @@ fromCore fsize tab =
BuiltinAnomaByteArrayToAnomaContents -> False
BuiltinAnomaByteArrayFromAnomaContents -> False
BuiltinAnomaSha256 -> False
BuiltinAnomaDelta -> False
BuiltinAnomaKind -> False
BuiltinAnomaResourceCommitment -> False
BuiltinAnomaResourceDelta -> False
BuiltinAnomaResourceNullifier -> False
BuiltinAnomaResourceKind -> False
BuiltinAnomaActionDelta -> False
BuiltinAnomaActionsDelta -> False
BuiltinAnomaAddDelta -> False
BuiltinAnomaSubDelta -> False
BuiltinAnomaZeroDelta -> False
BuiltinAnomaProveAction -> False
BuiltinAnomaProveDelta -> False
BuiltinPoseidon -> False
BuiltinEcOp -> False
BuiltinRandomEcPoint -> False
@ -129,6 +144,8 @@ fromCore fsize tab =
BuiltinNat -> False
BuiltinInt -> False
BuiltinBool -> False
BuiltinAnomaResource -> True
BuiltinAnomaAction -> True
translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo
translateFunctionInfo tab IdentifierInfo {..} =

2
src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
View File

@ -197,6 +197,8 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
BuiltinPair -> return ()
BuiltinPoseidonState -> return ()
BuiltinEcPoint -> return ()
BuiltinAnomaResource -> return ()
BuiltinAnomaAction -> return ()
addInductiveStartNode :: Sem r ()
addInductiveStartNode = addStartNode (i ^. inductiveName)

15
src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
View File

@ -520,6 +520,8 @@ checkBuiltinInductive d b = localBuiltins $ case b of
BuiltinPair -> checkPairDef d
BuiltinPoseidonState -> checkPoseidonStateDef d
BuiltinEcPoint -> checkEcPointDef d
BuiltinAnomaResource -> checkResource d
BuiltinAnomaAction -> checkAction d
localBuiltins :: (Members '[Reader S.InfoTable] r) => Sem (Reader BuiltinsTable ': r) a -> Sem r a
localBuiltins m = do
@ -601,6 +603,19 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
BuiltinAnomaByteArrayFromAnomaContents -> checkAnomaByteArrayFromAnomaContents d
BuiltinAnomaByteArrayToAnomaContents -> checkAnomaByteArrayToAnomaContents d
BuiltinAnomaSha256 -> checkAnomaSha256 d
BuiltinAnomaDelta -> checkDelta d
BuiltinAnomaKind -> checkKind d
BuiltinAnomaResourceCommitment -> checkResourceCommitment d
BuiltinAnomaResourceNullifier -> checkResourceNullifier d
BuiltinAnomaResourceKind -> checkResourceKind d
BuiltinAnomaResourceDelta -> checkResourceDelta d
BuiltinAnomaActionDelta -> checkActionDelta d
BuiltinAnomaActionsDelta -> checkActionsDelta d
BuiltinAnomaZeroDelta -> checkZeroDelta d
BuiltinAnomaAddDelta -> checkDeltaBinaryOp d
BuiltinAnomaSubDelta -> checkDeltaBinaryOp d
BuiltinAnomaProveDelta -> checkProveDelta d
BuiltinAnomaProveAction -> checkProveAction d
BuiltinPoseidon -> checkPoseidon d
BuiltinEcOp -> checkEcOp d
BuiltinRandomEcPoint -> checkRandomEcPoint d

2
src/Juvix/Compiler/Nockma/Evaluator.hs
View File

@ -229,7 +229,7 @@ evalProfile inistack initerm =
case _anomaLibCallRef of
AnomaLibValue (AnomaRmValue v) -> case v of
RmZeroDelta -> nonInterceptCall
AnomaLibFunction (AnomaRmFunction _) -> error "Resource Machine client library functions are not supported"
AnomaLibFunction (AnomaRmFunction _) -> nonInterceptCall
AnomaLibFunction (AnomaStdlibFunction f) -> case f of
StdlibDec -> unaArith pred
StdlibAdd -> binArith (+)

15
src/Juvix/Compiler/Nockma/Translation/FromTree.hs
View File

@ -571,6 +571,17 @@ compile = \case
Tree.OpAnomaByteArrayFromAnomaContents -> return (goAnomaByteArrayFromAnomaContents args)
Tree.OpAnomaByteArrayToAnomaContents -> return (goAnomaByteArrayToAnomaContents args)
Tree.OpAnomaSha256 -> goAnomaSha256 args
Tree.OpAnomaResourceCommitment -> callRm RmCommit args
Tree.OpAnomaResourceNullifier -> callRm RmNullify args
Tree.OpAnomaResourceKind -> callRm RmKind args
Tree.OpAnomaResourceDelta -> callRm RmResourceDelta args
Tree.OpAnomaActionDelta -> callRm RmActionDelta args
Tree.OpAnomaActionsDelta -> callRm RmMakeDelta args
Tree.OpAnomaProveAction -> callRm RmProveAction args
Tree.OpAnomaProveDelta -> callRm RmProveDelta args
Tree.OpAnomaZeroDelta -> rmValue RmZeroDelta
Tree.OpAnomaAddDelta -> callRm RmDeltaAdd args
Tree.OpAnomaSubDelta -> callRm RmDeltaSub args
goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural)
goByteArrayOp Tree.NodeByteArray {..} = do
@ -861,6 +872,10 @@ callAnomaLib fun args = do
callStdlib :: (Member (Reader CompilerCtx) r) => StdlibFunction -> [Term Natural] -> Sem r (Term Natural)
callStdlib f = callAnomaLib (AnomaStdlibFunction f)
-- | Convenience function to call an Anoma Resource Machine function
callRm :: (Member (Reader CompilerCtx) r) => RmFunction -> [Term Natural] -> Sem r (Term Natural)
callRm f = callAnomaLib (AnomaRmFunction f)
-- | Get a value from the Anoma library
anomaLibValue :: (Member (Reader CompilerCtx) r) => AnomaValue -> Sem r (Term Natural)
anomaLibValue v = do

11
src/Juvix/Compiler/Tree/Keywords.hs
View File

@ -9,16 +9,27 @@ import Juvix.Compiler.Tree.Keywords.Base
import Juvix.Data.Keyword.All
( kwAdd_,
kwAlloc,
kwAnomaActionDelta,
kwAnomaActionsDelta,
kwAnomaAddDelta,
kwAnomaByteArrayFromAnomaContents,
kwAnomaByteArrayToAnomaContents,
kwAnomaDecode,
kwAnomaEncode,
kwAnomaGet,
kwAnomaProveAction,
kwAnomaProveDelta,
kwAnomaResourceCommitment,
kwAnomaResourceDelta,
kwAnomaResourceKind,
kwAnomaResourceNullifier,
kwAnomaSha256,
kwAnomaSign,
kwAnomaSignDetached,
kwAnomaSubDelta,
kwAnomaVerifyDetached,
kwAnomaVerifyWithMessage,
kwAnomaZeroDelta,
kwArgsNum,
kwAssert,
kwAtoi,

24
src/Juvix/Compiler/Tree/Language/Builtins.hs
View File

@ -102,4 +102,26 @@ data AnomaOp
OpAnomaByteArrayFromAnomaContents
| -- | Hash a value using SHA256
OpAnomaSha256
deriving stock (Eq)
| -- | Compute the commitment of a Resource
OpAnomaResourceCommitment
| -- | Compute the nullifier of a Resource
OpAnomaResourceNullifier
| -- | Compute the kind of a Resource
OpAnomaResourceKind
| -- | Compute the delta of a Resource
OpAnomaResourceDelta
| -- | Compute the delta of an Action
OpAnomaActionDelta
| -- | Compute the delta of a list of Actions
OpAnomaActionsDelta
| -- | Compute the proof of an Action
OpAnomaProveAction
| -- | Compute the proof of a Delta
OpAnomaProveDelta
| -- | The zero Delta
OpAnomaZeroDelta
| -- | Add Deltas
OpAnomaAddDelta
| -- | Subtract Deltas
OpAnomaSubDelta
deriving stock (Eq, Show)

11
src/Juvix/Compiler/Tree/Pretty/Base.hs
View File

@ -287,6 +287,17 @@ instance PrettyCode AnomaOp where
OpAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
OpAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
OpAnomaSha256 -> Str.anomaSha256
OpAnomaResourceCommitment -> Str.anomaResourceCommitment
OpAnomaResourceNullifier -> Str.anomaResourceNullifier
OpAnomaResourceKind -> Str.anomaResourceKind
OpAnomaResourceDelta -> Str.anomaResourceDelta
OpAnomaActionDelta -> Str.anomaActionDelta
OpAnomaActionsDelta -> Str.anomaActionsDelta
OpAnomaProveAction -> Str.anomaProveAction
OpAnomaProveDelta -> Str.anomaProveDelta
OpAnomaZeroDelta -> Str.anomaZeroDelta
OpAnomaAddDelta -> Str.anomaAddDelta
OpAnomaSubDelta -> Str.anomaSubDelta
instance PrettyCode UnaryOpcode where
ppCode = \case

25
src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
View File

@ -10,23 +10,10 @@ checkNoAnoma = walkT checkNode
where
checkNode :: Symbol -> Node -> Sem r ()
checkNode _ = \case
Anoma NodeAnoma {..} -> case _nodeAnomaOpcode of
OpAnomaGet -> unsupportedErr "OpAnomaGet"
OpAnomaEncode -> unsupportedErr "OpAnomaEncode"
OpAnomaDecode -> unsupportedErr "OpAnomaDecode"
OpAnomaVerifyDetached -> unsupportedErr "OpAnomaVerifyDetached"
OpAnomaSign -> unsupportedErr "OpAnomaSign"
OpAnomaSignDetached -> unsupportedErr "OpAnomaSignDetached"
OpAnomaVerifyWithMessage -> unsupportedErr "OpAnomaVerifyWithMessage"
OpAnomaByteArrayFromAnomaContents -> unsupportedErr "OpAnomaByteArrayFromAnomaContents"
OpAnomaByteArrayToAnomaContents -> unsupportedErr "OpAnomaByteArrayToAnomaContents"
OpAnomaSha256 -> unsupportedErr "OpAnomaSha256"
where
unsupportedErr :: Text -> Sem r ()
unsupportedErr opName =
throw
TreeError
{ _treeErrorMsg = opName <> " is unsupported",
_treeErrorLoc = _nodeAnomaInfo ^. nodeInfoLocation
}
Anoma NodeAnoma {..} ->
throw
TreeError
{ _treeErrorMsg = show _nodeAnomaOpcode <> " is unsupported",
_treeErrorLoc = _nodeAnomaInfo ^. nodeInfoLocation
}
_ -> return ()

11
src/Juvix/Compiler/Tree/Translation/FromCore.hs
View File

@ -352,6 +352,17 @@ genCode infoTable fi =
Core.OpAnomaByteArrayToAnomaContents -> OpAnomaByteArrayToAnomaContents
Core.OpAnomaByteArrayFromAnomaContents -> OpAnomaByteArrayFromAnomaContents
Core.OpAnomaSha256 -> OpAnomaSha256
Core.OpAnomaResourceCommitment -> OpAnomaResourceCommitment
Core.OpAnomaResourceNullifier -> OpAnomaResourceNullifier
Core.OpAnomaResourceKind -> OpAnomaResourceKind
Core.OpAnomaResourceDelta -> OpAnomaResourceDelta
Core.OpAnomaActionDelta -> OpAnomaActionDelta
Core.OpAnomaActionsDelta -> OpAnomaActionsDelta
Core.OpAnomaProveAction -> OpAnomaProveAction
Core.OpAnomaProveDelta -> OpAnomaProveDelta
Core.OpAnomaZeroDelta -> OpAnomaZeroDelta
Core.OpAnomaAddDelta -> OpAnomaAddDelta
Core.OpAnomaSubDelta -> OpAnomaSubDelta
_ -> impossible
getArgsNum :: Symbol -> Int

11
src/Juvix/Compiler/Tree/Translation/FromSource.hs
View File

@ -156,6 +156,17 @@ parseAnoma =
<|> parseAnoma' kwAnomaByteArrayToAnomaContents OpAnomaByteArrayToAnomaContents
<|> parseAnoma' kwAnomaByteArrayFromAnomaContents OpAnomaByteArrayFromAnomaContents
<|> parseAnoma' kwAnomaSha256 OpAnomaSha256
<|> parseAnoma' kwAnomaResourceCommitment OpAnomaResourceCommitment
<|> parseAnoma' kwAnomaResourceNullifier OpAnomaResourceNullifier
<|> parseAnoma' kwAnomaResourceKind OpAnomaResourceKind
<|> parseAnoma' kwAnomaResourceDelta OpAnomaResourceDelta
<|> parseAnoma' kwAnomaActionDelta OpAnomaActionDelta
<|> parseAnoma' kwAnomaActionsDelta OpAnomaActionsDelta
<|> parseAnoma' kwAnomaProveAction OpAnomaProveAction
<|> parseAnoma' kwAnomaProveDelta OpAnomaProveDelta
<|> parseAnoma' kwAnomaZeroDelta OpAnomaZeroDelta
<|> parseAnoma' kwAnomaAddDelta OpAnomaAddDelta
<|> parseAnoma' kwAnomaSubDelta OpAnomaSubDelta
parseAnoma' ::
(Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) =>

33
src/Juvix/Data/Keyword/All.hs
View File

@ -502,6 +502,39 @@ kwByteArrayLength = asciiKw Str.byteArrayLength
kwAnomaSha256 :: Keyword
kwAnomaSha256 = asciiKw Str.anomaSha256
kwAnomaResourceCommitment :: Keyword
kwAnomaResourceCommitment = asciiKw Str.anomaResourceCommitment
kwAnomaResourceNullifier :: Keyword
kwAnomaResourceNullifier = asciiKw Str.anomaResourceNullifier
kwAnomaResourceKind :: Keyword
kwAnomaResourceKind = asciiKw Str.anomaResourceKind
kwAnomaResourceDelta :: Keyword
kwAnomaResourceDelta = asciiKw Str.anomaResourceDelta
kwAnomaActionDelta :: Keyword
kwAnomaActionDelta = asciiKw Str.anomaActionDelta
kwAnomaActionsDelta :: Keyword
kwAnomaActionsDelta = asciiKw Str.anomaActionsDelta
kwAnomaProveAction :: Keyword
kwAnomaProveAction = asciiKw Str.anomaProveAction
kwAnomaProveDelta :: Keyword
kwAnomaProveDelta = asciiKw Str.anomaProveDelta
kwAnomaZeroDelta :: Keyword
kwAnomaZeroDelta = asciiKw Str.anomaZeroDelta
kwAnomaAddDelta :: Keyword
kwAnomaAddDelta = asciiKw Str.anomaAddDelta
kwAnomaSubDelta :: Keyword
kwAnomaSubDelta = asciiKw Str.anomaSubDelta
delimBraceL :: Keyword
delimBraceL = mkDelim Str.braceL

51
src/Juvix/Extra/Strings.hs
View File

@ -392,6 +392,45 @@ anomaByteArrayFromAnomaContents = "anoma-bytearray-from-anoma-contents"
anomaSha256 :: (IsString s) => s
anomaSha256 = "anoma-sha256"
anomaDelta :: (IsString s) => s
anomaDelta = "anoma-delta"
anomaKind :: (IsString s) => s
anomaKind = "anoma-kind"
anomaResourceCommitment :: (IsString s) => s
anomaResourceCommitment = "anoma-resource-commitment"
anomaResourceNullifier :: (IsString s) => s
anomaResourceNullifier = "anoma-resource-nullifier"
anomaResourceKind :: (IsString s) => s
anomaResourceKind = "anoma-resource-kind"
anomaResourceDelta :: (IsString s) => s
anomaResourceDelta = "anoma-resource-delta"
anomaActionDelta :: (IsString s) => s
anomaActionDelta = "anoma-action-delta"
anomaActionsDelta :: (IsString s) => s
anomaActionsDelta = "anoma-actions-delta"
anomaZeroDelta :: (IsString s) => s
anomaZeroDelta = "anoma-zero-delta"
anomaAddDelta :: (IsString s) => s
anomaAddDelta = "anoma-add-delta"
anomaSubDelta :: (IsString s) => s
anomaSubDelta = "anoma-sub-delta"
anomaProveDelta :: (IsString s) => s
anomaProveDelta = "anoma-prove-delta"
anomaProveAction :: (IsString s) => s
anomaProveAction = "anoma-prove-action"
builtinSeq :: (IsString s) => s
builtinSeq = "seq"
@ -1079,6 +1118,18 @@ cairoEcPoint = "ec_point"
cairoMkEcPoint :: (IsString s) => s
cairoMkEcPoint = "mkEcPoint"
anomaResource :: (IsString s) => s
anomaResource = "anoma-resource"
anomaAction :: (IsString s) => s
anomaAction = "anoma-action"
anomaMkResource :: (IsString s) => s
anomaMkResource = "mkResource"
anomaMkAction :: (IsString s) => s
anomaMkAction = "mkAction"
rustFn :: (IsString s) => s
rustFn = "fn"

12
test/Anoma/Compilation/Positive.hs
View File

@ -655,5 +655,17 @@ allTests =
64
5092006196359674779938793937035252249221936503860319648757996882954518215195609232852607160812968472040491493412050369557521935588220586883008001462395444
] |]
],
mkAnomaCallTest
"Test085: Anoma Resource Machine builtins"
$(mkRelDir ".")
$(mkRelFile "test085.juvix")
[]
$ checkOutput
[ [nock| [[[11 22] 110] 0] |],
[nock| [10 11] |],
[nock| 478793196187462788804451 |],
[nock| 418565088612 |],
[nock| 0 |]
]
]

98
tests/Anoma/Compilation/positive/test085.juvix Normal file
View File

@ -0,0 +1,98 @@
module test085;
import Stdlib.Prelude open;
import Stdlib.Debug.Trace open;
-- This definition does not match the spec. For testing purposes only
builtin anoma-resource
type Resource :=
mkResource@{
label : Nat;
logic : Nat;
ephemeral : Bool;
quantity : Nat;
data : Pair Nat Nat;
nullifier-key : Nat;
nonce : Nat;
rseed : Nat
};
mkResource' (label logic : Nat) {quantity : Nat := 0} : Resource :=
mkResource@{
label;
logic;
ephemeral := false;
quantity;
data := 0, 0;
nullifier-key := 0;
nonce := 0;
rseed := 0
};
-- This definition does not match the spec. For testing purposes only
builtin anoma-action
type Action := mkAction Nat;
builtin anoma-delta
axiom Delta : Type;
builtin anoma-kind
axiom Kind : Type;
builtin anoma-resource-commitment
axiom commitment : Resource -> Nat;
builtin anoma-resource-nullifier
axiom nullifier : Resource -> Nat;
builtin anoma-resource-kind
axiom kind : Resource -> Kind;
builtin anoma-resource-delta
axiom resourceDelta : Resource -> Delta;
builtin anoma-action-delta
axiom actionDelta : Action -> Delta;
builtin anoma-actions-delta
axiom actionsDelta : List Action -> Delta;
builtin anoma-prove-action
axiom proveAction : Action -> Nat;
builtin anoma-prove-delta
axiom proveDelta : Delta -> Nat;
builtin anoma-zero-delta
axiom zeroDelta : Delta;
builtin anoma-add-delta
axiom addDelta : Delta -> Delta -> Delta;
builtin anoma-sub-delta
axiom subDelta : Delta -> Delta -> Delta;
main : Delta :=
trace
(resourceDelta
mkResource'@{
label := 11;
logic := 22;
quantity := 55
})
-- commitment is too slow to be tested
-- >-> trace (commitment (mkResource' 0 0))
-- nullifier is too slow to be tested
-- >-> trace (nullifier (mkResource' 0 0))
-- actionDelta is a crash in the nock library so cannot be tested
-- >-> trace (actionDelta (mkAction 0))
-- actionsDelta is a crash in the nock library so cannot be tested
-- >-> trace (actionsDelta [mkAction 0])
-- addDelta is a crash in the nock library so cannot be tested
-- >-> trace (addDelta zeroDelta zeroDelta)
-- subDelta is a crash in the nock library so cannot be tested
-- >-> trace (subDelta zeroDelta zeroDelta)
>-> trace (kind (mkResource' 10 11))
>-> trace (proveAction (mkAction 0))
>-> trace (proveDelta zeroDelta)
>-> zeroDelta;