Arithmetic leaves for proof-carrying binary routines -- proof internals

theorem Complexity.BinaryRoutine.clear_sound_internal {n : ℕ} (idx : Fin n) : (clear idx).Sound

theorem Complexity.BinaryRoutine.addConst_sound_internal {n : ℕ} (idx : Fin n) (constant : ℕ) : (addConst idx constant).Sound

theorem Complexity.BinaryRoutine.set_sound_internal {n : ℕ} (idx : Fin n) (value : ℕ) : (set idx value).Sound

theorem Complexity.BinaryRoutine.add_sound_internal {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : (add srcIdx dstIdx counterIdx).Sound

theorem Complexity.BinaryRoutine.mulAdd_sound_internal {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) : (mulAdd leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).Sound

theorem Complexity.BinaryRoutine.evalPolynomial_sound_internal {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (p : Polynomial ℕ) : (evalPolynomial inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx p).Sound

theorem Complexity.BinaryRoutine.emitNatCode_sound_internal {n : ℕ} (counterIdx valueIdx : Fin n) : (emitNatCode counterIdx valueIdx).Sound

theorem Complexity.BinaryRoutine.emitRawGate_sound_internal {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx input₀Idx input₁Idx : Fin n) : (emitRawGate op negated₀ negated₁ emitCounterIdx input₀Idx input₁Idx).Sound