x86 PUSH, POP instruction semantics

For Lvalue, ESP is applied after calculating ESP.
For Rvalue, ESP is applied before calculating ESP.

Therefore,

POP [esp]
::=
esp := esp0 + 4
[esp] = [esp0 + 4] := [esp0]

PUSH [esp]
::=
esp := esp0 - 4
[esp] = [esp0 - 4] := [esp0]

POP [esp+4]
::=
esp := esp0 + 4
[esp] = [esp0 + 4] := [esp + 4] = [esp0 + 4]
==> [esp0 + 4] = [esp0 + 4] => no change

PUSH [esp+4]
::=
esp := esp0 - 4
[esp] = [esp0 - 4] := [esp + 4] = [esp0 + 4]
==> [esp0 - 4] = [esp0 + 4]