modulus proof endlessly validates

Question

Why does this never verify? It's mostly equations and it seems like they're pretty much all equalities. Am I relying too heavily on the modulus axioms causing the problem? It doesn't return any feedback.

I have figured out that it is getting stuck on remainderTheorem, but the difference is that it does not get stuck on remainderTheorem(b, p, c); but it does for remainderTheorem(a,p*q,b). Why does p * q break it?

/*
Suppose ≡mod and ≡mod, then we have
=+=+(+)=(+)+
so that ≡mod
*/

lemma congruencePersistMod(a: nat, b: nat, p: nat, q: nat, c: nat)
    requires p != 0
    requires q != 0
    requires p*q != 0
    requires a % p*q == b;
    requires b % p == c;

    ensures a % p == c
{
    assert c % p == c;
    remainderTheorem(a,p*q,b);
    var r :| divAdd(r, p*q, b) == a;
    remainderTheorem(b, p, c);
    var s :| divAdd(s, p, c) == b;
    calc {
        a % p;
        (r * p * q + b) % p;
        (r * p * q + s*p + c) % p;
        (p*(r*q+s) + c) % p;
        == {modPlus(p*(r*q+s), c, p);}
        ( ((p*(r*q+ s)) % p) + (c % p)) % p;
        == {selfAnnihilation(p, (r*q+s));}
        (0 + c % p) % p;
        c % p;
        c;
    }
}

function divAdd(b: int, a: int, c: int): int {
    b * a + c
}

lemma remainderTheorem(x: int, a: int, c: int)
    requires a != 0
    requires x % a == c;
    ensures exists q  :: divAdd(q,a,c) == x
{
   var q := (x-c) / a;
   remainderSubtract(x,a,c);
   assert divAdd(q,a,c) == x;
}

lemma remainderSubtract(x: int, a: int, c: int) 
    requires a != 0
    requires c == x % a
    ensures (x-c) % a == 0

lemma modPlus(a: int, b: int, n: int)
    requires n != 0;
    ensures ((a % n) + (b % n)) % n == (a + b) % n

lemma selfAnnihilation(a: int, b: int) 
    requires a != 0
    ensures (b*a) % a == 0
{
    calc {
        (b * a) % a;
        {modMultiplication(a,0,b,b%a,a);}
        (0 * b%a) % a;
        0;
    }
}

lemma modMultiplication(aone: int, bone: int, atwo: int, btwo: int, n: int)
    requires n != 0
    requires aone % n == bone
    requires atwo % n == btwo
    ensures (aone * atwo) % n == (bone * btwo) % n 

Answer 1

Works but it's feels so silly...

function {:opaque} prod(x: int, y: int): int {
    x * y
}
function divAdd(b: int, a: int, c: int): int {
    prod(b,a) + c
}
lemma prodCommutes(a: int, b: int)
    ensures prod(a,b) == prod(b,a)
{
    reveal prod();
}

lemma prodCommutesThree(a: int, b: int, c: int) 
    ensures prod(a, prod(b, c)) == prod(b, prod(a, c))
{
    reveal prod();
}

lemma prodDistributes(a: int, b: int, c: int)
    ensures prod(a, b + c) == prod(a,b) + prod(a,c)
{
    reveal prod();
}

lemma prodSelfAnnihilation(a: int, b: int) 
    requires a != 0
    ensures prod(a,b) % a == 0
{
    reveal prod();
    calc {
        (b * a) % a;
        {modMultiplication(a,0,b,b%a,a);}
        (0 * b%a) % a;
        0;
    }
}

lemma congruencePersistMod(a: nat, b: nat, p: nat, q: nat, c: nat)
    requires p != 0
    requires q != 0
    requires prod(p,q) != 0
    requires a % prod(p,q) == b;
    requires b % p == c;

    ensures a % p == c
{
    assert c % p == c;
    remainderTheorem(a, prod(p,q), b);
    var r :| divAdd(r, prod(p,q), b) == a;
    remainderTheorem(b, p, c);
    var s :| divAdd(s, p, c) == b;
    calc {
        a % p;
        (prod(r, prod(p,q)) + b) % p;
        (prod(r, prod(p,q)) + prod(s, p) + c) % p;
        == {prodCommutes(s,p);}
        (prod(r, prod(p,q)) + prod(p, s) + c) % p;
        == {prodCommutesThree(r, p, q);}
        (prod(p, prod(r,q)) + prod(p, s) + c) % p;
        == {prodDistributes(p,prod(r,q),s);}
        (prod(p, prod(r,q) + s) + c) % p;
        == {modPlus(prod(p, prod(r,q) + s),c,p);}
        (prod(p, prod(r,q) + s) % p + c % p) % p;
        (prod(p, prod(r,q) + s) % p + c) % p;
        == {prodSelfAnnihilation(p, prod(r,q) + s);}
        (0 + c) % p;
        c % p; 
        c;
    }
}