OAI/Computability/MaxCut/PCP/HeaderAccumulate.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Actual fixed-coefficient affine address construction. A finite literal phase loads the coefficient, the checked width-two Horner machine reads coefficient and preserved offset with the rank as its radix, then the literal field is actually consumed. All operands and work stacks are restored.

  1. structure OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.Layout line 12
  2. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.statement line 22
  3. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.resultTapes line 27
  4. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.result_bits line 31
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.result_count line 35
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.result_accumulator line 39
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.result_frame line 44
  8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.trace line 49
  9. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.inTime line 95
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.inTime_steps line 109
  11. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.machine line 118
  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderAccumulate.source_inputBits_header line 129
  13. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceStartup.Tape line 147
  14. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceStartup.State line 148
  15. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ArithmeticLabel line 149
  16. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceStartup.Label line 150
  17. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.headerLayout line 154
  18. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.arithmeticEntry line 162
  19. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.arithmeticProgram line 165
  20. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.program line 170
  21. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialTapes line 176
  22. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initializedTapes line 179
  23. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.countedTapes line 182
  24. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.outputTapes line 186
  25. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.readyTapes line 191
  26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_formula line 198
  27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_current line 202
  28. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_remaining line 206
  29. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_variableHeader line 210
  30. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_clauseHeader line 216
  31. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_work line 222
  32. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_work_raw line 229
  33. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_field line 233
  34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialized_clean line 240
  35. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initialArithmeticMetadata line 254
  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initial_arithmetic line 257
  37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initial_loader line 261
  38. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.initializeInTime line 265
  39. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.arithmeticInTime line 281
  40. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.arithmeticConfiguration line 303
  41. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.arithmetic_step line 309
  42. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.arithmeticPlacedInTime line 327
  43. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.phaseBound line 342
  44. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.phasesInTime line 348
  45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.output_eq_ready line 357
  46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_formula line 374
  47. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_current line 377
  48. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_remaining line 380
  49. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_variableHeader line 383
  50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_clauseHeader line 386
  51. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_leftBlock line 389
  52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_dummy line 393
  53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_accumulator line 397
  54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_field line 401
  55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_work_blank line 404
  56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_sharedWork line 410
  57. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.ready_sharedFrame line 414
  58. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.startupInTime line 424
  59. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.timePolynomial line 432
  60. theorem OAI.MaxCutGames.Foundations.Hastad.SourceStartup.phaseBound_le_polynomial line 437
  61. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.startupInPolynomialTime line 458
  62. def OAI.MaxCutGames.Foundations.Hastad.SourceStartup.machine line 467
  63. inductive OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Label line 493
  64. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Layout line 499
  65. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.digits line 501
  66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.horner_value line 504
  67. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.steps line 508
  68. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.operandLength line 511
  69. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.timePolynomial line 514
  70. theorem OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.timePolynomial_eval line 518
  71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.steps_le_timePolynomial line 523
  72. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.statement line 540
  73. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.program line 548
  74. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.coefficientTapes line 552
  75. theorem OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.affineTrace line 556

    Source documentation

    Exact affine execution, including coefficient initialization and cleanup.

    theorem affineTrace (slots : Layout ↪ K) (coefficient : Nat) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, p (labels label) = statement slots coefficient labels exit label)
    (base : K → List Bool) (rank offset : Nat)
    (rankWord : base (slots (.inl 0)) = encodeWord rank)
    (offsetWord : base (slots (.inr 1)) = encodeWord offset)
    (coefficientEmpty : base (slots (.inr 0)) = [])
    (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step p))^[steps coefficient rank offset]
      (some ⟨some (labels .seed), ((ambient, ()), register), base⟩) =
      some ⟨exit, ((ambient, ()), none),
        MachineHorner.resultTapes slots base (coefficient * rank + offset)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Layout, OAI.MaxCutGames.Foundations.Hastad.coefficient, OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Label, OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.statement, OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.steps

  76. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.affineInTime line 624
  77. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.affineInPolynomialTime line 641
  78. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.programInTime line 658
  79. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.leftBaseInTime line 671

    Source documentation

    Left query-block base from the preserved variable tuple rank and a zero offset field.

    def leftBaseInTime (F : Formula) (u : Nat) (c : ClauseContext F u) (v : VariableContext F u)
    (slots : Layout ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, p (labels label) = statement slots (2 ^ (2 ^ u)) labels exit label)
    (base : K → List Bool)
    (rankWord : base (slots (.inl 0)) = encodeWord (((variableEncoding F u).code v).val))
    (zeroWord : base (slots (.inr 1)) = encodeWord 0)
    (coefficientEmpty : base (slots (.inr 0)) = [])
    (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step p)
      ⟨some (labels .seed), ((ambient, ()), register), base⟩
      (some ⟨exit, ((ambient, ()), none), MachineHorner.resultTapes slots base (baseValue F u c v 0)⟩)
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Label, OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.statement

  80. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.rightBaseInTime line 691

    Source documentation

    Right query-block base using the globally retained left-block size.

    def rightBaseInTime (F : Formula) (u : Nat) (c : ClauseContext F u) (v : VariableContext F u)
    (slots : Layout ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, p (labels label) = statement slots (2 ^ (8 ^ u)) labels exit label)
    (base : K → List Bool)
    (rankWord : base (slots (.inl 0)) = encodeWord (((clauseEncoding F u).code c).val))
    (leftBlockWord : base (slots (.inr 1)) = encodeWord (2 ^ (2 ^ u) * F.«variables» ^ u))
    (coefficientEmpty : base (slots (.inr 0)) = [])
    (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step p)
      ⟨some (labels .seed), ((ambient, ()), register), base⟩
      (some ⟨exit, ((ambient, ()), none), MachineHorner.resultTapes slots base (baseValue F u c v 1)⟩)
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Label, OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.statement

  81. theorem OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.resultTapes_dummy line 714

    Source documentation

    The retained dummy register is among the unchanged external tapes.

    theorem resultTapes_dummy (slots : Layout ↪ K) (base : K → List Bool) (value : Nat)
    (dummy : K) (distinct : dummy ≠ slots (.inl 3)) :
    MachineHorner.resultTapes slots base value dummy = base dummy :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.Layout

  82. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.machine line 719
  83. def OAI.MaxCutGames.Foundations.Hastad.SourceBasePhase.machineInTime line 730