  We introduce Refinement Reflection, a new framework for building SMT-based
deductive verifiers. The key idea is to reflect the code implementing a
user-defined function into the function's (output) refinement type. As a
consequence, at uses of the function, the function definition is instantiated
in the SMT logic in a precise fashion that permits decidable verification.
Reflection allows the user to write equational proofs of programs just by
writing other programs using pattern-matching and recursion to perform
case-splitting and induction. Thus, via the propositions-as-types principle, we
show that reflection permits the specification of arbitrary functional
correctness properties. Finally, we introduce a proof-search algorithm called
Proof by Logical Evaluation that uses techniques from model checking and
abstract interpretation, to completely automate equational reasoning. We have
implemented reflection in Liquid Haskell and used it to verify that the widely
used instances of the Monoid, Applicative, Functor, and Monad typeclasses
actually satisfy key algebraic laws required to make the clients safe, and have
used reflection to build the first library that actually verifies assumptions
about associativity and ordering that are crucial for safe deterministic
parallelism.
