How to prove a side effect in a function

Question

I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and databases.

In this question I am wondering about a more middle-level proof, this time about transforming an object $f : A \to B$ with side effect $C$. Say I have as input a string $A$, and as output an Abstract Syntax Tree (AST) $B$. All of this happens in memory with a small string of say a few KB. Right now, ignoring all the details of the hardware implementation and all the details of any particular language.

I am wondering at a high level what it takes to prove something like this. Specifically I wanted to focus on side effects in this question. Say during the parse process, we create a global symbol table to store classes. Then as we are parsing through the code and we encounter the class, we add to the symbol table. So instead of $f : A \to B$, we really have:

\begin{align} f : A &\to B\\ &\downarrow\\ &C \end{align}

That is for the symbol table $C$ and AST output $B$. Somewhere in the function $f$ implementation there is another function $g : \{C,c\} \to C'$, which adds the new symbol $c$ to $C$.

What I would like to prove (in this question, just at a high level, some key points) is that the function generates the symbol table $C$, even though the output of the function is the AST $B$. In type theory, the proof for AST $B$ could possibly just be the sequence of type definitions and transformations, similar to Hoare Logic. But to prove that the function $f$ has side effect $C$ seems much harder/trickier.

It seems that you have to go and step through the algorithm one step at a time, and (assuming everything is strongly typed), figure out what the "current state" would look like at that point (of the whole program). Then you would compare your pattern (the assertion of the post-condition if it were Hoare Logic) with the current state of the program at that point, and see if it was a match. And see if that stayed true until the end of the function/algorithm. But this sort of seems like it's becoming Model Checking, which I only know the basics about, not sure if that is correct to assume though. Also, this one-step-at-a-time stepping through the algorithm seems like program simulation, so wondering if that is true or not or if simulation has a role here.

So I'm wondering, at a high level, what is required to prove that function $f$ generates a side effect $C$. As a specification, I would write "$f$ generates the symbol table $C$".