:check crash on negative Integer index

[WeeknightMVP]

module S where

atXis0:
    {n, a, w}
    (fin n, Eq a, Zero a, Cmp w, Integral w, Literal n w) =>
    [n]a -> w -> Bit
property atXis0 seq i =
    zero == seq ==> i < `n ==> seq @ i == zero

Cryptol> :m S
Loading module Cryptol
Loading module S
S> :check atXis0`{4, Bit, Integer}
Using random testing.
Passed 100 tests.
S> :check atXis0`{4, Char, Integer}
Using random testing.
Testing...   3%cryptol: index out of bounds in call to: Data.Sequence.index -1580408924
CallStack (from HasCallStack):
  error, called at libraries/containers/containers/src/Data/Sequence/Internal.hs:2056:7 in containers-0.6.2.1:Data.Sequence.Internal

The problem appears to be an uncaught exception triggered when :check considers a negative Integer as the index for @. This appears not to be triggered when a is Bit or satisfies Zero a and seq is zero:

Cryptol> :m S
Loading module Cryptol
Loading module S
S> let at0is0 = atXis0`{8, Char, Integer} (zero:[8]Char)
S> :check at0is0
Using random testing.
Passed 100 tests.
S> let atBitsIs0 = atXis0`{8, Bit, Integer}
S> :check atBitsIs0 
Using random testing.
Passed 100 tests.

[brianhuffman]

The immediate source of the error is the call to Seq.index in the definition of function randomSequence:

cryptol/src/Cryptol/Testing/Random.hs

Lines 246 to 252 in 3bec6cd

	randomSequence :: (Backend sym, RandomGen g) => Integer -> Gen g sym -> Gen g sym
	randomSequence w mkElem sz g0 = do
	let (g1,g2) = split g0
	let f g = let (x,g') = mkElem sz g
	in seq x (Just (x, g'))
	let xs = Seq.fromList $ genericTake w $ unfoldr f g1
	seq xs (pure $ VSeq w $ IndexSeqMap $ (Seq.index xs . fromInteger), g2)

I'm not sure what invariant we're trying to maintain on IndexSeqMap: Either it's the responsibility of the function inside to check for negative indices, or else it's the responsibility of anything that consumes a SeqMap to avoid calling the function with negative indices. The proper fix will be depend on which invariant we choose. We should document that choice, in either case.

Alternatively, we could avoid the question by indexing SeqMaps with type Natural instead of Integer. (Although we may still have the same problem with out-of-bounds indices, so maybe this wouldn't buy us much.)

@robdockins, thoughts?

[brianhuffman]

I should also point out that this is an unsafe use of fromInteger (#637). Even if we knew that the SeqMap was only called with positive index arguments, the fromInteger could still wrap around to produce negative Int arguments to Seq.index. We need to be careful here.

[robdockins]

I've been operating under the invariant that consumers of SeqMap are required to only use in-bounds indices. The bounds are almost always bundled together with the SeqMap, as with the VSeq constructor. In this case, I believe the bug is with whatever use site this random sequence flows into.

We could use Natural instead of Integer, but the fundamental problem remains, and I think the failure condition when doing arithmetic on Natural is worse (you get a very generic error message from the - operation or somesuch).

[robdockins]

I suspect that the indexing primitive @ is checking that the integer value is less than the upper bound, but isn't checking that it is nonnegative; that check wasn't required when only bitvectors were used as indices.

[robdockins]

Indeed, it seems that this test is incomplete:

cryptol/src/Cryptol/Eval/Generic.hs

Line 1423 in 3bec6cd

= unless (i < n) (raiseError sym (InvalidIndex (Just i)))

Several of these cases look like they also need to handle the possibility that an integer index could be negative.