Array.foldl bug (can prove False with native_decide)

Stream: general

[cmlsharp]

theorem Array.foldl_broken : False := by
  let x := #[1,2,3].foldl (. + .) 0 (stop := 5)
  have : x = 6 := by rfl
  have : x = 0 := by native_decide
  contradiction

playground

Array.foldlMUnsafe and Array.foldlM (the latter of which is @[implemented_by]the former) are not equivalent functions. When stop is larger than the length of the array, the functions behave differently (the reference implementation handles stop > as.size by clamping stop, while foldMUnsafe returns init).

foldr does not seem to suffer from this issue (both implementations seem to choose the clamping behavior). Is clamping the intended behavior? I can submit a PR if so.

(as a side note, I wonder if it might be worth having theorems that prove that the unsafe Array functions are equivalent to their public definitions, given that \forall array, array.size < USize.size. the documentation guarantees this is true but it is unprovable. You could prove that this hypothesis implies the functions are equivalent though)

[cmlsharp]

(nvm wrong)

[cmlsharp]

GitHub issue

https://github.com/leanprover/lean4/issues/11773

[Eric Wieser]

I took the liberty of renaming this thread, to avoid it drawing more attention than necessary; native_decide is well-known to have soundness bugs, but it is still very valuable to report them each time you find them in Lean and Mathlib!

[cmlsharp]

Gotcha, appreciate it!

[cmlsharp]

I'll rename the Github issue as well

[Henrik Böving]

Fix at #11774

[Bhavik Mehta]

(lean4#11774)

[cmlsharp]

@Henrik Böving thanks! From reading the PR it seems like the “return init” behavior was selected, is this correct?

If so I think there’s a divergence between Array.foldl and Array.foldr. Maybe it’s not worth fixing, but it’s at least a bit odd.

When start > arr.size, I believe foldr clamps (no longer at my laptop so I can’t test)

[Henrik Böving]

I think this is worth discussing in an RFC, would you like to figure out what other languages do and write up a change proposal?

[Bhavik Mehta]

Note that docs#Array.foldlM_start_stop is already a specification for how Array.foldl should behave when stop is not its default value, and docs#Array.extract has lemmas for this case.

[cmlsharp]

Sure I can do that. Off the top of my head, I’m not aware of any languages that have fold itself take these parameters (usually you’d create a slice of the array which is where the validation would occur and then fold over that, whereas in Lean Subarray.fold is implemented in terms of the more general Array.fold with start/stop indices) but that might be my own ignorance talking. I’ll dig a bit to see if there’s other precedent for defining fold this way.

[cmlsharp]

Out of curiosity do you know why Lean chose to do things this way?

E.g. why not make “mapping/folding over a subarray” just be accomplished by creating a Subarray and then calling map/ fold. Then you never have to deal with what a sensible return value is if you get bad start/stop indices (or rather you deal with it exactly once when defining the semantics of slicing)

[Henrik Böving]

cmlsharp said:

Out of curiosity do you know why Lean chose to do things this way?

E.g. why not make “mapping/folding over a subarray” just be accomplished by creating a Subarray and then calling map/ fold. Then you never have to deal with what a sensible return value is if you get bad start/stop indices (or rather you deal with it exactly once when defining the semantics of slicing)

Creating a subarray currently allocates a subarray structure unless you have enough inlining and worker/wrapper style functions available to make the compiler optimize it away again. Though I'm inclined to believe it was simply done because it's possible back in the day.

[cmlsharp]

I’m surprised that creating a Subarray allocates. (I assume you mean it allocates a boxed structure that contains e.g. the pointer and length effectively?). is there somewhere I can read more about this?

[cmlsharp]

In particular I’m interested by your “enough worker/wrapper functions” comment.

[Henrik Böving]

(I assume you mean it allocates a boxed structure that contains e.g. the pointer and length effectively?)
Yes, Lean does nto currently have stack allocated structures, it will in the future.

cmlsharp said:

In particular I’m interested by your “enough worker/wrapper functions” comment.

Well if you write Subarray.foldl to be effectively Array.foldl subarray.arr subarray.start subarray.stop and inline that the compiler is smart enough to eliminate the subarray allocation because it is evidently not necessary.

[cmlsharp]

Ah I see. From a pure interface perspective what makes the most sense to me is for Array.foldl to not take start/stop indices but rather to actually be a wrapper around Subarray.foldl (or some common helper function which is where the real logic lives). That way you fully separate slice index validation from fold/map/etc and you don’t have to manually duplicate the same handling across all those functions. But the fact that the definitions of these functions are part of their public interface (and the allocation issue) makes this is challenging, perhaps untenable.

If foldl/foldr/map/etc really do need to be parameterized by an index, then I think the behavior that’s most consistent with subslice construction behavior in non-dependent typed languages while retaining totality is to clamp the stop index if it is too large. In my brief survey, the most common behaviors are either to throw an exception/panic (Rust, Haskell, OCaml, Go, etc) or clamp (Scala, F#, Python, JavaScript, Ruby, Elixir). I wasn’t able to find any languages that do Array.foldl’s now consistent behavior of treating an in-bounds start and out of bounds end as an empty array.

Another option of course would be to force you to provide proofs that start <= end <= array.size but that might be unwieldy.

[GasStationManager]

Claude code actually found an issue with the fixed version:
https://github.com/leanprover/lean4/issues/11778
Basically, when start >= size and start < stop, this causes a seg fault

[cmlsharp]

Great catch. This really makes me think it would be nice to have theorems which prove “arr.size < Usize.size => arr.foldlM = arr.foldlMUnsafe”.