An array load is either:

- guarded by a range check

- proven in bound at compile time (in which case its range constant fold)

- pinned

I propose adding verification logic for that.