Motoko-san: Second Iteration

Showcase
1

Project highlights

I’m happy to present the next iteration of the Motoko-san project, which is a formal, automated, code-level verifier for the Motoko smart contract language. It was announced as a prototype early last year, and our Serokell team had the opportunity to mature it during a grand for RFP-6.

We have extended supported subset of Motoko quite a bit (e.g. by adding array and variant types) along with the annotation syntax (e.g. ∀ quantifiers and loop invariants). So now Motoko-san can check a functional specification of small canisters like ToDo Manager. You can find a short example below and the full version with all annotations here.

Short Changelog

A short list what was supported:

  • Build-in types: arrays, tuples, option, variants, records (immut), nat
  • Motoko syntax: return values, patter matching, polymorphic private functions
  • Annotation syntax: quantifiers, loop invariant, Ret for return value, function post-conditions

Example

This is a small simplified piece of our todo.mo showcase. Image that we want an actor to manage collection of ToDo tasks stored in an array. Each ToDo has an id, a description and a state encoded via enum State.

We only focus on one function: addTodo. Its implementation is quite simple, but though it could be buggy. So we annotate the function by postconditions and Motoko-san will automatically check by analysing the function body.

For example, if we forgot to increament num then the postcondition num == old(num) + 1 will be violated and Motoko-san will report about it.

// @verify
import Prim "mo:⛔";
actor ToDoManager {
  public type State = { #TODO; #DONE };
  type ToDo =  { id: Nat; desc: Text; state: State };

  var todos : [var ToDo] = [var ];
  var num : Nat = 0;

  // actor-level invariant
  assert:invariant 0 <= num and num <= todos.size();

  public func addTodo(description : Text) : async Nat {
    // functional specification:
    // counter is increased
    assert:return num == (old(num)) + 1;
    // new task is added
    assert:return todos[num-1] == ({ id = Prim.Ret<Nat>(); desc = description; state = #TODO });
    // previous tasks are not affected
    assert:return Prim.forall<Nat>(func i =
       (0 <= i and i < num-1 implies todos[i] == (old(todos[i]))));
    // postcondition on return value
    assert:return Prim.Ret<Nat>() == (old(num));
    todos[num] := { id = num; desc = description; state = #TODO };
    num += 1;
    return id;
  };
}

How to install

Soon our PR will be merged and all new features will be available in the Motoko-san VS Code extension.

If you want to try it out right now, you can follow our debug workflow via debug workaround or build our fork of the motoko compiler locally and run:

cd motoko
nix-shell
moc --package base test/viper/pkg/base --viper FILE > file.vpr

Command above generate file.vpr file that can be investigated via Viper VS Code extension. Motoko-san extention do it automatically and propagate errors back highlighting violated annotations.

Resources

Future plans

We will not give the full list of current limitations and uncovered features here (see README for that), but we believe that Motoko-san will continue to grow though the efforts of the Dfinity community and will help keep its members be safe from bugs.

4 Likes
2

Awesome, this looks really cool! But I have a question about the examples: can they be expressed without importing the Prim module? I would really, really, really, really, really not showcase code that encourages everybody to import that module. It is a compiler-internal interface, subject to change, potentially unsafe, intentionally undocumented, and its funny URL was meant to indicate that it should not be accessed in user code. I wish we had done our homework at the time and never exposed it in the first place.

3

I think Prim is just used to separate the namespace for specification-related keywords. This way, users in non-viper mode can still declare, e.g., a local variable called forall. But if Prim isn’t a good module to use for this purpose, it could be changed to any other built-in module, I think.

How about

import MotokoSan "Spec";
...
Spec.forall ...

Wdyt @claudio ?

4

I agree that using Prim is suboptimal because it just encourages more abuse of the prim module, but the syntax of assertions is fairly provisional and I’m sure we can use some other mechanism in the future.

I don’t think it’'s a showstopper to just showcase what’s possible.

1 Like