If you implement an evaluator for the terms of a language $A$ in a total system $B$, and you have furthermore proven that your evaluator is correct, that is for every $t$ well-typed in $A$,
$$\mathrm{eval}(t) \simeq_A t $$
where $\simeq_A$ is the equality in $A$, then you have only shown that $\simeq_A$ is decidable.
If furthermore $\simeq_A$ naturally leads to a notion of reduction $\rightarrow_A$, and $\mathrm{eval}(t)$ is always in normal form, then you have proven that every term $t$ in $A$ is equivalent to a term in normal form.
This is enough for consistency of $A$ but is not equivalent to weak normalization, unless $\rightarrow_A$ is furthermore church-rosser!
This is essentially the approach taken by normalization by evaluation.
A proof of weak normalization in a constructive logic naturally leads to an evaluator, as every $\forall\exists$ statement leads to an algorithm (correct by construction).
There is a nice article by Ulrich Berger, Program extraction from normalization proofs, which implements this idea for simply typed $\lambda$-calculus.
For your second question, here is a counter example. Consider the language $A$ to have only two terms, $\Delta$ and $\bot$, with the reduction rules
$$\Delta\rightarrow \Delta $$
$$\Delta\rightarrow \bot $$
Feel free to add types if you like. The computation rules are weakly normalizing and confluent.
In Coq, you might write the eval function thus:
Fixpoint eval (t : A) : A :=
match t with
| Delta => Bottom
| Bottom => Bottom
It's not too hard to prove that if $t\leftrightarrow^* u$ then eval(t) = eval(u). Coq's reduction can be taken to be non-deterministic, in which case you have a counter-example to the SN "inheritance" that you expect.
