WIP: Adding protocol specific operations

This branch adds the missing operations in the grammar and provide a semantics for them.

To do so, the typing and semantics rules will need to carry the protocol context P.

This is a continuation of !5 (closed).