[CN] max/min constants

[jwshii]

(Ported from the CN heuristic evaluation results.) At least four participants expressed a desire for constants representing the maximum / minimum allowable integer. I see from looking around the CN channel that there is a way for the user to define such constants for themselves, but it could be nice to expose such constants directly. e.g.

/@ requires let sum = (i64) x + (i64) y;
                     MINi32 <= sum; sum <= MAXi32 @/

[dc-mak]

Fixed in https://github.com/rems-project/cerberus/commit/02a6f66f57c9a28c683a3e3cb569a6300adae1a9

[septract]

The fix means that examples need a lot of casts! Eg the example specification given above would be incorrect. We'd have to write:

signed int add_5(signed int x, signed int y)
/*@ requires 
      let sum = (i64) x + (i64) y;
      (i64) MINi32() <= sum; sum <= (i64) MAXi32(); @*/
/*@ ensures return == x + y; @*/
{
  signed int i;
  i = x + y;
  return i;
}

This is a bit awkward for sure, because if we define MINi32() with type i64 that also feels quite arbitrary. I wonder if the type should be integer?

[bcpierce00]

I’ve wondered the same: i64 here seems like a hack — what’s really meant is “unbounded signed int”, no?

On Fri, May 10, 2024 at 11:11 PM Mike Dodds @.***> wrote:

The fix means that examples need a lot of casts! Eg the example specification given above would be incorrect. We'd have to write:

signed int add_5(signed int x, signed int y) /@ requires let sum = (i64) x + (i64) y; (i64) MINi32() <= sum; sum <= (i64) MAXi32(); @/ /@ ensures return == x + y; @/ { signed int i; i = x + y; return i; }

This is a bit awkward for sure, because if we define MINi32() with type i64 that also feels quite arbitrary. I wonder if the type should be integer?

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/246*issuecomment-2105504395__;Iw!!IBzWLUs!XMAt2_tSgSqnJIPAMC-BVzE6f8ksWKGdc7b1UYTxxQVAFoRvnUpsVrkzmrZunm7QZkmvXYY5s3mXTHnYIUjcSxq-yeDM$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC5KZXRVLOWRVANQJ53ZBWD7FAVCNFSM6AAAAABHLBNFPKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBVGUYDIMZZGU__;!!IBzWLUs!XMAt2_tSgSqnJIPAMC-BVzE6f8ksWKGdc7b1UYTxxQVAFoRvnUpsVrkzmrZunm7QZkmvXYY5s3mXTHnYIUjcS-DhDnN_$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[PeterSewell]

On Sat, 11 May 2024 at 12:31, Benjamin Pierce @.***> wrote:

I’ve wondered the same: i64 here seems like a hack — what’s really meant is “unbounded signed int”, no?

The underlying decision is whether to map uniformly to SMT mathematical integers, or to SMT bitvectors, or to some hybrid. Initially CN did the first, but for at least some problems that doesn't work well and we switched to the second. It might be that a hybrid is necessary, but then one needs to figure out how the user should choose (and you can't afford to convert between them very much at all).

Peter

On Fri, May 10, 2024 at 11:11 PM Mike Dodds @.***> wrote:

The fix means that examples need a lot of casts! Eg the example specification given above would be incorrect. We'd have to write:

signed int add_5(signed int x, signed int y) /@ requires let sum = (i64) x + (i64) y; (i64) MINi32() <= sum; sum <= (i64) MAXi32(); @/ /@ ensures return == x + y; @/ { signed int i; i = x + y; return i; }

This is a bit awkward for sure, because if we define MINi32() with type i64 that also feels quite arbitrary. I wonder if the type should be integer?

— Reply to this email directly, view it on GitHub < https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/246*issuecomment-2105504395__;Iw!!IBzWLUs!XMAt2_tSgSqnJIPAMC-BVzE6f8ksWKGdc7b1UYTxxQVAFoRvnUpsVrkzmrZunm7QZkmvXYY5s3mXTHnYIUjcSxq-yeDM$>,

or unsubscribe < https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC5KZXRVLOWRVANQJ53ZBWD7FAVCNFSM6AAAAABHLBNFPKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBVGUYDIMZZGU__;!!IBzWLUs!XMAt2_tSgSqnJIPAMC-BVzE6f8ksWKGdc7b1UYTxxQVAFoRvnUpsVrkzmrZunm7QZkmvXYY5s3mXTHnYIUjcS-DhDnN_$>

. You are receiving this because you are subscribed to this thread.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/rems-project/cerberus/issues/246#issuecomment-2105685563, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZWI7GSGUVYOJD3L2E3ZBX6PBAVCNFSM6AAAAABHLBNFPKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBVGY4DKNJWGM . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[bcpierce00]

Fair enough, but I think the underlying point remains -- we want to reason in a space of "integers larger than machine integers," but the fact that this is exactly 64 bits is totally (?) irrelevant: what's relevant is that it's more than 32 bits! I.e., at least for me it would be more intuitive to write "bigunsigned" rather than "u64".

(Also, if we wanted to reason about a C program using u64 numbers, would there be an even larger CN type for that? If so, would it make sense to use that type as the meaning of bigunsigned all the time, rather than u64?)

(Also, for reasoning about 32-bit numbers, do we actually need all 64 bits of u64? Would u33 suffice?)

On Sat, May 11, 2024 at 7:36 AM Peter Sewell @.***> wrote:

On Sat, 11 May 2024 at 12:31, Benjamin Pierce @.***> wrote:

I’ve wondered the same: i64 here seems like a hack — what’s really meant is “unbounded signed int”, no?

The underlying decision is whether to map uniformly to SMT mathematical integers, or to SMT bitvectors, or to some hybrid. Initially CN did the first, but for at least some problems that doesn't work well and we switched to the second. It might be that a hybrid is necessary, but then one needs to figure out how the user should choose (and you can't afford to convert between them very much at all).

Peter

On Fri, May 10, 2024 at 11:11 PM Mike Dodds @.***> wrote:

The fix means that examples need a lot of casts! Eg the example specification given above would be incorrect. We'd have to write:

signed int add_5(signed int x, signed int y) /@ requires let sum = (i64) x + (i64) y; (i64) MINi32() <= sum; sum <= (i64) MAXi32(); @/ /@ ensures return == x + y; @/ { signed int i; i = x + y; return i; }

This is a bit awkward for sure, because if we define MINi32() with type i64 that also feels quite arbitrary. I wonder if the type should be integer?

— Reply to this email directly, view it on GitHub <

https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/246*issuecomment-2105504395__;Iw!!IBzWLUs!XMAt2_tSgSqnJIPAMC-BVzE6f8ksWKGdc7b1UYTxxQVAFoRvnUpsVrkzmrZunm7QZkmvXYY5s3mXTHnYIUjcSxq-yeDM$>,

or unsubscribe <

https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC5KZXRVLOWRVANQJ53ZBWD7FAVCNFSM6AAAAABHLBNFPKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBVGUYDIMZZGU__;!!IBzWLUs!XMAt2_tSgSqnJIPAMC-BVzE6f8ksWKGdc7b1UYTxxQVAFoRvnUpsVrkzmrZunm7QZkmvXYY5s3mXTHnYIUjcS-DhDnN_$>

. You are receiving this because you are subscribed to this thread.Message ID: @.***>

— Reply to this email directly, view it on GitHub < https://github.com/rems-project/cerberus/issues/246#issuecomment-2105685563>,

or unsubscribe < https://github.com/notifications/unsubscribe-auth/ABFMZZWI7GSGUVYOJD3L2E3ZBX6PBAVCNFSM6AAAAABHLBNFPKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBVGY4DKNJWGM>

. You are receiving this because you are subscribed to this thread.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/246*issuecomment-2105687897__;Iw!!IBzWLUs!R4q4A-wkcMbfp_hZeJKKVN8HWp7oqQQDni4NhrTbOapx5vH2GFXUxDFMNZZmd6AGi6U_Ll4tStpi3bqjbmR2um8wUwUT$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCYSRYW3D6A7XTB4V53ZBX7CNAVCNFSM6AAAAABHLBNFPKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBVGY4DOOBZG4__;!!IBzWLUs!R4q4A-wkcMbfp_hZeJKKVN8HWp7oqQQDni4NhrTbOapx5vH2GFXUxDFMNZZmd6AGi6U_Ll4tStpi3bqjbmR2uqMX08kC$ . You are receiving this because you commented.Message ID: @.***>