Documentation

Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape

Execution with saved coins #

Replay is a fold of one-step calls to the shared interpreter, with each supplied coin returned by a pure program. Exhausting the list retains the complete current configuration; a halted machine ignores the remaining coins. Query handlers can still have effects.

Sampling all coins in advance preserves the joint final configuration and private oracle state, provided the original coin program denotes a stateless fair bit. The query handler may be randomized and share state across its operations. This is a semantic equality; a deterministic machine implementing replay from an encoded input and coin tape needs a separate certificate.

Main definitions #

Main results #

References #

Adapted from the cslib crypto branch's Computability/Machines/Turing/MultiTape/Probabilistic/CoinTape.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common interpreter and typed program API.

source
def Turing.MultiTapePTM.runConfigFromCoins {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
Cslib.OracleComp spec (MultiTapeMachine.Config k Symbol State Oracle input)

Replay the shared interpreter with a supplied coin per step. Only the query handler can have effects; the replay itself does not draw randomness.

Instances For
    source
    @[simp]
    theorem Turing.MultiTapePTM.runConfigFromCoins_nil {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
    machine.runConfigFromCoins query [] cfg = pure cfg
    source
    theorem Turing.MultiTapePTM.runConfigFromCoins_cons {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (bit : Bool) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
    machine.runConfigFromCoins query (bit :: coins) cfg = machine.runConfigFrom (pure bit) query 1 cfg >>= machine.runConfigFromCoins query coins

    The first coin supplies one instruction before replay resumes on the tail.

    source
    @[simp]
    theorem Turing.MultiTapePTM.runConfigFromCoins_halted {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (h : cfg.tapes.state = none) :
    machine.runConfigFromCoins query coins cfg = pure cfg

    A halted machine ignores all remaining coins and performs no further queries.

    source
    theorem Turing.MultiTapePTM.runConfigFromCoins_append {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (coins more : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
    machine.runConfigFromCoins query (coins ++ more) cfg = machine.runConfigFromCoins query coins cfg >>= machine.runConfigFromCoins query more

    Concatenating tapes agrees with pausing and resuming, as an equality of typed programs.

    source
    theorem Turing.MultiTapePTM.interpret_runConfigFromCoins {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] {m : Type → Type u_1} [Monad m] [LawfulMonad m] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → m (spec q)) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
    Cslib.OracleComp.interpret oracle (machine.runConfigFromCoins query coins cfg) = List.foldlM (fun (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (bit : Bool) => Cslib.OracleComp.interpret oracle (machine.runConfigFrom (pure bit) query 1 cfg)) cfg coins

    Interpretation commutes with the replay fold, without resetting any handler state.

    source
    theorem Turing.MultiTapePTM.run_interpret_runConfigFrom_one {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] {OracleState : Type} (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hcoin : ∀ (s : OracleState), (Cslib.OracleComp.interpret oracle coin).run s = PMF.map (fun (bit : Bool) => (bit, s)) (Cslib.Probability.PMF.uniformOfFintype Bool)) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (s : OracleState) :
    (Cslib.OracleComp.interpret oracle (machine.runConfigFrom coin query 1 cfg)).run s = (Cslib.Probability.PMF.uniformOfFintype Bool).bind fun (bit : Bool) => (Cslib.OracleComp.interpret oracle (machine.runConfigFrom (pure bit) query 1 cfg)).run s

    A single instruction can use a pre-sampled coin when the coin program is stateless and fair. The entire query handler state is retained.

    source
    theorem Turing.MultiTapePTM.run_interpret_runConfigFrom_eq_coins {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] {OracleState : Type} (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hcoin : ∀ (s : OracleState), (Cslib.OracleComp.interpret oracle coin).run s = PMF.map (fun (bit : Bool) => (bit, s)) (Cslib.Probability.PMF.uniformOfFintype Bool)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (s : OracleState) :
    (Cslib.OracleComp.interpret oracle (machine.runConfigFrom coin query fuel cfg)).run s = (Cslib.BitString.uniformList fuel).bind fun (coins : List Bool) => (Cslib.OracleComp.interpret oracle (machine.runConfigFromCoins query coins cfg)).run s

    Sampling the entire private coin tape in advance preserves the joint configuration and private oracle state, including randomized query handlers sharing that state.

    source
    theorem Turing.MultiTapePTM.interpret_runConfigFrom_eq_coins {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → PMF (spec q)) (hcoin : Cslib.OracleComp.interpret oracle coin = Cslib.Probability.PMF.uniformOfFintype Bool) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
    Cslib.OracleComp.interpret oracle (machine.runConfigFrom coin query fuel cfg) = (Cslib.BitString.uniformList fuel).bind fun (coins : List Bool) => Cslib.OracleComp.interpret oracle (machine.runConfigFromCoins query coins cfg)

    Without private state, the clocked run is the average of its fixed-coin programs.

    source
    def Turing.MultiTapePTM.runFromCoins {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
    Cslib.OracleComp spec (List Symbol)

    Observe the output of a replay program, retaining any effects of its query handler.

    Instances For
      source
      def Turing.MultiTapePTM.runCoins {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (coins : List Bool) (input : List Symbol) :
      Cslib.OracleComp spec (List Symbol)

      Replay from blank work and communication tapes.

      Instances For
        source
        def Turing.MultiTapePTM.withCoin {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (bit : Bool) :
        MultiTapeMachine k Symbol State Empty Id

        Fix one Boolean branch of a closed table, retaining its original states and tapes.

        Instances For
          source
          def Turing.MultiTapePTM.runClosedConfigFromCoins {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
          MultiTapeMachine.Config k Symbol State Empty input

          Closed replay is a deterministic fold of the selected one-step transition tables.

          Instances For
            source
            theorem Turing.MultiTapePTM.runConfigFrom_pure_coin {k : ℕ} {Symbol State Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (bit : Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
            machine.runConfigFrom (pure bit) Empty.elim 1 cfg = pure ((machine.withCoin bit).step cfg)

            A closed one-step program with a fixed coin is a pure deterministic transition.

            source
            theorem Turing.MultiTapePTM.runConfigFromCoins_closed {k : ℕ} {Symbol State Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
            machine.runConfigFromCoins Empty.elim coins cfg = pure (machine.runClosedConfigFromCoins coins cfg)

            With no oracle channels, the entire fixed-coin program is pure.

            source
            def Turing.MultiTapePTM.runClosedCoins {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (input : List Symbol) :
            List Symbol

            The output of a closed replay from blank tapes, as a deterministic function.

            Instances For
              source
              theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_eq_map_coins {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
              (machine.runClosedConfigFrom fuel cfg).eval = PMF.map (fun (coins : List Bool) => machine.runClosedConfigFromCoins coins cfg) (Cslib.BitString.uniformList fuel)

              The complete closed configuration is a deterministic function of uniform saved coins.

              source
              theorem Turing.MultiTapePTM.eval_runClosed_eq_map_coins {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (input : List Symbol) :
              (machine.runClosed fuel input).eval = PMF.map (fun (coins : List Bool) => machine.runClosedCoins coins input) (Cslib.BitString.uniformList fuel)

              A closed fair-coin run is a deterministic function of a uniform tape of clock length.

              source
              theorem Turing.MultiTapePTM.runClosedConfigFromCoins_mem_support {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
              machine.runClosedConfigFromCoins coins cfg ∈ (machine.runClosedConfigFrom coins.length cfg).eval.support

              Every saved tape yields a supported configuration at the corresponding clock.

              source
              theorem Turing.MultiTapePTM.runClosedCoins_mem_support {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (input : List Symbol) :
              machine.runClosedCoins coins input ∈ (machine.runClosed coins.length input).eval.support

              Every saved tape yields a supported output, including inputs that run to the clock cutoff.