A recent paper by Barthe et al. (2019) defines a relational logic, rqPD, for proving facts about pairs of quantum programs, in which assertions are modeled as quantum effects; i.e., given a predicate $0 \leq A \leq I$ and a state $\rho$, $A$ holds on $\rho$ to degree $0 \leq \tr{A\rho} \leq 1$. This makes their approach promising for proving quantatative facts about quantum protocols, such as security loss for quantum cryptographic protocols. This approach poses some challenges, however: 1) How do we model the security of quantum protocols using a quantum-effect predicate in such a way that the security loss corresponds to the degree to which the predicate is satisfied? 2) How can we express a bound on this security loss using an rqPD-style judgement, and how can we reason about such judgements? We solve (1) by showing that the quantum equality predicates in Barthe et al. bound trace distance, which, when when applied appropriately, can be seen as an upper bound on the probability an adversary can distinguish the real and ideal programs in a cryptographic game. To solve (2), we demonstrate how loss can be incorporated into the predicate itself, and show that (for a subset of programs that encompasses many cryptographic protocols), quantum weakest precondition logic can be used to verify or compute the loss of a given predicate.