mod in Ivy

[benSepanski]

Modulo in ivy has a correctness bug. In numbers.ivy and order.ivy, mod is defined as

mod(X,Y) = X - X / Y * X

When it should instead be defined as

mod(Y,X) = X - X / Y * Y

(For example, mod(3, 2) should equal 3 - (3 / 2) * 2 = 3 - 1 * 2 = 1, not 3 - (3 / 2) * 3 = 3 - 1 * 3 = 0.

Here is an example using ivy to reproduce the bug:

#lang ivy1.8

include numbers
include order

process p = {
    export action take_mod(y:nat,x:nat)  # Computes y % x
    implement take_mod {
        require x ~= 0;

        var rem : nat;
        rem := y.mod(x);
        debug "Taking Mod" with dividend = y,
            divisor = x,
            remainder = rem
            ;
    }
    export action mod_table(upto:nat,by:nat)  # prints y % by for y = 0,1,...,upto-1
    implement mod_table {
        var dividend :nat;
        dividend := 0;
        while dividend < upto {
            take_mod(dividend, by);
            dividend := dividend.next;
        }
    }
} with nat

Running the above program, I can produce the following output:

> p.mod_table(4, 2)
{
    "event" : "Taking Mod",
    "dividend" : 0,
    "divisor" : 2,
    "remainder" : 0,
}
{
    "event" : "Taking Mod",
    "dividend" : 1,
    "divisor" : 2,
    "remainder" : 1,
}
{
    "event" : "Taking Mod",
    "dividend" : 2,
    "divisor" : 2,
    "remainder" : 0,
}
{
    "event" : "Taking Mod",
    "dividend" : 3,
    "divisor" : 2,
    "remainder" : 0,
}

[benSepanski]

I'm using ivy through a pip installation, I'm on ivy 1.8.8 (and re-ran pip install --upgrade right before running this program