How to apply Operational Semantics to this function

Question

Say I have a function like this:

function colorize(integer) {
  var hex = '#'

  if (integer > 1) hex += 'ff'
  else hex += '00'
  if (integer < 100) hex += 'aa'
  else hex += 'bb'
  if (integer > 10) hex += '11'
  else hex += '22'

  return hex
}

It returns CSS hex colors, not named colors or rgb(...) values or anything else. For now we can ignore the low-level / platform specific details of JavaScript and hardware and just deal with this abstractly as if it was in a perfect environment.

The goal is to use small step operational semantics to prove that it returns a CSS hex color. If it requires too much initialization to do the proof, then assume the initialization is already handled so all that's focused on is the specific function and its implementation.

From my understanding this means we would have some rule for var, =, if, ===, +=, and return. In addition, there is sort of a trace, since it is modifying the value in memory step by step.

From my understanding this would involve using the operational semantics configuration evaluation〈a, σ〉→〈a', σ'〉like:

〈=, σ〉→〈=, σ'[hex ↦ #]〉
   →
〈if (e) x else y, σ〉→〈...〉
   →
   ...

I am not sure how to:

1. Actually write the configurations out.
2. Write out the sequence of the evaluations.
3. Write a proof that the output will be a hex string such as #00aa22 if given 0 for example.

I was wondering if one could point me in the right direction on how to solve this. Basically:

1. What some configurations look like using this function as an example.
2. What a sequence of the evaluations (or trace) looks like.
3. What a proof would entail (not the actual proof as I imagine there will be lots of steps), maybe just the first few steps of the proof.

Thank you very much for your help.