Logical operations (IntersectMBO#5970)

* Initial port of logical ops * Add PlutusTx correspondents to the new builtins * Tests for logical operations * Rest of tests * Formatting of denotations * Rename byteStringReplicate to replicateByteString * Correct references to CIP-121 * Changelogs, document tests * Note commutativity for new operations * Properly rename replicate builtin, add to plutus-tx-plugin * Make new logical builtins available in V3 * Fix links to CIP-122, use toOpaque and fromOpaque instead * Correct all references to CIP-122 * Rename bitwise builtins, use proper costing * Bitwise primops will not be in Conway * Rename tests to suit new primop names
mlabs-haskell · Jun 9, 2024 · f6b9bdc · f6b9bdc
1 parent 37e681c
commit f6b9bdc
Show file tree

Hide file tree

Showing 17 changed files with 1,515 additions and 38 deletions.
diff --git a/plutus-core/changelog.d/20240510_104627_koz.ross_logical.md b/plutus-core/changelog.d/20240510_104627_koz.ross_logical.md
@@ -0,0 +1,38 @@
+<!--
+A new scriv changelog fragment.
+
+Uncomment the section that is right (remove the HTML comment wrapper).
+-->
+
+<!--
+### Removed
+
+- A bullet item for the Removed category.
+
+-->
+### Added
+
+- Logical operations as per [CIP-122](https://github.com/mlabs-haskell/CIPs/blob/koz/logic-ops/CIP-0122/CIP-0122.md).
+
+### Changed
+
+- References to CIP-87 have been corrected to refer to CIP-121.
+
+<!--
+### Deprecated
+
+- A bullet item for the Deprecated category.
+
+-->
+<!--
+### Fixed
+
+- A bullet item for the Fixed category.
+
+-->
+<!--
+### Security
+
+- A bullet item for the Security category.
+
+-->
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
@@ -93,6 +93,7 @@ library
     PlutusCore.Annotation
     PlutusCore.Arity
     PlutusCore.Bitwise.Convert
+    PlutusCore.Bitwise.Logical
     PlutusCore.Builtin
     PlutusCore.Builtin.Debug
     PlutusCore.Builtin.Elaborate
@@ -423,6 +424,7 @@ test-suite untyped-plutus-core-test
     Evaluation.Builtins.Conversion
     Evaluation.Builtins.Costing
     Evaluation.Builtins.Definition
+    Evaluation.Builtins.Laws
     Evaluation.Builtins.MakeRead
     Evaluation.Builtins.SignatureVerification
     Evaluation.Debug

diff --git a/plutus-core/plutus-core/src/PlutusCore/Bitwise/Convert.hs b/plutus-core/plutus-core/src/PlutusCore/Bitwise/Convert.hs
@@ -118,7 +118,7 @@ data IntegerToByteStringError =
   deriving stock (Eq, Show)
 
 -- | Conversion from 'Integer' to 'ByteString', as per
--- [CIP-0087](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX).
+-- [CIP-121](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-0121).
 --
 -- For performance and clarity, the endianness argument uses
 -- 'ByteOrder', and the length argument is an 'Int'.
@@ -232,7 +232,7 @@ integerToByteString requestedByteOrder requestedLength input
       Builder.bytes (BS.replicate paddingLength 0x0) <> acc
 
 -- | Conversion from 'ByteString' to 'Integer', as per
--- [CIP-0087](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX).
+-- [CIP-121](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-0121).
 --
 -- For clarity, the stated endianness argument uses 'ByteOrder'.
 byteStringToInteger :: ByteOrder -> ByteString -> Integer

diff --git a/plutus-core/plutus-core/src/PlutusCore/Bitwise/Logical.hs b/plutus-core/plutus-core/src/PlutusCore/Bitwise/Logical.hs
diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
@@ -27,6 +27,7 @@ import PlutusCore.Evaluation.Result (EvaluationResult (..))
 import PlutusCore.Pretty (PrettyConfigPlc)
 
 import PlutusCore.Bitwise.Convert as Convert
+import PlutusCore.Bitwise.Logical as Logical
 import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
 import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
 import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
@@ -152,6 +153,14 @@ data DefaultFun
     -- Conversions
     | IntegerToByteString
     | ByteStringToInteger
+    -- Logical
+    | AndByteString
+    | OrByteString
+    | XorByteString
+    | ComplementByteString
+    | ReadBit
+    | WriteBits
+    | ReplicateByteString
     deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Ix)
     deriving anyclass (NFData, Hashable, PrettyBy PrettyConfigPlc)
 
@@ -1805,21 +1814,80 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
     -- Conversions
     {- See Note [Input length limitation for IntegerToByteString] -}
     toBuiltinMeaning _semvar IntegerToByteString =
-      let integerToByteStringDenotation :: Bool -> LiteralByteSize -> Integer -> BuiltinResult BS.ByteString
-          {- The second argument is wrapped in a LiteralByteSize to allow us to interpret it as a size during
-             costing.  It appears as an integer in UPLC: see Note [Integral types as Integer]. -}
-          integerToByteStringDenotation b (LiteralByteSize w) n = integerToByteStringWrapper b w n
-          {-# INLINE integerToByteStringDenotation #-}
-        in makeBuiltinMeaning
-          integerToByteStringDenotation
-          (runCostingFunThreeArguments . paramIntegerToByteString)
+        let integerToByteStringDenotation :: Bool -> LiteralByteSize -> Integer -> BuiltinResult BS.ByteString
+            {- The second argument is wrapped in a LiteralByteSize to allow us to interpret it as a size during
+               costing.  It appears as an integer in UPLC: see Note [Integral types as Integer]. -}
+            integerToByteStringDenotation b (LiteralByteSize w) n = integerToByteStringWrapper b w n
+            {-# INLINE integerToByteStringDenotation #-}
+        in makeBuiltinMeaning
+            integerToByteStringDenotation
+            (runCostingFunThreeArguments . paramIntegerToByteString)
+
     toBuiltinMeaning _semvar ByteStringToInteger =
-      let byteStringToIntegerDenotation :: Bool -> BS.ByteString -> Integer
-          byteStringToIntegerDenotation = byteStringToIntegerWrapper
-          {-# INLINE byteStringToIntegerDenotation #-}
+        let byteStringToIntegerDenotation :: Bool -> BS.ByteString -> Integer
+            byteStringToIntegerDenotation = byteStringToIntegerWrapper
+            {-# INLINE byteStringToIntegerDenotation #-}
         in makeBuiltinMeaning
             byteStringToIntegerDenotation
             (runCostingFunTwoArguments . paramByteStringToInteger)
+
+    -- Logical
+    toBuiltinMeaning _semvar AndByteString =
+        let andByteStringDenotation :: Bool -> BS.ByteString -> BS.ByteString -> BS.ByteString
+            andByteStringDenotation = Logical.andByteString
+            {-# INLINE andByteStringDenotation #-}
+        in makeBuiltinMeaning
+            andByteStringDenotation
+            (runCostingFunThreeArguments . unimplementedCostingFun)
+
+    toBuiltinMeaning _semvar OrByteString =
+        let orByteStringDenotation :: Bool -> BS.ByteString -> BS.ByteString -> BS.ByteString
+            orByteStringDenotation = Logical.orByteString
+            {-# INLINE orByteStringDenotation #-}
+        in makeBuiltinMeaning
+            orByteStringDenotation
+            (runCostingFunThreeArguments . unimplementedCostingFun)
+
+    toBuiltinMeaning _semvar XorByteString =
+        let xorByteStringDenotation :: Bool -> BS.ByteString -> BS.ByteString -> BS.ByteString
+            xorByteStringDenotation = Logical.xorByteString
+            {-# INLINE xorByteStringDenotation #-}
+        in makeBuiltinMeaning
+            xorByteStringDenotation
+            (runCostingFunThreeArguments . unimplementedCostingFun)
+
+    toBuiltinMeaning _semvar ComplementByteString =
+        let complementByteStringDenotation :: BS.ByteString -> BS.ByteString
+            complementByteStringDenotation = Logical.complementByteString
+            {-# INLINE complementByteStringDenotation #-}
+        in makeBuiltinMeaning
+            complementByteStringDenotation
+            (runCostingFunOneArgument . unimplementedCostingFun)
+
+    toBuiltinMeaning _semvar ReadBit =
+        let readBitDenotation :: BS.ByteString -> Int -> BuiltinResult Bool
+            readBitDenotation = Logical.readBit
+            {-# INLINE readBitDenotation #-}
+        in makeBuiltinMeaning
+            readBitDenotation
+            (runCostingFunTwoArguments . unimplementedCostingFun)
+
+    toBuiltinMeaning _semvar WriteBits =
+        let writeBitsDenotation :: BS.ByteString -> [(Integer, Bool)] -> BuiltinResult BS.ByteString
+            writeBitsDenotation = Logical.writeBits
+            {-# INLINE writeBitsDenotation #-}
+        in makeBuiltinMeaning
+            writeBitsDenotation
+            (runCostingFunTwoArguments . unimplementedCostingFun)
+
+    toBuiltinMeaning _semvar ReplicateByteString =
+        let byteStringReplicateDenotation :: Int -> Word8 -> BuiltinResult BS.ByteString
+            byteStringReplicateDenotation = Logical.replicateByteString
+            {-# INLINE byteStringReplicateDenotation #-}
+        in makeBuiltinMeaning
+            byteStringReplicateDenotation
+            (runCostingFunTwoArguments . unimplementedCostingFun)
+
     -- See Note [Inlining meanings of builtins].
     {-# INLINE toBuiltinMeaning #-}
 
@@ -1947,6 +2015,14 @@ instance Flat DefaultFun where
               IntegerToByteString             -> 73
               ByteStringToInteger             -> 74
 
+              AndByteString                   -> 75
+              OrByteString                    -> 76
+              XorByteString                   -> 77
+              ComplementByteString            -> 78
+              ReadBit                         -> 79
+              WriteBits                       -> 80
+              ReplicateByteString             -> 81
+
     decode = go =<< decodeBuiltin
         where go 0  = pure AddInteger
               go 1  = pure SubtractInteger
@@ -2023,6 +2099,13 @@ instance Flat DefaultFun where
               go 72 = pure Blake2b_224
               go 73 = pure IntegerToByteString
               go 74 = pure ByteStringToInteger
+              go 75 = pure AndByteString
+              go 76 = pure OrByteString
+              go 77 = pure XorByteString
+              go 78 = pure ComplementByteString
+              go 79 = pure ReadBit
+              go 80 = pure WriteBits
+              go 81 = pure ReplicateByteString
               go t  = fail $ "Failed to decode builtin tag, got: " ++ show t
 
     size _ n = n + builtinTagWidth
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/CommuteFnWithConst.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/CommuteFnWithConst.hs
@@ -129,3 +129,12 @@ isCommutative = \case
   MkNilPairData                   -> False
   IntegerToByteString             -> False
   ByteStringToInteger             -> False
+  -- Currently, this requires commutativity in all arguments, which the
+  -- logical operations are not.
+  AndByteString                   -> False
+  OrByteString                    -> False
+  XorByteString                   -> False
+  ComplementByteString            -> False
+  ReadBit                         -> False
+  WriteBits                       -> False
+  ReplicateByteString             -> False
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Conversion.hs b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Conversion.hs
@@ -36,11 +36,10 @@ import Test.Tasty (TestTree)
 import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)
 import Text.Show.Pretty (ppShow)
 
--- Properties and examples directly from CIP-0087:
+-- Properties and examples directly from CIP-121:
 --
--- - https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX#builtinintegertobytestring
--- - https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX#builtinbytestringtointeger
-
+-- - https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-0121#builtinintegertobytestring
+-- - https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-0121#builtinbytestringtointeger
 
 -- lengthOfByteString (integerToByteString e d 0) = d
 i2bProperty1 :: PropertyT IO ()

diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Definition.hs b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Definition.hs
@@ -27,6 +27,7 @@ import PlutusCore.Pretty
 import PlutusPrelude
 import UntypedPlutusCore.Evaluation.Machine.Cek
 
+import PlutusCore qualified as PLC
 import PlutusCore.Examples.Builtins
 import PlutusCore.Examples.Data.Data
 import PlutusCore.StdLib.Data.Bool
@@ -39,20 +40,19 @@ import PlutusCore.StdLib.Data.ScottList qualified as Scott
 import PlutusCore.StdLib.Data.ScottUnit qualified as Scott
 import PlutusCore.StdLib.Data.Unit
 
-import Evaluation.Builtins.BLS12_381 (test_BLS12_381)
-import Evaluation.Builtins.Common
-import Evaluation.Builtins.Conversion qualified as Conversion
-import Evaluation.Builtins.SignatureVerification (ecdsaSecp256k1Prop, ed25519_VariantAProp,
-                                                  ed25519_VariantBProp, ed25519_VariantCProp,
-                                                  schnorrSecp256k1Prop)
-
-
 import Control.Exception
 import Data.ByteString (ByteString, pack)
 import Data.DList qualified as DList
 import Data.Proxy
 import Data.String (IsString (fromString))
 import Data.Text (Text)
+import Evaluation.Builtins.BLS12_381 (test_BLS12_381)
+import Evaluation.Builtins.Common
+import Evaluation.Builtins.Conversion qualified as Conversion
+import Evaluation.Builtins.Laws qualified as Laws
+import Evaluation.Builtins.SignatureVerification (ecdsaSecp256k1Prop, ed25519_VariantAProp,
+                                                  ed25519_VariantBProp, ed25519_VariantCProp,
+                                                  schnorrSecp256k1Prop)
 import Hedgehog hiding (Opaque, Size, Var)
 import Hedgehog.Gen qualified as Gen
 import Hedgehog.Range qualified as Range
@@ -889,7 +889,7 @@ test_Conversion =
         -- appendByteString (integerToByteString False 0 q)
         -- (integerToByteString False 0 r)
         testPropertyNamed "property 7" "i2b_prop7" . property $ Conversion.i2bProperty7,
-        testGroup "CIP-0087 examples" Conversion.i2bCipExamples,
+        testGroup "CIP-121 examples" Conversion.i2bCipExamples,
         testGroup "Tests for integerToByteString size limit" Conversion.i2bLimitTests
         ],
       testGroup "ByteString -> Integer" [
@@ -899,10 +899,56 @@ test_Conversion =
         testPropertyNamed "property 2" "b2i_prop2" . property $ Conversion.b2iProperty2,
         -- integerToByteString b (lengthOfByteString bs) (byteStringToInteger b bs) = bs
         testPropertyNamed "property 3" "b2i_prop3" . property $ Conversion.b2iProperty3,
-        testGroup "CIP-0087 examples" Conversion.b2iCipExamples
+        testGroup "CIP-121 examples" Conversion.b2iCipExamples
         ]
       ]
 
+-- Tests for the logical operations, as per [CIP-122](https://github.com/mlabs-haskell/CIPs/blob/koz/logic-ops/CIP-0122/CIP-0122.md)
+test_Logical :: TestTree
+test_Logical =
+  adjustOption (\x -> max x . HedgehogTestLimit . Just $ 4000) .
+  testGroup "Logical" $ [
+    testGroup "andByteString" [
+      Laws.abelianSemigroupLaws "truncation" PLC.AndByteString False,
+      Laws.idempotenceLaw "truncation" PLC.AndByteString False,
+      Laws.absorbtionLaw "truncation" PLC.AndByteString False "",
+      Laws.leftDistributiveLaw "truncation" "itself" PLC.AndByteString PLC.AndByteString False,
+      Laws.leftDistributiveLaw "truncation" "OR" PLC.AndByteString PLC.OrByteString False,
+      Laws.leftDistributiveLaw "truncation" "XOR" PLC.AndByteString PLC.XorByteString False,
+      Laws.abelianMonoidLaws "padding" PLC.AndByteString True "",
+      Laws.distributiveLaws "padding" PLC.AndByteString True
+      ],
+    testGroup "orByteString" [
+      Laws.abelianSemigroupLaws "truncation" PLC.OrByteString False,
+      Laws.idempotenceLaw "truncation" PLC.OrByteString False,
+      Laws.absorbtionLaw "truncation" PLC.OrByteString False "",
+      Laws.leftDistributiveLaw "truncation" "itself" PLC.OrByteString PLC.OrByteString False,
+      Laws.leftDistributiveLaw "truncation" "AND" PLC.OrByteString PLC.AndByteString False,
+      Laws.abelianMonoidLaws "padding" PLC.OrByteString True "",
+      Laws.distributiveLaws "padding" PLC.OrByteString True
+      ],
+    testGroup "xorByteString" [
+      Laws.abelianSemigroupLaws "truncation" PLC.XorByteString False,
+      Laws.absorbtionLaw "truncation" PLC.XorByteString False "",
+      Laws.xorInvoluteLaw,
+      Laws.abelianMonoidLaws "padding" PLC.XorByteString True ""
+      ],
+    testGroup "bitwiseLogicalComplement" [
+      Laws.complementSelfInverse,
+      Laws.deMorgan
+      ],
+    testGroup "bit reading and modification" [
+      Laws.getSet,
+      Laws.setGet,
+      Laws.setSet,
+      Laws.writeBitsHomomorphismLaws
+      ],
+    testGroup "replicateByteString" [
+      Laws.replicateHomomorphismLaws,
+      Laws.replicateIndex
+      ]
+    ]
+
 test_definition :: TestTree
 test_definition =
     testGroup "definition"
@@ -938,4 +984,5 @@ test_definition =
         , test_Version
         , test_ConsByteString
         , test_Conversion
+        , test_Logical
         ]