From 8d03ac2b6cb23e9439e456acafc9db1219760d73 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 19 Aug 2024 10:19:26 +0100 Subject: [PATCH 1/2] Add `anoma-bytearray-{to, from}-anoma-contents` builtins (#2960) The `anoma-bytearray-{to, from}-anoma-contents` are intended to be used to convert to/from atoms representing `ByteArrays`. These builtins are required temporarily until Anoma Node makes ByteArray representation uniform across all of its APIs. We represent ByteArrays in nock as a cell: ``` [size contents] ``` Where `size` is the size of the ByteArray and `contents` is an Atom representing the bytes in LSB ordering. The `size` is required in general because the encoding of ByteArrays to Atoms is ambiguous. For example the ByteArrays [0x01; 0x00] and [0x01] are represented by `1`. Some Anoma ByteArrays like keys and signatures are represented using on the `contents` atom because the size is constant. Users of Anoma APIs have to strip / add size information from ByteArrays depending on where the data is used. The new builtins provide this facility. These builtins are temporary because it's been agreed with Anoma engineering team to change the Anoma APIs to make the ByteArray representation uniform, i.e always represent ByteArrays using `[size content]`. When this is implemented in Anoma Node we can remove these builtins. ``` builtin anoma-bytearray-to-anoma-contents axiom toAnomaContents : ByteArray -> Nat; builtin anoma-bytearray-from-anoma-contents axiom fromAnomaContents : -- | The size of the ByteArray Nat -- | The contents of the ByteArray -> Nat -- | The resulting ByteArray -> ByteArray; ``` --- src/Juvix/Compiler/Builtins/Anoma.hs | 20 +++++++++ src/Juvix/Compiler/Concrete/Data/Builtins.hs | 6 +++ src/Juvix/Compiler/Core/Evaluator.hs | 28 +++++++++++++ src/Juvix/Compiler/Core/Extra/Utils.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 | 16 ++++++++ .../Core/Translation/Stripped/FromCore.hs | 2 + .../Internal/Translation/FromConcrete.hs | 2 + .../Compiler/Nockma/Translation/FromTree.hs | 12 ++++++ src/Juvix/Compiler/Tree/Language/Builtins.hs | 4 ++ src/Juvix/Compiler/Tree/Pretty/Base.hs | 2 + .../Tree/Transformation/CheckNoAnoma.hs | 2 + .../Compiler/Tree/Translation/FromCore.hs | 2 + src/Juvix/Extra/Strings.hs | 6 +++ test/Anoma/Compilation/Positive.hs | 12 ++++++ .../Anoma/Compilation/positive/test083.juvix | 41 +++++++++++++++++++ 18 files changed, 176 insertions(+), 1 deletion(-) create mode 100644 tests/Anoma/Compilation/positive/test083.juvix diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index 16956cd29f..7b8a7169a6 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -97,3 +97,23 @@ registerAnomaSignDetached f = do ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars) (error "anomaSignDetached must be of type {A : Type} -> A -> ByteArray -> ByteArray") registerBuiltin BuiltinAnomaSignDetached (f ^. axiomName) + +registerByteArrayToAnomaContents :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () +registerByteArrayToAnomaContents f = do + let loc = getLoc f + byteArray <- getBuiltinName loc BuiltinByteArray + nat_ <- getBuiltinName loc BuiltinNat + unless + (f ^. axiomType == (byteArray --> nat_)) + (error "toAnomaContents must be of type ByteArray -> Nat") + registerBuiltin BuiltinAnomaByteArrayToAnomaContents (f ^. axiomName) + +registerByteArrayFromAnomaContents :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () +registerByteArrayFromAnomaContents f = do + let loc = getLoc f + byteArray <- getBuiltinName loc BuiltinByteArray + nat_ <- getBuiltinName loc BuiltinNat + unless + (f ^. axiomType == (nat_ --> nat_ --> byteArray)) + (error "fromAnomaContents must be of type Nat -> Nat -> ByteArray") + registerBuiltin BuiltinAnomaByteArrayFromAnomaContents (f ^. axiomName) diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 698aab0a47..358bdeb752 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -215,6 +215,8 @@ data BuiltinAxiom | BuiltinAnomaSign | BuiltinAnomaSignDetached | BuiltinAnomaVerifyWithMessage + | BuiltinAnomaByteArrayToAnomaContents + | BuiltinAnomaByteArrayFromAnomaContents | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint @@ -259,6 +261,8 @@ instance HasNameKind BuiltinAxiom where BuiltinAnomaSign -> KNameFunction BuiltinAnomaSignDetached -> KNameFunction BuiltinAnomaVerifyWithMessage -> KNameFunction + BuiltinAnomaByteArrayToAnomaContents -> KNameFunction + BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction BuiltinPoseidon -> KNameFunction BuiltinEcOp -> KNameFunction BuiltinRandomEcPoint -> KNameFunction @@ -310,6 +314,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/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 1448a15339..21bc538477 100644 --- 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 index a57b0c4e26..d133dc8f67 100644 --- 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 index e4c1cb3d3b..c6c81a1bee 100644 --- 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 index 987f877be1..433567ce9d 100644 --- 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 index b180ad5763..812c60dcd6 100644 --- 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 index 14e76454c2..819ccf009f 100644 --- 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 index 6c25d41b0b..e87799c5af 100644 --- 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 index 295661c405..05b25ed201 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -584,6 +584,8 @@ registerBuiltinAxiom d = \case BuiltinAnomaSign -> registerAnomaSign d BuiltinAnomaSignDetached -> registerAnomaSignDetached d BuiltinAnomaVerifyWithMessage -> registerAnomaVerifyWithMessage d + BuiltinAnomaByteArrayToAnomaContents -> registerByteArrayToAnomaContents d + BuiltinAnomaByteArrayFromAnomaContents -> registerByteArrayFromAnomaContents d BuiltinPoseidon -> registerPoseidon d BuiltinEcOp -> registerEcOp d BuiltinRandomEcPoint -> registerRandomEcPoint d diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index 51dbed4187..31081dc833 100644 --- 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 index 3145026a2a..4802d90a28 100644 --- 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 index abdec2bd81..59433b8cdb 100644 --- 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 index 5ddfb1ae13..ca91ab57f9 100644 --- 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 index 52e5ead2bf..a5d578299a 100644 --- 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 diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index fa064e51b9..7fe7156802 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -374,6 +374,12 @@ anomaSignDetached = "anoma-sign-detached" anomaVerifyWithMessage :: (IsString s) => s anomaVerifyWithMessage = "anoma-verify-with-message" +anomaByteArrayToAnomaContents :: (IsString s) => s +anomaByteArrayToAnomaContents = "anoma-bytearray-to-anoma-contents" + +anomaByteArrayFromAnomaContents :: (IsString s) => s +anomaByteArrayFromAnomaContents = "anoma-bytearray-from-anoma-contents" + builtinSeq :: (IsString s) => s builtinSeq = "seq" diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index 91d414f485..3f53eb01ba 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -630,5 +630,17 @@ allTests = [nock| [2 258] |], [nock| 1 |], [nock| [1 0] |] + ], + mkAnomaCallTest + "Test083: Anoma ByteArray" + $(mkRelDir ".") + $(mkRelFile "test083.juvix") + [] + $ checkOutput + [ [nock| [[0 0] 0] |], + [nock| [[3 0] 0] |], + [nock| [[4 1] 1] |], + [nock| [[2 258] 258] |], + [nock| [[1 0] 0] |] ] ] diff --git a/tests/Anoma/Compilation/positive/test083.juvix b/tests/Anoma/Compilation/positive/test083.juvix new file mode 100644 index 0000000000..683558e2e5 --- /dev/null +++ b/tests/Anoma/Compilation/positive/test083.juvix @@ -0,0 +1,41 @@ +module test083; + +import Stdlib.Prelude open; +import Stdlib.Debug.Trace open; + +builtin bytearray +axiom ByteArray : Type; + +builtin bytearray-from-list-byte +axiom mkByteArray : List Byte -> ByteArray; + +builtin bytearray-length +axiom size : ByteArray -> Nat; + +builtin anoma-bytearray-to-anoma-contents +axiom toAnomaContents : ByteArray -> Nat; + +builtin anoma-bytearray-from-anoma-contents +axiom fromAnomaContents : Nat -> Nat -> ByteArray; + +bs0 : ByteArray := mkByteArray []; + +bs1 : ByteArray := mkByteArray [0x0; 0x0; 0x0]; + +bs2 : ByteArray := mkByteArray [0x1; 0x0; 0x0; 0x0]; + +bs3 : ByteArray := mkByteArray [0x2; 0x1]; + +bs4 : ByteArray := mkByteArray [0x100]; + +testByteArray (ba : ByteArray) : Pair ByteArray Nat := + let + anomaContents := toAnomaContents ba; + in fromAnomaContents (size ba) anomaContents, anomaContents; + +main : Pair ByteArray Nat := + trace (testByteArray bs0) + >-> trace (testByteArray bs1) + >-> trace (testByteArray bs2) + >-> trace (testByteArray bs3) + >-> testByteArray bs4; From 4fa5d3ca1bd1f26e6b819dffda0ce9c447807667 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Mon, 19 Aug 2024 12:22:10 +0200 Subject: [PATCH 2/2] Isabelle/HOL translation: the `isabelle-ignore` pragma (#2955) * Closes #2940 --- .../Backend/Isabelle/Translation/FromTyped.hs | 19 +++++++++----- .../FromParsed/Analysis/Scoping.hs | 15 ++++++++++- src/Juvix/Data/Pragmas.hs | 26 ++++++++++++++++--- tests/positive/Isabelle/Program.juvix | 1 + tests/positive/Isabelle/isabelle/Program.thy | 10 ------- 5 files changed, 51 insertions(+), 20 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 7c66fc1c23..61ae8f7b6c 100644 --- 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/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 7cbcdb536f..7e52ff866e 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1650,7 +1650,7 @@ checkSections sec = topBindings helper _projectionKind = kind, _projectionFieldBuiltin = field ^. fieldBuiltin, _projectionDoc = field ^. fieldDoc, - _projectionPragmas = field ^. fieldPragmas + _projectionPragmas = combinePragmas (i ^. inductivePragmas) (field ^. fieldPragmas) } where kind :: ProjectionKind @@ -1658,6 +1658,19 @@ checkSections sec = topBindings helper 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/Data/Pragmas.hs b/src/Juvix/Data/Pragmas.hs index ad0690e065..641692887e 100644 --- a/src/Juvix/Data/Pragmas.hs +++ b/src/Juvix/Data/Pragmas.hs @@ -71,6 +71,11 @@ newtype PragmaIsabelleFunction = PragmaIsabelleFunction } deriving stock (Show, Eq, Ord, Data, Generic) +newtype PragmaIsabelleIgnore = PragmaIsabelleIgnore + { _pragmaIsabelleIgnore :: Bool + } + deriving stock (Show, Eq, Ord, Data, Generic) + data Pragmas = Pragmas { _pragmasInline :: Maybe PragmaInline, _pragmasUnroll :: Maybe PragmaUnroll, @@ -82,7 +87,8 @@ data Pragmas = Pragmas _pragmasSpecialiseBy :: Maybe PragmaSpecialiseBy, _pragmasEval :: Maybe PragmaEval, _pragmasIsabelleOperator :: Maybe PragmaIsabelleOperator, - _pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction + _pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction, + _pragmasIsabelleIgnore :: Maybe PragmaIsabelleIgnore } deriving stock (Show, Eq, Ord, Data, Generic) @@ -121,6 +127,8 @@ instance Hashable PragmaIsabelleOperator instance Hashable PragmaIsabelleFunction +instance Hashable PragmaIsabelleIgnore + instance Hashable Pragmas instance Serialize PragmaInline @@ -171,6 +179,10 @@ instance Serialize PragmaIsabelleFunction instance NFData PragmaIsabelleFunction +instance Serialize PragmaIsabelleIgnore + +instance NFData PragmaIsabelleIgnore + instance Serialize Pragmas instance NFData Pragmas @@ -201,6 +213,7 @@ instance FromJSON Pragmas where _pragmasEval <- keyMay "eval" parseEval _pragmasIsabelleOperator <- keyMay "isabelle-operator" parseIsabelleOperator _pragmasIsabelleFunction <- keyMay "isabelle-function" parseIsabelleFunction + _pragmasIsabelleIgnore <- keyMay "isabelle-ignore" parseIsabelleIgnore return Pragmas {..} parseInline :: Parse YamlError PragmaInline @@ -273,6 +286,11 @@ instance FromJSON Pragmas where _pragmaIsabelleFunctionName <- key "name" asText return PragmaIsabelleFunction {..} + parseIsabelleIgnore :: Parse YamlError PragmaIsabelleIgnore + parseIsabelleIgnore = do + _pragmaIsabelleIgnore <- asBool + return PragmaIsabelleIgnore {..} + parseSpecialiseArg :: Parse YamlError PragmaSpecialiseArg parseSpecialiseArg = (SpecialiseArgNum <$> asIntegral) @@ -316,7 +334,8 @@ instance Semigroup Pragmas where _pragmasSpecialiseArgs = p2 ^. pragmasSpecialiseArgs <|> p1 ^. pragmasSpecialiseArgs, _pragmasSpecialiseBy = p2 ^. pragmasSpecialiseBy <|> p1 ^. pragmasSpecialiseBy, _pragmasIsabelleOperator = p2 ^. pragmasIsabelleOperator, - _pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction + _pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction, + _pragmasIsabelleIgnore = p2 ^. pragmasIsabelleIgnore <|> p1 ^. pragmasIsabelleIgnore } instance Monoid Pragmas where @@ -332,7 +351,8 @@ instance Monoid Pragmas where _pragmasSpecialiseBy = Nothing, _pragmasEval = Nothing, _pragmasIsabelleOperator = Nothing, - _pragmasIsabelleFunction = Nothing + _pragmasIsabelleFunction = Nothing, + _pragmasIsabelleIgnore = Nothing } adjustPragmaInline :: Int -> PragmaInline -> PragmaInline diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 69d15bdb4e..0cd881bc34 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -91,6 +91,7 @@ type Either' A B := Left' A | Right' B; -- Records +{-# isabelle-ignore: true #-} type R := mkR { r1 : Nat; r2 : Nat; diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index df548c13df..e9c72431aa 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -99,16 +99,6 @@ datatype ('A, 'B) Either' = Left' 'A | Right' 'B -record R = - r1 :: nat - r2 :: nat - -fun r1 :: "R \ nat" where - "r1 (mkR r1' r2') = r1'" - -fun r2 :: "R \ nat" where - "r2 (mkR r1' r2') = r2'" - fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))"