From 6b5c98e88b17187037be86ac91b3f59b5e5b1994 Mon Sep 17 00:00:00 2001 From: Sota Sato Date: Tue, 12 Mar 2024 02:01:58 +0900 Subject: [PATCH 1/3] Add st.balance consistent with contract_balance --- lib/gen_mlw.ml | 33 ++++++++++++++++++++++++++++++++- lib/mlw/preambles.mlw | 3 +++ 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/lib/gen_mlw.ml b/lib/gen_mlw.ml index b018922..1e0c2bc 100644 --- a/lib/gen_mlw.ml +++ b/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 diff --git a/lib/mlw/preambles.mlw b/lib/mlw/preambles.mlw index 9247c22..bc30272 100644 --- a/lib/mlw/preambles.mlw +++ b/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 } From 9bcb869d755ff4cc7c7df3e38f8ba036bfe92ba2 Mon Sep 17 00:00:00 2001 From: Sota Sato Date: Thu, 14 Mar 2024 15:25:44 +0900 Subject: [PATCH 2/3] Add examples/test_balance.tzw --- .github/workflows/actions.yml | 1 + examples/test_balance.tzw | 54 +++++++++++++++++++++++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 examples/test_balance.tzw diff --git a/.github/workflows/actions.yml b/.github/workflows/actions.yml index 0494fdf..88b82d9 100644 --- a/.github/workflows/actions.yml +++ b/.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 diff --git a/examples/test_balance.tzw b/examples/test_balance.tzw new file mode 100644 index 0000000..5cc111b --- /dev/null +++ b/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 + From 24c464a2ccfa9e3da06ab37f87b09b5010334cf1 Mon Sep 17 00:00:00 2001 From: Sota Sato Date: Thu, 14 Mar 2024 15:19:02 +0900 Subject: [PATCH 3/3] Add [@gen_wf] to neg/entrypoints.tzw --- examples/neg/entrypoints.tzw | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/neg/entrypoints.tzw b/examples/neg/entrypoints.tzw index 33b3c34..0468c5e 100644 --- a/examples/neg/entrypoints.tzw +++ b/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