✒️ Contract_manager_storage.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Manager_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Inconsistent_hash.
Record record : Set := Build {
public_key : Signature.public_key;
expected_hash : Signature.public_key_hash;
provided_hash : Signature.public_key_hash;
}.
Definition with_public_key public_key (r : record) :=
Build public_key r.(expected_hash) r.(provided_hash).
Definition with_expected_hash expected_hash (r : record) :=
Build r.(public_key) expected_hash r.(provided_hash).
Definition with_provided_hash provided_hash (r : record) :=
Build r.(public_key) r.(expected_hash) provided_hash.
End Inconsistent_hash.
Definition Inconsistent_hash := Inconsistent_hash.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Manager_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Inconsistent_hash.
Record record : Set := Build {
public_key : Signature.public_key;
expected_hash : Signature.public_key_hash;
provided_hash : Signature.public_key_hash;
}.
Definition with_public_key public_key (r : record) :=
Build public_key r.(expected_hash) r.(provided_hash).
Definition with_expected_hash expected_hash (r : record) :=
Build r.(public_key) expected_hash r.(provided_hash).
Definition with_provided_hash provided_hash (r : record) :=
Build r.(public_key) r.(expected_hash) provided_hash.
End Inconsistent_hash.
Definition Inconsistent_hash := Inconsistent_hash.record.
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "contract.unrevealed_key"
"Manager operation precedes key revelation"
"One tried to apply a manager operation without revealing the manager public key"
(Some
(fun (ppf : Format.formatter) ⇒
fun (s_value : Contract_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unrevealed manager key for contract "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Unrevealed manager key for contract %a.") Contract_repr.pp
s_value))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Contract_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unrevealed_manager_key" then
let s_value := cast Contract_repr.t payload in
Some s_value
else None
end)
(fun (s_value : Contract_repr.t) ⇒
Build_extensible "Unrevealed_manager_key" Contract_repr.t s_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"contract.manager.inconsistent_hash" "Inconsistent public key hash"
"A revealed manager public key is inconsistent with the announced hash"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(k_value, eh, ph) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The hash of the manager public key "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " is not "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" as announced but "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))
"The hash of the manager public key %s is not %a as announced but %a")
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.to_b58check) k_value)
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) ph
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) eh))
(Data_encoding.obj3
(Data_encoding.req None None "public_key"
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
(Data_encoding.req None None "expected_hash"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "provided_hash"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_hash" then
let '{|
Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := provided_hash
|} := cast Inconsistent_hash payload in
Some (public_key, expected_hash, provided_hash)
else None
end)
(fun (function_parameter :
Signature.public_key × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(public_key, expected_hash, provided_hash) := function_parameter in
Build_extensible "Inconsistent_hash" Inconsistent_hash
{| Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := provided_hash; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"contract.previously_revealed_key" "Manager operation already revealed"
"One tried to reveal twice a manager public key"
(Some
(fun (ppf : Format.formatter) ⇒
fun (s_value : Contract_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Previously revealed manager key for contract "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Previously revealed manager key for contract %a.")
Contract_repr.pp s_value))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Contract_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Previously_revealed_key" then
let s_value := cast Contract_repr.t payload in
Some s_value
else None
end)
(fun (s_value : Contract_repr.t) ⇒
Build_extensible "Previously_revealed_key" Contract_repr.t s_value) in
Error_monad.register_error_kind Error_monad.Branch
"contract.missing_manager_contract" "Missing manager contract"
"The manager contract is missing from the storage"
(Some
(fun (ppf : Format.formatter) ⇒
fun (s_value : Contract_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The contract "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is missing from the storage."
CamlinternalFormatBasics.End_of_format)))
"The contract %a is missing from the storage.") Contract_repr.pp
s_value))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Contract_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Missing_manager_contract" then
let s_value := cast Contract_repr.t payload in
Some s_value
else None
end)
(fun (s_value : Contract_repr.t) ⇒
Build_extensible "Missing_manager_contract" Contract_repr.t s_value).
Definition init_value
: Raw_context.t → Contract_repr.t → Manager_repr.manager_key →
M? Raw_context.t :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.init_value).
Definition is_manager_key_revealed
(c_value : Raw_context.t) (manager : Signature.public_key_hash) : M? bool :=
let contract := Contract_repr.Implicit manager in
let? function_parameter :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.find)
c_value contract in
match function_parameter with
| None ⇒ Error_monad.return_false
| Some (Manager_repr.Hash _) ⇒ Error_monad.return_false
| Some (Manager_repr.Public_key _) ⇒ Error_monad.return_true
end.
Definition check_public_key
(public_key : Signature.public_key)
(expected_hash : Signature.public_key_hash) : M? unit :=
let provided_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) public_key in
Error_monad.error_unless
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) provided_hash
expected_hash)
(Build_extensible "Inconsistent_hash" Inconsistent_hash
{| Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := provided_hash; |}).
Definition reveal_manager_key (op_staroptstar : option bool)
: Raw_context.t → Signature.public_key_hash → Signature.public_key →
M? Raw_context.t :=
let check_consistency :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ true
end in
fun (c_value : Raw_context.t) ⇒
fun (manager : Signature.public_key_hash) ⇒
fun (public_key : Signature.public_key) ⇒
let contract := Contract_repr.Implicit manager in
let? function_parameter :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.get)
c_value contract in
match function_parameter with
| Manager_repr.Public_key _ ⇒
Error_monad.tzfail
(Build_extensible "Previously_revealed_key" Contract_repr.t contract)
| Manager_repr.Hash expected_hash ⇒
let? '_ :=
Error_monad.error_unless
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
manager expected_hash)
(Build_extensible "Inconsistent_hash" Inconsistent_hash
{| Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := manager; |}) in
let? '_ :=
Error_monad.when_ check_consistency
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
check_public_key public_key expected_hash) in
let pk := Manager_repr.Public_key public_key in
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.update)
c_value contract pk
end.
Definition get_manager_key
(error_value : option Error_monad._error) (ctxt : Raw_context.t)
(pkh : Signature.public_key_hash) : M? Signature.public_key :=
let contract := Contract_repr.Implicit pkh in
let? function_parameter :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.find)
ctxt contract in
match function_parameter with
| None ⇒
match error_value with
| None ⇒
Error_monad.tzfail
(Build_extensible "Missing_manager_contract" Contract_repr.t contract)
| Some error_value ⇒ Error_monad.tzfail error_value
end
| Some (Manager_repr.Hash _) ⇒
match error_value with
| None ⇒
Error_monad.tzfail
(Build_extensible "Unrevealed_manager_key" Contract_repr.t contract)
| Some error_value ⇒ Error_monad.tzfail error_value
end
| Some (Manager_repr.Public_key pk) ⇒ return? pk
end.
Definition remove_existing
: Raw_context.t → Contract_repr.t → M? Raw_context.t :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing).
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "contract.unrevealed_key"
"Manager operation precedes key revelation"
"One tried to apply a manager operation without revealing the manager public key"
(Some
(fun (ppf : Format.formatter) ⇒
fun (s_value : Contract_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unrevealed manager key for contract "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Unrevealed manager key for contract %a.") Contract_repr.pp
s_value))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Contract_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unrevealed_manager_key" then
let s_value := cast Contract_repr.t payload in
Some s_value
else None
end)
(fun (s_value : Contract_repr.t) ⇒
Build_extensible "Unrevealed_manager_key" Contract_repr.t s_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"contract.manager.inconsistent_hash" "Inconsistent public key hash"
"A revealed manager public key is inconsistent with the announced hash"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(k_value, eh, ph) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The hash of the manager public key "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " is not "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" as announced but "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))
"The hash of the manager public key %s is not %a as announced but %a")
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.to_b58check) k_value)
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) ph
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) eh))
(Data_encoding.obj3
(Data_encoding.req None None "public_key"
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
(Data_encoding.req None None "expected_hash"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "provided_hash"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_hash" then
let '{|
Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := provided_hash
|} := cast Inconsistent_hash payload in
Some (public_key, expected_hash, provided_hash)
else None
end)
(fun (function_parameter :
Signature.public_key × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(public_key, expected_hash, provided_hash) := function_parameter in
Build_extensible "Inconsistent_hash" Inconsistent_hash
{| Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := provided_hash; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"contract.previously_revealed_key" "Manager operation already revealed"
"One tried to reveal twice a manager public key"
(Some
(fun (ppf : Format.formatter) ⇒
fun (s_value : Contract_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Previously revealed manager key for contract "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Previously revealed manager key for contract %a.")
Contract_repr.pp s_value))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Contract_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Previously_revealed_key" then
let s_value := cast Contract_repr.t payload in
Some s_value
else None
end)
(fun (s_value : Contract_repr.t) ⇒
Build_extensible "Previously_revealed_key" Contract_repr.t s_value) in
Error_monad.register_error_kind Error_monad.Branch
"contract.missing_manager_contract" "Missing manager contract"
"The manager contract is missing from the storage"
(Some
(fun (ppf : Format.formatter) ⇒
fun (s_value : Contract_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The contract "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is missing from the storage."
CamlinternalFormatBasics.End_of_format)))
"The contract %a is missing from the storage.") Contract_repr.pp
s_value))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Contract_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Missing_manager_contract" then
let s_value := cast Contract_repr.t payload in
Some s_value
else None
end)
(fun (s_value : Contract_repr.t) ⇒
Build_extensible "Missing_manager_contract" Contract_repr.t s_value).
Definition init_value
: Raw_context.t → Contract_repr.t → Manager_repr.manager_key →
M? Raw_context.t :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.init_value).
Definition is_manager_key_revealed
(c_value : Raw_context.t) (manager : Signature.public_key_hash) : M? bool :=
let contract := Contract_repr.Implicit manager in
let? function_parameter :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.find)
c_value contract in
match function_parameter with
| None ⇒ Error_monad.return_false
| Some (Manager_repr.Hash _) ⇒ Error_monad.return_false
| Some (Manager_repr.Public_key _) ⇒ Error_monad.return_true
end.
Definition check_public_key
(public_key : Signature.public_key)
(expected_hash : Signature.public_key_hash) : M? unit :=
let provided_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) public_key in
Error_monad.error_unless
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) provided_hash
expected_hash)
(Build_extensible "Inconsistent_hash" Inconsistent_hash
{| Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := provided_hash; |}).
Definition reveal_manager_key (op_staroptstar : option bool)
: Raw_context.t → Signature.public_key_hash → Signature.public_key →
M? Raw_context.t :=
let check_consistency :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ true
end in
fun (c_value : Raw_context.t) ⇒
fun (manager : Signature.public_key_hash) ⇒
fun (public_key : Signature.public_key) ⇒
let contract := Contract_repr.Implicit manager in
let? function_parameter :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.get)
c_value contract in
match function_parameter with
| Manager_repr.Public_key _ ⇒
Error_monad.tzfail
(Build_extensible "Previously_revealed_key" Contract_repr.t contract)
| Manager_repr.Hash expected_hash ⇒
let? '_ :=
Error_monad.error_unless
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
manager expected_hash)
(Build_extensible "Inconsistent_hash" Inconsistent_hash
{| Inconsistent_hash.public_key := public_key;
Inconsistent_hash.expected_hash := expected_hash;
Inconsistent_hash.provided_hash := manager; |}) in
let? '_ :=
Error_monad.when_ check_consistency
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
check_public_key public_key expected_hash) in
let pk := Manager_repr.Public_key public_key in
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.update)
c_value contract pk
end.
Definition get_manager_key
(error_value : option Error_monad._error) (ctxt : Raw_context.t)
(pkh : Signature.public_key_hash) : M? Signature.public_key :=
let contract := Contract_repr.Implicit pkh in
let? function_parameter :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.find)
ctxt contract in
match function_parameter with
| None ⇒
match error_value with
| None ⇒
Error_monad.tzfail
(Build_extensible "Missing_manager_contract" Contract_repr.t contract)
| Some error_value ⇒ Error_monad.tzfail error_value
end
| Some (Manager_repr.Hash _) ⇒
match error_value with
| None ⇒
Error_monad.tzfail
(Build_extensible "Unrevealed_manager_key" Contract_repr.t contract)
| Some error_value ⇒ Error_monad.tzfail error_value
end
| Some (Manager_repr.Public_key pk) ⇒ return? pk
end.
Definition remove_existing
: Raw_context.t → Contract_repr.t → M? Raw_context.t :=
Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing).