[Certora Audit] G-09. Cache array length outside of loop

[Certora Audit] G-09. Cache array length outside of loop #2873