mod is rem

[vsubhuman]

Hello! Not to be nitpicking, but mod expression actually performs rem operation :)

mod 5, -3 // 2

(https://i.imgur.com/6KC2rQk.png)

Mod and Rem are not the same

1. https://stackoverflow.com/questions/5891140/difference-between-mod-and-rem-in-haskell/28027235#28027235
2. https://www.quora.com/I-am-a-beginner-in-MATLAB-programming-What-is-the-difference-between-the-two-operations-rem-and-mod-How-are-both-functionally-different

At the moment mod performs "remainder" operation, not "modulo". This might cause problems.

Concern

Mod rule implemented using the internal %Int operation:

rule <k> #exec REG = mod W0 , W1 => #load REG W0 %Int W1  ... </k> requires W1 =/=Int 0

(https://github.com/runtimeverification/iele-semantics/blob/master/iele.md#expressions)

The % operation is not obvious in the history of languages, e.g.:

1. In Python % is Mod
2. In Java % is Rem

The concern is that if %Int operation is implemented in K using the % in an underlying language - IELE might return different results for mod operation on different backends. Imo, there need to be strict guarantees on the mod operation contract, describing how exactly mod should work, backend-agnostic.