There are several ways how to prove the completeness of this theory (let me call it $S$) without choice:
Prove in a purely syntactic way (by induction on the complexity of a formula) that $S$ has quantifier elimination.
Expand the theory to a theory $S'$ with countably many constants $\{c_n:n\in\omega\}$, and axioms that $c_n$ is not reachable from $c_m$ in finitely many steps for $n\ne m$. Using the compactness theorem, you easily show that if $\phi$ is consistent with $S$, it is consistent with $S'$, hence it holds in a countable model of $S'$ (this needs no choice as the language is countable). But reducts of countable models of $S'$ in the original language are all isomorphic (they consist of countably many copies of $(\mathbb Z,s)$).
The completeness of $S$ is an arithmetical ($\Pi_2$) statement. Thus, you can just prove the result in ZFC, and use the conservativity of ZFC over ZF for arithmetical sentences.