From 645988cf71cf0820c00030452a657ab95331cc76 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Wed, 24 Apr 2024 23:50:55 +0300
Subject: [PATCH] motoko-san: add basic support for Nat

New features:
* translate Nat to Int

New test cases:
* test/viper/nats.mo

Future work: encode in Viper that Nats are non-negative.
---
 src/viper/trans.ml            |  7 ++--
 test/viper/nats.mo            | 27 +++++++++++++++
 test/viper/ok/nats.silicon.ok |  1 +
 test/viper/ok/nats.vpr.ok     | 65 +++++++++++++++++++++++++++++++++++
 4 files changed, 97 insertions(+), 3 deletions(-)
 create mode 100644 test/viper/nats.mo
 create mode 100644 test/viper/ok/nats.silicon.ok
 create mode 100644 test/viper/ok/nats.vpr.ok

diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index db56f141888..562e9dfd2cf 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -485,6 +485,8 @@ and exp ctxt e =
        !!(BoolLitE b)
     | M.IntLit i ->
        !!(IntLitE i)
+    | M.NatLit i ->
+       !!(IntLitE i)
     | _ ->
        unsupported e.at (Arrange.exp e)
     end
@@ -526,9 +528,7 @@ and rets t_opt =
     (match T.normalize t.note with
      | T.Tup [] -> []
      | T.Async (T.Fut, _, _) -> []
-     | T.Prim T.Int  -> [(!!! (Source.no_region) "$Res", !!! (Source.no_region) IntT)]
-     | T.Prim T.Bool -> [(!!! (Source.no_region) "$Res", !!! (Source.no_region) BoolT)]
-     | _ -> unsupported t.at (Arrange.typ t)
+     | typ -> [(!!! (Source.no_region) "$Res", tr_typ typ)]
     )
 
 and id id = { it = id.it; at = id.at; note = NoInfo }
@@ -540,5 +540,6 @@ and tr_typ typ =
 and tr_typ' typ =
   match T.normalize typ with
   | T.Prim T.Int -> IntT
+  | T.Prim T.Nat -> IntT    (* Viper has no native support for Nat, so translate to Int *)
   | T.Prim T.Bool -> BoolT
   | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ (T.normalize typ))
diff --git a/test/viper/nats.mo b/test/viper/nats.mo
new file mode 100644
index 00000000000..0c4af629561
--- /dev/null
+++ b/test/viper/nats.mo
@@ -0,0 +1,27 @@
+// @verify
+
+actor Nats {
+
+  var x = 42 : Nat;
+
+  public func getZero() : async Nat {
+    return 0;
+  };
+
+  public func getX() : async Nat {
+    return x;
+  };
+
+  public func double() : async () {
+    x := x * 2;
+  };
+
+  public func natToInt(n : Nat) : async Int {
+    return n;
+  };
+
+  public func add(n : Nat, m : Int) : async Int {
+    return n + m;
+  };
+
+};
diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok
new file mode 100644
index 00000000000..1671de8e2f8
--- /dev/null
+++ b/test/viper/ok/nats.silicon.ok
@@ -0,0 +1 @@
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@2.1)
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
new file mode 100644
index 00000000000..472e810081c
--- /dev/null
+++ b/test/viper/ok/nats.vpr.ok
@@ -0,0 +1,65 @@
+define $Perm($Self) ((true && acc(($Self).x,write)))
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).x := 42 
+    }
+field x: Int
+method getZero($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := 0
+      goto $Ret
+      label $Ret 
+    }
+method getX($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := ($Self).x
+      goto $Ret
+      label $Ret 
+    }
+method double($Self: Ref)
+    
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).x := (($Self).x * 2)
+      label $Ret 
+    }
+method natToInt($Self: Ref, n: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := n
+      goto $Ret
+      label $Ret 
+    }
+method add($Self: Ref, n: Int, m: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := (n + m)
+      goto $Ret
+      label $Ret 
+    }