[Certora Audit] G-09. Cache array length outside of loop (#896)

[Certora Audit] G-09. Cache array length outside of loop (#896) #2902