Adversarial computations are a widely studied class of computations
where resource-bounded probabilistic adversaries have access to
oracles, i.e., probabilistic procedures with private state. These
computations arise routinely in several domains, including security,
privacy and machine learning.

In this paper, we develop program logics for reasoning about
adversarial computations in a higher-order setting. Our logics are
built on top of a simply typed $\lambda$-calculus extended with a
graded monad for probabilities and state. The grading is used to
model and restrict the memory footprint and the cost (in terms of
oracle calls) of computations. Under this view, an adversary is a
higher-order expression that expects as arguments the code of its
oracles. We develop unary program logics for reasoning about error
probabilities and expected values, and a relational logic for
reasoning about coupling-based properties. All logics feature rules
for adversarial computations, and yield guarantees that are valid
for all adversaries that satisfy a fixed resource policy. We prove
the soundness of the logics in the category of quasi-Borel spaces,
using a general notion of graded predicate liftings, and we use
logical relations over graded predicate liftings to establish the
soundness of proof rules for adversaries. We illustrate the working
of our logics with simple but illustrative examples.