OAI/Computability/MaxCut/Machines/Runtime2.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

Every work tape of the actual alphabet-table machine stores Bool symbols. This checks the work alphabets separately from the finite-machine structure's input-alphabet condition, without changing the runtime certificate.

  1. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial line 12
  2. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial_eval line 18
  3. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Runtime.time line 25
  4. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Runtime.tableOutputsInTime line 29

    Source documentation

    The concrete driver outputs exactly the checked table encoding.

    noncomputable def tableOutputsInTime {q : Nat} (input : GenericGraphTables.Table q) :
    TM2OutputsInTime (Driver.machine q) (GenericGraphTables.tableBits input)
      (some (GraphTables.tableBits (Table.build input)))
      ((time q).eval (GenericGraphTables.tableBits input).length) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Runtime.time

  5. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Runtime.tablePolynomialTime line 47

    Source documentation

    Fixed q determines one finite machine and one natural polynomial. The input and output alphabets use the exact shared Bool serialization interfaces.

    noncomputable def tablePolynomialTime (q : Nat) :
    TM2ComputableInPolyTime (GenericGraphTables.tableBits (q := q))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits

  6. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.finiteAlphabet line 74
  7. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Runtime.finiteAlphabet line 80
  8. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statement line 104

    Source documentation

    Translate instructions using the checked recursive translator, keeping every tape and destination label unchanged.

    abbrev statement (e : σ ≃ τ) : Stmt Γ Λ σ → Stmt Γ Λ τ :=
…
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statement_symm_statement line 109

    Source documentation

    Translating every instruction back restores the original statement, including its state-dependent instruction functions.

    @[simp] theorem statement_symm_statement (e : σ ≃ τ) (q : Stmt Γ Λ σ) :
    statement e.symm (statement e q) = q := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statement

  10. def OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration line 115
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration_label line 118
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration_state line 121
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration_tapes line 124
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration_symm_configuration line 127
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration_configuration_symm line 132
  16. def OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv line 138

    Source documentation

    This is a bijection on actual machine configurations, not just on states.

    def configurationEquiv (e : σ ≃ τ) : Cfg Γ Λ σ ≃ Cfg Γ Λ τ where
…
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv_apply line 144
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.control_configuration line 147
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.program line 152
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.program_symm_program line 155
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statementPushBound line 161

    Source documentation

    The register change does not alter the finite statement's push bound.

    theorem statementPushBound (e : σ ≃ τ) (q : Stmt Γ Λ σ) :
    Runtime.statementPushBound (statement e q) = Runtime.statementPushBound q := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.Runtime.statementPushBound, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statement

  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.supportsStmt_iff line 167

    Source documentation

    Exactly the same finite label set supports the translated statement.

    theorem supportsStmt_iff (e : σ ≃ τ) (S : Finset Λ) (q : Stmt Γ Λ σ) :
    SupportsStmt S (statement e q) ↔ SupportsStmt S q := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statement

  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.supports_iff line 189
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport line 197

    Source documentation

    The actual recursively interpreted statement commutes with the register equivalence, with exactly the same tape updates.

    theorem stepAux_transport (e : σ ≃ τ) (q : Stmt Γ Λ σ) (state : σ)
    (tapes : ∀ k, List (Γ k)) :
    stepAux (statement e q) (e state) tapes =
      configuration e (stepAux q state tapes) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statement, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration

  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport_symm line 204
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.step_transport line 212

    Source documentation

    Exact conjugacy also covers the halted configuration and the none step.

    theorem step_transport (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ) (c : Cfg Γ Λ σ) :
    step (program e source) (configuration e c) =
      (step source c).map (configuration e) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.program, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration

  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.step_iff line 224
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.advance_transport line 236
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.iterate_transport line 246

    Source documentation

    Every intermediate configuration is transported at its original time index. This includes traces whose option-valued result is none.

    theorem iterate_transport (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ) (n : Nat)
    (c : Option (Cfg Γ Λ σ)) :
    (MachineComposition.advance (step (program e source)))^[n]
        (c.map (configuration e)) =
      ((MachineComposition.advance (step source))^[n] c).map (configuration e) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.program, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration

  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.trace_iff line 259

    Source documentation

    A successful running trace exists for exactly the same number of steps in the translated and original program.

    theorem trace_iff (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ) (n : Nat)
    (a b : Cfg Γ Λ σ) :
    (MachineComposition.advance (step (program e source)))^[n]
        (some (configuration e a)) = some (configuration e b) ↔
      (MachineComposition.advance (step source))^[n] (some a) = some b := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.program, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration

  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.trace line 275
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.execution line 284

    Source documentation

    Transport an actual runtime witness without changing its step count or budget; the final option may be either a configuration or none.

    def execution (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ)
    {start : Cfg Γ Λ σ} {finish : Option (Cfg Γ Λ σ)} {budget : Nat}
    (run : StateTransition.EvalsToInTime (step source) start finish budget) :
    StateTransition.EvalsToInTime (step (program e source))
      (configuration e start) (finish.map (configuration e)) budget where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.program, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration

  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.execution_steps line 298
  34. def OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.execution_reflect line 305

    Source documentation

    Conversely, a translated runtime witness determines the original witness at exactly the same number of transitions.

    def execution_reflect (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ)
    {start : Cfg Γ Λ σ} {finish : Option (Cfg Γ Λ σ)} {budget : Nat}
    (run : StateTransition.EvalsToInTime (step (program e source))
      (configuration e start) (finish.map (configuration e)) budget) :
    StateTransition.EvalsToInTime (step source) start finish budget where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.program, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration

  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.execution_reflect_steps line 320
  36. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet line 335
  37. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.State line 336
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.clean line 338
  39. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.compareStateEquiv line 341

    Source documentation

    Reassociate the actual three comparison registers into the shared state.

    def compareStateEquiv (A : Type) : MachineCompare.State A ≃ State A where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.State

  40. inductive OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label line 347
  41. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList line 353
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_getElem?_ctorIdx_eq line 356
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_nodup line 360
  44. instance OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.(instance at line 362) line 362
  45. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.exitAt line 366
  46. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.bitEncoding line 371
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.emit line 374

    Source documentation

    Two fixed exits, each containing only literal push instructions.

    def emit (destination : K) (bit : Bool) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (State A) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.State

  48. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.instruction line 379
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.copySteps line 397
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.compareSteps line 398
  51. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.steps line 399
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.steps_le line 401
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.encodeWord_eq_iff line 405
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.emit_step line 414
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.joinTrace_inline_MachineUnaryEqualityBit line 426
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityTrace line 432

    Source documentation

    Actual execution of the two copies, the translated comparison, and the literal bit writer, inside any program containing the stated instructions.

    theorem equalityTrace (tape : Fin 6 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.State

  57. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime line 535

    Source documentation

    Timed correctness has only concrete input-tape and instruction premises.

    def equalityInTime (tape : Fin 6 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Label, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.State

  58. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.machine line 554
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryEqualityBit.machineInTime line 565
  60. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.Field line 603
  61. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.inputSize line 605
  62. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.fieldEquiv line 607
  63. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.inputEquiv line 611
  64. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.packData line 615

    Source documentation

    Proof-level organization of exactly the finite bits physically read.

    def packData {t S : Nat} (data : Fin t → Field S → Bool) : Buffer (inputSize t S) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.Field, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.inputSize

  65. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.packData_inputEquiv line 618
  66. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.basePredicate line 623
  67. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.leftMatches line 627
  68. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.rightMatches line 631
  69. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.firstMatch line 636

    Source documentation

    The scan order is the fixed increasing finite-index order.

    def firstMatch {S : Nat} (mask : Fin S → Bool) : Option (Fin S) :=
…
  70. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.firstMatch_spec line 639
  71. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.firstMatch_none line 646
  72. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.edgeAccept line 652

    Source documentation

    labelAt is a fixed finite lookup table determined by the reduction parameters, for example decodeLabel a (allAddresses.get i).

    def edgeAccept {t S q : Nat} (labelAt : Fin q → Fin S → GraphTables.Label)
    (bits : Buffer (inputSize t S)) (k : Fin t) (a b : Fin q) : Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.inputSize

  73. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.edgeAccept_of_matches line 658
  74. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.rowAccept line 666
  75. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.rowAccept_eq_true line 670
  76. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.rowBlock line 677

    Source documentation

    Every powered-label pair is written in the canonical row-major order.

    def rowBlock {t S q : Nat} (labelAt : Fin q → Fin S → GraphTables.Label)
    (bits : Buffer (inputSize t S)) : Buffer (q * q) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.inputSize

  77. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.rowBlock_at line 683
  78. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodeBit line 692
  79. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodeBits line 694
  80. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodeBits_append line 698
  81. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodeBits_graphWords line 704
  82. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodeBits_length_le line 711
  83. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.readEncodedSlots line 725

    Source documentation

    Read one zero-delimited unary Boolean field for each fixed register slot. The second pop occurs exactly when the value is one.

    def readEncodedSlots (src : K) : List (Fin N) →
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) →
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N)
  | [], next => next
  | i :: slots, next =>
      .pop src (fun state head =>
        (state.1, Function.update state.2 i (head.getD false)))
        (.branch (fun state => state.2 i)
          (.pop src (fun state _ => state) (readEncodedSlots src slots next))
          (readEncodedSlots src slots next))

variable [DecidableEq K]
  84. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedSlots line 738
  85. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedAll line 757
  86. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_readEncodedSlots line 773
  87. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.writeEncodedSlots line 783

    Source documentation

    The delimiter is pushed first, then the optional unary one; writing slots in reverse order gives the canonical field order on the destination stack.

    def writeEncodedSlots {M : Nat} (dst : K) (emit : σ → Buffer M) : List (Fin M) →
    TM2.Stmt (fun _ : K => Bool) Λ σ → TM2.Stmt (fun _ : K => Bool) Λ σ
  | [], next => next
  | i :: slots, next => .push dst (fun _ => false)
      (.branch (fun state => emit state i)
        (.push dst (fun _ => true) (writeEncodedSlots dst emit slots next))
        (writeEncodedSlots dst emit slots next))
  88. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.stepAux_writeEncodedSlots line 791
  89. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_writeEncodedSlots line 808
  90. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodedBlockStmt line 825
  91. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodedBlockAt line 832
  92. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_encodedBlockAt line 836
  93. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockStmt line 845
  94. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockAt line 860
  95. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.step_encodedBlockAt line 871
  96. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.rowAt line 890
  97. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.machine line 895
  98. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.machine_statementPushBound line 906
  99. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.machineInTime line 914

    Source documentation

    The input predicate/match block is consumed. The exact unary predicate row is prepended; the remaining input, old output, and ambient register are accounted for in the actual transition witness.

    def machineInTime {t S q : Nat} (labelAt : Fin q → Fin S → GraphTables.Label)
    (bits : Buffer (inputSize t S)) (suffix : List Bool)
    (register : Buffer (inputSize t S)) (tapes : Bool → List Bool)
    (hinput : tapes false = encodeBits (List.ofFn bits) ++ suffix) :
    StateTransition.EvalsToInTime (machine (t := t) labelAt).step
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.inputSize, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodeBits, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.machine