Leveraging Rust Types for Program Synthesis: AppendixJONÁŠ FIALA, Department of Computer Science, ETH Zurich, Switzerland
SHACHAR ITZHAKY, Technion, Israel
PETER MÜLLER, Department of Computer Science, ETH Zurich, Switzerland
NADIA POLIKARPOVA, University of California, San Diego, USAILYA SERGEY, National University of Singapore, Singapore
CCS Concepts: • Software and its engineering → Automatic programming.
Additional Key Words and Phrases: program synthesis, program logic, Rust, type systems
ACM Reference Format:
Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey. 2023. Leveraging Rust Typesfor Program Synthesis: Appendix. Proc. ACM Program. Lang. 7, PLDI, Article 164 (June 2023), 6 pages. https://doi.org/10.1145/3591278

ASYNTHESIS RULES

This appendix contains the full set of synthesis rules: Fig. 1 lists ownership rules, Fig. 2 lists
borrowing rules, and Fig. 3 lists structural rules.
Ownership Rules. The rules Drop, Rename, and Unreachable are straightforward: once a variable
is dropped or renamed (moved), it is no longer accessible due to ownership-types semantics. TheUnreachable rule may be encountered if a specification is inconsistent or, more importantly,
in combination with Destr when synthesizing a match expression one of whose branches is
unsatisfiable due to a contradiction with known assumptions (e.g. the Nil case when the matchedlist is known to be nonempty). This rule can only ever fire if a precondition is specified; otherwise,with no assumptions, it is impossible to deduce false.
The rules Primitive, Constr and Destr give the semantics of value construction and destructuring (pattern matching) for Rust data types, for the case where the given variable has an owned
type. The rules take care to update the snapshots accordingly; in Destr the input binding is unconstrained so that it can be applied to arbitrary arguments—by applying the rule we learn facts
about it the snapshot value. On the other hand, Primitive and Constr force a particular choice ofsnapshot on the right-hand-side since they create result objects where this value can be picked asrequired (when applied backwards).
Note that there is no construction rule for generic types T and that Constr cannot be applied toempty types (enums with no variants), since neither is constructable in Rust. While the Destr rule
still cannot be applied to generics but is equivalent to Unreachable for empty types.
Authors’ addresses: Jonáš Fiala, Department of Computer Science, ETH Zurich, Switzerland, jonas.fiala@inf.ethz.ch;
Shachar Itzhaky, Technion, Israel, shachari@cs.technion.ac.il; Peter Müller, Department of Computer Science, ETH Zurich,Switzerland, peter.mueller@inf.ethz.ch; Nadia Polikarpova, University of California, San Diego, USA, nadia.polikarpova@ucsd.edu; Ilya Sergey, National University of Singapore, Singapore, ilya@nus.edu.sg.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/6-ART164
https://doi.org/10.1145/3591278
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 164. Publication date: June 2023.

164164:2Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey

DropRename

𝑇 not ref{x : 𝑇 (𝑣)} drop!(x) {emp}
𝑇 not ref{x : 𝑇 (𝑣)} let y = x {y : 𝑇 (𝑣)}

Unreachable{false | 𝑃 } unreachable!() {Q}

Primitive
𝑇𝑎 , . . . ,𝑇𝑥 are primitive
𝑤 = 𝑣 ⊕ ...∧𝜙 |{𝜙 | a : 𝑇𝑎 (𝑣) ∗ . . .} let x = a ⊕ ...
x : 𝑇𝑥 (𝑤) ∗ a : 𝑇𝑎 (𝑣) ∗ . . .
Constr𝑇 = (𝑇0 × . . .) V0 + . . . + (𝑇𝑛 × . . .) Vn + . . .

{y : 𝑇𝑛 (𝑣) ∗ . . .} let x = Vn (y, ...) {x : 𝑇 ({𝛿 : Vn, y : 𝑣, . . .})}Destr

𝑇 = (𝑇𝑦 × . . .) V0 + (𝑇𝑧 × . . .) V1 + . . .
𝑣 = {𝛿 : V0, y : 𝑢, . . .} ∧ 𝜙 | y : 𝑇𝑦 (𝑢) ∗ . . . ∗ 𝑃 𝑐 0 {Q}{𝑣 = {𝛿 : V1, z : 𝑤, . . .} ∧ 𝜙 | z : 𝑇𝑧 (𝑤) ∗ . . . ∗ 𝑃 } 𝑐 1 {Q}{r, . . .} = returns(Q)...
{𝜙 | x : 𝑇 (𝑣) ∗ 𝑃 } let (r, ...) = match x { V0 (y, ...) => 𝑐 0, V1 (z, ...) => 𝑐 1, . . . } {Q}
Fig. 1. Ownership Rules.

Borrowing References. The borrowing rules were discussed in detail in Section 3, apart from
BorrowIn and BorrowOut. These rules are analogous to DestrBorrow and ConstrBorrow,respectively, but when the referent is itself a reference instead of a data type (that is, these rules
handle nested references).
Structural Rules. The rules Frame, Conseqence, and Seq are familiar from SL and Hoare logic.
One difference about our Frame rule is that it does not require a side condition that free variablesof 𝑅 are not modified by 𝑐, because in SOL a program variable can only appear in an assertion once.
The Call is similar to the one in SuSLik, except that it is applied backwards.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 164. Publication date: June 2023.

Leveraging Rust Types for Program Synthesis (Appendix)

164:3

DropRefWritenoˆ drop!(x) {𝑣 = 𝑥ˆ ∧ 𝜙 | emp}
𝜙 | x𝜃 ↦→ 𝑇 (𝑣, 𝑥)ReBorrow'𝑎 : '𝑏𝜇 = mut ? 𝜃 = {'𝑏} : 𝜈 = imm'𝑏ˆ ∗ y ↦−→𝜈 𝑇 (𝑣, 𝑦)'𝑎ˆ let y = &𝜈 ∗xx ↦−→𝜇 𝑇 (𝑣, 𝑥)'𝑎𝜃ˆ 𝑥)ˆ 
 x ↦−→𝜇 𝑇 (𝑦,DestrBorrow
𝑇 = (𝑇𝑦 × . . .) V0 + (𝑇𝑧 × . . .) V1 + . . .
ˆ ∗x ↦→mut 𝑇 (𝑣, 𝑥)
new : 𝑇 (𝑤)ˆ∗x = new {x ↦→mut 𝑇 (𝑤, 𝑥)}

CopyOut
𝑇 is primitiveˆ ∗x ↦→ 𝑇 (𝑣, 𝑥)
ˆ let y = ∗x{x ↦→ 𝑇 (𝑣, 𝑥)}y : 𝑇 (𝑣){r, . . .} = returns(Q){'𝑏 } '𝑎'𝑏'𝑏 is freshˆ . . .}, 𝑥)ˆ ∗ y ↦−→ 𝑇𝑦 (𝑢, 𝑦)ˆ ∗ . . . ∗ 𝑃 𝑐 0 {Q}𝑣 = {𝛿 : V0, 0 : 𝑢, . . .} ∧ 𝜙 | x↦−→ 𝑇 ({𝛿 : V0, 0 : 𝑦,
'𝑏{'𝑏 } '𝑎
ˆ . . .}, 𝑥)ˆ ∗ z ↦−→ 𝑇𝑧 (𝑤, 𝑧)ˆ ∗ . . . ∗ 𝑃 𝑐 1 {Q}𝑣 = {𝛿 : V1, 0 : 𝑤, . . .} ∧ 𝜙 | x↦−→ 𝑇 ({𝛿 : V1, 0 : 𝑧,...

V0 (y, ...) => 𝑐 0,'𝑎ˆ ∗ 𝑃 let (r, ...) = match x{Q}𝜙 | x ↦−→ 𝑇 (𝑣, 𝑥)
V1 (z, ...) => 𝑐 1, . . .

ConstrBorrow𝑇 = (𝑇0 × . . .) V0 + (𝑇1 × . . .) V1 + . . .
𝜃 = 𝛽 ∪...

no'𝑎'𝑏
ˆ . . .}, 𝑥)ˆ ∗ y𝛽 ↦−→ Tn (𝑣, 𝑦)ˆ ∗ . . . drop!(y); ... x𝜃 ↦→ 𝑇 ({𝛿 : Vn, 0 : 𝑣, . . .}, 𝑥)ˆx {'𝑏 } ↦−→ 𝑇 ({𝛿 : Vn, 0 : 𝑦,BorrowIn'𝑎ˆ 𝑥)
ˆ let y = &𝜇 ∗∗x xx ↦−→𝜇 &mut T((𝑣, 𝑎),{'𝑏 } '𝑎'𝑏ˆ 𝑎),ˆ 𝑥)ˆ ∗ y ↦−→𝜇 𝑇 (𝑣, 𝑦)ˆ↦−→𝜇 &mut T((𝑦,BorrowOut'𝑎'𝑏'𝑎ˆ 𝑎),ˆ 𝑥)ˆ ∗ y𝜃 ↦−→ 𝑇 (𝑣, 𝑦)ˆ drop!(y) x𝜃 ↦−→ &mut T((𝑣, 𝑎),ˆ 𝑥)
ˆx {'𝑏 } ↦−→ &mut T((𝑦,Fig. 2. Borrowing Rules.

Frame{𝜙 | 𝑃 } 𝑐 {𝜓 | 𝑄 }Conseqence′𝜙 ⇒ 𝜙 ′𝜓 ′ ⇒ 𝜓′
𝜙 |𝑃 𝑐 𝜓 |𝑄

{𝜙 | 𝑃 ∗ 𝑅} 𝑐 {𝜓 | 𝑄 ∗ 𝑅}

{𝜙 | 𝑃 } 𝑐 {𝜓 | 𝑄 }EmpCall𝜙 =⇒ 𝜙 ′𝜙 =⇒ 𝜓{𝜙 | emp} 𝑐 {𝜓 | emp}

Seq{𝜙 | 𝑃 } 𝑐 0 {𝜓 | 𝑄 }{𝜓 | 𝑄 } 𝑐 1 {𝜒 | 𝑅}

{𝜙 | 𝑃 } 𝑐 0 ; 𝑐 1 {𝜒 | 𝑅} ′𝜙 | a : 𝑇𝑎 (𝑣) ∗ . . . foo {𝜓 | result : 𝑇 (𝑤)}{𝜙 | a : 𝑇𝑎 (𝑣) ∗ . . . ∗ 𝑃 } 𝑐; let r = foo(a, ...) {𝜙 ∧ 𝜓 | r : 𝑇 (𝑤) ∗ 𝑃 }Fig. 3. Structural rules.

BNOTABLE SYNTHESIS RESULTS

B.1

Synthesis from Types Alone

Below is a sample of interesting examples from the “non-primitive” part of the 100-Crates test
suite; these programs are synthesized just from their type signatures.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 164. Publication date: June 2023.

164:4

Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey// h2/src/frame/data.rs:28 (identical to actual impl)
fn new(stream_id: StreamId, payload: T) -> Data<T> {let flags = DataFlags(0);Data { stream_id, data: payload, flags, pad_len: None }}// nom/src/internal.rs:348 (close to actual impl, but Ok case uses closure)fn parse(&mut self, i: I) -> Result<(I, O2), Err<E>> {let result = self.f.parse(i);match result {// Should be:// Result::Ok((i, o)) => Result::Ok((i, (self.g)(o))),Result::Ok(_) => {let _0 = Err::Incomplete(Needed::Unknown);
Result::Err(_0)}
Result::Err(_0) => Result::Err(_0),}}// either/src/lib.rs:832 (identical to actual impl)
fn factor_first(self) -> (T, Either<A, B>) {match self {Either::Left(_0) => {let _1 = Either::Left(_0.1);(_0.0, _1)}
Either::Right(_0) => {let _1 = Either::Right(_0.1);(_0.0, _1)}}}// syn/src/punctuated.rs:984 (identical to actual impl)
fn into_tuple(self) -> (T, Option<P>) {match self {Pair::Punctuated(_0, _1) => {let _1 = Some(_1);(_0, _1)}
Pair::End(_0) => (_0, None),}}B.2

Complex Reasoning about References

The next function for a linked list iterator, which operates on the Iter datatype with a referencetyped field.
// SLL Tutorial definition, rather than our simplified definition
struct List<T> { elem: T, next: Option<Box<List<T>>> }pub struct Iter<'a, T> { next: Option<&'a List<T>> }Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 164. Publication date: June 2023.

Leveraging Rust Types for Program Synthesis (Appendix)

164:5

impl<'a, T> Iterator for Iter<'a, T> {type Item = &'a T;#[ensures(match self.len() {0 => (^self).len() == 0 && matches!(result, None),v => (^self).len() == v-1 && matches!(result, Some(_)),})]
fn next(&mut self) -> Option<Self::Item> {let (new, result) = match &mut self.next {None => (None, None),Some(_0) => match &_0.next {None => {let result = Some(&_0.elem);(None, result)}Some(_0_next_de) => {let result = Some(&_0.elem);
let new = Some(&**_0_next_de);(new, result)}},};
self.next = new;result}}B.3

Complex Recursion

The non-destructive append benchmark takes as input immutable references to two linked lists andcreates a new list containing elements of both. The main function, sll_append_copy, recursively
traverses one of the lists, and upon reaching the end, it calls the auxiliary sll_append_copy_7,
whose task is to recursively copy the other list. This auxiliary is not provided by the user, but is
automatically discovered by RusSOL.
// Simple linked list
enum List<T> { Nil, Cons(Box<(T, List<T>)>) }#[ensures(result.len() == x1.len() + x2.len())]
fn sll_append_copy<T: Copy>(x1: &List<T>, x2: &List<T>) -> List<T> {match x2 {List::Nil => sll_append_copy_7(x1),List::Cons { elem, next } => {let de = *elem;
let result = sll_append_copy(x1, &**next);
let next = Box::new(result);
List::Cons { elem: de, next }}}}fn sll_append_copy_7<T: Copy>(x: &List<T>) -> List<T> {match x {List::Nil => List::Nil,Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 164. Publication date: June 2023.

164:6

Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey
List::Cons { elem, next } => {let de = *elem;
let result = sll_append_copy_7(next);
let next = Box::new(result);
List::Cons { elem: de, next }}}}The rose tree copy benchmark takes as input an immutable reference to a rose tree and createsa new tree with the same set of elements. A rose tree is a variable-arity tree, whose children are
stored in a linked list. To copy a rose tree, the synthesizer needs to create two mutually recursivefunctions: copy copies a tree and calls copy_8 to copy its children; copy_8 copies a list of trees andcalls copy to copy each of them.
// A rose tree is either empty or a node with a value and a linked list of subtrees
enum Tree<T> { Nil, Cons { elem: T, next: List<Tree<T>> } }// Simple linked list
enum List<T> { Nil, Cons(Box<(T, List<T>)>) }impl<T> Tree<T> {#[ensures(result.elems() == self.elems())]
fn copy(&self) -> Tree<T> {match self {Tree::Nil => Tree::Nil,Tree::Cons { elem, next } => {let de = *elem;
Self::copy_8(de, elem, next) // mutual recursion}}}fn copy_8(de: T, elem_self: &T, next: &List<Tree<T>>) -> Tree<T> {match next {List::Nil => Tree::Cons { elem: de, next: List::Nil },List::Cons(_0) => {let result = _0.0.copy(); // mutual recursion
match result {Tree::Nil => Self::copy_8(de, elem_self, &_0.1),
Tree::Cons { elem: elem_result, next } => {let result = Self::copy_8(de, elem_self, &_0.1);
let bx = (result, next);
let _0 = Box::new(bx);let next = List::Cons(_0);
Tree::Cons { elem: elem_result, next }
}
}
}
}
}
}

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 164. Publication date: June 2023.