---
# System prepended metadata

title: State of `polonius.next`

---

# 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`?