[DMS-34] motoko-san: add basic support for Nat

[int-index]

New features:

• translate Nat to Int

New test cases:

• test/viper/nats.mo

Future work: encode in Viper that Nats are non-negative.

[GoPavel]

I think this is sound translation because the translation is performing after typechecking.
Probably a good next step is to add auto deducing precondition (easy) and loop invariant (a bit harder).
Example:

private func foo(x: Nat)

translated into

method foo(x: Int)
  requries x >= 0

and

var i : Nat = 0
while (i < arr.size()) {
     // assert:invariant i >= 0  // auto inferred 
    arr[i] := i
    i := i + 1
}

I think this is useful general scheme (kinda refinement types). It will help support in the future int8 int16 and so on.

WDYT?
Probably we can postpone it for a next milestone

[GoPavel]

Except comment above LGTM

[int-index]

method foo(x: Int)
  requries x >= 0

kinda refinement types

Yeah, I've been thinking along these lines too. n : Nat is basically { n : Int | n >= 0 }, so we could encode this refinement type with predicates in Viper.

For Nat8, Nat16, etc, it's more tricky because arithmetic operations can overflow, so we'd have to translate a + b to (a + b) % 256 and (a + b) % 65536 respectively. Signed overflow (Int8, Int16, etc) is even trickier.

[int-index]

Probably we can postpone it for a next milestone

Yes, let's postpone because it would take some effort to get it right. For example:

• What happens when we have an array of Nat? That is, how should the requires clause look for ns : [Nat]?
• What happens if we emit ensures $Res >= 0 but the solver can't prove it?
• How do we track those predicates in the translator? How do we know that a loop invariant is needed?

We could probably solve such issues, but let's get some basic support for Nat first and enhance it later.