Decode.Reverse seems to have a loop where one isn't needed. For the loop that I changed, there is at most one iteration (the original value of i is 0 and the original value of j is at most 2; after one iteration, the loop condition will always be broken). Besides being harder to read, it is also harder to reason about and this complicates our proofs and maintenance in the VerifiedSCION project.
To preserve the behaviour that stores on slices and arrays are only performed when s.NumINF is at least 2, I added an if statement. If you prefer, we can drop that as well.
matzf
commented
6 months ago 
Decode.Reverseseems to have a loop where one isn't needed. For the loop that I changed, there is at most one iteration (the original value ofiis 0 and the original value ofjis at most 2; after one iteration, the loop condition will always be broken). Besides being harder to read, it is also harder to reason about and this complicates our proofs and maintenance in the VerifiedSCION project.To preserve the behaviour that stores on slices and arrays are only performed when
s.NumINFis at least 2, I added an if statement. If you prefer, we can drop that as well.