  Properties such as provable security and correctness for randomized programs
are naturally expressed relationally as approximate equivalences. As a result,
a number of relational program logics have been developed to reason about such
approximate equivalences of probabilistic programs. However, existing
approximate relational logics are mostly restricted to first-order programs
without general state.
  In this paper we develop Approxis, a higher-order approximate relational
separation logic for reasoning about approximate equivalence of programs
written in an expressive ML-like language with discrete probabilistic sampling,
higher-order functions, and higher-order state. The Approxis logic recasts the
concept of error credits in the relational setting to reason about relational
approximation, which allows for expressive notions of modularity and
composition, a range of new approximate relational rules, and an
internalization of a standard limiting argument for showing exact probabilistic
equivalences by approximation. We also use Approxis to develop a logical
relation model that quantifies over error credits, which can be used to prove
exact contextual equivalence. We demonstrate the flexibility of our approach on
a range of examples, including the PRP/PRF switching lemma, IND\$-CPA security
of an encryption scheme, and a collection of rejection samplers. All of the
results have been mechanized in the Coq proof assistant and the Iris separation
logic framework.
