Lazy if and division by zero

[lukaszcz]

I want to implement the GCD function in VampIR, unrolled up to some depth. Here is my code:

def isZero x = {def xi = fresh (1 | x); x * (1 - xi * x) = 0; 1 - xi * x};
def isBool x = (x * (x - 1) = 0);
def isNegative a = {def e = 2^30; def b = a + e; def b0 = fresh (b % e); def b1 = fresh (b \ e); isBool b1; b = b0 + e * b1; 1 - b1};
def lessThan x y = isNegative (x - y);
def lessOrEqual x y = lessThan x (y + 1);
def divRem a b = {def q = fresh (a\b); def r = fresh (a%b); isNegative r = 0; lessThan r b = 1; a = b * q + r; (q, r) };
def fst (x, y) = x;
def snd (x, y) = y;
def div x y = fst (divRem x y);
def rem x y = snd (divRem x y);
def if b x y = b * x + (1 - b) * y;

def gcd_0 x y = 0;
def gcd_1 x y = if (isZero x) y (gcd_0 (rem y x) x);
def gcd_2 x y = if (isZero x) y (gcd_1 (rem y x) x);
def gcd_3 x y = if (isZero x) y (gcd_2 (rem y x) x);
def gcd_4 x y = if (isZero x) y (gcd_3 (rem y x) x);
def gcd_5 x y = if (isZero x) y (gcd_4 (rem y x) x);
def gcd_6 x y = if (isZero x) y (gcd_5 (rem y x) x);
def gcd_7 x y = if (isZero x) y (gcd_6 (rem y x) x);
def gcd_8 x y = if (isZero x) y (gcd_7 (rem y x) x);
def gcd_9 x y = if (isZero x) y (gcd_8 (rem y x) x);
def gcd_10 x y = if (isZero x) y (gcd_9 (rem y x) x);

def gcd x y = if (lessThan y x) (gcd_10 y x) (gcd_10 x y);

gcd a b = c;

This compiles fine, but it will give a "division by zero" error while generating a proof for all small enough inputs. These are all the inputs we would want gcd to work with - it won't divide by zero only if the recursion depth limit is reached.

The problem is that the if is not lazy - it always "evaluates" both branches and one of them will ultimately lead to division by zero in a further recursive call.

Is there any way to implement a lazy if?

Otherwise, there doesn't seem to be any way to guard against division by zero, which seems to rule out the possibility of correctly compiling Juvix programs which check for zero and terminate early to avoid division by zero.

[lopeetall]

We can't exactly do a "lazy if" in Vamp-IR because circuits are static and can't introspect into the value of a variable to choose not to evaluate a branch. Both branches of an if must be evaluated.

However I think we can address this in a different way, using the "division or zero" (|) operation instead of field division in divRem. For a and b, if either a or b is zero, then a|b is zero. Otherwise a|b = a/b. This protects against failure because of division by zero, but you do need to think carefully when using it, because a|b = 0 does not imply a = 0 as in normal division.

I think divRem can be modified safely to use |, but I'd need to write it out first to convince myself.

[lukaszcz]

Thanks! Yes, using | should work. But what is a%0 equal to?

[AHartNtkn]

It just calls rust's built-in % operator, which will panic with "attempt to divide by zero".

[lukaszcz]

So it seems we need an analogue of | for modulo?

[AHartNtkn]

If you want to run a%0 without crashing, then yes. We've been careful to keep the set of built-in functions small. I'm not against adding more, and this seems like a natural addition, but it should be carefully considered. If you think it's necessary and Joshua approves, then I can add it.

[lukaszcz]

Without a non-crashing modulo there seems to be no way to compile Juvix programs which compute a remainder of a division by an unknown quantity, because there is no way to lazily check for 0. How would you implement the GCD function above without it? Unless you can somehow use | with other operations to compute the remainder, but I don't know how.

[AHartNtkn]

It is possible to calculate divRem without using / or %. See the implementation in tests/alu.pir, for example. Let me know if it works out.

[lukaszcz]

Thanks! But it seems in tests/alu.pir you just calculate the arithmetic operations bitwise, essentially implementing the primitive arithmetic operations with bit manipulation. Isn't this tragically inefficient? It seems this would generate a lot of circuity for division/modulo.

The broader question is why do you have the \ and % primitives at all instead of the more useful ones that don't crash on zero? Since there is no way to lazily check for zero, \ and % are useless when the second argument is not known to be non-zero beforehand.

[AHartNtkn]

I wouldn't call it tragic, but, yes, it would be less efficient. As for your other questions, I assume it was to minimize complexity. It's easier to call rust built-ins than to consider what might be most useful. But you do make a good point.

[lukaszcz]

I wouldn't call it tragic, but, yes, it would be less efficient.

My experience with compiling Juvix programs to VampIR is that this matters a lot. For example, I initially implemented isNegative as in https://anoma.github.io/VampIR-Book/section_4_3.html, decomposing the number into all 31 bits. This needed much more circuity than the current approach (as in the code above) of just checking the most significant bit. The generated programs needed many more PLONK parameters and everything ran at least an order of magnitude slower.

[AHartNtkn]

Your isNegative doesn't actually check that a number is negative. If we translate it into a predicate, it states that;

∃b0 b1. isBool b1 ∧ a + 2^30 = b0 + 2^30 * b1

It doesn't do any range check on b0. Remember, fresh is a black box. The final circuit doesn't check that b0 actually is b % e, nor that b1 actually is b \ e. When you generate a number using fresh, you're defining a circuit input whose values are automatically calculated separately from the circuit itself. In the case of your definition of isNegative, for example, a = b0 = b1 = 1 meets your predicate, but a isn't negative.

By contrast, decomp8 from that page corresponds to the predicate

∃x0...x7. isBool x0 ∧ ... ∧ isBool x7 ∧ x = x0 + 2*x1 + ... + 2^7*x7

If we used it in a definition of isNegative

def isNegative8 a = decomp8 (a + 2^8);

then isNegative8 is the predicate

∃x0...x7. isBool x0 ∧ ... ∧ isBool x7 ∧ a + 2^8 = x0 + 2*x1 + ... + 2^7*x7

You may notice that the last exponent on the x is 2^7, not 2^8. Correcting this in your predicate would give us

∃b0 b1. isBool b1 ∧ a + 2^30 = b0 + 2^29 * b1

but this still doesn't give us a guarantee that a is negative since b1 = 1, a = 1, and b0 = 2^29 + 1 still satisfies the relation with a being positive; the lack of range check allows b0 to exceed 2^29. The only way to force a to be negative is to additionally check that b0 < 2^29, which requires additional decomposition of b0.

[lukaszcz]

Yes, you're right, thanks. I know fresh is a black box, and the above looks obviously wrong once you point it out. I think I implicitly assumed that a, b0 will be in the right range because of division/modulo.

And it worked, because the values actually used are correct, just the circuit doesn't check it, as far as I understand.

[lukaszcz]

I'll correct it, but it is going to slow things down. These are basic operations used repeatedly everywhere - any slight inefficiency in their implementation results in significant overhead overall.

[lukaszcz]

Sorry, maybe this is a stupid question, but I still don't understand why you add 2^8 instead of 2^7. If a is in [-2^7, 2^7) then a + 2^8 is in [2^7, 2^8+2^7). So a + 2^8 might have the 9th bit (2^8) set, but you're then decomposing it into 8 bits? I don't understand how this is supposed to work. If a is negative, then a + 2^8 is in [2^7, 2^8), so the 8th bit is set. But if a is non-negative, then a + 2^8 is in [2^8, 2^8 + 2^7), so the 8th bit is not set, but the 9th is. Wouldn't this always give an unsatisfiable constraint for non-negative a if you're decomposing a + 2^8 into 8 bits?

[lukaszcz]

Sorry, maybe this is a stupid question, but I still don't understand why you add 2^8 instead of 2^7. If a is in [-2^7, 2^7) then a + 2^8 is in [2^7, 2^8+2^7). So a + 2^8 might have the 9th bit (2^8) set, but you're then decomposing it into 8 bits? I don't understand how this is supposed to work. If a is negative, then a + 2^8 is in [2^7, 2^8), so the 7th bit is set. But if a is non-negative, then a + 2^8 is in [2^8, 2^8 + 2^7), so the 8th bit is not set, but the 9th is. Wouldn't this always give an unsatisfiable constraint for non-negative a if you're decomposing a + 2^8 into 8 bits?

I guess it works because in the decomp implemented with iter you actually discard all bits after the 8th. But wouldn't it be more understandable to add 2^7 instead and check that the 8th bit is 0?

[lukaszcz]

I guess you also want some close to two's complement bit decomposition for a negative number, but the exact form of the bit decomposition doesn't matter for just checking if number is negative?

And with the iter version of decomp you don't seem to be checking if there are some "extra" bits outside the range?

[lukaszcz]

Or maybe the idea is that all numbers (positive and negative) are represented by field elements in the range [0,2^8) and interpreted bitwise? I would like this explained better in the Vamp-IR book.

[lukaszcz]

Or maybe the idea is that all numbers (positive and negative) are represented by field elements in the range [0,2^8) and interpreted bitwise? I would like this explained better in the Vamp-IR book.

No, this doesn't seem to make sense, because then adding 2^8 wouldn't change the first 8 bits and you're looking only at them?

[lukaszcz]

From the documentation:

intDecomp 8 ((-55)) = 1:0:0:1:0:0:1:1:[];

This will return what is almost the two's complement representation. The main difference is that the last bit, indicating the > sign, is the opposite of what it is in usual presentations of two's complement.

Isn't this just exactly the two's complement representation of -55 in an 8bit system? It's the binary representation of 2^8 - 55, so just the ordinary two's complement?

[AHartNtkn]

If a is in [-2^7, 2^7) ...

isNegative8 isn't testing that a ∈ [-2^7, 2^7), it's testing that a ∈ [-2^8, 0) since it's testing for negativity. This latter condition is the same as a + 2^8 ∈ [0, 2^8), and the 8 bit decomposition of a + 2^8 tests this.

It's the binary representation of 2^8 - 55, so just the ordinary two's complement?

Hmm... it appears that you're right. The implementation in that section is incorrect. It should be 2^7 - 55, which has its last bit flipped. With the current implementation, intDecomp 8 127 would check that 127 + 2^8 ∈ [0, 2^8), which will obviously fail. I'll correct it.

To clear up some confusion, the isNegative8 I gave in my previous comment would cause a proof error if the input isn't negative. The isNegative in the Vamp-IR book doesn't do this, but rather, range checks and then returns a bit indicating negativity. So, they aren't doing the same thing. I may have been a bit confused when I wrote that comment, but it doesn't detract from the original point, I suppose.

[lukaszcz]

Yes, thanks for the explanation. I was talking about the isNegative from the book though, and you add 2^8 instead of 2^7 there as well. I understand now this is a mistake.

[lukaszcz]

And in the book the decomp implemented with iter doesn't seem to check the range actually, because it will just ignore all bits after the 8th it seems. At the last application of decomp_rec the a1 will just be ignored, because it's passed to bits which is a constant function returning [].