Merge remote-tracking branch 'origin/main' into register-builtins-sco…

…ping
anoma · Aug 19, 2024 · f863107 · f863107
2 parents cffadad + 4fa5d3c
commit f863107
Show file tree

Hide file tree

Showing 23 changed files with 227 additions and 21 deletions.
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -56,7 +56,9 @@ goModule onlyTypes infoTable Internal.Module {..} =
   Theory
     { _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName,
       _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
-      _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
+      _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
+        Just (PragmaIsabelleIgnore True) -> []
+        _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
     toIsabelleName :: Text -> Text
@@ -75,13 +77,18 @@ goModule onlyTypes infoTable Internal.Module {..} =
     goMutualBlock :: Internal.MutualBlock -> [Statement]
     goMutualBlock Internal.MutualBlock {..} =
       filter (\stmt -> not onlyTypes || isTypeDef stmt) $
-        map goMutualStatement (toList _mutualStatements)
+        mapMaybe goMutualStatement (toList _mutualStatements)
 
-    goMutualStatement :: Internal.MutualStatement -> Statement
+    checkNotIgnored :: Pragmas -> a -> Maybe a
+    checkNotIgnored pragmas x = case pragmas ^. pragmasIsabelleIgnore of
+      Just (PragmaIsabelleIgnore True) -> Nothing
+      _ -> Just x
+
+    goMutualStatement :: Internal.MutualStatement -> Maybe Statement
     goMutualStatement = \case
-      Internal.StatementInductive x -> goInductiveDef x
-      Internal.StatementFunction x -> goFunctionDef x
-      Internal.StatementAxiom x -> goAxiomDef x
+      Internal.StatementInductive x -> checkNotIgnored (x ^. Internal.inductivePragmas) $ goInductiveDef x
+      Internal.StatementFunction x -> checkNotIgnored (x ^. Internal.funDefPragmas) $ goFunctionDef x
+      Internal.StatementAxiom x -> checkNotIgnored (x ^. Internal.axiomPragmas) $ goAxiomDef x
 
     goInductiveDef :: Internal.InductiveDef -> Statement
     goInductiveDef Internal.InductiveDef {..}

diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs
@@ -87,3 +87,23 @@ checkAnomaSignDetached f = do
   unless
     ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars)
     $ builtinsErrorText (getLoc f) "anomaSignDetached must be of type {A : Type} -> A -> ByteArray -> ByteArray"
+
+checkAnomaByteArrayToAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaByteArrayToAnomaContents f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype == (byteArray --> nat_))
+    $ builtinsErrorText l "toAnomaContents must be of type ByteArray -> Nat"
+
+checkAnomaByteArrayFromAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaByteArrayFromAnomaContents f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype == (nat_ --> nat_ --> byteArray))
+    $ builtinsErrorText l "fromAnomaContents must be of type Nat -> Nat -> ByteArray"
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -221,6 +221,8 @@ data BuiltinAxiom
   | BuiltinAnomaSign
   | BuiltinAnomaSignDetached
   | BuiltinAnomaVerifyWithMessage
+  | BuiltinAnomaByteArrayToAnomaContents
+  | BuiltinAnomaByteArrayFromAnomaContents
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -265,6 +267,8 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaSign -> KNameFunction
     BuiltinAnomaSignDetached -> KNameFunction
     BuiltinAnomaVerifyWithMessage -> KNameFunction
+    BuiltinAnomaByteArrayToAnomaContents -> KNameFunction
+    BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -316,6 +320,8 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaSignDetached -> Str.anomaSignDetached
     BuiltinAnomaSign -> Str.anomaSign
     BuiltinAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage
+    BuiltinAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
+    BuiltinAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1687,14 +1687,27 @@ checkSections sec = topBindings helper
                                   _projectionKind = kind,
                                   _projectionFieldBuiltin = field ^. fieldBuiltin,
                                   _projectionDoc = field ^. fieldDoc,
-                                  _projectionPragmas = field ^. fieldPragmas
+                                  _projectionPragmas = combinePragmas (i ^. inductivePragmas) (field ^. fieldPragmas)
                                 }
                               where
                                 kind :: ProjectionKind
                                 kind = case field ^. fieldIsImplicit of
                                   ExplicitField -> ProjectionExplicit
                                   ImplicitInstanceField -> ProjectionCoercion
 
+                                combinePragmas :: Maybe ParsedPragmas -> Maybe ParsedPragmas -> Maybe ParsedPragmas
+                                combinePragmas p1 p2 = case (p1, p2) of
+                                  (Nothing, Nothing) -> Nothing
+                                  (Just p, Nothing) -> Just p
+                                  (Nothing, Just p) -> Just p
+                                  (Just p1', Just p2') ->
+                                    Just
+                                      ( over
+                                          (withLocParam . withSourceValue . pragmasIsabelleIgnore)
+                                          (\i2 -> i2 <|> (p1' ^. withLocParam . withSourceValue . pragmasIsabelleIgnore))
+                                          p2'
+                                      )
+
                             getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
                             getFields = case i ^. inductiveConstructors of
                               c :| [] -> case c ^. constructorRhs of

diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -16,6 +16,7 @@ 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.ByteString (byteStringToIntegerLE, integerToByteStringLELen)
 import Juvix.Compiler.Nockma.Encoding.Ed25519 qualified as E
 import Juvix.Compiler.Store.Core.Extra qualified as Store
 import Juvix.Data.Field
@@ -211,6 +212,8 @@ geval opts herr tab env0 = eval' env0
       OpAnomaSign -> anomaSignOp
       OpAnomaSignDetached -> anomaSignDetachedOp
       OpAnomaVerifyWithMessage -> anomaVerifyWithMessageOp
+      OpAnomaByteArrayToAnomaContents -> anomaByteArrayToAnomaContents
+      OpAnomaByteArrayFromAnomaContents -> anomaByteArrayFromAnomaContents
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -432,6 +435,31 @@ geval opts herr tab env0 = eval' env0
                         _ -> err "anomaVerifyWithMessageOp: both arguments are not bytearrays"
         {-# INLINE anomaVerifyWithMessageOp #-}
 
+        anomaByteArrayToAnomaContents :: [Node] -> Node
+        anomaByteArrayToAnomaContents = checkApply $ \arg ->
+          let !v = eval' env arg
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaByteArrayToAnomaContents [v]
+                  | otherwise ->
+                      case (byteStringFromNode v) of
+                        (Just bs) -> nodeFromInteger (byteStringToIntegerLE bs)
+                        _ -> err "anomaByteArrayToAnomaContents: expected argument to be a bytearray"
+        {-# INLINE anomaByteArrayToAnomaContents #-}
+
+        anomaByteArrayFromAnomaContents :: [Node] -> Node
+        anomaByteArrayFromAnomaContents = checkApply $ \arg1 arg2 ->
+          let !v1 = eval' env arg1
+              !v2 = eval' env arg2
+           in if
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                      mkBuiltinApp' OpAnomaByteArrayFromAnomaContents [v1, v2]
+                  | otherwise ->
+                      case (integerFromNode v1, integerFromNode v2) of
+                        (Just i1, Just i2) -> nodeFromByteString (integerToByteStringLELen (fromIntegral i1) i2)
+                        _ -> err "anomaByteArrayFromAnomaContents: expected both argmuments to be integers"
+        {-# INLINE anomaByteArrayFromAnomaContents #-}
+
         poseidonHashOp :: [Node] -> Node
         poseidonHashOp = unary $ \arg ->
           if

diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
@@ -430,6 +430,8 @@ builtinOpArgTypes = \case
   OpAnomaSign -> [mkDynamic', mkDynamic']
   OpAnomaSignDetached -> [mkDynamic', mkDynamic']
   OpAnomaVerifyWithMessage -> [mkDynamic', mkDynamic']
+  OpAnomaByteArrayToAnomaContents -> [mkDynamic']
+  OpAnomaByteArrayFromAnomaContents -> [mkTypeInteger', mkTypeInteger']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs
@@ -33,6 +33,8 @@ data BuiltinOp
   | OpAnomaSign
   | OpAnomaSignDetached
   | OpAnomaVerifyWithMessage
+  | OpAnomaByteArrayToAnomaContents
+  | OpAnomaByteArrayFromAnomaContents
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -91,6 +93,8 @@ builtinOpArgsNum = \case
   OpAnomaSign -> 2
   OpAnomaSignDetached -> 2
   OpAnomaVerifyWithMessage -> 2
+  OpAnomaByteArrayToAnomaContents -> 1
+  OpAnomaByteArrayFromAnomaContents -> 2
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -138,6 +142,8 @@ builtinIsFoldable = \case
   OpAnomaSign -> False
   OpAnomaSignDetached -> False
   OpAnomaVerifyWithMessage -> False
+  OpAnomaByteArrayToAnomaContents -> False
+  OpAnomaByteArrayFromAnomaContents -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -169,7 +175,9 @@ builtinsAnoma =
     OpAnomaVerifyDetached,
     OpAnomaSign,
     OpAnomaVerifyWithMessage,
-    OpAnomaSignDetached
+    OpAnomaSignDetached,
+    OpAnomaByteArrayToAnomaContents,
+    OpAnomaByteArrayFromAnomaContents
   ]
 
 builtinsUInt8 :: [BuiltinOp]

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -60,6 +60,8 @@ instance PrettyCode BuiltinOp where
     OpAnomaSign -> return primAnomaSign
     OpAnomaSignDetached -> return primAnomaSignDetached
     OpAnomaVerifyWithMessage -> return primAnomaVerifyWithMessage
+    OpAnomaByteArrayToAnomaContents -> return primAnomaByteArrayToAnomaContents
+    OpAnomaByteArrayFromAnomaContents -> return primAnomaByteArrayFromAnomaContents
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -875,6 +877,12 @@ primAnomaSignDetached = primitive Str.anomaSignDetached
 primAnomaVerifyWithMessage :: Doc Ann
 primAnomaVerifyWithMessage = primitive Str.anomaVerifyWithMessage
 
+primAnomaByteArrayToAnomaContents :: Doc Ann
+primAnomaByteArrayToAnomaContents = primitive Str.anomaByteArrayToAnomaContents
+
+primAnomaByteArrayFromAnomaContents :: Doc Ann
+primAnomaByteArrayFromAnomaContents = primitive Str.anomaByteArrayFromAnomaContents
+
 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
@@ -75,6 +75,8 @@ computeNodeTypeInfo md = umapL go
           OpAnomaSign -> Info.getNodeType node
           OpAnomaSignDetached -> Info.getNodeType node
           OpAnomaVerifyWithMessage -> Info.getNodeType node
+          OpAnomaByteArrayFromAnomaContents -> Info.getNodeType node
+          OpAnomaByteArrayToAnomaContents -> mkTypeInteger'
           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
@@ -616,6 +616,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaSign -> return ()
       Internal.BuiltinAnomaSignDetached -> return ()
       Internal.BuiltinAnomaVerifyWithMessage -> return ()
+      BuiltinAnomaByteArrayToAnomaContents -> return ()
+      BuiltinAnomaByteArrayFromAnomaContents -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -811,6 +813,18 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   )
               )
           )
+      Internal.BuiltinAnomaByteArrayToAnomaContents ->
+        registerAxiomDef (mkLambda' mkDynamic' (mkBuiltinApp' OpAnomaByteArrayToAnomaContents [mkVar' 0]))
+      Internal.BuiltinAnomaByteArrayFromAnomaContents -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              natType
+              ( mkLambda'
+                  natType
+                  (mkBuiltinApp' OpAnomaByteArrayFromAnomaContents [mkVar' 1, mkVar' 0])
+              )
+          )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
         psSym <- getPoseidonStateSymbol
@@ -1233,6 +1247,8 @@ goApplication a = do
         Just Internal.BuiltinAnomaSign -> app
         Just Internal.BuiltinAnomaSignDetached -> app
         Just Internal.BuiltinAnomaVerifyWithMessage -> app
+        Just Internal.BuiltinAnomaByteArrayToAnomaContents -> app
+        Just Internal.BuiltinAnomaByteArrayFromAnomaContents -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -105,6 +105,8 @@ fromCore fsize tab =
         BuiltinAnomaSign -> False
         BuiltinAnomaSignDetached -> False
         BuiltinAnomaVerifyWithMessage -> False
+        BuiltinAnomaByteArrayToAnomaContents -> False
+        BuiltinAnomaByteArrayFromAnomaContents -> 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
@@ -585,6 +585,8 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaSign -> checkAnomaSign d
   BuiltinAnomaSignDetached -> checkAnomaSignDetached d
   BuiltinAnomaVerifyWithMessage -> checkAnomaVerifyWithMessage d
+  BuiltinAnomaByteArrayFromAnomaContents -> checkAnomaByteArrayFromAnomaContents d
+  BuiltinAnomaByteArrayToAnomaContents -> checkAnomaByteArrayToAnomaContents d
   BuiltinPoseidon -> checkPoseidon d
   BuiltinEcOp -> checkEcOp d
   BuiltinRandomEcPoint -> checkRandomEcPoint d

diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
@@ -495,6 +495,8 @@ compile = \case
         Tree.OpAnomaSign -> return (goAnomaSign args)
         Tree.OpAnomaVerifyWithMessage -> return (goAnomaVerifyWithMessage args)
         Tree.OpAnomaSignDetached -> return (goAnomaSignDetached args)
+        Tree.OpAnomaByteArrayFromAnomaContents -> return (goAnomaByteArrayFromAnomaContents args)
+        Tree.OpAnomaByteArrayToAnomaContents -> return (goAnomaByteArrayToAnomaContents args)
 
     goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural)
     goByteArrayOp Tree.NodeByteArray {..} = do
@@ -591,6 +593,16 @@ compile = \case
           )
       _ -> impossible
 
+    goAnomaByteArrayToAnomaContents :: [Term Natural] -> Term Natural
+    goAnomaByteArrayToAnomaContents = \case
+      [ba] -> byteArrayPayload "bytearryToAnomaContents-payload" ba
+      _ -> impossible
+
+    goAnomaByteArrayFromAnomaContents :: [Term Natural] -> Term Natural
+    goAnomaByteArrayFromAnomaContents = \case
+      [len, contents] -> mkByteArray len contents
+      _ -> impossible
+
     -- Conceptually this function is:
     -- anomaDecode <$> verify signedMessage pubKey
     --

diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs
@@ -96,4 +96,8 @@ data AnomaOp
     OpAnomaVerifyWithMessage
   | -- | Produce a cryptographic signature of an Anoma value
     OpAnomaSignDetached
+  | -- | Construct an Anoma atom from a ByteArray with LSB ordering
+    OpAnomaByteArrayToAnomaContents
+  | -- | Construct a ByteArray from the bytes of an Anoma atom with LSB ordering
+    OpAnomaByteArrayFromAnomaContents
   deriving stock (Eq)
diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs
@@ -291,6 +291,8 @@ instance PrettyCode AnomaOp where
     OpAnomaSign -> Str.anomaSign
     OpAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage
     OpAnomaSignDetached -> Str.anomaSignDetached
+    OpAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
+    OpAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case

diff --git a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
@@ -18,6 +18,8 @@ checkNoAnoma = walkT checkNode
         OpAnomaSign -> unsupportedErr "OpAnomaSign"
         OpAnomaSignDetached -> unsupportedErr "OpAnomaSignDetached"
         OpAnomaVerifyWithMessage -> unsupportedErr "OpAnomaVerifyWithMessage"
+        OpAnomaByteArrayFromAnomaContents -> unsupportedErr "OpAnomaByteArrayFromAnomaContents"
+        OpAnomaByteArrayToAnomaContents -> unsupportedErr "OpAnomaByteArrayToAnomaContents"
         where
           unsupportedErr :: Text -> Sem r ()
           unsupportedErr opName =

diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
@@ -339,6 +339,8 @@ genCode infoTable fi =
       Core.OpAnomaSign -> OpAnomaSign
       Core.OpAnomaSignDetached -> OpAnomaSignDetached
       Core.OpAnomaVerifyWithMessage -> OpAnomaVerifyWithMessage
+      Core.OpAnomaByteArrayToAnomaContents -> OpAnomaByteArrayToAnomaContents
+      Core.OpAnomaByteArrayFromAnomaContents -> OpAnomaByteArrayFromAnomaContents
       _ -> impossible
 
     getArgsNum :: Symbol -> Int