Generic value range types

[chriseth]

Support generic types of the form

number<low..high[,precision]>

such that arithmetic operators on these types just naturally extend the ranges.

Example:

function f(number<0..2000> a, number<0..2000> b) returns (number<0..4000>) {
  return a + b;
}

The type of the expression a + b is number<0..4000>. Similarly, the type of a * b would be number<0..4000000>.

The precision parameter represents the number of (decimal) digits after the radix point and we have the natural rules:

number<...,c> + number<...,d> -> number<...,max(c, d)>
number<...,c> * number<...,d> -> number<...,c + d>

[axic]

I took the following notation:

• number{N} where N represent the number of decimal digits. If N is 0, it must be omitted, e.g. number represents integers
• number<A,B,C> to represent exact values
• number<[A..B]> to represent ranges
• number<A,B,[C..D],[E..F]>

A complex example: number{4}<1,2,3,[42..84],[196..256]>, though this makes sense to be typedef'd.

[chriseth]

It seems like [ and ] can be omitted.
Hm, I must admit that {N} looks a little weird. Also, why is it not part of < ... >?

What about:

number<6..7,8,9|3>?

Also, what does it exactly mean?

[VoR0220]

would it be possible to use global variables in these ranges? Matters such as "currentBlockNumber" and other areas that show what people would probably want to do with this in terms of defining price ranges that automatically assess risk, that being use them in ranges for proper collateralization techniques of their smart contracts. In other words, could one set these in a way where the inputs could be determined by external oracles/contracts? Or would this be/should this be explicitly disallowed? My gut tells me that it shouldn't be but that there could be interesting applications using this.

[axic]

Since in #2136 we've agreed to use {} with named fields, we could revise #2918 (comment) as:

• number{digits=N}
• number<A,B,C> to represent exact values
• number<A..B> to represent ranges
• and number<A..B,C,D,E..F> to represent a combination of values and ranges

However as a start, I'd only implement support for single ranges: number<A..B> as exact values may be better represented via enums.

[axic]

cc @ekpyron

[ekpyron]

Yeah, this came up again, since with yul-codegen we will use overflow-checked math by default - and for that it makes almost no difference, whether the checks are against powers of two or not (apart from the fact that the constants used might be more expensive to store).
So with yul codegen

function f(uint8 a, uint8 b) ... { uint8 c = a + b; ... }

Is basically the same as

function f(number<0,255> a, number<0, 255> b) ... {
    number<0, 255> c = number<0, 255>(a + b); // downcast that throws on out-of-range errors
}

Where for the latter any other range would be valid as well at insignificant additional cost.

And the question was, why to only allow this kind of logic specifically for powers of two, where ranges of real-world quantities are rarely accidentally powers of two.

I actually think this is a nice direction to go - we could at some point only allow the old sized integer types in unchecked blocks altogether.

[ekpyron]

We're considering this for 0.7.
We need to solve the following issues:

• Are non-arithmetic operations allowed?
• How will these types be represented in the ABI?
• What about ranges exceeding 256-bits?
• Do we need/want type aliases to alleviate verbosity in casting? Would those help or confuse?

My first reaction to those:

• At first non-arithmetic operations are not allowed, but only possible via casting to bit-sized types. We can think about supporting them in a second step.
• I think the types should all have proper ABI types, but we need to come up with a good, future proof naming schema and should probably get non-solidity feedback about this.
• 256-bits is the maximum range for the first implementation. number{0,2^256} + number{0,2^256} is valid, but it has an inexpressible type that only supports one operation: namely downcasting.

Also we need to define behaviour in weird cases, e.g. number{0, 10} a; number{20,30} b = number{20,30}(a); should probably be a compile-time error, since it will always have to revert.

If it makes things easier a first implementation could also have some restrictions, e.g. we can start with only ranges of the form number{0,max} and extend to signed ranges later (but it may in fact be straightforward enough to do both in one go). But especially precisions, if we want them in the long run, I would postpone for a second step.

Also we should write some example code to evaluate the syntax and its readability, especially wrt casting/converting.

Gimmick for a future step: we could allow implicit downcasts, whenever the compiler can deduce that the actual value will be in range, i.e. number{0,100} a; could be implicitly convertible to number{0,50}, after a require(a <= 50) or inside an if (a <= 50) or inside an if (a <= b) for number{0,50} b, etc.

[ekpyron]

And yeah... I just used number{min,max} as syntax placeholder, but we need to decide on a final syntax as well of course. I think we decided against any syntax involving <...> in the past, since it's hard to parse, but we could also just look into working around that, if possible. I'm not sure if a syntax for a finite set of exact discrete values (as @axic suggested above) is too useful... maybe it is, but arithmetic on them - depending on how that would work - could be hell... so I'd stick to a single range per type at least as first step (as also suggested by @axic above).

[ekpyron]

Syntax-wise number{min: 0, max: 100} would of course be future-proof and fit the create2 and gas/value syntax nicely - but I'm afraid it's too verbose... with that we'd probably really need to allow user-defined aliases...

Regarding casting: maybe we should actually evaluate how much effort range-tracking would be:

number{0,100} a; number{0,100} b;
require(a + b <= 100);
a = a + b; // fine without casting due to imposed constraints!

could be much nicer than having to use

number{0,100} a; number{0,100} b;
a = number{0,100}(a + b); // looks weirder and makes it less explicit that this may revert

But tracking ranges well enough might be (too) tough. It might be enough to only consider constraints of the exact form expression <= constant (and constant <= expression or with any other comparison operator). Or we can restrict to all linear constraints - that'd also be easy to solve.

[ekpyron]

@leonardoalt In theory, how much trust would you have into using SMT solving for the range constraints for this :-)? We probably can't do it anyways, at least as long as we can't make SMT solvers a hard dependency of the compiler, which we can't until we have emscripten builds for them... and in general it might cause loads of problems, e.g. for reproducable builds, etc., but might still be fun to think about...

[ekpyron]

Interestingly, things like += won't be possible on these types unless we track constraints.

[ekpyron]

Another question: is dividing by a type with 0 in its range allowed :-)?

[chriseth]

To get good answers to all these questions, we should probably take a look at a DSL that has that feature.

[github-actions]

This issue has been marked as stale due to inactivity for the last 90 days.
It will be automatically closed in 7 days.

[github-actions]

Hi everyone! This issue has been automatically closed due to inactivity.
If you think this issue is still relevant in the latest Solidity version and you have something to contribute, feel free to reopen.
However, unless the issue is a concrete proposal that can be implemented, we recommend starting a language discussion on the forum instead.