🐣 Bootstrap_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.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.
Init function; without side-effects in Coq
Definition init_module : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"bootstrap.unrevealed_public_key"
"Forbidden delegation from unrevealed public key"
"Tried to delegate from an unrevealed public key"
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Delegation from an unrevealed public key (for "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ") is forbidden."
CamlinternalFormatBasics.End_of_format)))
"Delegation from an unrevealed public key (for %a) is forbidden.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegator"
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 "Unrevealed_public_key" then
let pkh := cast Signature.public_key_hash payload in
Some pkh
else None
end)
(fun (pkh : Signature.public_key_hash) ⇒
Build_extensible "Unrevealed_public_key" Signature.public_key_hash pkh).
Definition init_account
(function_parameter :
Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin))
: Parameters_repr.bootstrap_account →
M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let '(ctxt, balance_updates) := function_parameter in
fun (function_parameter : Parameters_repr.bootstrap_account) ⇒
let '{|
Parameters_repr.bootstrap_account.public_key_hash := public_key_hash;
Parameters_repr.bootstrap_account.public_key := public_key;
Parameters_repr.bootstrap_account.amount := amount;
Parameters_repr.bootstrap_account.delegate_to := delegate_to;
Parameters_repr.bootstrap_account.consensus_key := consensus_key
|} := function_parameter in
let contract := Contract_repr.Implicit public_key_hash in
let? '(ctxt, new_balance_updates) :=
Token.transfer (Some Receipt_repr.Protocol_migration) ctxt
(Token.Source_infinite Token.Bootstrap)
(Token.Sink_container (Token.Contract contract)) amount in
let? ctxt :=
match public_key with
| Some public_key ⇒
let? ctxt :=
Contract_manager_storage.reveal_manager_key None ctxt public_key_hash
public_key in
let? ctxt :=
Delegate_storage.Contract.set ctxt contract
(Some (Option.value_value delegate_to public_key_hash)) in
match consensus_key with
| None ⇒ return? ctxt
| Some consensus_key ⇒
Delegate_consensus_key.init_value ctxt public_key_hash consensus_key
end
| None ⇒
let? '_ :=
Error_monad.fail_when (Option.is_some delegate_to)
(Build_extensible "Unrevealed_public_key" Signature.public_key_hash
public_key_hash) in
return? ctxt
end in
return? (ctxt, (Pervasives.op_at new_balance_updates balance_updates)).
Definition init_contract
(typecheck :
Raw_context.t → Script_repr.t →
M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
(function_parameter :
Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin))
: Parameters_repr.bootstrap_contract →
M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let '(ctxt, balance_updates) := function_parameter in
fun (function_parameter : Parameters_repr.bootstrap_contract) ⇒
let '{|
Parameters_repr.bootstrap_contract.delegate := delegate;
Parameters_repr.bootstrap_contract.amount := amount;
Parameters_repr.bootstrap_contract.script := script
|} := function_parameter in
let? '(ctxt, contract_hash) :=
Contract_storage.fresh_contract_from_current_nonce ctxt in
let? '(script, ctxt) := typecheck ctxt script in
let? ctxt := Contract_storage.raw_originate ctxt true contract_hash script
in
let contract := Contract_repr.Originated contract_hash in
let? ctxt :=
match delegate with
| None ⇒ return? ctxt
| Some delegate ⇒
Delegate_storage.Contract.init_value ctxt contract delegate
end in
let origin := Receipt_repr.Protocol_migration in
let? '(ctxt, new_balance_updates) :=
Token.transfer (Some origin) ctxt (Token.Source_infinite Token.Bootstrap)
(Token.Sink_container (Token.Contract contract)) amount in
return? (ctxt, (Pervasives.op_at new_balance_updates balance_updates)).
Definition init_value
(ctxt : Raw_context.t)
(typecheck :
Raw_context.t → Script_repr.t →
M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
(no_reward_cycles : option int)
(accounts : list Parameters_repr.bootstrap_account)
(contracts : list Parameters_repr.bootstrap_contract)
: M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let nonce_value := Operation_hash.hash_string None [ "Un festival de GADT." ]
in
let ctxt := Raw_context.init_origination_nonce ctxt nonce_value in
let? '(ctxt, balance_updates) :=
List.fold_left_es init_account (ctxt, nil) accounts in
let? '(ctxt, balance_updates) :=
List.fold_left_es (init_contract typecheck) (ctxt, balance_updates)
contracts in
let? ctxt :=
match no_reward_cycles with
| None ⇒ return? ctxt
| Some cycles ⇒
let constants := Raw_context.constants ctxt in
let ctxt :=
Raw_context.patch_constants ctxt
(fun (c_value : Constants_parametric_repr.t) ⇒
Constants_parametric_repr.t.with_endorsing_reward_per_slot
Tez_repr.zero
(Constants_parametric_repr.t.with_baking_reward_bonus_per_slot
Tez_repr.zero
(Constants_parametric_repr.t.with_baking_reward_fixed_portion
Tez_repr.zero c_value))) in
Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.init_value)
ctxt (Cycle_repr.of_int32_exn (Int32.of_int cycles))
{|
Storage.Ramp_up.reward.baking_reward_fixed_portion :=
constants.(Constants_parametric_repr.t.baking_reward_fixed_portion);
Storage.Ramp_up.reward.baking_reward_bonus_per_slot :=
constants.(Constants_parametric_repr.t.baking_reward_bonus_per_slot);
Storage.Ramp_up.reward.endorsing_reward_per_slot :=
constants.(Constants_parametric_repr.t.endorsing_reward_per_slot);
|}
end in
return? (ctxt, balance_updates).
Definition cycle_end (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
: M? Raw_context.t :=
let next_cycle := Cycle_repr.succ last_cycle in
let? function_parameter :=
Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.find) ctxt
next_cycle in
match function_parameter with
| None ⇒ return? ctxt
|
Some {|
Storage.Ramp_up.reward.baking_reward_fixed_portion :=
baking_reward_fixed_portion;
Storage.Ramp_up.reward.baking_reward_bonus_per_slot :=
baking_reward_bonus_per_slot;
Storage.Ramp_up.reward.endorsing_reward_per_slot :=
endorsing_reward_per_slot
|} ⇒
let? ctxt :=
Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt next_cycle in
Error_monad.op_gtpipeeq
(Raw_context.patch_constants ctxt
(fun (c_value : Constants_parametric_repr.t) ⇒
Constants_parametric_repr.t.with_endorsing_reward_per_slot
endorsing_reward_per_slot
(Constants_parametric_repr.t.with_baking_reward_bonus_per_slot
baking_reward_bonus_per_slot
(Constants_parametric_repr.t.with_baking_reward_fixed_portion
baking_reward_fixed_portion c_value)))) Error_monad.ok
end.
Error_monad.register_error_kind Error_monad.Permanent
"bootstrap.unrevealed_public_key"
"Forbidden delegation from unrevealed public key"
"Tried to delegate from an unrevealed public key"
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Delegation from an unrevealed public key (for "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ") is forbidden."
CamlinternalFormatBasics.End_of_format)))
"Delegation from an unrevealed public key (for %a) is forbidden.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegator"
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 "Unrevealed_public_key" then
let pkh := cast Signature.public_key_hash payload in
Some pkh
else None
end)
(fun (pkh : Signature.public_key_hash) ⇒
Build_extensible "Unrevealed_public_key" Signature.public_key_hash pkh).
Definition init_account
(function_parameter :
Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin))
: Parameters_repr.bootstrap_account →
M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let '(ctxt, balance_updates) := function_parameter in
fun (function_parameter : Parameters_repr.bootstrap_account) ⇒
let '{|
Parameters_repr.bootstrap_account.public_key_hash := public_key_hash;
Parameters_repr.bootstrap_account.public_key := public_key;
Parameters_repr.bootstrap_account.amount := amount;
Parameters_repr.bootstrap_account.delegate_to := delegate_to;
Parameters_repr.bootstrap_account.consensus_key := consensus_key
|} := function_parameter in
let contract := Contract_repr.Implicit public_key_hash in
let? '(ctxt, new_balance_updates) :=
Token.transfer (Some Receipt_repr.Protocol_migration) ctxt
(Token.Source_infinite Token.Bootstrap)
(Token.Sink_container (Token.Contract contract)) amount in
let? ctxt :=
match public_key with
| Some public_key ⇒
let? ctxt :=
Contract_manager_storage.reveal_manager_key None ctxt public_key_hash
public_key in
let? ctxt :=
Delegate_storage.Contract.set ctxt contract
(Some (Option.value_value delegate_to public_key_hash)) in
match consensus_key with
| None ⇒ return? ctxt
| Some consensus_key ⇒
Delegate_consensus_key.init_value ctxt public_key_hash consensus_key
end
| None ⇒
let? '_ :=
Error_monad.fail_when (Option.is_some delegate_to)
(Build_extensible "Unrevealed_public_key" Signature.public_key_hash
public_key_hash) in
return? ctxt
end in
return? (ctxt, (Pervasives.op_at new_balance_updates balance_updates)).
Definition init_contract
(typecheck :
Raw_context.t → Script_repr.t →
M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
(function_parameter :
Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin))
: Parameters_repr.bootstrap_contract →
M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let '(ctxt, balance_updates) := function_parameter in
fun (function_parameter : Parameters_repr.bootstrap_contract) ⇒
let '{|
Parameters_repr.bootstrap_contract.delegate := delegate;
Parameters_repr.bootstrap_contract.amount := amount;
Parameters_repr.bootstrap_contract.script := script
|} := function_parameter in
let? '(ctxt, contract_hash) :=
Contract_storage.fresh_contract_from_current_nonce ctxt in
let? '(script, ctxt) := typecheck ctxt script in
let? ctxt := Contract_storage.raw_originate ctxt true contract_hash script
in
let contract := Contract_repr.Originated contract_hash in
let? ctxt :=
match delegate with
| None ⇒ return? ctxt
| Some delegate ⇒
Delegate_storage.Contract.init_value ctxt contract delegate
end in
let origin := Receipt_repr.Protocol_migration in
let? '(ctxt, new_balance_updates) :=
Token.transfer (Some origin) ctxt (Token.Source_infinite Token.Bootstrap)
(Token.Sink_container (Token.Contract contract)) amount in
return? (ctxt, (Pervasives.op_at new_balance_updates balance_updates)).
Definition init_value
(ctxt : Raw_context.t)
(typecheck :
Raw_context.t → Script_repr.t →
M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
(no_reward_cycles : option int)
(accounts : list Parameters_repr.bootstrap_account)
(contracts : list Parameters_repr.bootstrap_contract)
: M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let nonce_value := Operation_hash.hash_string None [ "Un festival de GADT." ]
in
let ctxt := Raw_context.init_origination_nonce ctxt nonce_value in
let? '(ctxt, balance_updates) :=
List.fold_left_es init_account (ctxt, nil) accounts in
let? '(ctxt, balance_updates) :=
List.fold_left_es (init_contract typecheck) (ctxt, balance_updates)
contracts in
let? ctxt :=
match no_reward_cycles with
| None ⇒ return? ctxt
| Some cycles ⇒
let constants := Raw_context.constants ctxt in
let ctxt :=
Raw_context.patch_constants ctxt
(fun (c_value : Constants_parametric_repr.t) ⇒
Constants_parametric_repr.t.with_endorsing_reward_per_slot
Tez_repr.zero
(Constants_parametric_repr.t.with_baking_reward_bonus_per_slot
Tez_repr.zero
(Constants_parametric_repr.t.with_baking_reward_fixed_portion
Tez_repr.zero c_value))) in
Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.init_value)
ctxt (Cycle_repr.of_int32_exn (Int32.of_int cycles))
{|
Storage.Ramp_up.reward.baking_reward_fixed_portion :=
constants.(Constants_parametric_repr.t.baking_reward_fixed_portion);
Storage.Ramp_up.reward.baking_reward_bonus_per_slot :=
constants.(Constants_parametric_repr.t.baking_reward_bonus_per_slot);
Storage.Ramp_up.reward.endorsing_reward_per_slot :=
constants.(Constants_parametric_repr.t.endorsing_reward_per_slot);
|}
end in
return? (ctxt, balance_updates).
Definition cycle_end (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
: M? Raw_context.t :=
let next_cycle := Cycle_repr.succ last_cycle in
let? function_parameter :=
Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.find) ctxt
next_cycle in
match function_parameter with
| None ⇒ return? ctxt
|
Some {|
Storage.Ramp_up.reward.baking_reward_fixed_portion :=
baking_reward_fixed_portion;
Storage.Ramp_up.reward.baking_reward_bonus_per_slot :=
baking_reward_bonus_per_slot;
Storage.Ramp_up.reward.endorsing_reward_per_slot :=
endorsing_reward_per_slot
|} ⇒
let? ctxt :=
Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt next_cycle in
Error_monad.op_gtpipeeq
(Raw_context.patch_constants ctxt
(fun (c_value : Constants_parametric_repr.t) ⇒
Constants_parametric_repr.t.with_endorsing_reward_per_slot
endorsing_reward_per_slot
(Constants_parametric_repr.t.with_baking_reward_bonus_per_slot
baking_reward_bonus_per_slot
(Constants_parametric_repr.t.with_baking_reward_fixed_portion
baking_reward_fixed_portion c_value)))) Error_monad.ok
end.