Define a dyadic logarithm of an odd dyadic integer $a$ as the limit of $\frac{a^z-1}{z}$ for $z\to0$ in the dyadic sense. I can prove, I'm assuming it's also well known, that dyadic exponentiation makes sense. (This is not true in general for p-adic integers.) A definition that works is to define $a^z$ as the limit of $a_n^{z_m}$ where $a_n$ is a sequence of positive integers that converges to $a$ in the dyadic sense and similarly $z_m \to z$.
I also have a proof that what I'm calling the dyadic logarithm exists and has some algebraic properties, such as the dyadic logarithm of a product is the sum of the dyadic logarithms. The dyadic logarithm of $-1$ and $1$ are both $0$.
I wonder if there are any known properties or uses of this function. Maybe cryptographic, or fast binary multiplication? Or perhaps it's used to prove some number theoretic result?
Yes, this is rather well known, especially to folks in the formal-group racket.
You’re dealing with the formal group $\mathscr M(x,y)=x+y+xy=(1+x)(1+y)-1$, the formal group associated to multiplication, or in fancier (but perhaps rather sloppy) language, the formal group of the multiplicative group scheme $\mathbf G_{\mathrm m}$.
I hope you see that my formula for $\mathscr M$ is just a recoordinatization of multiplication, with the neutral element moved from $1$ to $0$. Your construction of the logarithm, which is a homomorphism from $\mathscr M$ to the additive formal group $\mathscr A(x,y)=x+y$, is perfect. In fact, it can be expressed by the $p$-adically convergent power series, $-\sum_1^\infty(-x)^n/n$, which you know from Calculus, but with the $1+x$ replaced by $x$. A wonderful thing about it is that it remains convergent whenever you substitute for $x$ something that’s closer to $0$ than $1$ is: in technical terms, $\log(a)$ is convergent for all $a$ with $|a|_p<1$, equivalently $v_p(a)>0$. So, for instance, you can plug $\sqrt2$ in for $a$ in your $2$-adic logarithm, and get a good value.
Only one other thing to say for now, and that’s that you don’t need to consider all $z\to0$ in your formula, you can just take powers of $2$ (powers of $p$ in the general case).