Let's imagine (weird) protected mode environment setting with stack's segment address attribute 16 bits (this is possible because of B flag in stack descriptor) and code segment's address and operand size 32 bits (D flag in code descriptor).

What happens when opcode 0x50 (PUSH AX/EAX) is executed? Is the following pseudocode correct?

In other words, is it correct that high word of EAX rewrites the word stored on the stack last time (before the operation was executed)?

I was wrong, the stack pointer is decremented according to current operand-size attribute of the code segment (as the manual says). Now it makes sense - nothing is destroyed.