The relevant contract boundary isn't specifically at the edge of the unsafe block, it's at some other level like the public face of your ADT, inside which your

The relevant contract boundary isn't specifically at the edge of the unsafe block, it's at some other level like the public face of your ADT, inside which your unsafe and technically safe regions of code share the same set of invariants. It's immaterial whether the integer operation that results in overflow happens inside or outside what is technically the unsafe block, it should still be trapped. (Sorry about being unclear in that part of my previous comment.)