[DA] Conditions of Correctness

[amehsan]

The purpose of this issue is to document proofs of correctness for tests in dependence analysis. The goal is to make assumptions required for correctness explicit. Given the complexity of this analysis, I believe this will be useful. Eventually, when the proofs are written clearly and concisely and if there is no objection to them, they can become comments in the code.

I don't expect separate proofs for different tests. I expect proofs can be generalized. Also I will try to cover current implementation and potential extensions that we may need in the future to increase accuracy of the analysis.

I will update the issue gradually and I expect it to take a few weeks until completion.

[amehsan]

Motivation

There are two motivations for this:

Over the last couple of months I have spent significant amount of time discussing the issue of whether DA needs to check loop guard of a loop or not. I suspect this kind of concern will exist in the future specially when we a bug in DA is found and people may be tempted to go to incorrect directions. So I believe it is important for us to document proofs of correctness to avoid such mistakes.

In the existing DA, to ensure correctness, we need to ensure some conditions are met (e.g. no wrapping in subscript calculation). But there are realistic cases in which these conditions are not satisified. During the discussions above, I realized there are also alternative sets of conditions that may help us establish correctness of DA, when current conditions are not satisfied. There is no need to implement this at this point. But since this may be useful for future, I thought to write it down along with the proofs of corretness for future reference.