[llvm] [DA] Introduce domain for monotonicity (PR #176367)

[Sjoerd Meijer via llvm-commits]

sjoerdmeijer wrote:

> In the interest of progressing, I think the emphasis on proofs does not bring us any further.

I agree. And whether it is a proof, or a refinement showing which conditions need to hold, it is really not important. To save ourselves time, I am not going to expand on it, "I agree" is enough. 

@Meinersbur : I have the same question: where does this leave us, do we need monotonicity? It is genuinely unclear to me. I don't think we have answered the question, or did we?

The strong disagreement expressed earlier to solve this in the current framework without monotonicity evolved around:

> I'm strongly disagree with this direction because:
> - This proof is tightly coupled with the implementation details. 

I am just genuinely puzzled by this. In compiler work, our daily practice is precisely to implement algorithms and "proofs"; that is our bread and butter. This work seems to fit this pattern as well: a new definition and a new abstraction is introduced, together with a corresponding implementation. The current proposal is simply to change or extend that definition, and then adjust the implementation accordingly. To me, that is entirely normal—definitions and algorithms evolve, and implementations follow. I do not see how this situation is different in the second approach, whether we call it a proof or an algorithm. I am not trying to argue against your view; I just do not understand this specific concern.

@Meinersbur : can you help? Can you explain why we need this patch?

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