 Solution

Let expr(e) generate postfix code that evaluates a program expression once, leaving one value above an otherwise unchanged evaluation stack. Let stmt(s) preserve the evaluation stack's height. Use EQ to pop two integers and push their Boolean equality result; JZ L pops that result and jumps to L when it is false. JMP is unconditional. All labels returned by fresh() are distinct, including labels inside recursively generated bodies.

generateCase(Case(control, arms)):
    done := fresh()
    emit expr(control)
    for (labelExpression, body) in arms, in source order:
        next := fresh()
        emit DUP
        emit expr(labelExpression)
        emit EQ
        emit JZ next
        emit POP
        emit stmt(body)
        emit JMP done
        emit LABEL next
    emit POP
    emit LABEL done

To verify the stack invariant, write the incoming evaluation stack as $sigma$. Immediately before any label test it is $sigma,v$, where $v$ is the controlling value. DUP, evaluation of the label with value $w$, and EQ change this to $sigma,v,[v=w]$. JZ removes the Boolean. On failure the surviving $v$ is available for the next label; on success POP removes it before the body runs. The body therefore starts and ends with $sigma$ and jumps past every remaining label. If every label fails, the final POP restores $sigma$.

The controlling expression is evaluated once, each reached label is evaluated once, and no later label or arm is evaluated after a match. Keeping $v$ on the evaluation stack also preserves its original value if a label evaluation has a side effect that changes a variable appearing in the controlling program expression. A nested Case uses the same stack invariant relative to whatever stack it receives. The concise contract is