# State of `polonius.next`

## `domenicquirl:subset-paths`
* **Experiment!**
* Tries to solve the issue of telling apart subset relationships that may occur on different paths, but not at the same time _without liveness_
* e.g. `if` branching
* Does so by tracking the "derivation path" of subset facts, that is, the chain of basic blocks back to where they were introduced in the CFG
* Transitive closure is only computed between paths that are prefixes of each other, so no closure for branching paths

## `domenicquirl:purely-forward-liveness`
* Tries to solve the same issue _with liveness_, but _without_ backwards propagation
* Does so by tracking which origins need to be still live where a fact was introduced for that fact to hold
* e.g. a new subset relationship between two origins only holds if both origins are live (same rule as for subset propagation on `main`)
* Then records (relevant) origins that are accessed and "materializes" the correct "proven" fact if all required origins are seen to be live
* prove has to happen for every CFG edge
* Uses DDLog to be able to use set types
* Matches `main` test output

## `main`
* We have a Rust parser and fact generator now!
* Passes all tests
* Uses backwards propagation of liveness

### TODOs for fact generation (as of #4, #10, #17)
* invalidation of mutable borrows through shared ones?
* invalidation of copies vs. moves (#10, Draft, Dylan)
* models invalidation, but not yet integrated into fact generation. Also has some FIXMEs
* derefs only matter for shallow accesses, which don't yet exist in the code
* handling of fields and projections (see also TODOs)
* subset relations stemming from lifetimes in signatures of called functions
* unrolling rules (though do we need that?)
* migrating tests
* FIXMEs in manual tests plus some additional clears/invalidations are PR'd in #20

## `reintroduce-leases` (#15)
* reintroduces an explicit distinction between type origins (in the type of viariables) and loan origins (borrows `&'L_x x`)
* the latter are now called "leases"
* Motivation: loan origins had to be treated differently in multiple places already, but were confounded with type origins [see also [these Zulip comments by Niko](https://rust-lang.zulipchat.com/#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Reintroducing.20loans/near/260133407)]
* loan origins had to always be live, even though they are never accessed (because they cannot be directly referenced)
* creating a borrow `&'L_x x` required emitting a `clear_origin('L_x)` fact to counteract the invalidation of the origin through the initial creation of `x = 3`
* moves us ever closer to "old" `polonius` ruleset
* passes tests, but with changed input facts

# Summary of `polonius.next` vs. `polonius` rules
Including leases (#15), courtesy of Dylan ([on Zulip](https://rust-lang.zulipchat.com/#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Reintroducing.20loans/near/260324772))
* `access_origin` <= `var_accessed_at`, new rules consider each origin separately instead of all origins in type of var
* `clear_origin` <= `var_defined_at`, as above though probably these fall together quite often?
* `clear_lease` == `kill_loan`
* `member_on_{entry,exit}` == `origin_contains_loan_at`/`requires`
* In general: `_on_{entry,exit}` modelled as rules/facts instead of CFG split (we were overall positive about this wrt. understandability / not solving this "outside" Polonius (like in fact gen))
* `invalidate_origin` is propagated as `origin_invalidated` until accessed in `.next`, whereas `polonius` only has the former
* this is probably unnecessary for computing the correct result - we know from liveness whether the invalidated origin will be accessed again later
* _But_ it maps 1:1 to the error message of "thing that is borrowed at point A is invalidated here at point B, but is used again later at point C"
* _But but_ it produces a lot of facts because it has to propagate forward across the entire CFG
* see also [me on Zulip](https://rust-lang.zulipchat.com/#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Reintroducing.20loans/near/259696140)

# Further PRs

## `ecstatic-morse:origin-bounds` (#11)
* parser support for `fn foo<'a, 'b: 'a>()` outlives constraints in generic origins
* probably straightforward

## `Moxinilian:tldr` (#21)
* adds README / developer docs with a description of the rules
* needs review
* also how does this relate to the book / `polonius`?

# Action Items
* Cleanup / clippy pass
* Use fact generator in tests?
* Do we actually need to unroll more than once?
* Merge #11
* Review #20
* Review #21
* Follow up #11 with actually adding rules for placeholder origins
* Maybe remove `origin_invalidated`?