Polynomial-time Adversaries

import Onewayf.PolyTime
import Onewayf.Bitstrings

-- leandown
-- [meta]
-- title = "Polynomial-time adversaries"
-- group = "Cryptography"
-- [content]

-- # {{definition}}: Polynomial-time adversaries
--
-- In cryptography, an **adversary** is an algorithm that tries to break a
-- security property — for instance, inverting a one-way function. We model
-- adversaries as functions `BitString → PMF BitString`: given a challenge,
-- they return a probability distribution over responses.
--
-- The predicate `PolyTimeAdversary F` asserts that `F` runs in polynomial time.
-- It is defined inductively with two constructors:
--
-- **`ofDet`** — the base case. Any `PolyTimeComputable` function
-- `f : BitString → BitString` gives a poly-time adversary by returning
-- `pure (f x)` (a point mass at the deterministic output). This covers all
-- adversaries that make no random choices.
--
-- **`uniformPad`** — models the standard reduction technique where an adversary
-- needs fresh random coins but only receives a deterministic query. Given a
-- `PolyTimeAdversary` `F` and a padding length `k`, the new adversary on input
-- `y`:
-- 1. samples `a ←$ {0,1}^k` (fresh uniform random bits)
-- 2. runs `F` on `a ++ y` (the padded input)
-- 3. strips the first `k` bits of the output and returns the rest
--
-- The point is that `F` sees a uniformly random prefix on top of its real
-- input, which is exactly the structure used in reductions like `buildAdv`
-- in the quadratic OWF construction.
--
/-- A polynomial-time adversary: a poly-time algorithm (possibly randomized via
    uniform sampling) producing a distribution over bit strings. -/
inductive PolyTimeAdversary : (BitString → PMF BitString) → Prop where
  /-- A deterministic poly-time function, lifted to a distribution via `pure`. -/
  | ofDet {f} : PolyTimeComputable f →
      PolyTimeAdversary (fun x => PMF.pure (f x))
  /-- Prepend `k` fresh uniform random bits to the input, run `F`, then strip
      the prefix. Models reductions that supply random coins to a sub-adversary. -/
  | uniformPad (k : ℕ) {F} : PolyTimeAdversary F →
      PolyTimeAdversary (fun y => do
        let a ← uniformBitStringOfLength k
        let z ← F (a ++ y)
        return List.drop k z)
  /-- Prepend a *fixed* bit string to the input, run `F`, then strip `k` bits.
      Models reductions that use a fixed index or constant prefix. -/
  | fixedPad (pfx : BitString) (k : ℕ) {F} : PolyTimeAdversary F →
      PolyTimeAdversary (fun y => (F (pfx ++ y)).map (·.drop k))