Gen.oneOf is broken in v4.17 with both a runtime error and incorrect evaluation

[johnchandlerburnham]

LSpec/LSpec/SlimCheck/Gen.lean

Line 69 in 8ff5984

xs.get! x

Array.get! in oneOf and similar functions can runtime-error

def genAlphaNum : Gen Char := do
  let n <- oneOf #[choose Nat 48 57, choose Nat 65 90, choose Nat 97 122]
  return Char.ofNat n

throws

././.lake/build/bin/Tests-Main(+0x2798a2) [0x558c06f948a2]
././.lake/build/bin/Tests-Main(+0x2798a2) [0x558c06f948a2]
Error: index out of bounds
...

at runtime when running a Slimcheck property test. Furthermore

def testGen : Gen Nat :=
  oneOf #[ pure 1, pure 2]

#eval Gen.run testGen 11 -- 0

Worse, this error is not detected by default lspecIO hooks and reports a passing test, only shows up when running:

def myConfig : SlimCheck.Configuration where
  maxSize := 100
  traceDiscarded := true
  traceSuccesses := true
  traceShrink := true
  traceShrinkCandidates := true

def dbg := do
  SlimCheck.Checkable.check (∀ x: Ix.Univ, transportUniv x) myConfig

By comparison, replacing oneOf with the following:

def frequency' (default: Gen α) (xs: List (Nat × Gen α)) : Gen α := do
  let n ← choose Nat 0 total
  pick n xs
  where
    total := List.sum (Prod.fst <$> xs)
    pick n xs := match xs with
    | [] => default
    | (k, x) :: xs => if n <= k then x else pick (n - k) xs

def frequency [Inhabited α] (xs: List (Nat × Gen α)) : Gen α :=
  frequency' xs.head!.snd xs

def testGen : Gen Nat :=
  frequency [ (100, pure 1), (100, pure 2)]

We should remove potentially unsafe operations like get! from LSpec