https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 6f7815a0315cc619c967802918199981c0230eaa authored by Arvid Jakobsson on 25 April 2021, 12:22:00 UTC
Merge branch 'arvid@rafoo@fuelfree-wp' into 'dev'
Merge branch 'arvid@rafoo@fuelfree-wp' into 'dev'
Tip revision: 6f7815a
manager.v
(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <contact@nomadic-labs.com> *)
(* 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)) (Some "%do"%string) unit (Some "%default"%string).
Definition storage_ty := key_hash.
Module manager(C:ContractContext).
Module semantics := Semantics C. Import semantics.
Definition manager : full_contract _ parameter_ty None 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
(env : @proto_env (Some (parameter_ty, None)))
(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_ unit (implicit_account storage) /\
new_storage = storage /\
eval_seq (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
(env : @proto_env (Some (parameter_ty, None)))
(storage : data storage_ty)
(param : data parameter_ty)
(new_storage : data storage_ty)
(returned_operations : data (list operation))
(fuel : Datatypes.nat) :
fuel >= 42 ->
eval_seq env manager (2 + fuel) ((param, storage), tt) = Return ((returned_operations, new_storage), tt)
<-> manager_spec env storage param new_storage returned_operations fuel.
Proof.
intro Hfuel.
unfold ">=" in Hfuel.
rewrite return_precond.
rewrite eval_seq_precond_correct.
unfold manager_spec.
more_fuel; simpl.
more_fuel; simpl.
destruct param as [(tff, lam)|[]].
- rewrite (eqb_eq mutez).
apply and_both.
rewrite (eqb_eq address).
apply and_both.
repeat rewrite fold_eval_precond.
fold (eval_seq_precond (S (S fuel)) (self_type := None)).
rewrite <- eval_seq_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.
- intuition congruence.
Qed.
End manager.