Unhandled exception (index out of bounds)

[TomMD]

I'm seeing:

./Data/Vector/Generic.hs:249 ((!)): index out of bounds (96,0)

From the below code which was intended to prove the Cryptol implementation of crypto_secretbox from NaCl is identical to itself.

import "CryptoBox.cry";

let main : TopLevel () = do {
    let cry_crypto_secretbox = {{ \s k n -> crypto_secretbox (s : [1][8]) k n }};
    cryAIG  <- bitblast cry_crypto_secretbox;
    res <- cec cryAIG cryAIG;
    print res;
};

To reproduce just git-clone GaloisInc/crylock, add the above code to src/prim/CryptoBox.saw directory and saw CryptoBox.saw.

[robdockins]

This is probably an abcBridge bug. I'll look into it.

[robdockins]

Contrary to expectation, this is not an abcBridge bug. Instead, it seems to be a bug with the translation of the Cryptol expression [0..]. The following is a minimal reproducible example. Changing [0..] into something with an upper bound (e.g. [0..1]) causes the error to disappear.

let {{
  type Key      = [256/8][8]
  type Nonce    = [192/8][8]
  type Counter  = [64]

  my_XSalsa20 : {r} (8 >= width r) => Key -> Nonce -> Counter -> [64][8]
  my_XSalsa20 key0 nonce0 ctr = zero

  my_XSalsa20_expansion : {r} (8 >= width r) => Key -> Nonce -> [1][8]
  my_XSalsa20_expansion k n = take (join ks)
    where
     ks = [my_XSalsa20 `{r=r} k n i | i <- [0..] ]
}};

let main : TopLevel () = do {
    let asdf = {{ \k n -> my_XSalsa20_expansion `{r=20} k n }};
    print {{ asdf (split zero) (split zero) }};
};

[brianhuffman]

Here is an even more minimal example:

let {{
  foo : [1][8]
  foo = take [ zero | (i:[64]) <- [0..] ]
}};
print {{ foo }};

What's happening here is that the subexpression [0..] is a vector with 2^64 elements. Some places in SAWScript use the Haskell type Int to represent vector lengths, so when the vector [0..] is created, its length wraps around to 0. When take tries to select the first element from the 0-length vector, the out-of-bounds error occurs.

As a workaround, you can use [0...] (of type [inf][8]) instead of [0..] (of type [2^^64][8]) in the Cryptol source.

We can certainly switch from Int to Integer for representing vector lengths, but this would only reveal another problem: SAW uses an array-like type (Data.Vector) to represent finite vector values, and so evaluating [0..] would quickly run out of memory even if we don't force evaluation of the elements. (You can see this for yourself by changing 64 to 60 in the example above.)

[robdockins]

After a few additional tweaks to saw-core and cryptol-verifier, I can now confirm that altering the XSalsa20_expansion function to use [0...] instead of [0..] allows the original proof to go through.

Let's leave this bug open for now to track the continuing work that needs to happen to support the [0..] form for large bitwidths.

[atomb]

A nice compromise would be to use different data structures for different sizes of vectors. We could use array-like structures for small vectors, and list-like (or even map-like) structures for large vectors.

[robdockins]

We deleted the [x..] form, so no additional work needs to be done to support it.