  We introduce Flux, which shows how logical refinements can work hand in glove
with Rust's ownership mechanisms to yield ergonomic type-based verification of
low-level pointer manipulating programs. First, we design a novel refined type
system for Rust that indexes mutable locations, with pure (immutable) values
that can appear in refinements, and then exploits Rust's ownership mechanisms
to abstract sub-structural reasoning about locations within Rust's polymorphic
type constructors, while supporting strong updates. We formalize the crucial
dependency upon Rust's strong aliasing guarantees by exploiting the stacked
borrows aliasing model to prove that ``well-borrowed evaluations of well-typed
programs do not get stuck''. Second, we implement our type system in Flux, a
plug-in to the Rust compiler that exploits the factoring of complex invariants
into types and refinements to efficiently synthesize loop annotations --
including complex quantified invariants describing the contents of containers
-- via liquid inference. Third, we evaluate Flux with a benchmark suite of
vector manipulating programs and parts of a previously verified secure
sandboxing library to demonstrate the advantages of refinement types over
program logics as implemented in the state-of-the-art Prusti verifier. While
Prusti's more expressive program logic can, in general, verify deep functional
correctness specifications, for the lightweight but ubiquitous and important
verification use-cases covered by our benchmarks, liquid typing makes
verification ergonomic by slashing specification lines by a factor of two,
verification time by an order of magnitude, and annotation overhead from up to
24% of code size (average 9%) to nothing at all.
