[llvm] [RFC][Uniformity] add proof section uniformity is safe to use across transforms (PR #170628)

[Nicolai Hähnle via llvm-commits]

================
@@ -713,3 +713,310 @@ relation over dynamic instances and a :ref:`controlled m-converged
 <controlled_m_converged>` property of static instances. The :ref:`uniformity
 analysis <uniformity-analysis>` implemented in LLVM includes this for targets
 that support convergence control tokens.
+
+Preservation of Uniformity at Use
+=================================
+
+Introduction
+------------
+
+In execution of a program, the outputs produced by two converged dynamic
+instances of a static instance are *uniform* if they compare equal; 
+otherwise, *divergent*. In any given program, uniformity is determined 
+through static analysis, which depends on the current state of the program’s 
+control flow. During execution, a transformation may alter the original 
+structure of the program, potentially leading to a change in control flow.
----------------
nhaehnle wrote:

This paragraph uses terms rather strangely to my ears.

"execution" to me means program executing, which happens long after compilation. No transformations run during execution.

Also, the static analysis is a conservative approximation of the actual uniformity at runtime. This is why we sometimes use terms like "dynamically uniform" to clarify.

https://github.com/llvm/llvm-project/pull/170628