Examples

Run liquid-rust

To run liquid-rust in one of the examples copy the liquid-rust script to somewhere in your path and edit the file to define the LIQUID_RUST variable to point to the root of the liquid-rust repository. Then you should be able to run it on examples like so

$ liquid-rust --crate-type=rlib src/ex5_simple_rvec.rs

Comparisons with Prusti

Example Name	Prusti	LR	Source
Fill	Pr		toy
Min Index	Pr	LR	toy
KMP	Pr	LR	LH
Union-Find	Pr		src
Heap-Sort	Pr	LR	rosetta
Knight's Tour	Pr		rosetta
Knuth Shuffle	Pr	LR	rosetta
Copy	Pr	LR	DML
BinSearch	Pr	LR	DML
Dot-Product	Pr	LR	DML
FFT	Pr	LR	DML
Simplex	Pr	LR	DML
Kmeans	Pr*	LR	self

Dsolve Examples

• [~] src/arraymax.rs (requires HOF/Fn support)

Notes on Comparison with Prusti (WIP)

Hard to reason about nested data structures

While it is possible to work around this issue, you are constrained in how you specify nested data structures. Example: simplex.rs -- need to make 2D matrix wrapper, whereas in liquid rust you don't need to make one

There's also an ergonomics issue since the nested structure may not implement copy, so you have to pass around references.

Especially mutable nested data structures

A big part of the issue is from viperproject/prusti-dev#389, which seems to pop up in a lot of places when working with mutable nested data structures (e.g., in kmeans.rs). Additionally, there's the following error in Prusti currently: viperproject/prusti-dev#903.

With mutation, you want to use == to reason about the data in the outer structure. However, the default implementation of == for, e.g., vectors isn't pure so can't be used in the specification. Example: see vec_test.rs.

Loop invariants often necessary, sometimes redundant

Examples

ex2_min_index_loop.rs -- need body_invariant!(i < sz); despite the loop condition being i < sz. ex4_kmp.rs -- need body_invariant!(t.len() == pattern.len()); despite neither vector being mutable and their lengths not being changed