cryptol: Prelude.(!!): negative index

[jpziegler]

I was playing around in Cryptol with a toy problem (digits of pi) and received the following error, crashing everything and dumping me out of the repl. My Cryptol version is 2.0.0 (86b2a80).

Main> ((pi`{a=4} 0) && 0xffff0000000000) == 0x243f0000000000
cryptol: Prelude.(!!): negative index

Here's the code I was running:

type D = 14
M = `(16^^D):[D*8]
SHIFT = `(4 * D):[D*8]
MASK = M - 1

S j n = lsum+rsum
  where
    lsums = [ (s + ((modexp 16 (n-k) r)<<SHIFT)/r) && MASK where r = 8*k+j
            | k <- [0...] | s <- [0]#lsums ]
    lsum = lsums@n
    rsums = [ t + xp/(8*(n+k)+j) where xp = M >> (4*k)
            | k <- [1...] | t <- [0]#rsums ]
    rsum = rsums@(max n 12)

modexp a n m =
  if n == 0 then 1
  else if n % 2 == 0 then modexp ((a * a) % m) (n / 2) m
  else (a * modexp ((a * a) % m) (n / 2) m) % m

pi : {a} (112 - a >= 1, 112 >= a) => [112 - a] -> [D*4]
pi n = reverse(take`{D*4}(reverse((4*(S 1 n') - 2*(S 4 n') - (S 5 n') - (S 6 n'\
)) && MASK where n' = 0#n-1)))

[TomMD]

I can reproduce this on a fresh build of cryptol from master, thanks for the report!

[TomMD]

A simpler version strongly implies that the implementation of @ is a Haskell (list !!) . fromIntegral:

Main> [1..(2^^128)] @ (~zero : [64])
Assuming a = 129
cryptol: Prelude.(!!): negative index

[TomMD]

I pushed a quick fix but the issue also raises the question of how much sanity checking Cryptol should do for the user. @kiniry @dylanmc Is it Cryptol's job to tell the user when they are being absurd by doing something that, while sematically meaningful, will not terminate or is likely to take a long time (such as this case, iterating through 2^64 or even more elements in a list)?

[weaversa]

Though, the real culprit is 1-based indexing.

n' = 0#n-1

[jpziegler]

Yeah... not my prettiest code. It's a work in progress! ;)