How to prove a side effect in a function
If the function has two outputs, a standard way to represent this is as a function $f: A \to (B \times C)$, i.e., $f$ outputs a pair of an AST and a symbol table.

If the function updates an existing symbol table, you could represent this as a function $f : (A \times C) \to (B \times C)$.  It takes as an input a pair of a string and a symbol table, and outputs a pair of an AST and an updated symbol table.

You could also read about monads, which are a way to structure and reason about side effects in a functional programming language.  They are notoriously challenging to understand.

You don't prove a side effect.  You can prove a fact about the possible side effects, but you need to state what you are claiming; a side effect isn't something that can be proven or not.  Similarly, you don't prove a function.  You can prove the correctness of a function, if you specify what correctness means for that particular function, but you don't prove the function.