Feature request: a non-crashing modulo operation

[lukaszcz]

Following the discussion in #107, it would be very useful to have a version of % analogous to | which returns 0 instead of crashing when the second argument is 0. The alternative of implementing modulo bitwise using available primitives would have a significant impact on the efficiency of VampIR code generated from Juvix programs.

[lukaszcz]

This does make a very significant difference from the efficiency perspective.

For the following program:

// Access elements of a list

def hd (h:t) = h;

def tl (h:t) = t;

def nth lst n = hd (iter n tl lst);

// Ensure that the given argument is 1 or 0, and returns it

def bool x = { x*(x-1) = 0; x };

// Extract the n+1 bits from a number argument
// given a range function for n bits

def range_ind range a = {
    def a0 = bool (fresh (a%2));
    def a1 = fresh (a\2);
    a = a0 + 2*a1;
    (a0 : range a1)
};

// Inductively define range for each bit width

def range_base 0 = [];

def range n = iter n range_ind range_base;

// Multiply each tuple element by corresponding unit

def combine_aux x y = x + 2*y;

def combine xs = fold xs combine_aux 0;

// Unsigned less than or equal. 1 if true, 0 otherwise

def ule n a b = {
    def c = range (n+1) ((2^n)+b-a);
    nth c n
};

// Unsigned less than for 8 bits

def ult n a b = ule n a (b-1);

// Extract the first element of any supplied pair

def fst (a,b) = a;

// Extract the second element of any supplied pair

def snd (a,b) = b;

// Single round of n bit unsigned Euclidean division

def div_next prev a b m n acc = {
    def n = n - 1;
    // Shift the divisor
    def c = b * (2^n);
    // Check if shifting produces larger number
    def d = ule m c a;
    // Subtract the shifted value if it is smaller or equal
    def e = a - d * c;
    // Move to the next round on the remainder
    prev e b m n (d:acc)
};

// n bit unsigned Euclidean division base case

def div_base a b m n acc = (acc, a);

// n bit unsigned Euclidean division

def divrem n a b = {
    // Inductively build up division function
    def div = iter n div_next div_base;
    // Do the division, doubling space for inequalities
    def (quot, rem) = div a b (2*n) n [];
    // Combine the bits into a number again
    (combine quot, rem)
};

def div n a b = fst (divrem n a b);

def divRemA n a b = {
    def q = fresh (a\b);
    def r = fresh (a%b);
    ult n r b = 1;
    a = b * q + r;
    (q, r)
};

def divA n a b = fst (divRemA n a b);

iter 101 (divA 16 282) x = 282;

I have:

• circuit size: 1.6M
• compilation: 23s
• proving: 7.5s
• verification: 1.5s

Changing divA to div in the last equation results in:

• circuit size: 56M
• compilation: 1049s
• proving: stack overflow
• verification: -

[lukaszcz]

BTW, "executing" anything in a circuit (the proving phase) is extremely slow. In the first version above we're just doing 100 divisions and this takes over 7s to prove. ENIAC could execute 35 divisions per second.

[lukaszcz]

Sorry if this came out as disrespectful, this was not at all my intention. I well realize that there are more things going on in the circuit than just doing divisions.

My point is that if you want to compile from a higher-level language that is not close to the circuit model, and you just want to do say 100 integer divisions (not field element divisions) in that higher-level language, then in the actual circuit, as you point out, you'll be doing lots of other things. But the high-level user cares about the 100 integer division, which if compiled to native machine instructions would roughly be dominated by doing 100 division instructions.

I'm sorry again if this was read as criticism of VampIR, which it is not. It was meant as a general comment on the difficulty of creating an efficient circuit from a high-level language, with proving/"executing" efficiency comparable to what one would achieve with even a direct interpreter. This is what I'm concerned with all the time.

And indeed I have been a bit frustrated by my inability to achieve such efficiency, but this is not a criticism of VampIR, just my general comment on the situation.

You're right that I should've perhaps provided more context and phrased this comment differently, but there is no need to assume malice on my part.

[AHartNtkn]

I realized my original comment was a bit hostile, and I didn't understand what you were trying to communicate. I accept your apology and offer mine in return.