Documentation

Complexitylib.Classes.PPoly.Uniform.Unrolling.Generator.Transition.Case.Internal

Direct-unrolling transition-case generator -- proof internals #

source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseChoice_sound_internal (choiceValue : Bool) :
(emitCaseChoice choiceValue).Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseRead_sound_internal (stateCount workCount tapeIndex symbolIndex : ℕ) :
(emitCaseRead stateCount workCount tapeIndex symbolIndex).Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers_sound_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) :
(emitCaseMembers stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCaseReadSize_sound_internal :
prepareCaseReadSize.Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseConnector_sound_internal :
emitCaseConnector.Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseReadConnector_sound_internal :
emitPreviousCaseReadConnector.Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseChoiceConnector_sound_internal :
emitPreviousCaseChoiceConnector.Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_sound_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) :
(emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).Sound
source
def Complexity.CircuitUnrolling.Serializer.DirectGenerator.caseReadStartValues (values : BinaryValues WorkCount) (tapeIndex symbolIndex : ℕ) :
BinaryValues WorkCount

Register state used to begin reading one transition case.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseChoice_effect_internal (choiceValue : Bool) (values : BinaryValues WorkCount) (hreference₀ : values Work.reference₀ = 0) (hreference₁ : values Work.reference₁ = 0) :
    (emitCaseChoice choiceValue).effect values = Function.update values Work.available (values Work.available + caseChoiceLiteralSize choiceValue)
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseChoice_emitted_internal (choiceValue : Bool) (values : BinaryValues WorkCount) :
    (emitCaseChoice choiceValue).emitted values = List.flatMap CircuitCode.RawGate.encode (caseChoiceLiteralSchedule (values Work.available) (values Work.reference₀) choiceValue)
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseChoice_requires_internal (choiceValue : Bool) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hemit : values Work.emitCounter = 0) :
    (emitCaseChoice choiceValue).requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseRead_effect_internal (stateCount workCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) :
    (emitCaseRead stateCount workCount tapeIndex symbolIndex).effect values = Function.update (caseReadStartValues values tapeIndex symbolIndex) Work.available (values Work.available + caseReadSize (values Work.horizon))
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseRead_emitted_internal (stateCount workCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) :
    (emitCaseRead stateCount workCount tapeIndex symbolIndex).emitted values = List.flatMap CircuitCode.RawGate.encode (readFormulaSchedule stateCount (workCount + 2) (values Work.horizon) (values Work.configBase) (values Work.available) tapeIndex symbolIndex)
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseRead_requires_internal (stateCount workCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) :
    (emitCaseRead stateCount workCount tapeIndex symbolIndex).requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCaseReadSize_effect_internal (values : BinaryValues WorkCount) :
    prepareCaseReadSize.effect values = Function.update (Function.update values Work.temporary₃ (caseReadSize (values Work.horizon))) Work.temporary₂ 0
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCaseReadSize_emitted_internal (values : BinaryValues WorkCount) :
    prepareCaseReadSize.emitted values = []
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCaseReadSize_requires_internal (values : BinaryValues WorkCount) (hmultiply : values Work.multiplyCounter = 0) (hadd : values Work.addCounter = 0) :
    prepareCaseReadSize.requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseConnector_effect_internal (values : BinaryValues WorkCount) :
    emitCaseConnector.effect values = Function.update (Function.update values Work.available (values Work.available + 1)) Work.reference₁ 0
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseConnector_emitted_internal (values : BinaryValues WorkCount) :
    emitCaseConnector.emitted values = { op := AndOrOp.and, input₀ := values Work.reference₀, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseConnector_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (havailable : 1 ≤ values Work.available) (hemit : values Work.emitCounter = 0) :
    emitCaseConnector.requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseReadConnector_effect_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₃ = 0) :
    emitPreviousCaseReadConnector.effect values = Function.update (Function.update (Function.update values Work.reference₀ (values Work.reference₀ - values Work.temporary₃)) Work.available (values Work.available + 1)) Work.reference₁ 0
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseReadConnector_emitted_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₃ = 0) :
    emitPreviousCaseReadConnector.emitted values = { op := AndOrOp.and, input₀ := values Work.reference₀ - values Work.temporary₃, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseReadConnector_requires_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₃ = 0) (hoffset : values Work.temporary₃ ≤ values Work.reference₀) (hcopy : values Work.copyCounter = 0) (havailable : 1 ≤ values Work.available) (hemit : values Work.emitCounter = 0) :
    emitPreviousCaseReadConnector.requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseChoiceConnector_effect_internal (values : BinaryValues WorkCount) :
    emitPreviousCaseChoiceConnector.effect values = Function.update (Function.update (Function.update values Work.reference₀ (values Work.reference₀ - 1)) Work.available (values Work.available + 1)) Work.reference₁ 0
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseChoiceConnector_emitted_internal (values : BinaryValues WorkCount) :
    emitPreviousCaseChoiceConnector.emitted values = { op := AndOrOp.and, input₀ := values Work.reference₀ - 1, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseChoiceConnector_requires_internal (values : BinaryValues WorkCount) (hreference : 1 ≤ values Work.reference₀) (hcopy : values Work.copyCounter = 0) (havailable : 1 ≤ values Work.available) (hemit : values Work.emitCounter = 0) :
    emitPreviousCaseChoiceConnector.requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers_effect_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) :
    (emitCaseMembers stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).effect values = Function.update (caseReadStartValues values (workCount + 1) outputSymbolIndex) Work.available (values Work.available + caseFormulaMembersSize workCount (values Work.horizon) choiceValue)
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers_requires_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) :
    (emitCaseMembers stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers_emitted_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) :
    (emitCaseMembers stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).emitted values = List.flatMap CircuitCode.RawGate.encode (caseFormulaMemberGates stateCount workCount (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt)
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_effect_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) :
    (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).effect values = Function.update values Work.available (values Work.available + caseFormulaScheduleSize workCount (values Work.horizon) choiceValue)
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_requires_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) :
    (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).requires values
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_emitted_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) :
    (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).emitted values = List.flatMap CircuitCode.RawGate.encode (caseFormulaSchedule stateCount workCount (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt)
    source
    theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_spaceBoundByWidth_internal (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), CaseFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hinputSymbol : inputSymbolIndex < 4) (houtputSymbol : outputSymbolIndex < 4) (hworkSymbols : ∀ index < workCount, workSymbolIndexAt index < 4) (hcap : ∀ (inputLength tapeIndex symbolIndex position : ℕ), tapeIndex ≤ workCount + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon → values inputLength Work.available + caseFormulaScheduleSize workCount (values inputLength Work.horizon) choiceValue + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef stateCount (workCount + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (workCount + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + values inputLength Work.horizon ≤ width inputLength) :
    (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).SpaceBoundByWidthAt initialSpace values width