---
# System prepended metadata

title: Polonius 2022-11-02 Hackathon Master Document

---

# Polonius 2022-11-02 Hackathon Master Document

## Agenda

* Introductions
* Review and discuss goals
    * including those that are publishable work for Amanda
* Review the polonius.next rules
    * compare with the original rules
    * (also: the claim that they are not equivalent and polonius.next's `clear_origin` would allow patterns that regular polonius wouldn't)
* Possible reports:
    * Experience and insights from integration with a-mir-formality (nikomatsakis)

## Links

* https://github.com/nikomatsakis/polonius.next/
* borrowck in a-mir-formality
    *  https://github.com/nikomatsakis/a-mir-formality/pull/110 and https://github.com/nikomatsakis/a-mir-formality/pull/111
    *  more polonius-like https://github.com/nikomatsakis/a-mir-formality/pull/113

## Goals for the day

* Breakdown of tasks, clarity around who would do what
* Plans for next hackathon

## architectural design

```mermaid
flowchart TD
    MirConstruction --produces --> DefaultMir
    DefaultMir -- read by --> InitializationAnalysis
    DefaultMir[(Default MIR)]
    InitializationAnalysis -- produces --> DropElaboratedMir
    DropElaboratedMir[(Drop-elaborated MIR)]
    
    DropElaboratedMir -- read by --> MirTypeChecker
    MirTypeChecker -- produces --> TypeCheckConstraints
    
    TypeCheckConstraints[(Type-check constraints)]
    
    
    TypeCheckConstraints -- read by --> LoanAnalysis
    DropElaboratedMir -- read by --> LoanAnalysis
    TypeCheckConstraints -- read by --> SubsetAnalysis
    DropElaboratedMir -- read by --> SubsetAnalysis
    
    subgraph Polonius
        LoanAnalysis
        SubsetAnalysis
    end    
```

## task listing

```mermaid
flowchart TD
    drop_if_refactoring["
        drop-if-refactoring: use `DROP_IF` in
        representation of Drop-Elaborated MIR
    "]
    class drop_if_refactoring nice_to_have;

    shallow_subtyping["
        shallow-subtyping: resolve higher-ranked
        outlives constraints in trait solver
    "]
    class shallow_subtyping active_development;

    extract_mir_to_library["
        extract-mir-to-library: represent MIR
        as a separate library
    "]
    class extract_mir_to_library nice_to_have;

    loan_analysis_rules["
        loan-analysis-rules: draft polonius.next and polonius 
        into rules for loan-analysis, specify fact generation
    "]
    class loan_analysis_rules active_development;

    loan_analysis_code_complete["
        loan-analysis-code-complete: implement 
        loan analysis in rustc
    "]
    class loan_analysis_code_complete blocking;

    loan_analysis_passing_test_suite["
        loan-analysis-passing-test-suite: go through every regression
        and fix the problems, address issues found by user testing
    "]
    class loan_analysis_passing_test_suite blocking;

    loan_analysis_in_mir_formality["
        loan-analysis-in-mir-formality: model loan-analysis
        rules in mir-formality
    "]
    class loan_analysis_in_mir_formality blocking;

    polonius_fuzzer["
        polonius-fuzzer: generate programs and check if polonius
        diverges from compiler
    "]
    class polonius_fuzzer nice_to_have;
    
    ship_polonius_crate["
       ship-polonius-crate: polonius ships as an independent thing
       that can be used outside of rustc, from crates.io
    "]
    class ship_polonius_crate blocking;
    
    drop_if_refactoring -..-> loan_analysis_code_complete
    
    loan_analysis_rules --> loan_analysis_code_complete
    
    loan_analysis_rules --> loan_analysis_in_mir_formality
    
    loan_analysis_in_mir_formality --> polonius_fuzzer
    
    loan_analysis_code_complete --> loan_analysis_passing_test_suite
    
    shallow_subtyping --> loan_analysis_passing_test_suite
    
    loan_analysis_code_complete --> polonius_fuzzer
    
    polonius_fuzzer -..-> loan_analysis_passing_test_suite
    
    loan_analysis_passing_test_suite --> ship_polonius_crate
    extract_mir_to_library --> ship_polonius_crate
    
    classDef nice_to_have fill:#7FDBFF,color:black
    classDef blocking fill:#0074D9,color:white
    classDef active_development fill:#B10DC9,color:white
```

<span style="background: #7FDBFF; padding: 2px 5px; border-radius: 3px">Cyan things</span> are "nice to have"

<span style="background: #0074D9; color: white; padding: 2px 5px; border-radius: 3px">Blue things</span> are "blocking a stable polonius"

<span style="background: #B10DC9; color: white; padding: 2px 5px; border-radius: 3px">Purple things</span> are "under active development"

### examples

```rust
fn foo<'a>(x: &'a u32)
where
    for<'b> 'a: 'b, // effectively the same as `'a: 'static`
{
    /* */
}

fn main() {
    let mut x = 22;
    let p: &i32 = &x;
    foo(p);
    x += 1; // error
}
```

in the compiler today.

Produce MIR for `main`

```
main() {
    let x: i32;
    let p: &'0 i32;
    
    BB0 {
        p = &'1 x;          // &'1 i32 <: &'0 i32 ===> '1: '0
        foo(p) returns BB1; // for<'b> '0: 'b ===>
            // adds a constraint `for<'b> '0: 'b` to the borrow checker
    }
    
    BB1 {
        x += 1;
        StorageDead(x);
    }
}
```

* Today, the output from MIR type checking are constraints like:
    * `for<'v...> 'r0: 'r1`
* Borrow check to take those as input and figure out what they mean
    * it figures out that this means `'0: 'static`
    * `'0` includes all points in the CFG
    * `'1` outlives `'0` -- so it too includes all points in the CFG
    * reports an error at `x += 1` is inside `'1`

How nikomatsakis expects it to work when we're done:

* MIR type checker (or trait solver) deals with higher-ranked stuff and only emits constraints of the form
    * `r0: 'r1`
* So in this example:
    * `foo(p)` would yield a constraint like `'0: 'static`
* Polonius would take that as input and, based on it, figure out that `x += 1` is an error

### examples

```rust
fn foo<'a>(x: &'a u32)
where
    for<'b> if ('a: 'b) 'a: 'b, // gets derived by 
    for<'b> fn(&'b &'a u32) : Ord, // proving that `fn` is well-formed here
{
    /* */
}

fn main() {
    let mut x = 22;
    let p: &i32 = &x;
    foo(p);
    x += 1; // error
}
```

### reviewing the rules

https://github.com/nikomatsakis/polonius.next/blob/main/src/polonius.dl

https://hackmd.io/CGMNjt1hR_qYtsR9hgdGmw

### polonius.next

```rust
let mut x = 1;
let p = &x; // p: &{O0} i32, O0 includes x
x += 1; // invalid = {x}
drop(p); // error: use of reference with invalidated origin (`x`)
```

* compute live variables at each point
* for each origin that appears in their type, call that origin live at that point
* for each `&'0 x` expression in the MIR, create a loan L0
    * and require that `'0` includes `{L0}`
    * propagate these using dataflow
* gives rise to, each point:
    * origin includes some set of loans L...
    * set set of origins O... are live
    * if a live origin O includes a loan L, 
        * and the node takes an action that contradicts L,
        * then you have an error
* work item:
    * merge liveness into polonius.next to produce the preferred rules
    * simplify polonius to remove before/after nodes and to remove initialization, liveness computation

```rust
impl LinkedList {
    fn get_next(&mut self) -> Option<&mut Self>;
}

fn foo(tmp: &mut LinkedList) {
    loop {
        match get_next(tmp) {
            Some(p) => {
                tmp = p;
            }
            None => { }
        }
    }
}
```

* compiler can tell us the live origins at each point
* https://github.com/domenicquirl/polonius.next/blob/subset-paths/src/polonius.dl

### location insensitive variant of polonius

* loan active is a dataflow computation:
    * loans become active when they are issued (at the `&x` instruction)
    * loans are killed when the path that was borrowed is mutated
    * propagate till fixed point

```rust
fn main() {
    let mut x = 3;
    
    // L0 is not active here
    
    let p = &x; // loan L0
    
    // L0 is active here
    
    drop(p); // p goes dead here
    
    // L0 is still active here
    
    x = 5; // this mutates the path that was borrowed
    
    // loan is inactive
}
```

* every origin maps to a set of loans that you are computing
* MIR type check produces `'a: 'b` constraints
* if some point P has an action that contradicts loan L and L is active at P:
    * search each live origin O at P
    * report an error if O contains L

```
inputs:
    subset(O1, O2).
    borrow_loan(O, L).

error(P) :-
    contradicts(P, L),
    loan_active(L, P),
    live_origin(P, O),
    contains_loan(O, L).
    
contains_loan(O, L) :-
    contains_loan(O1, L),
    subset(O1, O).
    
contains_loan(O, L) :-
    borrow_loan(O, L).
```

https://github.com/rust-lang/polonius/blob/master/polonius-engine/src/output/location_insensitive.rs

purely forward propagation errors and thoughts: https://hackmd.io/KpK0ICQOQLSPxIcNIlhkJQ

## Follow-up items

* figuring out the spec (nikomatsakis driving to some extent :)
    * a-mir-formality / coordinate on types team stream?
        * implement MIR + MIR type checker (to some extent) on the riir branch of a-mir-formality https://github.com/nikomatsakis/a-mir-formality/tree/riir
        * port redex rules for NLL to that
    * update on current status of .next rules, and in-progress work        
        * to compare with regular rules
        * check the claim that they maybe are not equivalent in expressive power
        * domenicquirl to look at that first
    * simplify existing polonius rules to remove CFG points / strip down to the loan check
        * lqd to pick that up next
* prototyping an actual impl (lqd driving) 
    * factor out the universe logic to simplify higher-ranked constraints
        * theo 
    * prototype "polonius-style" checker in rustc
        * lqd could follow-up / move forward
    * assess current status of test suite
        * theo to pursue (and will look at that first)
        * what is working? what fails and why?