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.
Observe that $S$ has only one countable recursively saturated model.
For an elementary version of this argument: expand $S$ 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)$).
Show that any two models of $S$ are elementarily equivalent by an Ehrenfeucht–Fraïssé argument. Or, apply a ready-made EF argument: Gaifman's locality theorem.
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.