  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.
