Proving correctness of an exponentiation routine
A standard approach to proving correctness of a program involving a loop is to use a loop invariant. Loop invariant $P(j)$ is a statement indexed by the iteration number $j$ (or a parameter related to the iteration number) that asserts a certain mathematical relationship between some variables appearing in your code. Proving $P(j)$ is true for all $j$ is typically done by induction. You show that $P(0)$ is true, i.e., the loop invariant is true prior to the beginning of the loop. You show that $P(i)$ is true implies $P(i+1)$ is true. Then you can conclude that the statement $P(n)$ (or $P(n+1)$) must be true, which asserts the relationship between the variables of interest that is directly relevant to the correctness of the algorithm. Note that if $j$ is some parameter related to the iteration number (e.g., $j$ could be $n$ minus the iteration number), the starting point and the direction of the induction might be different. Finding the right loop invariant is usually the hardest part.

Let's find a loop invariant for your code. Note that you overwrite the variable $a$ inside the loop. This means that I cannot use $a$ in the loop invariant to refer to the original input, but I'd like to. Therefore I introduce a new letter $\alpha$ to refer to the value of $a$ that is passed to the function, i.e., the first input. The rest of the variables are exactly as in your code. Our loop invariant $P(i)$ will be indexed by the variable $i$, which is related to the iteration number, but starts with $n$ and decreases to $0$ similar to what I wrote about above. Define the following loop invariant:
$$P(i) \text{ is true if and only if } x*a^i == \alpha^n$$
Clearly, at the beginning you have $x=1$,  $a=\alpha$, and $i = n$, so $P(n)$ is true. I leave proving the inductive step to you (note you will be proving $P(n)$ is true implies $P(\lfloor n/2 \rfloor)$ is true, so this induction skips over lots of values, but it's okay - why?). When the algorithm terminates you have $P(0)$, which asserts $x*a^0 = \alpha^n$, i.e., $x = \alpha^n$, which is what you needed to prove.