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:

* anoma/anoma#1832

.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
 

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"

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

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

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 -> []

src/Juvix/Compiler/Core/Keywords.hs

@@ -24,6 +24,8 @@ import Juvix.Data.Keyword.All
     kwAnomaResourceDelta,
     kwAnomaResourceKind,
     kwAnomaResourceNullifier,
+    kwAnomaSetFromList,
+    kwAnomaSetToList,
     kwAnomaSha256,
     kwAnomaSign,
     kwAnomaSignDetached,

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]

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
 

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"

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

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

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

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

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] |]

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

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

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

src/Juvix/Compiler/Tree/Keywords.hs

@@ -28,6 +28,8 @@ import Juvix.Data.Keyword.All
     kwAnomaResourceDelta,
     kwAnomaResourceKind,
     kwAnomaResourceNullifier,
+    kwAnomaSetFromList,
+    kwAnomaSetToList,
     kwAnomaSha256,
     kwAnomaSign,
     kwAnomaSignDetached,

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)

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

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

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) =>