Add the bitwise builtins to the metatheory (#6368)

* Initial metatheory for rest of bitwise builtins

* Separate lists of expected failures for evaluation tests and budget tests

* Remove temporary test data

* Fix memory usage for lists in Agda

* Forgot about haskell-steppable-conformance

* Remove suprious s

plutus-conformance/agda/Spec.hs

@@ -102,15 +102,25 @@ agdaEvalUplcProg WithoutCosting =
                          Left _          -> Nothing
                          Right namedTerm -> Just $ UPLC.Program () version namedTerm
 
-{- | Any tests here currently fail, so they are marked as expected to fail.  Once
- a fix for a test is pushed, the test will succeed and should be removed from
- this list.  The entries of the list are paths from the root of
- plutus-conformance to the directory containing the test, eg
+{- | A list of evaluation tests which are currently expected to fail.  Once a fix
+ for a test is pushed, the test will succeed and should be removed from the
+ list.  The entries of the list are paths from the root of plutus-conformance to
+ the directory containing the test, eg
  "test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger1"
 -}
-failingTests :: [FilePath]
-failingTests = []
+failingEvaluationTests :: [FilePath]
+failingEvaluationTests = []
+
+{- | A list of budget tests which are currently expected to fail.  Once a fix for
+ a test is pushed, the test will succeed and should be removed from the list.
+ The entries of the list are paths from the root of plutus-conformance to the
+ directory containing the test, eg
+ "test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger1"
+-}
+failingBudgetTests :: [FilePath]
+failingBudgetTests = []
 
 -- Run the tests: see Note [Evaluation with and without costing] above.
 main :: IO ()
-main = runUplcEvalTests (agdaEvalUplcProg WithCosting) (\dir -> elem dir failingTests)
+main = runUplcEvalTests (agdaEvalUplcProg WithCosting)
+       (flip elem failingEvaluationTests) (flip elem failingBudgetTests)

plutus-conformance/haskell-steppable/Spec.hs

@@ -9,8 +9,11 @@ import UntypedPlutusCore.Evaluation.Machine.SteppableCek qualified as SCek
 
 import Control.Lens
 
-failingTests :: [FilePath]
-failingTests = []
+failingEvaluationTests :: [FilePath]
+failingEvaluationTests = []
+
+failingBudgetTests :: [FilePath]
+failingBudgetTests = []
 
 -- | The `evaluator` for the steppable-version of the CEK machine.
 evalSteppableUplcProg :: UplcEvaluator
@@ -27,4 +30,5 @@ evalSteppableUplcProg = UplcEvaluatorWithoutCosting $ traverseOf UPLC.progTerm $
 main :: IO ()
 main =
     -- UPLC evaluation tests
-    runUplcEvalTests evalSteppableUplcProg (\dir -> elem dir failingTests)
+    runUplcEvalTests evalSteppableUplcProg
+    (flip elem failingEvaluationTests) (flip elem failingBudgetTests)

plutus-conformance/haskell/Spec.hs

@@ -24,10 +24,25 @@ evalUplcProg = UplcEvaluatorWithCosting $ \modelParams (UPLC.Program a v t) ->
             (Left _, _)                   -> Nothing
             (Right prog, CountingSt cost) -> Just (UPLC.Program a v prog, cost)
 
-failingTests :: [FilePath]
-failingTests = []
+{- | A list of evaluation tests which are currently expected to fail.  Once a fix
+ for a test is pushed, the test will succeed and should be removed from the
+ list.  The entries of the list are paths from the root of plutus-conformance to
+ the directory containing the test, eg
+ "test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger1"
+-}
+failingEvaluationTests :: [FilePath]
+failingEvaluationTests = []
+
+{- | A list of budget tests which are currently expected to fail.  Once a fix for
+ a test is pushed, the test will succeed and should be removed from the list.
+ The entries of the list are paths from the root of plutus-conformance to the
+ directory containing the test, eg
+ "test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger1"
+-}
+failingBudgetTests :: [FilePath]
+failingBudgetTests = []
 
 main :: IO ()
 main =
     -- UPLC evaluation tests
-    runUplcEvalTests evalUplcProg (\dir -> elem dir failingTests)
+    runUplcEvalTests evalUplcProg (flip elem failingEvaluationTests) (flip elem failingBudgetTests)

plutus-conformance/src/PlutusConformance/Common.hs

@@ -75,11 +75,16 @@ discoverTests
   :: UplcEvaluator -- ^ The evaluator to be tested.
   -> CostModelParams
   -> (FilePath -> Bool)
-  -- ^ A function that takes a test name and returns
-  -- whether it should be labelled as `ExpectedFailure`.
-  -> FilePath -- ^ The directory to search for tests.
+  -- ^ A function that takes a test directory and returns a Bool indicating
+  -- whether the evaluation test for the file in that directory is expected to
+  -- fail.
+  -> (FilePath -> Bool)
+  -- ^ A function that takes a test directory and returns a Bool indicating
+  -- whether the budget test for the file in that directory is expected to fail.
+  -> FilePath
+  -- ^ The directory to search for tests.
   -> IO TestTree
-discoverTests eval modelParams expectedFailureFn = go
+discoverTests eval modelParams evaluationFailureExpected budgetFailureExpected = go
   where
     go dir = do
         let name = takeBaseName dir
@@ -97,35 +102,36 @@ discoverTests eval modelParams expectedFailureFn = go
                         , testForBudget dir name (fmap snd . f modelParams)
                         ]
                     UplcEvaluatorWithoutCosting f -> testForEval dir name f
-            in
-                -- if the test is expected to fail, mark it so.
-                if expectedFailureFn dir
-                then pure $ expectFail tests
-                -- the test isn't expected to fail, make the `TestTree` as usual.
-                else pure tests
+            in pure tests
         -- has children, so it's a grouping directory
         else testGroup name <$> traverse go subdirs
     testForEval :: FilePath -> String -> UplcEvaluatorFun UplcProg -> TestTree
     testForEval dir name e =
         let goldenFilePath = dir </> name <.> "uplc.expected"
-        in goldenTest
-            (name ++ " (evaluation)")
-            -- get the golden test value
-            (expectedToProg <$> T.readFile goldenFilePath)
-            -- get the tested value
-            (getTestedValue e dir)
-            (\ x y -> pure $ compareAlphaEq x y) -- comparison function
-            (updateGoldenFile goldenFilePath) -- update the golden file
-
+            test = goldenTest
+                   (name ++ " (evaluation)")
+                   -- get the golden test value
+                   (expectedToProg <$> T.readFile goldenFilePath)
+                   -- get the tested value
+                   (getTestedValue e dir)
+                   (\ x y -> pure $ compareAlphaEq x y) -- comparison function
+                   (updateGoldenFile goldenFilePath) -- update the golden file
+        in possiblyFailingTest (evaluationFailureExpected dir) test
     testForBudget :: FilePath -> String -> UplcEvaluatorFun ExBudget -> TestTree
     testForBudget dir name e =
         let goldenFilePath = dir </> name <.> "uplc.budget.expected"
             prettyEither (Left l)  = pretty l
             prettyEither (Right r) = pretty r
-        in goldenVsDocM
-            (name ++ " (budget)")
-            goldenFilePath
-            (prettyEither <$> getTestedValue e dir)
+            test =  goldenVsDocM
+                    (name ++ " (budget)")
+                    goldenFilePath
+                    (prettyEither <$> getTestedValue e dir)
+        in possiblyFailingTest (budgetFailureExpected dir) test
+    possiblyFailingTest :: Bool -> TestTree -> TestTree
+    possiblyFailingTest failureExpected test =
+        if failureExpected
+        then expectFail test
+        else test
 
 -- | Turn the expected file content in text to a `UplcProg` unless the expected result
 -- is a parse or evaluation error.
@@ -217,14 +223,18 @@ runUplcEvalTests ::
     -> (FilePath -> Bool)
     -- ^ A function that takes a test name and returns
     -- whether it should labelled as `ExpectedFailure`.
+    -> (FilePath -> Bool)
+    -- ^ A function that takes a test name and returns
+    -- whether it should labelled as `ExpectedBudgetFailure`.
     -> IO ()
-runUplcEvalTests eval expectedFailTests = do
+runUplcEvalTests eval expectedFailTests expectedBudgetFailTests = do
     let params = fromJust defaultCostModelParamsForTesting
     tests <-
         discoverTests
             eval
             params
             expectedFailTests
+            expectedBudgetFailTests
             "test-cases/uplc/evaluation"
     defaultMain $ testGroup "UPLC evaluation tests" [tests]
 

plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs

@@ -1941,6 +1941,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         in makeBuiltinMeaning
             writeBitsDenotation
             (runCostingFunThreeArguments . paramWriteBits)
+
     toBuiltinMeaning _semvar ReplicateByte =
         let replicateByteDenotation :: NumBytesCostedAsNumWords -> Word8 -> BuiltinResult BS.ByteString
             replicateByteDenotation (NumBytesCostedAsNumWords n) w = Bitwise.replicateByte n w

plutus-metatheory/src/Algorithmic/CEK.lagda.md

@@ -319,6 +319,23 @@ BUILTIN byteStringToInteger (base $ V-con e $ V-con s) = inj₂ (V-con (BStoI e
 BUILTIN integerToByteString (base $ V-con e $ V-con w $ V-con n) with ItoBS e w n
 ... | just s = inj₂ (V-con s)
 ... | nothing = inj₁ (con (ne (^ (atomic aBytestring))))
+BUILTIN andByteString (base  $ V-con b $ V-con s $ V-con s') = inj₂ (V-con (andBYTESTRING b s s'))
+BUILTIN orByteString  (base  $ V-con b $ V-con s $ V-con s') = inj₂ (V-con (orBYTESTRING b s s'))
+BUILTIN xorByteString (base  $ V-con b $ V-con s $ V-con s') = inj₂ (V-con (xorBYTESTRING b s s'))
+BUILTIN complementByteString (base $ V-con s) = inj₂ (V-con (complementBYTESTRING s))
+BUILTIN readBit (base $ V-con s $ V-con i) with readBIT s i
+... | just r = inj₂ (V-con r)
+... | nothing  = inj₁ (con (ne (^ (atomic aBool))))
+BUILTIN writeBits (base $ V-con s $ V-con ps $ V-con us) with writeBITS s (toList ps) (toList us)
+... | just r = inj₂ (V-con r)
+... | nothing  = inj₁ (con (ne (^ (atomic aBytestring))))
+BUILTIN replicateByte (base  $ V-con l $ V-con w) with replicateBYTE l w 
+... | just r = inj₂ (V-con r)
+... | nothing  = inj₁ (con (ne (^ (atomic aBytestring))))
+BUILTIN shiftByteString (base $ V-con s $ V-con i) = inj₂ (V-con (shiftBYTESTRING s i))
+BUILTIN rotateByteString (base $ V-con s $ V-con i) = inj₂ (V-con (rotateBYTESTRING s i))
+BUILTIN countSetBits (base $ V-con  s) = inj₂ (V-con (countSetBITS s))
+BUILTIN findFirstSetBit (base $ V-con s) = inj₂ (V-con (findFirstSetBIT s))
 
 BUILTIN' : ∀ b {A}
   → ∀{tn} → {pt : tn ∔ 0 ≣ fv (signature b)}

plutus-metatheory/src/Builtin.lagda.md

@@ -132,6 +132,17 @@ data Builtin : Set where
   -- Bitwise operations
   byteStringToInteger             : Builtin
   integerToByteString             : Builtin
+  andByteString                   : Builtin
+  orByteString                    : Builtin
+  xorByteString                   : Builtin
+  complementByteString            : Builtin
+  readBit                         : Builtin
+  writeBits                       : Builtin
+  replicateByte                   : Builtin
+  shiftByteString                 : Builtin
+  rotateByteString                : Builtin
+  countSetBits                    : Builtin
+  findFirstSetBit                 : Builtin
 ```
 
 ## Signatures
@@ -300,6 +311,17 @@ sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
     signature bls12-381-finalVerify           = ∙ [ bls12-381-mlresult ↑ , bls12-381-mlresult ↑ ]⟶ bool ↑
     signature byteStringToInteger             = ∙ [ bool ↑ , bytestring ↑ ]⟶ integer ↑
     signature integerToByteString             = ∙ [ bool ↑ , integer ↑ , integer ↑ ]⟶  bytestring ↑
+    signature andByteString                   = ∙ [ bool ↑ , bytestring ↑ , bytestring ↑ ]⟶  bytestring ↑
+    signature orByteString                    = ∙ [ bool ↑ , bytestring ↑ , bytestring ↑ ]⟶  bytestring ↑
+    signature xorByteString                   = ∙ [ bool ↑ , bytestring ↑ , bytestring ↑ ]⟶  bytestring ↑
+    signature complementByteString            = ∙ [ bytestring ↑ ]⟶  bytestring ↑
+    signature readBit                         = ∙ [ bytestring ↑ , integer ↑ ]⟶  bool ↑
+    signature writeBits                       = ∙ [ bytestring ↑ , list integer , list bool ]⟶  bytestring ↑
+    signature replicateByte                   = ∙ [ integer ↑ , integer ↑ ]⟶  bytestring ↑
+    signature shiftByteString                 = ∙ [ bytestring ↑ , integer ↑ ]⟶  bytestring ↑
+    signature rotateByteString                = ∙ [ bytestring ↑ , integer ↑ ]⟶  bytestring ↑
+    signature countSetBits                    = ∙ [ bytestring ↑ ]⟶  integer ↑
+    signature findFirstSetBit                 = ∙ [ bytestring ↑ ]⟶  integer ↑
 
 open SugaredSignature using (signature) public
 
@@ -390,6 +412,17 @@ Each Agda built-in name must be mapped to a Haskell name.
                                           | Blake2b_224
                                           | ByteStringToInteger
                                           | IntegerToByteString
+                                          | AndByteString
+                                          | OrByteString
+                                          | XorByteString
+                                          | ComplementByteString
+                                          | ReadBit
+                                          | WriteBits
+                                          | ReplicateByte
+                                          | ShiftByteString
+                                          | RotateByteString
+                                          | CountSetBits
+                                          | FindFirstSetBit
                                           ) #-}
 ```
 
@@ -445,6 +478,17 @@ postulate
   BLAKE2B-224               : ByteString → ByteString
   BStoI                     : Bool -> ByteString -> Int
   ItoBS                     : Bool -> Int -> Int -> Maybe ByteString
+  andBYTESTRING             : Bool -> ByteString -> ByteString -> ByteString
+  orBYTESTRING              : Bool -> ByteString -> ByteString -> ByteString
+  xorBYTESTRING             : Bool -> ByteString -> ByteString -> ByteString
+  complementBYTESTRING      : ByteString -> ByteString
+  readBIT                   : ByteString -> Int -> Maybe Bool
+  writeBITS                 : ByteString -> List Int -> List Bool -> Maybe ByteString
+  replicateBYTE             : Int -> Int -> Maybe ByteString
+  shiftBYTESTRING           : ByteString -> Int -> ByteString
+  rotateBYTESTRING          : ByteString -> Int -> ByteString
+  countSetBITS              : ByteString -> Int
+  findFirstSetBIT           : ByteString -> Int
 ```
 
 ### What builtin operations should be compiled to if we compile to Haskell
@@ -535,9 +579,20 @@ postulate
 {-# COMPILE GHC KECCAK-256 = Hash.keccak_256 #-}
 {-# COMPILE GHC BLAKE2B-224 = Hash.blake2b_224 #-}
 
-{-# FOREIGN GHC import PlutusCore.Bitwise qualified as Convert #-}
-{-# COMPILE GHC BStoI = Convert.byteStringToIntegerWrapper #-}
-{-# COMPILE GHC ItoBS = \e w n -> builtinResultToMaybe $ Convert.integerToByteStringWrapper e w n #-}
+{-# FOREIGN GHC import PlutusCore.Bitwise qualified as Bitwise #-}
+{-# COMPILE GHC BStoI = Bitwise.byteStringToIntegerWrapper #-}
+{-# COMPILE GHC ItoBS = \e w n -> builtinResultToMaybe $ Bitwise.integerToByteStringWrapper e w n #-}
+{-# COMPILE GHC andBYTESTRING = Bitwise.andByteString #-}
+{-# COMPILE GHC orBYTESTRING = Bitwise.orByteString #-}
+{-# COMPILE GHC xorBYTESTRING = Bitwise.xorByteString #-}
+{-# COMPILE GHC complementBYTESTRING = Bitwise.complementByteString #-}
+{-# COMPILE GHC readBIT = \s n -> builtinResultToMaybe $ Bitwise.readBit s (fromIntegral n) #-}
+{-# COMPILE GHC writeBITS = \s ps us -> builtinResultToMaybe $ Bitwise.writeBits s (fmap fromIntegral ps) us #-}
+{-# COMPILE GHC replicateBYTE = \n w8 -> builtinResultToMaybe $ Bitwise.replicateByte (fromIntegral n) (fromIntegral w8) #-}
+{-# COMPILE GHC shiftBYTESTRING = \s n -> Bitwise.shiftByteString s (fromIntegral n) #-}
+{-# COMPILE GHC rotateBYTESTRING = \s n -> Bitwise.rotateByteString s (fromIntegral n) #-}
+{-# COMPILE GHC countSetBITS = \s -> fromIntegral $ Bitwise.countSetBits s #-}
+{-# COMPILE GHC findFirstSetBIT = \s -> fromIntegral $ Bitwise.findFirstSetBit s #-}
 
 -- no binding needed for appendStr
 -- no binding needed for traceStr

plutus-metatheory/src/Cost/Model.lagda.md

@@ -28,7 +28,8 @@ open import Relation.Binary.PropositionalEquality using (refl)
 open import Utils using (List;_×_;[];_∷_;_,_;length)
 open import Data.Vec using (Vec;[];_∷_;sum;foldr;lookup;map)
 open import Cost.Base
-open import Cost.Raw renaming (mkLinearFunction to mkLF; mkOneVariableQuadraticFunction to mkQF1; mkTwoVariableQuadraticFunction to mkQF2)
+open import Cost.Raw renaming (mkLinearFunction to mkLF; mkTwoVariableLinearFunction to mkLF2;
+  mkOneVariableQuadraticFunction to mkQF1; mkTwoVariableQuadraticFunction to mkQF2)
 open import Cost.Size using () renaming (defaultValueMeasure to sizeOf)
 open import Builtin using (Builtin;arity;builtinList;showBuiltin;decBuiltin)
 open import Builtin.Signature using (_⊢♯)
@@ -73,11 +74,13 @@ data CostingModel : ℕ → Set where
   minSize            : ∀{n} → Intercept → Slope → CostingModel (1 + n)
   maxSize            : ∀{n} → Intercept → Slope → CostingModel (1 + n)
    -- exactly two arguments
-  twoArgumentsLinearInXAndY      : Intercept → Slope → Slope → CostingModel 2
   twoArgumentsSubtractedSizes    : Intercept → Slope → CostingNat → CostingModel 2
   twoArgumentsConstAboveDiagonal : CostingNat → CostingModel 2 → CostingModel 2
   twoArgumentsConstBelowDiagonal : CostingNat → CostingModel 2 → CostingModel 2
   twoArgumentsConstOffDiagonal   : CostingNat → CostingModel 2 → CostingModel 2
+  -- exactly 3 arguments
+  twoArgumentsLinearInYAndZ      : Intercept → Slope → Slope → CostingModel 3
+  twoArgumentsLinearInMaxYZ      : Intercept → Slope → CostingModel 3
 ```
 
 A model of a builtin consists of a pair of costing models, one for CPU and one for memory.
@@ -119,10 +122,14 @@ runModel (addedSizes i s) xs = i + s * (sum (map sizeOf xs))
 runModel (multipliedSizes i s) xs = i + s * (prod (map sizeOf xs))
 runModel (minSize i s) xs = i + s * minimum (map sizeOf xs)
 runModel (maxSize i s) xs = i + s * maximum (map sizeOf xs)
-runModel (twoArgumentsLinearInXAndY i s₁ s₂) (x ∷ y ∷ []) =
-  let a = sizeOf x
-      b = sizeOf y
+runModel (twoArgumentsLinearInYAndZ i s₁ s₂) (_ ∷ y ∷ z ∷ []) =
+  let a = sizeOf y
+      b = sizeOf z
   in i + s₁ * a + s₂ * b
+runModel (twoArgumentsLinearInMaxYZ i s) (_ ∷ y ∷ z ∷ []) =
+  let a = sizeOf y
+      b = sizeOf z
+  in i + s * maximum (a ∷ b ∷ [])
 runModel (twoArgumentsSubtractedSizes i s min) (x ∷ y ∷ []) =
   let a = sizeOf x
       b = sizeOf y
@@ -164,6 +171,9 @@ convertRawModel {suc n} (MinSize (mkLF intercept slope)) = just (minSize interce
 convertRawModel {suc n} (MaxSize (mkLF intercept slope)) = just (maxSize intercept slope)
 convertRawModel {suc n} (LinearInX (mkLF intercept slope)) = just (linearCostIn zero intercept slope)
 convertRawModel {suc (suc n)} (LinearInY (mkLF intercept slope)) = just (linearCostIn (suc zero) intercept slope)
+convertRawModel {3} (LinearInYAndZ (mkLF2 intercept slope1 slope2)) =
+                   just (twoArgumentsLinearInYAndZ intercept slope1 slope2)
+convertRawModel {3} (LinearInMaxYZ (mkLF intercept slope)) = just (twoArgumentsLinearInMaxYZ intercept slope)
 convertRawModel {suc (suc n)} (QuadraticInY (mkQF1 c0 c1 c2)) = just (quadraticCostIn1 (suc zero) c0 c1 c2)
 convertRawModel {suc (suc (suc n))}(LinearInZ (mkLF intercept slope)) = just (linearCostIn (suc (suc zero)) intercept slope)
 convertRawModel {suc (suc (suc n))} (QuadraticInZ (mkQF1 c0 c1 c2)) = just (quadraticCostIn1 (suc (suc zero)) c0 c1 c2)