K-Michelson: a Case Study on Formal, Executable Language Specification

Project Updates
1

Hello again! This is Stephen Skeirik from Runtime Verification.

Some time ago, we introduced K-Michelson: a formal verification framework for Michelson in this post. Today, I’d like to give some brief updates on progress we have made:

  1. We added native support for most Michelson macros, even the old ones. This means tests like the following will run:

    code { DIIP { PUSH int 1 ; ADD } } ;
input { Stack_elt int 3 ; Stack_elt int 4 ; Stack_elt int 5 } ;
output { Stack_elt int 3 ; Stack_elt int 4 ; Stack_elt int 6 }

    You did know about the DIIP macro, right?

  2. We added support for reasoning about more symbolic data structures including symbolic map and lambda. This lets us check that symbolic map updates work as expected. A small example:

    # Map Update Test
#
# Check that if:
#   M2 == M1 [ K <- V1 ]
# Then:
#   M2 [ K ] == V1
#
input { Stack_elt int $K ; Stack_elt (option int) $V1 ; Stack_elt (map int int) $M1 } ;
code { UPDATE } ;
output { Stack_elt (map int int) $M2 } ;
postcondition {
#
# Postcondition unwraps two optional values requiring two IF_NONEs
# We have 4 cases (represented graphically):
# { None    - None } => True  { None    - Some V2 } => True
# { Some V1 - None } => False { Some V1 - Some V2 } => V1 =? V2
#
  { PUSH (option int) $V1 ;
                  IF_NONE { PUSH (map int int) $M2 ; PUSH int $K ; GET ; IF_NONE { PUSH bool True  } { PUSH bool False } }
                          { PUSH (map int int) $M2 ; PUSH int $K ; GET ; IF_NONE { PUSH bool False } { COMPARE ; EQ    } }
  }
}

    This example uses a new feature of our tool, symbolic variables, represented by the syntax $VAR. What happens is that symbolic variables bound in our input stack or expected output stack remain accessible inside the postcondition clause so that we can perform computation on them.

  3. We have removed lots of legacy code and updated our documentation. This makes it easier to get started and to contribute.

We have more updates planned in the near future—continued improvements to our documentation, making our syntax more consistent with upstream, and further refinements to our tooling to increase the range of programs that we can reason about.

I recently wrote a small blog post about our overall vision at Runtime Verification and how that applies to K-Michelson. Feel free to check it out!

Finally, if this kind of thing interests you, our GitHub repo is always a click away.

4 Likes