Benefits of Proving Index Access is Valid

Stream: general

[Asei Inoue]

What are the benefits of proving that an index access is valid? I’d like to know what potential advantages there are.

In my view, for example,

• using get! instead of get requires an additional Inhabited instance. So if we prove that the index access is valid, we don’t need an Inhabited instance—this is one benefit.
• Also, calling panic! might cause a default value to be used, which could in turn require extra assumptions or unnecessary case splits during proofs.

What other benefits can you think of? I'd appreciate it if you could also provide code examples.

[Jason Rute]

Is this for programming or math?

[Jason Rute]

There are also four options: get, get!, get?, getD. All have their own advantages.

[Jason Rute]

Also another disadvantage of get! (or really []!) is that in some cases it doesn’t panic, like in #eval.

[Jason Rute]

Oh, it looks like that has been fixed. But still the panic may be hard to notice. I just checked it and missed it myself!

[Asei Inoue]

Is this for programming or math?

Both!

[Kim Morrison]

No runtime bounds checks.

[Markus Himmel]

Another benefit is that the lemmas for get/getElem are often simpler and there might be more simp lemmas available. Compare for example Std.HashMap.getElem!_erase and docs#Std.HashMap.getElem_erase.

[Asei Inoue]

I gave it a try. Indeed, it seems that proving its validity makes it run faster.

variable {α : Type} [Add α] [Zero α] [Inhabited α]

@[noinline]
def sum! (xs : Array α) : α := Id.run do
  let mut acc : α := 0
  for i in [0:xs.size] do
    acc := acc + xs[i]!
  return acc

@[noinline]
def sum (xs : Array α) : α := Id.run do
  let mut acc : α := 0
  for h : i in [0:xs.size] do
    acc := acc + xs[i]
  return acc

@[noinline]
def main : IO Unit := do
  let size := 10_000_000
  let array := Array.range size

  let start_time1 ← IO.monoNanosNow
  let result1 := sum! array
  let end_time1 ← IO.monoNanosNow
  let time1 := end_time1 - start_time1
  IO.println s!"sum! result: {result1}, time taken: {time1} ns"

  let start_time2 ← IO.monoNanosNow
  let result2 := sum array
  let end_time2 ← IO.monoNanosNow
  let time2 := end_time2 - start_time2
  IO.println s!"sum result: {result2}, time taken: {time2} ns"

  if time1 < time2 then
    throw <| .userError s!"sum! is faster: {time1} ns < {time2} ns"

#eval main

[Robin Arnez]

Asei Inoue schrieb:

I gave it a try. Indeed, it seems that proving its validity makes it run faster.

That's not a good test, it won't actually execute sum! between the two IO.monoNanosNow, you need to wrap it in IO:

variable {α : Type} [Add α] [Zero α] [Inhabited α]

@[noinline]
def sum! (xs : Array α) : IO α := pure <| Id.run do
  let mut acc : α := 0
  for i in [0:xs.size] do
    acc := acc + xs[i]!
  return acc

@[noinline]
def sum (xs : Array α) : IO α := pure <| Id.run do
  let mut acc : α := 0
  for h : i in [0:xs.size] do
    acc := acc + xs[i]
  return acc

def main : IO Unit := do
  let size := 10_000_000
  let array := Array.range size

  let start_time1 ← IO.monoNanosNow
  let result1 ← sum! array
  let end_time1 ← IO.monoNanosNow
  let time1 := end_time1 - start_time1
  IO.println s!"sum! result: {result1}, time taken: {time1} ns"

  let start_time2 ← IO.monoNanosNow
  let result2 ← sum array
  let end_time2 ← IO.monoNanosNow
  let time2 := end_time2 - start_time2
  IO.println s!"sum result: {result2}, time taken: {time2} ns"

  if time1 < time2 then
    throw <| .userError s!"sum! is faster: {time1} ns < {time2} ns"

[Robin Arnez]

Interestingly enough, sum! seems to be faster when interpreted but slower when compiled (in comparison to sum)

[Asei Inoue]

Thanks!!!
why sum! is not executed in my version?

[Robin Arnez]

It is! But because it is a pure computation the compiler just put the sum! computation after the end_time1 and the sum computation after end_time2