What is the execution sequence of this Michelson code snippet

Question

I tried to get a better grip on michelson but found myself fail at a simple piece of michelson code. Is anyone willing to help on the logic of below code? Thanks a lot!

parameter (pair nat nat);
storage (pair nat nat);
code{
      CAR; UNPAIR;
      DUP; DIP { ADD };
      PAIR;
      NIL operation;
      PAIR};

It says "If called with the initial storage (Pair 0 0) and the parameter (Pair 15 9) then the final storage will be (Pair 15 24).", however I cannot think it through.

==========

My attempt:

1. CAR, take the parameter (15,9);
2. UNPAIR, gets it unpair meaning to separate the pair as two numbers 15 9; so that's 15:9:(0,0):[]
3. DUP, means 15:15:9:(0,0):[]
4. DIP, means protect the top stack,i.e. the 15. In plain language, that is, keep it there, don't do anything with it.
5. ADD, means take from the second left number 15, add all the numbers down to the bottom of the stack. (It seems illegal, as integer adds on pair)
6. Head gets exploded...

Reference: https://tezos.gitlab.io/michelson-reference/#instr-DIP

Answer 1

You can get a step-by-step trace of execution with the --trace-stack option of tezos-client. The following command:

tezos-client run script 'parameter (pair nat nat); storage (pair nat nat); code{ CAR; UNPAIR; DUP; DIP { ADD }; PAIR; NIL operation; PAIR};' on storage 'Pair 0 0' and input 'Pair 15 9' --trace-stack

results in

storage
  (Pair 15 24)
emitted operations

big_map diff

trace
  - location: 10 (remaining gas: 1039463 units remaining)
    [ (Pair (Pair 15 9) (Pair 0 0))      ]
  - location: 11 (remaining gas: 1039463 units remaining)
    [ (Pair 15 9)   @parameter ]
  - location: 14 (remaining gas: 1039462 units remaining)
    [ (Pair 15 9)   @parameter
      (Pair 15 9)   @parameter ]
  - location: 15 (remaining gas: 1039462 units remaining)
    [ 15    
      (Pair 15 9)   @parameter ]
  - location: 18 (remaining gas: 1039461 units remaining)
    [ 9      ]
  - location: 17 (remaining gas: 1039461 units remaining)
    [ 9      ]
  - location: 16 (remaining gas: 1039461 units remaining)
    [ 15    
      9      ]
  - location: -1 (remaining gas: 1039461 units remaining)
    [ 15    
      9      ]
  - location: 12 (remaining gas: 1039460 units remaining)
    [ 15    
      9      ]
  - location: 19 (remaining gas: 1039460 units remaining)
    [ 15    
      15    
      9      ]
  - location: 22 (remaining gas: 1039458 units remaining)
    [ 24     ]
  - location: 21 (remaining gas: 1039458 units remaining)
    [ 24     ]
  - location: 20 (remaining gas: 1039458 units remaining)
    [ 15    
      24     ]
  - location: 23 (remaining gas: 1039458 units remaining)
    [ (Pair 15 24)       ]
  - location: 24 (remaining gas: 1039457 units remaining)
    [ {}    
      (Pair 15 24)       ]
  - location: 26 (remaining gas: 1039457 units remaining)
    [ (Pair {} (Pair 15 24))     ]
  - location: -1 (remaining gas: 1039457 units remaining)

A more interactive trace execution is also available in the try-michelson online editor.