Leveraging Rust Types for
Program Synthesis
Jonáš Fiala, Shachar Itzhaky, Peter Müller,
Nadia Polikarpova, Ilya Sergey
21.06.23

Program Synthesis for Rust with Guarantees
Rust type+functional spec

RusSOLcode
well-typed
correct2

This Talk

1. A taste of RusSOL
2. Synthetic Ownership Logic (SOL)
3. Evaluation3

Demosum typeenum List<T> {Nil,Cons { elem: T, next: Box<List<T>> },}generic payload

pointer with ownership

4

RusSOL Workflow
struct UserType{ … }#[requires(…)]#[ensures(…)]
fn target(x: T1,…)-> T

RusSOL
frontendsynthesisgoal{P} _ {Q}deductivesynthesis
engineproof{P} s {Q}prettyprinterfn target(x: T1,…)-> T{ s’ }#[pure]fn f(x: T1,…) -> T{ … }which program logic?
5This Talk

1. A taste of RusSOL
2. Synthetic Ownership Logic (SOL)
3. Evaluation

6

Key Properties
ownership & borrowing
Aeneas [Ho & Protzenko’22]

Synthetic Ownership Logic(SOL)
programsynthesis
SuSLik [Polikarpova & Sergey’19]#[requires(…)]#[ensures(…)]
fn target(x: T1,…)-> T#[pure]fn f(x: T1,…) -> T{ … }functional propertiesof safe Rust
Prusti [Astrauskas et al’19]
Creusot [Denis et al’21]
7

Example: Constr Rule8

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}

todo!();// {result: List}
result}9

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}

todo!();// {elem: T ∗ next: Box}let result = List::Cons{elem, next}; // Constr.Cons// {result: List}
result}10

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}

todo!();// {elem: T ∗ next: Box}let result = List::Cons{elem, next}; // Constr.Cons// {result: List}
result}11

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}
todo!();// {elem: T ∗ list: List}
let next = Box::new(list);// Constr.Box// {elem: T ∗ next: Box}let result = List::Cons{elem, next}; // Constr.Cons// {result: List}
result}12

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}
todo!();// {elem: T ∗ list: List}
let next = Box::new(list);// Constr.Box// {elem: T ∗ next: Box}let result = List::Cons{elem, next}; // Constr.Cons// {result: List}
result}13

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}
todo!();// {elem: T}
let list = List::Nil;// Constr.Nil// {elem: T ∗ list: List}
let next = Box::new(list);// Constr.Box// {elem: T ∗ next: Box}let result = List::Cons{elem, next}; // Constr.Cons// {result: List}
result}14

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}
todo!();// {elem: T}
let list = List::Nil;// Constr.Nil// {elem: T ∗ list: List}
let next = Box::new(list);// Constr.Box// {elem: T ∗ next: Box}let result = List::Cons{elem, next}; // Constr.Cons// {result: List}
result}15

Example: Singleton
fn singleton<T>(elem: T) -> List<T> {// {elem: T}
CONSTR.NIL

CONSTR.CONS// {elem: T}
let list = List::Nil;// Constr.Nil// {elem: T ∗ list: List}
let next = Box::new(list);// Constr.Box

CONSTR.BOX
CONSTR.NIL

CONSTR.CONS// {elem: T ∗ next: Box}let result = List::Cons{elem, next}; // Constr.Cons// {result: List}
result}16

This Talk

1. A taste of RusSOL
2. Synthetic Ownership Logic (SOL)
3. Evaluation17

Annotated

3 sources
Rust
SuSLikVerifiers18

Annotated117 tasks

115 solved

all correct

3 sources
Rust

5.4 LOCSuSLikVerifiers

19

Annotatedenum Tree<T> { Nil, Cons { elem: T, next: List<Tree<T>> } }enum List<T> { Nil, Cons(Box<(T, List<T>)>) }#[ensures(result.len() == tree.size())]
fn flatten<T>(tree: Tree<T>) -> List<T> {match tree {Tree::Nil => List::Nil,Tree::Cons { elem, next } => flatten_3(elem, next),}}fn flatten_3<T>(elem: T, next: List<Tree<T>>) -> List<T> {match next {List::Nil => {let bx = (elem, List::Nil);
let _0 = Box::new(bx);
List::Cons(_0)}
List::Cons(_0) => {let result = flatten(_0.0);
flatten_14(elem, _0.1, result)}}}
fn flatten_14<T>(elem: T, _1: List<Tree<T>>, result: List<T>) -> List<T> {match result {List::Nil => flatten_3(elem, _1),
List::Cons(_0) => {let result = flatten_14(_0.0, _1, _0.1);
let bx = (elem, result);
let _0 = Box::new(bx);
List::Cons(_0)}}}

2 aux fns

24 LOC

10s
20

Unannotated// either/src/lib.rs:832

no spec~3K LOC

100 mostdownloadedpackages(crates)

all solutions
well-typed

fn factor_first<T, L, R>(x: Either<(T, L), (T, R)>)-> (T, Either<L, R>) {match x {Either::Left(_0) => {let _1 = Either::Left(_0.1);(_0.0, _1)}
Either::Right(_0) => {let _1 = Either::Right(_0.1);(_0.0, _1)}}}

filter unsupported fns21

Conclusion

RusSOL
first deductive synthesis tool for Rustleverages Rust types to reduce spec overhead

Synthetic Ownership Logic (SOL)verifies well-typed programs which satisfy spec

Online demot.ly/2-8ATools -> RusSOL

leverages Rust types to prune search space
friendly to synthesis22fn push<T>(x: &mut List<T>, elem: T) {let list: List<T>= *x; // error!

std::mem::replace(x, List::Nil);
let next: Box<List<T>> = Box::new(list);
let extended: List<T>= List::Cons{elem, next};*x = extended}&mut V → Vimpossible in safe Rust#[ensures(result == *idol)]fn std::mem::replace<V>(idol: &mut V, bag: V) -> V {unsafe}

23