Loop detection too strict

[weaversa]

I'm really surprised that Cryptol thinks it's stuck in a loop here! Any idea about what's going on? The reference evaluator seems to work though.

f : [1] -> [2]
f x = out
  where out = x # [out@0]

g : [1] -> [2]
g x = out
  where out = x # (take out)

$ ./cryptol-2.7.1-2019-08-21-OSX-64/bin/cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.7.1 (12805be, modified)

Loading module Cryptol
Cryptol> :l test.cry
Loading module Cryptol
Loading module Main
Main> f 0
0x0
Main> g 0

<<loop>> while evaluating (at ./test.cry:7:9--7:12, Main::out)
Main> :eval f 0
0x0
Main> :eval g 0
0x0
Main> 

[yav]

This is probably to do with the packed representation for sequences of bits. As a reference point, the following does not loop:

g : [1] [8] -> [2] [8]
g x = out
  where out = x # take out

[brianhuffman]

It would be nice to fix this, but it's tricky to get the behavior correct without seriously hurting performance in the common case.

[robdockins]

After looking into this some more, the basic problem here is that # is too strict on its inputs at bitvector types. This is done very specifically to avoid having to fall back to the unpacked "bit by bit" representation of bitvectors unless absolutely necessary. Instead we force bitvector values in order to see if they are actually packed representations, which we can concatenate directly.

One option I considered to fix this bug is to redefine the semantics so that # is strict in its arguments. Unfortunately, that totally breaks the common Cryptol style of writing recurrences with an initial segment concatenated onto a tail portion that is defined recursively in terms of the sequence being defined. A strict # causes such definitions to fail.

We could instead just codify the current situation, which is that # is strict in its arguments, but only at bitvector types. This is... rather unsatisfying.

I've tried a few methods to make # lazier in its arguments, but so far they have all caused pretty extreme performance regressions. I still have a few ideas I want to try.

[robdockins]

Turns out, the particular example I was worried about here was doing a lot of hashing using SuiteB::sha384, and the added laziness of # was interacting badly with the setup phase of the hash function, where padding is added and then the message is split into blocks. Adding an rnf call to the hash padding phase forces a packed word before being split into blocks of work, and this squashes the space leak.