Max stack depth of a Michelson program?

Question

Is it possible to determine an upper bound for the (runtime) max stack depth that a given Michelson program will use?

I'm thinking here in terms of static analysis of the program. So, 'given a Michelson program X, I can guarantee X will use a stack of size N elements or less throughout the lifetime of the program'.

Answer 1

Yes, that is possible, and in fact, trivial. The type system of Michelson ensures that the type (including the depth) of the stack is statically known at each program point.

Consider loops for instance. The type system ensures that the body of loops must have a fixed type (and depth by extension) at the beginning and the end of each iteration. In other words, we could not write an infinite loop that just pushes values. Similarly, the type system ensures that each branch of conditionals (IF ...) has the same final type.

So the static analysis that you suggest is already implemented by Michelson's typechecker. Consider the program test.tz:

parameter unit ;
storage unit;
code { CDR;
       PUSH nat 1;
       PUSH nat 2;
       PUSH nat 3;
       DROP; DROP; DROP;
       NIL operation;
       PAIR;
     };

We can use tezos-client to typecheck the program in this way, passing the flag -v to get an output where each program point is annotated with the type at that location:

$ tezos-client typecheck script test.tz -v
Well typed
Gas remaining: 1039990.990 units remaining
{ parameter unit ;
  storage unit ;
  code { /* [ pair (unit @parameter) (unit @storage) ] */
         CDR
         /* [ @storage unit ] */ ;
         PUSH nat 1
         /* [ nat : @storage unit ] */ ;
         PUSH nat 2
         /* [ nat : nat : @storage unit ] */ ;
         PUSH nat 3
         /* [ nat : nat : nat : @storage unit ] */ ;
         DROP
         /* [ nat : nat : @storage unit ] */ ;
         DROP
         /* [ nat : @storage unit ] */ ;
         DROP
         /* [ @storage unit ] */ ;
         NIL operation
         /* [ list operation : @storage unit ] */ ;
         PAIR
         /* [ pair (list operation) (unit @storage) ] */ } }

The typechecker reports the type of the stack, including its depth at each program point. For instance, we see that after pushing the 3 nats on top of the original storage, we indeed have the stack of 4 elements:

         /* [ nat : nat : nat : @storage unit ] */ ;