Add st.balance consistent with contract_balance

.github/workflows/actions.yml

@@ -65,4 +65,5 @@ jobs:
       - run: opam exec -- why3 prove -P z3 examples/boomerang_acc.tzw
       - run: opam exec -- why3 prove -P z3 examples/auction.tzw
       - run: opam exec -- why3 prove -P z3 examples/callback.tzw
+      - run: opam exec -- why3 prove -P z3 examples/test_balance.tzw
       - run: opam exec -- why3 prove -P z3 examples/dexter2/liquidity.tzw 

examples/neg/entrypoints.tzw

@@ -18,7 +18,7 @@ end
 
 scope Alice
 
-  type storage = address
+  type storage [@gen_wf] = address
 
   predicate pre (_st : step) (_gp : gparam) (c : ctx) = inv_pre c
 
@@ -39,7 +39,7 @@ end
 
 scope Bob
 
-  type storage = address
+  type storage [@gen_wf] = address
 
   predicate pre (_st : step) (_gp : gparam) (c : ctx) = inv_pre c
 
@@ -59,7 +59,7 @@ end
 
 scope Carol
 
-  type storage = address
+  type storage [@gen_wf] = address
 
   predicate pre (_st : step) (_gp : gparam) (c : ctx) = inv_pre c
 

examples/test_balance.tzw

@@ -0,0 +1,54 @@
+(*
+  `ctx.[contract_name]_balance` is the balance of the contract
+  without the amount of the current transfer.
+  `st.balance` corresponds to the `BALANCE` operation of Michelson,
+  including the amount of the current transfer.
+*)
+
+scope Postambles
+  predicate inv (c : ctx) =
+    c.a_storage = A.{ acc = c.a_balance; diff = 0 }
+end
+
+scope Unknown
+
+  predicate pre (c : ctx) = inv c
+
+  predicate post (_c : ctx) (c' : ctx) = inv c'
+
+  scope Entrypoint
+
+  predicate default unit
+
+  end
+
+end
+
+scope A
+
+  type storage [@gen_wf] = {
+    acc : mutez;
+    diff : mutez
+  }
+
+  predicate pre (_st : step) (_gp : gparam) (c : ctx) = inv c
+
+  predicate post (st : step) (_gp : gparam) (c : ctx) (c' : ctx) =
+    st.balance = c.a_balance + st.amount /\
+    c'.a_balance = c.a_balance + st.amount /\
+    inv c'
+
+  let upper_ops = 1
+
+  scope Spec
+
+    predicate default (st : step) (_p : unit) (s : storage) (ops : list operation) (s' : storage) =
+      let acc' = s.acc + st.amount in
+      let abs a b = if a > b then a - b else b - a in
+      s' = { acc = acc'; diff = s.diff + abs acc' st.balance } /\
+      ops = Nil
+
+  end
+
+end
+

lib/gen_mlw.ml

@@ -126,6 +126,7 @@ module T = struct
           (* Hack: && => /\ *)
           Tbinnop (of_expr e1, Dterm.DTand, of_expr e2)
       | Eapply (e1, e2) -> Tapply (of_expr e1, of_expr e2)
+      | Eif (e1, e2, e3) -> Tif (of_expr e1, of_expr e2, of_expr e3)
       | _ ->
           Format.eprintf "T.of_expr: unsupported: %a@."
             (Mlw_printer.pp_expr ~attr:true).closed e;
@@ -203,13 +204,14 @@ module E = struct
 end
 
 module Step_constant = struct
-  let mk source sender self amount level now : expr =
+  let mk source sender self amount balance level now : expr =
     E.mk_record
       [
         (qualid [ "source" ], source);
         (qualid [ "sender" ], sender);
         (qualid [ "self" ], self);
         (qualid [ "amount" ], amount);
+        (qualid [ "balance" ], balance);
         (qualid [ "level" ], level);
         (qualid [ "now" ], now);
       ]
@@ -218,6 +220,7 @@ module Step_constant = struct
   let sender st : expr = eapp (qualid [ "sender" ]) [ st ]
   let self st : expr = eapp (qualid [ "self" ]) [ st ]
   let amount st : expr = eapp (qualid [ "amount" ]) [ st ]
+  let balance st : expr = eapp (qualid [ "balance" ]) [ st ]
   let level st : expr = eapp (qualid [ "level" ]) [ st ]
   let now st : expr = eapp (qualid [ "now" ]) [ st ]
 end
@@ -496,6 +499,13 @@ module Generator (D : Desc) = struct
               call_ctx_wf @@ E.var_of_binder ctx;
               call_step_wf @@ E.var_of_binder st;
               call_param_wf_of contract @@ E.var_of_binder gparam;
+              E.mk_bin
+                (Step_constant.balance @@ E.var_of_binder st)
+                "="
+                (E.mk_bin
+                   (balance_of contract (E.var_of_binder ctx))
+                   "+"
+                   (Step_constant.amount @@ E.var_of_binder st));
               call_pre_of contract (E.var_of_binder st) (E.var_of_binder gparam)
                 (E.var_of_binder ctx);
             ];
@@ -558,6 +568,14 @@ module Generator (D : Desc) = struct
                                   (source @@ E.var_of_binder st)
                                   (self @@ E.var_of_binder st)
                                   (E.mk_var dst) (E.mk_var amt)
+                                  (M.fold
+                                     (fun _ c e ->
+                                       E.mk_if
+                                         (is_contract_of c @@ E.mk_var dst)
+                                         (E.mk_bin (balance_of c ctx) "+"
+                                            (E.mk_var amt))
+                                         e)
+                                     contracts (econst 0))
                                   (level @@ E.var_of_binder st)
                                   (now @@ E.var_of_binder st))
                             in
@@ -648,6 +666,19 @@ module Generator (D : Desc) = struct
          in
          let+ p = E.mk_any gparam_pty in
          wrap_assume ~assumption:(wf st)
+         @@ wrap_assume
+              ~assumption:
+                (T.of_expr
+                @@ M.fold
+                     (fun _ c e ->
+                       E.mk_if
+                         (is_contract_of c @@ Step_constant.self st)
+                         (E.mk_bin (Step_constant.balance st) "="
+                            (E.mk_bin
+                               (balance_of c (E.var_of_binder ctx))
+                               "+" (Step_constant.amount st)))
+                         e)
+                     contracts (expr Etrue))
          @@ let+ ctx = dispatch_transfer (E.var_of_binder ctx) st p in
             call_unknown ctx
     in

lib/mlw/preambles.mlw

@@ -78,6 +78,7 @@ type step =
     sender: address;
     self: address;
     amount: mutez;
+    balance: mutez;
     level: nat;
     now: timestamp
   }
@@ -87,12 +88,14 @@ function mk_step
     (sender : address)
     (self : address)
     (amount : mutez)
+    (balance : mutez)
     (level : nat)
     (now : timestamp) : step =
   { source= source;
     sender= sender;
     self= self;
     amount= amount;
+    balance= balance;
     level= level;
     now= now }