Conformance tests for replicateByte (#6392)

* Conformance for replicateByte

* Fix goldens for merge

* Fix for Agda conformance

* Fix Agda interface to replicateBytes; add conformance tests

* Note

* Note

* Delete trailing whitespace (again)

* Initial draft

* Tests

* Benchmark

* Ready for PR

* Fix benchmarks to avoid CTE

* Golden tests for 8-queens

* Goldens for Ed25519

* Set Ed25519 benchmark to be unbuildable for now

* Change INLINE to INLINEABLE in benchmarks to avoid code blowout

* Refactor Ed25519 to make use of SHA512 clearer

* Fix warnings about plutus-tx-plugin

* Refactor some definitions to be local to checkValid

* Refactor, link to SHA512 RFC

* Use liftCodeDef instead of compile for constants

* Clarify where the Ed25519 implementation came from, remove useless comment

* Fix merge

* Remove unnecessary dependency

---------

Co-authored-by: Koz Ross <koz.ross@retro-freedom.nz>

plutus-conformance/agda/Spec.hs

@@ -119,7 +119,13 @@ failingEvaluationTests = []
 -}
 failingBudgetTests :: [FilePath]
 failingBudgetTests =
-  [ "test-cases/uplc/evaluation/builtin/semantics/writeBits/case-11"
+  -- These currently fail because the Agda code doesn't know about alternative
+  -- size measures used by `replicateByte` and `writeBits`: see
+  -- https://github.com/IntersectMBO/plutus/pull/6368.  Some of the budget tests
+  -- do pass, either because evaluation fails or because two different size
+  -- measures happen to be the same for small inputs.
+  [ "test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-7"
+  , "test-cases/uplc/evaluation/builtin/semantics/writeBits/case-11"
   , "test-cases/uplc/evaluation/builtin/semantics/writeBits/case-12"
   , "test-cases/uplc/evaluation/builtin/semantics/writeBits/case-13"
   , "test-cases/uplc/evaluation/builtin/semantics/writeBits/case-14"

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-1/case-1.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer -1) ] (con integer 0) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-1/case-1.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-1/case-1.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-2/case-2.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer -1) ] (con integer 3) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-2/case-2.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-2/case-2.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-3/case-3.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer 1) ] (con integer -1) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-3/case-3.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-3/case-3.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-4/case-4.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer 1) ] (con integer 256) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-4/case-4.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-4/case-4.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-5/case-5.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer 4) ] (con integer -1) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-5/case-5.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-5/case-5.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-6/case-6.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer 4) ] (con integer 256) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-6/case-6.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-6/case-6.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-7/case-7.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer 0) ] (con integer 255) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-7/case-7.uplc.budget.expected

@@ -0,0 +1,2 @@
+({cpu: 260294
+| mem: 601})

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-7/case-7.uplc.expected

@@ -0,0 +1 @@
+(program 1.0.0 (con bytestring #))

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-8/case-8.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ (builtin replicateByte) (con integer 4) ] (con integer 255) ])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-8/case-8.uplc.budget.expected

@@ -0,0 +1,2 @@
+({cpu: 260453
+| mem: 602})

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-8/case-8.uplc.expected

@@ -0,0 +1 @@
+(program 1.0.0 (con bytestring #ffffffff))

plutus-metatheory/src/Builtin.lagda.md

@@ -494,6 +494,19 @@ postulate
 ### What builtin operations should be compiled to if we compile to Haskell
 
 ```
+{- Note [Fixed-width integral types in builtins in Agda].  Many of the
+   denotations in PlutusCore.Default.Builtins involve arguments which are of
+   fixed-width integral types such as Int or Word8. These all appear as
+   `integer` in Plutus Core, and the builtin machinery handles the conversion
+   from Haskell's `Integer` (the underlying type of `integer`) to the
+   appropriate type automatically.  If a argument of this kind doesn't fit into
+   the bounds of the relevant type then *an error will occur* at run-time; this
+   happens for example with `consByteString`, where the first argument must be
+   in the range [0..255].  To preserve the semantics here, a bounds check must
+   be performed on `Int` arguments to builtins which expect an argument of some
+   fixed-width argument; this can be done using `toIntegralSized`, for example.
+-}
+
 {-# FOREIGN GHC {-# LANGUAGE TypeApplications #-} #-}
 {-# FOREIGN GHC import Control.Composition ((.*)) #-}
 {-# FOREIGN GHC import qualified Data.ByteString as BS #-}
@@ -537,10 +550,9 @@ postulate
 {-# FOREIGN GHC import PlutusCore.Crypto.Ed25519 #-}
 {-# FOREIGN GHC import PlutusCore.Crypto.Secp256k1 #-}
 
--- The Vasil verification functions return results wrapped in BuiltinResult, which
--- may perform a side-effect such as writing some text to a log.  The code below
--- provides an adaptor function which turns a BuiltinResult r into
--- Just r, where r is the real return type of the builtin.
+-- Some builtins return results wrapped in BuiltinResult, which may perform a side-effect such as
+-- writing some text to a log.  The code below provides an adaptor function which turns a
+-- BuiltinResult r into Just r, where r is the real return type of the builtin.
 -- TODO: deal directly with emitters in Agda?
 
 {-# FOREIGN GHC import PlutusPrelude (reoption) #-}
@@ -588,7 +600,12 @@ postulate
 {-# 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) #-}
+-- The Plutus Core version of `replicateByte n w` can fail in two ways: if n < 0 or n >= 8192 then
+-- the implementation PlutusCore.Bitwise will return BuiltinFailure; if w < 0 or w >= 256 then the
+-- denotation in `PlutusCore.Default.Builtins` will fail when the builtin machinery tries to convert
+-- it to a Word8.  We have to replicate this behaviour here. -}
+{-# COMPILE GHC replicateBYTE = \n w8 ->
+        case toIntegralSized w8 of { Nothing -> Nothing; Just w -> builtinResultToMaybe $ Bitwise.replicateByte n w } #-}
 {-# COMPILE GHC shiftBYTESTRING = Bitwise.shiftByteString #-}
 {-# COMPILE GHC rotateBYTESTRING = Bitwise.rotateByteString #-}
 {-# COMPILE GHC countSetBITS = \s -> fromIntegral $ Bitwise.countSetBits s #-}