This is a sub-milestone of %(2023Q3-Q4) Michelson-in-Rust, for the fully featured implementation phase.

This work will be addressed along with other topics, in a more vertical way.

Context

While we're using TZT to verify the implementation of the MIR interpreter, we cannot use the test suite to check the MIR type-checker since type-check failing tests are missing in TZT.

To check type-checking success, we can simply use the existing interpreter tests, since they are supposed to pass type-checking, and milestone %(2023Q3) MIR: add some missing interpretation tests to TZT will add missing interpreter tests in such a way that all instructions should be covered.

Thus, the goal of this milestone is to add a syntax to declare the result of a TZT test as a type-checking failure, and to implement at least one test for each Michelson instruction that should be rejected during type-checking.

Work break down

Total: 0/178 (0%) instructions with a type-check failing test.

• Propose a syntax to specify that a test should fail type-checking.
• Control structures.
• Stack manipulation.
• Arithmetic operations.
• Boolean operations.
• Operations on data structures.
• Operations on tickets.
• Cryptographic operations.
• Blockchain operations.