OAI/Computability/MaxCut/PCP/ContextPrepare.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.Arena line 13
2. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.LoadState line 14
3. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.PrepareState line 15
4. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.State line 16
5. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.Label line 17
6. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.prepareEntry line 21
7. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.stateSwap line 25
8. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.program line 28
9. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.preparationConfiguration line 34
10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.preparation_step line 42
11. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.initialState line 61
12. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.finalState line 65
13. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.loadInTime line 70
14. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.signatureInTime line 91
15. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.prepareInTime line 113
16. def OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.machine line 135
17. inductive OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.HeaderTape line 155
18. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList line 158
19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_getElem?_ctorIdx_eq line 160
20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_nodup line 164
21. instance OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.(instance at line 166) line 166
22. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.Tape line 170
23. inductive OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.Label line 172
24. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.variableHeader line 180
25. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.clauseHeader line 181
26. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.headerDestination line 182
27. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.readStart line 183
28. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.readLoop line 184
29. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.labelAt line 185
30. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.program line 187
31. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.atReadStart line 206
32. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.atReadLoop line 211
33. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.atReadDone line 216
34. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.copiedInput line 222
35. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.readOutput line 225
36. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.headerOutput line 229
37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.clear_readOutput line 234
38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.readOutput_work line 244
39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.headerOutput_frame line 249
40. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.headerInTime line 253
41. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.digitOutput line 289
42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.digitOutput_frame line 292
43. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.digitInTime line 296
44. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.stageTapes line 339
45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.stageTapes_frame line 344
46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.stageTapes_current line 355
47. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.stageTapes_remaining line 375
48. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.prefixInTime line 396
49. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.digitsInTime line 424
50. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.outputTapes line 443
51. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.initializeInTime line 446
52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_current line 478
53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_remaining line 482
54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_frame line 486
55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_work line 492
56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_variableHeader line 497
57. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_clauseHeader line 502
58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_headers line 507
59. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.output_formula line 513
60. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.timePolynomial line 518
61. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.timePolynomial_eval line 521
62. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.machine line 525
63. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.rank line 544
64. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.reverseDigits line 547
65. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.reverseDigits_apply line 550
66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.horner_value_sum line 554
67. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.horner_reverse_eq_rank line 569
68. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.reverseSlots line 589

    Source documentation

    Reverse only digit positions. All six fixed work/control roles stay put.

    def reverseSlots (slots : MachineHorner.Layout width ↪ K) : MachineHorner.Layout width ↪ K :=
    …

69. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.reverseSlots_control line 592
70. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.reverseSlots_digit line 595
71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.clean_reverseSlots line 601
72. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.statement line 608
73. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.program line 613
74. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.rankTrace line 619

    Source documentation

    Exact execution using existing digit fields; only the destination changes.

    theorem rankTrace (slots : MachineHorner.Layout width ↪ K)
        (labels : MachineHorner.Label width → Λ) (exit : Option Λ)
        (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ label, p (labels label) = statement slots labels exit label)
        (base : K → List Bool) (radix : Nat) (digits : Fin width → Nat)
        (operandRadix : base (slots (.inl 0)) = encodeWord radix)
        (operandDigits : ∀ i, base (slots (.inr i)) = encodeWord (digits i))
        (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
        (MachineComposition.advance (TM2.step p))^[
          MachineHorner.steps radix (reverseDigits digits) width]
          (some ⟨some (labels .start), ((ambient, ()), register), base⟩) =
          some ⟨exit, ((ambient, ()), none), MachineHorner.resultTapes slots base (rank radix digits)⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.statement, OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.reverseDigits, OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.rank

75. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.rankInTime line 638
76. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.rankInPolynomialTime line 655
77. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.variableRankInTime line 674
78. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.clauseRankInTime line 690
79. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.programInTime line 706
80. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.machine line 718
81. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.machineInTime line 729
82. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.clauseSlots line 744

    Source documentation

    Control roles may include preserved headers and dedicated protected extras.

    def clauseSlots (controls : Fin 6 ↪ Extra) :
        MachineHorner.Layout u ↪ SourceContextLoad.Tape u Extra where
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.Tape

83. def OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.variableSlots line 762

    Source documentation

    Each coordinate selects its own loaded variable field, even if names repeat.

    def variableSlots (controls : Fin 6 ↪ Extra) (selected : SlotContext u) :
        MachineHorner.Layout u ↪ SourceContextLoad.Tape u Extra where
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.Tape

84. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.clauseSlots_control line 779
85. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.clauseSlots_digit line 782
86. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.variableSlots_control line 785
87. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.variableSlots_digit line 788
88. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRankPhase.selectedDigits_loaded line 792