Performance regression: SIV-rfc5297.md

[robdockins]

Trying to compute the test vectors in this example using the new evaluator consumes an absurd amount of memory before dying. This is a regression from the evaluator in Cryptol 2.4.0, where performance is acceptable.

The problem appears to be related to the ctr64 function. Hypothesis: the definition of stream forces the computation down to a stream of individual bits, which are not being handled intelligently, for some reason.

[robdockins]

The ctr64 function is in fact the culprit. The troublesome case has to do with the definition of ivs below:

ctr64 : {n} (2^^71 - 128 >= n) => Key -> [128] -> [n] -> [n]
ctr64 k iv pt = pt ^ take stream
 where
 stream = join [E(k,v) | v <- ivs]
 ivs    = [take `{64} iv # cnt + i | i <- [0,1..]]
 cnt    = drop `{back=64} iv

The issue is that the enumeration [0,1..] enumerates all 64-bit integers. This isn't ordinarily a problem because sequence positions are only evaluated when they are forced, and this function will only need a few of the positions. HOWEVER, sequences of Bit are treated specially, and the call to join in the definition of stream generates a value of type [128 * 2^64]. The evaluator then attempts to evaluate every single one of those bit values and place them into a vector, from which it then intends to project out only the first n bits. Unfortunately, there is no machine on the planet with enough RAM for this intermediate data structure, so the program eats memory until it dies.

This issue is essentially another incarnation of issue GaloisInc/saw-script#11. A short-term fix is to use the infinite enumeration [0...] instead; infinite streams have a different representation which avoids this issue.

A proper long-term fix is to be more intelligent about the representation of bit sequences. Very long bitvectors, like this one, should probably be treated as "effectively infinite" and use the same representations that are used for infinite streams.

[robdockins]

Fixed by 771d07f

This patch, and nearby related ones, changes the representation of unpacked bitvectors to be similar to the one used for sequences at other types, and forces a change to the unpacked representation when the size of a bitvector crosses a size threshold (2^16 bits, currently... I'm not sure what is a principled way to decide on this value).

This fixes the original problem and does not seem to introduce significant performance degradations elsewhere.