The chaining function used for verification was incorrect.
It returned (_, [state.1, state.2, ..., state.(k+1), state.(k+1)]) instead of the expectable (_, [state.0, state.1, ..., state.k, state.(k+1)]).
This in turn made the restricted state condition incorrect, off by one.
Swire42
commented
6 months ago
The chaining function used for verification was incorrect. It returned
(_, [state.1, state.2, ..., state.(k+1), state.(k+1)])instead of the expectable(_, [state.0, state.1, ..., state.k, state.(k+1)]). This in turn made the restricted state condition incorrect, off by one.