motoko-san: Update README.md

[int-index]

Update the README.md to describe features implemented by Serokell for Milestone 1 and Milestone 2

Milestone 1

1. Arguments and return values
2. The return statement, early exit
3. Loop invariants
4. Method calls in let/var declarations, assignments
5. The Nat data type (translated to Int)
6. Arrays of primitive types
7. Monomorphisation of private methods (new pass: prep.ml)
8. Assertions on the result (the var:return syntax)

Milestone 2

1. Tuples of primitive types, matching on tuples in let
2. Option types
3. Variant types using the ADT Viper plugin (nominative typing, generics supported)
4. switch statements to match on tuples, options, variants

[GoPavel]

LGTM
Only one thing: I think that it's useful to mention that loop invariant should hold before and after loop. Sometimes you might come up with invariant that holds only after at least one iteration and be confused.

[aterga]

Idea: We could alternatively use an uninterpreted function eq(x: Tuple, y:: Tuple) that is axiomatized as

forall x, y :: eq(x, y) <==> x.0 == y.0 && x.1 == y.1

etc.

This goes, however, into the direction of program-specific preamble generation (as we don't know which tuple types we would need to compare for equality), which is not what we're currently doing.

[crusso]

@aterga, I'm not sure why your comment is relevant here - I think they are talking about type equality being structural, not value equality.

[aterga]

IIUC, they are saying "Motoko equality is structural, but we translate it to Viper using ==, which reduces the completeness of the translation." Did I get it wrongly?

If not, then I'm merely suggesting that there could be a straightforward, yet more complete translation. Although I'm not suggesting that it's implemented it in the scope of the current Serokell grant.

[int-index]

Maybe I phrased it poorly, but I meant to talk about type equality here, as @crusso points out.

[aterga]

Do you think this is conceptually harder than what we do for Arrays, or about the same complexity?

[int-index]

If we find the right axioms, it should be possible, but we won't know until we try. For arrays there was an example in Viper's documentation, a hashmap would require more tinkering

[aterga]

Thanks, this is just my curiosity.

We do have some drafts for translating HashMap from Motoko to Viper from a very long time ago (even before Motoko-san was created). But let's keep working on concrete examples, and I don't think we need to add anything with HashMaps into this project (there's enough interesting canisters with arrays, ADTs and things that we already support — we should utilize those before expanding).

[aterga]

Would the following work, too?

      if (length == 0) {
        return a;   // conditional early exit
      };
      a     // normal exit

[int-index]

We could make it work, but at the moment it doesn't.

[crusso]

Suggested change

	nominative equality of variants, so type inference is not reliable:
	nominal equality of variants, so type inference is not reliable:

I guess we will just have to live with this fundamental difference between Viper and Motoko. @aterga is there any way to teach Viper about structural type equivalence (and subtyping)?

[aterga]

Yes.

The Viper language is designed to be simple, and to allow modeling programs in many different (imperative) languages. So while we cannot translate many statement from Motoko into Viper 1:1, of course there are multiple ways we could model those cases in Viper and still support them.

That is where I was going with this comment, btw: #19 (comment)

[GoPavel]

For example Prusti encode all Rust types as predicates. I think in that approach subtyping is not a big deal, but there will be other drawbacks e.g. folding/unfolding Viper isorecursive predicates.

[aterga]

Correct. I would not recommend using separation logic predicates in Motoko-san, as they would require generating ghost statements to fold / unfold the definitions, and they are limited to tree structures (so, e.g., an array cannot be expressed this way).

[aterga]

We could perhaps remove this line now

[int-index]

We would first have to add support for nested pattern matching, I imagine?

[aterga]

Indeed, but then the line could be "Supporting general pattern-matching is conceptually simple." :-)

This is a very, very minor issue, so feel free to ignore

[GoPavel]

We can take it into account when we will update README after the 3rd Milestone

[GoPavel]

Done