Decorated proofs for computational effects: States