cmd/compile: add reverse proof to prove pass?

[JAicewizard]

What version of Go are you using (go version)?

$ go version
1.17.1

Does this issue reproduce with the latest release?

yes

I dont know if there are propper terms for these. I call the current way the prove pass works forwards, as it proves from what it knows, whereas I call what I propose backwards because it goes the opposite way. (trying to find out what knowlege is needed to prove the branch).

While seeing what happens in some cases I recently reported, I found that essentially that trying to improve the ft.update function might be a simple solution for proving things, but its also one-way. It tries to proof things from what it already knows. However in some cases it is actually almost trivial to do this in reverse. Look at what condition you're branching on, and then see what you need to prove this.

Adding more of the forward rules will grow exponentially, because each rule will trigger another etc. Adding a backwards rule would only grow the complexity linearly. Of course its affect is also smaller, but adding forward rules will eventually hit diminishing returns as maybe only 1% of the rules applied actually end up being useful.

[JAicewizard]

see https://github.com/JAicewizard/go/tree/add_backwards_checks_ssa for my current implementation. Along with the backwards rules, I also added some other improvements to make sure my own issue is fixed.
One thing to note that I initially forgot, is that these are specific cases, not general rules. like "if this value was negated, and before that it was incremented and is was smaller than 0 then we know it is now bigger than or equal to 0", more like rewrite rules.

[randall77]

It's an interesting idea. The prove pass certainly proves a lot of things to itself that it doesn't end up using.

The prove pass is currently very delicate, error-prone code. I think at this point I'm much more concerned about the complexity of the code itself than the amount of work it does at compile time. So I think I'm not that excited about making the prove pass more efficient. If this rework makes it more obviously correct, that would make me excited.

[JAicewizard]

My code doesnt really touch the existing code in the prove pass. What I have right now is sort of like a pattern matching function that tries to match a pattern of values, sees if it the required facts are known, and if so adds a conclusion fact. I think it makes most sense for complex logic that the prove pass would never be able to prove due to the nature of information it stores. eg: it only stores the range a value can be in as a min/max, but what if we know if its between -x and MinInt-x? this doesn't get stored at all, and doing so would make the code even more complex.

Assuming this pattern matching function is correct, the tricky part would be getting correct patterns and facts, not the code itself.

We could also make something like how the current update function works, but this would be just as complex as update and wouldn't be able to prove something like the example above (although it would certainly be interesting! ).