Bounded unsigned integer spells #1230

Kukovec · 2023-10-25T20:59:42Z

Tests added for any new code
Documentation added for any new functionality
Entries added to the respective CHANGELOG.md for any new functionality
Feature table on README.md updated for any listed functionality

coauthored w/ @thpani

shonfeder

Just a few questions and small suggestions from me :)

Generally looks great.

examples/README.md

shonfeder · 2023-10-30T21:10:25Z

examples/spells/BoundedUInt.qnt

+  /// If the `error` field is nonempty, the record represents an exception of some
+  /// sort happening during computation, such as an overflow.
+  /// Otherwise, the record represents the integer `v`, such that `MIN <= v <= MAX`. 
+  type T = { v: int, error: str }


Seems like UInt would be a more descriptive type name. Otherwise it is impractical to import the module unqualified.

I'm wondering if actual use case needs an error message string. Would it be possible that having error: bool would be more ergonomic and just knowing that there is an error one way or the other would suffice?

I can rename it UintT (UInt clashes with the constructor). As for the error field, I prefer keeping it. You can always call i.isValid, and get a boolean evaluation, whereas the error string is more descriptive (and already implemented)

The constructor could be intToUInt. I think this is how we are making converters of, e.g., maps to sets: https://github.com/informalsystems/quint/blob/main/quint/src/builtin.qnt#L310

Not sure if that article is supposed to be an example of nomenclature, or if you mis-pasted it.

Miss pasted! Sorry. That should be https://github.com/informalsystems/quint/blob/main/quint/src/builtin.qnt#L310

I'm wondering if actual use case needs an error message string. Would it be possible that having error: bool would be more ergonomic and just knowing that there is an error one way or the other would suffice?

The error field is similar to what was done with the modelling of Decimals in https://github.com/informalsystems/quint-sandbox/blob/main/decimal/decimal.qnt. While a Boolean would suffice, having a string is almost as cheap (from the analysis p.o.v.) as having a Boolean, and it it produces better counterexamples.

I'm fine with leaving it as an error message if that has proven useful.

I think the remaining item left for this comment is then the type name.

I think

UInt: int => UIntT

looks much nicer than

intToUInt: int => UInt

mainly because, if I have to type intToUInt for every integer literal in my spec, that's a lot of line-width bloat.
@konnov @thpani @bugarela

True, it looks nicer. If we go with an interface that requires wrapping values, makes sense to keep it short.

examples/spells/BoundedUInt.qnt

shonfeder · 2023-10-31T13:11:24Z

examples/spells/BoundedUInt.qnt

+    ///////////////////////////
+   // SATURATING OPERATIONS //
+  ///////////////////////////
+
+  /// Unsafe saturating integer addition. 
+  /// Computes `lhs + rhs`, saturating at the numeric bounds instead of overflowing.
+  /// Assumes lhs and rhs are valid (w.r.t. `isValid`).
+  pure def saturatingAddUnsafe(lhs: T, rhs: T): T = {
+    val res = lhs.v + rhs.v
+    { 
+      v: if (res < MAX) res else MAX, 
+      error: "" 
+    }
+  }


Since these don't error out, would it not make more sense to just have it defined over int?

I thought the same thing. Seems to me that we'd want all saturating and wrapping operators to be defined over int.

It's an interface question. You want these operations to all be (UIntT, UIntT) => UIntT so you can chain them.
If this returned an int, you couldn't do e.g. saturatingAdd(saturatingAdd(a,b), c)

We are thinking the signature should be (int, int) => int, so that would chain fine.

For saturating alone, yes, but you couldn't combine e.g. saturatingAdd(checkedAdd(a,b), c) (which was supposed to be the example above, but I borked it in copypaste)

Just to make sure I understand the above, you also prefer

saturatingAdd: (int, int) => int checkedAdd: (int, int) => T

?
We can do it like that, but I'll just reiterate #1230 (comment), doing this allows for "nonsensical" (in the unsigned-int universe) constructions.

Both ways are "chainable"

Our goal here should be brief, self-explanatory specs

I agree with that goal! But its worth noting that requiring the saturatinAdd arguments and return value to be wrapped introduces its own complexity, and leaving them as type int makes it clearer when interacting with other int operators, like say the predicates or indexing operations.

Wrapping everything in the UInt type, whether or not it is needed, will make it easier to chain these operators and that is clearer, but at the expense of every other point where the returned or supplied values have to be cast to/from an int.

An additional benefit of expecting this to use Option combinators for chaining (once sum types are in, but using a makeshift maybe in the meantime) is that it makes it self-explanatory to readers that one is chaining partial computations.

Some example use cases using the two different approaches may be illustrative to track the tradeoffs. Do we have any code in mind that would be a good test case?

At least from the code where this would be useful that I've seen (Rust in Cosmos, bounded integers in smart contracts), you would firmly stay within the bounded fragment. I've never seen an unwrap to integers.

For this purpose, I believe that a single, initial wrapping of Quint's native int into a UInt, and then simply remaining in UInt, is the most practical.

But I'm happy to consider other examples, or if we have none atm, revise this library when necessary.

Makes sense.

examples/spells/BoundedUInt.qnt

shonfeder · 2023-10-31T13:21:23Z

quint/cli-tests.md

+<!-- !test check BoundedUint8 - Syntax/Types & Effects/Unit tests -->
+    quint test --main=BoundedUInt8Test ../examples/spells/BoundedUInt.qnt


Tests should get run in the examples dashboard. Whats the added value of adding an additional test here?

examples/spells/BoundedUInt.qnt

konnov

left a few comments

examples/spells/BoundedUInt.qnt

konnov · 2023-11-06T11:48:34Z

examples/spells/BoundedUInt.qnt

+    ///////////////////////////
+   // SATURATING OPERATIONS //
+  ///////////////////////////
+
+  /// Unsafe saturating integer addition. 
+  /// Computes `lhs + rhs`, saturating at the numeric bounds instead of overflowing.
+  /// Assumes lhs and rhs are valid (w.r.t. `isValid`).
+  pure def saturatingAddUnsafe(lhs: T, rhs: T): T = {
+    val res = lhs.v + rhs.v
+    { 
+      v: if (res < MAX) res else MAX, 
+      error: "" 
+    }
+  }


yeah, chaining would be good IMO

bugarela

I love the new tests! Thank you for all the changes 💅

shonfeder

Thanks for making the tests clearer :)

Kukovec requested review from thpani, konnov and bugarela October 25, 2023 20:59

shonfeder reviewed Oct 31, 2023

View reviewed changes

bugarela reviewed Oct 31, 2023

View reviewed changes

examples/spells/BoundedUInt.qnt Show resolved Hide resolved

konnov reviewed Nov 6, 2023

View reviewed changes

Kukovec and others added 7 commits November 8, 2023 13:12

BoundedUInt

f29e9ae

docs + format

1d8a8bb

tests

fd32dfb

Fix casing and examples

3fc8f43

Fix casing in test

1473bbd

Fix test in examples dashboard

e1b7bb9

test fix

0580a4d

Kukovec force-pushed the jk/ciWeek branch from ce5b6df to 0580a4d Compare November 8, 2023 12:13

Kukovec requested review from konnov, shonfeder and bugarela November 8, 2023 12:14

oor fix

4dd0d78

bugarela approved these changes Nov 8, 2023

View reviewed changes

Merge branch 'main' into jk/ciWeek

f05dd1e

shonfeder approved these changes Nov 8, 2023

View reviewed changes

Kukovec merged commit 3b0209c into main Nov 8, 2023
15 checks passed

Kukovec deleted the jk/ciWeek branch November 8, 2023 14:26

Kukovec restored the jk/ciWeek branch November 8, 2023 14:26

Kukovec deleted the jk/ciWeek branch November 8, 2023 14:26

Kukovec restored the jk/ciWeek branch November 8, 2023 14:26

Kukovec deleted the jk/ciWeek branch November 8, 2023 14:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Bounded unsigned integer spells #1230

Bounded unsigned integer spells #1230

Kukovec commented Oct 25, 2023 •

edited

Loading

shonfeder left a comment

shonfeder Oct 30, 2023

shonfeder Oct 31, 2023

Kukovec Oct 31, 2023

shonfeder Oct 31, 2023 •

edited

Loading

Kukovec Oct 31, 2023

shonfeder Oct 31, 2023

konnov Nov 6, 2023

shonfeder Nov 7, 2023

Kukovec Nov 7, 2023

shonfeder Nov 7, 2023

shonfeder Oct 31, 2023

bugarela Oct 31, 2023

Kukovec Oct 31, 2023

shonfeder Oct 31, 2023

Kukovec Oct 31, 2023

Kukovec Nov 6, 2023

Kukovec Nov 6, 2023

shonfeder Nov 7, 2023

thpani Nov 8, 2023

shonfeder Nov 8, 2023

shonfeder Oct 31, 2023

konnov left a comment

konnov Nov 6, 2023

bugarela left a comment

shonfeder left a comment

		<!-- !test check BoundedUint8 - Syntax/Types & Effects/Unit tests -->
		quint test --main=BoundedUInt8Test ../examples/spells/BoundedUInt.qnt

Bounded unsigned integer spells #1230

Bounded unsigned integer spells #1230

Conversation

Kukovec commented Oct 25, 2023 • edited Loading

shonfeder 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

shonfeder Oct 31, 2023 • 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

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

konnov left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bugarela left a comment

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment

Kukovec commented Oct 25, 2023 •

edited

Loading

shonfeder Oct 31, 2023 •

edited

Loading