Pick uniform convention for inclusive vs.exclusive bounds in runtime and CBMC bounds checking macros

[hanno-becker]

We have debug-build runtime checks (e.g. POLY_BOUND(...)) as well as CBMC assertions ARRAY_IN_BOUND(...) both expressing bounds on an int16_t array. However, the runtime assertions use exclusive bounds, while the CBMC assertions use inclusive bounds. This is confusing and was close to leading to a poor spec in #https://github.com/pq-code-package/mlkem-c-aarch64/pull/313.

• Make a pick and use inclusive or exclusive bounds in both runtime and CBMC bounds checking macros.

[hanno-becker]

@rod-chapman Can you work on this?

I lean towards following the inclusive bound convention from our CBMC macros, which would mean merely changing the few runtime assertions.

[mkannwischer]

Agree - this should be consistent.
I don't think this is essential for the alpha-release. Moving to the next one.

[rod-chapman]

I've been thinking a bit on this one. Writing assertions and contracts, I always tend to use inclusive bounds, but I've been trying to work out why... observations:

1. Ada's subtype inclusion operator ("X in S") and subtype range declaration ("type T is range 0 .. 3328;") are inclusive at both ends, so writing explicit bounds the same way always feels consistent to me, and it's ground into me as a habit over the last 30 years. But that's just Ada for you...
2. Thinking about proofs, I prefer inclusive bounds since (I think) I find it easier to derive one inequality from another if the ranges are inclusive. e.g. if I know

a <= b

then I can ask the tool to prove something like

a + C <= b + C

with reasonably confidence that I haven't screwed it up. I always seem to get it wrong where "<" and ">" are involved.
Also things like transitivity:

(a >= b) and (b >= c) -> (a >= c)

feel more natural to me with inclusive relations.

Does any of that make sense?

[mkannwischer]

Not sure I can follow the transitivity argument. Doesn't a>b and b>c imply a>c? Maybe I need more caffeine.

I have no strong opinion on using inclusive or exclusive bounds - but I'd like it to be consistent.
Since you both lean towards inclusive bounds, let's go for that and change the runtime assertions.

[rod-chapman]

Yeah... the transitivity rules work with ">" of course, but I just find it easier to think about them if they all of the same "sense".