Rewriter loop?

[weaversa]

Is the rewriter going in a loop here? If so, I'm not sure why...

$ cat bug2.saw
let {{
  type ZP = Z 653

  BVtoZP : {n} (fin n) => [n] -> ZP
  BVtoZP v =  fromInteger (toInteger v)

  ZPtoBV: {n} (fin n) => ZP -> [n]
  ZPtoBV v = fromInteger (fromZ v)

  func: {n} (fin n) => [n] -> [n] -> [n]
  func x y = ZPtoBV ((BVtoZP x) * (BVtoZP y))
}};

let p = {{\(x:[32]) -> \y -> (func x y) == (func y x) }};


let p1 = {{\(x:[32]) -> \y -> func (func x y) (func x y) ==
                              func (func y x) (func x y)}};

commutes <- prove_print z3 p;
ss1 <- addsimp commutes empty_ss;
p2 <- rewrite ss1 (rewrite (cryptol_ss ()) p1);
print "hello";
prove_print z3  p2;

$ saw bug2.saw
[01:34:21.684] Loading file "bug2.saw"
[01:34:21.781] Valid
^C[01:34:23.204] user interrupt

[atomb]

Yeah, that looks like a rewriter loop. Rewriting for commutativity manually doesn't tend to work well. The rule p, if it applies once, will always continue to apply to the resulting term. So it'll just keep swapping the arguments to func back and forth as long as you're willing to wait.

[weaversa]

There is some loop detection in Cryptol. We get a <<loop>> error sometimes...could something similar be applied here?

[brianhuffman]

func x y == func y x is an example of what is called a "permutative rewrite rule", as the right and left sides are equivalent up to a permutation of the variable names. Some theorem provers (e.g. Isabelle) have special support for rewriting with permutative rewrite rules. Basically what you need to do is to check each rewrite rule and put a special tag on the permutative ones; then if a permutative rewrite rule matches a subterm, you only perform the rewrite if the new subterm is strictly less than the old one according to some well-founded ordering on terms. The term ordering has to be carefully designed in order for this to work well with other rewrite rules, e.g. if you want to rewrite with both associativity and commutativity rules for some operator.

Of course, even with these extra checks on permutative rewrite rules, it's still possible to make a rewriter loop using combinations of two or more rules. It might be possible (but might be expensive) to detect when the rewriter is creating the same exact term repeatedly. But other rewrite rules can yield infinite loops of ever-larger terms that are never the same, so in general I don't think it's possible to prevent all forms of looping rewrites.

One easy thing we could do is add some configurable resource limits to the saw-core rewriter, so that the rewriter could quit with an error message instead of just running forever in situations like this.

[weaversa]

Does @msaaltink's recent work (GaloisInc/saw-core#173) apply here?

[msaaltink]

It should apply to these specific rules. It is certainly not going to prevent or even detect all loops,though; there are rules like \ x -> f x == f (f x) or \ x -> g 0 x == g 0 0 that are not permutative but still cause looping,and there can be combinations of rules, each fine by itself, that loop. The small rewriter patch for permutative rewriting does not deal with any of that.

I think ACL2 has some interesting loop detection capability but I forget the details.

[robdockins]

The termination of rewriting systems is, in general, a very difficult and deep topic. Are there other low-hanging fruit here we can pick, or should we close this ticket?

[langston-barrett]

I recently learned about E-graphs, which are data structures for efficiently storing many equivalent/rewritten versions of the same term and performaing pattern-matching style rewrites on them. These are nice because they make the order of rewrites less important, and they "saturate", making issues with rewrites like commutativity and associativity less serious.

This definitely isn't "low-hanging fruit", but might be worth considering if the rewriter is ever overhauled.

[brianhuffman]

I agree that it probably makes sense to close this ticket, because it's kind of vague and open-ended. We already have a more specific issue #1266 about choosing the right term ordering for permutative rewrite rules. If we want to implement some other specific fix, e.g. adding some kind of resource bounds to the rewriter, we should open a separate ticket for that.