Documentation

Complexity.Computability.Machines.Turing.MultiTape.Machine.Program

Clocked machine execution as a typed program #

The transition-choice and query handlers express one machine run in the shared OracleComp language. A deterministic handler returns its action; a fair-coin handler samples a bit and selects that branch. The handlers are explicit semantic parameters: an arbitrary handler need not be fair, efficient, or even respect the choices supplied by the transition table.

Each unit of fuel executes one table instruction. Submitting a query costs one instruction; writing its buffer and reading its reply cost ordinary instructions. The handler's internal computation is external to this clock. Resource predicates must fix the intended choice handler and separately account for substituted oracle implementations.

Clock exhaustion retains the entire configuration. Pausing and resuming, and replacing either handler by another program, preserve the program itself, hence its interaction with every stateful interpreter and the final private state.

The interpreter and proof patterns are adapted from the cslib crypto branch's fair-coin interpreter at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common choice mechanism and the typed program interface of cslib PR #1129.

Main definitions #

Main results #

source
def Turing.MultiTapeMachine.runConfigFrom {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) :
ℕ → Config k Symbol State Oracle input → Cslib.OracleComp spec (Config k Symbol State Oracle input)

Unfold a bounded run, retaining the entire configuration on halting or clock exhaustion.

Instances For
    source
    def Turing.MultiTapeMachine.runFrom {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) :
    Cslib.OracleComp spec (List Symbol)

    Observe only the output word after a bounded execution.

    Instances For
      source
      def Turing.MultiTapeMachine.run {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (input : List Symbol) :
      Cslib.OracleComp spec (List Symbol)

      Run from blank work and communication tapes.

      Instances For
        source
        @[simp]
        theorem Turing.MultiTapeMachine.runConfigFrom_zero {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (cfg : Config k Symbol State Oracle input) :
        machine.runConfigFrom choose query 0 cfg = pure cfg
        source
        @[simp]
        theorem Turing.MultiTapeMachine.runConfigFrom_halted {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) (h : cfg.tapes.state = none) :
        machine.runConfigFrom choose query fuel cfg = pure cfg
        source
        @[simp]
        theorem Turing.MultiTapeMachine.runFrom_zero {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (cfg : Config k Symbol State Oracle input) :
        machine.runFrom choose query 0 cfg = pure cfg.tapes.output
        source
        theorem Turing.MultiTapeMachine.runConfigFrom_add {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (first second : ℕ) (cfg : Config k Symbol State Oracle input) :
        machine.runConfigFrom choose query (first + second) cfg = machine.runConfigFrom choose query first cfg >>= machine.runConfigFrom choose query second

        Pausing and resuming preserves the entire program and uses the sum of the two clocks.

        source
        theorem Turing.MultiTapeMachine.runFrom_add {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (first second : ℕ) (cfg : Config k Symbol State Oracle input) :
        machine.runFrom choose query (first + second) cfg = machine.runConfigFrom choose query first cfg >>= machine.runFrom choose query second

        Resume a paused execution and then observe its output.

        source
        theorem Turing.MultiTapeMachine.interpret_runConfigFrom {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {Query' : Type u} {spec' : Cslib.OracleSpec Query'} (handler : (q : Query) → Cslib.OracleComp spec' (spec q)) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) :
        Cslib.OracleComp.interpret handler (machine.runConfigFrom choose query fuel cfg) = machine.runConfigFrom (fun (choices : Choose (Action k Symbol State Oracle)) => Cslib.OracleComp.interpret handler (choose choices)) (fun (oracle : Oracle) (word : List Symbol) => Cslib.OracleComp.interpret handler (query oracle word)) fuel cfg

        Substituting either handler commutes with clocked execution, before interpreting any effects. In particular, substitution does not reset the private state shared by calls.

        source
        theorem Turing.MultiTapeMachine.interpret_run {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {Query' : Type u} {spec' : Cslib.OracleSpec Query'} (handler : (q : Query) → Cslib.OracleComp spec' (spec q)) (fuel : ℕ) (input : List Symbol) :
        Cslib.OracleComp.interpret handler (machine.run choose query fuel input) = machine.run (fun (choices : Choose (Action k Symbol State Oracle)) => Cslib.OracleComp.interpret handler (choose choices)) (fun (oracle : Oracle) (word : List Symbol) => Cslib.OracleComp.interpret handler (query oracle word)) fuel input

        Substituting handlers preserves the complete output program.

        source
        theorem Turing.MultiTapeMachine.length_output_runConfigFrom_le {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {OracleState : Type} (oracle : (q : Query) → StateT OracleState PMF (spec q)) (fuel : ℕ) (cfg final : Config k Symbol State Oracle input) (s s' : OracleState) (h : (final, s') ∈ ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query fuel cfg)).run s).support) :
        final.tapes.output.length ≤ cfg.tapes.output.length + fuel

        Every supported execution writes at most one output symbol per instruction, regardless of the sizes of oracle replies or the private state shared by the handlers.

        source
        theorem Turing.MultiTapeMachine.length_output_runFrom_le {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {OracleState : Type} (oracle : (q : Query) → StateT OracleState PMF (spec q)) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) (s s' : OracleState) (output : List Symbol) (h : (output, s') ∈ ((Cslib.OracleComp.interpret oracle (machine.runFrom choose query fuel cfg)).run s).support) :
        output.length ≤ cfg.tapes.output.length + fuel

        Observing only the output preserves the supported-output bound.

        source
        theorem Turing.MultiTapeMachine.runConfigFrom_pure {k : ℕ} {Symbol State Query : Type} {input : List Symbol} {spec : Cslib.OracleSpec Query} (machine : MultiTapeMachine k Symbol State Empty Id) (fuel : ℕ) (cfg : Config k Symbol State Empty input) :
        machine.runConfigFrom pure (fun (oracle : Empty) => oracle.elim) fuel cfg = pure (machine.step^[fuel] cfg)

        The deterministic run program computes exactly the iterated deterministic step.

        source
        theorem Turing.MultiTapeMachine.runConfigFrom_toTM {k : ℕ} {Symbol State Query : Type} {input : List Symbol} {spec : Cslib.OracleSpec Query} (machine : MultiTapeMachine k Symbol State Empty Id) (fuel : ℕ) (cfg : Config k Symbol State Empty input) :
        Config.tapes <$> machine.runConfigFrom pure (fun (oracle : Empty) => oracle.elim) fuel cfg = pure (MultiTapeTM.runFrom cfg.tapes fuel)

        Removing the empty channels from a deterministic run program gives the upstream clocked run.