marp	theme	style
true	default	img[alt~="center"] { display: block; margin: 0 auto; }

`Flux`: Liquid types for Rust

Nico Lehmann, Adam Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala

Motivation

Types vs. Floyd-Hoare logic

Demonstration

Flux - Liquid Types for Rust

Evaluation

Flux v. Prusti for Memory safety

Types vs. Floyd-Hoare logic

Liquid/Refinements 101

type Nat = {v: Int | 0 <= v}

Int is the base type of the value
v names the value being described
0 <=v is a predicate constraint

Liquid/Refinements 101

Generate the sequence of values between lo and hi

range :: lo:Int -> {hi:Int | lo <= hi} -> List {v:Int|lo <= v && v < hi}

Liquid/Refinements 101

Generate the sequence of values between lo and hi

range :: lo:Int -> {hi:Int | lo <= hi} -> List {v:Int|lo <= v && v < hi}

Input Type is a Precondition

lo <= hi

Liquid/Refinements 101

Generate the sequence of values between lo and hi

range :: lo:Int -> {hi:Int | lo <= hi} -> List {v:Int|lo <= v && v < hi}

Output Type is a Postcondition

Every element in sequence is between lo and hi

Types vs. Floyd-Hoare logic

Types decompose (quantified) assertions to quantifier-free refinements

Lists in Dafny vs LiquidHaskell

Accessing the `i`-th List Element

Floyd-Hoare requires elements and quantified axioms

Liquid Parametric polymorphism yields spec for free

Building and Using Lists

Floyd-Hoare Quantified postcondition (hard to infer)

Building and Using Lists

Liquid Quantifier-free type (easy to infer)

Int -> k:Int -> List {v:Int| k <= v}

Types vs. Floyd-Hoare logic

Types decompose assertions to quantif-free refinements ...

... but what about imperative programs

Motivation

Types vs. Floyd-Hoare logic

Demonstration

Flux Liquid Types for Rust

Evaluation

Flux v. Prusti for Memory Safety

`Flux` Liquid Types for Rust

flux (/flʌks/)

n. 1 a flowing or flow. 2 a substance used to refine metals. v. 3 to melt; make fluid.

`Flux` Liquid Types for Rust

Motivation

Types vs. Floyd-Hoare logic

Demonstration

Flux Liquid Types for Rust

Evaluation

Flux v. Prusti for Memory Safety

Evaluation

Flux v. Prusti for Memory Safety

`Flux` v. `Prusti` by the numbers

`Flux` v. `Prusti` : Types Simplify Specifications

// Rust
fn store(&mut self, idx: usize, value: T)

// Flux
fn store(self: &mut RVec<T>[@n], idx: usize{idx < n}, value: T)

// Prusti
requires(index < self.len())
ensures(self.len() == old(self.len()))
ensures(forall(|i:usize| (i < self.len() && i != index) ==>
                    self.lookup(i) == old(self.lookup(i))))
ensures(self.lookup(index) == value)

Quantifiers make SMT slow!

`Flux` v. `Prusti` : Types Enable Code Reuse

Example: `kmeans.rs` in `flux`

fn kmeans(n:usize, cs: k@RVec<RVec<f32>[n]>, ps: &RVec<RVec<f32>[n]>, iters: i32) -> RVec<RVec<f32>[n]>[k] where 0 < k

Point is an n dimensional float-vec RVec<f32>[n]
Centers are a vector of k points RVec<RVec<f32>[n]>[k]

`Flux` v. `Prusti` : Types Enable Code Reuse

Example: `kmeans.rs` in `prusti`

ensures(forall(|i:usize| (i < self.len() && i != index) ==>
                    self.lookup(i) == old(self.lookup(i))))

Value equality prevents vector nesting!

Have to duplicate code in new (untrusted) wrapper library

`Flux` v. `Prusti` : Types Simplify Invariants & Inference

Dimension preservation obfuscated by `Prusti` spec

#[requires(i < self.rows() && j < self.cols())]
#[ensures(self.cols() == old(self.cols()) && self.rows() == old(self.rows()))]
pub fn set(&mut self, i: usize, j: usize, value: T) {
  self.inner[i][j] = value;
}

Hassle programmer for dimension preservation invariants

kmeans::normalize_centers in prusti vs. flux
fft::loop_a in prusti vs. flux

Burden programmer with dimension preservation invariants

fft::loop_a in prusti vs. flux

`Flux` v. `Prusti` : Types Simplify Invariants & Inference

Types decompose quantified assertions to quantifier-free refinements

flux infers quantifier-free refinements via Horn-clauses/Liquid Typing

`Flux` v. `Prusti` : Types Simplify Invariants & Inference

kmp_search in prusti vs. flux

// Prusti
body_invariant!(forall(|x: usize| x < t.len() ==> t.lookup(x) < pat_len));

// Flux
t: RVec<{v:v < pat_len}>

Types decompose quantified assertions to quantifier-free refinements

flux infers quantifier-free refinements via Horn-clauses/Liquid Typing

Types decompose quantified assertions to quantifier-free refinements

kmp_search in prusti vs. flux

Motivation

Types vs. Floyd-Hoare logic

Demonstration

Flux Liquid Types for Rust

Evaluation

Flux v. Prusti for Memory Safety

Conclusions

Refinements + Rust's Ownership = Ergonomic Imperative Verification...

Specify complex invariants by composing type constructors & QF refinements
Verify complex invariants by decomposing validity checks via syntactic subtyping

Conclusions

Refinements + Rust's Ownership = Ergonomic Imperative Verification...

Specify complex invariants by composing type constructors & QF refinements
Verify complex invariants by decomposing validity checks via syntactic subtyping

... But this is just the beginning

Flux restricts specifications, Prusti allows way more ...
... how to stretch types to "full functional correctness"?

What are interesting application domains to focus on?

`flux` https://github.com/liquid-rust/flux/