better error detection in mutez operations

docs/user_doc/print.html

@@ -463,7 +463,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 stack:
 |==================================================================================================|
 |                                                                                         @storage |
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |--------------------------------------------------------------------------------------------------|
 |                                                                                          @amount |
@@ -699,7 +699,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 running test script...
 stack:
 |==================================================================================================|
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 
@@ -817,7 +817,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 running test script...
 stack:
 |==================================================================================================|
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 
@@ -939,7 +939,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 running test script...
 stack:
 |==================================================================================================|
-| 1                                                                                                |
+| 1p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 

docs/user_doc/testing/anonymous.html

@@ -246,7 +246,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 running test script...
 stack:
 |==================================================================================================|
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 

docs/user_doc/testing/contracts.html

@@ -212,7 +212,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 stack:
 |==================================================================================================|
 |                                                                                         @storage |
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |--------------------------------------------------------------------------------------------------|
 |                                                                                          @amount |

docs/user_doc/testing/inspection.html

@@ -233,7 +233,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 running test script...
 stack:
 |==================================================================================================|
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 

docs/user_doc/testing/transfers.html

@@ -250,7 +250,7 @@ <h1 class="menu-title">Techelson User Documentation</h1>
 running test script...
 stack:
 |==================================================================================================|
-| 1                                                                                                |
+| 1p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 

src/1_base/exc.ml

@@ -20,13 +20,26 @@ module Protocol = struct
     | Failure of string
     | TooPoor of string * string * Int64.t
     | MutezOvrflw of string
+    | MutezUdrflw of string
+    | DivZero of string
     | Tezos of string
 
     let fmt (fmt : formatter) (self : t) : unit =
         match self with
         | Failure blah -> fprintf fmt "Failure on value %s" blah
         | Tezos blah -> fprintf fmt "%s" blah
-        | MutezOvrflw blah -> fprintf fmt "mutez operation overflow: %s" blah
+        | MutezOvrflw blah -> (
+            fprintf fmt "mutez operation overflow";
+            if blah <> "" then fprintf fmt ": %s" blah
+        )
+        | MutezUdrflw blah -> (
+            fprintf fmt "mutez operation underflow";
+            if blah <> "" then fprintf fmt ": %s" blah
+        )
+        | DivZero blah -> (
+            fprintf fmt "division by zero";
+            if blah <> "" then fprintf fmt ": %s" blah
+        )
         | TooPoor (src, tgt, mutez) ->
             fprintf fmt
                 "@[<hov>insufficient balance to process transaction of %s mutez"
@@ -62,6 +75,12 @@ module Throw = struct
 
     let mutez_overflow (blah : string) : 'a =
         Exc (Protocol (Protocol.MutezOvrflw blah)) |> raise
+
+    let mutez_underflow (blah : string) : 'a =
+        Exc (Protocol (Protocol.MutezUdrflw blah)) |> raise
+
+    let div_zero (blah : string) : 'a =
+        Exc (Protocol (Protocol.DivZero blah)) |> raise
 end
 
 let rec fmt (fmtt : formatter) (e : exn) : unit =

src/1_base/exc.mli

@@ -38,6 +38,13 @@ module Protocol : sig
 
         Can happen either during a transfer or during operations on mutez.
     *)
+    | MutezUdrflw of string
+    (** Mutez underflow.
+
+        Can happen either during a transfer or during operations on mutez.
+    *)
+    | DivZero of string
+    (** Division by zero. *)
     | Tezos of string
     (** Something went wrong in the protocol.
 
@@ -79,6 +86,12 @@ module Throw : sig
 
     (** Raises a mutez overflow error. *)
     val mutez_overflow : string -> 'a
+
+    (** Raises a mutez underflow error. *)
+    val mutez_underflow : string -> 'a
+
+    (** Raises a division by zero error. *)
+    val div_zero : string -> 'a
 end
 
 (** Raises an exception from a single trace frame. *)

src/4_theory/bigArith.ml

@@ -28,6 +28,8 @@ end
 module BNat = struct
     include BigInt
 
+    let fmt fmt n = fprintf fmt "%ap" Z.pp_print n
+
     let of_string (s : string) : t =
         let nat = Z.of_string s in
         if Z.geq nat Z.zero then nat

src/4_theory/dune

@@ -6,7 +6,8 @@
     (libraries
         base
         parse
-        zarith
         ptime
+        stdint
+        zarith
     )
 )

src/4_theory/make.ml

@@ -21,69 +21,92 @@ module Theory (
         include P
 
         module Tez = struct
-            type t = Int64.t
+            open Stdint
+            type t = Uint64.t
             type nat = Nat.t
 
             let to_string (t : t) : string =
-                Int64.to_string t
+                Uint64.to_string t
 
             let fmt (fmt : formatter) (t : t) : unit =
-                Int64.to_string t |> fprintf fmt "%sutz"
+                Uint64.to_string t |> fprintf fmt "%sutz"
 
             let to_nat (t : t) : nat =
-                (fun () -> Int64.to_string t |> Nat.of_string)
+                (fun () -> Uint64.to_string t |> Nat.of_string)
                 |> Exc.erase_err (
                     fun () -> asprintf "cannot convert %a to nat" fmt t
                 )
             let of_nat (n : nat) : t =
-                (fun () -> Nat.to_string n |> Int64.of_string)
+                (fun () -> Nat.to_string n |> Uint64.of_string)
                 |> Exc.chain_err (
                     fun () -> asprintf "cannot convert %a to mutez" Nat.fmt n
                 )
 
             let of_string (s : string) : t =
-                (fun () -> Int64.of_string s)
+                (fun () -> Uint64.of_string s)
                 |> Exc.erase_err (
-                    fun () -> sprintf "cannot convert string `%s` to tezos" s
+                    fun () -> sprintf "cannot convert string `%s` to mutez" s
                 )
-            let of_native (n : Int64.t) : t = n
-            let to_native (t : t) : Int64.t = t
+            let of_native (n : Int64.t) : t = Uint64.of_int64 n
+            let to_native (t : t) : Int64.t = Uint64.to_int64 t
 
             let add (t_1 : t) (t_2 : t) : t =
-                let overflow_if_gt_zero = Int64.sub Int64.max_int t_1 |> Int64.compare t_2 in
-                if overflow_if_gt_zero <= 0 then
-                    Int64.add t_1 t_2
-                else (
-                    asprintf "while adding %a and %a" fmt t_1 fmt t_2
-                    |> Exc.Throw.mutez_overflow
+                (fun () ->
+                    let overflow_if_gt_zero =
+                        Uint64.sub Uint64.max_int t_1 |> Uint64.compare t_2
+                    in
+                    if overflow_if_gt_zero <= 0
+                    then Uint64.add t_1 t_2
+                    else Exc.Throw.mutez_overflow ""
+                )
+                |> Exc.chain_err (
+                    fun () -> asprintf "while evaluating `%a + %a`" fmt t_1 fmt t_2
                 )
 
             let sub (t_1 : t) (t_2 : t) : t =
-                if t_1 < t_2 then (
-                    sprintf
-                        "underflow on thezos subtraction `%s - %s`"
-                        (Int64.to_string t_1) (Int64.to_string t_2)
-                    |> Exc.throw
-                ) else Int64.sub t_1 t_2
+                (fun () ->
+                    if t_1 < t_2
+                    then Exc.Throw.mutez_underflow ""
+                    else Uint64.sub t_1 t_2
+                )
+                |> Exc.chain_err (
+                    fun () -> asprintf "while evaluating `%a - %a`" fmt t_1 fmt t_2
+                )
+
             let mul_nat (t : t) (n : nat) : t =
-                (fun () -> of_nat n |> Int64.mul t)
-                |> Exc.erase_err (
+                (fun () ->
+                    let n_64 = Nat.to_string n |> of_string in
+                    let div = Uint64.div Uint64.max_int n_64 in
+                    if t > div then Exc.Throw.mutez_overflow "";
+                    of_nat n |> Uint64.mul t
+                )
+                |> Exc.chain_err (
                     fun () -> asprintf "while evaluating `%a * %a`" fmt t Nat.fmt n
                 )
+
             let div_nat (t : t) (n : nat) : t =
-                (fun () -> of_nat n |> Int64.mul t)
-                |> Exc.erase_err (
+                (fun () ->
+                    if n = Nat.zero
+                    then Exc.Throw.div_zero ""
+                    else of_nat n |> Uint64.div t
+                )
+                |> Exc.chain_err (
                     fun () -> asprintf "while evaluating `%a / %a`" fmt t Nat.fmt n
                 )
             let div (t_1 : t) (t_2 : t) : t =
-                if t_2 = Int64.zero then (
-                    asprintf "cannot divide by zero in `%a / %a`" fmt t_1 fmt t_2
-                    |> Exc.throw
-                );
-                Int64.div t_1 t_2
+                (fun () ->
+                    if t_2 = Uint64.zero
+                    then Exc.Throw.div_zero ""
+                    else Uint64.div t_1 t_2
+                )
+                |> Exc.chain_err (
+                    fun () -> asprintf "while evaluating `%a / %a`" fmt t_1 fmt t_2
+                )
+
             let compare (t_1 : t) (t_2 : t) : int =
                 compare t_1 t_2
-            let zero : t = Int64.zero
+
+            let zero : t = Uint64.zero
         end
 
         type t =

user_doc/rsc/no_contract/okay/anonymous.techel.output

@@ -29,7 +29,7 @@ stopping [retrieved the balance of the contract] press `return` to continue
 running test script...
 stack:
 |==================================================================================================|
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 

user_doc/rsc/simpleExample/okay/create1.techel.output

@@ -5,7 +5,7 @@ running test script...
 stack:
 |==================================================================================================|
 |                                                                                         @storage |
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |--------------------------------------------------------------------------------------------------|
 |                                                                                          @amount |

user_doc/rsc/simpleExample/okay/inspection.techel.output

@@ -24,7 +24,7 @@ stopping [retrieved the balance of the contract] press `return` to continue
 running test script...
 stack:
 |==================================================================================================|
-| 0                                                                                                |
+| 0p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|
 

user_doc/rsc/simpleExample/okay/transfer.techel.output

@@ -39,7 +39,7 @@ stopping [retrieved the balance of the contract] press `return` to continue
 running test script...
 stack:
 |==================================================================================================|
-| 1                                                                                                |
+| 1p                                                                                               |
 | nat                                                                                              |
 |==================================================================================================|