https://gitlab.com/nomadic-labs/mi-cho-coq
Revision d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC, committed by kristinas on 11 May 2021, 09:41:59 UTC
1 parent f70493e
Tip revision: d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC
Added README
Added README
Tip revision: d116674
spending_limit_contract_definition.v
From Michocoq Require Import macros syntax.
Require Import ZArith String.
Definition payload_ty :=
or
(pair
(pair
(* %journaliere) *)
key_hash
(pair
(pair
(*
* %fonds_restant
*)
mutez
(*
* %duree_de_blocage
*)
int)
(* %file *)
(pair
(list (pair timestamp mutez))
(list (pair timestamp mutez)))))
(* %nouvelle_clef_maitresse *)
key_hash)
None
(pair
(lambda unit (list operation))
(* %nouvelle_clef_publique *)
key_hash)
None.
Definition parameter_master_ty :=
(pair
(pair
(* %clef_publique) *)
key signature)
payload_ty).
Definition parameter_transfer_ty :=
(pair (* %transfer *)
(pair
(list (* %beneficiaires *)
(pair
(* %montant *)
mutez
(* %beneficiaire *)
(contract unit)))
(* %novelle_clef_journaliere *)
key_hash)
(pair
(* %clef_publique *)
key
signature)).
Definition parameter_ty : type :=
(or
(*
* %send
*)
unit
(Some "%send"%string)
(or
parameter_master_ty (Some "%appel_clef_maitresse"%string)
parameter_transfer_ty (Some "%transfer"%string)) None).
Definition storage_context_ty :=
(pair
(* journaliere *)
key_hash
(pair
(pair
(*
* %fonds_restant
*)
mutez
(* %duree_de_blocage *)
int)
(* %file *)
(pair
(list (pair timestamp mutez))
(list (pair timestamp mutez))))).
Definition storage_auth_ty :=
(pair
(* %maitresse *)
key_hash
(* %sel *)
(pair nat nat)).
Definition storage_ty := (pair storage_context_ty storage_auth_ty).
Definition slc_ep_master_lambda :
instruction_seq (Some (parameter_ty, None))
false
((pair
(lambda unit (list operation))
(* %nouvelle_clef_publique *)
key_hash) ::: (pair nat nat)::: storage_context_ty ::: nil)
(list operation ::: storage_context_ty ::: storage_auth_ty ::: nil)
:=
(* execute lambda *)
{ UNPAIR (* @function *) (* @new_master_key *) ;
DIP1 { PAIR; SWAP };
UNIT ;
EXEC }%michelson.
Definition slc_ep_master :
instruction_seq (Some (parameter_ty, None))
false
(parameter_master_ty ::: storage_context_ty ::: storage_auth_ty ::: nil)
(list operation ::: storage_context_ty ::: storage_auth_ty ::: nil) :=
{ (* retrieve master_key and salt from storage *)
DIP1 {SWAP};
SWAP ;
UNPAIR ;
(* pack the payload with the header (contract, chain_id, salt) *)
DIP1 {SWAP;
UNPAIR;
DIP1 { DUP;
(* pack the received payload (new storage or lambda) *)
PACK (* @packedpayload *) ;
(* pack the header *)
DIP1 { DIP1 { UNPAIR;
DUP ;
DIP1 {
PUSH nat (comparable_constant nat 2%N) ;
(* increment salt *)
ADD (s := add_nat_nat) (* @salt_inc *) ;
PAIR };
PACK (* @packed_salt *) ;
(* packed(salt) *)
CHAIN_ID ;
SELF (self_type := parameter_ty) (self_annot := None) None I ;
PAIR ;
PACK (* @packed_self_chain_id *) ;
(* packed(self, chain_id) : packed(salt) : ... *)
CONCAT (i := stringlike_bytes) (* @packedheader *)
(* (packed(self, chain_id) ++ packed(salt)) : ... *)
} ;
SWAP} ;
CONCAT (i := stringlike_bytes) (* @packedpayload *) ;
(* (packed(storage) *)
(* ++ packed(self, chain_id) *)
(* ++ packed(salt)) : ... *)
DUP (* @packedpayloadDup *) } ;
UNPAIR ;
DUP ;
HASH_KEY (* @sender_public_key_hash *)
} ;
(* verify that the public key hash of the sender equal the public key has of the master *)
ASSERT_CMPEQ ;
(* verify that the that the signature is a signature of the payload with from master *)
CHECK_SIGNATURE ;
(* if not, fail. *)
IF_TRUE {DROP1} {FAILWITH} ;
IF_LEFT { (* set new storage *)
UNPAIR (* @new_storage *) (* @new_master_key *) ;
(* pair up the incremented salt with the new master key *)
DIP1{ PAIR ;
SWAP ;
DROP1} ;
(* no operations will be executed *)
NIL operation}
((* execute lambda *)
slc_ep_master_lambda
)}%michelson.
Definition slc_ep_transfer2_transaction_iter_body {A}:
instruction_seq (Some (parameter_ty, None)) false
(pair mutez (contract unit) ::: list operation ::: mutez ::: A)
(list operation ::: mutez ::: A) :=
{ UNPAIR ; (* production des transactions *)
DUP ;
DIP1 {
UNIT ;
TRANSFER_TOKENS ;
CONS
} ;
SWAP ;
(* #calcul du temps de blocage *)
DIP1 { SWAP ; ADD (s := add_tez_tez) }}%michelson.
Definition slc_ep_transfer2_transaction_iter {A} :
instruction
(Some (parameter_ty, None))
false
(list (pair mutez (contract unit)) ::: list operation ::: mutez ::: A)
_
:=
ITER (i := iter_list _) (slc_ep_transfer2_transaction_iter_body).
Definition slc_ep_transfer_loop_body :
instruction (Some (parameter_ty, None)) _
(list (pair timestamp mutez) ::: list (pair timestamp mutez) ::: mutez ::: storage_auth_ty ::: nil)
(bool ::: list (pair timestamp mutez) ::: list (pair timestamp mutez) ::: mutez ::: storage_auth_ty::: nil)
:= (IF_CONS { DUP ;
CAR ;
NOW ;
IFCMPGE { CDR ;
SWAP ;
DIP1 { SWAP ;
DIP1 { ADD (s := add_tez_tez)}} ;
PUSH bool True }
{ CONS ;
PUSH bool False}}
{ IF_CONS { NIL (pair timestamp mutez) ;
SWAP ;
CONS ;
SWAP ;
ITER (i := iter_list _) { CONS } ;
NIL (pair timestamp mutez) ;
SWAP ;
PUSH bool True}
{ NIL (pair timestamp mutez) ;
DUP ;
PUSH bool False}
})%michelson.
Definition slc_ep_transfer_loop : instruction _ _ _ _ :=
(LOOP { slc_ep_transfer_loop_body })%michelson.
Definition slc_ep_transfer1_check_signature :
instruction_seq (Some (parameter_ty, None)) Datatypes.false
(parameter_transfer_ty ::: storage_context_ty ::: storage_auth_ty ::: nil)
(list (pair mutez (contract unit)) :::
list operation ::: mutez ::: key_hash ::: int ::: mutez ::: list (pair timestamp mutez) :::
list (pair timestamp mutez) ::: storage_auth_ty ::: nil)
(*
* (list operation ::: mutez ::: key_hash ::: int ::: mutez :::
* (list (pair timestamp mutez)) :::
* (list (pair timestamp mutez)) :::
* (pair key_hash nat) ::: nil)
*)
:=
{
DIP1 { UNPAPAIR } ; (* cas d'un appel simple *)
UNPAIR ;
DUP ;
PACK ;
DIP1 {
UNPAIR (a := list (pair mutez (contract unit)))
(b := key_hash) ;
DIP1 {SWAP}} ;
SWAP ;
DIP1 { DIP1 { DIP1 {SWAP} ;
SWAP ;
DIP1 { UNPAIR ;
DUP ;
HASH_KEY } ;
ASSERT_CMPEQ ; (* verification de compatibilite des clefs *)
DIG 5 (S1 := (_ ::: _ ::: _ ::: _ ::: _ ::: nil)) (@eq_refl _ 5) ;
UNPAIR ;
DIP1 { UNPAIR;
DIP1 { DUP ;
PUSH nat (Comparable_constant nat 2%N) ;
ADD (s:= add_nat_nat) } ;
PAIR };
PAIR ;
DUG 6 (S1 := (_ ::: _ ::: _ ::: _ ::: _ ::: _ ::: nil)) (@eq_refl _ 6) ;
PACK ;
CHAIN_ID ;
SELF (self_type := parameter_ty) (self_annot := None) None I ;
PAIR ;
PACK ;
CONCAT (i := stringlike_bytes)
} ;
CONCAT (i := stringlike_bytes) ;
SWAP ;
DIP1 { SWAP ;
DIP1 {DUP}} ;
CHECK_SIGNATURE ; (* #verification de signature *)
IF_TRUE {DROP1} {FAILWITH} ;
DIP1 { UNPAIR (b := int) ;
SWAP ;
DIP1 { SWAP ;
UNPAIR ;
PUSH bool True ;
(* recherche de fonds à liberer *)
slc_ep_transfer_loop ;
DIP1 {SWAP} ;
SWAP
}
} ;
PUSH mutez (0 ~mutez) ;
NIL operation
}}%michelson.
Definition slc_ep_transfer3_register :
instruction (Some (parameter_ty, None)) false
(list operation ::: mutez ::: key_hash ::: int ::: mutez :::
list (pair timestamp mutez) :::
list (pair timestamp mutez) :::
storage_auth_ty ::: nil)
(list operation ::: storage_context_ty ::: storage_auth_ty ::: nil)
:=
DIP1 { SWAP ; (* blocage des fonds depensés *)
DIP1 { SWAP ;
DUP ;
NOW ;
ADD (s := add_timestamp_int);
SWAP ;
DIP1 { DIP1 { SWAP } ;
SWAP ;
DIP1 { SWAP ;
DUP ;
DIP1 { SWAP ;
PAIR ;
SWAP ;
DIP1 { CONS } ; (* ajout dans la file *)
PAIR}} ;
SUB (s := sub_tez_tez)} ; (* calcul du reste non bloqué *)
SWAP ;
PAIR ;
PAIR
} ;
PAIR}%michelson.
Definition slc_ep_transfer :
instruction_seq (Some (parameter_ty, None)) false
(parameter_transfer_ty ::: storage_context_ty ::: storage_auth_ty ::: nil)
(list operation ::: storage_context_ty ::: storage_auth_ty ::: nil)
:= slc_ep_transfer1_check_signature ;;;
{ slc_ep_transfer2_transaction_iter ;
slc_ep_transfer3_register }.
Definition slc_ep_receive :
instruction_seq (Some (parameter_ty, None)) false
(unit ::: storage_context_ty ::: storage_auth_ty ::: nil)
(list operation ::: storage_context_ty ::: storage_auth_ty ::: nil)
:= { DROP1 ; (* cas d'un simple ajout de fonds (parameter : (Left Unit)) *)
NIL operation }%michelson.
Definition dsl :
instruction_seq _ _
(pair parameter_ty storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil)
:=
{ UNPAPAIR ;
IF_RIGHT { (* cas d'un appel par la clef maîtresse *)
IF_LEFT
slc_ep_master
slc_ep_transfer
}
slc_ep_receive ;
PAPAIR}%michelson.
Definition slc_contract_file : contract_file :=
Mk_contract_file parameter_ty None storage_ty Datatypes.false dsl.
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...