Always good to read more about John Regehr's work! His blog's been pretty quiet for a while, but there's lots of interesting posts on compiler implementation an

Always good to read more about John Regehr's work! His blog's been pretty quiet for a while, but there's lots of interesting posts on compiler implementation and bugfinding in the archives. One thing I was confused about: "The refinement relation, then, holds when — for every possible circumstance (values of arguments, values stored in memory, etc.) in which that function could end up being called — the optimized function exhibits a subset of the behaviors of the original function." It sounds from this definition like a refinement from "add x and y, return the result" to "always return 0" would be valid, but that doesn't make much sense. Am I misunderstanding the definition?