From 36311fe6293c543694299fe4bb92bfde52a46597 Mon Sep 17 00:00:00 2001 From: Kenneth MacKenzie Date: Mon, 5 Aug 2024 06:44:41 +0100 Subject: [PATCH] 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 | 24 +++-- plutus-conformance/haskell-steppable/Spec.hs | 10 +- plutus-conformance/haskell/Spec.hs | 21 ++++- .../src/PlutusConformance/Common.hs | 58 +++++++----- .../src/PlutusCore/Default/Builtins.hs | 1 + .../src/Algorithmic/CEK.lagda.md | 17 ++++ plutus-metatheory/src/Builtin.lagda.md | 61 +++++++++++- plutus-metatheory/src/Cost/Model.lagda.md | 20 +++- plutus-metatheory/src/Cost/Raw.lagda.md | 21 ++++- plutus-metatheory/src/Cost/Size.lagda.md | 11 ++- plutus-metatheory/src/Untyped/CEK.lagda.md | 92 +++++++++++++++---- 11 files changed, 262 insertions(+), 74 deletions(-) diff --git a/plutus-conformance/agda/Spec.hs b/plutus-conformance/agda/Spec.hs index b0cab2ff946..100f181fa05 100644 --- a/plutus-conformance/agda/Spec.hs +++ b/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) diff --git a/plutus-conformance/haskell-steppable/Spec.hs b/plutus-conformance/haskell-steppable/Spec.hs index b6bfcad3fe3..4ff5ebd3861 100644 --- a/plutus-conformance/haskell-steppable/Spec.hs +++ b/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) diff --git a/plutus-conformance/haskell/Spec.hs b/plutus-conformance/haskell/Spec.hs index a544b7ef95b..d944f7275c7 100644 --- a/plutus-conformance/haskell/Spec.hs +++ b/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) diff --git a/plutus-conformance/src/PlutusConformance/Common.hs b/plutus-conformance/src/PlutusConformance/Common.hs index dbf19163fda..9f477bfd384 100644 --- a/plutus-conformance/src/PlutusConformance/Common.hs +++ b/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] diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs index b3bd314cf76..2e3b17dc3b2 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs +++ b/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 diff --git a/plutus-metatheory/src/Algorithmic/CEK.lagda.md b/plutus-metatheory/src/Algorithmic/CEK.lagda.md index 321dae4a290..6b745082e68 100644 --- a/plutus-metatheory/src/Algorithmic/CEK.lagda.md +++ b/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)} diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md index 6662d72c408..4359a6123d3 100644 --- a/plutus-metatheory/src/Builtin.lagda.md +++ 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 diff --git a/plutus-metatheory/src/Cost/Model.lagda.md b/plutus-metatheory/src/Cost/Model.lagda.md index b557032b724..c255d8f4641 100644 --- a/plutus-metatheory/src/Cost/Model.lagda.md +++ b/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) diff --git a/plutus-metatheory/src/Cost/Raw.lagda.md b/plutus-metatheory/src/Cost/Raw.lagda.md index 94892f352dc..d2c9f673da8 100644 --- a/plutus-metatheory/src/Cost/Raw.lagda.md +++ b/plutus-metatheory/src/Cost/Raw.lagda.md @@ -87,6 +87,15 @@ record OneVariableQuadraticFunction : Set where {-# COMPILE GHC OneVariableQuadraticFunction = data OneVariableQuadraticFunction(OneVariableQuadraticFunction) #-} +record TwoVariableLinearFunction : Set where + constructor mkTwoVariableLinearFunction + field + intercept : CostingNat + slope1 : CostingNat + slope2 : CostingNat + +{-# COMPILE GHC TwoVariableLinearFunction = data TwoVariableLinearFunction(TwoVariableLinearFunction) #-} + record TwoVariableQuadraticFunction : Set where constructor mkTwoVariableQuadraticFunction field @@ -110,6 +119,8 @@ data RawModel : Set where LinearInY : LinearFunction → RawModel LinearInZ : LinearFunction → RawModel LiteralInYOrLinearInZ : LinearFunction → RawModel + LinearInMaxYZ : LinearFunction → RawModel + LinearInYAndZ : TwoVariableLinearFunction -> RawModel QuadraticInY : OneVariableQuadraticFunction → RawModel QuadraticInZ : OneVariableQuadraticFunction → RawModel QuadraticInXAndY : TwoVariableQuadraticFunction → RawModel @@ -118,11 +129,11 @@ data RawModel : Set where ConstBelowDiagonal : CostingNat → RawModel → RawModel ConstOffDiagonal : CostingNat → RawModel → RawModel -{-# COMPILE GHC RawModel = data Model (ConstantCost | AddedSizes | MultipliedSizes | - MinSize | MaxSize | LinearInX | LinearInY | LinearInZ | - LiteralInYOrLinearInZ | QuadraticInY | QuadraticInZ | - QuadraticInXAndY | SubtractedSizes | ConstAboveDiagonal | - ConstBelowDiagonal | ConstOffDiagonal) #-} +{-# COMPILE GHC RawModel = data Model (ConstantCost | AddedSizes | + MultipliedSizes | MinSize | MaxSize | LinearInX | LinearInY | LinearInZ | + LiteralInYOrLinearInZ | LinearInMaxYZ | LinearInYAndZ |QuadraticInY | + QuadraticInZ | QuadraticInXAndY | SubtractedSizes | ConstAboveDiagonal | + ConstBelowDiagonal | ConstOffDiagonal) #-} record CpuAndMemoryModel : Set where constructor mkCpuAndMemoryModel diff --git a/plutus-metatheory/src/Cost/Size.lagda.md b/plutus-metatheory/src/Cost/Size.lagda.md index 86776e130de..8286f41ec2e 100644 --- a/plutus-metatheory/src/Cost/Size.lagda.md +++ b/plutus-metatheory/src/Cost/Size.lagda.md @@ -61,7 +61,8 @@ postulate stringSize : String → CostingNat ``` For each constant we return the corresponding size. - +These *must* match the size functions defined in +`PlutusCore.Evaluation.Machine.ExMemoryUsage` ``` defaultConstantMeasure : TmCon → CostingNat defaultConstantMeasure (tmCon (atomic aInteger) x) = integerSize x @@ -73,13 +74,13 @@ defaultConstantMeasure (tmCon (atomic aData) d) = dataSize d defaultConstantMeasure (tmCon (atomic aBls12-381-g1-element) x) = g1ElementSize x defaultConstantMeasure (tmCon (atomic aBls12-381-g2-element) x) = g2ElementSize x defaultConstantMeasure (tmCon (atomic aBls12-381-mlresult) x) = mlResultElementSize x -defaultConstantMeasure (tmCon (list t) []) = 0 +defaultConstantMeasure (tmCon (list t) []) = 1 defaultConstantMeasure (tmCon (list t) (x ∷ xs)) = - defaultConstantMeasure (tmCon t x) - + defaultConstantMeasure (tmCon (list t) xs) + 3 + defaultConstantMeasure (tmCon t x) + + defaultConstantMeasure (tmCon (list t) xs) defaultConstantMeasure (tmCon (pair t u) (x , y)) = 1 + defaultConstantMeasure (tmCon t x) - + defaultConstantMeasure (tmCon u y) + + defaultConstantMeasure (tmCon u y) -- This is the main sizing function for Values -- It only measures constants. Other types should use models where the size diff --git a/plutus-metatheory/src/Untyped/CEK.lagda.md b/plutus-metatheory/src/Untyped/CEK.lagda.md index f3915779ca4..7257c64d936 100644 --- a/plutus-metatheory/src/Untyped/CEK.lagda.md +++ b/plutus-metatheory/src/Untyped/CEK.lagda.md @@ -58,13 +58,13 @@ data Value where V-con : (ty : TyTag) → ⟦ ty ⟧tag → Value V-delay : ∀{X} → Env X → X ⊢ → Value V-constr : (i : ℕ) → (vs : Stack Value) → Value - V-I⇒ : ∀ b {tn} - → {pt : tn ∔ 0 ≣ fv (signature b)} + V-I⇒ : ∀ b {tn} + → {pt : tn ∔ 0 ≣ fv (signature b)} → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} → BApp b pt pa → Value - V-IΠ : ∀ b - → ∀{tn tm}{pt : tn ∔ (suc tm) ≣ fv (signature b)} + V-IΠ : ∀ b + → ∀{tn tm}{pt : tn ∔ (suc tm) ≣ fv (signature b)} → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} → BApp b pt pa → Value @@ -72,13 +72,13 @@ data Value where data BApp b where base : BApp b (start (fv (signature b))) (start (args♯ (signature b))) app : ∀{tn} - {pt : tn ∔ 0 ≣ fv (signature b)} + {pt : tn ∔ 0 ≣ fv (signature b)} → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} → BApp b pt pa → Value → BApp b pt (bubble pa) - app⋆ : - ∀{tn tm} {pt : tn ∔ (suc tm) ≣ fv (signature b)} + app⋆ : + ∀{tn tm} {pt : tn ∔ (suc tm) ≣ fv (signature b)} → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} → BApp b pt pa → BApp b (bubble pt) pa @@ -131,7 +131,7 @@ lookup : ∀{Γ} → Env Γ → Γ → Value lookup (ρ ∷ v) nothing = v lookup (ρ ∷ v) (just x) = lookup ρ x -V-I : ∀ b +V-I : ∀ b → ∀{tn tm} {pt : tn ∔ tm ≣ fv (signature b)} → ∀{an am} {pa : an ∔ suc am ≣ args♯ (signature b)} → BApp b pt pa @@ -282,10 +282,10 @@ BUILTIN bData = λ { (app base (V-con bytestring b)) -> inj₂ (V-con pdata (bDATA b)) ; _ -> inj₁ userError } -BUILTIN consByteString (app (app base (V-con integer i)) (V-con bytestring b)) with cons i b +BUILTIN consByteString (app (app base (V-con integer i)) (V-con bytestring b)) with cons i b ... | just b' = inj₂ (V-con bytestring b') ... | nothing = inj₁ userError -BUILTIN consByteString _ = inj₁ userError +BUILTIN consByteString _ = inj₁ userError BUILTIN sliceByteString = λ { (app (app (app base (V-con integer st)) (V-con integer n)) (V-con bytestring b)) -> inj₂ (V-con bytestring (slice st n b)) ; _ -> inj₁ userError @@ -338,8 +338,8 @@ BUILTIN chooseList = λ ; (app (app (app (app⋆ (app⋆ base)) (V-con (list _) (_ ∷ _))) _) v) → inj₂ v ; _ -> inj₁ userError } -BUILTIN mkCons (app (app (app⋆ base) (V-con t x)) (V-con (list ts) xs)) with decTag t ts -... | yes refl = inj₂ (V-con (list ts) (x ∷ xs)) +BUILTIN mkCons (app (app (app⋆ base) (V-con t x)) (V-con (list ts) xs)) with decTag t ts +... | yes refl = inj₂ (V-con (list ts) (x ∷ xs)) ... | no _ = inj₁ userError BUILTIN mkCons _ = inj₁ userError BUILTIN headList = λ @@ -369,12 +369,12 @@ BUILTIN constrData = λ ; _ -> inj₁ userError } BUILTIN mapData = λ - { (app base (V-con (list (pair pdata pdata)) xs)) → do + { (app base (V-con (list (pair pdata pdata)) xs)) → do return (V-con pdata (MapDATA xs)) ; _ -> inj₁ userError } BUILTIN listData = λ - { (app base (V-con (list pdata) xs)) → do + { (app base (V-con (list pdata) xs)) → do return (V-con pdata (ListDATA xs)) ; _ -> inj₁ userError } @@ -391,7 +391,7 @@ BUILTIN unListData = λ ; _ -> inj₁ userError } BUILTIN equalsData = λ - { + { (app (app base (V-con pdata x)) (V-con pdata y)) → inj₂ (V-con bool (eqDATA x y)) ; _ -> inj₁ userError } @@ -424,7 +424,7 @@ BUILTIN bls12-381-G1-equal = λ ; _ -> inj₁ userError } BUILTIN bls12-381-G1-hashToGroup = λ - { (app (app base (V-con bytestring msg)) (V-con bytestring dst)) -> case BLS12-381-G1-hashToGroup msg dst of λ + { (app (app base (V-con bytestring msg)) (V-con bytestring dst)) -> case BLS12-381-G1-hashToGroup msg dst of λ { (just p) -> inj₂ (V-con bls12-381-g1-element p) ; nothing -> inj₁ userError } @@ -434,7 +434,7 @@ BUILTIN bls12-381-G1-compress = λ { (app base (V-con bls12-381-g1-element e)) -> inj₂ (V-con bytestring (BLS12-381-G1-compress e)) ; _ -> inj₁ userError } -BUILTIN bls12-381-G1-uncompress = λ +BUILTIN bls12-381-G1-uncompress = λ { (app base (V-con bytestring b)) -> case BLS12-381-G1-uncompress b of λ { (just e) -> inj₂ (V-con bls12-381-g1-element e) ; nothing -> inj₁ userError @@ -458,7 +458,7 @@ BUILTIN bls12-381-G2-equal = λ ; _ -> inj₁ userError } BUILTIN bls12-381-G2-hashToGroup = λ - { (app (app base (V-con bytestring msg)) (V-con bytestring dst)) -> case BLS12-381-G2-hashToGroup msg dst of λ + { (app (app base (V-con bytestring msg)) (V-con bytestring dst)) -> case BLS12-381-G2-hashToGroup msg dst of λ { (just p) -> inj₂ (V-con bls12-381-g2-element p) ; nothing -> inj₁ userError } @@ -468,7 +468,7 @@ BUILTIN bls12-381-G2-compress = λ { (app base (V-con bls12-381-g2-element e)) -> inj₂ (V-con bytestring (BLS12-381-G2-compress e)) ; _ -> inj₁ userError } -BUILTIN bls12-381-G2-uncompress = λ +BUILTIN bls12-381-G2-uncompress = λ { (app base (V-con bytestring b)) -> case BLS12-381-G2-uncompress b of λ { (just e) -> inj₂ (V-con bls12-381-g2-element e) ; nothing -> inj₁ userError @@ -506,6 +506,60 @@ BUILTIN integerToByteString = λ } ; _ -> inj₁ userError } +BUILTIN andByteString = λ + { (app (app (app base (V-con bool b)) (V-con bytestring s)) (V-con bytestring s')) -> inj₂ (V-con bytestring (andBYTESTRING b s s')) + ; _ -> inj₁ userError + } +BUILTIN orByteString = λ + { (app (app (app base (V-con bool b)) (V-con bytestring s)) (V-con bytestring s')) -> inj₂ (V-con bytestring (orBYTESTRING b s s')) + ; _ -> inj₁ userError + } +BUILTIN xorByteString = λ + { (app (app (app base (V-con bool b)) (V-con bytestring s)) (V-con bytestring s')) -> inj₂ (V-con bytestring (xorBYTESTRING b s s')) + ; _ -> inj₁ userError + } +BUILTIN complementByteString = λ + { (app base (V-con bytestring s)) -> inj₂ (V-con bytestring (complementBYTESTRING s)) + ; _ -> inj₁ userError + } +BUILTIN readBit = λ + { (app (app base (V-con bytestring s)) (V-con integer i)) -> case readBIT s i of λ + { (just r) -> inj₂ (V-con bool r) + ; nothing -> inj₁ userError + } + ; _ -> inj₁ userError + } +BUILTIN writeBits = λ + { (app (app (app base (V-con bytestring s)) (V-con (list integer) ps)) (V-con (list bool) us)) -> + case writeBITS s (toList ps) (toList us) of λ + { (just r) -> inj₂ (V-con bytestring r) + ; nothing -> inj₁ userError + } + ; _ -> inj₁ userError + } +BUILTIN replicateByte = λ + { (app (app base (V-con integer l)) (V-con integer w)) -> case replicateBYTE l w of λ + { (just r) -> inj₂ (V-con bytestring r) + ; nothing -> inj₁ userError + } + ; _ -> inj₁ userError + } +BUILTIN shiftByteString = λ + { (app (app base (V-con bytestring s)) (V-con integer i)) -> inj₂ (V-con bytestring (shiftBYTESTRING s i)) + ; _ -> inj₁ userError + } +BUILTIN rotateByteString = λ + { (app (app base (V-con bytestring s)) (V-con integer i)) -> inj₂ (V-con bytestring (rotateBYTESTRING s i)) + ; _ -> inj₁ userError + } +BUILTIN countSetBits = λ + { (app base (V-con bytestring s)) -> inj₂ (V-con integer (countSetBITS s)) + ; _ -> inj₁ userError + } +BUILTIN findFirstSetBit = λ + { (app base (V-con bytestring s)) -> inj₂ (V-con integer (findFirstSetBIT s)) + ; _ -> inj₁ userError + } -- Take an apparently more general index and show that it is a fully applied builtin. mkFullyAppliedBuiltin : ∀ { b }