Skip to main content

🌌 Alpha_context.v

Translated OCaml

See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_repr.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Bootstrap_storage.
Require TezosOfOCaml.Proto_alpha.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Commitment_repr.
Require TezosOfOCaml.Proto_alpha.Commitment_storage.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_delegate_storage.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Dal_endorsement_repr.
Require TezosOfOCaml.Proto_alpha.Dal_errors_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_cycles.
Require TezosOfOCaml.Proto_alpha.Delegate_missed_endorsements_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_sampler.
Require TezosOfOCaml.Proto_alpha.Delegate_slashed_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Fees_storage.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Global_constants_storage.
Require TezosOfOCaml.Proto_alpha.Init_storage.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_storage.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_storage.
Require TezosOfOCaml.Proto_alpha.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Require TezosOfOCaml.Proto_alpha.Sapling_validator.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_arith.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_refutation_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_wasm.
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.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_builder.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_storage.
Require TezosOfOCaml.Proto_alpha.Time_repr.
Require TezosOfOCaml.Proto_alpha.Token.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_hash_builder.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_list_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Vote_storage.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_ticket_repr.

Definition t : Set := Raw_context.t.

Definition context : Set := t.

Module BASIC_DATA.
  Record signature {t : Set} : Set := {
    t := t;
    op_eq : t t bool;
    op_ltgt : t t bool;
    op_lt : t t bool;
    op_lteq : t t bool;
    op_gteq : t t bool;
    op_gt : t t bool;
    compare : t t int;
    equal : t t bool;
    max : t t t;
    min : t t t;
    encoding : Data_encoding.t t;
    pp : Format.formatter t unit;
  }.
End BASIC_DATA.
Definition BASIC_DATA := @BASIC_DATA.signature.
Arguments BASIC_DATA {_}.

Module Tez := Tez_repr.

Module Period := Period_repr.

Module Timestamp.
  Include Time_repr.

  Definition current : Raw_context.t Time.t := Raw_context.current_timestamp.

  Definition predecessor : Raw_context.t Time.t :=
    Raw_context.predecessor_timestamp.
End Timestamp.

Module Slot := Slot_repr.

Module Sc_rollup_repr := Sc_rollup_repr.

Module Sc_rollup.
  Module Tick := Sc_rollup_tick_repr.

  Include Sc_rollup_repr.

  Include Sc_rollup_PVM_sig.

  Module ArithPVM := Sc_rollup_arith.

  Module Wasm_2_0_0PVM := Sc_rollup_wasm.V2_0_0.

  Module Inbox_message := Sc_rollup_inbox_message_repr.

  Module Inbox.
    Include Sc_rollup_inbox_repr.

    Include Sc_rollup_inbox_storage.
  End Inbox.

  Module Proof := Sc_rollup_proof_repr.

  Module Game := Sc_rollup_game_repr.

  Module Commitment.
    Include Sc_rollup_commitment_repr.

    Include Sc_rollup_commitment_storage.
  End Commitment.

  Module Stake_storage.
    Include Sc_rollup_stake_storage.
  End Stake_storage.

  Module Refutation_storage := Sc_rollup_refutation_storage.

  Include Sc_rollup_storage.

  Include Sc_rollups.

  Module Outbox.
    Include Sc_rollup_outbox_storage.

    Module Message := Sc_rollup_outbox_message_repr.
  End Outbox.

  Module Errors := Sc_rollup_errors.
End Sc_rollup.

Module Dal.
  Module Slot_index.
    Include Dal_slot_repr.Index.
  End Slot_index.

  Module Endorsement.
    Include Dal_endorsement_repr.

    Include Raw_context.Dal.
  End Endorsement.

  Module Page.
    Include Dal_slot_repr.Page.
  End Page.

  Module Slot.
    Include Dal_slot_repr.

    Include Dal_slot_storage.

    Include Raw_context.Dal.
  End Slot.

  Module Slots_history := Dal_slot_repr.Slots_history.

  Module Slots_storage := Dal_slot_storage.
End Dal.

Module Dal_errors := Dal_errors_repr.

Module Zk_rollup.
  Include Zk_rollup_repr.

  Module State := Zk_rollup_state_repr.

  Module Account := Zk_rollup_account_repr.

  Module Operation := Zk_rollup_operation_repr.

  Module Ticket := Zk_rollup_ticket_repr.

  Module Errors := Zk_rollup_errors.

  Include Zk_rollup_storage.
End Zk_rollup.

Module Entrypoint := Entrypoint_repr.

Include Operation_repr.

Module Operation.
  Definition t : Set := operation.

  Definition packed : Set := packed_operation.

  Definition unsigned_encoding
    : Data_encoding.t (Operation.shell_header × packed_contents_list) :=
    unsigned_operation_encoding.

  Include Operation_repr.
End Operation.

Module Block_header := Block_header_repr.

Module Vote.
  Include Vote_repr.

  Include Vote_storage.
End Vote.

Module Block_payload.
  Include Block_payload_repr.
End Block_payload.

Module First_level_of_protocol.
  Definition get : Raw_context.t M? Raw_level_repr.t :=
    Storage.Tenderbake.First_level_of_protocol.(Storage_sigs.Single_data_storage.get).
End First_level_of_protocol.

Module Ratio := Ratio_repr.

Module Raw_level := Raw_level_repr.

Module Cycle := Cycle_repr.

Module Fees := Fees_storage.

Definition public_key : Set := Signature.public_key.

Definition public_key_hash : Set := Signature.public_key_hash.

Definition signature : Set := Signature.t.

Module Constants.
  Include Constants_repr.

  Include Constants_storage.

  Module Parametric := Constants_parametric_repr.

  Definition round_durations (ctxt : Raw_context.t) : Round_repr.Durations.t :=
    Raw_context.round_durations ctxt.

  Definition all (ctxt : Raw_context.t) : t :=
    all_of_parametric (parametric_value ctxt).
End Constants.

Module Voting_period.
  Include Voting_period_repr.

  Include Voting_period_storage.
End Voting_period.

Module Round.
  Include Round_repr.

  Definition round_durations : Set := Durations.t.

  Definition pp_round_durations : Format.formatter Durations.t unit :=
    Durations.pp.

  Definition round_durations_encoding : Data_encoding.encoding Durations.t :=
    Durations.encoding.

  Definition round_duration
    : Round_repr.Durations.t Round_repr.round Period_repr.t :=
    Round_repr.Durations.round_duration.

  Definition update (ctxt : Raw_context.t) (round : Round_repr.round)
    : M? Raw_context.t :=
    Storage.Block_round.(Storage.Simple_single_data_storage.update) ctxt round.

  Definition get (ctxt : Raw_context.t) : M? Round_repr.round :=
    Storage.Block_round.(Storage.Simple_single_data_storage.get) ctxt.
End Round.

Module Gas.
  Include Gas_limit_repr.

  Definition set_limit
    : Raw_context.t Gas_limit_repr.Arith.t Raw_context.t :=
    Raw_context.set_gas_limit.

  Definition consume_limit_in_block
    : Raw_context.t Gas_limit_repr.Arith.t M? Raw_context.t :=
    Raw_context.consume_gas_limit_in_block.

  Definition set_unlimited : Raw_context.t Raw_context.t :=
    Raw_context.set_gas_unlimited.

  Definition consume
    : Raw_context.t Gas_limit_repr.cost M? Raw_context.t :=
    Raw_context.consume_gas.

  Definition consume_from (available_gas : Arith.fp) (cost : cost)
    : M? Arith.fp :=
    match raw_consume available_gas cost with
    | Some remaining_gasreturn? remaining_gas
    | None
      Error_monad.error_value
        (Build_extensible "Operation_quota_exceeded" unit tt)
    end.

  Definition remaining_operation_gas
    : Raw_context.t Gas_limit_repr.Arith.fp :=
    Raw_context.remaining_operation_gas.

  Definition update_remaining_operation_gas
    : Raw_context.t Gas_limit_repr.Arith.fp Raw_context.t :=
    Raw_context.update_remaining_operation_gas.

  Definition reset_block_gas (ctxt : Raw_context.t) : Raw_context.t :=
    let gas := Arith.fp_value (Constants.hard_gas_limit_per_block ctxt) in
    Raw_context.update_remaining_block_gas ctxt gas.

  Definition level : Raw_context.t Gas_limit_repr.t := Raw_context.gas_level.

  Definition consumed
    : Raw_context.t Raw_context.t Gas_limit_repr.Arith.fp :=
    Raw_context.gas_consumed.

  Definition block_level : Raw_context.t Gas_limit_repr.Arith.fp :=
    Raw_context.block_gas_level.

  Definition cost_of_repr {A : Set} (cost : A) : A := cost.
End Gas.

Module Script.
  Include Michelson_v1_primitives.

  Include Script_repr.

  Inductive consume_deserialization_gas : Set :=
  | Always : consume_deserialization_gas
  | When_needed : consume_deserialization_gas.

  Definition force_decode_in_context
    (consume_deserialization_gas : consume_deserialization_gas)
    (ctxt : Raw_context.t) (lexpr : Script_repr.lazy_expr)
    : M? (Script_repr.expr × Raw_context.t) :=
    let gas_cost :=
      match consume_deserialization_gas with
      | AlwaysScript_repr.stable_force_decode_cost lexpr
      | When_neededScript_repr.force_decode_cost lexpr
      end in
    let? ctxt := Raw_context.consume_gas ctxt gas_cost in
    let? v_value := Script_repr.force_decode lexpr in
    return? (v_value, ctxt).

  Definition force_bytes_in_context
    (ctxt : Raw_context.t) (lexpr : Script_repr.lazy_expr)
    : M? (bytes × Raw_context.t) :=
    let? ctxt :=
      Raw_context.consume_gas ctxt (Script_repr.force_bytes_cost lexpr) in
    let? v_value := Script_repr.force_bytes lexpr in
    return? (v_value, ctxt).

  Definition consume_decoding_gas
    (available_gas : Gas.Arith.fp) (lexpr : Script_repr.lazy_expr)
    : M? Gas.Arith.fp :=
    let gas_cost := Script_repr.stable_force_decode_cost lexpr in
    Gas.consume_from available_gas gas_cost.
End Script.

Module Level.
  Include Level_repr.

  Include Level_storage.
End Level.

Module Lazy_storage.
  Module Kind := Lazy_storage_kind.

  Module IdSet := Kind.IdSet.

  Include Lazy_storage_diff.
End Lazy_storage.

Module Origination_nonce.
  Definition init_value : Raw_context.t Operation_hash.t Raw_context.t :=
    Raw_context.init_origination_nonce.

  Definition unset : Raw_context.t Raw_context.t :=
    Raw_context.unset_origination_nonce.
End Origination_nonce.

Module Destination := Destination_repr.

Module Contract.
  Include Contract_repr.

  Include Contract_storage.

  Definition is_manager_key_revealed
    : Raw_context.t Signature.public_key_hash M? bool :=
    Contract_manager_storage.is_manager_key_revealed.

  Definition check_public_key
    : Signature.public_key Signature.public_key_hash M? unit :=
    Contract_manager_storage.check_public_key.

  Definition reveal_manager_key
    : option bool Raw_context.t Signature.public_key_hash
    Signature.public_key M? Raw_context.t :=
    Contract_manager_storage.reveal_manager_key.

  Definition get_manager_key
    : option Error_monad._error Raw_context.t Signature.public_key_hash
    M? Signature.public_key := Contract_manager_storage.get_manager_key.

  Module Delegate.
    Definition find
      : Raw_context.t Contract_repr.t
      M? (option Signature.public_key_hash) := Contract_delegate_storage.find.

    Include Delegate_storage.Contract.
  End Delegate.
End Contract.

Module Tx_rollup_level := Tx_rollup_level_repr.

Module Tx_rollup_commitment_hash := Tx_rollup_commitment_repr.Hash.

Module Tx_rollup_message_result_hash := Tx_rollup_message_result_hash_repr.

Module Tx_rollup.
  Include Tx_rollup_repr.

  Include Tx_rollup_storage.
End Tx_rollup.

Module Tx_rollup_state.
  Include Tx_rollup_state_repr.

  Include Tx_rollup_state_storage.
End Tx_rollup_state.

Module Tx_rollup_withdraw := Tx_rollup_withdraw_repr.

Module Tx_rollup_withdraw_list_hash := Tx_rollup_withdraw_list_hash_repr.

Module Tx_rollup_message_result := Tx_rollup_message_result_repr.

Module Tx_rollup_reveal.
  Include Tx_rollup_reveal_repr.

  Include Tx_rollup_reveal_storage.
End Tx_rollup_reveal.

Module Tx_rollup_message.
  Include Tx_rollup_message_repr.

  Definition make_message (msg : t) : t × int := (msg, (size_value msg)).

  Definition make_batch (string_value : string) : t × int :=
    make_message (Tx_rollup_message_repr.Batch string_value).

  Definition make_deposit
    (sender : Signature.public_key_hash)
    (destination : Tx_rollup_l2_address.Indexable.value)
    (ticket_hash : Ticket_hash_repr.t) (amount : Tx_rollup_l2_qty.t)
    : t × int :=
    make_message
      (Tx_rollup_message_repr.Deposit
        {| Tx_rollup_message_repr.deposit.sender := sender;
          Tx_rollup_message_repr.deposit.destination := destination;
          Tx_rollup_message_repr.deposit.ticket_hash := ticket_hash;
          Tx_rollup_message_repr.deposit.amount := amount; |}).
End Tx_rollup_message.

Module Tx_rollup_message_hash := Tx_rollup_message_hash_repr.

Module Tx_rollup_inbox.
  Include Tx_rollup_inbox_repr.

  Include Tx_rollup_inbox_storage.
End Tx_rollup_inbox.

Module Tx_rollup_commitment.
  Include Tx_rollup_commitment_repr.

  Include Tx_rollup_commitment_storage.
End Tx_rollup_commitment.

Module Tx_rollup_hash := Tx_rollup_hash_builder.

Module Tx_rollup_errors := Tx_rollup_errors_repr.

Module Global_constants_storage := Global_constants_storage.

Module Big_map.
  Module Big_map := Lazy_storage_kind.Big_map.

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

    Definition encoding
      : Data_encoding.t Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
      Big_map.Id.(Lazy_storage_kind.ID.encoding).

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

    Definition parse_z
      : Z.t Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
      Big_map.Id.(Lazy_storage_kind.ID.parse_z).

    Definition unparse_to_z
      : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) Z.t :=
      Big_map.Id.(Lazy_storage_kind.ID.unparse_to_z).
  End Id.

  Definition fresh (temporary : bool) (c_value : Raw_context.t)
    : M? (Raw_context.t × Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)) :=
    (Lazy_storage.fresh (a := Big_map.alloc) (u := Big_map.updates))
      Lazy_storage_kind.Big_map temporary c_value.

  Definition mem
    (c_value : Raw_context.t) (m_value : Storage.Big_map.id)
    (k_value : Script_expr_hash.t) : M? (Raw_context.t × bool) :=
    Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.mem)
      (c_value, m_value) k_value.

  Definition get_opt
    (c_value : Raw_context.t) (m_value : Storage.Big_map.id)
    (k_value : Script_expr_hash.t)
    : M? (Raw_context.t × option Script_repr.expr) :=
    Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.find)
      (c_value, m_value) k_value.

  Definition list_key_values
    (offset : option int) (length : option int) (c_value : Raw_context.t)
    (m_value : Storage.Big_map.id)
    : M? (Raw_context.t × list (Script_expr_hash.t × Script_repr.expr)) :=
    Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.list_key_values)
      offset length (c_value, m_value).

  Definition _exists
    (c_value : Raw_context.t)
    (id : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
    : M? (Raw_context.t × option (Script_repr.expr × Script_repr.expr)) :=
    let? c_value :=
      Raw_context.consume_gas c_value (Gas_limit_repr.read_bytes_cost 0) in
    let? kt :=
      Storage.Big_map.Key_type.(Storage_sigs.Indexed_data_storage.find) c_value
        id in
    match kt with
    | Nonereturn? (c_value, None)
    | Some kt
      let? kv :=
        Storage.Big_map.Value_type.(Storage_sigs.Indexed_data_storage.get)
          c_value id in
      return? (c_value, (Some (kt, kv)))
    end.

  Definition update : Set := Big_map.update.

  Definition updates : Set := Big_map.updates.

  Definition alloc : Set := Big_map.alloc.
End Big_map.

Module Sapling.
  Module Sapling_state := Lazy_storage_kind.Sapling_state.

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

    Definition encoding
      : Data_encoding.t
        Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
      Sapling_state.Id.(Lazy_storage_kind.ID.encoding).

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

    Definition parse_z
      : Z.t Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
      Sapling_state.Id.(Lazy_storage_kind.ID.parse_z).

    Definition unparse_to_z
      : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) Z.t :=
      Sapling_state.Id.(Lazy_storage_kind.ID.unparse_to_z).
  End Id.

  Include Sapling_repr.

  Include Sapling_storage.

  Include Sapling_validator.

  Definition fresh (temporary : bool) (c_value : Raw_context.t)
    : M?
      (Raw_context.t ×
        Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t)) :=
    (Lazy_storage.fresh (a := Sapling_state.alloc) (u := Sapling_state.updates))
      Lazy_storage_kind.Sapling_state temporary c_value.

  Definition updates : Set := Sapling_state.updates.

  Definition alloc : Set := Sapling_state.alloc.

  Module Legacy.
    Include Sapling.UTXO.Legacy.

    Definition transaction_get_memo_size (transaction : transaction)
      : option int :=
      match
        transaction.(Sapling.Legacy.transaction.outputs)
        with
      | []None
      | cons {| Sapling.UTXO.output.ciphertext := ciphertext |} _
        Some (Sapling.Ciphertext.get_memo_size ciphertext)
      end.

    Definition transaction_in_memory_size (transaction : transaction)
      : Saturation_repr.t := transaction_in_memory_size (cast transaction).

    Definition verify_update
      (ctxt : Raw_context.t) (state_value : Sapling_storage.state)
      (transaction : transaction) (key_value : string)
      : M? (Raw_context.t × option (Int64.t × Sapling_storage.state)) :=
      verify_update ctxt state_value (cast transaction) key_value.
  End Legacy.
End Sapling.

Module Bond_id.
  Include Bond_id_repr.
End Bond_id.

Module Receipt := Receipt_repr.

Module Consensus_key := Delegate_consensus_key.

Module Delegate.
  Include Delegate_storage.

  Include Delegate_missed_endorsements_storage.

  Include Delegate_slashed_deposits_storage.

  Include Delegate_cycles.

  Definition deposits : Set := Storage.deposits.

  Definition last_cycle_before_deactivation
    : Raw_context.t Signature.public_key_hash M? Cycle_repr.t :=
    Delegate_activation_storage.last_cycle_before_deactivation.

  Definition prepare_stake_distribution : Raw_context.t M? Raw_context.t :=
    Stake_storage.prepare_stake_distribution.

  Definition delegated_contracts
    : Raw_context.t Signature.public_key_hash M? (list Contract_repr.t) :=
    Contract_delegate_storage.delegated_contracts.

  Definition deactivated
    : Raw_context.t Signature.public_key_hash M? bool :=
    Delegate_activation_storage.is_inactive.

  Module Consensus_key := Delegate_consensus_key.
End Delegate.

Module Stake_distribution.
  Definition snapshot_value : Raw_context.t M? Raw_context.t :=
    Stake_storage.snapshot_value.

  Definition compute_snapshot_index
    : Raw_context.t Cycle_repr.t int M? int :=
    Delegate_sampler.compute_snapshot_index.

  Definition baking_rights_owner
    : Raw_context.t Level_repr.t Round_repr.round
    M? (Raw_context.t × Slot_repr.t × Delegate_consensus_key.pk) :=
    Delegate_sampler.baking_rights_owner.

  Definition slot_owner
    : Raw_context.t Level_repr.t Slot_repr.t
    M? (Raw_context.t × Delegate_consensus_key.pk) :=
    Delegate_sampler.slot_owner.
End Stake_distribution.

Module Nonce := Nonce_storage.

Module Seed.
  Include Seed_repr.

  Include Seed_storage.
End Seed.

Module Fitness.
  Definition raw : Set := Environment.V7.Fitness.t.

  Include Fitness_repr.
End Fitness.

Module Bootstrap := Bootstrap_storage.

Module Commitment.
  Include Commitment_repr.

  Include Commitment_storage.
End Commitment.

Module Migration := Migration_repr.

Module Consensus.
Inclusion of the module [Raw_context.Consensus]
  Definition allowed_endorsements :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.allowed_endorsements).

  Definition allowed_preendorsements :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.allowed_preendorsements).

  Definition current_endorsement_power :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.current_endorsement_power).

  Definition initialize_consensus_operation :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.initialize_consensus_operation).

  Definition record_grand_parent_endorsement :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.record_grand_parent_endorsement).

  Definition record_endorsement :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.record_endorsement).

  Definition record_preendorsement :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.record_preendorsement).

  Definition endorsements_seen :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.endorsements_seen).

  Definition get_preendorsements_quorum_round :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.get_preendorsements_quorum_round).

  Definition set_preendorsements_quorum_round :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.set_preendorsements_quorum_round).

  Definition locked_round_evidence :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.locked_round_evidence).

  Definition set_endorsement_branch :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.set_endorsement_branch).

  Definition endorsement_branch :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.endorsement_branch).

  Definition set_grand_parent_branch :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.set_grand_parent_branch).

  Definition grand_parent_branch :=
    Raw_context.Consensus.(Raw_context.CONSENSUS.grand_parent_branch).

  Definition load_endorsement_branch (ctxt : Raw_context.t)
    : M? Raw_context.t :=
    let? function_parameter :=
      Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.find)
        ctxt in
    match function_parameter with
    | Some endorsement_branch
      return?
        (Raw_context.Consensus.(Raw_context.CONSENSUS.set_endorsement_branch)
          ctxt endorsement_branch)
    | Nonereturn? ctxt
    end.

  Definition store_endorsement_branch
    (ctxt : Raw_context.t)
    (branch :
      Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.value))
    : Raw_context.t :=
    let ctxt := set_endorsement_branch ctxt branch in
    Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.add)
      ctxt branch.

  Definition load_grand_parent_branch (ctxt : Raw_context.t)
    : M? Raw_context.t :=
    let? function_parameter :=
      Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.find)
        ctxt in
    match function_parameter with
    | Some grand_parent_branch
      return?
        (Raw_context.Consensus.(Raw_context.CONSENSUS.set_grand_parent_branch)
          ctxt grand_parent_branch)
    | Nonereturn? ctxt
    end.

  Definition store_grand_parent_branch
    (ctxt : Raw_context.t)
    (branch :
      Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.value))
    : Raw_context.t :=
    let ctxt := set_grand_parent_branch ctxt branch in
    Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.add)
      ctxt branch.
End Consensus.

Definition prepare_first_block
  : Chain_id.t Context.t
  (Raw_context.t Script_repr.t
  M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
  int32 Time.t M? Raw_context.t := Init_storage.prepare_first_block.

Definition prepare
  (ctxt : Context.t) (level : Int32.t) (predecessor_timestamp : Time.t)
  (timestamp : Time.t)
  : M?
    (Raw_context.t × Receipt_repr.balance_updates ×
      list Migration_repr.origination_result) :=
  let? '(ctxt, balance_updates, origination_results) :=
    Init_storage.prepare ctxt level predecessor_timestamp timestamp in
  let? ctxt := Consensus.load_endorsement_branch ctxt in
  let? ctxt := Consensus.load_grand_parent_branch ctxt in
  return? (ctxt, balance_updates, origination_results).

Definition finalize
  (message : option string) (c_value : Raw_context.t) (fitness : Environment.V7.Fitness.t)
  : M? Updater.validation_result :=
  let? last_allowed_fork_level := Level.last_allowed_fork_level c_value in
  let context_value := Raw_context.recover c_value in
  return?
    {| Updater.validation_result.context := context_value;
      Updater.validation_result.fitness := fitness;
      Updater.validation_result.message := message;
      Updater.validation_result.max_operations_ttl :=
        (Raw_context.constants c_value).(Constants_parametric_repr.t.max_operations_time_to_live);
      Updater.validation_result.last_allowed_fork_level :=
        Raw_level.to_int32 last_allowed_fork_level; |}.

Definition current_context (c_value : Raw_context.t) : Context.t :=
  Raw_context.recover c_value.

Definition record_non_consensus_operation_hash
  : Raw_context.t Operation_hash.t Raw_context.t :=
  Raw_context.record_non_consensus_operation_hash.

Definition non_consensus_operations : Raw_context.t list Operation_hash.t :=
  Raw_context.non_consensus_operations.

Definition record_dictator_proposal_seen : Raw_context.t Raw_context.t :=
  Raw_context.record_dictator_proposal_seen.

Definition dictator_proposal_seen : Raw_context.t bool :=
  Raw_context.dictator_proposal_seen.

Definition activate : Raw_context.t Protocol_hash.t Raw_context.t :=
  Raw_context.activate.

Definition reset_internal_nonce : Raw_context.t Raw_context.t :=
  Raw_context.reset_internal_nonce.

Definition fresh_internal_nonce : Raw_context.t M? (Raw_context.t × int) :=
  Raw_context.fresh_internal_nonce.

Definition record_internal_nonce : Raw_context.t int Raw_context.t :=
  Raw_context.record_internal_nonce.

Definition internal_nonce_already_recorded : Raw_context.t int bool :=
  Raw_context.internal_nonce_already_recorded.

Definition description : Storage_description.t Raw_context.t :=
  Raw_context.description.

Module Parameters := Parameters_repr.

Module Liquidity_baking.
  Include Liquidity_baking_repr.

  Include Liquidity_baking_storage.
End Liquidity_baking.

Module Ticket_hash.
  Include Ticket_hash_repr.

  Include Ticket_hash_builder.
End Ticket_hash.

Module Ticket_balance.
  Include Ticket_storage.
End Ticket_balance.

Module Ticket_receipt.
  Include Ticket_receipt_repr.
End Ticket_receipt.

Module Token := Token.

Module Cache := Cache_repr.