Laziness in Cryptol missing in SAW

[weaversa]

The following works fine in cryptol (d67f6de), but hangs in saw (5ef5ca0)

sawscript> let {{ [a, b] = take ([0..]:[_][32]) }}
sawscript> print {{ a }}
^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^Csaw: too many pending signals

Cryptol> let [a, b] = take ([0..]:[_][32])
Cryptol> a
0x00000000

[brianhuffman]

The problem here is the data structure that saw uses to represent finite sequences. You're making a sequence with type [4294967296][32], and I believe saw uses ordinary Haskell arrays or vectors for all finite vector sizes. Allocating and initializing one with 2^32 elements takes a long time. Here's another example that will produce the same result:

sawscript> print {{ (zero : [4294967296][32]) @ 0 }}

Cryptol has some special clever representations for sequences that are really large but still finite. We should probably adapt saw to use the same representation.

[jpziegler]

For completeness I'll add that, at least in the case of the example above, you can use ... to get around this bug. Using ... generates an infinite sequence, so SAW has no choice but to be lazy!

sawscript> let {{ [a,b] = take ([0...]:[_][32]) }}
sawscript> print {{ a }}
0

I will say that the .. versus ... question continues to confuse Cryptol users both new and old. Might not be anything to do to resolve that, but there it is. (I personally like having both.)

[brianhuffman]

We are going to try to rework the saw-core interpreter to reuse more code from the Cryptol interpreter. Problems like this should be taken care of as a side effect of that effort. (See e.g. GaloisInc/cryptol#651)