The problem of interest to the OP is not determining the truth value of sentences in Presburger arithmetic (that is, sentences using addition, equations/inequal

The problem of interest to the OP is not determining the truth value of sentences in Presburger arithmetic (that is, sentences using addition, equations/inequalities, Boolean operations, and the quantifiers "There exists an integer such that" and "For all integers, it is the case that"), which, although algorithmically decidable, is nonetheless in general very computationally taxing (the time to compute whether such a sentence is true or false is doubly exponential in the size of the sentence). Rather, the OP is simply interested in carrying out arithmetic calculations of a sort which are trivially computable (after all, the inputs the OP is dealing with are the very programs which would compute the answer!), but notes that one can in a principled way transform naive specifications of these computations (including loops like "Do this a million times") into faster methods of attaining the same answer (by thinking of such loops as matrix exponentiations and then using quick, rather than naive, exponentiation).