In the article 'A natural model of the multiverse axioms' by Gitman and Hamkins, they give the following lemma:
Lemma 5. If ZFC is consistent, then there are $2^{ℵ_0}$ many pairwise nonisomorphic countable computably saturated models of ZFC. Every real is in the standard system of such a model.
Here I understand a real a subset of $\mathbb{N}$, but then, not every real can be coded by a set in a countable model $M$, since two sets which codes different reals should be different. I also have a trouble to understand the proof of this article. It says
(...) For any real $x$, one can ensure that the type expressing that $x$ is coded is realized.
but the type $$ p(y) = \{\ulcorner y\subset \omega\urcorner \}\cup \{\ulcorner S^n0\in y\urcorner : n\in x\} \cup \{\ulcorner S^n0\notin y\urcorner : n\notin x\},$$ which says $y$ codes $x$, is not necessarily computable unless $x$ is computable. I feel there is a misunderstanding somewhere, and I can't find what makes a trouble. I would appropriate someone's help.