Support implications as rewrite rules

[mrogers67]

Suppose you have a conditional rewrite rule that only holds for arguments in a certain range:

lemma <- prove_print z3 (rewrite (cryptol_ss ()) {{
  \a b -> (a < 8 /\ b < 8) ==> (f a b == g a b)
}});

SAW could use it as a rewrite rule if it finds a matching predicate of an enclosing implication, which e.g. might be due to a given precondition.

let spec = do {
    a <- llvm_fresh_var "a" (llvm_int 32);
    b <- llvm_fresh_var “b” (llvm_int 32);

    llvm_precond {{ a < 8 /\ b < 8 }};

    llvm_execute_func [llvm_term {{ a }}, llvm_term {{ b }}];
    llvm_return (llvm_term {{ g a b }});
};

llvm_verify m “func” [fov] false spec do {
  simplify (simpset [lemma]);
  z3;
};

Perhaps there’s already another way to do these kinds of transformations with SAW?

[sauclovian-g]

In theory you should be able to do that (AIUI) but it has to match the goal at the saw-core level, and there's many reasons it might not. You can use print_goal in the proof-script context to examine the goal, and just printing the value of the lemma from the repl will show its saw-core form.

Unfortunately they probably don't match, and then it's very difficult to wrangle this stuff. You can start a proof-script repl with proof_subshell () (requires enable_experimental) but it's not at all easy to use even by theorem-prover standards.

[sauclovian-g]

Hmm, I think I misunderstood.

I can't even get it to accept the initial lemma (I get

sequentToSATQuery: expected first order type or assertion:
isort 0

)

let alone actually rewrite with it, which after sleeping on it I think is probably/possibly also not supported (since simpsets are intended for autorewriting)

...so the issue is not that you tried this and it should work, but it didn't go and it isn't clear why (since that is certainly a something that could happen) but that it isn't even expected to work. (But it seems like it should.)

Is that right?

[sauclovian-g]

here's a related standalone example:

enable_experimental;

let {{
   x = 3
   y = 3
   prop = x == y ==> y == x
}};

lemma1 <- prove_print z3 (rewrite (cryptol_ss()) {{
  \a -> a == 3 ==> a == y
}});

lemma2 <- prove_print z3 (rewrite (cryptol_ss()) {{
  x == y
}});

print "With lemma1:";

prove_print (do {
   goal_normalize ["x", "y"];
   print_goal;
   simplify (addsimp lemma1 empty_ss);
   print_goal;
   z3;
}) {{ prop }};

print "With lemma2:";

prove_print (do {
   goal_normalize ["x", "y"];
   print_goal;
   simplify (addsimp lemma2 empty_ss);
   print_goal;
   z3;
}) {{ prop }};

[msaaltink]

There's a hack to get the effect of conditional rewriting like this, that we used (or tried to use; I forget exactly) in some of the BLST proofs a few years ago. The trick is to make an unconditional rewrite rule, but prevent it from looping on itself. So we define a function apply like this:

let {{ apply f x = f x }};

then state your fact

lemma <- prove_print z3 (rewrite (cryptol_ss ()) {{
  \a b -> (a < 8 /\ b < 8) ==> (f a b == g a b)
}});

as an unconditional rewrite:

lemma' <- prove_print z3 (rewrite (cryptol_ss ()) {{
  \a b -> f a b == if (a < 8 /\ b < 8) then g a b else apply f a b
}});

The apply keeps it from looping, and can be removed from a formula with unfolding ["apply"] in case a rewrite does not work (that is, the condition does not hold).

Here's an example proof:

prove_print do {
  simplify (addsimp lemma' (cryptol_ss ()));
  print_goal;
  w4_unint_z3 ["f","g"];
  }
{{ \x y -> x+y < 8 ==> f (x+y) 3 == g (x+y) 3 }};

where because of the rewriting we can prove without using the definitions of f and g.

Admittedly this is a gross hack, and having real support for conditional rewriting would be much better.