OAI/Computability/MaxCut/Machines/MachineStateFrame.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameStatement line 13

   Source documentation

   Same code and stacks, with an untouched caller-register component.

   def frameStatement : TM2.Stmt Γ Λ σ → TM2.Stmt Γ Λ (σ × τ)
     | .push k f next => .push k (fun state => f state.1) (frameStatement next)
     | .peek k f next => .peek k (fun state bit => (f state.1 bit, state.2))
         (frameStatement next)
     | .pop k f next => .pop k (fun state bit => (f state.1 bit, state.2))
         (frameStatement next)
     | .load f next => .load (fun state => (f state.1, state.2)) (frameStatement next)
     | .branch f yes no => .branch (fun state => f state.1)
         (frameStatement yes) (frameStatement no)
     | .goto f => .goto (fun state => f state.1)
     | .halt => .halt

2. def OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration line 25
3. def OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameProgram line 28
4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_state line 31
5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_metadata line 34
6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_tapes line 37
7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameStatement_pushBound line 40
8. def OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.statement line 45

   Source documentation

   Optional continuation and labels use the existing subroutine semantics.

   def statement (labels : Λ → Λ') (exit : Option Λ') (q : TM2.Stmt Γ Λ σ) :
       TM2.Stmt Γ Λ' (σ × τ) :=
   …

9. def OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.configuration line 49
10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.configuration_state line 53
11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.configuration_metadata line 57
12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.configuration_tapes line 61
13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.statement_pushBound line 65
14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frame_stepAux line 75
15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frame_step line 97

    Source documentation

    This identity also covers the final halted configuration.

    theorem frame_step (source : Λ → TM2.Stmt Γ Λ σ) (ambient : τ)
        (c : TM2.Cfg Γ Λ σ) :
        TM2.step (frameProgram source) (frameConfiguration ambient c) =
          (TM2.step source c).map (frameConfiguration ambient) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameProgram, OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration

16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frame_advance line 109
17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frame_iterate line 118
18. def OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameExecution line 131

    Source documentation

    Actual execution with the same step count, budget, and tapes.

    def frameExecution (source : Λ → TM2.Stmt Γ Λ σ) (ambient : τ)
        {start : TM2.Cfg Γ Λ σ} {finish : Option (TM2.Cfg Γ Λ σ)} {budget : ℕ}
        (run : StateTransition.EvalsToInTime (TM2.step source) start finish budget) :
        StateTransition.EvalsToInTime (TM2.step (frameProgram source))
          (frameConfiguration ambient start) (finish.map (frameConfiguration ambient)) budget where
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameProgram, OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration

19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameExecution_steps line 145
20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.stepAux_simulation line 150
21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.step_simulation line 157
22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.trace line 170
23. def OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.execution line 181
24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.execution_steps line 191