cryptol-remote-api runtime error

[michaelabernardo]

Hi there! I'm getting a runtime error using cryptol-remote-api when I use undefined in a property, even if it doesn't get used. Checking the property in the Cryptol interpreter passes as expected, but it fails in cryptol-remote-api. It worked previously, but stopped working with a newer version of the nightly Docker image last week.

Example Cryptol Code:

undefXor : {n} (fin n, n <= 16) => [32] -> [16] -> [n] -> [32]
undefXor a b c = a ^ (b # c # 0)

property testundefXor = undefXor`{n=0} 0x00000001 0x0001 undefined == 0x00010001

Error when checking property on cryptol-remote-api:

argo_client.interaction.ArgoException: Internal error Run-time error: undefined

[atomb]

Thanks for pointing this out! I suspect it's a consequence of some refactoring we recently did to properly support the newtype construct. We'll need to adjust how we handle it a bit, it seems.

[atomb]

I'm wrong about the previous: that work hasn't landed yet. But, in the process of finishing it up, we'll consider this issue. It's possible that the changes so far will already fix it.

[pnwamk]

This happens to not be an issue with the remote API per se, but a result from some changes in how Cryptol treats undefined and # since the 2.11 release (and I believe these changes are only noticeable in some corner cases such as this one). In particular, # is now strict in the structure of sequences (i.e., the finite portions of a sequence's spine structure is evaluated and laid out while the actual elements and/or infinite portions or the sequence remain unevaluated), which is why that usage of undefined is now raising an error.

As for the testundefXor property, it will pass with the new updated undefined/# handling if the third parameter undefined is replaced with repeat undefined, as the former ends up being strictly evaluated and raising an error when it is an argument to # while the latter is not.

[pnwamk]

If there's a lingering issue or another behavioral change you're noticing related to this plese feel free to reopen the issue.