Regarding the wrong code, I already wrote (and you can confirm in my unrolled analysis):

> every instance of testing `k < 16` is true before we hit UB. Therefore it can be simplified to true without loss of functionality, because after we hit UB, we are allowed to do absolutely anything.

Regarding the correct code, the key insight is that when k is 16, the test `k < 16` is false, so we break out of the loop and avoid reading out of bounds. Always check bounds before indexing the array, not after!

This article is a helpful introduction: https://blog.regehr.org/archives/213

> is the compiler doing a loop unroll and study that parallels your analysis?

Yes, compilers do all sorts of crazy stuff from bounds analyses to loop induction transformations. Personally, I've seen GCC eliminate my second loop variable in an implementation of the TEA cipher because it figured out that the first variable can be derived from the second, and it adjusted the bounds.

> it also seems a bit nuts that these c guys remediated that behavior by allowing an out of bounds index access with their change

You are right, it's insane that they decided to make a special case for one piece of wrong code (SPEC), probably because it's too popular to fail. That's a social/political problem, not a technical one.