OAI/Computability/UniqueGames/Reduction/AddressTupleBody.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Arena line 16
2. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Rows line 17
3. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Slots line 18
4. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleBody.BodyState line 19
5. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleBody.CleanupLabel line 20
6. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleBody.RowLabel line 22
7. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Label line 24
8. instance OAI.UniqueGamesTheorem.Integration.AddressTupleBody.labelFintype line 28
9. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.sourceLabels line 34
10. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.rhsLabel line 36
11. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.rowLabels line 37
12. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.cleanupLabels line 39
13. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.resetLabel line 41
14. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.main line 44
15. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.reset line 46
16. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.instruction line 49
17. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.program line 63
18. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.rhs line 67
19. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.loaded line 70
20. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.tupleBits line 74
21. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.emitted line 79
22. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.finalTapes line 86
23. structure OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Ready line 92
24. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.budget line 102
25. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.run line 111
26. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.source line 165
27. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBody.rhs_eq_actual line 168
28. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBody.canonicalValues_eq_actual line 171
29. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBody.tupleBits_actual line 180
30. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBody.actualInvariant line 193

    Source documentation

    All generic template-correctness obligations are discharged from the actual loader's canonical field values and the checked fixed-row specs.

    theorem actualInvariant (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
        (T : NoiseTables.Table s d) (base : Arena k s d noiseCount → List Bool)
        (ready : Ready F tuple base)
        (clean : MachineAddressEdge.Clean (Slots k s d noiseCount) base) (B C : Nat)
        (hB : base (headerTape k s d noiseCount .baseValue) = encodeWord B)
        (hC : base (headerTape k s d noiseCount .capacity) = encodeWord C) :
        MachineOutcomeRows.Invariant (Slots k s d noiseCount) B C
          (AddressOutcomeSpecs.values (AddressTupleLoaded.canonicalValues F tuple))
          (MachineOutcomeRows.selected (AddressOutcomeSpecs.rows k T) (rhs F tuple))
          (loaded F tuple base) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Ready, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Slots, OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.canonicalValues, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.rhs, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.loaded

31. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.run_fixed_rows line 217

    Source documentation

    Actual fixed-row execution. Physical readiness and stored header values are its only data hypotheses; no template or body-execution premise remains.

    noncomputable def run_fixed_rows (T : NoiseTables.Table s d)
        (labels : Label k s d noiseCount (AddressOutcomeSpecs.rows k T) → Λ) (exit : Option Λ)
        (P : Λ → TM2.Stmt (fun _ : Arena k s d noiseCount => Bool) Λ (BodyState k))
        (atLabels : ∀l, P (labels l) = instruction (AddressOutcomeSpecs.rows k T) labels exit l)
        (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
        (base : Arena k s d noiseCount → List Bool) (ready : Ready F tuple base)
        (clean : MachineAddressEdge.Clean (Slots k s d noiseCount) base)
        (oldRhs : Fin k → Bool) (B C : Nat)
        (hB : base (headerTape k s d noiseCount .baseValue) = encodeWord B)
        (hC : base (headerTape k s d noiseCount .capacity) = encodeWord C) :
        StateTransition.EvalsToInTime (TM2.step P)
          ⟨some (labels (main (AddressOutcomeSpecs.rows k T))), (((oldRhs, ()), ()), none), base⟩
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Label, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.BodyState, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.instruction, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Ready, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Slots, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.main

32. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBody.finalTapes_eq line 238
33. def OAI.UniqueGamesTheorem.Integration.AddressTupleBody.run_actual line 246
34. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBody.saved_of_current line 272