In this new series of blog posts, we will be introducing Coq and Mi-Cho-Coq for proving Tezos smart contracts written in or compiled to Michelson. This series is structured as follows:
- 01. Formal proving: What is it about, what are Coq and Mi-Cho-Coq, and why will we need them.
- 02. A quick introduction to Coq
- 03. A quick introduction to Mi-Cho-Coq: proving our first Michelson smart contract.
- 04. Proving the increment contract
- 05. Proving if conditions.
- 06. Proving a token minting entrypoint
Chaper VI: Proving a minting contract
Introduction
Let’s now continue our Mi-Cho-Coq journey by proving an actually useful contract. In the previous chapter, we saw how to prove that conditions were properly implemented, we’ll now see how to prove that Michelson mode that makes use of maps are properly implemented by proving a contract that mints tokens.
The contract
The ligo contract implementation is show bellow. We define the storage with a contract owner, a map of balances, a a total supply, as was done in the previous chapter. We also define the minting entrypoint parameter as a record containing the amount to mint and the address to mint to.
In the mint entrypoint implementation, we restrict the entrypoint such that only the contract owner can call it, we update the balances map by checking if the address we are minting to already has an existing balance or not, and we return an updated storage with no operations:
type security_token_storage_t = {
owner : address ;
balances : ( address , nat ) big_map ;
tokens : nat ;
}
type param_t = {
amount : nat ;
tr_to : address ;
}
type security_token_ret_t = (operation list * security_token_storage_t)
let mint (param, s : param_t * security_token_storage_t)
: security_token_ret_t =
let check_sender =
if (
sender <> s.owner
) then failwith "error"
in
let new_balances =
match Big_map.find_opt param.tr_to s.balances with
| None -> Big_map.update param.tr_to (Some (param.amount)) s.balances
| Some n -> Big_map.update param.tr_to (Some (n + param.amount)) s.balances
in
let new_s = {
tokens = s.tokens + param.amount ;
owner = s.owner ;
balances = new_balances ;
} in
( ([] : operation list) , new_s )
Let’s compile it to Michelson, we can use the Nyx docker container to have a Ligo compiler ready in seconds:
host $ git clone git@gitlab.com:equisafe/nyx.git
host $ docker-compose up -d
host $ docker ps
CONTAINER ID IMAGE
c7499257de73 thomasbinetruy/eqs-nyx:pynyx
721b910c1c59 thomasbinetruy/eqs-nyx:tz-sandbox
Let’s compile it to Michelson, we can use the Nyx docker container to have a Ligo compiler ready in seconds:
host $ git clone git@gitlab.com:equisafe/nyx.git
host $ docker-compose up -d
host $ docker ps
CONTAINER ID IMAGE
c7499257de73 thomasbinetruy/eqs-nyx:pynyx
721b910c1c59 thomasbinetruy/eqs-nyx:tz-sandbox
We can now hop into the container and compile our file:
host $ docker exec -it c7499 bash
container $ cd mi-cho-coq/tutorials/scripts/if/
container $ ligo compile-contract if.mligo main
Which outputs the following Michelson, as you can see, it is quite long ! Indeed, since we have to modify the storage, there are quite a few variables to fetch thoughout the contract, as can be seen by the many DIG, DUP and DUG:
{ parameter (pair (nat %amount) (address %tr_to)) ;
storage (pair (pair (big_map %balances address nat) (address %owner)) (nat %tokens)) ;
code { DUP ;
CAR ;
DIG 1 ;
DUP ;
DUG 2 ;
CDR ;
DUP ;
CAR ;
CDR ;
SENDER ;
COMPARE ;
NEQ ;
IF { PUSH string "error" ; FAILWITH } { PUSH unit Unit } ;
DIG 1 ;
DUP ;
DUG 2 ;
CAR ;
CAR ;
DIG 3 ;
DUP ;
DUG 4 ;
CDR ;
GET ;
IF_NONE
{ DIG 1 ;
DUP ;
DUG 2 ;
CAR ;
CAR ;
DIG 3 ;
DUP ;
DUG 4 ;
CAR ;
SOME ;
DIG 4 ;
DUP ;
DUG 5 ;
CDR ;
UPDATE }
{ DIG 2 ;
DUP ;
DUG 3 ;
CAR ;
CAR ;
DIG 4 ;
DUP ;
DUG 5 ;
CAR ;
DIG 2 ;
DUP ;
DUG 3 ;
ADD ;
SOME ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
UPDATE ;
DIP { DROP } } ;
DIG 3 ;
DUP ;
DUG 4 ;
CAR ;
DIG 3 ;
DUP ;
DUG 4 ;
CDR ;
ADD ;
DIG 3 ;
DUP ;
DUG 4 ;
CAR ;
CDR ;
DIG 2 ;
DUP ;
DUG 3 ;
PAIR ;
PAIR ;
DUP ;
NIL operation ;
PAIR ;
DIP { DROP 6 } } }
Proving the contract
Let’s start with a few import and the storage definition as was done in the previous chapter:
Require Import Michocoq.macros.
Import Michocoq.syntax.
Require Import Michocoq.semantics.
Require Import Michocoq.util.
Import error.
Require Import ZArith.
Import comparable.
Definition amount_ty := nat.
Definition destination_address_ty := address.
Definition parameter_ty := (pair amount_ty destination_address_ty).
Definition balances_ty := map address nat.
Definition owner_ty := address.
Definition supply_ty := nat.
Definition storage_ty := (pair (pair balances_ty owner_ty) supply_ty).
Module ST : (SelfType with Definition self_type := parameter_ty).
Definition self_type := parameter_ty.
End ST.
Module if_contract(C:ContractContext)(E:Env ST C).
Module semantics := Semantics ST C E. Import semantics.
Let’s now convert our Michelson, code compiled in the previous question, to the Michocoq representation. To do that, let’s first write a few definitions that will make the conversion simpler: instead of having to write DUG (S1 := [_; _]) 2 eq_refl ;; when “DUG’ing” with a depth 2, we’d like to now write DUG2. Looking at the Ligo compiler output, we notice that it “DUG’s” at most 6, let’s write our helper definitions. Note that similar definitions already exist for DIP instructions.
Definition DUG1 {a S2 t self_type} : instruction self_type Datatypes.false (t ::: a ::: S2) (a ::: (t ::: S2)) :=
DUG (S1 := [_]) 1 eq_refl.
Definition DUG2 {a b S2 t self_type} :
instruction self_type _ (t ::: a ::: b ::: S2) (a ::: b :::(t ::: S2)) :=
DUG (S1 := [_; _]) 2 eq_refl.
Definition DUG3 {a b c S2 t self_type} :
instruction self_type _ (t ::: a ::: b ::: c ::: S2) (a ::: b ::: c ::: (t ::: S2)) :=
DUG (S1 := [_; _; _]) 3 eq_refl.
Definition DUG4 {a b c d S2 t self_type} :
instruction self_type _ (t ::: a ::: b ::: c ::: d ::: S2) (a ::: b ::: c ::: d ::: (t ::: S2)) :=
DUG (S1 := [_; _; _; _]) 4 eq_refl.
Definition DUG5 {a b c d e S2 t self_type} :
instruction self_type _ (t ::: a ::: b ::: c ::: d ::: e ::: S2) (a ::: b ::: c ::: d ::: e ::: (t ::: S2)) :=
DUG (S1 := [_; _; _; _; _]) 5 eq_refl.
Definition DUG6 {a b c d e f S2 t self_type} :
instruction self_type _ (t ::: a ::: b ::: c ::: d ::: e ::: f ::: S2) (a ::: b ::: c ::: d ::: e ::: f ::: (t ::: S2)) :=
DUG (S1 := [_; _; _; _; _; _]) 6 eq_refl.
Similarly, let’s make similar helper definitions for the DIG and DROP instructions:
Definition DIG1 {a S2 t self_type} : instruction self_type Datatypes.false (a ::: (t ::: S2)) (t ::: a ::: S2) :=
DIG (S1 := [_]) 1 eq_refl.
Definition DIG2 {a b S2 t self_type} :
instruction self_type _ (a ::: b :::(t ::: S2)) (t ::: a ::: b ::: S2) :=
DIG (S1 := [_; _]) 2 eq_refl.
Definition DIG3 {a b c S2 t self_type} :
instruction self_type _ (a ::: b ::: c ::: (t ::: S2)) (t ::: a ::: b ::: c ::: S2) :=
DIG (S1 := [_; _; _]) 3 eq_refl.
Definition DIG4 {a b c d S2 t self_type} :
instruction self_type _ (a ::: b ::: c ::: d ::: (t ::: S2)) (t ::: a ::: b ::: c ::: d ::: S2) :=
DIG (S1 := [_; _; _; _]) 4 eq_refl.
Definition DIG5 {a b c d e S2 t self_type} :
instruction self_type _ (a ::: b ::: c ::: d ::: e ::: (t ::: S2)) (t ::: a ::: b ::: c ::: d ::: e ::: S2) :=
DIG (S1 := [_; _; _; _; _]) 5 eq_refl.
Definition DIG6 {a b c d e f S2 t self_type} :
instruction self_type _ (a ::: b ::: c ::: d ::: e ::: f ::: (t ::: S2)) (t ::: a ::: b ::: c ::: d ::: e ::: f ::: S2) :=
DIG (S1 := [_; _; _; _; _; _]) 6 eq_refl.
Definition DROP2 {a b SA self_type} : instruction self_type Datatypes.false (a ::: b ::: SA) SA :=
DROP (A := [_; _]) 2 eq_refl.
Definition DROP3 {a b c SA self_type} : instruction self_type Datatypes.false (a ::: b ::: c ::: SA) SA :=
DROP (A := [_; _; _]) 3 eq_refl.
Definition DROP4 {a b c d SA self_type} : instruction self_type Datatypes.false (a ::: b ::: c ::: d ::: SA) SA :=
DROP (A := [_; _; _; _]) 4 eq_refl.
Definition DROP5 {a b c d e SA self_type} : instruction self_type Datatypes.false (a ::: b ::: c ::: d ::: e ::: SA) SA :=
DROP (A := [_; _; _; _; _]) 5 eq_refl.
Definition DROP6 {a b c d e f SA self_type} : instruction self_type Datatypes.false (a ::: b ::: c ::: d ::: e ::: f ::: SA) SA :=
DROP (A := [_; _; _; _; _; _]) 6 eq_refl.
Now, defining the contract is simple:
Definition mint_contract : full_contract _ ST.self_type storage_ty :=
( DUP ;;
CAR ;;
DIG1 ;;
DUP ;;
DUG2 ;;
CDR ;;
DUP ;;
CAR ;;
CDR ;;
SENDER ;;
COMPARE ;;
NEQ ;;
IF ( FAIL ) ( UNIT ) ;;
DIG1 ;;
DUP ;;
DUG2 ;;
CAR ;;
CAR ;;
DIG3 ;;
DUP ;;
DUG4 ;;
CDR ;;
GET (i := get_map address nat);;
IF_NONE
( DIG1 ;;
DUP ;;
DUG2 ;;
CAR ;;
CAR ;;
DIG3 ;;
DUP ;;
DUG4 ;;
CAR ;;
SOME ;;
DIG4 ;;
DUP ;;
DUG5 ;;
CDR ;;
UPDATE (i := Mk_update address (option nat) (map address nat) (Update_variant_map address nat)))
( DIG2 ;;
DUP ;;
DUG3 ;;
CAR ;;
CAR ;;
DIG4 ;;
DUP ;;
DUG5 ;;
CAR ;;
DIG2 ;;
DUP ;;
DUG3 ;;
ADD ;;
SOME ;;
DIG5 ;;
DUP ;;
DUG6 ;;
CDR ;;
UPDATE (i := Mk_update address (option nat) (map address nat) (Update_variant_map address nat));;
DIP1 ( DROP1 ) ) ;;
DIG3 ;;
DUP ;;
DUG4 ;;
CAR ;;
DIG3 ;;
DUP ;;
DUG4 ;;
CDR ;;
ADD ;;
DIG3 ;;
DUP ;;
DUG4 ;;
CAR ;;
CDR ;;
DIG2 ;;
DUP ;;
DUG3 ;;
PAIR ;;
PAIR ;;
DUP ;;
NIL operation ;;
PAIR ;;
DIP1 ( DROP6 ) ).
Let’s now define the contract entrypoint:
Definition amount_ty := nat.
Definition destination_address_ty := address.
Definition parameter_ty := (pair amount_ty destination_address_ty).
We can now finally write the contract specification that we’ll be proving. We want to express the following:
- Only the contract owner can call it,
- The contract return an empty list of operations,
- The new supply equals the amount the contract was called with added to the original storage,
- If the address we are minting to existed in the balances map, then the new balance for that address equals the old balance plus the amount the contract was called with. Otherwise, the new balance equals the amount,
- For all addresses that are different from the one we are minting to, if they existed in the balance map before the contract was called, then the balance was not changed; and if they did not exist in the balance map, they still do not after the contract was called,
- For all addresses different from the one being minted to, if they were in the balance map before the contract was called, they still are after.
This is formalized in Coq as follows:
Theorem mint_contract_correct :
forall (amount : data amount_ty)
(destination_address : data destination_address_ty)
(balances_in : data balances_ty)
(owner : data owner_ty)
(supply_in : data supply_ty)
(balances_out : data balances_ty)
(supply_out : data supply_ty)
(ops : data (list operation))
(fuel : Datatypes.nat),
let input : data parameter_ty := (amount, destination_address) in
let storage_in : data storage_ty := ((balances_in, owner), supply_in) in
let storage_out : data storage_ty := ((balances_out, owner), supply_out) in
fuel >= 100 ->
eval env mint_contract fuel ((input, storage_in), tt) = Return ((ops, storage_out), tt)
<->
(sender env) = owner /\
ops = nil /\
supply_out = N.add supply_in amount /\
match (get _ _ _ (Get_variant_map _ nat) destination_address balances_in) with
| Some n1 => match (get _ _ _ (Get_variant_map _ nat) destination_address balances_out) with
| Some n2 => n2 = N.add n1 amount
| None => False
end
| None => match (get _ _ _ (Get_variant_map _ nat) destination_address balances_out) with
| Some n2 => n2 = amount
| None => False
end
end /\
(forall s, s <> destination_address ->
match (get _ _ _ (Get_variant_map _ nat) s balances_in) with
| Some n1 => match (get _ _ _ (Get_variant_map _ nat) s balances_out) with
| Some n2 => n2 = n1
| None => False
end
| None => True end) /\
(forall s, s <> destination_address -> (mem _ _ (Mem_variant_map _ nat) s balances_in) <->
(mem _ _ (Mem_variant_map _ nat) s balances_out)).
Let’s now get to the proof. Notice in the Michelson instructions that we first check that the transaction sender is indeed the contract owner, and then we check if the address to mint to exists in the storage balances map or not. Our proof will be structured similarly:
- we use more_fuel to step until the condition that the sender is the contract owner and handle both cases.
- If the sender is the contract owner, then we step until the we are looking for the investor to mint to in the storage balances map and handle both cases:
- the key is in the map,
- the key is not in the map.
Of course, since we are proving that the evaluation of the contract implies our specification and vice-versa (using the implication both way <->), we’ll need to handle both directions in our proof.
Let’s structure our proof:
Proof.
intros amount destination_address balances_in owner supply_in balances_out supply_out ops fuel input storage_in storage_out Hfuel.
unfold eval.
rewrite return_precond.
rewrite eval_precond_correct.
unfold ">=" in Hfuel.
simpl.
do 14 more_fuel ; simpl.
destruct (negb (comparison_to_int (address_compare (sender env) owner) =? 0)%Z) eqn:condition.
(* owner is not sender *)
- do 2 more_fuel ; simpl. split.
+ (* -> *) admit.
+ (* <- *) admit.
(* owner is sender *)
- do 11 more_fuel ; simpl. split.
(* -> *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* admit.
(* key is not in the map *)
* admit.
(* <- *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* admit.
(* key is not in the map *)
* admit.
Admitted.
It’s now just a matter of filling in the proof. Let’s start with the « owner is not sender » case as it is the simplest:
(* owner is not sender *)
- do 2 more_fuel ; simpl. split.
+ (* -> *) intros H. contradiction H.
+ (* <- *) intros H.
apply sender_is_not_owner in condition.
intuition.
Not that we’ve made use of the sender_is_not_owner lemma that we wrote in the previous chapter. Recall it’s definition along with that of the sender_is_owner lemma:
Lemma sender_is_not_owner : forall owner sender: address_constant,
negb
(comparison_to_int
(address_compare
owner sender) =? 0) %Z = true
-> owner <> sender.
Proof.
intros owner sender.
rewrite Bool.negb_true_iff.
rewrite Z.eqb_neq.
unfold comparison_to_int.
intuition.
destruct H.
rewrite H0. rewrite address_compare_Eq. reflexivity.
Qed.
Lemma sender_is_owner : forall owner sender: address_constant,
negb
(comparison_to_int
(address_compare
owner sender) =? 0) %Z = false
-> owner = sender.
Proof.
intros owner sender.
rewrite Bool.negb_false_iff.
rewrite (eqb_eq address).
intuition.
Qed.
We’ll now look at a few map related lemme provided by Michocoq that will prove to be helpful when manipulating our goals and hypotheses. Say we want to rewrite map.get addr balances_in = Some amount into map.mem addr balances_in, we can use the map_getmem lemma. If we want to go the other way around, we can user the map_memget lemma. If we want to rewrite map.get addr (map.update addr (Some amount) balances_in) as Some amount, we can use the map_updateeq lemma. On the other hand, if we want to rewrite map.get addr2 (map.update addr1 (Some amount) balances_in) for addr2 <> addr1 into map.get addr2 balances_in, we can use the map_updateneq lemma. Typically, this last lemma can be used to show that for all the addresses different from the one we are minting to, the balance remains unchanged after minting. If we want now to rewrite balances_out = map.update miting_address (Some amount) balances_in into (map.get minting_address balances_out = (Some amount) /\ (forall addr, minting_address <> addr -> map.get addr balances_out = map.get addr balances_in)), we can use the map_updateSome_spec lemma. If we want to rewrite map.mem minting_addr balances_in as forall addr, map.mem minting_address (map.update addr (Some amount) balances_in), we can use the map_updatemem lemma. Finally, if we want to go the other way around, that is going from map.mem minting_address (map.update addr (Some amount) balances_in) for all addr <> minting_address to map.mem miting_address balances_in, we can use the map_updatemem_rev lemma.
With these lemme in hand, proving the contract becomes simple. As you can see however, there are a lot of optionals to handle in our proof, let’s write some lemme to help use with that:
Lemma some_eq : forall a b: N, Some a = Some b -> a = b.
Proof.
intros. inversion H. reflexivity.
Qed.
Lemma eq_some : forall a b: N, a = b -> Some a = Some b.
Proof.
intros. rewrite H. reflexivity.
Qed.
Lemma some_is_not_none : forall a: N, None = Some a <-> False.
Proof.
intros. split.
- intros. inversion H.
- intros. inversion H.
Qed.
Lemma some_is_not_none_rev : forall a: N, Some a = None <-> False.
Proof.
intros. split.
- intros. inversion H.
- intros. inversion H.
Qed.
We’ll also need a two lemme to compare addresses. The Michocoq comparable.v file defines a few types including stings but not for addresses, so let’s write them:
Lemma address_compare_Eq : forall a : address_constant,
address_compare a a = Eq.
Proof.
intros a. induction a. simpl. rewrite string_compare_Eq_correct. reflexivity.
Qed.
Lemma address_compare_Eq2 : forall a1 a2 : address_constant,
address_compare a1 a2 = Eq <-> a1 = a2.
Proof.
intros.
rewrite (compare_eq_iff address); auto. split.
- intros. assumption.
- intros. assumption.
Qed.
The proof is now fairly simple to write. Let’s by proving the forward direction « key is in the map » case:
(* owner is sender *)
- do 11 more_fuel ; simpl. split.
(* -> *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* do 23 more_fuel ; simpl. intros. inversion H.
split.
-- (* (sender env) = owner *) apply sender_is_owner in condition. trivial.
-- split.
++ (* ops = nil *) reflexivity.
++ split.
** (* supply_out = N.add supply_in amount *) reflexivity.
** rewrite map.map_updateeq. split.
--- (* minter balance is increased by minted amount *) reflexivity.
--- split.
+++ (* non minter balances have not changed *)
intros addr Hdiff.
destruct (map.get address_constant N address_compare addr balances_in) eqn:mapget2.
*** rewrite map.map_updateneq.
destruct (map.get address_constant N address_compare addr balances_in) eqn:mapget3.
---- apply some_eq. trivial.
---- apply some_is_not_none in mapget2. contradiction.
---- apply addr_not_eq_sym. trivial.
*** trivial.
+++ (* all non minter addresses are still in the balances map *)
intros addr. split.
*** intros. apply map.map_updatemem. assumption.
*** intros. destruct (address_compare addr destination_address) eqn:addrcmp.
rewrite address_compare_Eq2 in addrcmp ; subst.
apply map.map_getmem with n. assumption.
eapply map.map_updatemem_rev with (k':= destination_address).
rewrite <- (compare_diff address). left. eassumption. eassumption.
eapply map.map_updatemem_rev with (k':= destination_address).
rewrite <- (compare_diff address). right. eassumption. eassumption.
(* key is not in the map *)
* admit.
Similarly, we prove the forward « key is not in the map » case:
(* owner is sender *)
- do 11 more_fuel ; simpl. split.
(* -> *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* ...
(* key is not in the map *)
* do 23 more_fuel ; simpl.
intros. inversion H. split.
-- apply sender_is_owner in condition. trivial.
-- split.
++ reflexivity.
++ split.
** reflexivity.
** rewrite map.map_updateeq. split.
--- reflexivity.
--- split.
+++ intros addr Hdiff.
destruct (map.get address_constant N address_compare addr balances_in) eqn:mapget2.
rewrite map.map_updateneq.
destruct (map.get address_constant N address_compare addr balances_in) eqn:mapget3.
*** apply some_eq. trivial.
*** apply some_is_not_none in mapget2. contradiction.
*** apply addr_not_eq_sym. trivial.
*** trivial.
+++ intros addr. split.
*** intros. apply map.map_updatemem. assumption.
*** intros. destruct (address_compare addr destination_address) eqn:addrcmp.
---- rewrite address_compare_Eq2 in addrcmp. contradiction.
---- eapply map.map_updatemem_rev with (k':= destination_address).
rewrite <- (compare_diff address). left. eassumption. eassumption.
---- eapply map.map_updatemem_rev with (k':= destination_address).
rewrite <- (compare_diff address). right. eassumption. eassumption.
We can now prove the reverse implication for the key being in the map:
(* owner is sender *)
- do 11 more_fuel ; simpl. split.
(* -> *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* ...
(* key is not in the map *)
* ...
(* <- *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* do 23 more_fuel ; simpl. intros. inversion H. inversion H1. inversion H3.
apply sender_is_owner in condition.
repeat f_equal.
-- symmetry. trivial.
-- subst storage_out. repeat f_equal.
++ symmetry. rewrite map.map_updateSome_spec. split.
** destruct (map.get address_constant N address_compare destination_address balances_out) eqn:mapget2.
+++ inversion H5. rewrite H6. reflexivity.
+++ inversion H5. contradiction.
** intros addr Hdiff. inversion H5. inversion H7. specialize (H8 addr).
destruct (map.get address_constant N address_compare addr balances_out) eqn:mapget2;
destruct (map.get address_constant N address_compare addr balances_in) eqn:mapget3;
subst; try reflexivity.
+++ apply addr_not_eq_sym in Hdiff.
apply H8 in Hdiff.
apply eq_some in Hdiff. trivial.
+++ apply map.map_getmem in mapget2.
rewrite <- H9 in mapget2. apply map.map_memget in mapget2.
destruct mapget2 as [v mapget2]. rewrite mapget3 in mapget2. discriminate mapget2.
auto.
+++ apply map.map_getmem in mapget3.
rewrite -> H9 in mapget3. apply map.map_memget in mapget3.
destruct mapget3 as [v mapget3]. rewrite mapget2 in mapget3. discriminate mapget3.
auto.
++ symmetry. trivial.
(* key is not in the map *)
* admit.
And the « key is not in the map » case for the reverse implication:
(* owner is sender *)
- do 11 more_fuel ; simpl. split.
(* -> *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* ...
(* key is not in the map *)
* ...
(* <- *)
+ destruct (map.get address_constant N address_compare destination_address balances_in) eqn:mapget.
(* key is in the map *)
* ...
(* key is not in the map *)
* do 23 more_fuel ; simpl. intros. destruct H as [H1 [H2 [H3 [H4 [H5 H6]]]]].
apply sender_is_owner in condition.
repeat f_equal.
-- symmetry. trivial.
-- subst storage_out. repeat f_equal.
++ symmetry. rewrite map.map_updateSome_spec. split.
** destruct (map.get address_constant N address_compare destination_address balances_out) eqn:mapget2.
+++ apply eq_some in H4. trivial.
+++ contradiction.
** intros addr Hdiff.
destruct (map.get address_constant N address_compare addr balances_out) eqn:mapget2;
destruct (map.get address_constant N address_compare addr balances_in) eqn:mapget3;
subst; try reflexivity.
+++ specialize (H5 addr). apply addr_not_eq_sym in Hdiff. apply H5 in Hdiff.
destruct (map.get address_constant N address_compare addr balances_in).
destruct (map.get address_constant N address_compare addr balances_out).
apply some_eq in mapget2. apply some_eq in mapget3. rewrite Hdiff in mapget2.
rewrite mapget2 in mapget3. apply eq_some. trivial. apply some_is_not_none in mapget2.
contradiction. apply some_is_not_none in mapget3. contradiction.
+++ apply map.map_getmem in mapget2. specialize (H6 addr). apply addr_not_eq_sym in Hdiff.
apply H6 in Hdiff. apply Hdiff in mapget2. apply map.map_memget in mapget2.
destruct mapget2. rewrite H in mapget3. apply some_is_not_none_rev in mapget3.
contradiction.
+++ apply map.map_getmem in mapget3. specialize (H6 addr). apply addr_not_eq_sym in Hdiff.
apply H6 in Hdiff. apply Hdiff in mapget3. apply map.map_memget in mapget3.
destruct mapget3. rewrite H in mapget2. apply some_is_not_none_rev in mapget2.
contradiction.
++ auto.
Qed.
Thus, we prove our minting contract :)
Conclusion
In this chapter, we have prove that a somewhat complex Ligo contract was properly implemented with respect to a specification we have defined. We’ve built upon what we learned in the previous chapters. However our proof is much longer since we specified many characteristics of the contract which we each had to prove.
Moreover, we have seen how to handle goals and hypotheses involving maps by getting familiar with some lemme that Michocoq provides.
Finally, the full prove is available here. Make sure that you step through it in the Coq IDE to see how we manipulate goals and hypotheses to achieve our proof.
.png)
.png)
