Issue with by (compute) with quantifiers causes Rust to panic

[amarshah1]

Running the following code:

` pub closed spec fn is_prime(n : nat ) -> bool { forall|i : nat| 1 < i < n ==> #[trigger] (n % i) != 0 } 2024-09-20-17-09-47.zip

proof fn sanity_check()
    {
        assert (is_prime(7)) by (compute);
}

`

Gives the error:

thread '<unnamed>' panicked at rust_verify/src/verifier.rs:780:21: internal error: generated ill-typed AIR code: error 'error 'error 'error 'use of undeclared variable n!' in expression 'n!'' in expression '(%I n!)'' in expression '(EucMod (%I n!) i$)'' in expression '(nClip (EucMod (%I n!) i$))' note: run withRUST_BACKTRACE=1environment variable to display a backtrace thread '<unnamed>' panicked at rust_verify/src/verifier.rs:2108:29: worker thread panicked

We think Verus should catch this and return an error, instead of panicking. Thanks!

See the attached zip archive: 2024-09-20-17-09-47.zip

[parno]

Yep, that looks buggy. I suspect that it tried to evaluate down in the quantifier, realized it couldn't make progress (since quantifiers are not supported) and lost track of the n argument that's passed to is_prime.

I'll try to look into it at some point.