Since the protocol update to Babylon all KT1 accounts were replaced with smart contracts which contain the manager.tz script.
Code:
parameter
(or
(lambda %do unit (list operation))
(unit %default));
storage key_hash;
code
{ UNPAIR ;
IF_LEFT
{ # 'do' entrypoint
# Assert no token was sent:
# to send tokens, the default entry point should be used
PUSH mutez 0 ;
AMOUNT ;
ASSERT_CMPEQ ;
# Assert that the sender is the manager
DUUP ;
IMPLICIT_ACCOUNT ;
ADDRESS ;
SENDER ;
ASSERT_CMPEQ ;
# Execute the lambda argument
UNIT ;
EXEC ;
PAIR ;
}
{ # 'default' entrypoint
DROP ;
NIL operation ;
PAIR ;
}
};
or (source: better-call.dev):
{
{ { DUP ; CAR ; DIP { CDR } } } ;
IF_LEFT {
PUSH mutez "0.000000 ꜩ" ;
AMOUNT ;
{
{ COMPARE ; EQ } ;
IF { }
$ELSE { { UNIT ; FAILWITH } }
} ;
{ DIP { DUP } ; SWAP } ;
IMPLICIT_ACCOUNT ;
ADDRESS ;
SENDER ;
{
{ COMPARE ; EQ } ;
IF { }
$ELSE { { UNIT ; FAILWITH } }
} ;
UNIT ;
EXEC ;
PAIR
}
$ELSE { DROP ; NIL operation; PAIR }
}
The formal proof manager.v:
(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <[email protected]> *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
Require Import String.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import ZArith.
Require Import semantics.
Require Import util.
Import error.
Require List.
Require Import Lia.
Definition parameter_ty := or (lambda unit (list operation)) unit.
Definition storage_ty := key_hash.
Module ST : (SelfType with Definition self_type := parameter_ty).
Definition self_type := parameter_ty.
End ST.
Module manager(C:ContractContext)(E:Env ST C).
Module semantics := Semantics ST C E. Import semantics.
Definition manager : full_contract _ ST.self_type storage_ty :=
(UNPAIR ;;
IF_LEFT
( (* 'do' entrypoint *)
(* Assert no token was sent: *)
(* to send tokens, the default entry point should be used *)
PUSH mutez (0 ~mutez) ;;
AMOUNT ;;
ASSERT_CMPEQ ;;
(* Assert that the sender is the manager *)
DUUP ;;
IMPLICIT_ACCOUNT ;;
ADDRESS ;;
SENDER ;;
ASSERT_CMPEQ ;;
(* Execute the lambda argument *)
UNIT ;;
EXEC ;;
PAIR
)
( (* 'default' entrypoint *)
DROP1 ;;
NIL operation ;;
PAIR
)
).
Definition manager_spec
(storage : data storage_ty)
(param : data parameter_ty)
(new_storage : data storage_ty)
(returned_operations : data (list operation))
(fuel : Datatypes.nat) :=
match param with
| inr tt =>
(* %default: anybody can send tokens this does not modify the
storage and produces no operation. *)
new_storage = storage /\ returned_operations = nil
| inl (existT _ _ lam) =>
(* %do is only available to the stored manager and rejects non-null amounts*)
amount env = (0 ~Mutez) /\
sender env = address_ env unit (implicit_account env storage) /\
new_storage = storage /\
eval (no_self env) lam fuel (tt, tt) = Return _ (returned_operations, tt)
end.
Lemma eqb_eq a c1 c2 :
BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = true <->
c1 = c2.
Proof.
rewrite BinInt.Z.eqb_eq.
rewrite comparison_to_int_Eq.
apply comparable.compare_eq_iff.
Qed.
Lemma eqb_neq a c1 c2 :
BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = false <->
c1 <> c2.
Proof.
split.
- intros H He.
apply eqb_eq in He.
congruence.
- intro Hneq.
rewrite <- eqb_eq in Hneq.
generalize (BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0) Hneq.
intros []; congruence.
Qed.
Lemma and_right {P Q R : Prop} : P -> (Q <-> R) -> (Q <-> (P /\ R)).
Proof.
intuition.
Qed.
Lemma and_both {P Q R : Prop} : (Q <-> R) -> ((P /\ Q) <-> (P /\ R)).
Proof.
intuition.
Qed.
Lemma fold_eval_precond fuel :
@eval_precond_body (@semantics.eval_precond fuel) =
@semantics.eval_precond (S fuel).
Proof.
reflexivity.
Qed.
Lemma if_false_is_and (b : Datatypes.bool) P : (if b then P else false) <-> b = true /\ P.
Proof.
destruct b.
- intuition.
- simpl.
intuition discriminate.
Qed.
Lemma manager_correct
(storage : data storage_ty)
(param : data parameter_ty)
(new_storage : data storage_ty)
(returned_operations : data (list operation))
(fuel : Datatypes.nat) :
fuel >= 42 ->
eval env manager (13 + fuel) ((param, storage), tt) = Return _ ((returned_operations, new_storage), tt)
<-> manager_spec storage param new_storage returned_operations fuel.
Proof.
intro Hfuel.
remember (13 + fuel) as fuel2.
assert (30 <= fuel2) by lia.
rewrite return_precond.
rewrite eval_precond_correct.
unfold manager_spec.
do 5 (more_fuel; simpl).
destruct param as [(tff, lam)|[]].
- do 5 (more_fuel; simpl).
simpl.
rewrite if_false_is_and.
rewrite (eqb_eq mutez).
apply and_both.
do 5 (more_fuel; simpl).
rewrite if_false_is_and.
rewrite (eqb_eq address).
apply and_both.
simpl in Heqfuel2.
repeat rewrite fold_eval_precond.
assert (fuel = S (S fuel2)) by lia.
subst fuel. clear Hfuel.
rewrite <- eval_precond_correct.
rewrite precond_exists.
unfold precond_ex.
split.
++ intros ((ops, []), (Hops, Hs)).
injection Hs; intros; subst.
auto.
++ intros ([], Hlam).
exists (returned_operations, tt).
auto.
- simpl.
intuition congruence.
Qed.
End manager.
How can a community member verify this with "Mi-Cho-Coq" by himself? Is there an easy way like an online site where you can paste the Michelson code and the proof and then somehow see the checks, verify the outputs and something like code coverage or something like unit-tests? I would like to know which aspects of the code are being tested and which different states it can have, as I am unable to understand the code.
