Direct-unrolling read-formula generator -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadMember_sound_internal (stateCount tapeCount : ℕ) : (emitReadMember stateCount tapeCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setReadFormulaLimit_sound_internal : setReadFormulaLimit.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadMembers_sound_internal (stateCount tapeCount : ℕ) : (emitReadMembers stateCount tapeCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadIdentity_sound_internal : emitReadIdentity.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadConnector_sound_internal : emitReadConnector.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadNextConnector_sound_internal : emitReadNextConnector.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_sound_internal (stateCount tapeCount : ℕ) : (emitReadFormula stateCount tapeCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadMember_effect_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) : (emitReadMember stateCount tapeCount).effect values = Function.update (Function.update (Function.update (Function.update (Function.update (Function.update values Work.available (values Work.available + 3)) Work.reference₀ 0) Work.reference₁ 0) Work.temporary₀ 0) Work.temporary₁ 0) Work.temporary₂ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadMember_emitted_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) : (emitReadMember stateCount tapeCount).emitted values = List.flatMap CircuitCode.RawGate.encode [CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position)), CircuitCode.RawGate.copy (transitionCellRef stateCount tapeCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position) (values Work.symbolIndex)), { op := AndOrOp.and, input₀ := values Work.available, input₁ := values Work.available + 1, negated₀ := false, negated₁ := false }]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadMember_requires_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitReadMember stateCount tapeCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setReadFormulaLimit_effect_internal (values : BinaryValues WorkCount) : setReadFormulaLimit.effect values = Function.update values Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setReadFormulaLimit_emitted_internal (values : BinaryValues WorkCount) : setReadFormulaLimit.emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setReadFormulaLimit_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) : setReadFormulaLimit.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadIdentity_effect_internal (values : BinaryValues WorkCount) : emitReadIdentity.effect values = Function.update values Work.available (values Work.available + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadIdentity_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : emitReadIdentity.emitted values = (CircuitCode.RawGate.constant 0 false).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadIdentity_requires_internal (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : emitReadIdentity.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadConnector_effect_internal (values : BinaryValues WorkCount) : emitReadConnector.effect values = Function.update (Function.update values Work.available (values Work.available + 1)) Work.reference₁ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadConnector_emitted_internal (values : BinaryValues WorkCount) : emitReadConnector.emitted values = { op := AndOrOp.or, input₀ := values Work.reference₀, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadConnector_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (havailable : 1 ≤ values Work.available) (hemit : values Work.emitCounter = 0) : emitReadConnector.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadConnector_spaceBoundByWidth_internal {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (havailablePositive : ∀ (inputLength : ℕ), 1 ≤ values inputLength Work.available) (hreference₀ : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) (hreference₁ : ∀ (inputLength : ℕ), values inputLength Work.reference₁ ≤ width inputLength) : emitReadConnector.SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadNextConnector_effect_internal (values : BinaryValues WorkCount) : emitReadNextConnector.effect values = Function.update (Function.update (Function.update values Work.reference₀ (values Work.reference₀ - 3)) Work.available (values Work.available + 1)) Work.reference₁ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadNextConnector_emitted_internal (values : BinaryValues WorkCount) : emitReadNextConnector.emitted values = { op := AndOrOp.or, input₀ := values Work.reference₀ - 3, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadNextConnector_requires_internal (values : BinaryValues WorkCount) (hreference : 3 ≤ values Work.reference₀) (hcopy : values Work.copyCounter = 0) (havailable : 1 ≤ values Work.available) (hemit : values Work.emitCounter = 0) : emitReadNextConnector.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_spaceBoundByWidth_internal (stateCount tapeCount : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), ReadFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hfrontier : ∀ (inputLength : ℕ), values inputLength Work.available + (4 * (values inputLength Work.horizon + 1) + 1) ≤ width inputLength) (hheadCap : ∀ (inputLength position : ℕ), position ≤ values inputLength Work.horizon → transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) position + values inputLength Work.tapeIndex + values inputLength Work.horizon + 1 ≤ width inputLength) (hcellCap : ∀ (inputLength position : ℕ), position ≤ values inputLength Work.horizon → transitionCellRef stateCount tapeCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) position (values inputLength Work.symbolIndex) + (values inputLength Work.tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + tapeCount + values inputLength Work.tapeIndex + 4 ≤ width inputLength) : (emitReadFormula stateCount tapeCount).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_requires_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) : (emitReadFormula stateCount tapeCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_effect_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) : (emitReadFormula stateCount tapeCount).effect values = Function.update values Work.available (values Work.available + (4 * (values Work.horizon + 1) + 1))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_emitted_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) : (emitReadFormula stateCount tapeCount).emitted values = List.flatMap CircuitCode.RawGate.encode (readFormulaSchedule stateCount tapeCount (values Work.horizon) (values Work.configBase) (values Work.available) (values Work.tapeIndex) (values Work.symbolIndex))