Add support for anoma specific functions to the Core evaluator (#2851)

This PR adds support for the `anoma{encode, decode, sign, verify,
signDetached, verifyDetached}` functions to the Core evaluator.

## Encoding / Decoding

The serialization of values to `ByteString` for `anomaEncode` reuses the
Stored Core serialization. The Stored Core `Node` is extended to include
closures.

Anoma expects encoding of bytes as little-endian integers. In general
`ByteString -> Integer` is ambiguous because two `ByteString`s that
differ only by zero padding will map to the same integer. So we must
encode the length of the ByteString in the encoded integer alongside the
ByteString data so when it is decoded we can pad appropriately. We use
the same length encoding scheme that is used by Nockma jam.

## Verify

The Core evaluator implementation of `anomaVerify` crashes if the
verification fails. This matches the behaviour of Anoma node.

### `jvc` Support

You can now use `anoma-*` functions within `.jvc` core files.

* Closes https://github.com/anoma/juvix/issues/2808

src/Juvix/Compiler/Core/Evaluator.hs

@@ -1,7 +1,9 @@
 module Juvix.Compiler.Core.Evaluator where
 
 import Control.Exception qualified as Exception
+import Crypto.Sign.Ed25519 qualified as E
 import Data.HashMap.Strict qualified as HashMap
+import Data.Serialize qualified as S
 import GHC.Base (seq)
 import GHC.Conc qualified as GHC
 import GHC.IO (unsafePerformIO)
@@ -12,6 +14,9 @@ import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo
 import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Nockma.Encoding qualified as Encoding
+import Juvix.Compiler.Nockma.Encoding.Ed25519 qualified as E
+import Juvix.Compiler.Store.Core.Extra qualified as Store
 import Juvix.Data.Field
 import Text.Read qualified as T
 
@@ -345,56 +350,73 @@ geval opts herr ctx env0 = eval' env0
 
         anomaEncodeOp :: [Node] -> Node
         anomaEncodeOp = unary $ \arg ->
-          if
-              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
-                  mkBuiltinApp' OpAnomaEncode [eval' env arg]
-              | otherwise ->
-                  err "unsupported builtin operation: OpAnomaEncode"
+          let !v = eval' env arg
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaEncode [v]
+                  | otherwise -> nodeFromInteger (serializeToInteger v)
         {-# INLINE anomaEncodeOp #-}
 
         anomaDecodeOp :: [Node] -> Node
         anomaDecodeOp = unary $ \arg ->
-          if
-              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
-                  mkBuiltinApp' OpAnomaDecode [eval' env arg]
-              | otherwise ->
-                  err "unsupported builtin operation: OpAnomaDecode"
+          let !v = eval' env arg
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaDecode [v]
+                  | otherwise -> case integerFromNode v of
+                      Just i -> deserializeFromInteger i
+                      Nothing -> err "anomaDecodeOp: argument not an integer"
         {-# INLINE anomaDecodeOp #-}
 
         anomaVerifyDetachedOp :: [Node] -> Node
         anomaVerifyDetachedOp = checkApply $ \arg1 arg2 arg3 ->
-          if
-              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
-                  mkBuiltinApp' OpAnomaVerifyDetached (eval' env <$> [arg1, arg2, arg3])
-              | otherwise ->
-                  err "unsupported builtin operation: OpAnomaVerifyDetached"
+          let !v1 = eval' env arg1
+              !v2 = eval' env arg2
+              !v3 = eval' env arg3
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaVerifyDetached [v1, v2, v3]
+                  | otherwise ->
+                      case (integerFromNode v1, integerFromNode v3) of
+                        (Just i1, Just i3) -> verifyDetached i1 v2 i3
+                        _ -> err "OpAnomaVerifyDetached: first and third arguments must be integers"
         {-# INLINE anomaVerifyDetachedOp #-}
 
         anomaSignOp :: [Node] -> Node
         anomaSignOp = checkApply $ \arg1 arg2 ->
-          if
-              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
-                  mkBuiltinApp' OpAnomaSign (eval' env <$> [arg1, arg2])
-              | otherwise ->
-                  err "unsupported builtin operation: OpAnomaSign"
+          let !v1 = eval' env arg1
+              !v2 = eval' env arg2
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaSign [v1, v2]
+                  | otherwise -> case integerFromNode v2 of
+                      Just i -> sign v1 i
+                      Nothing -> err "anomaSignOp: second argument not an integer"
         {-# INLINE anomaSignOp #-}
 
         anomaSignDetachedOp :: [Node] -> Node
         anomaSignDetachedOp = checkApply $ \arg1 arg2 ->
-          if
-              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
-                  mkBuiltinApp' OpAnomaSignDetached (eval' env <$> [arg1, arg2])
-              | otherwise ->
-                  err "unsupported builtin operation: OpAnomaSignDetached"
+          let !v1 = eval' env arg1
+              !v2 = eval' env arg2
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaSignDetached [v1, v2]
+                  | otherwise -> case integerFromNode v2 of
+                      Just i -> signDetached v1 i
+                      Nothing -> err "anomaSignDetachedOp: second argument not an integer"
         {-# INLINE anomaSignDetachedOp #-}
 
         anomaVerifyOp :: [Node] -> Node
         anomaVerifyOp = checkApply $ \arg1 arg2 ->
-          if
-              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
-                  mkBuiltinApp' OpAnomaVerify (eval' env <$> [arg1, arg2])
-              | otherwise ->
-                  err "unsupported builtin operation: OpAnomaVerify"
+          let !v1 = eval' env arg1
+              !v2 = eval' env arg2
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaVerify [v1, v2]
+                  | otherwise ->
+                      case (integerFromNode v1, integerFromNode v2) of
+                        (Just i1, Just i2) -> verify i1 i2
+                        _ -> err "anomaVerifyOp: both arguments are not integers"
         {-# INLINE anomaVerifyOp #-}
 
         poseidonHashOp :: [Node] -> Node
@@ -423,8 +445,75 @@ geval opts herr ctx env0 = eval' env0
           _ ->
             err "unsupported builtin operation: OpPoseidonHash"
         {-# INLINE randomEcPointOp #-}
+
+        -- Deserialize a Node that was serialized using `serializeNode`.
+        deserializeNode :: ByteString -> Node
+        deserializeNode = fromRight decodeErr . fmap (eval' env . Store.toCoreNode) . S.decode
+          where
+            decodeErr :: Node
+            decodeErr = err "failed to decode to Node"
+        {-# INLINE deserializeNode #-}
+
+        -- Deserialize a Integer, serialized using `serializeInteger` to a Node
+        deserializeFromInteger :: Integer -> Node
+        deserializeFromInteger = deserializeNode . decodeByteString
+        {-# INLINE deserializeFromInteger #-}
+
+        serializeToInteger :: Node -> Integer
+        serializeToInteger = Encoding.encodeByteString . serializeNode
+        {-# INLINE serializeToInteger #-}
+
+        decodeByteString :: Integer -> ByteString
+        decodeByteString = Encoding.decodeByteStringWithDefault decodeErr
+          where
+            decodeErr :: ByteString
+            decodeErr = err "failed to decode Integer"
+        {-# INLINE decodeByteString #-}
+
+        sign :: Node -> Integer -> Node
+        sign !messageNode !secretKeyInt =
+          let !message = serializeNode messageNode
+              !secretKey = secretKeyFromInteger secretKeyInt
+           in nodeFromInteger (Encoding.encodeByteString (E.sign secretKey message))
+        {-# INLINE sign #-}
+
+        verify :: Integer -> Integer -> Node
+        verify !signedMessageInt !publicKeyInt =
+          let !signedMessage = decodeByteString signedMessageInt
+              !publicKey = publicKeyFromInteger publicKeyInt
+           in if
+                  | E.verify publicKey signedMessage -> deserializeNode (E.removeSignature signedMessage)
+                  | otherwise -> err "signature verification failed"
+        {-# INLINE verify #-}
+
+        signDetached :: Node -> Integer -> Node
+        signDetached !messageNode !secretKeyInt =
+          let !message = serializeNode messageNode
+              !secretKey = secretKeyFromInteger secretKeyInt
+              (E.Signature !sig) = E.dsign secretKey message
+           in nodeFromInteger (Encoding.encodeByteString sig)
+        {-# INLINE signDetached #-}
+
+        verifyDetached :: Integer -> Node -> Integer -> Node
+        verifyDetached !signatureInt !messageNode !publicKeyInt =
+          let !sig = E.Signature (decodeByteString signatureInt)
+              !message = serializeNode messageNode
+              !publicKey = publicKeyFromInteger publicKeyInt
+           in nodeFromBool (E.dverify publicKey message sig)
+        {-# INLINE verifyDetached #-}
     {-# INLINE applyBuiltin #-}
 
+    -- secretKey, publicKey are not encoded with their length as
+    -- a bytestring in order to be compatible with Anoma sign. Therefore the
+    -- expected length of each must be specified.
+    secretKeyFromInteger :: Integer -> E.SecretKey
+    secretKeyFromInteger = E.SecretKey . Encoding.integerToByteStringLELen 64
+    {-# INLINE secretKeyFromInteger #-}
+
+    publicKeyFromInteger :: Integer -> E.PublicKey
+    publicKeyFromInteger = E.PublicKey . Encoding.integerToByteStringLELen 32
+    {-# INLINE publicKeyFromInteger #-}
+
     nodeFromInteger :: Integer -> Node
     nodeFromInteger !int = mkConstant' (ConstInteger int)
     {-# INLINE nodeFromInteger #-}
@@ -572,6 +661,9 @@ doEval mfsize noIO loc tab node
         (\fsize -> defaultEvalOptions {_evalOptionsFieldSize = fsize})
         mfsize
 
+serializeNode :: Node -> ByteString
+serializeNode = S.encode . Store.fromCoreNode . removeClosures
+
 doEvalIO ::
   Maybe Natural ->
   Bool ->

src/Juvix/Compiler/Core/Keywords.hs

@@ -8,6 +8,12 @@ where
 import Juvix.Data.Keyword
 import Juvix.Data.Keyword.All
   ( delimSemicolon,
+    kwAnomaDecode,
+    kwAnomaEncode,
+    kwAnomaSign,
+    kwAnomaSignDetached,
+    kwAnomaVerify,
+    kwAnomaVerifyDetached,
     kwAny,
     kwAssign,
     kwBind,

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -573,6 +573,12 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwPoseidon $> OpPoseidonHash)
       <|> (kw kwEcOp $> OpEc)
       <|> (kw kwRandomEcPoint $> OpRandomEcPoint)
+      <|> (kw kwAnomaEncode $> OpAnomaEncode)
+      <|> (kw kwAnomaDecode $> OpAnomaDecode)
+      <|> (kw kwAnomaSign $> OpAnomaSign)
+      <|> (kw kwAnomaVerify $> OpAnomaVerify)
+      <|> (kw kwAnomaSignDetached $> OpAnomaSignDetached)
+      <|> (kw kwAnomaVerifyDetached $> OpAnomaVerifyDetached)
   args <- P.many (atom varsNum vars)
   return $ mkBuiltinApp' op args
 

src/Juvix/Compiler/Nockma/Encoding/Base.hs

@@ -3,6 +3,7 @@ module Juvix.Compiler.Nockma.Encoding.Base where
 import Data.Bit as Bit
 import Data.Bits
 import Data.Vector.Unboxed qualified as U
+import Juvix.Compiler.Nockma.Encoding.Effect.BitReader
 import Juvix.Compiler.Nockma.Encoding.Effect.BitWriter
 import Juvix.Prelude.Base
 
@@ -44,3 +45,36 @@ safeNaturalToInt :: Natural -> Maybe Int
 safeNaturalToInt n
   | n > fromIntegral (maxBound :: Int) = Nothing
   | otherwise = Just (fromIntegral n)
+
+-- | Write the binary encoding of argument interpreted as a length to the output
+writeLength :: forall r. (Member BitWriter r) => Int -> Sem r ()
+writeLength len = do
+  let lenOfLen = finiteBitSize len - countLeadingZeros len
+  replicateM_ lenOfLen writeZero
+  writeOne
+  unless (lenOfLen == 0) (go len)
+  where
+    go :: Int -> Sem r ()
+    -- Exclude the most significant bit of the length
+    go l = unless (l == 1) $ do
+      writeBit (Bit (testBit l 0))
+      go (l `shiftR` 1)
+
+-- | Consume the encoded length from the input bits
+consumeLength :: forall r. (Members '[BitReader, Error BitReadError] r) => Sem r Int
+consumeLength = do
+  lenOfLen <- countBitsUntilOne
+  if
+      | lenOfLen == 0 -> return 0
+      | otherwise -> do
+          -- The most significant bit of the length is omitted
+          let lenBits = lenOfLen - 1
+          foldlM go (bit lenBits) [0 .. lenBits - 1]
+  where
+    go :: Int -> Int -> Sem r Int
+    go acc n = do
+      Bit b <- nextBit
+      return $
+        if
+            | b -> setBit acc n
+            | otherwise -> acc

src/Juvix/Compiler/Nockma/Encoding/ByteString.hs

@@ -1,8 +1,12 @@
 module Juvix.Compiler.Nockma.Encoding.ByteString where
 
+import Data.Bit
 import Data.Bits
 import Data.ByteString qualified as BS
 import Data.ByteString.Builder qualified as BS
+import Juvix.Compiler.Nockma.Encoding.Base
+import Juvix.Compiler.Nockma.Encoding.Effect.BitReader
+import Juvix.Compiler.Nockma.Encoding.Effect.BitWriter
 import Juvix.Compiler.Nockma.Language
 import Juvix.Prelude.Base
 
@@ -34,6 +38,9 @@ integerToByteStringLE = BS.toStrict . BS.toLazyByteString . go
       0 -> mempty
       n -> BS.word8 (fromIntegral n) <> go (n `shiftR` 8)
 
+integerToByteStringLELen :: Int -> Integer -> ByteString
+integerToByteStringLELen len = padByteString len . integerToByteStringLE
+
 textToNatural :: Text -> Natural
 textToNatural = byteStringToNatural . encodeUtf8
 
@@ -59,3 +66,27 @@ padByteString :: Int -> ByteString -> ByteString
 padByteString n bs
   | BS.length bs >= n = bs
   | otherwise = BS.append bs (BS.replicate (n - BS.length bs) 0)
+
+-- | encode a ByteString to an Integer with its length as part of the encoding.
+encodeByteString :: ByteString -> Integer
+encodeByteString = vectorBitsToInteger . run . execBitWriter . go
+  where
+    go :: ByteString -> Sem (BitWriter ': r) ()
+    go bs = do
+      let len = BS.length bs
+      writeLength len
+      writeByteString bs
+
+-- | decode a ByteString that was encoded using `encodeByteString`
+decodeByteString :: forall r. (Member (Error BitReadError) r) => Integer -> Sem r ByteString
+decodeByteString i = evalBitReader (integerToVectorBits i) go
+  where
+    go :: Sem (BitReader ': r) ByteString
+    go = do
+      len <- consumeLength
+      v <- consumeRemaining
+      return (padByteString len (cloneToByteString v))
+
+-- | decode a ByteString that was encoded using `encodeByteString` with a default that's used if decoding fails.
+decodeByteStringWithDefault :: ByteString -> Integer -> ByteString
+decodeByteStringWithDefault d = fromRight d . run . runErrorNoCallStack @BitReadError . decodeByteString

src/Juvix/Compiler/Nockma/Encoding/Cue.hs

@@ -1,7 +1,6 @@
 module Juvix.Compiler.Nockma.Encoding.Cue where
 
 import Data.Bit as Bit
-import Data.Bits
 import Juvix.Compiler.Nockma.Encoding.Base
 import Juvix.Compiler.Nockma.Encoding.Effect.BitReader
 import Juvix.Compiler.Nockma.Language
@@ -66,23 +65,8 @@ handleBitError :: (Member (Error DecodingError) r) => DecodingError -> Sem (Erro
 handleBitError e = mapError @_ @_ @BitReadError (const e)
 
 -- | Consume the encoded length from the input bits
-consumeLength :: forall r. (Members '[BitReader, Error DecodingError] r) => Sem r Int
-consumeLength = do
-  lenOfLen <- handleBitError DecodingErrorInvalidLength countBitsUntilOne
-  if
-      | lenOfLen == 0 -> return 0
-      | otherwise -> do
-          -- The most significant bit of the length is omitted
-          let lenBits = lenOfLen - 1
-          foldlM go (bit lenBits) [0 .. lenBits - 1]
-  where
-    go :: Int -> Int -> Sem r Int
-    go acc n = do
-      Bit b <- handleBitError DecodingErrorInvalidLength nextBit
-      return $
-        if
-            | b -> setBit acc n
-            | otherwise -> acc
+consumeLength' :: forall r. (Members '[BitReader, Error DecodingError] r) => Sem r Int
+consumeLength' = handleBitError DecodingErrorInvalidLength consumeLength
 
 -- | Consume a nock integer from the input bits
 consumeInteger ::
@@ -225,7 +209,7 @@ cueFromBitsSem = registerElementStart $ do
 
     consumeNatAtom :: Sem r (Atom Natural)
     consumeNatAtom = do
-      len <- consumeLength
+      len <- consumeLength'
       if
           | len == 0 -> return (Atom 0 emptyAtomInfo)
           | otherwise -> do
@@ -234,7 +218,7 @@ cueFromBitsSem = registerElementStart $ do
 
     consumeAtom :: Sem r (Atom a)
     consumeAtom = do
-      len <- consumeLength
+      len <- consumeLength'
       if
           | len == 0 -> do
               z <- fromNatural' @a 0

src/Juvix/Compiler/Nockma/Encoding/Effect/BitReader.hs

@@ -1,6 +1,7 @@
 module Juvix.Compiler.Nockma.Encoding.Effect.BitReader where
 
 import Data.Bit as Bit
+import Data.Vector.Generic qualified as V
 import Data.Vector.Unboxed qualified as U
 import Effectful (Eff)
 import Juvix.Prelude.Base
@@ -10,6 +11,7 @@ data BitReadError = BitReadErrorNoMoreBits
 data BitReader :: Effect where
   -- makeSem ''BitReader has a type error if Sem is used instead of Eff
   NextBit :: (Member (Error BitReadError) r) => BitReader (Eff r) Bit
+  ConsumeRemaining :: BitReader m (Bit.Vector Bit)
   GetCurrentPosition :: BitReader m Int
 
 makeSem ''BitReader
@@ -50,6 +52,10 @@ evalBitReader v = evalState (initReaderState v) . re
 re :: Sem (BitReader ': r) a -> Sem (State ReaderState ': r) a
 re = interpretTopH $ \env -> \case
   GetCurrentPosition -> gets (^. readerStateCurrentPos)
+  ConsumeRemaining -> do
+    pos <- gets (^. readerStateCurrentPos)
+    bits <- gets (^. readerStateBits)
+    modify' (set readerStateCurrentPos (V.length bits)) >> return (V.drop pos bits)
   NextBit -> do
     bits <- gets (^. readerStateBits)
     pos <- gets (^. readerStateCurrentPos)

src/Juvix/Compiler/Nockma/Encoding/Effect/BitWriter.hs

@@ -7,6 +7,7 @@ import VectorBuilder.Vector
 
 data BitWriter :: Effect where
   WriteBit :: Bit -> BitWriter m ()
+  WriteByteString :: ByteString -> BitWriter m ()
   GetCurrentPosition :: BitWriter m Int
 
 makeSem ''BitWriter
@@ -39,6 +40,7 @@ execBitWriter sem = do
 re :: Sem (BitWriter ': r) a -> Sem (State WriterState ': r) a
 re = interpretTop $ \case
   WriteBit b -> writeBit' b
+  WriteByteString bs -> writeByteString' bs
   GetCurrentPosition -> getCurrentPosition'
 
 writeBit' :: (Member (State WriterState) r) => Bit -> Sem r ()
@@ -47,5 +49,11 @@ writeBit' b = modify appendBit
     appendBit :: WriterState -> WriterState
     appendBit = over writerStateBuilder (<> Builder.singleton b)
 
+writeByteString' :: (Member (State WriterState) r) => ByteString -> Sem r ()
+writeByteString' bs = modify appendByteString
+  where
+    appendByteString :: WriterState -> WriterState
+    appendByteString = over writerStateBuilder (<> Builder.vector (cloneFromByteString bs))
+
 getCurrentPosition' :: (Member (State WriterState) r) => Sem r Int
 getCurrentPosition' = Builder.size <$> gets (^. writerStateBuilder)

src/Juvix/Compiler/Nockma/Encoding/Jam.hs

@@ -25,20 +25,6 @@ initJamState =
 
 makeLenses ''JamState
 
--- | Write the binary encoding of argument interpreted as a length to the output
-writeLength :: forall r. (Member BitWriter r) => Int -> Sem r ()
-writeLength len = do
-  let lenOfLen = finiteBitSize len - countLeadingZeros len
-  replicateM_ lenOfLen writeZero
-  writeOne
-  unless (lenOfLen == 0) (go len)
-  where
-    go :: Int -> Sem r ()
-    -- Exclude the most significant bit of the length
-    go l = unless (l == 1) $ do
-      writeBit (Bit (testBit l 0))
-      go (l `shiftR` 1)
-
 -- | Write the atom tag 0b0 to the output
 writeAtomTag :: (Member BitWriter r) => Sem r ()
 writeAtomTag = writeZero

src/Juvix/Compiler/Store/Core/Extra.hs

@@ -8,7 +8,7 @@ import Juvix.Compiler.Store.Core.Language
 toCore :: InfoTable -> Core.InfoTable
 toCore InfoTable {..} =
   Core.InfoTable
-    { _identContext = fmap goNode _identContext,
+    { _identContext = fmap toCoreNode _identContext,
       _identMap,
       _infoMain,
       _infoIdentifiers = fmap goIdentifierInfo _infoIdentifiers,
@@ -24,14 +24,14 @@ toCore InfoTable {..} =
     goIdentifierInfo :: IdentifierInfo -> Core.IdentifierInfo
     goIdentifierInfo IdentifierInfo {..} =
       Core.IdentifierInfo
-        { _identifierType = goNode _identifierType,
+        { _identifierType = toCoreNode _identifierType,
           ..
         }
 
     goInductiveInfo :: InductiveInfo -> Core.InductiveInfo
     goInductiveInfo InductiveInfo {..} =
       Core.InductiveInfo
-        { _inductiveKind = goNode _inductiveKind,
+        { _inductiveKind = toCoreNode _inductiveKind,
           _inductiveParams = map goParameterInfo _inductiveParams,
           ..
         }
@@ -39,63 +39,63 @@ toCore InfoTable {..} =
     goParameterInfo :: ParameterInfo -> Core.ParameterInfo
     goParameterInfo ParameterInfo {..} =
       Core.ParameterInfo
-        { _paramKind = goNode _paramKind,
+        { _paramKind = toCoreNode _paramKind,
           ..
         }
 
     goConstructorInfo :: ConstructorInfo -> Core.ConstructorInfo
     goConstructorInfo ConstructorInfo {..} =
       Core.ConstructorInfo
-        { _constructorType = goNode _constructorType,
+        { _constructorType = toCoreNode _constructorType,
           ..
         }
 
     goAxiomInfo :: AxiomInfo -> Core.AxiomInfo
     goAxiomInfo AxiomInfo {..} =
       Core.AxiomInfo
-        { _axiomType = goNode _axiomType,
+        { _axiomType = toCoreNode _axiomType,
           ..
         }
 
     goSpecialisationInfo :: SpecialisationInfo -> Core.SpecialisationInfo
     goSpecialisationInfo SpecialisationInfo {..} =
       Core.SpecialisationInfo
-        { _specSignature = first (map goNode) _specSignature,
+        { _specSignature = first (map toCoreNode) _specSignature,
           ..
         }
 
-    goNode :: Node -> Core.Node
-    goNode = \case
-      NVar Var {..} -> Core.mkVar' _varIndex
-      NIdt Ident {..} -> Core.mkIdent' _identSymbol
-      NCst Constant {..} -> Core.mkConstant' _constantValue
-      NApp App {..} -> Core.mkApp' (goNode _appLeft) (goNode _appRight)
-      NBlt BuiltinApp {..} -> Core.mkBuiltinApp' _builtinAppOp (map goNode _builtinAppArgs)
-      NCtr Constr {..} -> Core.mkConstr' _constrTag (map goNode _constrArgs)
-      NLam Lambda {..} -> Core.mkLambda mempty (goBinder _lambdaBinder) (goNode _lambdaBody)
-      NLet Let {..} -> Core.NLet $ Core.Let mempty (goLetItem _letItem) (goNode _letBody)
-      NRec LetRec {..} -> Core.NRec $ Core.LetRec mempty (fmap goLetItem _letRecValues) (goNode _letRecBody)
-      NCase Case {..} -> Core.mkCase' _caseInductive (goNode _caseValue) (map goCaseBranch _caseBranches) (fmap goNode _caseDefault)
-      NPi Pi {..} -> Core.mkPi mempty (goBinder _piBinder) (goNode _piBody)
-      NUniv Univ {..} -> Core.mkUniv' _univLevel
-      NTyp TypeConstr {..} -> Core.mkTypeConstr' _typeConstrSymbol (map goNode _typeConstrArgs)
-      NPrim TypePrim {..} -> Core.mkTypePrim' _typePrimPrimitive
-      NDyn DynamicTy {} -> Core.mkDynamic'
-      NBot Bottom {..} -> Core.mkBottom mempty (goNode _bottomType)
-
+toCoreNode :: Node -> Core.Node
+toCoreNode = \case
+  NVar Var {..} -> Core.mkVar' _varIndex
+  NIdt Ident {..} -> Core.mkIdent' _identSymbol
+  NCst Constant {..} -> Core.mkConstant' _constantValue
+  NApp App {..} -> Core.mkApp' (toCoreNode _appLeft) (toCoreNode _appRight)
+  NBlt BuiltinApp {..} -> Core.mkBuiltinApp' _builtinAppOp (map toCoreNode _builtinAppArgs)
+  NCtr Constr {..} -> Core.mkConstr' _constrTag (map toCoreNode _constrArgs)
+  NLam Lambda {..} -> Core.mkLambda mempty (goBinder _lambdaBinder) (toCoreNode _lambdaBody)
+  NLet Let {..} -> Core.NLet $ Core.Let mempty (goLetItem _letItem) (toCoreNode _letBody)
+  NRec LetRec {..} -> Core.NRec $ Core.LetRec mempty (fmap goLetItem _letRecValues) (toCoreNode _letRecBody)
+  NCase Case {..} -> Core.mkCase' _caseInductive (toCoreNode _caseValue) (map goCaseBranch _caseBranches) (fmap toCoreNode _caseDefault)
+  NPi Pi {..} -> Core.mkPi mempty (goBinder _piBinder) (toCoreNode _piBody)
+  NUniv Univ {..} -> Core.mkUniv' _univLevel
+  NTyp TypeConstr {..} -> Core.mkTypeConstr' _typeConstrSymbol (map toCoreNode _typeConstrArgs)
+  NPrim TypePrim {..} -> Core.mkTypePrim' _typePrimPrimitive
+  NDyn DynamicTy {} -> Core.mkDynamic'
+  NBot Bottom {..} -> Core.mkBottom mempty (toCoreNode _bottomType)
+  where
     goBinder :: Binder -> Core.Binder
-    goBinder Binder {..} = Core.Binder _binderName _binderLocation (goNode _binderType)
+    goBinder Binder {..} = Core.Binder _binderName _binderLocation (toCoreNode _binderType)
 
     goLetItem :: LetItem -> Core.LetItem
-    goLetItem LetItem {..} = Core.LetItem (goBinder _letItemBinder) (goNode _letItemValue)
+    goLetItem LetItem {..} = Core.LetItem (goBinder _letItemBinder) (toCoreNode _letItemValue)
 
     goCaseBranch :: CaseBranch -> Core.CaseBranch
-    goCaseBranch CaseBranch {..} = Core.CaseBranch mempty _caseBranchTag (map goBinder _caseBranchBinders) _caseBranchBindersNum (goNode _caseBranchBody)
+    goCaseBranch CaseBranch {..} = Core.CaseBranch mempty _caseBranchTag (map goBinder _caseBranchBinders) _caseBranchBindersNum (toCoreNode _caseBranchBody)
 
 fromCore :: Core.InfoTable -> InfoTable
 fromCore Core.InfoTable {..} =
   InfoTable
-    { _identContext = fmap goNode _identContext,
+    { _identContext = fmap fromCoreNode _identContext,
       _identMap,
       _infoMain,
       _infoIdentifiers = fmap goIdentifierInfo _infoIdentifiers,
@@ -111,14 +111,14 @@ fromCore Core.InfoTable {..} =
     goIdentifierInfo :: Core.IdentifierInfo -> IdentifierInfo
     goIdentifierInfo Core.IdentifierInfo {..} =
       IdentifierInfo
-        { _identifierType = goNode _identifierType,
+        { _identifierType = fromCoreNode _identifierType,
           ..
         }
 
     goInductiveInfo :: Core.InductiveInfo -> InductiveInfo
     goInductiveInfo Core.InductiveInfo {..} =
       InductiveInfo
-        { _inductiveKind = goNode _inductiveKind,
+        { _inductiveKind = fromCoreNode _inductiveKind,
           _inductiveParams = map goParameterInfo _inductiveParams,
           ..
         }
@@ -126,57 +126,57 @@ fromCore Core.InfoTable {..} =
     goParameterInfo :: Core.ParameterInfo -> ParameterInfo
     goParameterInfo Core.ParameterInfo {..} =
       ParameterInfo
-        { _paramKind = goNode _paramKind,
+        { _paramKind = fromCoreNode _paramKind,
           ..
         }
 
     goConstructorInfo :: Core.ConstructorInfo -> ConstructorInfo
     goConstructorInfo Core.ConstructorInfo {..} =
       ConstructorInfo
-        { _constructorType = goNode _constructorType,
+        { _constructorType = fromCoreNode _constructorType,
           ..
         }
 
     goAxiomInfo :: Core.AxiomInfo -> AxiomInfo
     goAxiomInfo Core.AxiomInfo {..} =
       AxiomInfo
-        { _axiomType = goNode _axiomType,
+        { _axiomType = fromCoreNode _axiomType,
           ..
         }
 
     goSpecialisationInfo :: Core.SpecialisationInfo -> SpecialisationInfo
     goSpecialisationInfo Core.SpecialisationInfo {..} =
       SpecialisationInfo
-        { _specSignature = first (map goNode) _specSignature,
+        { _specSignature = first (map fromCoreNode) _specSignature,
           ..
         }
 
-    goNode :: Core.Node -> Node
-    goNode = \case
-      Core.NVar Core.Var {..} -> NVar $ Var () _varIndex
-      Core.NIdt Core.Ident {..} -> NIdt $ Ident () _identSymbol
-      Core.NCst Core.Constant {..} -> NCst $ Constant () _constantValue
-      Core.NApp Core.App {..} -> NApp $ App () (goNode _appLeft) (goNode _appRight)
-      Core.NBlt Core.BuiltinApp {..} -> NBlt $ BuiltinApp () _builtinAppOp (map goNode _builtinAppArgs)
-      Core.NCtr Core.Constr {..} -> NCtr $ Constr () _constrTag (map goNode _constrArgs)
-      Core.NLam Core.Lambda {..} -> NLam $ Lambda () (goBinder _lambdaBinder) (goNode _lambdaBody)
-      Core.NLet Core.Let {..} -> NLet $ Let () (goLetItem _letItem) (goNode _letBody)
-      Core.NRec Core.LetRec {..} -> NRec $ LetRec () (fmap goLetItem _letRecValues) (goNode _letRecBody)
-      Core.NCase Core.Case {..} -> NCase $ Case () _caseInductive (goNode _caseValue) (map goCaseBranch _caseBranches) (fmap goNode _caseDefault)
-      Core.NPi Core.Pi {..} -> NPi $ Pi () (goBinder _piBinder) (goNode _piBody)
-      Core.NUniv Core.Univ {..} -> NUniv $ Univ () _univLevel
-      Core.NTyp Core.TypeConstr {..} -> NTyp $ TypeConstr () _typeConstrSymbol (map goNode _typeConstrArgs)
-      Core.NPrim Core.TypePrim {..} -> NPrim $ TypePrim () _typePrimPrimitive
-      Core.NDyn Core.DynamicTy {} -> NDyn $ DynamicTy ()
-      Core.NBot Core.Bottom {..} -> NBot $ Bottom () (goNode _bottomType)
-      Core.NMatch {} -> impossible
-      Core.Closure {} -> impossible
-
+fromCoreNode :: Core.Node -> Node
+fromCoreNode = \case
+  Core.NVar Core.Var {..} -> NVar $ Var () _varIndex
+  Core.NIdt Core.Ident {..} -> NIdt $ Ident () _identSymbol
+  Core.NCst Core.Constant {..} -> NCst $ Constant () _constantValue
+  Core.NApp Core.App {..} -> NApp $ App () (fromCoreNode _appLeft) (fromCoreNode _appRight)
+  Core.NBlt Core.BuiltinApp {..} -> NBlt $ BuiltinApp () _builtinAppOp (map fromCoreNode _builtinAppArgs)
+  Core.NCtr Core.Constr {..} -> NCtr $ Constr () _constrTag (map fromCoreNode _constrArgs)
+  Core.NLam Core.Lambda {..} -> NLam $ Lambda () (goBinder _lambdaBinder) (fromCoreNode _lambdaBody)
+  Core.NLet Core.Let {..} -> NLet $ Let () (goLetItem _letItem) (fromCoreNode _letBody)
+  Core.NRec Core.LetRec {..} -> NRec $ LetRec () (fmap goLetItem _letRecValues) (fromCoreNode _letRecBody)
+  Core.NCase Core.Case {..} -> NCase $ Case () _caseInductive (fromCoreNode _caseValue) (map goCaseBranch _caseBranches) (fmap fromCoreNode _caseDefault)
+  Core.NPi Core.Pi {..} -> NPi $ Pi () (goBinder _piBinder) (fromCoreNode _piBody)
+  Core.NUniv Core.Univ {..} -> NUniv $ Univ () _univLevel
+  Core.NTyp Core.TypeConstr {..} -> NTyp $ TypeConstr () _typeConstrSymbol (map fromCoreNode _typeConstrArgs)
+  Core.NPrim Core.TypePrim {..} -> NPrim $ TypePrim () _typePrimPrimitive
+  Core.NDyn Core.DynamicTy {} -> NDyn $ DynamicTy ()
+  Core.NBot Core.Bottom {..} -> NBot $ Bottom () (fromCoreNode _bottomType)
+  Core.NMatch {} -> impossible
+  Core.Closure {} -> impossible
+  where
     goBinder :: Core.Binder -> Binder
-    goBinder Core.Binder {..} = Binder _binderName _binderLocation (goNode _binderType)
+    goBinder Core.Binder {..} = Binder _binderName _binderLocation (fromCoreNode _binderType)
 
     goLetItem :: Core.LetItem -> LetItem
-    goLetItem Core.LetItem {..} = LetItem (goBinder _letItemBinder) (goNode _letItemValue)
+    goLetItem Core.LetItem {..} = LetItem (goBinder _letItemBinder) (fromCoreNode _letItemValue)
 
     goCaseBranch :: Core.CaseBranch -> CaseBranch
-    goCaseBranch Core.CaseBranch {..} = CaseBranch mempty _caseBranchTag (map goBinder _caseBranchBinders) _caseBranchBindersNum (goNode _caseBranchBody)
+    goCaseBranch Core.CaseBranch {..} = CaseBranch mempty _caseBranchTag (map goBinder _caseBranchBinders) _caseBranchBindersNum (fromCoreNode _caseBranchBody)

test/Core/Asm/Positive.hs

@@ -8,7 +8,7 @@ allTests :: TestTree
 allTests = testGroup "JuvixCore to JuvixAsm positive tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.compilableTests))
 
 ignoredTests :: [String]
-ignoredTests = []
+ignoredTests = ["Test062: Anoma"]
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =

test/Core/Compile/Positive.hs

@@ -16,7 +16,8 @@ ignoredTests =
     "Test026: Nested 'case', 'let' and 'if' with variable capture",
     "Test036: Big numbers",
     "Test040: LetRec - fib, fact",
-    "Test061: Fields"
+    "Test061: Fields",
+    "Test062: Anoma"
   ]
 
 liftTest :: Eval.PosTest -> TestTree

test/Core/Eval/Positive.hs

@@ -347,5 +347,10 @@ tests =
       "Test061: Fields"
       $(mkRelDir ".")
       $(mkRelFile "test061.jvc")
-      $(mkRelFile "out/test061.out")
+      $(mkRelFile "out/test061.out"),
+    PosTest
+      "Test062: Anoma"
+      $(mkRelDir ".")
+      $(mkRelFile "test062.jvc")
+      $(mkRelFile "out/test062.out")
   ]

tests/Core/positive/out/test062.out

@@ -0,0 +1,5 @@
+true
+true
+true
+true
+false

tests/Core/positive/test062.jvc

@@ -0,0 +1,30 @@
+--- anoma builtins
+
+type t : Type {
+   ctor : Int -> t;
+};
+
+type tClosure : Type {
+   ctorCl : (Int -> Int) -> tClosure;
+};
+
+def privKey : Int := 11617894433197913967256772080085224292574263152640782716628013903136761875218972825378605552167075549144813844196048766885080313195607865362963533894031960;
+
+def pubKey : Int := 100334094580390620383139794340338190270834129828455530198518726236886616013505;
+
+def v1 : t := ctor 10;
+def v2 : t := ctor 0;
+def f1 : Int -> Int := \x 2 * x;
+def v3 : tClosure := ctorCl f1;
+
+def writeLn := \x write x >> write "\n";
+
+def projectClosure := \t match t with {
+  ctorCl f := f;
+};
+
+writeLn (anoma-decode (anoma-encode v1) = v1)
+>> writeLn (projectClosure (anoma-decode (anoma-encode v3)) 10 = 20)
+>> writeLn (anoma-verify (anoma-sign v1 privKey) pubKey = v1)
+>> writeLn (anoma-verify-detached (anoma-sign-detached v1 privKey) v1 pubKey)
+>> writeLn (anoma-verify-detached (anoma-sign-detached v1 privKey) v2 pubKey)