Assuming the postcondition fails when using `forall_arith`

[jaybosamiya]

use vstd::prelude::*;

verus! {

proof fn what_in_tarnation(n: int)
    requires n > 0
    ensures  
        forall_arith ( |x: int| #[trigger]((x + n) % n) == x % n ),
{
    assume(forall_arith ( |x: int| #[trigger]((x + n) % n) == x % n ) );
}

}

fn main() {}

fails to verify on current main: (playground)

note: verifying root module

error: postcondition not satisfied
  --> /playground/src/main.rs:9:1
   |
8  |           forall_arith ( |x: int| #[trigger]((x + n) % n) == x % n ),
   |           ---------------------------------------------------------- failed this postcondition
9  | / {
10 | |     assume(forall_arith ( |x: int| #[trigger]((x + n) % n) == x % n ) );
11 | | }
   | |_^ at the end of the function body

error: aborting due to previous error

Notice that the ensures clause is exactly equivalent to the assume. Using assume(false) succeeds fwiw.

This originally manifested on the https://github.com/verus-lang/verus/tree/quant_arith branch (where @ahuoguo appeared to be facing instability on some proofs he was writing). I helped minimize his instability example down (to the above, but with forall instead of forall_arith). This minimized example is a particularly bad incompleteness since the assumed clause is exactly the same as the post-condition, so it seems practically impossible to work-around by writing any more proof.

Looking at the SMT2 encoding, the encoding looks (at least at first glance) basically the same as what I'd expect to be there, so I tried to manually write an equivalent query by-hand for z3 (where it succeeded in showing unsat just fine; it gives the unknown on the Verus one with (:reason-unknown "(incomplete (theory arithmetic))")), so somewhere along the way, it appears to be confused with everything else going on.

[jaybosamiya]

Some more info while chasing this down:

1. Original SMT file produced from Verus code above: gives unknown (incomplete theory arithmetic)

2. Manually grabbing just the relevant assert: gives unsat

(declare-const %%query%% Bool)
(declare-fun EucMod (Int Int) Int)
(declare-const n~2@ Int)
(declare-const %%location_label%%0 Bool)
(assert
  (=>
   %%query%%
   (not (=>
     (forall ((x~70$ Int)) (!
       (= (EucMod (+ x~70$ n~2@) n~2@) (EucMod x~70$ n~2@))
       :pattern ((EucMod (+ x~70$ n~2@) n~2@))
       :qid user_instability3_modified__what_in_tarnation_2
       :skolemid skolem_user_instability3_modified__what_in_tarnation_2
     ))
     (=>
      %%location_label%%0
      (forall ((x~33$ Int)) (!
        (= (EucMod (+ x~33$ n~2@) n~2@) (EucMod x~33$ n~2@))
        :pattern ((EucMod (+ x~33$ n~2@) n~2@))
        :qid user_instability3_modified__what_in_tarnation_1
        :skolemid skolem_user_instability3_modified__what_in_tarnation_1
 )))))))
(assert %%query%%)
(assert %%location_label%%0)
(check-sat)

3. Automatically minimized version of the original Verus query that gives unknown (note: this query is not equivalent to the above, just an automatic minimization of the original query from (1) with the criteria that it should still give unknown; so not much can be gleaned from this directly, other than just what sorts of features tend to show up):

   (set-option :smt.arith.solver 2)
   (set-option :smt.arith.nl false)
   (declare-fun a (Int Int) Int)
   (assert (forall ((b Int) (c Int)) (! (= (a b c) (mod b c)))))
   (push)
   (declare-const d~2@ Int)
   (declare-const %%f%%0 Bool)
   (declare-const %%e%% Bool)
   (assert (= %%e%%
          (not (> (forall (($ Int)) (! (= 0 0)))
                  (> %%f%%0 (forall (($ Int)) (! (= 0 (a 3 d~2@)))))))))
   (check-sat)
   (get-info :reason-unknown)

Based on the above, it appears that the (set-option :smt.arith.solver 2), (set-option :smt.arith.nl false), and/or (push) might be relevant, but even if I add those to the manually-minimized query (2), it still gives unsat; so it seems like the issue might not be all that obvious.

[ahuoguo]

The issue raised above now verifies individually, but the following code is still in trouble:

#[verifier(spinoff_prover)]
proof fn lemma_mod_basics_auto(n: int)
    requires n > 0
    ensures  
        forall |x: int| #[trigger]((x + n) % n) == x % n,
        forall |x: int| #[trigger]((x - n) % n) == x % n,
        forall |x: int| #[trigger]((x + n) / n) == x / n + 1,
        forall |x: int| #[trigger]((x - n) / n) == x / n - 1,
        forall |x: int| 0 <= x < n <==> #[trigger](x % n) == x,
{
    assume(forall |x: int| #[trigger]((x + n) % n) == x % n);
    assume(forall |x: int| #[trigger]((x - n) % n) == x % n);
    assume(forall |x: int| #[trigger]((x + n) / n) == x / n + 1);    
    assume(forall |x: int| #[trigger]((x - n) % n) == x % n);
    assume(forall |x: int| 0 <= x < n <==> #[trigger](x % n) == x);
}

However, assuming the postconditions all together verifies

#[verifier(spinoff_prover)]
proof fn lemma_mod_basics_auto1(n: int)
    requires n > 0
    ensures  
        forall |x: int| #[trigger]((x + n) % n) == x % n,
        forall |x: int| #[trigger]((x - n) % n) == x % n,
        forall |x: int| #[trigger]((x + n) / n) == x / n + 1,
        forall |x: int| #[trigger]((x - n) / n) == x / n - 1,
        forall |x: int| 0 <= x < n <==> #[trigger](x % n) == x,
{
    assume( {
        &&& forall |x: int| #[trigger]((x + n) % n) == x % n
        &&& forall |x: int| #[trigger]((x - n) % n) == x % n
        &&& forall |x: int| #[trigger]((x + n) / n) == x / n + 1
        &&& forall |x: int| #[trigger]((x - n) / n) == x / n - 1
        &&& forall |x: int| 0 <= x < n <==> #[trigger](x % n) == x
    }    
)
}

[Chris-Hawblitzel]

It looks like forall|x: int| #[trigger]((x - n) / n) == x / n - 1 is missing in the failing code.

[ahuoguo]

OMG my bad! Sorry for not checking this. The new design for quant arith https://github.com/verus-lang/verus/pull/625 should fix this.