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

1. basics

2. borrows

3. rvec-api

4. vectors

---

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/