What is an assembly-level representation of pushl/popl %esp?

Question

I'm trying to understand the behavior of pushing and popping the stack pointer register. In AT&T:

pushl %esp

and

popl %esp

Note that they store the computed value back into %esp.

I'm considering these instructions independently, not in sequence. I know that the value stored in %esp is always the value before the increment/decrement, but how could I represent the behavior in assembly language? This is what I've come up with so far.

For pushl %esp (ignoring FLAGS and the effect on the temporary register):

movl %esp, %edx     1. save value of %esp
subl  $4, %esp      2. decrement stack pointer
movl %edx, (%esp)   3. store old value of %esp on top of stack

For popl %esp:

movl (%esp), %esp   You wouldn’t need the increment portion. 

Is this correct? If not, where am I going wrong?

Answer 1

As it says about push esp in Intel® 64 and IA-32 Architectures Developer's Manual: Combined Volumes (actually in vol.2, or HTML scrape at https://www.felixcloutier.com/x86/push):

The PUSH ESP instruction pushes the value of the ESP register as it existed before the instruction was executed. If a PUSH instruction uses a memory operand in which the ESP register is used for computing the operand address, the address of the operand is computed before the ESP register is decremented.

And as regards to pop esp (https://www.felixcloutier.com/x86/pop):

The POP ESP instruction increments the stack pointer (ESP) before data at the old top of stack is written into the destination.

and pop 16(%esp)

If the ESP register is used as a base register for addressing a destination operand in memory, the POP instruction computes the effective address of the operand after it increments the ESP register.

So yes, your pseudo-code is correct except for modifying FLAGS and %edx.