Integer division rounds to negative infinite, not documented

[amosr]

Hi Daniel,

We had an issue with integer division a while ago, but I forgot to log it. Kind2 and SMT-lib use the 'euclidean' definition of integer division, which has different rounding behaviour to C, and by extension, most of the other Lustre compilers. We noticed the discrepancy with Heptagon. I don't know whether it makes sense to change Kind2's behaviour though - maybe it should just be mentioned in the user manual somewhere.

A concrete example is that (-1) / 100 is -1 in Kind2, but it evaluates to 0 in C. This lets us prove some properties that hold for Kind2's semantics but wouldn't hold if we were to compile it with, say, Heptagon:

node div_example(i: int)
returns (j: int)
let
   j = i div 100;
   --%PROPERTY i < 0 => j < 0;
tel

I'm not sure about the Rust codegen. It looks like it doesn't support div syntax, but I thought the / syntax worked on integers too, so it might have the same issue: [https://github.com/kind2-mc/kind2/blob/develop/src/lustre/lustreToRust.ml#L490](Rust div).

To work around this, we just implemented a C function that has Kind2's division semantics, so that our Heptagon-compiled code matched Kind2's semantics. I will try to rewrite this implementation, as it might be useful as documentation, but I don't have access to the code any more and I found it pretty subtle to get right.

It is possible to express C rounding semantics in SMT-lib, but I don't know whether that's really useful, since integer division is hard enough already.

[amosr]

Just to clarify, this isn't a pressing issue at all, I just thought it would be good to write it down. I was reminded by some recent discussion about the same issue in F*:

• http://fstar-lang.org/tutorial/book/part1/part1_getting_off_the_ground.html#integers
• 1/-1 %// 2 cases not validating or computing FStarLang/FStar#2913