In terms about reasoning about a system, having a set of invariants that we can speak out about reason about correctness of higher level behaviors from is very valuable. 

I think we should try (maybe by M68) to introduce the invariant that a surface of a given surface ID can only be created once and destroyed once.

This is not currently the case which makes reasoning about surfaces fairly difficult. I think we should try to get to this point next.
 

Having a set of invariants for surfaces allows us to reason about the correctness of higher level behaviors such as surface synchronization and frame eviction.

I think we should try (maybe by M68) to introduce the invariant that a surface of a given surface ID can only be created once and destroyed once.

This is not currently the case which makes reasoning about surfaces fairly difficult. I think we should try to get to this point next.