Pass universally quantified assumptions to Z3

[nano-o]

I often have to prove by rewriting that two terms involving field operations are equivalent. Unfortunately, SAW's SMT tactics are seemingly of no help due to the bitwidth I am dealing with.

However, it seems that Z3 can handle some of those goals if passed equations saying e.g. that multiplication is commutative. The problem is that if I express commutativity of multiplication as a universally quantified formula in my SAW goal, it does not appear in the output passed to the solver. Would it be possible to change that? Alternatively, are there other ways to deal with those goals? (at the moment I am resorting to rewriting within SAW using simplify, but it is tedious).

Here is a simplified example drawn from a recent proof:

let {{
  type vec_t = [384]
  p = 0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab
  mul : vec_t -> vec_t -> vec_t
  mul x y = undefined // this would be e.g. multiplication modulo p
  add : vec_t -> vec_t -> vec_t
  add x y = undefined
  term1 x y z1 z2 z3 = add (mul (add (mul (add (mul x y) z1) x) z2) x) z3
  term2 x y z1 z2 z3 = add (mul y (mul x (mul x x))) (add (mul z1 (mul x x)) (add (mul z2 x) z3))
}};

lemmas <- for
  [ {{ \x y -> mul x y == mul y x }}
  , {{ \x y -> add x y == add y x }}
  , {{ \x y z -> mul (mul x y) z == mul x (mul y z) }}
  , {{ \x y z -> add (add x y) z == add x (add y z) }}
  , {{ \x y z -> mul (add x y) z == add (mul x z) (mul y z) }}
  ]
  (prove_print assume_unsat);

enable_experimental;

_ <- prove_print
  (do {
    unfolding ["term1","term2"];
    for lemmas goal_insert;
    print_goal;
    offline_w4_unint_z3 ["mul","add"] "test_w4"; // the lemmas have dissapeared
  })
  {{ \x y z1 z2 z3 -> term1 x y z1 z2 z3 == term2 x y z1 z2 z3 }};

Z3 does fine with the following encoding, so I'm hoping it would too when called from SAW if passed the lemmas:

(declare-fun mul ((_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun add ((_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-const x (_ BitVec 384))
(declare-const y (_ BitVec 384))
(declare-const z1 (_ BitVec 384))
(declare-const z2 (_ BitVec 384))
(declare-const z3 (_ BitVec 384))
(assert (forall ((x (_ BitVec 384)) (y (_ BitVec 384))) (= (mul x y) (mul y x))))
(assert (forall ((x (_ BitVec 384)) (y (_ BitVec 384))) (= (add x y) (add y x))))
(assert (forall ((x (_ BitVec 384)) (y (_ BitVec 384)) (z (_ BitVec 384))) (= (mul (mul x y) z) (mul x (mul y z)))))
(assert (forall ((x (_ BitVec 384)) (y (_ BitVec 384)) (z (_ BitVec 384))) (= (add (add x y) z) (add x (add y z)))))
(assert (forall ((x (_ BitVec 384)) (y (_ BitVec 384)) (z (_ BitVec 384))) (= (mul (add x y) z) (add (mul x z) (mul y z)))))
(assert (not (= (add (mul (add (mul (add (mul x y) z1) x) z2) x) z3) (add (mul y (mul x (mul x x))) (add (mul z1 (mul x x)) (add (mul z2 x) z3))))))
(check-sat)

[atomb]

We've been considering this for a long time, but had held off on implementing it mostly because it wasn't clear whether we could build a useful solver-independent interface to it. However, maybe it's worth just going ahead and doing it in a solver-specific way, and perhaps generalize it later if that seems feasible. I believe What4 does support passing in universally quantified lemmas, so the next step might be to decide what the SAWScript API should look like.

[atomb]

I wonder if @brianhuffman or @robdockins have a sense for how hard this would be with the current state of the What4 backend.

[nano-o]

What I got from the discussion on the SAW channel is that What4 already supports quantified formulas, and so I presume that making sure those formulas are passed to Z3 is a matter of calling What4 the right way. It would be useful for the blst project if someone could throw together a saw-scrip command that does it, just for us to try it out (no need for anything fancy like support triggers etc. I would just like to see the universally quantified formulas in my saw-core terms make it to Z3). We are spending a significant portion of our time doing manual rewrites of field-arithmetic expressions, so this could potentially save us quite a bit of work. Alternatively, could someone give me a few pointers to get me started on implementing it myself?