🕹️ Parameters_repr.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.Commitment_repr.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Module bootstrap_account.
Record record : Set := Build {
public_key_hash : Signature.public_key_hash;
public_key : option Signature.public_key;
amount : Tez_repr.t;
delegate_to : option Signature.public_key_hash;
consensus_key : option Signature.public_key;
}.
Definition with_public_key_hash public_key_hash (r : record) :=
Build public_key_hash r.(public_key) r.(amount) r.(delegate_to)
r.(consensus_key).
Definition with_public_key public_key (r : record) :=
Build r.(public_key_hash) public_key r.(amount) r.(delegate_to)
r.(consensus_key).
Definition with_amount amount (r : record) :=
Build r.(public_key_hash) r.(public_key) amount r.(delegate_to)
r.(consensus_key).
Definition with_delegate_to delegate_to (r : record) :=
Build r.(public_key_hash) r.(public_key) r.(amount) delegate_to
r.(consensus_key).
Definition with_consensus_key consensus_key (r : record) :=
Build r.(public_key_hash) r.(public_key) r.(amount) r.(delegate_to)
consensus_key.
End bootstrap_account.
Definition bootstrap_account := bootstrap_account.record.
Module bootstrap_contract.
Record record : Set := Build {
delegate : option Signature.public_key_hash;
amount : Tez_repr.t;
script : Script_repr.t;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(amount) r.(script).
Definition with_amount amount (r : record) :=
Build r.(delegate) amount r.(script).
Definition with_script script (r : record) :=
Build r.(delegate) r.(amount) script.
End bootstrap_contract.
Definition bootstrap_contract := bootstrap_contract.record.
Module t.
Record record : Set := Build {
bootstrap_accounts : list bootstrap_account;
bootstrap_contracts : list bootstrap_contract;
commitments : list Commitment_repr.t;
constants : Constants_parametric_repr.t;
security_deposit_ramp_up_cycles : option int;
no_reward_cycles : option int;
}.
Definition with_bootstrap_accounts bootstrap_accounts (r : record) :=
Build bootstrap_accounts r.(bootstrap_contracts) r.(commitments)
r.(constants) r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_bootstrap_contracts bootstrap_contracts (r : record) :=
Build r.(bootstrap_accounts) bootstrap_contracts r.(commitments)
r.(constants) r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_commitments commitments (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) commitments
r.(constants) r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_constants constants (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) r.(commitments)
constants r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_security_deposit_ramp_up_cycles
security_deposit_ramp_up_cycles (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) r.(commitments)
r.(constants) security_deposit_ramp_up_cycles r.(no_reward_cycles).
Definition with_no_reward_cycles no_reward_cycles (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) r.(commitments)
r.(constants) r.(security_deposit_ramp_up_cycles) no_reward_cycles.
End t.
Definition t := t.record.
Definition bootstrap_account_encoding
: Data_encoding.encoding bootstrap_account :=
Data_encoding.union None
[
Data_encoding.case_value "Public_key_known" None (Data_encoding.Tag 0)
(Data_encoding.tup2
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
Tez_repr.encoding)
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None
|} ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key) public_key_hash) in
Some (public_key, amount)
|
({| bootstrap_account.public_key := None |} | {|
bootstrap_account.delegate_to := Some _ |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter : Signature.public_key × Tez_repr.t) ⇒
let '(public_key, amount) := function_parameter in
{|
bootstrap_account.public_key_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_unknown" None (Data_encoding.Tag 1)
(Data_encoding.tup2
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
Tez_repr.encoding)
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None
|} ⇒ Some (public_key_hash, amount)
|
({| bootstrap_account.public_key := Some _ |} | {|
bootstrap_account.delegate_to := Some _ |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(public_key_hash, amount) := function_parameter in
{| bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_known_with_delegate" None
(Data_encoding.Tag 2)
(Data_encoding.tup3
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
Tez_repr.encoding
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None
|} ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key) public_key_hash) in
Some (public_key, amount, delegate)
|
({| bootstrap_account.public_key := None |} | {|
bootstrap_account.delegate_to := None |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter :
Signature.public_key × Tez_repr.t × Signature.public_key_hash) ⇒
let '(public_key, amount, delegate) := function_parameter in
{|
bootstrap_account.public_key_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_unknown_with_delegate" None
(Data_encoding.Tag 3)
(Data_encoding.tup3
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
Tez_repr.encoding
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None
|} ⇒ Some (public_key_hash, amount, delegate)
|
({| bootstrap_account.public_key := Some _ |} | {|
bootstrap_account.delegate_to := None |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter :
Signature.public_key_hash × Tez_repr.t × Signature.public_key_hash)
⇒
let '(public_key_hash, amount, delegate) := function_parameter in
{| bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_known_with_consensus_key" None
(Data_encoding.Tag 4)
(Data_encoding.tup3
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
Tez_repr.encoding
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := Some consensus_key
|} ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key) public_key_hash) in
Some (public_key, amount, consensus_key)
|
({| bootstrap_account.public_key := None |} | {|
bootstrap_account.delegate_to := Some _ |} | {|
bootstrap_account.consensus_key := None |}) ⇒ None
end)
(fun (function_parameter :
Signature.public_key × Tez_repr.t × Signature.public_key) ⇒
let '(public_key, amount, consensus_key) := function_parameter in
{|
bootstrap_account.public_key_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := Some consensus_key; |})
].
Definition bootstrap_contract_encoding
: Data_encoding.encoding bootstrap_contract :=
Data_encoding.conv
(fun (function_parameter : bootstrap_contract) ⇒
let '{|
bootstrap_contract.delegate := delegate;
bootstrap_contract.amount := amount;
bootstrap_contract.script := script
|} := function_parameter in
(delegate, amount, script))
(fun (function_parameter :
option Signature.public_key_hash × Tez_repr.t × Script_repr.t) ⇒
let '(delegate, amount, script) := function_parameter in
{| bootstrap_contract.delegate := delegate;
bootstrap_contract.amount := amount;
bootstrap_contract.script := script; |}) None
(Data_encoding.obj3
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "amount" Tez_repr.encoding)
(Data_encoding.req None None "script" Script_repr.encoding)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.bootstrap_accounts := bootstrap_accounts;
t.bootstrap_contracts := bootstrap_contracts;
t.commitments := commitments;
t.constants := constants;
t.security_deposit_ramp_up_cycles := security_deposit_ramp_up_cycles;
t.no_reward_cycles := no_reward_cycles
|} := function_parameter in
((bootstrap_accounts, bootstrap_contracts, commitments,
security_deposit_ramp_up_cycles, no_reward_cycles), constants))
(fun (function_parameter :
(list bootstrap_account × list bootstrap_contract × list Commitment_repr.t
× option int × option int) × Constants_parametric_repr.t) ⇒
let
'((bootstrap_accounts, bootstrap_contracts, commitments,
security_deposit_ramp_up_cycles, no_reward_cycles), constants) :=
function_parameter in
{| t.bootstrap_accounts := bootstrap_accounts;
t.bootstrap_contracts := bootstrap_contracts;
t.commitments := commitments; t.constants := constants;
t.security_deposit_ramp_up_cycles := security_deposit_ramp_up_cycles;
t.no_reward_cycles := no_reward_cycles; |}) None
(Data_encoding.merge_objs
(Data_encoding.obj5
(Data_encoding.req None None "bootstrap_accounts"
(Data_encoding.list_value None bootstrap_account_encoding))
(Data_encoding.dft None None "bootstrap_contracts"
(Data_encoding.list_value None bootstrap_contract_encoding) nil)
(Data_encoding.dft None None "commitments"
(Data_encoding.list_value None Commitment_repr.encoding) nil)
(Data_encoding.opt None None "security_deposit_ramp_up_cycles"
Data_encoding.int31)
(Data_encoding.opt None None "no_reward_cycles" Data_encoding.int31))
Constants_parametric_repr.encoding).
Definition check_params (params : t) : M? unit :=
Constants_repr.check_constants params.(t.constants).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Commitment_repr.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Module bootstrap_account.
Record record : Set := Build {
public_key_hash : Signature.public_key_hash;
public_key : option Signature.public_key;
amount : Tez_repr.t;
delegate_to : option Signature.public_key_hash;
consensus_key : option Signature.public_key;
}.
Definition with_public_key_hash public_key_hash (r : record) :=
Build public_key_hash r.(public_key) r.(amount) r.(delegate_to)
r.(consensus_key).
Definition with_public_key public_key (r : record) :=
Build r.(public_key_hash) public_key r.(amount) r.(delegate_to)
r.(consensus_key).
Definition with_amount amount (r : record) :=
Build r.(public_key_hash) r.(public_key) amount r.(delegate_to)
r.(consensus_key).
Definition with_delegate_to delegate_to (r : record) :=
Build r.(public_key_hash) r.(public_key) r.(amount) delegate_to
r.(consensus_key).
Definition with_consensus_key consensus_key (r : record) :=
Build r.(public_key_hash) r.(public_key) r.(amount) r.(delegate_to)
consensus_key.
End bootstrap_account.
Definition bootstrap_account := bootstrap_account.record.
Module bootstrap_contract.
Record record : Set := Build {
delegate : option Signature.public_key_hash;
amount : Tez_repr.t;
script : Script_repr.t;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(amount) r.(script).
Definition with_amount amount (r : record) :=
Build r.(delegate) amount r.(script).
Definition with_script script (r : record) :=
Build r.(delegate) r.(amount) script.
End bootstrap_contract.
Definition bootstrap_contract := bootstrap_contract.record.
Module t.
Record record : Set := Build {
bootstrap_accounts : list bootstrap_account;
bootstrap_contracts : list bootstrap_contract;
commitments : list Commitment_repr.t;
constants : Constants_parametric_repr.t;
security_deposit_ramp_up_cycles : option int;
no_reward_cycles : option int;
}.
Definition with_bootstrap_accounts bootstrap_accounts (r : record) :=
Build bootstrap_accounts r.(bootstrap_contracts) r.(commitments)
r.(constants) r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_bootstrap_contracts bootstrap_contracts (r : record) :=
Build r.(bootstrap_accounts) bootstrap_contracts r.(commitments)
r.(constants) r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_commitments commitments (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) commitments
r.(constants) r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_constants constants (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) r.(commitments)
constants r.(security_deposit_ramp_up_cycles) r.(no_reward_cycles).
Definition with_security_deposit_ramp_up_cycles
security_deposit_ramp_up_cycles (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) r.(commitments)
r.(constants) security_deposit_ramp_up_cycles r.(no_reward_cycles).
Definition with_no_reward_cycles no_reward_cycles (r : record) :=
Build r.(bootstrap_accounts) r.(bootstrap_contracts) r.(commitments)
r.(constants) r.(security_deposit_ramp_up_cycles) no_reward_cycles.
End t.
Definition t := t.record.
Definition bootstrap_account_encoding
: Data_encoding.encoding bootstrap_account :=
Data_encoding.union None
[
Data_encoding.case_value "Public_key_known" None (Data_encoding.Tag 0)
(Data_encoding.tup2
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
Tez_repr.encoding)
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None
|} ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key) public_key_hash) in
Some (public_key, amount)
|
({| bootstrap_account.public_key := None |} | {|
bootstrap_account.delegate_to := Some _ |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter : Signature.public_key × Tez_repr.t) ⇒
let '(public_key, amount) := function_parameter in
{|
bootstrap_account.public_key_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_unknown" None (Data_encoding.Tag 1)
(Data_encoding.tup2
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
Tez_repr.encoding)
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None
|} ⇒ Some (public_key_hash, amount)
|
({| bootstrap_account.public_key := Some _ |} | {|
bootstrap_account.delegate_to := Some _ |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(public_key_hash, amount) := function_parameter in
{| bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_known_with_delegate" None
(Data_encoding.Tag 2)
(Data_encoding.tup3
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
Tez_repr.encoding
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None
|} ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key) public_key_hash) in
Some (public_key, amount, delegate)
|
({| bootstrap_account.public_key := None |} | {|
bootstrap_account.delegate_to := None |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter :
Signature.public_key × Tez_repr.t × Signature.public_key_hash) ⇒
let '(public_key, amount, delegate) := function_parameter in
{|
bootstrap_account.public_key_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_unknown_with_delegate" None
(Data_encoding.Tag 3)
(Data_encoding.tup3
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
Tez_repr.encoding
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None
|} ⇒ Some (public_key_hash, amount, delegate)
|
({| bootstrap_account.public_key := Some _ |} | {|
bootstrap_account.delegate_to := None |} | {|
bootstrap_account.consensus_key := Some _ |}) ⇒ None
end)
(fun (function_parameter :
Signature.public_key_hash × Tez_repr.t × Signature.public_key_hash)
⇒
let '(public_key_hash, amount, delegate) := function_parameter in
{| bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := None;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := Some delegate;
bootstrap_account.consensus_key := None; |});
Data_encoding.case_value "Public_key_known_with_consensus_key" None
(Data_encoding.Tag 4)
(Data_encoding.tup3
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
Tez_repr.encoding
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
(fun (function_parameter : bootstrap_account) ⇒
match function_parameter with
| {|
bootstrap_account.public_key_hash := public_key_hash;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := Some consensus_key
|} ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
(Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key) public_key_hash) in
Some (public_key, amount, consensus_key)
|
({| bootstrap_account.public_key := None |} | {|
bootstrap_account.delegate_to := Some _ |} | {|
bootstrap_account.consensus_key := None |}) ⇒ None
end)
(fun (function_parameter :
Signature.public_key × Tez_repr.t × Signature.public_key) ⇒
let '(public_key, amount, consensus_key) := function_parameter in
{|
bootstrap_account.public_key_hash :=
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
public_key;
bootstrap_account.public_key := Some public_key;
bootstrap_account.amount := amount;
bootstrap_account.delegate_to := None;
bootstrap_account.consensus_key := Some consensus_key; |})
].
Definition bootstrap_contract_encoding
: Data_encoding.encoding bootstrap_contract :=
Data_encoding.conv
(fun (function_parameter : bootstrap_contract) ⇒
let '{|
bootstrap_contract.delegate := delegate;
bootstrap_contract.amount := amount;
bootstrap_contract.script := script
|} := function_parameter in
(delegate, amount, script))
(fun (function_parameter :
option Signature.public_key_hash × Tez_repr.t × Script_repr.t) ⇒
let '(delegate, amount, script) := function_parameter in
{| bootstrap_contract.delegate := delegate;
bootstrap_contract.amount := amount;
bootstrap_contract.script := script; |}) None
(Data_encoding.obj3
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "amount" Tez_repr.encoding)
(Data_encoding.req None None "script" Script_repr.encoding)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.bootstrap_accounts := bootstrap_accounts;
t.bootstrap_contracts := bootstrap_contracts;
t.commitments := commitments;
t.constants := constants;
t.security_deposit_ramp_up_cycles := security_deposit_ramp_up_cycles;
t.no_reward_cycles := no_reward_cycles
|} := function_parameter in
((bootstrap_accounts, bootstrap_contracts, commitments,
security_deposit_ramp_up_cycles, no_reward_cycles), constants))
(fun (function_parameter :
(list bootstrap_account × list bootstrap_contract × list Commitment_repr.t
× option int × option int) × Constants_parametric_repr.t) ⇒
let
'((bootstrap_accounts, bootstrap_contracts, commitments,
security_deposit_ramp_up_cycles, no_reward_cycles), constants) :=
function_parameter in
{| t.bootstrap_accounts := bootstrap_accounts;
t.bootstrap_contracts := bootstrap_contracts;
t.commitments := commitments; t.constants := constants;
t.security_deposit_ramp_up_cycles := security_deposit_ramp_up_cycles;
t.no_reward_cycles := no_reward_cycles; |}) None
(Data_encoding.merge_objs
(Data_encoding.obj5
(Data_encoding.req None None "bootstrap_accounts"
(Data_encoding.list_value None bootstrap_account_encoding))
(Data_encoding.dft None None "bootstrap_contracts"
(Data_encoding.list_value None bootstrap_contract_encoding) nil)
(Data_encoding.dft None None "commitments"
(Data_encoding.list_value None Commitment_repr.encoding) nil)
(Data_encoding.opt None None "security_deposit_ramp_up_cycles"
Data_encoding.int31)
(Data_encoding.opt None None "no_reward_cycles" Data_encoding.int31))
Constants_parametric_repr.encoding).
Definition check_params (params : t) : M? unit :=
Constants_repr.check_constants params.(t.constants).