💾 Storage.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.V8.
Require TezosOfOCaml.Proto_alpha.Bitset.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Manager_counter_repr.
Require TezosOfOCaml.Proto_alpha.Manager_repr.
Require TezosOfOCaml.Proto_alpha.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_context_intf.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_data_version_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Storage_functors.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.

Module Encoding.
  Module UInt16.
    Definition t : Set := int.

    Definition encoding : Data_encoding.encoding int := Data_encoding.uint16.

    (* UInt16 *)
    Definition module :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End UInt16.
  Definition UInt16 : Storage_sigs.VALUE (t := int) := UInt16.module.

  Module Int32.
    Definition t : Set := Int32.t.

    Definition encoding : Data_encoding.encoding int32 :=
      Data_encoding.int32_value.

    (* Int32 *)
    Definition module :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End Int32.
  Definition Int32 : Storage_sigs.VALUE (t := Int32.t) := Int32.module.

  Module Int64.
    Definition t : Set := Int64.t.

    Definition encoding : Data_encoding.encoding int64 :=
      Data_encoding.int64_value.

    (* Int64 *)
    Definition module :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End Int64.
  Definition Int64 : Storage_sigs.VALUE (t := Int64.t) := Int64.module.

  Module Z.
    Definition t : Set := Z.t.

    Definition encoding : Data_encoding.encoding Z.t := Data_encoding.z_value.

    (* Z *)
    Definition module :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End Z.
  Definition Z : Storage_sigs.VALUE (t := Z.t) := Z.module.

  Module Manager_counter.
    Definition t : Set := Manager_counter_repr.t.

    Definition encoding : Data_encoding.t Manager_counter_repr.t :=
      Manager_counter_repr.encoding_for_storage.

    (* Manager_counter *)
    Definition module :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End Manager_counter.
  Definition Manager_counter : Storage_sigs.VALUE (t := Manager_counter_repr.t)
    := Manager_counter.module.
End Encoding.

Module Int31_index.
  Definition t : Set := int.

  Definition path_length : M? int := return? 1.

  Definition to_path (c_value : int) (l_value : list string) : list string :=
    cons (Pervasives.string_of_int c_value) l_value.

  Definition of_path (function_parameter : list string) : M? (option int) :=
    match function_parameter with
    | ([] | cons _ (cons _ _)) ⇒ return? None
    | cons c_value [] ⇒ return? (Pervasives.int_of_string_opt c_value)
    end.

  Definition ipath (a : Set) : Set := a × t.

  Definition args : Storage_description.args :=
    Storage_description.One
      {| Storage_description.args.One.rpc_arg := RPC_arg.int_value;
        Storage_description.args.One.encoding := Data_encoding.int31;
        Storage_description.args.One.compare := Compare.Int.compare; |}.

  (* Int31_index *)
  Definition module : Storage_functors.INDEX.signature (ipath := ipath) := {|
      Storage_functors.INDEX.to_path := to_path;
      Storage_functors.INDEX.of_path := of_path;
      Storage_functors.INDEX.path_length := path_length;
      Storage_functors.INDEX.args := args
    |}.
End Int31_index.
Definition Int31_index : Storage_functors.INDEX (t := int) (ipath := _) :=
  Int31_index.module.

Module Make_index.
  Class FArgs {H_t : Set} := {
    H : Storage_description.INDEX (t := H_t);
  }.
  Arguments Build_FArgs {_}.

Inclusion of the module [H]

  Definition t `{FArgs} := H.(Storage_description.INDEX.t).

  Definition to_path `{FArgs} := H.(Storage_description.INDEX.to_path).

  Definition of_path `{FArgs} := H.(Storage_description.INDEX.of_path).

  Definition path_length `{FArgs} := H.(Storage_description.INDEX.path_length).

  Definition rpc_arg `{FArgs} := H.(Storage_description.INDEX.rpc_arg).

  Definition encoding `{FArgs} := H.(Storage_description.INDEX.encoding).

  Definition compare `{FArgs} := H.(Storage_description.INDEX.compare).

  Definition ipath `{FArgs} (a : Set) : Set := a × t.

  Definition args `{FArgs} : Storage_description.args :=
    Storage_description.One
      {| Storage_description.args.One.rpc_arg := rpc_arg;
        Storage_description.args.One.encoding := encoding;
        Storage_description.args.One.compare := compare; |}.

  (* Make_index *)
  Definition functor `{FArgs} : Storage_functors.INDEX.signature (ipath := ipath) := {|
      Storage_functors.INDEX.to_path := to_path;
      Storage_functors.INDEX.of_path := of_path;
      Storage_functors.INDEX.path_length := path_length;
      Storage_functors.INDEX.args := args
    |}.
End Make_index.
Definition Make_index {H_t : Set} (H : Storage_description.INDEX (t := H_t))
  : Storage_functors.INDEX (t := H.(Storage_description.INDEX.t))
    (ipath := fun (a : Set) ⇒ a × H.(Storage_description.INDEX.t)) :=
  let '_ := Make_index.Build_FArgs H in
  Make_index.functor.

Module Simple_single_data_storage.
  Record signature {value : Set} : Set := {
    value := value;
    get : Raw_context.t → M? value;
    update : Raw_context.t → value → M? Raw_context.t;
    init_value : Raw_context.t → value → M? Raw_context.t;
  }.
End Simple_single_data_storage.
Definition Simple_single_data_storage := @Simple_single_data_storage.signature.
Arguments Simple_single_data_storage {_}.

Definition Block_round : Simple_single_data_storage (value := Round_repr.t) :=
  let functor_result :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "block_round" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Round_repr.encoding
      |} in
  {|
    Simple_single_data_storage.get :=
      functor_result.(Storage_sigs.Single_data_storage.get);
    Simple_single_data_storage.update :=
      functor_result.(Storage_sigs.Single_data_storage.update);
    Simple_single_data_storage.init_value :=
      functor_result.(Storage_sigs.Single_data_storage.init_value)
  |}.

Module Tenderbake.
  Definition First_level_of_protocol :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "first_level_of_protocol" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Raw_level_repr.encoding
      |}.

  Module Branch.
    Definition t : Set := Block_hash.t × Block_payload_hash.t.

    Definition encoding
      : Data_encoding.encoding (Block_hash.t × Block_payload_hash.t) :=
      Data_encoding.obj2
        (Data_encoding.req None None "grand_parent_hash" Block_hash.encoding)
        (Data_encoding.req None None "predecessor_payload"
          Block_payload_hash.encoding).

    (* Branch *)
    Definition module :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End Branch.
  Definition Branch := Branch.module.

  Definition Endorsement_branch :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "endorsement_branch" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Branch.

  Definition Grand_parent_branch :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "grand_parent_branch" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Branch.
End Tenderbake.

Module deposits.
  Record record : Set := Build {
    initial_amount : Tez_repr.t;
    current_amount : Tez_repr.t;
  }.
  Definition with_initial_amount initial_amount (r : record) :=
    Build initial_amount r.(current_amount).
  Definition with_current_amount current_amount (r : record) :=
    Build r.(initial_amount) current_amount.
End deposits.
Definition deposits := deposits.record.

Module Deposits.
  Definition t : Set := deposits.

  Definition encoding : Data_encoding.encoding deposits :=
    Data_encoding.conv
      (fun (function_parameter : deposits) ⇒
        let '{|
          deposits.initial_amount := initial_amount;
            deposits.current_amount := current_amount
            |} := function_parameter in
        (initial_amount, current_amount))
      (fun (function_parameter : Tez_repr.t × Tez_repr.t) ⇒
        let '(initial_amount, current_amount) := function_parameter in
        {| deposits.initial_amount := initial_amount;
          deposits.current_amount := current_amount; |}) None
      (Data_encoding.obj2
        (Data_encoding.req None None "initial_amount" Tez_repr.encoding)
        (Data_encoding.req None None "actual_amount" Tez_repr.encoding)).

  (* Deposits *)
  Definition module :=
    {|
      Storage_sigs.VALUE.encoding := encoding
    |}.
End Deposits.
Definition Deposits := Deposits.module.

Module missed_endorsements_info.
  Record record : Set := Build {
    remaining_slots : int;
    missed_levels : int;
  }.
  Definition with_remaining_slots remaining_slots (r : record) :=
    Build remaining_slots r.(missed_levels).
  Definition with_missed_levels missed_levels (r : record) :=
    Build r.(remaining_slots) missed_levels.
End missed_endorsements_info.
Definition missed_endorsements_info := missed_endorsements_info.record.

Module Missed_endorsements_info.
  Definition t : Set := missed_endorsements_info.

  Definition encoding : Data_encoding.encoding missed_endorsements_info :=
    Data_encoding.conv
      (fun (function_parameter : missed_endorsements_info) ⇒
        let '{|
          missed_endorsements_info.remaining_slots := remaining_slots;
            missed_endorsements_info.missed_levels := missed_levels
            |} := function_parameter in
        (remaining_slots, missed_levels))
      (fun (function_parameter : int × int) ⇒
        let '(remaining_slots, missed_levels) := function_parameter in
        {| missed_endorsements_info.remaining_slots := remaining_slots;
          missed_endorsements_info.missed_levels := missed_levels; |}) None
      (Data_encoding.obj2
        (Data_encoding.req None None "remaining_slots" Data_encoding.int31)
        (Data_encoding.req None None "missed_levels" Data_encoding.int31)).

  (* Missed_endorsements_info *)
  Definition module :=
    {|
      Storage_sigs.VALUE.encoding := encoding
    |}.
End Missed_endorsements_info.
Definition Missed_endorsements_info := Missed_endorsements_info.module.

Module Contract.
  Definition Raw_context :=
    Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "contracts" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition Global_counter :
    Simple_single_data_storage (value := Manager_counter_repr.t) :=
    let functor_result :=
      Storage_functors.Make_single_data_storage Storage_functors.Registered
        Raw_context
        (let name := [ "global_counter" ] in
        {|
          Storage_sigs.NAME.name := name
        |}) Encoding.Manager_counter in
    {|
      Simple_single_data_storage.get :=
        functor_result.(Storage_sigs.Single_data_storage.get);
      Simple_single_data_storage.update :=
        functor_result.(Storage_sigs.Single_data_storage.update);
      Simple_single_data_storage.init_value :=
        functor_result.(Storage_sigs.Single_data_storage.init_value)
    |}.

  Definition Indexed_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "index" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Contract_repr.Index).

  Definition fold {A : Set}
    : Raw_context.t → Variant.t → A → (Contract_repr.t → A → M? A) → M? A :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.fold_keys).

  Definition list_value : Raw_context.t → M? (list Contract_repr.t) :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.keys).

  Definition local_context : Set :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.local_context).

  Definition with_local_context {A : Set}
    : Raw_context.t → Contract_repr.t →
    (Indexed_context.(Storage_sigs.Indexed_raw_context.local_context) →
    M? (Indexed_context.(Storage_sigs.Indexed_raw_context.local_context) × A))
    → M? (Raw_context.t × A) :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.with_local_context).

  Definition Spendable_balance :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
      Storage_functors.Registered
      (let name := [ "balance" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Tez_repr.encoding
      |}.

  Definition Missed_endorsements :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := missed_endorsements_info) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "missed_endorsements" ] in
        {|
          Storage_sigs.NAME.name := name
        |}) Missed_endorsements_info in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Manager :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
      Storage_functors.Registered
      (let name := [ "manager" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Manager_repr.encoding
      |}.

  Definition Consensus_key :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := Signature.public_key) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "consensus_key"; "active" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding :=
            Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
        |} in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Pending_consensus_keys :=
    Storage_functors.Make_indexed_data_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "consensus_key"; "pendings" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Cycle_repr.Index)
      {|
        Storage_sigs.VALUE.encoding :=
          Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
      |}.

  Definition Delegate :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := Signature.public_key_hash) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "delegate" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding :=
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
        |} in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Inactive_delegate :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_set)
      Storage_functors.Registered
      (let name := [ "inactive_delegate" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition Delegate_last_cycle_before_deactivation :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := Cycle_repr.t) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "delegate_desactivation" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding := Cycle_repr.encoding
        |} in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Delegated :=
    Storage_functors.Make_data_set_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "delegated" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Contract_repr.Index).

  Definition Counter :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
      Storage_functors.Registered
      (let name := [ "counter" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Manager_counter.

  Module Make_carbonated_map_expr.
    Class FArgs := {
      N : Storage_sigs.NAME;
    }.

    Definition I `{FArgs} :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
        Storage_functors.Registered N
        (let t : Set := Script_repr.lazy_expr in
        let encoding := Script_repr.lazy_expr_encoding in
        {|
          Storage_sigs.VALUE.encoding := encoding
        |}).

    Definition context `{FArgs} : Set := Raw_context.t.

    Definition key `{FArgs} : Set := Contract_repr.t.

    Definition value `{FArgs} : Set := Script_repr.lazy_expr.

    Definition mem `{FArgs}
      : Raw_context.t → Contract_repr.t → M? (Raw_context.t × bool) :=
      I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem).

    Definition remove_existing `{FArgs}
      : Raw_context.t → Contract_repr.t → M? (Raw_context.t × int) :=
      I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing).

    Definition remove `{FArgs}
      : Raw_context.t → Contract_repr.t → M? (Raw_context.t × int × bool) :=
      I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove).

    Definition consume_deserialize_gas `{FArgs}
      (ctxt : Raw_context.t) (value_value : Script_repr.lazy_expr)
      : M? Raw_context.t :=
      Raw_context.(Raw_context_intf.T.consume_gas) ctxt
        (Script_repr.force_decode_cost value_value).

    Definition consume_serialize_gas `{FArgs}
      (ctxt : Raw_context.t) (value_value : Script_repr.lazy_expr)
      : M? Raw_context.t :=
      Raw_context.(Raw_context_intf.T.consume_gas) ctxt
        (Script_repr.force_bytes_cost value_value).

    Definition get `{FArgs} (ctxt : Raw_context.t) (contract : Contract_repr.t)
      : M? (Raw_context.t × Script_repr.lazy_expr) :=
      let? '(ctxt, value_value) :=
        I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get) ctxt
          contract in
      let? ctxt := consume_deserialize_gas ctxt value_value in
      return? (ctxt, value_value).

    Definition find `{FArgs} (ctxt : Raw_context.t) (contract : Contract_repr.t)
      : M? (Raw_context.t × option Script_repr.lazy_expr) :=
      let? '(ctxt, value_opt) :=
        I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find) ctxt
          contract in
      match value_opt with
      | None ⇒ return? (ctxt, None)
      | Some value_value ⇒
        let? ctxt := consume_deserialize_gas ctxt value_value in
        return? (ctxt, value_opt)
      end.

    Definition update `{FArgs}
      (ctxt : Raw_context.t) (contract : Contract_repr.t)
      (value_value : Script_repr.lazy_expr) : M? (Raw_context.t × int) :=
      let? ctxt := consume_serialize_gas ctxt value_value in
      I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update) ctxt
        contract value_value.

    Definition add_or_remove `{FArgs}
      (ctxt : Raw_context.t) (contract : Contract_repr.t)
      (value_opt : option Script_repr.lazy_expr)
      : M? (Raw_context.t × int × bool) :=
      match value_opt with
      | None ⇒
        I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove)
          ctxt contract None
      | Some value_value ⇒
        let? ctxt := consume_serialize_gas ctxt value_value in
        I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove)
          ctxt contract value_opt
      end.

    Definition init_value `{FArgs}
      (ctxt : Raw_context.t) (contract : Contract_repr.t)
      (value_value : Script_repr.lazy_expr) : M? (Raw_context.t × int) :=
      let? ctxt := consume_serialize_gas ctxt value_value in
      I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
        ctxt contract value_value.

    Definition add `{FArgs}
      (ctxt : Raw_context.t) (contract : Contract_repr.t)
      (value_value : Script_repr.lazy_expr) : M? (Raw_context.t × int × bool) :=
      let? ctxt := consume_serialize_gas ctxt value_value in
      I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add) ctxt
        contract value_value.

    Definition keys_unaccounted `{FArgs}
      : Raw_context.t → M? (list Contract_repr.t) :=
      I.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted).

    (* Make_carbonated_map_expr *)
    Definition functor `{FArgs} :=
      {|
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem := mem;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get := get;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find := find;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update :=
          update;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value :=
          init_value;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add := add;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove :=
          add_or_remove;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing :=
          remove_existing;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove :=
          remove;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted :=
          keys_unaccounted
      |}.
  End Make_carbonated_map_expr.
  Definition Make_carbonated_map_expr (N : Storage_sigs.NAME)
    : Storage_sigs.Non_iterable_indexed_carbonated_data_storage
      (t := Raw_context.t) (key := Contract_repr.t)
      (value := Script_repr.lazy_expr) :=
    let '_ := Make_carbonated_map_expr.Build_FArgs N in
    Make_carbonated_map_expr.functor.

  Definition Code :=
    Make_carbonated_map_expr
      (let name := [ "code" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition Storage :=
    Make_carbonated_map_expr
      (let name := [ "storage" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition Paid_storage_space :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := Z.t) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "paid_bytes" ] in
        {|
          Storage_sigs.NAME.name := name
        |}) Encoding.Z in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Used_storage_space :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := Z.t) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "used_bytes" ] in
        {|
          Storage_sigs.NAME.name := name
        |}) Encoding.Z in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Frozen_deposits :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := deposits) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "frozen_deposits" ] in
        {|
          Storage_sigs.NAME.name := name
        |}) Deposits in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Frozen_deposits_limit :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := Tez_repr.t) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "frozen_deposits_limit" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding := Tez_repr.encoding
        |} in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Bond_id_index :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "bond_id_index" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Bond_id_repr.Index).

  Definition Frozen_bonds :=
    Bond_id_index.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "frozen_bonds" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Tez_repr.encoding
      |}.

  Definition fold_bond_ids {A : Set}
    : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
    → Variant.t → A → (Bond_id_repr.t → A → M? A) → M? A :=
    Bond_id_index.(Storage_sigs.Indexed_raw_context.fold_keys).

  Definition Total_frozen_bonds :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t)
      (key := Contract_repr.t) (value := Tez_repr.t) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "total_frozen_bonds" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding := Tez_repr.encoding
        |} in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.
End Contract.

Module NEXT.
  Record signature {id : Set} : Set := {
    id := id;
    init_value : Raw_context.t → M? Raw_context.t;
    incr : Raw_context.t → M? (Raw_context.t × id);
  }.
End NEXT.
Definition NEXT := @NEXT.signature.
Arguments NEXT {_}.

Module Global_constants.
  Definition Map :
    Storage_sigs.Non_iterable_indexed_carbonated_data_storage
      (t := Raw_context.t) (key := Script_expr_hash.t)
      (value := Script_repr.expr) :=
    let functor_result :=
      Storage_functors.Make_indexed_carbonated_data_storage
        (Storage_functors.Make_subcontext Storage_functors.Registered
          Raw_context.M
          (let name := [ "global_constant" ] in
          {|
            Storage_sigs.NAME.name := name
          |}))
        (Make_index
          {|
            Storage_description.INDEX.to_path := Script_expr_hash.to_path;
            Storage_description.INDEX.of_path := Script_expr_hash.of_path;
            Storage_description.INDEX.path_length :=
              Script_expr_hash.path_length;
            Storage_description.INDEX.rpc_arg := Script_expr_hash.rpc_arg;
            Storage_description.INDEX.encoding := Script_expr_hash.encoding;
            Storage_description.INDEX.compare := Script_expr_hash.compare
          |})
        (let t : Set := Script_repr.expr in
        let encoding := Script_repr.expr_encoding in
        {|
          Storage_sigs.VALUE.encoding := encoding
        |}) in
    {|
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.mem);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.get);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.find);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.update);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.init_value);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add_or_remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove_existing);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.keys_unaccounted)
    |}.
End Global_constants.

Module Big_map.
  Definition id : Set := Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t).

  Definition Raw_context :=
    Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "big_maps" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Module Next.
    Definition Storage :=
      Storage_functors.Make_single_data_storage Storage_functors.Registered
        Raw_context
        (let name := [ "next" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding :=
            Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.encoding)
        |}.

    Definition incr (ctxt : Raw_context.t)
      : M?
        (Raw_context.t × Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)) :=
      let? i_value := Storage.(Storage_sigs.Single_data_storage.get) ctxt in
      let? ctxt :=
        Storage.(Storage_sigs.Single_data_storage.update) ctxt
          (Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.next) i_value) in
      return? (ctxt, i_value).

    Definition init_value (ctxt : Raw_context.t) : M? Raw_context.t :=
      Storage.(Storage_sigs.Single_data_storage.init_value) ctxt
        Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.init_value).

    (* Next *)
    Definition module :=
      {|
        NEXT.init_value := init_value;
        NEXT.incr := incr
      |}.
  End Next.
  Definition Next : NEXT (id := id) := Next.module.

  Definition Index := Lazy_storage_kind.Big_map.Id.

  Definition Indexed_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "index" ] in
        {|
          Storage_sigs.NAME.name := name
        |}))
      (Make_index
        {|
          Storage_description.INDEX.to_path :=
            Index.(Lazy_storage_kind.ID.to_path);
          Storage_description.INDEX.of_path :=
            Index.(Lazy_storage_kind.ID.of_path);
          Storage_description.INDEX.path_length :=
            Index.(Lazy_storage_kind.ID.path_length);
          Storage_description.INDEX.rpc_arg :=
            Index.(Lazy_storage_kind.ID.rpc_arg);
          Storage_description.INDEX.encoding :=
            Index.(Lazy_storage_kind.ID.encoding);
          Storage_description.INDEX.compare :=
            Index.(Lazy_storage_kind.ID.compare)
        |}).

  Definition rpc_arg
    : RPC_arg.arg Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
    Index.(Lazy_storage_kind.ID.rpc_arg).

  Definition fold {A : Set}
    : Raw_context.t → Variant.t → A →
    (Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) → A → M? A) → M? A :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.fold_keys).

  Definition list_value
    : Raw_context.t →
    M? (list Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)) :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.keys).

  Definition remove
    (ctxt : Raw_context.t)
    (n_value : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
    : Raw_context.t :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.remove) ctxt n_value.

  Definition copy
    (ctxt : Raw_context.t)
    (from : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
    (to_ : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
    : M? Raw_context.t :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.copy) ctxt from to_.

  Definition key : Set :=
    Raw_context.t × Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t).

  Definition Total_bytes :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
      Storage_functors.Registered
      (let name := [ "total_bytes" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Z.

  Definition Key_type :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t) (key := id)
      (value := Script_repr.expr) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "key_type" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        (let t : Set := Script_repr.expr in
        let encoding := Script_repr.expr_encoding in
        {|
          Storage_sigs.VALUE.encoding := encoding
        |}) in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Value_type :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t) (key := id)
      (value := Script_repr.expr) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "value_type" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        (let t : Set := Script_repr.expr in
        let encoding := Script_repr.expr_encoding in
        {|
          Storage_sigs.VALUE.encoding := encoding
        |}) in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Module Contents.
    Definition I :=
      Storage_functors.Make_indexed_carbonated_data_storage
        (Storage_functors.Make_subcontext Storage_functors.Registered
          Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
          (let name := [ "contents" ] in
          {|
            Storage_sigs.NAME.name := name
          |}))
        (Make_index
          {|
            Storage_description.INDEX.to_path := Script_expr_hash.to_path;
            Storage_description.INDEX.of_path := Script_expr_hash.of_path;
            Storage_description.INDEX.path_length :=
              Script_expr_hash.path_length;
            Storage_description.INDEX.rpc_arg := Script_expr_hash.rpc_arg;
            Storage_description.INDEX.encoding := Script_expr_hash.encoding;
            Storage_description.INDEX.compare := Script_expr_hash.compare
          |})
        (let t : Set := Script_repr.expr in
        let encoding := Script_repr.expr_encoding in
        {|
          Storage_sigs.VALUE.encoding := encoding
        |}).

    Definition context : Set :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t).

    Definition key : Set := Script_expr_hash.t.

    Definition value : Set := Script_repr.expr.

    Definition mem
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → Script_expr_hash.t → M? (Raw_context.t × bool) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.mem).

    Definition remove_existing
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → Script_expr_hash.t → M? (Raw_context.t × int) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.remove_existing).

    Definition remove
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → Script_expr_hash.t → M? (Raw_context.t × int × bool) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.remove).

    Definition update
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → Script_expr_hash.t → Script_repr.expr → M? (Raw_context.t × int) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.update).

    Definition add_or_remove
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → Script_expr_hash.t → option Script_repr.expr →
      M? (Raw_context.t × int × bool) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.add_or_remove).

    Definition init_value
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → Script_expr_hash.t → Script_repr.expr → M? (Raw_context.t × int) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.init_value).

    Definition add
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → Script_expr_hash.t → Script_repr.expr →
      M? (Raw_context.t × int × bool) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.add).

    Definition list_key_values
      : option int → option int →
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → M? (Raw_context.t × list (Script_expr_hash.t × Script_repr.expr)) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.list_key_values).

    Definition consume_deserialize_gas
      (ctxt : Raw_context.t) (value_value : Script_repr.expr)
      : M? Raw_context.t :=
      Raw_context.(Raw_context_intf.T.consume_gas) ctxt
        (Script_repr.deserialized_cost value_value).

    Definition get
      (ctxt :
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t))
      (contract : Script_expr_hash.t) : M? (Raw_context.t × Script_repr.expr) :=
      let? '(ctxt, value_value) :=
        I.(Storage_sigs.Indexed_carbonated_data_storage.get) ctxt contract in
      let? ctxt := consume_deserialize_gas ctxt value_value in
      return? (ctxt, value_value).

    Definition find
      (ctxt :
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t))
      (contract : Script_expr_hash.t)
      : M? (Raw_context.t × option Script_repr.expr) :=
      let? '(ctxt, value_opt) :=
        I.(Storage_sigs.Indexed_carbonated_data_storage.find) ctxt contract in
      match value_opt with
      | None ⇒ return? (ctxt, None)
      | Some value_value ⇒
        let? ctxt := consume_deserialize_gas ctxt value_value in
        return? (ctxt, value_opt)
      end.

    Definition keys_unaccounted
      : Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.t)
      → M? (list Script_expr_hash.t) :=
      I.(Storage_sigs.Indexed_carbonated_data_storage.keys_unaccounted).

    (* Contents *)
    Definition module :=
      {|
        Storage_sigs.Indexed_carbonated_data_storage.mem := mem;
        Storage_sigs.Indexed_carbonated_data_storage.get := get;
        Storage_sigs.Indexed_carbonated_data_storage.find := find;
        Storage_sigs.Indexed_carbonated_data_storage.update := update;
        Storage_sigs.Indexed_carbonated_data_storage.init_value := init_value;
        Storage_sigs.Indexed_carbonated_data_storage.add := add;
        Storage_sigs.Indexed_carbonated_data_storage.add_or_remove :=
          add_or_remove;
        Storage_sigs.Indexed_carbonated_data_storage.remove_existing :=
          remove_existing;
        Storage_sigs.Indexed_carbonated_data_storage.remove := remove;
        Storage_sigs.Indexed_carbonated_data_storage.keys_unaccounted :=
          keys_unaccounted;
        Storage_sigs.Indexed_carbonated_data_storage.list_key_values :=
          list_key_values
      |}.
  End Contents.
  Definition Contents
    : Storage_sigs.Indexed_carbonated_data_storage (t := key)
      (key := Script_expr_hash.t) (value := Script_repr.expr) :=
    Contents.module.
End Big_map.

Module Sapling.
  Definition id : Set :=
    Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t).

  Definition Raw_context :=
    Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "sapling" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Module Next.
    Definition Storage :=
      Storage_functors.Make_single_data_storage Storage_functors.Registered
        Raw_context
        (let name := [ "next" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding :=
            Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.encoding)
        |}.

    Definition incr (ctxt : Raw_context.t)
      : M?
        (Raw_context.t ×
          Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t)) :=
      let? i_value := Storage.(Storage_sigs.Single_data_storage.get) ctxt in
      let? ctxt :=
        Storage.(Storage_sigs.Single_data_storage.update) ctxt
          (Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.next)
            i_value) in
      return? (ctxt, i_value).

    Definition init_value (ctxt : Raw_context.t) : M? Raw_context.t :=
      Storage.(Storage_sigs.Single_data_storage.init_value) ctxt
        Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.init_value).
  End Next.

  Definition Index := Lazy_storage_kind.Sapling_state.Id.

  Definition rpc_arg
    : RPC_arg.arg Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
    Index.(Lazy_storage_kind.ID.rpc_arg).

  Definition Indexed_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "index" ] in
        {|
          Storage_sigs.NAME.name := name
        |}))
      (Make_index
        {|
          Storage_description.INDEX.to_path :=
            Index.(Lazy_storage_kind.ID.to_path);
          Storage_description.INDEX.of_path :=
            Index.(Lazy_storage_kind.ID.of_path);
          Storage_description.INDEX.path_length :=
            Index.(Lazy_storage_kind.ID.path_length);
          Storage_description.INDEX.rpc_arg :=
            Index.(Lazy_storage_kind.ID.rpc_arg);
          Storage_description.INDEX.encoding :=
            Index.(Lazy_storage_kind.ID.encoding);
          Storage_description.INDEX.compare :=
            Index.(Lazy_storage_kind.ID.compare)
        |}).

  Definition remove
    (ctxt : Raw_context.t)
    (n_value : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
    : Raw_context.t :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.remove) ctxt n_value.

  Definition copy
    (ctxt : Raw_context.t)
    (from : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
    (to_ : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
    : M? Raw_context.t :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.copy) ctxt from to_.

  Definition Total_bytes :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
      Storage_functors.Registered
      (let name := [ "total_bytes" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Z.

  Definition Commitments_size :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
      (let name := [ "commitments_size" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Int64.

  Definition Memo_size :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
      (let name := [ "memo_size" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Sapling_repr.Memo_size.encoding
      |}.

  Definition Commitments :
    Storage_sigs.Non_iterable_indexed_carbonated_data_storage
      (t := Raw_context.t × id) (key := int64) (value := Sapling.Hash.t) :=
    let functor_result :=
      Storage_functors.Make_indexed_carbonated_data_storage
        (Storage_functors.Make_subcontext Storage_functors.Registered
          Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
          (let name := [ "commitments" ] in
          {|
            Storage_sigs.NAME.name := name
          |}))
        (Make_index
          (let t : Set := int64 in
          let rpc_arg :=
            let construct := Int64.to_string in
            let destruct (hash_value : string)
              : Pervasives.result int64 string :=
              Result.of_option "Cannot parse node position"
                (Int64.of_string_opt hash_value) in
            RPC_arg.make
              (Some "The position of a node in a sapling commitment tree")
              "sapling_node_position" destruct construct tt in
          let encoding :=
            Data_encoding.def "sapling_node_position"
              (Some "Sapling node position")
              (Some "The position of a node in a sapling commitment tree")
              Data_encoding.int64_value in
          let compare := Compare.Int64.(Compare.S.compare) in
          let path_length := return? 1 in
          let to_path (c_value : int64) (l_value : list string) : list string :=
            cons (Int64.to_string c_value) l_value in
          let of_path (function_parameter : list string) : M? (option int64) :=
            match function_parameter with
            | cons c_value [] ⇒ return? (Int64.of_string_opt c_value)
            | _ ⇒ return? None
            end in
          {|
            Storage_description.INDEX.to_path := to_path;
            Storage_description.INDEX.of_path := of_path;
            Storage_description.INDEX.path_length := path_length;
            Storage_description.INDEX.rpc_arg := rpc_arg;
            Storage_description.INDEX.encoding := encoding;
            Storage_description.INDEX.compare := compare
          |}))
        {|
          Storage_sigs.VALUE.encoding := Sapling.Hash.encoding
        |} in
    {|
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.mem);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.get);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.find);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.update);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.init_value);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add_or_remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove_existing);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.keys_unaccounted)
    |}.

  Definition commitments_init
    (ctx : Raw_context.t)
    (id : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
    : Raw_context.t :=
    let '(ctx, _id) :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.remove)
        (ctx, id) [ "commitments" ] in
    ctx.

  Definition Ciphertexts :
    Storage_sigs.Non_iterable_indexed_carbonated_data_storage
      (t := Raw_context.t × id) (key := int64) (value := Sapling.Ciphertext.t)
    :=
    let functor_result :=
      Storage_functors.Make_indexed_carbonated_data_storage
        (Storage_functors.Make_subcontext Storage_functors.Registered
          Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
          (let name := [ "ciphertexts" ] in
          {|
            Storage_sigs.NAME.name := name
          |}))
        (Make_index
          (let t : Set := int64 in
          let rpc_arg :=
            let construct := Int64.to_string in
            let destruct (hash_value : string)
              : Pervasives.result int64 string :=
              Result.of_option "Cannot parse ciphertext position"
                (Int64.of_string_opt hash_value) in
            RPC_arg.make (Some "The position of a sapling ciphertext")
              "sapling_ciphertext_position" destruct construct tt in
          let encoding :=
            Data_encoding.def "sapling_ciphertext_position"
              (Some "Sapling ciphertext position")
              (Some "The position of a sapling ciphertext")
              Data_encoding.int64_value in
          let compare := Compare.Int64.(Compare.S.compare) in
          let path_length := return? 1 in
          let to_path (c_value : int64) (l_value : list string) : list string :=
            cons (Int64.to_string c_value) l_value in
          let of_path (function_parameter : list string) : M? (option int64) :=
            match function_parameter with
            | cons c_value [] ⇒ return? (Int64.of_string_opt c_value)
            | _ ⇒ return? None
            end in
          {|
            Storage_description.INDEX.to_path := to_path;
            Storage_description.INDEX.of_path := of_path;
            Storage_description.INDEX.path_length := path_length;
            Storage_description.INDEX.rpc_arg := rpc_arg;
            Storage_description.INDEX.encoding := encoding;
            Storage_description.INDEX.compare := compare
          |}))
        {|
          Storage_sigs.VALUE.encoding := Sapling.Ciphertext.encoding
        |} in
    {|
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.mem);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.get);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.find);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.update);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.init_value);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add_or_remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove_existing);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.keys_unaccounted)
    |}.

  Definition ciphertexts_init
    (ctx : Raw_context.t)
    (id : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
    : Raw_context.t :=
    let '(ctx, _id) :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.remove)
        (ctx, id) [ "commitments" ] in
    ctx.

  Definition Nullifiers_size :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
      (let name := [ "nullifiers_size" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Int64.

  Definition Nullifiers_ordered :
    Storage_sigs.Non_iterable_indexed_data_storage (t := Raw_context.t × id)
      (key := int64) (value := Sapling.Nullifier.t) :=
    let functor_result :=
      Storage_functors.Make_indexed_data_storage
        (Storage_functors.Make_subcontext Storage_functors.Registered
          Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
          (let name := [ "nullifiers_ordered" ] in
          {|
            Storage_sigs.NAME.name := name
          |}))
        (Make_index
          (let t : Set := int64 in
          let rpc_arg :=
            let construct := Int64.to_string in
            let destruct (hash_value : string)
              : Pervasives.result int64 string :=
              Result.of_option "Cannot parse nullifier position"
                (Int64.of_string_opt hash_value) in
            RPC_arg.make (Some "A sapling nullifier position")
              "sapling_nullifier_position" destruct construct tt in
          let encoding :=
            Data_encoding.def "sapling_nullifier_position"
              (Some "Sapling nullifier position")
              (Some "Sapling nullifier position") Data_encoding.int64_value in
          let compare := Compare.Int64.(Compare.S.compare) in
          let path_length := return? 1 in
          let to_path (c_value : int64) (l_value : list string) : list string :=
            cons (Int64.to_string c_value) l_value in
          let of_path (function_parameter : list string) : M? (option int64) :=
            match function_parameter with
            | cons c_value [] ⇒ return? (Int64.of_string_opt c_value)
            | _ ⇒ return? None
            end in
          {|
            Storage_description.INDEX.to_path := to_path;
            Storage_description.INDEX.of_path := of_path;
            Storage_description.INDEX.path_length := path_length;
            Storage_description.INDEX.rpc_arg := rpc_arg;
            Storage_description.INDEX.encoding := encoding;
            Storage_description.INDEX.compare := compare
          |}))
        {|
          Storage_sigs.VALUE.encoding := Sapling.Nullifier.encoding
        |} in
    {|
      Storage_sigs.Non_iterable_indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage.mem);
      Storage_sigs.Non_iterable_indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage.get);
      Storage_sigs.Non_iterable_indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage.find);
      Storage_sigs.Non_iterable_indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage.update);
      Storage_sigs.Non_iterable_indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage.init_value);
      Storage_sigs.Non_iterable_indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage.add);
      Storage_sigs.Non_iterable_indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage.add_or_remove);
      Storage_sigs.Non_iterable_indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage.remove_existing);
      Storage_sigs.Non_iterable_indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage.remove)
    |}.

  Definition Nullifiers_hashed :=
    Storage_functors.Make_carbonated_data_set_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "nullifiers_hashed" ] in
        {|
          Storage_sigs.NAME.name := name
        |}))
      (Make_index
        (let t : Set := Sapling.Nullifier.t in
        let encoding := Sapling.Nullifier.encoding in
        let of_string (hexstring : string)
          : Pervasives.result Sapling.Nullifier.t string :=
          Result.of_option "Cannot parse sapling nullifier"
            (Option.bind (Hex.to_bytes (Hex.Hex hexstring))
              (Data_encoding.Binary.of_bytes_opt encoding)) in
        let to_string (nf : Sapling.Nullifier.t) : string :=
          let b_value := Data_encoding.Binary.to_bytes_exn None encoding nf in
          let 'Hex.Hex hexstring := Hex.of_bytes None b_value in
          hexstring in
        let rpc_arg :=
          RPC_arg.make (Some "A sapling nullifier") "sapling_nullifier"
            of_string to_string tt in
        let compare := Sapling.Nullifier.compare in
        let path_length := return? 1 in
        let to_path (c_value : Sapling.Nullifier.t) (l_value : list string)
          : list string :=
          cons (to_string c_value) l_value in
        let of_path (function_parameter : list string)
          : M? (option Sapling.Nullifier.t) :=
          match function_parameter with
          | cons c_value [] ⇒ return? (Result.to_option (of_string c_value))
          | _ ⇒ return? None
          end in
        {|
          Storage_description.INDEX.to_path := to_path;
          Storage_description.INDEX.of_path := of_path;
          Storage_description.INDEX.path_length := path_length;
          Storage_description.INDEX.rpc_arg := rpc_arg;
          Storage_description.INDEX.encoding := encoding;
          Storage_description.INDEX.compare := compare
        |})).

  Definition nullifiers_init
    (ctx : Raw_context.t)
    (id : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
    : Raw_context.t :=
    let ctx :=
      Nullifiers_size.(Storage_sigs.Single_data_storage.add) (ctx, id)
        Int64.zero in
    let '(ctx, id) :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.remove)
        (ctx, id) [ "nullifiers_ordered" ] in
    let '(ctx, _id) :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context).(Raw_context_intf.T.remove)
        (ctx, id) [ "nullifiers_hashed" ] in
    ctx.

  Definition Roots :
    Storage_sigs.Non_iterable_indexed_data_storage (t := Raw_context.t × id)
      (key := int32) (value := Sapling.Hash.t) :=
    let functor_result :=
      Storage_functors.Make_indexed_data_storage
        (Storage_functors.Make_subcontext Storage_functors.Registered
          Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
          (let name := [ "roots" ] in
          {|
            Storage_sigs.NAME.name := name
          |}))
        (Make_index
          (let t : Set := int32 in
          let rpc_arg :=
            let construct := Int32.to_string in
            let destruct (hash_value : string)
              : Pervasives.result int32 string :=
              Result.of_option "Cannot parse nullifier position"
                (Int32.of_string_opt hash_value) in
            RPC_arg.make (Some "A sapling root") "sapling_root" destruct
              construct tt in
          let encoding :=
            Data_encoding.def "sapling_root" (Some "Sapling root")
              (Some "Sapling root") Data_encoding.int32_value in
          let compare := Compare.Int32.(Compare.S.compare) in
          let path_length := return? 1 in
          let to_path (c_value : int32) (l_value : list string) : list string :=
            cons (Int32.to_string c_value) l_value in
          let of_path (function_parameter : list string) : M? (option int32) :=
            match function_parameter with
            | cons c_value [] ⇒ return? (Int32.of_string_opt c_value)
            | _ ⇒ return? None
            end in
          {|
            Storage_description.INDEX.to_path := to_path;
            Storage_description.INDEX.of_path := of_path;
            Storage_description.INDEX.path_length := path_length;
            Storage_description.INDEX.rpc_arg := rpc_arg;
            Storage_description.INDEX.encoding := encoding;
            Storage_description.INDEX.compare := compare
          |}))
        {|
          Storage_sigs.VALUE.encoding := Sapling.Hash.encoding
        |} in
    {|
      Storage_sigs.Non_iterable_indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage.mem);
      Storage_sigs.Non_iterable_indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage.get);
      Storage_sigs.Non_iterable_indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage.find);
      Storage_sigs.Non_iterable_indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage.update);
      Storage_sigs.Non_iterable_indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage.init_value);
      Storage_sigs.Non_iterable_indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage.add);
      Storage_sigs.Non_iterable_indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage.add_or_remove);
      Storage_sigs.Non_iterable_indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage.remove_existing);
      Storage_sigs.Non_iterable_indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage.remove)
    |}.

  Definition Roots_pos :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
      (let name := [ "roots_pos" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Int32.

  Definition Roots_level :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
      (let name := [ "roots_level" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Raw_level_repr.encoding
      |}.
End Sapling.

Module Public_key_hash.

Inclusion of the module [Signature.Public_key_hash]

  Definition t := Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t).

  Definition pp := Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp).

  Definition pp_short :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short).

  Definition op_eq :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_eq).

  Definition op_ltgt :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_ltgt).

  Definition op_lt :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lt).

  Definition op_lteq :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lteq).

  Definition op_gteq :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gteq).

  Definition op_gt :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gt).

  Definition compare :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare).

  Definition equal :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal).

  Definition max := Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.max).

  Definition min := Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.min).

  Definition size_value :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value).

  Definition to_bytes :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes).

  Definition of_bytes_opt :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt).

  Definition of_bytes_exn :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_exn).

  Definition to_b58check :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check).

  Definition to_short_b58check :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_short_b58check).

  Definition of_b58check_exn :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_exn).

  Definition of_b58check_opt :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt).

  Definition b58check_encoding :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.b58check_encoding).

  Definition encoding :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding).

  Definition rpc_arg :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg).

  Definition zero :=
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero).

  Definition Path_Ed25519 :=
    Path_encoding.Make_hex
      {|
        Path_encoding.ENCODING.to_bytes :=
          Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes);
        Path_encoding.ENCODING.of_bytes_opt :=
          Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt)
      |}.

  Definition Path_Secp256k1 :=
    Path_encoding.Make_hex
      {|
        Path_encoding.ENCODING.to_bytes :=
          Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes);
        Path_encoding.ENCODING.of_bytes_opt :=
          Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt)
      |}.

  Definition Path_P256 :=
    Path_encoding.Make_hex
      {|
        Path_encoding.ENCODING.to_bytes :=
          P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes);
        Path_encoding.ENCODING.of_bytes_opt :=
          P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt)
      |}.

  Definition to_path
    (key_value : Signature.public_key_hash) (l_value : list string)
    : list string :=
    match key_value with
    | Signature.Ed25519Hash h_value ⇒
      cons "ed25519" (Path_Ed25519.(Path_encoding.S.to_path) h_value l_value)
    | Signature.Secp256k1Hash h_value ⇒
      cons "secp256k1"
        (Path_Secp256k1.(Path_encoding.S.to_path) h_value l_value)
    | Signature.P256Hash h_value ⇒
      cons "p256" (Path_P256.(Path_encoding.S.to_path) h_value l_value)
    end.

  Definition of_path (function_parameter : list string)
    : M? (option Signature.public_key_hash) :=
    match function_parameter with
    | cons "ed25519" rest ⇒
      let? rest := Path_Ed25519.(Path_encoding.S.of_path) rest in
      match rest with
      | Some pkh ⇒ return? (Some (Signature.Ed25519Hash pkh))
      | None ⇒ return? None
      end
    | cons "secp256k1" rest ⇒
      let? rest := Path_Secp256k1.(Path_encoding.S.of_path) rest in
      match rest with
      | Some pkh ⇒ return? (Some (Signature.Secp256k1Hash pkh))
      | None ⇒ return? None
      end
    | cons "p256" rest ⇒
      let? rest := Path_P256.(Path_encoding.S.of_path) rest in
      match rest with
      | Some pkh ⇒ return? (Some (Signature.P256Hash pkh))
      | None ⇒ return? None
      end
    | _ ⇒ return? None
    end.

  Definition path_length : M? int :=
    let? l1 := Path_Ed25519.(Path_encoding.S.path_length) in
    let? l2 := Path_Secp256k1.(Path_encoding.S.path_length) in
    let? l3 := Path_P256.(Path_encoding.S.path_length) in
    if (l1 =i l2) && (l2 =i l3) then
      return? (l1 +i 1)
    else
      Error_monad.error_value (Build_extensible "Asserted" unit tt).
End Public_key_hash.

Definition Public_key_hash_index :=
  Make_index
    {|
      Storage_description.INDEX.to_path := Public_key_hash.to_path;
      Storage_description.INDEX.of_path := Public_key_hash.of_path;
      Storage_description.INDEX.path_length := Public_key_hash.path_length;
      Storage_description.INDEX.rpc_arg := Public_key_hash.rpc_arg;
      Storage_description.INDEX.encoding := Public_key_hash.encoding;
      Storage_description.INDEX.compare := Public_key_hash.compare
    |}.

Module Protocol_hash_with_path_encoding.
  Include Protocol_hash.

  Definition Path_encoding_Make_hex_include :=
    Path_encoding.Make_hex
      {|
        Path_encoding.ENCODING.to_bytes := Protocol_hash.to_bytes;
        Path_encoding.ENCODING.of_bytes_opt := Protocol_hash.of_bytes_opt
      |}.

Inclusion of the module [Path_encoding_Make_hex_include]

  Definition to_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.to_path).

  Definition of_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.of_path).

  Definition path_length :=
    Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
End Protocol_hash_with_path_encoding.

Definition Delegates :=
  Storage_functors.Make_data_set_storage
    (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "delegates" ] in
      {|
        Storage_sigs.NAME.name := name
      |})) Public_key_hash_index.

Definition Consensus_keys :=
  Storage_functors.Make_data_set_storage
    (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "consensus_keys" ] in
      {|
        Storage_sigs.NAME.name := name
      |})) Public_key_hash_index.

Module slashed_level.
  Record record : Set := Build {
    for_double_endorsing : bool;
    for_double_baking : bool;
  }.
  Definition with_for_double_endorsing for_double_endorsing (r : record) :=
    Build for_double_endorsing r.(for_double_baking).
  Definition with_for_double_baking for_double_baking (r : record) :=
    Build r.(for_double_endorsing) for_double_baking.
End slashed_level.
Definition slashed_level := slashed_level.record.

Module Slashed_level.
  Definition t : Set := slashed_level.

  Definition encoding : Data_encoding.encoding slashed_level :=
    Data_encoding.conv
      (fun (function_parameter : slashed_level) ⇒
        let '{|
          slashed_level.for_double_endorsing := for_double_endorsing;
            slashed_level.for_double_baking := for_double_baking
            |} := function_parameter in
        (for_double_endorsing, for_double_baking))
      (fun (function_parameter : bool × bool) ⇒
        let '(for_double_endorsing, for_double_baking) := function_parameter in
        {| slashed_level.for_double_endorsing := for_double_endorsing;
          slashed_level.for_double_baking := for_double_baking; |}) None
      (Data_encoding.obj2
        (Data_encoding.req None None "for_double_endorsing"
          Data_encoding.bool_value)
        (Data_encoding.req None None "for_double_baking"
          Data_encoding.bool_value)).

  (* Slashed_level *)
  Definition module :=
    {|
      Storage_sigs.VALUE.encoding := encoding
    |}.
End Slashed_level.
Definition Slashed_level := Slashed_level.module.

Module Cycle.
  Definition Indexed_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Raw_context.M
        (let name := [ "cycle" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Cycle_repr.Index).

  Definition Slashed_deposits :=
    Storage_functors.Make_indexed_data_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "slashed_deposits" ] in
        {|
          Storage_sigs.NAME.name := name
        |}))
      (Storage_functors.Pair (Make_index Raw_level_repr.Index)
        Public_key_hash_index) Slashed_level.

  Definition Selected_stake_distribution :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
      Storage_functors.Registered
      (let name := [ "selected_stake_distribution" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := list (Signature.public_key_hash × Tez_repr.t) in
      let encoding :=
        Data_encoding._Variable.list_value None
          (Data_encoding.obj2
            (Data_encoding.req None None "baker"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "active_stake" Tez_repr.encoding)) in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Total_active_stake :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t) (key := Cycle_repr.t)
      (value := Tez_repr.t) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "total_active_stake" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        {|
          Storage_sigs.VALUE.encoding := Tez_repr.encoding
        |} in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Delegate_sampler_state :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t) (key := Cycle_repr.t)
      (value := Sampler.t Raw_context.consensus_pk) :=
    let functor_result :=
      Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
        Storage_functors.Registered
        (let name := [ "delegate_sampler_state" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        (let t : Set := Sampler.t Raw_context.consensus_pk in
        let encoding := Sampler.encoding Raw_context.consensus_pk_encoding in
        {|
          Storage_sigs.VALUE.encoding := encoding
        |}) in
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        functor_result.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Module unrevealed_nonce.
    Record record : Set := Build {
      nonce_hash : Nonce_hash.t;
      delegate : Signature.public_key_hash;
    }.
    Definition with_nonce_hash nonce_hash (r : record) :=
      Build nonce_hash r.(delegate).
    Definition with_delegate delegate (r : record) :=
      Build r.(nonce_hash) delegate.
  End unrevealed_nonce.
  Definition unrevealed_nonce := unrevealed_nonce.record.

  Inductive nonce_status : Set :=
  | Unrevealed : unrevealed_nonce → nonce_status
  | Revealed : Seed_repr.nonce → nonce_status.

  Definition nonce_status_encoding : Data_encoding.encoding nonce_status :=
    Data_encoding.union None
      [
        Data_encoding.case_value "Unrevealed" None (Data_encoding.Tag 0)
          (Data_encoding.tup2 Nonce_hash.encoding
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
          (fun (function_parameter : nonce_status) ⇒
            match function_parameter with
            |
              Unrevealed {|
                unrevealed_nonce.nonce_hash := nonce_hash;
                  unrevealed_nonce.delegate := delegate
                  |} ⇒ Some (nonce_hash, delegate)
            | _ ⇒ None
            end)
          (fun (function_parameter :
            Nonce_hash.t × Signature.public_key_hash) ⇒
            let '(nonce_hash, delegate) := function_parameter in
            Unrevealed
              {| unrevealed_nonce.nonce_hash := nonce_hash;
                unrevealed_nonce.delegate := delegate; |});
        Data_encoding.case_value "Revealed" None (Data_encoding.Tag 1)
          Seed_repr.nonce_encoding
          (fun (function_parameter : nonce_status) ⇒
            match function_parameter with
            | Revealed nonce_value ⇒ Some nonce_value
            | _ ⇒ None
            end)
          (fun (nonce_value : Seed_repr.nonce) ⇒ Revealed nonce_value)
      ].

  Definition Nonce :=
    Storage_functors.Make_indexed_data_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "nonces" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Raw_level_repr.Index)
      (let t : Set := nonce_status in
      let encoding := nonce_status_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Seed :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_map)
      Storage_functors.Registered
      (let name := [ "random_seed" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Seed_repr.seed in
      let encoding := Seed_repr.seed_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).
End Cycle.

Definition Slashed_deposits := Cycle.Slashed_deposits.

Module Stake.
  Definition Staking_balance :=
    Storage_functors.Make_indexed_data_snapshotable_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Raw_context.M
        (let name := [ "staking_balance" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) Int31_index Public_key_hash_index
      {|
        Storage_sigs.VALUE.encoding := Tez_repr.encoding
      |}.

  Definition Active_delegates_with_minimal_stake :=
    Storage_functors.Make_indexed_data_snapshotable_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Raw_context.M
        (let name := [ "active_delegate_with_one_roll" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) Int31_index Public_key_hash_index
      (let t : Set := unit in
      let encoding := Data_encoding.unit_value in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Selected_distribution_for_cycle :
    Storage_sigs.Indexed_data_storage (t := Raw_context.t) (key := Cycle_repr.t)
      (value := list (Signature.public_key_hash × Tez_repr.t)) :=
    {|
      Storage_sigs.Indexed_data_storage.mem :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.mem);
      Storage_sigs.Indexed_data_storage.get :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.get);
      Storage_sigs.Indexed_data_storage.find :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.find);
      Storage_sigs.Indexed_data_storage.update :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.update);
      Storage_sigs.Indexed_data_storage.init_value :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.init_value);
      Storage_sigs.Indexed_data_storage.add :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.add);
      Storage_sigs.Indexed_data_storage.add_or_remove :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove);
      Storage_sigs.Indexed_data_storage.remove_existing :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing);
      Storage_sigs.Indexed_data_storage.remove :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.remove);
      Storage_sigs.Indexed_data_storage.clear :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.clear);
      Storage_sigs.Indexed_data_storage.keys :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.keys);
      Storage_sigs.Indexed_data_storage.bindings :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.bindings);
      Storage_sigs.Indexed_data_storage.fold _ :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.fold);
      Storage_sigs.Indexed_data_storage.fold_keys _ :=
        Cycle.Selected_stake_distribution.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
    |}.

  Definition Total_active_stake := Cycle.Total_active_stake.

  Definition Last_snapshot :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "last_snapshot" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.UInt16.
End Stake.

Definition Delegate_sampler_state := Cycle.Delegate_sampler_state.

Module Vote.
  Definition Raw_context :=
    Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "votes" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition Pred_period_kind :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context
      (let name := [ "pred_period_kind" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Voting_period_repr.kind in
      let encoding := Voting_period_repr.kind_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Current_period :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context
      (let name := [ "current_period" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Voting_period_repr.t in
      let encoding := Voting_period_repr.encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Participation_ema :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context
      (let name := [ "participation_ema" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Int32.

  Definition Current_proposal :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context
      (let name := [ "current_proposal" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Protocol_hash.encoding
      |}.

  Definition Voting_power_in_listings :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context
      (let name := [ "voting_power_in_listings" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Int64.

  Definition Listings :=
    Storage_functors.Make_indexed_data_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "listings" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) Public_key_hash_index Encoding.Int64.

  Definition Proposals :=
    Storage_functors.Make_data_set_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "proposals" ] in
        {|
          Storage_sigs.NAME.name := name
        |}))
      (Storage_functors.Pair
        (Make_index
          {|
            Storage_description.INDEX.to_path :=
              Protocol_hash_with_path_encoding.to_path;
            Storage_description.INDEX.of_path :=
              Protocol_hash_with_path_encoding.of_path;
            Storage_description.INDEX.path_length :=
              Protocol_hash_with_path_encoding.path_length;
            Storage_description.INDEX.rpc_arg :=
              Protocol_hash_with_path_encoding.rpc_arg;
            Storage_description.INDEX.encoding :=
              Protocol_hash_with_path_encoding.encoding;
            Storage_description.INDEX.compare :=
              Protocol_hash_with_path_encoding.compare
          |}) Public_key_hash_index).

  Definition Proposals_count :=
    Storage_functors.Make_indexed_data_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "proposals_count" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) Public_key_hash_index Encoding.UInt16.

  Definition Ballots :=
    Storage_functors.Make_indexed_data_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "ballots" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) Public_key_hash_index
      (let t : Set := Vote_repr.ballot in
      let encoding := Vote_repr.ballot_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).
End Vote.

Module FOR_CYCLE.
  Record signature : Set := {
    init_value :
      Raw_context.t → Cycle_repr.t → Seed_repr.seed → M? Raw_context.t;
    mem : Raw_context.t → Cycle_repr.t → bool;
    get : Raw_context.t → Cycle_repr.t → M? Seed_repr.seed;
    update :
      Raw_context.t → Cycle_repr.t → Seed_repr.seed →
      Seed_repr.seed_status → M? Raw_context.t;
    remove_existing : Raw_context.t → Cycle_repr.t → M? Raw_context.t;
  }.
End FOR_CYCLE.
Definition FOR_CYCLE := FOR_CYCLE.signature.

Definition Seed_status :
  Storage_sigs.Single_data_storage (t := Raw_context.t)
    (value := Seed_repr.seed_status) :=
  Storage_functors.Make_single_data_storage Storage_functors.Registered
    Raw_context.M
    (let name := [ "seed_status" ] in
    {|
      Storage_sigs.NAME.name := name
    |})
    (let t : Set := Seed_repr.seed_status in
    let encoding := Seed_repr.seed_status_encoding in
    {|
      Storage_sigs.VALUE.encoding := encoding
    |}).

Module Seed.
  Definition unrevealed_nonce : Set := Cycle.unrevealed_nonce.

  Definition nonce_status : Set := Cycle.nonce_status.

  Module Nonce.
    Definition context : Set := Raw_context.t.

    Definition mem (ctxt : Raw_context.t) (l_value : Level_repr.t) : bool :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.mem)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level).

    Definition get (ctxt : Raw_context.t) (l_value : Level_repr.t)
      : M? Cycle.nonce_status :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.get)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level).

    Definition find (ctxt : Raw_context.t) (l_value : Level_repr.t)
      : M? (option Cycle.nonce_status) :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.find)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level).

    Definition update
      (ctxt : Raw_context.t) (l_value : Level_repr.t)
      (v_value : Cycle.nonce_status) : M? Raw_context.t :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.update)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level)
        v_value.

    Definition init_value
      (ctxt : Raw_context.t) (l_value : Level_repr.t)
      (v_value : Cycle.nonce_status) : M? Raw_context.t :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.init_value)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level)
        v_value.

    Definition add
      (ctxt : Raw_context.t) (l_value : Level_repr.t)
      (v_value : Cycle.nonce_status) : Raw_context.t :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.add)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level)
        v_value.

    Definition add_or_remove
      (ctxt : Raw_context.t) (l_value : Level_repr.t)
      (v_value : option Cycle.nonce_status) : Raw_context.t :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.add_or_remove)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level)
        v_value.

    Definition remove_existing (ctxt : Raw_context.t) (l_value : Level_repr.t)
      : M? Raw_context.t :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.remove_existing)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level).

    Definition remove (ctxt : Raw_context.t) (l_value : Level_repr.t)
      : Raw_context.t :=
      Cycle.Nonce.(Storage_sigs.Indexed_data_storage.remove)
        (ctxt, l_value.(Level_repr.t.cycle)) l_value.(Level_repr.t.level).

    (* Nonce *)
    Definition module :=
      {|
        Storage_sigs.Non_iterable_indexed_data_storage.mem := mem;
        Storage_sigs.Non_iterable_indexed_data_storage.get := get;
        Storage_sigs.Non_iterable_indexed_data_storage.find := find;
        Storage_sigs.Non_iterable_indexed_data_storage.update := update;
        Storage_sigs.Non_iterable_indexed_data_storage.init_value := init_value;
        Storage_sigs.Non_iterable_indexed_data_storage.add := add;
        Storage_sigs.Non_iterable_indexed_data_storage.add_or_remove :=
          add_or_remove;
        Storage_sigs.Non_iterable_indexed_data_storage.remove_existing :=
          remove_existing;
        Storage_sigs.Non_iterable_indexed_data_storage.remove := remove
      |}.
  End Nonce.
  Definition Nonce
    : Storage_sigs.Non_iterable_indexed_data_storage (t := Raw_context.t)
      (key := Level_repr.t) (value := nonce_status) := Nonce.module.

  Definition VDF_setup :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "vdf_challenge" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Seed_repr.vdf_setup in
      let encoding := Seed_repr.vdf_setup_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Module For_cycle.
    Definition init_value
      (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
      (seed_value : Seed_repr.seed) : M? Raw_context.t :=
      let? ctxt :=
        Cycle.Seed.(Storage_sigs.Indexed_data_storage_with_local_context.init_value)
          ctxt cycle seed_value in
      let ctxt :=
        Seed_status.(Storage_sigs.Single_data_storage.add) ctxt
          Seed_repr.RANDAO_seed in
      return? ctxt.

    Definition mem : Raw_context.t → Cycle_repr.t → bool :=
      Cycle.Seed.(Storage_sigs.Indexed_data_storage_with_local_context.mem).

    Definition get : Raw_context.t → Cycle_repr.t → M? Seed_repr.seed :=
      Cycle.Seed.(Storage_sigs.Indexed_data_storage_with_local_context.get).

    Definition update
      (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
      (seed_value : Seed_repr.seed) (status : Seed_repr.seed_status)
      : M? Raw_context.t :=
      let? ctxt :=
        Cycle.Seed.(Storage_sigs.Indexed_data_storage_with_local_context.update)
          ctxt cycle seed_value in
      Seed_status.(Storage_sigs.Single_data_storage.update) ctxt status.

    Definition remove_existing
      : Raw_context.t → Cycle_repr.t → M? Raw_context.t :=
      Cycle.Seed.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing).

    (* For_cycle *)
    Definition module :=
      {|
        FOR_CYCLE.init_value := init_value;
        FOR_CYCLE.mem := mem;
        FOR_CYCLE.get := get;
        FOR_CYCLE.update := update;
        FOR_CYCLE.remove_existing := remove_existing
      |}.
  End For_cycle.
  Definition For_cycle : FOR_CYCLE := For_cycle.module.

  Definition get_status : Raw_context.t → M? Seed_repr.seed_status :=
    Seed_status.(Storage_sigs.Single_data_storage.get).
End Seed.

Definition Commitments :=
  Storage_functors.Make_indexed_data_storage
    (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "commitments" ] in
      {|
        Storage_sigs.NAME.name := name
      |})) (Make_index Blinded_public_key_hash.Index)
    {|
      Storage_sigs.VALUE.encoding := Tez_repr.encoding
    |}.

Module Ramp_up.
  Module reward.
    Record record : Set := Build {
      baking_reward_fixed_portion : Tez_repr.t;
      baking_reward_bonus_per_slot : Tez_repr.t;
      endorsing_reward_per_slot : Tez_repr.t;
    }.
    Definition with_baking_reward_fixed_portion baking_reward_fixed_portion
      (r : record) :=
      Build baking_reward_fixed_portion r.(baking_reward_bonus_per_slot)
        r.(endorsing_reward_per_slot).
    Definition with_baking_reward_bonus_per_slot baking_reward_bonus_per_slot
      (r : record) :=
      Build r.(baking_reward_fixed_portion) baking_reward_bonus_per_slot
        r.(endorsing_reward_per_slot).
    Definition with_endorsing_reward_per_slot endorsing_reward_per_slot
      (r : record) :=
      Build r.(baking_reward_fixed_portion) r.(baking_reward_bonus_per_slot)
        endorsing_reward_per_slot.
  End reward.
  Definition reward := reward.record.

  Definition Rewards :=
    Storage_functors.Make_indexed_data_storage
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Raw_context.M
        (let name := [ "ramp_up"; "rewards" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Cycle_repr.Index)
      (let t : Set := reward in
      let encoding :=
        Data_encoding.conv
          (fun (function_parameter : reward) ⇒
            let '{|
              reward.baking_reward_fixed_portion := baking_reward_fixed_portion;
                reward.baking_reward_bonus_per_slot :=
                  baking_reward_bonus_per_slot;
                reward.endorsing_reward_per_slot := endorsing_reward_per_slot
                |} := function_parameter in
            (baking_reward_fixed_portion, baking_reward_bonus_per_slot,
              endorsing_reward_per_slot))
          (fun (function_parameter : Tez_repr.t × Tez_repr.t × Tez_repr.t) ⇒
            let
              '(baking_reward_fixed_portion, baking_reward_bonus_per_slot,
                endorsing_reward_per_slot) := function_parameter in
            {|
              reward.baking_reward_fixed_portion := baking_reward_fixed_portion;
              reward.baking_reward_bonus_per_slot :=
                baking_reward_bonus_per_slot;
              reward.endorsing_reward_per_slot := endorsing_reward_per_slot; |})
          None
          (Data_encoding.obj3
            (Data_encoding.req None None "baking_reward_fixed_portion"
              Tez_repr.encoding)
            (Data_encoding.req None None "baking_reward_bonus_per_slot"
              Tez_repr.encoding)
            (Data_encoding.req None None "endorsing_reward_per_slot"
              Tez_repr.encoding)) in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).
End Ramp_up.

Module Pending_migration.
  Definition Balance_updates :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "pending_migration_balance_updates" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Receipt_repr.balance_updates in
      let encoding := Receipt_repr.balance_updates_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Operation_results :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "pending_migration_operation_results" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := list Migration_repr.origination_result in
      let encoding := Migration_repr.origination_result_list_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition remove (ctxt : Raw_context.t)
    : M?
      (Raw_context.t × Receipt_repr.balance_updates ×
        Operation_results.(Storage_sigs.Single_data_storage.value)) :=
    let balance_updates (ctxt : Raw_context.t)
      : M? (Raw_context.t × Receipt_repr.balance_updates) :=
      let? function_parameter :=
        Balance_updates.(Storage_sigs.Single_data_storage.find) ctxt in
      match function_parameter with
      | Some balance_updates ⇒
        let ctxt :=
          Balance_updates.(Storage_sigs.Single_data_storage.remove) ctxt in
        return? (ctxt, balance_updates)
      | None ⇒ return? (ctxt, nil)
      end in
    let operation_results (ctxt : Raw_context.t)
      : M?
        (Raw_context.t ×
          Operation_results.(Storage_sigs.Single_data_storage.value)) :=
      let? function_parameter :=
        Operation_results.(Storage_sigs.Single_data_storage.find) ctxt in
      match function_parameter with
      | Some operation_results ⇒
        let ctxt :=
          Operation_results.(Storage_sigs.Single_data_storage.remove) ctxt in
        return? (ctxt, operation_results)
      | None ⇒ return? (ctxt, nil)
      end in
    let? '(ctxt, balance_updates) := balance_updates ctxt in
    let? '(ctxt, operation_results) := operation_results ctxt in
    return? (ctxt, balance_updates, operation_results).
End Pending_migration.

Module Liquidity_baking.
  Definition Toggle_ema :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "liquidity_baking_escape_ema" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Int32.

  Definition Cpmm_address :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context.M
      (let name := [ "liquidity_baking_cpmm_address" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Contract_hash.t in
      let encoding := Contract_repr.originated_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).
End Liquidity_baking.

Module Ticket_balance.
  Module Name.
    Definition name : list string := [ "ticket_balance" ].

    (* Name *)
    Definition module :=
      {|
        Storage_sigs.NAME.name := name
      |}.
  End Name.
  Definition Name := Name.module.

  Definition Raw_context :=
    Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      Name.

  Definition Paid_storage_space :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context
      (let name := [ "paid_bytes" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Z.

  Definition Used_storage_space :=
    Storage_functors.Make_single_data_storage Storage_functors.Registered
      Raw_context
      (let name := [ "used_bytes" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Encoding.Z.

  Definition Table_context :=
    Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
      (let name := [ "table" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition Index := Make_index Ticket_hash_repr.Index.

  Definition Table :
    Storage_sigs.Non_iterable_indexed_carbonated_data_storage
      (t := Raw_context.t) (key := Ticket_hash_repr.t) (value := Z.t) :=
    let functor_result :=
      Storage_functors.Make_indexed_carbonated_data_storage Table_context Index
        Encoding.Z in
    {|
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.mem);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.get);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.find);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.update);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.init_value);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.add_or_remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove_existing);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.remove);
      Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted :=
        functor_result.(Storage_sigs.Indexed_carbonated_data_storage.keys_unaccounted)
    |}.
End Ticket_balance.

Module Tx_rollup.
  Definition Indexed_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Raw_context.M
        (let name := [ "tx_rollup" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Tx_rollup_repr.Index).

  Definition State :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "state" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Tx_rollup_state_repr.encoding
      |}.

  Definition Level_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "tx_level" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Tx_rollup_level_repr.Index).

  Definition Inbox :=
    Level_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "inbox" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Tx_rollup_inbox_repr.t in
      let encoding := Tx_rollup_inbox_repr.encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Revealed_withdrawals :=
    Level_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "withdrawals" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      {|
        Storage_sigs.VALUE.encoding := Bitset.encoding
      |}.

  Definition Commitment :=
    Level_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "commitment" ] in
      {|
        Storage_sigs.NAME.name := name
      |}) Tx_rollup_commitment_repr.Submitted_commitment.

  Definition Bond_indexed_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered
        Indexed_context.(Storage_sigs.Indexed_raw_context.Raw_context)
        (let name := [ "bond" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) Public_key_hash_index.

  Definition Commitment_bond :=
    Bond_indexed_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "commitment" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := int in
      let encoding := Data_encoding.int31 in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).
End Tx_rollup.

Module Sc_rollup.
  Definition Raw_context :=
    Storage_functors.Make_subcontext Storage_functors.Registered Raw_context.M
      (let name := [ "sc_rollup" ] in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition Indexed_context :=
    Storage_functors.Make_indexed_subcontext
      (Storage_functors.Make_subcontext Storage_functors.Registered Raw_context
        (let name := [ "index" ] in
        {|
          Storage_sigs.NAME.name := name
        |})) (Make_index Sc_rollup_repr.Index).

  Module DATA_STORAGE.
    Record signature {context key value : Set} : Set := {
      context := context;
      key := key;
      value := value;
      get : context → key → M? (Raw_context.t × value);
      find : context → key → M? (Raw_context.t × option value);
      update : context → key → value → M? (Raw_context.t × int);
      init_value : context → key → value → M? (Raw_context.t × int);
      add : context → key → value → M? (Raw_context.t × int × bool);
      add_or_remove :
        context → key → option value → M? (Raw_context.t × int × bool);
    }.
  End DATA_STORAGE.
  Definition DATA_STORAGE := @DATA_STORAGE.signature.
  Arguments DATA_STORAGE {_ _ _}.

  Module Make_versioned.
    Class FArgs
      {Versioned_value_t Versioned_value_versioned Data_storage_context
        Data_storage_key : Set} := {
      Versioned_value :
        Sc_rollup_data_version_sig.S (t := Versioned_value_t)
          (versioned := Versioned_value_versioned);
      Data_storage :
        DATA_STORAGE (context := Data_storage_context) (key := Data_storage_key)
          (value := Versioned_value.(Sc_rollup_data_version_sig.S.versioned));
    }.
    Arguments Build_FArgs {_ _ _ _}.

    Definition value `{FArgs} : Set :=
      Versioned_value.(Sc_rollup_data_version_sig.S.t).

    Definition get `{FArgs}
      (ctxt : Data_storage.(DATA_STORAGE.context))
      (key_value : Data_storage.(DATA_STORAGE.key))
      : M? (Raw_context.t × Versioned_value.(Sc_rollup_data_version_sig.S.t)) :=
      let? '(ctxt, versioned) := Data_storage.(DATA_STORAGE.get) ctxt key_value
        in
      return?
        (ctxt,
          (Versioned_value.(Sc_rollup_data_version_sig.S.of_versioned) versioned)).

    Definition find `{FArgs}
      (ctxt : Data_storage.(DATA_STORAGE.context))
      (key_value : Data_storage.(DATA_STORAGE.key))
      : M?
        (Raw_context.t × option Versioned_value.(Sc_rollup_data_version_sig.S.t)) :=
      let? '(ctxt, versioned) := Data_storage.(DATA_STORAGE.find) ctxt key_value
        in
      return?
        (ctxt,
          (Option.map
            Versioned_value.(Sc_rollup_data_version_sig.S.of_versioned)
            versioned)).

    Definition update `{FArgs}
      (ctxt : Data_storage.(DATA_STORAGE.context))
      (key_value : Data_storage.(DATA_STORAGE.key))
      (value_value : Versioned_value.(Sc_rollup_data_version_sig.S.t))
      : M? (Raw_context.t × int) :=
      Data_storage.(DATA_STORAGE.update) ctxt key_value
        (Versioned_value.(Sc_rollup_data_version_sig.S.to_versioned) value_value).

    Definition init_value `{FArgs}
      (ctxt : Data_storage.(DATA_STORAGE.context))
      (key_value : Data_storage.(DATA_STORAGE.key))
      (value_value : Versioned_value.(Sc_rollup_data_version_sig.S.t))
      : M? (Raw_context.t × int) :=
      Data_storage.(DATA_STORAGE.init_value) ctxt key_value
        (Versioned_value.(Sc_rollup_data_version_sig.S.to_versioned) value_value).

    Definition add `{FArgs}
      (ctxt : Data_storage.(DATA_STORAGE.context))
      (key_value : Data_storage.(DATA_STORAGE.key))
      (value_value : Versioned_value.(Sc_rollup_data_version_sig.S.t))
      : M? (Raw_context.t × int × bool) :=
      Data_storage.(DATA_STORAGE.add) ctxt key_value
        (Versioned_value.(Sc_rollup_data_version_sig.S.to_versioned) value_value).

    Definition add_or_remove `{FArgs}
      (ctxt : Data_storage.(DATA_STORAGE.context))
      (key_value : Data_storage.(DATA_STORAGE.key))
      (value_value : option Versioned_value.(Sc_rollup_data_version_sig.S.t))
      : M? (Raw_context.t × int × bool) :=
      Data_storage.(DATA_STORAGE.add_or_remove) ctxt key_value
        (Option.map Versioned_value.(Sc_rollup_data_version_sig.S.to_versioned)
          value_value).

    (* Make_versioned *)
    Definition functor `{FArgs} :=
      {|
        DATA_STORAGE.get := get;
        DATA_STORAGE.find := find;
        DATA_STORAGE.update := update;
        DATA_STORAGE.init_value := init_value;
        DATA_STORAGE.add := add;
        DATA_STORAGE.add_or_remove := add_or_remove
      |}.
  End Make_versioned.
  Definition Make_versioned
    {Versioned_value_t Versioned_value_versioned Data_storage_context
      Data_storage_key : Set}
    (Versioned_value :
      Sc_rollup_data_version_sig.S (t := Versioned_value_t)
        (versioned := Versioned_value_versioned))
    (Data_storage :
      DATA_STORAGE (context := Data_storage_context) (key := Data_storage_key)
        (value := Versioned_value.(Sc_rollup_data_version_sig.S.versioned))) :=
    let '_ := Make_versioned.Build_FArgs Versioned_value Data_storage in
    Make_versioned.functor.

  Definition PVM_kind :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "kind" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Sc_rollups.Kind.t in
      let encoding := Sc_rollups.Kind.encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Parameters_type :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "parameters_type" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Script_repr.lazy_expr in
      let encoding := Script_repr.lazy_expr_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Definition Genesis_info :=
    Indexed_context.(Storage_sigs.Indexed_raw_context.Make_carbonated_map)
      Storage_functors.Registered
      (let name := [ "genesis_info" ] in
      {|
        Storage_sigs.NAME.name := name
      |})
      (let t : Set := Sc_rollup_commitment_repr.genesis_info in
      let encoding := Sc_rollup_commitment_repr.genesis_info_encoding in
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}).

  Module Inbox.
    Definition Inbox :=
      Storage_functors.Make_single_data_storage Storage_functors.Registered
        Raw_context
        (let name := [ "sc_rollup_inbox" ] in
        {|
          Storage_sigs.NAME.name := name
        |})
        (let t : Set := Sc_rollup_inbox_repr.versioned in
        let encoding := Sc_rollup_inbox_repr.versioned_encoding in
        {|
          Storage_sigs.VALUE.encoding := encoding
        |}).

    Definition context : Set := Raw_context.t.

    Definition mem : Raw_context.t → bool :=
      Inbox.(Storage_sigs.Single_data_storage.mem).

    Definition remove_existing : Raw_context.t → M? Raw_context.t :=
      Inbox.(Storage_sigs.Single_data_storage.remove_existing).

    Definition remove : Raw_context.t → Raw_context.t :=
      Inbox.(Storage_sigs.Single_data_storage.remove).

    Definition value : Set := Sc_rollup_inbox_repr.t.

    Definition of_versioned
      : Sc_rollup_inbox_repr.versioned → Sc_rollup_inbox_repr.V1.t :=
      Sc_rollup_inbox_repr.of_versioned.

    Definition to_versioned
      : Sc_rollup_inbox_repr.V1.t → Sc_rollup_inbox_repr.versioned :=
      Sc_rollup_inbox_repr.to_versioned.

    Definition get (ctxt : Raw_context.t) : M? Sc_rollup_inbox_repr.V1.t :=
      let? versioned := Inbox.(Storage_sigs.Single_data_storage.get) ctxt in
      return? (of_versioned versioned).

    Definition find (ctxt : Raw_context.t)
      : M? (option Sc_rollup_inbox_repr.V1.t) :=
      let? versioned := Inbox.(Storage_sigs.Single_data_storage.find) ctxt in
      return? (Option.map of_versioned versioned).

    Definition init_value
      (ctxt : Raw_context.t) (value_value : Sc_rollup_inbox_repr.V1.t)
      : M? Raw_context.t :=
      Inbox.(Storage_sigs.Single_data_storage.init_value) ctxt
        (to_versioned value_value