Hm, I think you are using the term "total function" for what I would call a "pure function". Wikipedia lists "the function has no side effects" as requirement for a pure function, and in PL theory, both throwing an exception and looping indefinitely are typically considered side-effects (precisely because they break equational reasoning of the form my example is based on).
But maybe there's so few functions that are fully pure that it's not worth having an annotation for that.