Skip to main content

🕹️ Parameters_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
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).