https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 1fee3f13fee3d9826281af144b49be74df2535aa authored by Arvid Jakobsson on 25 April 2021, 08:49:19 UTC
Merge branch 'chain-modelisation-guestbook' into 'master'
Merge branch 'chain-modelisation-guestbook' into 'master'
Tip revision: 1fee3f1
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)) 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.