Wanted: Tactic for dealing with Z.div and Z.modulo and Z.pow about fiat-crypto HOT 6 CLOSED

One thought that I've had:
Replace (a / b)%Z with ((a - (a mod b)) / b)%Q, saturate the context with enough facts about a mod b (whatever that means), replace / b with * b^-1 and add b * b^-1 = b^-1 * b = 1 to the context, and use nsatz to handle the goal. (I can't figure out what "enough facts" would look like, though.) There's also the issue that we need to handle things like 2^(k * n + n + n)...

from fiat-crypto.

Hmm. There really seems to be a lack of good reference to work from: sympy and sage do not recognize integer division of symbolic variables, maxima documentation says that division syntactic sugar for (a*b^1)%Q. I didn't manage to find documentation on magma. I wonder what Z3 does for integer divison (I think I recall from http://css.csail.mit.edu/6.858/2015/labs/lab3.html that it does something).

I also have a good feeling about transforming (a / b)%Z to ((a - (a mod b)) / b)%Q, but I don't know where to go from there. Could you give a human-reading-sized example where non-obvious information about a mod b is necessary to conclude?

Are the zsimplfy integer division lemmas a good test case of what should be solved by the automation to be built?

from fiat-crypto.

I've written Z.div_mod_to_quot_rem. It sometimes works well with nia. (For example, after suitable normalization of Z.pow, it proves that the carry bit on ripple-carry-add is correct.) However, this combination cannot prove 0 < z -> (x + y) mod z = (y + x) mod z; I think the issue is that of bug #5022. This comes up, for example, in the following goal which I believe is true, which says that carrying associates and does not overflow (it may need 0 < k, though; I'm not sure):

1 ≤ n
 → 0 ≤ k
 → (0 ≤ z₁ < 2 * 2ⁿ - 1)
 → 1 < 2ⁿ
 → 0 < 2ᵏ
 → (0 ≤ z₀ < 2 * 2ᵏ)
 → z₀ mod 2ᵏ + ((z₁ + z₀ / 2ᵏ) mod 2ⁿ) * 2ᵏ = (z₀ + (z₁ mod 2ⁿ) * 2ᵏ) mod (2ⁿ * 2ᵏ)

from fiat-crypto.

(If that fails to render, there are subscript 0s and 1s, and superscript ns and ks.)

from fiat-crypto.

StackOverflow points me at Mathematica for handling systems of nonlinear inequalities. I think converting to quotient + remainder and adding the universal property to the context (that n = q * d + r with 0 <= r < d for n mod d = q and n / d = q) is the right way to go; it is local (doesn't require converting everything to Q), general (works in any Euclidean domain), and is information-preserving. This reduces the problem to that of nonlinear integer inequalities, which is, unfortunately, undecidable in general. (And it seems that Coq's heuristics are not sufficiently powerful.)

This doesn't handle Z.pow, but I think normalization of Z.pow should be feasable-ish if we can get this working (namely, if we find b^x and b^y with y a subterm of x, we try to decompose b^x in a way that exposes b^y).

from fiat-crypto.

Closed due to inactivity.

from fiat-crypto.