Fixed point 2.0

[nikomatsakis]

What does this PR do?

This PR refactors the judgment and fixed-point runtime options. We used to have a separate #[fixed_point] combinator for Rust functions but lately I've been moving everything instead to judgment functions which I think is better. This PR merges the fixed-point code into the judgment code and also adds memoization. We only memoize within the solving of a particular judgment to avoid interactions between tests.

How does it work, what questions do you have?

The way memoization and fixed point cycles interact is as follows: when computing a judgment J, we also compute a set of memoized judgment results MJ. This set MJ is local to the computation of J. Once we have completed all proofs of J: if J is the root judgment, we just drop the memoized results. Otherwise, we merge them into the parent. When a judgment re-executes to reach a fixed point, we discard all of its memoizations because they are no longer correct.

No real questions.

AI disclosure

• I used an AI to author the main logic of the code

[rustbot]

Thanks for contributing to formality! :)
A reviewer will take a look at your PR within a week or two. If not, come talk to us on https://rust-lang.zulipchat.com/#narrow/channel/402470-t-types.2Fformality

[tiif]

I am very interested to know how the new fixed point computation and memoization are done here, but I am still very much don't understand after reading for a bit xD It will be nice to talk about this in next office hour because I might need to ask questions continuously depends on the answer to get the full picture.

[nikomatsakis]

I am very interested to know how the new fixed point computation and memoization are done here, but I am still very much don't understand after reading for a bit xD It will be nice to talk about this in next office hour because I might need to ask questions continuously depends on the answer to get the full picture.

let's do that

[bit-aloo]

Really learnt stuff reading the code, thanks. I was also wondering whether judgment evaluation could be parallelized, for example, by evaluating independent components on separate threads and then coalescing their results

View changes since this review

[bit-aloo]

hmm... I am wondering if we really need to invalidate every completed computation here. Could some results already be final and independent of the cycle, allowing us to re evaluate only the relevant components and reuse the rest?