[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.
+
+When a group of threads executes the same program in parallel, the program's 
+control flow determines which subset of threads will execute any given static 
+instance. With the change in control flow, it is possible that the new set of 
+threads reaching a static instance includes some threads that did not previously 
+execute it.
+
+Although the original set of threads continues to execute the same static 
+instance, the inclusion of these additional threads may change the 
+classification. This means that during execution, a static instance marked 
+as *uniform* by the analysis may be marked as *divergent* after a transformation
+that changes the control flow of the original program.
----------------
nhaehnle wrote:

Same issue here. The way this text talks about "execution" feels wrong.

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