Rewriting SAW core vector folds #1811
Conversation
…rewriter to be able to rewrite with these axioms by allowing patterns of the form Succ x to match nat literals
| fnc_lemma <- proveit {{ \x y z i -> (fnc' (fnc (x, y, z) i) i).0 == x }} z3; | ||
|
|
||
| proveit {{ foldFunctionInverse }} do { | ||
| unfolding [ "foldFunctionInverse" |
There was a problem hiding this comment.
I think this is redundant, goal_normalize ["fnc", "fnc'"]; should do this as well.
| , "foldFunction'" | ||
| ]; | ||
| goal_normalize ["fnc", "fnc'"]; | ||
| simplify (add_prelude_eqs ["foldl_cons","foldl_nil", |
There was a problem hiding this comment.
Did you mean to use fnc_lemma here with the use_lemmas function you created above?
Also, this script would be more convincing if the trivial prover was used (rather than z3).
There was a problem hiding this comment.
I agree, that it would be a better example if we could figure out a way to use fnc_lemma, but unfortunately it doesn't match any term in the goal. I tried for a while to modify fnc_lemma to actually apply in this case, but couldn't figure out a way to make it work, so I just had Z3 unfold all the calls to fnc and fnc' to prove the result. After rewriting all the foldls away, the resulting term looks like
\x y z -> (fnc' (fnc' (... (fnc' ((fnc (fnc (... (fnc (x,y,z) 0)...) 14) 15).0, y, z) 15) ... 1) 0).0 == True
So fnc_lemma needs to somehow rewrite a term of that form, probably something of the form fnc' ((fnc tup i).0, y, z) i but I wasn't sure what to rewrite that to, since the final .0 doesn't apply until all 16 fnc' applications happen.
There was a problem hiding this comment.
The purpose of this example for now is to demonstrate rewriting folds, and it does that. So I'm going to merge this PR now. I'd love to figure out the "right" way to write this lemma, but let's not wait on that before merging this PR.
eddywestbrook
added
ready-to-merge
The
foldlandfoldroperations in SAW core do not have any axioms to reason about them, which is a problem because they areprimitives, and so don't compute. This PR adds axioms that define their behavior, in terms of a pair of rules for each operation, one for the0length case and one for theSucclength case. These rules are written in terms of the vectorheadandtailoperations, which also needed rewrite rules to define their behavior when applied to a vector created bygen.In testing these new rules, I also discovered that the SAW rewriter was not able to match a term of the form
Succ xagainst a natural number literal. So this PR also includes a fix for that problem. I also added some comments to explain how the rewriter works in more detail, as I had to figure out that detail in order to modify the rewriter.The
intTestsdirectory has been expanded with a new test,test_fold_rewrite_proof, that uses this new functionality to prove a property about a simple cryptol function.