Certain recursive definitions cause non-termination in the symbolic backend

[brianhuffman]

Here's an example, which was derived by minimizing SHA256MessageSchedule in examples/MiniLock/prim/SHA256.cry:

Cryptol> let foo (x:[8]) = xs where xs = [x, xs@0]
Cryptol> :prove \x -> foo x == [x, x]
^CCtrl-C
Cryptol> :prove foo 3 == [3, 3]
^CCtrl-C

Both proofs get stuck before making it to the external prover.

[robdockins]

Interestingly, the SAW symbolic simulator seems to deal with this just fine:

sawscript> let {{ foo (x:[8]) = xs where xs = [x, xs@0] }}
sawscript> prove z3 {{ \x -> foo x == [x,x] }};
Valid

[brianhuffman]

Strangely enough, the example works just fine if I change the type from [8] to anything that is not a bitvector type:

Cryptol> :prove \(x:[8]) -> [x,x] == (xs where xs = [x, xs@0])
^CCtrl-C
Cryptol> :prove \(x:[2][8]) -> [x,x] == (xs where xs = [x, xs@0])
Q.E.D.
Cryptol> :prove \(x:Bit) -> [x,x] == (xs where xs = [x, xs@0])
Q.E.D.
Cryptol> :prove \(x:([8],Bit)) -> [x,x] == (xs where xs = [x, xs@0])
Q.E.D.

@robdockins: What git revision of SAW are you using? SAW also fails to terminate for me on this example (with any type, not just bitvectors).

[robdockins]

Ah... that actually doesn't surprise me. The simulators are overaggressive about forcing things at bitvector types. I suspect the new simulator branch I'm working on will fix this once it's finished.

The SAW version I have lying around her is a somewhat older build from late Feburary.
GaloisInc/saw-script@b08b125

[brianhuffman]

I think I have it figured out. It seems that the problem is with the indexing operator (@), which is too strict. For lists of bitvectors, the function atV in Cryptol/Symbolic/Prims.hs tries to use the lookup function svSelect from SBV (as an optimization). Unfortunately, this has the side effect of forcing every element of the list.

[robdockins]

This issue is fixed by the evaluator rewrite #338