Documentation

CslibFrontier.Computability.Complexity.Classes.IP.CoinFixing

Fixing the coins of a verifier machine #

An IP verifier is realized by the clocked run of a finite fair-coin oracle machine M (Cslib.Probability.IsOraclePPTOn). Every live instruction of the run draws one fresh coin, so a run of t instructions is determined by t coins and the replies. Fixing the coins r and truncating every reply to its first t bits, which the run cannot read beyond, leaves the program Cslib.Complexity.Interaction.coinProgram M t x r making word requests. Against every stateful prover the run is the average of these programs over uniform coins (Cslib.Complexity.Interaction.run_interpret_runOracle_eq_coins), so the acceptance probability of the verifier is the average of the acceptance probabilities of the programs (Cslib.Complexity.Interaction.acceptProb_eq_sum).

A deterministic replay of a program against a history executes one instruction per coin, answering the messages from the history (Cslib.Complexity.Interaction.replayStep, Cslib.Complexity.Interaction.simulate); it computes the outcome of the program (Cslib.Complexity.Interaction.outcome_coinProgram). Along the replay the machine sends at most one message per instruction, of length at most the number of instructions so far, and reads replies only through their first t bits. So the programs of t coins form a bounded family, with at most t messages, each of length less than t (Cslib.Complexity.Interaction.isBounded_coinFamily).

Main definitions #

Main results #

References #

Programs of fixed coins #

source
def Cslib.Complexity.Interaction.coinStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (M : Turing.MultiTapePTM k Bool Control Operation) (t : ℕ) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation) (b : Bool) :
WordQueryComp Operation (Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation)

One instruction of M with the coin b, its replies truncated to their first t bits.

Instances For
    source
    def Cslib.Complexity.Interaction.coinProgram {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (M : Turing.MultiTapePTM k Bool Control Operation) (t : ℕ) (x r : List Bool) :
    WordQueryComp Operation Bool

    The verifier M on the input x with the coins r, one per instruction, its replies truncated to their first t bits; it accepts when its output is [true].

    Instances For
      source
      def Cslib.Complexity.Interaction.coinFamily {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (M : Turing.MultiTapePTM k Bool Control Operation) (t : ℕ) (x : List Bool) (r : Fin t → Bool) :
      WordQueryComp Operation Bool

      The family of the programs of t coins.

      Instances For
        source
        theorem Cslib.Complexity.Interaction.run_interpret_runOracle_eq_coins {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (M : Turing.MultiTapePTM k Bool Control Operation) {S : Type} (oracle : Operation × List Bool → StateT S PMF (List Bool)) (t : ℕ) (x : List Bool) (s : S) :
        (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (M.runOracle t x)).run s = (BitString.uniformList t).bind fun (r : List Bool) => (OracleComp.interpret oracle ((fun (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation) => cfg.tapes.output) <$> List.foldlM (coinStep M t) (Turing.MultiTapeMachine.FiniteConfig.init M.initial x) r)).run s

        The run averages the programs of fixed coins, against every stateful prover, retaining its final state.

        source
        theorem Cslib.Complexity.Interaction.acceptProb_eq_sum {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (M : Turing.MultiTapePTM k Bool Control Operation) {V : Probability.WordOracleComp Operation Bool} {t : ℕ} {x : List Bool} (hV : ∀ (S : Type) (oracle : Operation × List Bool → StateT S PMF (List Bool)) (s : S), (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (⇑Turing.MultiTapeTM.encBool <$> V)).run s = (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (M.runOracle t x)).run s) (P : Prover Operation) :
        acceptProb V P = (2 ^ t)⁻¹ * ∑ r : Fin t → Bool, acceptFrom P P.init (some (coinProgram M t x (List.ofFn r)))

        Acceptance averages over the coins. If the verifier V is realized by the run of M under the clock t, then its acceptance probability against P averages the acceptance probabilities of the programs of fixed coins.

        The replay #

        source
        def Cslib.Complexity.Interaction.replayStep {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) (t : ℕ) (p : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit × History) (b : Bool) :
        Except (Option (List Bool)) (Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit × History)

        One instruction of M with the coin b, answering a message from the history, if any; failing with the message when the history is exhausted, and with none when the message differs from the history.

        Instances For
          source
          def Cslib.Complexity.Interaction.simulate {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) (t : ℕ) (x r : List Bool) (h : History) :
          Except (Option (List Bool)) (Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit × History)

          The replay of M on the input x with the coins r against the history h.

          Instances For
            source
            theorem Cslib.Complexity.Interaction.outcome_coinProgram {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) (t : ℕ) (x r : List Bool) (h : History) :
            outcome (coinProgram M t x r) h = replayOutcome (Except.map (fun (p : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit × History) => (decide (p.1.tapes.output = [true]), p.2)) (simulate M t x r h))

            Outcomes are replays: the outcome of the program of the coins r after the history h is read off the replay.

            Bounds on the replay #

            source
            def Cslib.Complexity.Interaction.ReplayInv {k : ℕ} {Control : Type} (t : ℕ) (x : List Bool) (h : History) (i : ℕ) :
            Except (Option (List Bool)) (Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit × History) → Prop

            The invariant of the replay after i instructions against h: a live replay has consumed at most i entries of h and its storage is bounded; a replay out of history has consumed all of h within fewer than i instructions and its message is shorter than i.

            Instances For
              source
              theorem Cslib.Complexity.Interaction.isBounded_coinFamily {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) (t : ℕ) (x : List Bool) :
              IsBounded (coinFamily M t x) t t

              The programs of t coins form a bounded family: at most t messages, each of length at most t, and only the first t bits of each reply matter.