-
Notifications
You must be signed in to change notification settings - Fork 482
Restrict Value quantities to signed 128-bit integer range #7389
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Restrict Value quantities to signed 128-bit integer range #7389
Conversation
Union with overflow detection is not mathematically associative when overflow occurs on different evaluation paths. Updated the test to: 1. Only test associativity when all intermediate operations succeed 2. Discard test cases where overflow occurs, as non-associativity is expected and correct behavior in these cases The test now validates: "IF all union operations succeed, THEN the results are equal regardless of evaluation order." Example of expected non-associativity: - v1 ∪ v2 may underflow (< -2^127), causing left path to fail - v2 ∪ v3 may succeed, allowing right path to succeed - This is correct behavior, not a bug Fixes the CI failure in PR #7389 where the test was incorrectly expecting associativity in all cases.
| {-# INLINE empty #-} | ||
|
|
||
| toList :: Value -> [(K, [(K, Integer)])] | ||
| toList :: Value -> [(K, [(K, Quantity)])] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Given we are using a single letter K for keys, it would be more consistent to use a single letter - Q or V for value.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I find K confusing. I'd rather use Key instead.
9959bc9 to
50c29ba
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks fine but please get @effectfully's approval before merging
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, even though performance can be improved. My comments are mostly nitpicking, feel free to ignore.
I don't like the AI-generated OP, as it's mostly noise. Just the Summary part would be enough, the rest is easily inferable from the code changes.
I didn't review the tests fully, will do that another time.
| {-# INLINE maxBound #-} | ||
|
|
||
| -- | Smart constructor for Quantity that validates bounds. | ||
| quantity :: Integer -> Maybe Quantity |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should perhaps use EvaluationResult instead of Maybe as the former is properly strict.
| {-# INLINEABLE decode #-} | ||
|
|
||
| instance Flat.Flat Quantity where | ||
| encode (UnsafeQuantity i) = Flat.encode i |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We normally don't encode negative quantities, what problem would such instance solve?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What you have there is a recursive function for both the encoder and the decoder. But you know the width of Quantity, you don't need any recursion there, you can do what they do for Word64 if you don't want to encode negative quantities (which you do, hence you should sprinkle ZigZag on top).
I.e. negative quantities are irrelevant, you handle them already anyway and you will keep doing so. The point is that this implementation is not efficient (and is likely not compact either).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(and is likely not compact either)
I don't think it'll make any difference in terms of size. Flat encodes natural numbers as a seqence of seven-bit blocks with the final block preceded by a 0 and all of the others preceded by a 1. If you add the zigzag thing on top I think you're going to need eight bits for numbers in [-64..63] and sixteen for numbers in [-128..--65] ∪[64..127].
| instance PrettyBy ConstConfig Value.K where | ||
| prettyBy config = prettyBy config . Value.unK | ||
|
|
||
| instance PrettyBy ConstConfig Value.Quantity where | ||
| prettyBy config = prettyBy config . Value.unQuantity | ||
|
|
||
| instance PrettyBy ConstConfig Value where | ||
| prettyBy config = prettyBy config . Value.toList |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not that it matters much, but these should be newtype-derivable.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would require data constructors to be in scope (they aren't).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh I see. Yeah I guess that makes sense.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few small changes needed
Introduce a Quantity newtype to enforce that all Value amounts are within signed 128-bit integer bounds (-(2^127) to 2^127-1). This replaces the previous unbounded Integer type for quantities. - Add Quantity newtype with UnsafeQuantity constructor - Add smart constructor `quantity` that validates bounds - Implement Bounded instance with 128-bit min/max values - Add helper functions: zeroQuantity, addQuantity - Add serialization instances (CBOR, Flat) with validation - Add Pretty instance for Quantity - Update NestedMap type alias to use Quantity instead of Integer This is a foundational change required for fixing issue #1881 where Value quantities were previously unbounded and could overflow.
Update the Value parser to validate quantity bounds and provide clear error messages when parsing fails. - Update conValue to validate quantities during parsing - Add explicit quantity bound checks with descriptive errors - Add key length validation with descriptive errors - Handle BuiltinResult pattern matching for parser failures - Remove unused TemplateHaskell and FunctionalDependencies extensions Error messages now clearly indicate whether the issue is with key length (32-byte limit) or quantity bounds (128-bit signed integer).
Comprehensively update the test suite to work with the new Quantity type and test bound validation, including using Foldable idioms for cleaner test code. - Replace ValueAmount with V.Quantity in property tests - Use arbitraryBuiltin for generating valid quantities - Add quantity validation tests for min/max bounds - Add comprehensive mixed-quantity validation test - Add test generators for out-of-bounds quantities - Update toPositiveValue to preserve quantity bounds - Simplify prop_unionAssociative with Foldable combinators: - Use `not . null` for succeeded check (BuiltinResult is Foldable) - Use `foldr const error` for extractValue - Use nested if-then-else with do-notation for clarity - Use explicit `discard` for overflow test cases - Update prop_unionCommutative to handle BuiltinResult patterns - Update all test helpers to use Quantity type The new tests ensure that: - Valid quantities within bounds are accepted - Out-of-bounds quantities are properly rejected - Mixed valid/invalid quantities are handled correctly The Foldable approach in union tests reduces code while maintaining the same semantics and properly handling overflow cases.
Update the UnionValue builtin signature to reflect that it now returns BuiltinResult Value instead of Value, enabling proper error handling for overflow cases. - Update unionValueDenotation type signature - Update golden signature test file - Update PlutusTx.Builtins.Internal for new signature This completes the API changes for quantity restriction, ensuring all builtin signatures accurately reflect the new error-handling behavior.
258f7dc to
b98b765
Compare
| -- | Validate all quantities in a nested map are within bounds. | ||
| validateQuantities :: HasCallStack => NestedMap -> BuiltinResult NestedMap | ||
| validateQuantities nestedMap = | ||
| case find isOutOfBounds allQuantities of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
any (any isOutOfBounds . M.elems) (M.elems nestedMap)
|
@Unisay @effectfully @zliu41 newtype Value = Value { getValue :: Map CurrencySymbol (Map TokenName Integer) } |
|
Yeah we'll do that later, likely after the HF |
Summary
This PR introduces a
Quantitynewtype to enforce bounds checking for Value amounts, restricting them to the signed 128-bit integer range (-2^127 to 2^127-1).Changes
Core Changes
Quantitynewtype inPlutusCore.Valuewith smart constructor and validatorsunionValueto returnBuiltinResult Valueto handle overflow detectionQuantityinstead of rawIntegerArbitraryBuiltininstance forQuantitywith improved value distributionTest Updates
unionValuesignature change (Value -> Value -> Value→Value -> Value -> BuiltinResult Value)BuiltinResultandQuantitytypesarbitraryBuiltinfor better test coverageImplementation Details
QuantityusesUnsafeQuantityconstructor (not exported)quantity :: Integer -> Maybe Quantityvalidates boundsBuiltinResultfor operations that can failarbitraryBuiltinprovides better distribution of test values than stockArbitrary, with improved coverage of edge cases near boundsCloses https://github.com/IntersectMBO/plutus-private/issues/1881