`%` bug

[kidherofun]

(1 ^ 2 + 2 ^ 2 + 3 ^ 2 + 4 ^ 2 + 5 ^ 2 + 6 ^ 2 + 7 ^ 2 + 8 ^ 2 + 9 ^ 2) % 10 works well.

But the following code is not:

claim:
    forall n Z:
        sum = 1 ^ 2 + 2 ^ 2 + 3 ^ 2 + 4 ^ 2 + 5 ^ 2 + 6 ^ 2 + 7 ^ 2 + 8 ^ 2 + 9 ^ 2
        digit_sum = sum % 10
        =>:
            digit_sum = 5
    prove:
        sum = 1 + 4 + 9 + 16 + 25 + 36 + 49 + 64 + 81 = 285
        digit_sum = 285 % 10 = 5

The Error from terminal is:

Error: failed :( line 7:
some atoms in the following fact are undeclared:
forall n Z:
    sum = (((((((((1 ^ 2) + (2 ^ 2)) + (3 ^ 2)) + (4 ^ 2)) + (5 ^ 2)) + (6 ^ 2)) + (7 ^ 2)) + (8 ^ 2)) + (9 ^ 2))
    digit_sum = (sum %!)(MISSING)
    =>:
        digit_sum = 5

[yuniruyuni]

I'm not sure but it seems sum and digit_sum is not yet introduced in the context so you should write following:

claim:
    forall n, sum, digit_sum Z:
        sum = 1 ^ 2 + 2 ^ 2 + 3 ^ 2 + 4 ^ 2 + 5 ^ 2 + 6 ^ 2 + 7 ^ 2 + 8 ^ 2 + 9 ^ 2
        digit_sum = sum % 10
        =>:
            digit_sum = 5
    prove:
        sum = 1 + 4 + 9 + 16 + 25 + 36 + 49 + 64 + 81 = 285
        digit_sum = 285 % 10
        digit_sum = 5

I think litex's forall X: Y means forall X s.t. Y

[kidherofun]

claim: forall n, sum, digit_sum Z: sum = 1 ^ 2 + 2 ^ 2 + 3 ^ 2 + 4 ^ 2 + 5 ^ 2 + 6 ^ 2 + 7 ^ 2 + 8 ^ 2 + 9 ^ 2 digit_sum = sum % 10 =>: digit_sum = 5 prove: sum = 1 + 4 + 9 + 16 + 25 + 36 + 49 + 64 + 81 = 285 digit_sum = 285 % 10 digit_sum = 5

Thank you. That works!

[malloc-realloc]

@yuniruyuni THANK YOU! You are the first community participant who isn't known to our core team but has been answering questions under the Litex repository! We would love to get to know you better. Could you please share your email with us? Also, if you could say a few kind words about Litex that we could feature on our website as a community voice, we would greatly appreciate it! Thank you!