OAI/Computability/MaxCut/Games/EquationLookup.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape line 15
2. inductive OAI.MaxCutGames.Reduction.SourceEquationLookup.Label line 19
3. def OAI.MaxCutGames.Reduction.SourceEquationLookup.fieldDestination line 25
4. def OAI.MaxCutGames.Reduction.SourceEquationLookup.readStart line 26
5. def OAI.MaxCutGames.Reduction.SourceEquationLookup.readLoop line 27
6. def OAI.MaxCutGames.Reduction.SourceEquationLookup.skipLabel line 28
7. def OAI.MaxCutGames.Reduction.SourceEquationLookup.headerLabel line 29
8. def OAI.MaxCutGames.Reduction.SourceEquationLookup.program line 36

   Source documentation

   Eight binary stacks and fixed finite control. Every loop scans one actual bit or tests one actual counter bit. The arbitrary ambient state is preserved.

   def program : Label → TM2.Stmt (fun _ : Tape => Bool) Label (σ × Option Bool)
     | .copyOut => Reduction.MachineTransfer.loopAt .source .scratch id false
         .copyOut (some .copyBack)
     | .copyBack => MachineCopy.forkLoop .scratch .source .work false
         .copyBack (some .headerFirst)
     | .headerFirst => MachineLookup.discard .work .headerFirst .headerSecond
     | .headerSecond => MachineLookup.discard .work .headerSecond .guard
     | .guard => MachineUnaryCounter.guard .index (skipLabel 0) (readStart 0)
     | .skip slot => MachineLookup.discard .work (.skip slot) (skipLabel (slot.val + 1))
     | .read slot =>
         if slot.1.val < 4 then
           if slot.2 then
   …

   Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Label, OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Reduction.SourceEquationLookup.skipLabel, OAI.MaxCutGames.Reduction.SourceEquationLookup.readStart

9. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.atSkip line 53
10. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.atReadStart line 57
11. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.atReadLoop line 61
12. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.atReadDone line 66
13. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.discardHeadersTrace line 70

    Source documentation

    The two header fields are physically consumed from the work copy.

    theorem discardHeadersTrace (base : Tape → List Bool) (variableCount equations : Nat)
        (suffix : List Bool) (hinput : base .work = encodeWords [variableCount, equations] ++ suffix) (ambient : σ) :
        (advance (TM2.step program))^[variableCount + equations + 2]
          (some ⟨some .headerFirst, (ambient, none), base⟩) =
          some ⟨some .guard, (ambient, none), Function.update base .work suffix⟩ := by
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.SourceEquationLookup.program

14. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.discardFourTrace line 84

    Source documentation

    The fixed skip body consumes four complete unary fields and returns to the same counter guard, preserving the counter and every other tape.

    theorem discardFourTrace (base : Tape → List Bool) (values : List Nat)
        (hlen : values.length = 4) (suffix : List Bool)
        (hinput : base .work = encodeWords values ++ suffix) (ambient : σ) :
        (advance (TM2.step program))^[(encodeWords values).length]
          (some ⟨some (skipLabel 0), (ambient, none), base⟩) =
          some ⟨some .guard, (ambient, none), Function.update base .work suffix⟩ := by
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.SourceEquationLookup.program, OAI.MaxCutGames.Reduction.SourceEquationLookup.skipLabel

15. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.readFourTrace line 95

    Source documentation

    Read the selected four fields using the already checked scanner.

    theorem readFourTrace (base : Tape → List Bool) (values : List Nat)
        (hlen : values.length = 4) (suffix : List Bool)
        (hinput : base .work = encodeWords values ++ suffix) (ambient : σ) :
        (advance (TM2.step program))^[(encodeWords values).length + 5]
          (some ⟨some (readStart 0), (ambient, none), base⟩) =
          some ⟨none, (ambient, none),
            SourceFieldArray.sequenceTapes .work fieldDestination base 0 values suffix⟩ := by
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.SourceEquationLookup.program, OAI.MaxCutGames.Reduction.SourceEquationLookup.readStart, OAI.MaxCutGames.Reduction.SourceEquationLookup.fieldDestination

16. def OAI.MaxCutGames.Reduction.SourceEquationLookup.scanTapes line 112

    Source documentation

    Normal form for the changing counter and consumed work-copy prefix.

    def scanTapes (base : Tape → List Bool) (index : Nat)
        (indexSuffix input : List Bool) : Tape → List Bool :=
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape

17. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.scanTapes_work line 116
18. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.scanTapes_index line 120
19. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.scanTapes_other line 125
20. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.update_scanTapes_work line 130
21. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.skipEquationsTrace line 139

    Source documentation

    Each equation-index bit causes one genuine guard transition and exactly four field-discard loops. The final zero guard enters the field reader.

    theorem skipEquationsTrace {n : Nat} (base : Tape → List Bool)
        (prior : List (CloneGap.Equation (Fin n))) (indexSuffix suffix : List Bool)
        (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[(encodeWords (prior.flatMap equationWords)).length + prior.length + 1]
          (some ⟨some .guard, (ambient, register), scanTapes base prior.length indexSuffix
            (encodeWords (prior.flatMap equationWords) ++ suffix)⟩) =
          some ⟨some (readStart 0), (ambient, none), scanTapes base 0 indexSuffix suffix⟩ := by
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.CloneGap.Equation, OAI.MaxCutGames.Reduction.SourceEquationLookup.program, OAI.MaxCutGames.Reduction.SourceEquationLookup.scanTapes, OAI.MaxCutGames.Reduction.SourceEquationLookup.readStart

22. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.fieldDestination_eq line 187
23. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.fieldDestination_injective_below line 193
24. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.readFour_output_field line 199
25. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.readFour_output_work line 211
26. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.readFour_output_frame line 219
27. def OAI.MaxCutGames.Reduction.SourceEquationLookup.outputTapes line 227
28. def OAI.MaxCutGames.Reduction.SourceEquationLookup.scanSteps line 233
29. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.scanReadTrace line 239
30. def OAI.MaxCutGames.Reduction.SourceEquationLookup.lookupSteps line 267
31. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.lookupWithSplitTrace line 271
32. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_source line 301
33. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_index line 307
34. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_work line 313
35. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_field line 319
36. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_first line 326
37. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_second line 332
38. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_third line 338
39. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_rhs line 344
40. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_frame line 350
41. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.equationWords_four line 357
42. def OAI.MaxCutGames.Reduction.SourceEquationLookup.fieldWords line 362
43. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.output_fieldWords line 365
44. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.lookupSteps_le_input line 371
45. def OAI.MaxCutGames.Reduction.SourceEquationLookup.timePolynomial line 390
46. theorem OAI.MaxCutGames.Reduction.SourceEquationLookup.timePolynomial_eval line 392
47. def OAI.MaxCutGames.Reduction.SourceEquationLookup.lookupWithSplitInTime line 396

    Source documentation

    A polynomial bound on the actual complete copy/skip/read execution.

    def lookupWithSplitInTime (F : SourceEncoding.Input) (prior : List (CloneGap.Equation (Fin F.«variables»)))
        (equation : CloneGap.Equation (Fin F.«variables»)) (after : List (CloneGap.Equation (Fin F.«variables»)))
        (hsplit : F.equations = prior ++ equation :: after)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hsource : base .source = inputBits F)
        (hindex : base .index = encodeWord prior.length ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (ambient : σ) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some .copyOut, (ambient, register), base⟩
          (some ⟨none, (ambient, none),
            outputTapes base equation indexSuffix (encodeWords (after.flatMap equationWords))⟩)
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.CloneGap.Equation, OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.SourceEquationLookup.program, OAI.MaxCutGames.Reduction.SourceEquationLookup.outputTapes

48. def OAI.MaxCutGames.Reduction.SourceEquationLookup.lookupInTime line 416
49. def OAI.MaxCutGames.Reduction.SourceEquationLookup.machine line 435
50. def OAI.MaxCutGames.Reduction.SourceEquationLookup.machineInTime line 447

    Source documentation

    The same proved run stated directly for the concrete finite machine.

    def machineInTime (F : SourceEncoding.Input) (i : Fin F.equations.length)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hsource : base .source = inputBits F)
        (hindex : base .index = encodeWord i.val ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (register : Option Bool) :
        StateTransition.EvalsToInTime machine.step
          ⟨some .copyOut, ((), register), base⟩
          (some ⟨none, ((), none), outputTapes base F.equations[i.val] indexSuffix
            (encodeWords ((F.equations.drop (i.val + 1)).flatMap equationWords))⟩)
          (timePolynomial.eval (inputBits F).length) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.SourceEquationLookup.outputTapes

51. def OAI.MaxCutGames.Reduction.SourceEquationLookup.placedLookupInTime line 463

    Source documentation

    Same-tape placement into the caller's finite control. Choosing the ambient type to be τ × Unit gives the shared state (τ × Unit) × Option Bool used by the field-template machinery. The lookup's final transition enters exit.

    noncomputable def placedLookupInTime {Λ' : Type}
        (labels : Label → Λ') (exit : Option Λ')
        (target : Λ' → TM2.Stmt (fun _ : Tape => Bool) Λ' (σ × Option Bool))
        (atLabels : ∀ l, target (labels l) =
          MachineSubroutine.statement labels exit (program (σ := σ) l))
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Label, OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.SourceEquationLookup.program

52. def OAI.MaxCutGames.Reduction.SourceEquationLookup.embeddedLookupInTime line 484

    Source documentation

    An optional disjoint-stack placement preserves arbitrary extra tapes and state. It reuses the same generic lookup and introduces no extra transitions.

    noncomputable def embeddedLookupInTime {E Λextra τ : Type} [DecidableEq E]
        (continuation : Option (Label ⊕ Λextra)) (extraState : τ)
        (extraTapes : E → List Bool)
        (extra : Λextra → TM2.Stmt
          (MachineEmbedding.Alphabet (fun _ : Tape => Bool) (fun _ : E => Bool))
          (Label ⊕ Λextra) ((σ × Option Bool) × τ))
        (input : SourceEncoding.Input) (i : Fin input.equations.length)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hsource : base .source = inputBits input)
        (hindex : base .index = encodeWord i.val ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (ambient : σ) (register : Option Bool) :
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEquationLookup.Label, OAI.MaxCutGames.Reduction.SourceEquationLookup.Tape, OAI.MaxCutGames.Reduction.SourceEncoding.Input