Bitwise costing (PLT-8790) #5733

kwxm · 2024-01-19T12:08:14Z

This extends the costing infrastructure to handle the ByteStringToInteger and IntegerToByteString functions added in #5654. The CPU usage of these is quadratic at the moment, and that required quite a few additions. Once we no longer he tavo support GHC 8.10 it's hoped that we can have a linear-time implementation instead: this won't require any further changes to the costing infrastructure since a linear function can be represented by a quadratic function with a zero coefficient (or more likely a very small coefficient) in degree 2. Also, IntegerToByteString will currently fail if the length of the output bytestring would be greater than 8000 (accurate costing becomes difficult beyond this point). We may remove that limit when the implementation is updated, and if we do that will require a new semantic variant.

IntegerToByteString takes a size argument that says how long the output should be, and that required another small extension so that the value of that argument is treated as a literal size for memory costing purposes (ie we don't take the memory usage to be the size of that argument, but the argument itself).

I've added costing benchmarks and run them, and added the resulting data to builtinCostModel.json. The benchmarks may still need a little tuning, but that can be done later.

I also fixed a few small things that I ran into related to plugin integration.

kwxm · 2024-01-23T11:55:43Z

@michaelpj @effectfully I've now moved the size checks out of Default.Builtins and back into Bitwise.Conversions and added some tests, so you might want to take another look.

kwxm · 2024-01-23T11:59:08Z

The maximum size for outputs of integerToByteString is 8000, but maybe 8192 (=8K) would be better.

kwxm · 2024-01-23T12:50:52Z

plutus-core/plutus-core/src/PlutusCore/Bitwise/Convert.hs

+   integerToByteString in Plutus Core so that we can continue to support the
+   current behaviour for old scripts.-}
+integerToByteStringMaximumOutputLength :: Integer
+integerToByteStringMaximumOutputLength = 8000


Maybe 8192 would be better.

I'd prefer that indeed, because 8000 feels entirely arbitrary and 8K somehow feels less arbitrary, but it's again my craziness is talking. 8192 also gives the reader a hint of what this is about.

I'd prefer that indeed, because 8000 feels entirely arbitrary

Oh well, I suppose so. I'll have to change a lot of the conformance tests now too [goes off grumbling].

…se-conversions

effectfully

Great tests.

effectfully · 2024-01-25T22:08:20Z

plutus-core/plutus-core/src/PlutusCore/Bitwise/Convert.hs

+  -- Int (so it should be at most 2^29, which is the largest bound that GHC
+  -- guarantees).


Big kudos for that precision. But I think it doesn't apply to us, because we simply refuse to build on a non-64 machine. @michaelpj is that right? I'm talking about #if WORD_SIZE_IN_BITS == 64 in Universe.hs.

Yeah, I don't think we need to worry about 32bit platforms.

Yep, this is right.

OK, I've removed that and just said it should fit into an Int.

effectfully · 2024-01-25T22:13:10Z

plutus-core/plutus-core/src/PlutusCore/Bitwise/Convert.hs

+   has integerLog2 but only in GHC >= 9.0. We should use the library function
+   instead when we stop supporting 8.10. -}
+integerLog2 :: Integer -> Int
+integerLog2 !i = I# (integerLog2# i)


I wonder what's the story behind that bang, but I understand that you just copied that stuff from ghc-bignum and I agree it's the right thing to do to copy it verbatim.

effectfully · 2024-01-25T22:16:13Z

plutus-core/plutus-core/src/PlutusCore/Bitwise/Convert.hs

+      emit . pack $ "integerToByteString: input too long (maximum is 2^"
+               ++ (show (8 * integerToByteStringMaximumOutputLength))
+               ++ "-1)"
+      emit $ "Length required: " <> (pack . show $ bytesRequiredFor input)
      evaluationFailure
  | otherwise = let endianness = endiannessArgToByteOrder endiannessArg in
    -- We use fromIntegral here, despite advice to the contrary in general when defining builtin


BTW, whoever wrote this comment, thank you a ton.

effectfully · 2024-01-25T22:17:48Z

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

@@ -1800,20 +1801,23 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
            (runCostingFunOneArgument . paramBlake2b_224)

    -- Conversions
+    {- See Note [Input length limitation for IntegerToByteString] -}


Probably not worth referencing it from here anymore, since that logic is now packed within integerToByteStringWrapper?

effectfully · 2024-01-25T22:18:23Z

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

    toBuiltinMeaning _semvar ByteStringToInteger =
      let byteStringToIntegerDenotation :: Bool -> BS.ByteString -> Integer
          byteStringToIntegerDenotation = byteStringToIntegerWrapper
+          {-# INLINE byteStringToIntegerDenotation #-}


effectfully · 2024-01-25T22:38:23Z

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExMemoryUsage.hs

 -- | Calculate a 'CostingInteger' for the given 'Integer'.
 memoryUsageInteger :: Integer -> CostingInteger
 -- integerLog2# is unspecified for 0 (but in practice returns -1)
+-- ^ This changed with GHC 9.2: it now returns 0.  It's probably safest if we
+-- keep this special case for the time being though.


Good comment.

effectfully · 2024-01-25T22:39:28Z

plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Conversion.hs

+                      let actualExp = mkIterAppNoAnn (builtin () PLC.IntegerToByteString) [
+                                       mkConstant @Bool () endianness,
+                                       mkConstant @Integer () 0,
+                                       mkConstant @Integer () maxAcceptableInput
+                                      ]


Nit: I'd perhaps abstract into a mkIntegerToByteString helper or something. But it's OK.

👍 Good idea.

effectfully · 2024-01-25T22:42:41Z

plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs

+    -- Bitwise operations
+    defineBuiltinTerm annMayInline 'Builtins.integerToByteString $ mkBuiltin PLC.IntegerToByteString
+    defineBuiltinTerm annMayInline 'Builtins.byteStringToInteger $ mkBuiltin PLC.ByteStringToInteger


I don't think you need these three lines? The two builtins are handled within the for_ enumerate block below, it should be safe to remove them from here. Please try doing that and let's see if CI agrees with my reasoning.

I wonder if we should have a test catching this situation where the same builtin is defined twice. @michaelpj do you have an opinion?

I think we could just make it throw if you redefine the same name. There's really no reason to do that.

I don't think you need these three lines?

Ooh, well-spotted. Maybe we should have some tests that make sure that you can actually use all of the builtins in Haskell code: it's quite easy to forget to add something here or in plutus-tx (although here we've added something too often).

What happens if you define something twice with different semantics here? Does the later definition override the earlier one?

effectfully · 2024-01-25T23:01:54Z

plutus-conformance/agda/Spec.hs

+failingTests =
+    [
+     --- byteStringToInteger
+      "test-cases/uplc/evaluation/builtin/semantics/byteStringToInteger/big-endian/all-zeros"


It says failingTests, but all-zeros isn't a failing test? I'm confused.

It says failingTests, but all-zeros isn't a failing test? I'm confused.

These do fail in the metatheory because in this branch the Agda code doesn't know about the new builtins yet. They'll be added in a PR that'll appear shortly (and which I should have done before this one). In that branch failingTests is empty.

If you run the agda-conformance tests you get errors like

big-endian all-zeros: FAIL (expected) Agda: unreachable code reached. CallStack (from HasCallStack): error, called at /blah/blah/blah/plutus-metatheory-0.1.0.0/build/MAlonzo/RTE.hs:44:23 in plutus-metatheory-0.1.0.0-inplace:MAlonzo.RTE (expected failure)

I see, thank you for the explanation.

effectfully · 2024-01-25T23:11:57Z

...mantics/integerToByteString/little-endian/bounded/maximum-width-zero/maximum-width-zero.uplc

+-- Check that we can encode zero using the maximum width (8000).
+(program 1.0.1
+ [(builtin integerToByteString) (con bool False) (con integer 8000) (con integer 0)]


If you're going to make it 8192, don't forget to update this test. And I guess plenty of other ones. So maybe it's easier to just keep 8000.

zliu41

Great work.

zliu41 · 2024-01-25T21:42:29Z

...es/uplc/evaluation/builtin/semantics/byteStringToInteger/big-endian/all-zeros/all-zeros.uplc

@@ -0,0 +1,4 @@
+-- A bytestring consisting entirely of zeros decodes to 0.
+(program 1.0.1


This should be 1.1.0? There's no 1.0.1.

Oops. I'll just make it 1.0.0 since that's what all the others have and this doesn't depend on 1.1.0 behaviour.

zliu41 · 2024-01-25T23:48:54Z

plutus-tx/src/PlutusTx/Builtins.hs

@@ -603,13 +603,13 @@ bls12_381_finalVerify a b = fromBuiltin (BI.bls12_381_finalVerify a b)

 -- | Convert a 'BuiltinInteger' into a 'BuiltinByteString', as described in
 -- [CIP-0087](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX).
-{-# INLINEABLE integerToByteString #-}
+{-# INLINABLE integerToByteString #-}
 integerToByteString :: Bool -> Integer -> Integer -> BuiltinByteString


Would it be better to take an Endianness type instead of Bool, and newtype the first Integer parameter?
At the very least there should be Haddock on the parameters

This is a good point, for the "exposed" version of the builtins we can indeed give a nicer interface again.

Yes, that'd be quite helpful.

OK, I've made the plutus-tx versions take a ByteOrder argument.

zliu41 · 2024-01-25T23:53:00Z

plutus-core/cost-model/budgeting-bench/Benchmarks/Bitwise.hs

+
+-- Make an integer of size n which encodes to 0xFF...FF
+allFF :: Int -> Integer
+allFF n = 256^(8*n) - 1


What is 256? Is it not 2^(8*n) - 1?

What is 256? Is it not 2^(8*n) - 1?

No, that's right. We're looking for size n here, which means 8* n bytes (thanks again to the infuriating fact that we measure sizes in 8-byte words). Since that's a number of bytes, the total number of bits is 8 * 8 * n, and 2^(8 * 8 * n) = 256^(8 * n) is 1000...000 with (64 * n) zero bits. Subtracting 1 from that removes the 1 at the front and changes all the remaining bits to 1, so you've got (64 * n) 1 bits, or (8 * n) 0xFF bytes, which is what you want. Thanks for making me check though: it's very easy to get this kind of thing wrong.

Probably the easiest way to check this is to try n=2 or something.

zliu41 · 2024-01-26T00:16:14Z

plutus-core/plutus-core/src/PlutusCore/Bitwise/Convert.hs

+  -- Int (so it should be at most 2^29, which is the largest bound that GHC
+  -- guarantees).


Yeah, I don't think we need to worry about 32bit platforms.

kwxm · 2024-01-26T10:21:02Z

Oh, I seem to have accidentally merged the conformance tests with this PR a few days ago when I was trying to do the opposite. That's a bit confusing.

kwxm · 2024-01-26T16:15:52Z

Right, I'm going to merge this while the going's good.

kozross and others added 30 commits November 22, 2023 13:51

Move conversion code into Plutus Core

0dc2637

Merge branch 'master' into koz/cip-0087

94757e7

Documentation and notes on implementations

77b606f

Wrap implementations into builtins

a8798ad

Merge branch 'master' into koz/cip-0087

1b942c5

Properties as per CIP-0087

ea205dd

CIP-0087 examples as tests

3bc9afa

Merge branch 'master' into koz/cip-0087

1376602

Add new builtins to PlutusTx

747fe3b

Document fromIntegral usage as a note

5a6c93a

Changelogs for CIP-0087 primitives

d3e1a49

Merge branch 'master' into koz/cip-0087

4e1ef6b

Ensure conversions don't break on too-large arguments

1b6f849

Ensure that conversions are available in V3

e9be20a

Merge branch 'master' into koz/cip-0087

d9ff42f

Merge branch 'master' into koz/cip-0087

2016ad1

Remove unnecessary pragmata on tests

fa90942

Fix overly-long test names, clarify test meaning in comments

db91938

CIP link consistency

ab94f21

Merge branch 'master' into koz/cip-0087

d0594ca

Re-order integerToByteString arguments, avoid unnecessary padding

0b8aad3

Better documentation for implementations

dfd2fa3

Correct properties for ByteStringToInteger

d4bc659

Merge branch 'master' into koz/cip-0087

77f026a

Address feedback

f2a7c26

Integer/ByteString conversion costing experiments

1ec3b1f

Turn off warning

dd466d0

Turn off warning

b9d6d1f

Merge branch 'master' into kwxm/bitwise-costing

8c7e0cf

Initial costing for bitwise conversions

3830e98

kwxm added 2 commits January 23, 2024 11:35

Move size limit check back to Convert.hs and add some tests

9126d67

Move size limit check back to Convert.hs and add some tests

3bf0494

kwxm requested review from effectfully and michaelpj January 23, 2024 11:54

Workaround for integerLog2 missing in GHC 8.10

bd4f0d5

kwxm commented Jan 23, 2024

View reviewed changes

kwxm added 10 commits January 23, 2024 12:51

Workaround for integerLog2 missing in GHC 8.10

485eb44

Workaround for integerLog2 missing in GHC 8.10

0f87af6

Merge branch 'kwxm/bitwise-costing' into kwxm/conformance-tests/bitwi…

045ce5a

…se-conversions

Add some more test cases

b9d0dea

More test cases

3298e74

More test cases

f88088c

More tests

f8c49cf

More test cases

e1bdeeb

Formatting

7978471

Update comment

6d08772

effectfully approved these changes Jan 25, 2024

View reviewed changes

zliu41 approved these changes Jan 26, 2024

View reviewed changes

kwxm added 4 commits January 26, 2024 10:43

Fix PLC version number in bitwise conformance tests

b771a3f

Update golden tests for new maximum width

6fa30b6

Address PR comments

4ca7889

Test output mysteriously rearranged again

4da3e0a

kwxm merged commit e3de827 into master Jan 26, 2024
4 checks passed

kwxm deleted the kwxm/bitwise-costing branch January 26, 2024 16:16

kwxm mentioned this pull request Jan 26, 2024

Conformance tests for bitwise conversions #5744

Merged

kwxm mentioned this pull request Feb 15, 2024

memoryUsage of empty ByteString is 1 instead of 0 #5775

Closed

		-- Int (so it should be at most 2^29, which is the largest bound that GHC
		-- guarantees).

		@@ -0,0 +1,4 @@
		-- A bytestring consisting entirely of zeros decodes to 0.
		(program 1.0.1

Bitwise costing (PLT-8790) #5733

Bitwise costing (PLT-8790) #5733

Conversation

kwxm commented Jan 19, 2024

kwxm commented Jan 23, 2024 • edited Loading

kwxm commented Jan 23, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

effectfully left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kwxm Jan 26, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zliu41 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kwxm Jan 26, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kwxm commented Jan 26, 2024 • edited Loading

kwxm commented Jan 26, 2024

kwxm commented Jan 23, 2024 •

edited

Loading

kwxm commented Jan 23, 2024 •

edited

Loading

kwxm Jan 26, 2024 •

edited

Loading

kwxm Jan 26, 2024 •

edited

Loading

kwxm commented Jan 26, 2024 •

edited

Loading