From 7d1c6a453648ed95ed35bad4b0e788a14e543559 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 29 Jan 2025 17:13:48 +0000 Subject: [PATCH] Add support for AnomaSet and AnomaSet{to, from}List (#3296) This PR adds support for the `AnomaSet` type and related builtins: ``` builtin anoma-set axiom AnomaSet : Type -> Type; builtin anoma-set-to-list axiom anomaSetToList {A} (set : AnomaSet A) : List A; builtin anoma-set-from-list axiom anomaSetFromList {A} (list : List A) : AnomaSet A; ``` These builtins require an Anoma node ref update, specifically `5c7bd8121206fbebdc3f7f75fdea3697f09566a0` because of a bug in Anoma node related to handling of Nock list -> Elixir list transformations. see: * https://github.com/anoma/anoma/pull/1832 --- .github/workflows/ci.yml | 2 +- src/Juvix/Compiler/Builtins/Anoma.hs | 32 +++++++++++++++++++ src/Juvix/Compiler/Concrete/Data/Builtins.hs | 9 ++++++ src/Juvix/Compiler/Core/Evaluator.hs | 2 ++ src/Juvix/Compiler/Core/Extra/Utils.hs | 4 +++ src/Juvix/Compiler/Core/Keywords.hs | 2 ++ src/Juvix/Compiler/Core/Language/Builtins.hs | 10 +++++- src/Juvix/Compiler/Core/Pretty/Base.hs | 8 +++++ .../Core/Transformation/ComputeTypeInfo.hs | 2 ++ .../Compiler/Core/Translation/FromInternal.hs | 25 +++++++++++++++ .../Compiler/Core/Translation/FromSource.hs | 2 ++ .../Core/Translation/Stripped/FromCore.hs | 3 ++ .../Internal/Translation/FromConcrete.hs | 3 ++ src/Juvix/Compiler/Nockma/AnomaLib.hs | 6 ++++ src/Juvix/Compiler/Nockma/AnomaLib/Base.hs | 4 +++ src/Juvix/Compiler/Nockma/Evaluator.hs | 23 ++++++++++++- .../Compiler/Nockma/Translation/FromTree.hs | 8 +++++ src/Juvix/Compiler/Tree/Keywords.hs | 2 ++ src/Juvix/Compiler/Tree/Language/Builtins.hs | 2 ++ src/Juvix/Compiler/Tree/Pretty/Base.hs | 2 ++ .../Compiler/Tree/Translation/FromCore.hs | 2 ++ .../Compiler/Tree/Translation/FromSource.hs | 2 ++ src/Juvix/Data/Keyword/All.hs | 6 ++++ src/Juvix/Extra/Strings.hs | 9 ++++++ test/Anoma/Compilation/Positive.hs | 13 +++++++- .../Anoma/Compilation/positive/test087.juvix | 14 ++++++++ 26 files changed, 193 insertions(+), 4 deletions(-) create mode 100644 tests/Anoma/Compilation/positive/test087.juvix diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 979ceec3d2..1254a8d033 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -28,7 +28,7 @@ env: RISC0_VM_VERSION: v1.0.1 # This is the top commit hash in the branch paul/juvix-ci-stable # of the anoma repository. - ANOMA_VERSION: 8cc25d3fd64ad20623c8135eaa0a6d2096016549 + ANOMA_VERSION: 5c7bd8121206fbebdc3f7f75fdea3697f09566a0 JUST_ARGS: runtimeCcArg=$CC runtimeLibtoolArg=$LIBTOOL STACK_BUILD_ARGS: --pedantic -j4 --ghc-options=-j diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index 5b802fc27f..2ff184f82e 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -267,3 +267,35 @@ checkAnomaIsNullifier f = do bool_ <- getBuiltinNameScoper l BuiltinBool unless (f ^. axiomType == (nat_ --> bool_)) $ builtinsErrorText l "isNullifier must be of type Nat -> Bool" + +checkAnomaSet :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r () +checkAnomaSet t = do + let ty = t ^. axiomType + l = getLoc t + u = ExpressionUniverse smallUniverseNoLoc + unless (ty == (u --> u)) $ + builtinsErrorText l "AnomaSet should have type: Type -> Type" + +checkAnomaSetToList :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r () +checkAnomaSetToList f = do + let ty = f ^. axiomType + u = ExpressionUniverse smallUniverseNoLoc + l = getLoc f + elemT <- freshVar l "elemT" + list_ <- getBuiltinNameScoper l BuiltinList + anomaSet <- getBuiltinNameScoper l BuiltinAnomaSet + let freeVars = HashSet.fromList [elemT] + unless ((ty ==% (u <>--> anomaSet @@ elemT --> list_ @@ elemT)) freeVars) $ + builtinsErrorText l "anomaSetToList should have type: {A : Type} -> AnomaSet A -> List A" + +checkAnomaSetFromList :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r () +checkAnomaSetFromList f = do + let ty = f ^. axiomType + u = ExpressionUniverse smallUniverseNoLoc + l = getLoc f + elemT <- freshVar l "elemT" + list_ <- getBuiltinNameScoper l BuiltinList + anomaSet <- getBuiltinNameScoper l BuiltinAnomaSet + let freeVars = HashSet.fromList [elemT] + unless ((ty ==% (u <>--> list_ @@ elemT --> anomaSet @@ elemT)) freeVars) $ + builtinsErrorText l "anomaSetFromList should have type: {A : Type} -> List A -> AnomaSet A" diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 0e5aed62ad..33164e873f 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -280,6 +280,9 @@ data BuiltinAxiom | BuiltinAnomaRandomSplit | BuiltinAnomaIsCommitment | BuiltinAnomaIsNullifier + | BuiltinAnomaSet + | BuiltinAnomaSetToList + | BuiltinAnomaSetFromList | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint @@ -356,6 +359,9 @@ instance HasNameKind BuiltinAxiom where BuiltinByteArray -> KNameInductive BuiltinByteArrayFromListByte -> KNameFunction BuiltinByteArrayLength -> KNameFunction + BuiltinAnomaSet -> KNameInductive + BuiltinAnomaSetToList -> KNameInductive + BuiltinAnomaSetFromList -> KNameInductive getNameKindPretty :: BuiltinAxiom -> NameKind getNameKindPretty = getNameKind @@ -419,6 +425,9 @@ instance Pretty BuiltinAxiom where BuiltinAnomaRandomSplit -> Str.anomaRandomSplit BuiltinAnomaIsCommitment -> Str.anomaIsCommitment BuiltinAnomaIsNullifier -> Str.anomaIsNullifier + BuiltinAnomaSet -> Str.anomaSet + BuiltinAnomaSetToList -> Str.anomaSetToList + BuiltinAnomaSetFromList -> Str.anomaSetFromList BuiltinPoseidon -> Str.cairoPoseidon BuiltinEcOp -> Str.cairoEcOp BuiltinRandomEcPoint -> Str.cairoRandomEcPoint diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 95dbd24689..bb787ed883 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -244,6 +244,8 @@ geval opts herr tab env0 = eval' env0 OpAnomaRandomSplit -> normalizeOrUnsupported opcode OpAnomaIsCommitment -> normalizeOrUnsupported opcode OpAnomaIsNullifier -> normalizeOrUnsupported opcode + OpAnomaSetToList -> normalizeOrUnsupported opcode + OpAnomaSetFromList -> normalizeOrUnsupported opcode OpPoseidonHash -> poseidonHashOp OpEc -> ecOp OpRandomEcPoint -> randomEcPointOp diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index 720d736bf9..f57e55efa8 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -235,6 +235,8 @@ isDebugOp = \case OpAnomaRandomSplit -> False OpAnomaIsCommitment -> False OpAnomaIsNullifier -> False + OpAnomaSetToList -> False + OpAnomaSetFromList -> False OpEc -> False OpFieldAdd -> False OpFieldDiv -> False @@ -538,6 +540,8 @@ builtinOpArgTypes = \case OpAnomaRandomSplit -> [mkTypeRandomGenerator'] OpAnomaIsCommitment -> [mkTypeInteger'] OpAnomaIsNullifier -> [mkTypeInteger'] + OpAnomaSetToList -> [mkDynamic'] + OpAnomaSetFromList -> [mkDynamic'] OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] OpRandomEcPoint -> [] diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs index 083dcf764d..53044824fe 100644 --- a/src/Juvix/Compiler/Core/Keywords.hs +++ b/src/Juvix/Compiler/Core/Keywords.hs @@ -24,6 +24,8 @@ import Juvix.Data.Keyword.All kwAnomaResourceDelta, kwAnomaResourceKind, kwAnomaResourceNullifier, + kwAnomaSetFromList, + kwAnomaSetToList, kwAnomaSha256, kwAnomaSign, kwAnomaSignDetached, diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index a8b0de4bb6..8e04c2b4f5 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -56,6 +56,8 @@ data BuiltinOp | OpAnomaRandomSplit | OpAnomaIsCommitment | OpAnomaIsNullifier + | OpAnomaSetToList + | OpAnomaSetFromList | OpPoseidonHash | OpEc | OpRandomEcPoint @@ -146,6 +148,8 @@ builtinOpArgsNum = \case OpAnomaRandomSplit -> 1 OpAnomaIsCommitment -> 1 OpAnomaIsNullifier -> 1 + OpAnomaSetToList -> 1 + OpAnomaSetFromList -> 1 OpPoseidonHash -> 1 OpEc -> 3 OpRandomEcPoint -> 0 @@ -213,6 +217,8 @@ builtinIsFoldable = \case OpAnomaRandomSplit -> False OpAnomaIsCommitment -> False OpAnomaIsNullifier -> False + OpAnomaSetToList -> False + OpAnomaSetFromList -> False OpPoseidonHash -> False OpEc -> False OpRandomEcPoint -> False @@ -252,7 +258,9 @@ builtinsAnoma = OpAnomaSubDelta, OpAnomaRandomGeneratorInit, OpAnomaRandomNextBytes, - OpAnomaRandomSplit + OpAnomaRandomSplit, + OpAnomaSetToList, + OpAnomaSetFromList ] builtinsUInt8 :: [BuiltinOp] diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 7802c862bb..29f62ed48e 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -80,6 +80,8 @@ instance PrettyCode BuiltinOp where OpAnomaRandomSplit -> return primRandomSplit OpAnomaIsCommitment -> return primIsCommitment OpAnomaIsNullifier -> return primIsNullifier + OpAnomaSetToList -> return primAnomaSetToList + OpAnomaSetFromList -> return primAnomaSetFromList OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc OpRandomEcPoint -> return primRandomEcPoint @@ -1023,6 +1025,12 @@ primIsCommitment = primitive Str.anomaIsCommitment primIsNullifier :: Doc Ann primIsNullifier = primitive Str.anomaIsNullifier +primAnomaSetToList :: Doc Ann +primAnomaSetToList = primitive Str.anomaSetToList + +primAnomaSetFromList :: Doc Ann +primAnomaSetFromList = primitive Str.anomaSetFromList + primPoseidonHash :: Doc Ann primPoseidonHash = primitive Str.cairoPoseidon diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 2a070c30d2..654c8dd7d4 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -105,6 +105,8 @@ computeNodeTypeInfo md = umapL go OpAnomaRandomSplit -> mkDynamic' OpAnomaIsCommitment -> mkTypeBool' OpAnomaIsNullifier -> mkTypeBool' + OpAnomaSetToList -> mkDynamic' + OpAnomaSetFromList -> mkDynamic' OpPoseidonHash -> case _builtinAppArgs of [arg] -> Info.getNodeType arg _ -> error "incorrect poseidon builtin application" diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 4a3e088500..c015cd6c1f 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -674,6 +674,9 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinAnomaRandomSplit -> return () Internal.BuiltinAnomaIsCommitment -> return () Internal.BuiltinAnomaIsNullifier -> return () + Internal.BuiltinAnomaSet -> registerInductiveAxiom (Just BuiltinAnomaSet) [] + Internal.BuiltinAnomaSetToList -> return () + Internal.BuiltinAnomaSetFromList -> return () Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () @@ -1003,6 +1006,25 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) natType (mkBuiltinApp' OpAnomaIsNullifier [mkVar' 0]) ) + Internal.BuiltinAnomaSet -> return () + Internal.BuiltinAnomaSetToList -> do + registerAxiomDef + ( mkLambda' + mkSmallUniv + ( mkLambda' + mkDynamic' + (mkBuiltinApp' OpAnomaSetToList [mkVar' 0]) + ) + ) + Internal.BuiltinAnomaSetFromList -> do + registerAxiomDef + ( mkLambda' + mkSmallUniv + ( mkLambda' + mkDynamic' + (mkBuiltinApp' OpAnomaSetFromList [mkVar' 0]) + ) + ) Internal.BuiltinPoseidon -> do psName <- getPoseidonStateName psSym <- getPoseidonStateSymbol @@ -1460,6 +1482,9 @@ goApplication a = do Just Internal.BuiltinAnomaRandomSplit -> app Just Internal.BuiltinAnomaIsCommitment -> app Just Internal.BuiltinAnomaIsNullifier -> app + Just Internal.BuiltinAnomaSet -> app + Just Internal.BuiltinAnomaSetToList -> app + Just Internal.BuiltinAnomaSetFromList -> app Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index 893a61a2d9..64e931f8b3 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -601,6 +601,8 @@ builtinAppExpr varsNum vars = do <|> (kw kwAnomaRandomSplit $> OpAnomaRandomSplit) <|> (kw kwAnomaIsCommitment $> OpAnomaIsCommitment) <|> (kw kwAnomaIsNullifier $> OpAnomaIsNullifier) + <|> (kw kwAnomaSetToList $> OpAnomaSetToList) + <|> (kw kwAnomaSetFromList $> OpAnomaSetFromList) args <- P.many (atom varsNum vars) return $ mkBuiltinApp' op args diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 7f4ef11dd3..cd33b28da4 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -138,6 +138,9 @@ fromCore fsize tab = BuiltinAnomaRandomSplit -> False BuiltinAnomaIsCommitment -> False BuiltinAnomaIsNullifier -> False + BuiltinAnomaSet -> False + BuiltinAnomaSetToList -> False + BuiltinAnomaSetFromList -> False BuiltinPoseidon -> False BuiltinEcOp -> False BuiltinRandomEcPoint -> False diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index cebf8097b7..87307ffc2a 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -1143,6 +1143,9 @@ checkBuiltinAxiom d b = localBuiltins $ case b of BuiltinAnomaRandomSplit -> checkAnomaRandomSplit d BuiltinAnomaIsCommitment -> checkAnomaIsCommitment d BuiltinAnomaIsNullifier -> checkAnomaIsNullifier d + BuiltinAnomaSet -> checkAnomaSet d + BuiltinAnomaSetToList -> checkAnomaSetToList d + BuiltinAnomaSetFromList -> checkAnomaSetFromList d BuiltinPoseidon -> checkPoseidon d BuiltinEcOp -> checkEcOp d BuiltinRandomEcPoint -> checkRandomEcPoint d diff --git a/src/Juvix/Compiler/Nockma/AnomaLib.hs b/src/Juvix/Compiler/Nockma/AnomaLib.hs index 61ada2248c..c24b49b2fe 100644 --- a/src/Juvix/Compiler/Nockma/AnomaLib.hs +++ b/src/Juvix/Compiler/Nockma/AnomaLib.hs @@ -104,6 +104,12 @@ anomaLibPath = \case -- -- => rm != |= [rng=*] split:`_og`rng StdlibRandomSplit -> [nock| [8 [1 0] [1 7 [0 6] 9 21 0 1] 0 1] |] + -- obtained from the urbit dojo using: + -- + -- => rm != |= a=(set) ~(tap in a) + StdlibAnomaSetToList -> [nock| [8 [1 0] [1 8 [9 21 0 31] 9 186 10 [6 0 14] 0 2] 0 1] |] + -- called silt in hoon + StdlibAnomaSetFromList -> [nock| [9 22 0 7] |] AnomaLibFunction (AnomaRmFunction f) -> case f of RmCommit -> [nock| [9 94 0 1] |] RmNullify -> [nock| [9 350 0 1] |] diff --git a/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs b/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs index 9865eea7e7..7f8febdc94 100644 --- a/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs +++ b/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs @@ -37,6 +37,8 @@ data StdlibFunction | StdlibRandomInitGen | StdlibRandomNextBytes | StdlibRandomSplit + | StdlibAnomaSetToList + | StdlibAnomaSetFromList deriving stock (Show, Lift, Eq, Bounded, Enum, Generic) instance Hashable StdlibFunction @@ -116,6 +118,8 @@ instance Pretty StdlibFunction where StdlibRandomInitGen -> "random-init" StdlibRandomNextBytes -> "random-next-bytes" StdlibRandomSplit -> "random-split" + StdlibAnomaSetToList -> "set-to-list" + StdlibAnomaSetFromList -> "set-from-list" instance Pretty RmFunction where pretty = \case diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs index fd5d39e3c6..60ae68b4c5 100644 --- a/src/Juvix/Compiler/Nockma/Evaluator.hs +++ b/src/Juvix/Compiler/Nockma/Evaluator.hs @@ -177,7 +177,19 @@ eval initstack initterm = ignoreOpCounts (evalProfile initstack initterm) evalProfile :: forall s a. - (Hashable a, Integral a, Members '[Reader (Storage a), State OpCounts, Reader EvalOptions, Output (Term a), Error (NockEvalError a), Error (ErrNockNatural a)] s, NockNatural a) => + ( Hashable a, + Integral a, + Members + '[ Reader (Storage a), + State OpCounts, + Reader EvalOptions, + Output (Term a), + Error (NockEvalError a), + Error (ErrNockNatural a) + ] + s, + NockNatural a + ) => Term a -> Term a -> Sem s (Term a) @@ -284,7 +296,16 @@ evalProfile inistack initerm = TermCell (Cell g (TermAtom n)) -> goRandomNextBytes n g _ -> error "StdlibRandomNextBytes must be called with a cell containing an atom and a term" StdlibRandomSplit -> goRandomSplit args' + StdlibAnomaSetFromList -> return (goAnomaSetFromList args') + StdlibAnomaSetToList -> return args' where + goAnomaSetFromList :: Term a -> Term a + goAnomaSetFromList arg = + foldr + (\t acc -> TermCell (Cell' t acc emptyCellInfo)) + (TermAtom nockNil) + (nubHashable (checkTermToList arg)) + serializeSMGen :: R.SMGen -> Term a serializeSMGen s = let (seed, gamma) = R.unseedSMGen s diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index 33520aa426..6d262295be 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -563,6 +563,8 @@ compile = \case Tree.OpAnomaRandomSplit -> callStdlib StdlibRandomSplit args Tree.OpAnomaIsCommitment -> callRm RmIsCommitment args Tree.OpAnomaIsNullifier -> callRm RmIsNullifier args + Tree.OpAnomaSetToList -> goAnomaSetToList args + Tree.OpAnomaSetFromList -> goAnomaSetFromList args goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural) goByteArrayOp Tree.NodeByteArray {..} = do @@ -680,6 +682,12 @@ compile = \case [len, contents] -> mkByteArray len contents _ -> impossible + goAnomaSetToList :: [Term Natural] -> Sem r (Term Natural) + goAnomaSetToList arg = callStdlib StdlibAnomaSetToList arg + + goAnomaSetFromList :: [Term Natural] -> Sem r (Term Natural) + goAnomaSetFromList arg = callStdlib StdlibAnomaSetFromList arg + goAnomaSha256 :: [Term Natural] -> Sem r (Term Natural) goAnomaSha256 arg = do stdcall <- callStdlib StdlibSha256 arg diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs index c8b4379070..cfcab3d7cf 100644 --- a/src/Juvix/Compiler/Tree/Keywords.hs +++ b/src/Juvix/Compiler/Tree/Keywords.hs @@ -28,6 +28,8 @@ import Juvix.Data.Keyword.All kwAnomaResourceDelta, kwAnomaResourceKind, kwAnomaResourceNullifier, + kwAnomaSetFromList, + kwAnomaSetToList, kwAnomaSha256, kwAnomaSign, kwAnomaSignDetached, diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index b06263e1a9..dc6bcee47a 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -134,4 +134,6 @@ data AnomaOp OpAnomaIsCommitment | -- | Returns true if its argument is a nullifier OpAnomaIsNullifier + | OpAnomaSetToList + | OpAnomaSetFromList deriving stock (Eq, Show) diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index 44f54c4c80..b625b97a9a 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -305,6 +305,8 @@ instance PrettyCode AnomaOp where OpAnomaRandomSplit -> Str.anomaRandomSplit OpAnomaIsCommitment -> Str.anomaIsCommitment OpAnomaIsNullifier -> Str.anomaIsNullifier + OpAnomaSetToList -> Str.anomaSetToList + OpAnomaSetFromList -> Str.anomaSetFromList instance PrettyCode UnaryOpcode where ppCode = \case diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index 48ea1f4c24..e8f41766e6 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -75,6 +75,8 @@ toTreeOp = \case Core.OpAnomaRandomSplit -> TreeAnomaOp OpAnomaRandomSplit Core.OpAnomaIsCommitment -> TreeAnomaOp OpAnomaIsCommitment Core.OpAnomaIsNullifier -> TreeAnomaOp OpAnomaIsNullifier + Core.OpAnomaSetToList -> TreeAnomaOp OpAnomaSetToList + Core.OpAnomaSetFromList -> TreeAnomaOp OpAnomaSetFromList -- TreeCairoOp Core.OpPoseidonHash -> TreeCairoOp OpCairoPoseidon Core.OpEc -> TreeCairoOp OpCairoEc diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs index 2bab7573a8..e52a1ff781 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs @@ -172,6 +172,8 @@ parseAnoma = <|> parseAnoma' kwAnomaRandomSplit OpAnomaRandomSplit <|> parseAnoma' kwAnomaIsCommitment OpAnomaIsCommitment <|> parseAnoma' kwAnomaIsNullifier OpAnomaIsNullifier + <|> parseAnoma' kwAnomaSetToList OpAnomaSetToList + <|> parseAnoma' kwAnomaSetFromList OpAnomaSetFromList parseAnoma' :: (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) => diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index 95ae770655..a8b9ba724e 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -580,6 +580,12 @@ kwAnomaIsCommitment = asciiKw Str.anomaIsCommitment kwAnomaIsNullifier :: Keyword kwAnomaIsNullifier = asciiKw Str.anomaIsNullifier +kwAnomaSetToList :: Keyword +kwAnomaSetToList = asciiKw Str.anomaSetToList + +kwAnomaSetFromList :: Keyword +kwAnomaSetFromList = asciiKw Str.anomaSetFromList + delimBraceL :: Keyword delimBraceL = mkDelim Str.braceL diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 239908a262..a6f48dcd8b 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -452,6 +452,15 @@ anomaIsCommitment = "anoma-is-commitment" anomaIsNullifier :: (IsString s) => s anomaIsNullifier = "anoma-is-nullifier" +anomaSet :: (IsString s) => s +anomaSet = "anoma-set" + +anomaSetToList :: (IsString s) => s +anomaSetToList = "anoma-set-to-list" + +anomaSetFromList :: (IsString s) => s +anomaSetFromList = "anoma-set-from-list" + builtinSeq :: (IsString s) => s builtinSeq = "seq" diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index b4ad6a7b66..ee7aa47924 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -233,6 +233,7 @@ classify AnomaTest {..} = case _anomaTestNum of 84 -> ClassWorking 85 -> ClassWorking 86 -> ClassExpectedFail + 87 -> ClassWorking _ -> error "non-exhaustive test classification" allTests :: TestTree @@ -1041,5 +1042,15 @@ allTests = [nock| [3 10689019] |], [nock| [2 20159] |], [nock| [4 4187579825] |] - ] + ], + let testList :: Term Natural = [nock| [1 2 nil] |] + expectedOutput :: Term Natural = [nock| [2 1 nil] |] + in mkAnomaTest + 87 + AnomaTestModeNodeOnly + "AnomaSet" + $(mkRelDir ".") + $(mkRelFile "test087.juvix") + [testList] + $ checkOutput [expectedOutput] ] diff --git a/tests/Anoma/Compilation/positive/test087.juvix b/tests/Anoma/Compilation/positive/test087.juvix new file mode 100644 index 0000000000..48b832966c --- /dev/null +++ b/tests/Anoma/Compilation/positive/test087.juvix @@ -0,0 +1,14 @@ +module test087; + +import Stdlib.Prelude open; + +builtin anoma-set +axiom AnomaSet : Type -> Type; + +builtin anoma-set-to-list +axiom anomaSetToList {A} (set : AnomaSet A) : List A; + +builtin anoma-set-from-list +axiom anomaSetFromList {A} (list : List A) : AnomaSet A; + +main (xs : List Nat) : List Nat := anomaSetToList (anomaSetFromList xs);