Skip to main content

🖼️ Raw_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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context_intf.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.State_hash.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.

Definition Int_set :=
  _Set.Make
    {|
      Compare.COMPARABLE.compare := Compare.Int.compare
    |}.

Module Raw_consensus.
  Module t.
    Record record : Set := Build {
      current_endorsement_power : int;
      allowed_endorsements :
        Slot_repr.Map.(Map.S.t)
          (Signature.public_key × Signature.public_key_hash × int);
      allowed_preendorsements :
        Slot_repr.Map.(Map.S.t)
          (Signature.public_key × Signature.public_key_hash × int);
      grand_parent_endorsements_seen :
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t);
      endorsements_seen : Slot_repr._Set.(_Set.S.t);
      preendorsements_seen : Slot_repr._Set.(_Set.S.t);
      locked_round_evidence : option (Round_repr.t × int);
      preendorsements_quorum_round : option Round_repr.t;
      endorsement_branch : option (Block_hash.t × Block_payload_hash.t);
      grand_parent_branch : option (Block_hash.t × Block_payload_hash.t);
    }.
    Definition with_current_endorsement_power current_endorsement_power
      (r : record) :=
      Build current_endorsement_power r.(allowed_endorsements)
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_allowed_endorsements allowed_endorsements (r : record) :=
      Build r.(current_endorsement_power) allowed_endorsements
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_allowed_preendorsements allowed_preendorsements
      (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        allowed_preendorsements r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_grand_parent_endorsements_seen
      grand_parent_endorsements_seen (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        r.(allowed_preendorsements) grand_parent_endorsements_seen
        r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_endorsements_seen endorsements_seen (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        endorsements_seen r.(preendorsements_seen) r.(locked_round_evidence)
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_preendorsements_seen preendorsements_seen (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) preendorsements_seen r.(locked_round_evidence)
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_locked_round_evidence locked_round_evidence (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) r.(preendorsements_seen) locked_round_evidence
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_preendorsements_quorum_round preendorsements_quorum_round
      (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
        preendorsements_quorum_round r.(endorsement_branch)
        r.(grand_parent_branch).
    Definition with_endorsement_branch endorsement_branch (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
        r.(preendorsements_quorum_round) endorsement_branch
        r.(grand_parent_branch).
    Definition with_grand_parent_branch grand_parent_branch (r : record) :=
      Build r.(current_endorsement_power) r.(allowed_endorsements)
        r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
        r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
        r.(preendorsements_quorum_round) r.(endorsement_branch)
        grand_parent_branch.
  End t.
  Definition t := t.record.

  Definition empty : t :=
    {| t.current_endorsement_power := 0;
      t.allowed_endorsements := Slot_repr.Map.(Map.S.empty);
      t.allowed_preendorsements := Slot_repr.Map.(Map.S.empty);
      t.grand_parent_endorsements_seen :=
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty);
      t.endorsements_seen := Slot_repr._Set.(_Set.S.empty);
      t.preendorsements_seen := Slot_repr._Set.(_Set.S.empty);
      t.locked_round_evidence := None; t.preendorsements_quorum_round := None;
      t.endorsement_branch := None; t.grand_parent_branch := None; |}.

Init function; without side-effects in Coq
  Definition init_module1 : unit :=
    Error_monad.register_error_kind Error_monad.Branch
      "operation.double_inclusion_of_consensus_operation"
      "Double inclusion of consensus operation"
      "double inclusion of consensus operation"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Double inclusion of consensus operation"
                  CamlinternalFormatBasics.End_of_format)
                "Double inclusion of consensus operation"))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Double_inclusion_of_consensus_operation" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Double_inclusion_of_consensus_operation" unit tt).

  Definition record_grand_parent_endorsement
    (t_value : t) (pkh : Signature.public_key_hash) : M? t :=
    let? '_ :=
      Error_monad.error_when
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.mem)
          pkh t_value.(t.grand_parent_endorsements_seen))
        (Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
    return?
      (t.with_grand_parent_endorsements_seen
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.add)
          pkh t_value.(t.grand_parent_endorsements_seen)) t_value).

  Definition record_endorsement
    (t_value : t) (initial_slot : Slot_repr.t) (power : int) : M? t :=
    let? '_ :=
      Error_monad.error_when
        (Slot_repr._Set.(_Set.S.mem) initial_slot t_value.(t.endorsements_seen))
        (Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
    return?
      (t.with_endorsements_seen
        (Slot_repr._Set.(_Set.S.add) initial_slot t_value.(t.endorsements_seen))
        (t.with_current_endorsement_power
          (t_value.(t.current_endorsement_power) +i power) t_value)).

  Definition record_preendorsement
    (initial_slot : Slot_repr.t) (power : int) (round : Round_repr.t)
    (t_value : t) : M? t :=
    let? '_ :=
      Error_monad.error_when
        (Slot_repr._Set.(_Set.S.mem) initial_slot
          t_value.(t.preendorsements_seen))
        (Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
    let locked_round_evidence :=
      match t_value.(t.locked_round_evidence) with
      | NoneSome (round, power)
      | Some (_stored_round, evidences)Some (round, (evidences +i power))
      end in
    return?
      (t.with_locked_round_evidence locked_round_evidence
        (t.with_preendorsements_seen
          (Slot_repr._Set.(_Set.S.add) initial_slot
            t_value.(t.preendorsements_seen)) t_value)).

  Definition set_preendorsements_quorum_round
    (round : Round_repr.t) (t_value : t) : t :=
    match t_value.(t.preendorsements_quorum_round) with
    | Some round'
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit (Round_repr.equal round round') in
      t_value
    | Nonet.with_preendorsements_quorum_round (Some round) t_value
    end.

  Definition initialize_with_endorsements_and_preendorsements
    (allowed_endorsements :
      Slot_repr.Map.(Map.S.t)
        (Signature.public_key × Signature.public_key_hash × int))
    (allowed_preendorsements :
      Slot_repr.Map.(Map.S.t)
        (Signature.public_key × Signature.public_key_hash × int)) (t_value : t)
    : t :=
    t.with_allowed_preendorsements allowed_preendorsements
      (t.with_allowed_endorsements allowed_endorsements t_value).

  Definition locked_round_evidence (t_value : t)
    : option (Round_repr.t × int) := t_value.(t.locked_round_evidence).

  Definition endorsement_branch (t_value : t)
    : option (Block_hash.t × Block_payload_hash.t) :=
    t_value.(t.endorsement_branch).

  Definition grand_parent_branch (t_value : t)
    : option (Block_hash.t × Block_payload_hash.t) :=
    t_value.(t.grand_parent_branch).

  Definition set_endorsement_branch
    (t_value : t) (endorsement_branch : Block_hash.t × Block_payload_hash.t)
    : t := t.with_endorsement_branch (Some endorsement_branch) t_value.

  Definition set_grand_parent_branch
    (t_value : t) (grand_parent_branch : Block_hash.t × Block_payload_hash.t)
    : t := t.with_grand_parent_branch (Some grand_parent_branch) t_value.
End Raw_consensus.

Module back.
  Record record : Set := Build {
    context : Context.t;
    constants : Constants_repr.parametric;
    round_durations : Round_repr.Durations.t;
    cycle_eras : Level_repr.cycle_eras;
    level : Level_repr.t;
    predecessor_timestamp : Time.t;
    timestamp : Time.t;
    fees : Tez_repr.t;
    origination_nonce : option Origination_nonce.t;
    temporary_lazy_storage_ids : Lazy_storage_kind.Temp_ids.t;
    internal_nonce : int;
    internal_nonces_used : Int_set.(_Set.S.t);
    remaining_block_gas : Gas_limit_repr.Arith.fp;
    unlimited_operation_gas : bool;
    consensus : Raw_consensus.t;
    non_consensus_operations_rev : list Operation_hash.t;
    sampler_state :
      Cycle_repr.Map.(Map.S.t)
        (Seed_repr.seed ×
          Sampler.t (Signature.public_key × Signature.public_key_hash));
    stake_distribution_for_current_cycle :
      option
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
          Tez_repr.t);
    tx_rollup_current_messages :
      Tx_rollup_repr.Map.(Map.S.t) Tx_rollup_inbox_repr.Merkle.tree;
    sc_rollup_current_messages :
      Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.t) Context.tree;
  }.
  Definition with_context context (r : record) :=
    Build context r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_constants constants (r : record) :=
    Build r.(context) constants r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_round_durations round_durations (r : record) :=
    Build r.(context) r.(constants) round_durations r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_cycle_eras cycle_eras (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) cycle_eras r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_level level (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) level
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_predecessor_timestamp predecessor_timestamp (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      predecessor_timestamp r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_timestamp timestamp (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) timestamp r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_fees fees (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) fees r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_origination_nonce origination_nonce (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) origination_nonce
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_temporary_lazy_storage_ids temporary_lazy_storage_ids
    (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      temporary_lazy_storage_ids r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_internal_nonce internal_nonce (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) internal_nonce r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_internal_nonces_used internal_nonces_used (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) internal_nonces_used
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_remaining_block_gas remaining_block_gas (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      remaining_block_gas r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_unlimited_operation_gas unlimited_operation_gas
    (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) unlimited_operation_gas r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_consensus consensus (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) consensus
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_non_consensus_operations_rev non_consensus_operations_rev
    (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      non_consensus_operations_rev r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_sampler_state sampler_state (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) sampler_state
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_stake_distribution_for_current_cycle
    stake_distribution_for_current_cycle (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      stake_distribution_for_current_cycle r.(tx_rollup_current_messages)
      r.(sc_rollup_current_messages).
  Definition with_tx_rollup_current_messages tx_rollup_current_messages
    (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) tx_rollup_current_messages
      r.(sc_rollup_current_messages).
  Definition with_sc_rollup_current_messages sc_rollup_current_messages
    (r : record) :=
    Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
      r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
      r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
      r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
      r.(non_consensus_operations_rev) r.(sampler_state)
      r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
      sc_rollup_current_messages.
End back.
Definition back := back.record.

Module t.
  Record record : Set := Build {
    remaining_operation_gas : Gas_limit_repr.Arith.fp;
    back : back;
  }.
  Definition with_remaining_operation_gas remaining_operation_gas
    (r : record) :=
    Build remaining_operation_gas r.(back).
  Definition with_back back (r : record) :=
    Build r.(remaining_operation_gas) back.
End t.
Definition t := t.record.

Definition root : Set := t.

Definition context_value (ctxt : t) : Context.t := ctxt.(t.back).(back.context).

Definition current_level (ctxt : t) : Level_repr.t :=
  ctxt.(t.back).(back.level).

Definition predecessor_timestamp (ctxt : t) : Time.t :=
  ctxt.(t.back).(back.predecessor_timestamp).

Definition current_timestamp (ctxt : t) : Time.t :=
  ctxt.(t.back).(back.timestamp).

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

Definition cycle_eras (ctxt : t) : Level_repr.cycle_eras :=
  ctxt.(t.back).(back.cycle_eras).

Definition constants (ctxt : t) : Constants_repr.parametric :=
  ctxt.(t.back).(back.constants).

Definition recover (ctxt : t) : Context.t := ctxt.(t.back).(back.context).

Definition fees (ctxt : t) : Tez_repr.t := ctxt.(t.back).(back.fees).

Definition origination_nonce (ctxt : t) : option Origination_nonce.t :=
  ctxt.(t.back).(back.origination_nonce).

Definition internal_nonce (ctxt : t) : int :=
  ctxt.(t.back).(back.internal_nonce).

Definition internal_nonces_used (ctxt : t) : Int_set.(_Set.S.t) :=
  ctxt.(t.back).(back.internal_nonces_used).

Definition remaining_block_gas (ctxt : t) : Gas_limit_repr.Arith.fp :=
  ctxt.(t.back).(back.remaining_block_gas).

Definition unlimited_operation_gas (ctxt : t) : bool :=
  ctxt.(t.back).(back.unlimited_operation_gas).

Definition temporary_lazy_storage_ids (ctxt : t)
  : Lazy_storage_kind.Temp_ids.t :=
  ctxt.(t.back).(back.temporary_lazy_storage_ids).

Definition remaining_operation_gas (ctxt : t) : Gas_limit_repr.Arith.fp :=
  ctxt.(t.remaining_operation_gas).

Definition non_consensus_operations_rev (ctxt : t) : list Operation_hash.t :=
  ctxt.(t.back).(back.non_consensus_operations_rev).

Definition sampler_state (ctxt : t)
  : Cycle_repr.Map.(Map.S.t)
    (Seed_repr.seed ×
      Sampler.t (Signature.public_key × Signature.public_key_hash)) :=
  ctxt.(t.back).(back.sampler_state).

Definition update_back (ctxt : t) (back : back) : t := t.with_back back ctxt.

Definition update_remaining_block_gas
  (ctxt : t) (remaining_block_gas : Gas_limit_repr.Arith.fp) : t :=
  update_back ctxt
    (back.with_remaining_block_gas remaining_block_gas ctxt.(t.back)).

Definition update_remaining_operation_gas
  (ctxt : t) (remaining_operation_gas : Gas_limit_repr.Arith.fp) : t :=
  t.with_remaining_operation_gas remaining_operation_gas ctxt.

Definition update_unlimited_operation_gas
  (ctxt : t) (unlimited_operation_gas : bool) : t :=
  update_back ctxt
    (back.with_unlimited_operation_gas unlimited_operation_gas ctxt.(t.back)).

Definition update_context (ctxt : t) (context_value : Context.t) : t :=
  update_back ctxt (back.with_context context_value ctxt.(t.back)).

Definition update_constants (ctxt : t) (constants : Constants_repr.parametric)
  : t := update_back ctxt (back.with_constants constants ctxt.(t.back)).

Definition update_origination_nonce
  (ctxt : t) (origination_nonce : option Origination_nonce.t) : t :=
  update_back ctxt (back.with_origination_nonce origination_nonce ctxt.(t.back)).

Definition update_internal_nonce (ctxt : t) (internal_nonce : int) : t :=
  update_back ctxt (back.with_internal_nonce internal_nonce ctxt.(t.back)).

Definition update_internal_nonces_used
  (ctxt : t) (internal_nonces_used : Int_set.(_Set.S.t)) : t :=
  update_back ctxt
    (back.with_internal_nonces_used internal_nonces_used ctxt.(t.back)).

Definition update_fees (ctxt : t) (fees : Tez_repr.t) : t :=
  update_back ctxt (back.with_fees fees ctxt.(t.back)).

Definition update_temporary_lazy_storage_ids
  (ctxt : t) (temporary_lazy_storage_ids : Lazy_storage_kind.Temp_ids.t) : t :=
  update_back ctxt
    (back.with_temporary_lazy_storage_ids temporary_lazy_storage_ids
      ctxt.(t.back)).

Definition update_non_consensus_operations_rev
  (ctxt : t) (non_consensus_operations_rev : list Operation_hash.t) : t :=
  update_back ctxt
    (back.with_non_consensus_operations_rev non_consensus_operations_rev
      ctxt.(t.back)).

Definition update_sampler_state
  (ctxt : t)
  (sampler_state :
    Cycle_repr.Map.(Map.S.t)
      (Seed_repr.seed ×
        Sampler.t (Signature.public_key × Signature.public_key_hash))) : t :=
  update_back ctxt (back.with_sampler_state sampler_state ctxt.(t.back)).

Init function; without side-effects in Coq
Definition init_module2 : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "too_many_internal_operations" "Too many internal operations"
      "A transaction exceeded the hard limit of internal operations it can emit"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Too_many_internal_operations" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_internal_operations" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "gas_exhausted.operation" "Gas quota exceeded for the operation"
      "A script or one of its callee took more time than the operation said it would"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Operation_quota_exceeded" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Operation_quota_exceeded" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "gas_exhausted.block"
      "Gas quota exceeded for the block"
      "The sum of gas consumed by all the operations in the block exceeds the hard gas limit per block"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Block_quota_exceeded" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Block_quota_exceeded" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "delegate.stake_distribution_not_set" "Stake distribution not set"
      "The stake distribution for the current cycle is not set."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The stake distribution for the current cycle is not set."
                  CamlinternalFormatBasics.End_of_format)
                "The stake distribution for the current cycle is not set.")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Stake_distribution_not_set" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Stake_distribution_not_set" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent "sampler_already_set"
    "Sampler already set"
    "Internal error: Raw_context.set_sampler_for_cycle was called twice for a given cycle"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (c_value : Cycle_repr.cycle) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Internal error: sampler already set for cycle "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Char_literal "." % char
                    CamlinternalFormatBasics.End_of_format)))
              "Internal error: sampler already set for cycle %a.") Cycle_repr.pp
            c_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "cycle" Cycle_repr.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Sampler_already_set" then
          let c_value := cast Cycle_repr.t payload in
          Some c_value
        else None
      end)
    (fun (c_value : Cycle_repr.cycle) ⇒
      Build_extensible "Sampler_already_set" Cycle_repr.cycle c_value).

Definition fresh_internal_nonce (ctxt : t) : M? (t × int) :=
  if (internal_nonce ctxt) i 65535 then
    Error_monad.error_value
      (Build_extensible "Too_many_internal_operations" unit tt)
  else
    return?
      ((update_internal_nonce ctxt ((internal_nonce ctxt) +i 1)),
        (internal_nonce ctxt)).

Definition reset_internal_nonce (ctxt : t) : t :=
  let ctxt := update_internal_nonce ctxt 0 in
  update_internal_nonces_used ctxt Int_set.(_Set.S.empty).

Definition record_internal_nonce (ctxt : t) (k_value : Compare.Int.t) : t :=
  update_internal_nonces_used ctxt
    (Int_set.(_Set.S.add) k_value (internal_nonces_used ctxt)).

Definition internal_nonce_already_recorded (ctxt : t) (k_value : Compare.Int.t)
  : bool := Int_set.(_Set.S.mem) k_value (internal_nonces_used ctxt).

Definition get_collected_fees (ctxt : t) : Tez_repr.t := fees ctxt.

Definition credit_collected_fees_only_call_from_token
  (ctxt : t) (fees' : Tez_repr.t) : M? t :=
  let previous := get_collected_fees ctxt in
  let? fees := Tez_repr.op_plusquestion previous fees' in
  return? (update_fees ctxt fees).

Definition spend_collected_fees_only_call_from_token
  (ctxt : t) (fees' : Tez_repr.t) : M? t :=
  let previous := get_collected_fees ctxt in
  let? fees := Tez_repr.op_minusquestion previous fees' in
  return? (update_fees ctxt fees).

Init function; without side-effects in Coq
Definition init_module3 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "undefined_operation_nonce" "Ill timed access to the origination nonce"
    "An origination was attempted out of the scope of a manager operation" None
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Undefined_operation_nonce" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Undefined_operation_nonce" unit tt).

Definition init_origination_nonce (ctxt : t) (operation_hash : Operation_hash.t)
  : t :=
  let origination_nonce := Some (Origination_nonce.initial operation_hash) in
  update_origination_nonce ctxt origination_nonce.

Definition increment_origination_nonce (ctxt : t)
  : M? (t × Origination_nonce.t) :=
  match origination_nonce ctxt with
  | None
    Error_monad.error_value
      (Build_extensible "Undefined_operation_nonce" unit tt)
  | Some cur_origination_nonce
    let origination_nonce := Some (Origination_nonce.incr cur_origination_nonce)
      in
    let ctxt := update_origination_nonce ctxt origination_nonce in
    return? (ctxt, cur_origination_nonce)
  end.

Definition get_origination_nonce (ctxt : t) : M? Origination_nonce.t :=
  match origination_nonce ctxt with
  | None
    Error_monad.error_value
      (Build_extensible "Undefined_operation_nonce" unit tt)
  | Some origination_noncereturn? origination_nonce
  end.

Definition unset_origination_nonce (ctxt : t) : t :=
  update_origination_nonce ctxt None.

Init function; without side-effects in Coq
Definition init_module4 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent "gas_limit_too_high"
    "Gas limit out of protocol hard bounds"
    "A transaction tried to exceed the hard limit on gas" None
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Gas_limit_too_high" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Gas_limit_too_high" unit tt).

Definition gas_level (ctxt : t) : Gas_limit_repr.t :=
  if unlimited_operation_gas ctxt then
    Gas_limit_repr.Unaccounted
  else
    Gas_limit_repr.Limited
      {| Gas_limit_repr.t.Limited.remaining := remaining_operation_gas ctxt; |}.

Definition block_gas_level : t Gas_limit_repr.Arith.fp :=
  remaining_block_gas.

Definition check_gas_limit_is_valid
  (ctxt : t) (remaining : Gas_limit_repr.Arith.t) : M? unit :=
  if
    (Gas_limit_repr.Arith.op_gt remaining
      (constants ctxt).(Constants_repr.parametric.hard_gas_limit_per_operation))
    || (Gas_limit_repr.Arith.op_lt remaining Gas_limit_repr.Arith.zero)
  then
    Error_monad.error_value (Build_extensible "Gas_limit_too_high" unit tt)
  else
    Result.return_unit.

Definition consume_gas_limit_in_block
  (ctxt : t) (limit : Gas_limit_repr.Arith.t) : M? t :=
  let? '_ := check_gas_limit_is_valid ctxt limit in
  let block_gas := block_gas_level ctxt in
  let limit := Gas_limit_repr.Arith.fp_value limit in
  if Gas_limit_repr.Arith.op_gt limit block_gas then
    Error_monad.error_value (Build_extensible "Block_quota_exceeded" unit tt)
  else
    let level := Gas_limit_repr.Arith.sub (block_gas_level ctxt) limit in
    let ctxt := update_remaining_block_gas ctxt level in
    Pervasives.Ok ctxt.

Definition set_gas_limit (ctxt : t) (remaining : Gas_limit_repr.Arith.t) : t :=
  let remaining_operation_gas := Gas_limit_repr.Arith.fp_value remaining in
  let ctxt := update_unlimited_operation_gas ctxt false in
  t.with_remaining_operation_gas remaining_operation_gas ctxt.

Definition set_gas_unlimited (ctxt : t) : t :=
  update_unlimited_operation_gas ctxt true.

Definition consume_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M? t :=
  match Gas_limit_repr.raw_consume (remaining_operation_gas ctxt) cost with
  | Some gas_counter
    Pervasives.Ok (update_remaining_operation_gas ctxt gas_counter)
  | None
    if unlimited_operation_gas ctxt then
      return? ctxt
    else
      Error_monad.error_value
        (Build_extensible "Operation_quota_exceeded" unit tt)
  end.

Definition check_enough_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M? unit :=
  let? function_parameter := consume_gas ctxt cost in
  let '_ := function_parameter in
  Result.return_unit.

Definition gas_consumed (since : t) (until : t) : Gas_limit_repr.Arith.t :=
  match ((gas_level since), (gas_level until)) with
  |
    (Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := before |},
      Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := after |})
    ⇒ Gas_limit_repr.Arith.sub before after
  | (_, _)Gas_limit_repr.Arith.zero
  end.

Inductive missing_key_kind : Set :=
| Get : missing_key_kind
| _Set : missing_key_kind
| Del : missing_key_kind
| Copy : missing_key_kind.

Inductive storage_error : Set :=
| Incompatible_protocol_version : string storage_error
| Missing_key : list string missing_key_kind storage_error
| Existing_key : list string storage_error
| Corrupted_data : list string storage_error.

Definition storage_error_encoding : Data_encoding.encoding storage_error :=
  Data_encoding.union None
    [
      Data_encoding.case_value "Incompatible_protocol_version" None
        (Data_encoding.Tag 0)
        (Data_encoding.obj1
          (Data_encoding.req None None "incompatible_protocol_version"
            Data_encoding.string_value))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Incompatible_protocol_version argSome arg
          | _None
          end) (fun (arg : string) ⇒ Incompatible_protocol_version arg);
      Data_encoding.case_value "Missing_key" None (Data_encoding.Tag 1)
        (Data_encoding.obj2
          (Data_encoding.req None None "missing_key"
            (Data_encoding.list_value None Data_encoding.string_value))
          (Data_encoding.req None None "function"
            (Data_encoding.string_enum
              [
                ("get", Get);
                ("set", _Set);
                ("del", Del);
                ("copy", Copy)
              ])))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Missing_key key_value f_valueSome (key_value, f_value)
          | _None
          end)
        (fun (function_parameter : list string × missing_key_kind) ⇒
          let '(key_value, f_value) := function_parameter in
          Missing_key key_value f_value);
      Data_encoding.case_value "Existing_key" None (Data_encoding.Tag 2)
        (Data_encoding.obj1
          (Data_encoding.req None None "existing_key"
            (Data_encoding.list_value None Data_encoding.string_value)))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Existing_key key_valueSome key_value
          | _None
          end) (fun (key_value : list string) ⇒ Existing_key key_value);
      Data_encoding.case_value "Corrupted_data" None (Data_encoding.Tag 3)
        (Data_encoding.obj1
          (Data_encoding.req None None "corrupted_data"
            (Data_encoding.list_value None Data_encoding.string_value)))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Corrupted_data key_valueSome key_value
          | _None
          end) (fun (key_value : list string) ⇒ Corrupted_data key_value)
    ].

Definition pp_storage_error
  (ppf : Format.formatter) (function_parameter : storage_error) : unit :=
  match function_parameter with
  | Incompatible_protocol_version version
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Found a context with an unexpected version '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Found a context with an unexpected version '%s'.") version
  | Missing_key key_value Get
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Missing key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format))) "Missing key '%s'.")
      (String.concat "/" key_value)
  | Missing_key key_value _Set
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Cannot set undefined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot set undefined key '%s'.") (String.concat "/" key_value)
  | Missing_key key_value Del
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Cannot delete undefined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot delete undefined key '%s'.") (String.concat "/" key_value)
  | Missing_key key_value Copy
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Cannot copy undefined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot copy undefined key '%s'.") (String.concat "/" key_value)
  | Existing_key key_value
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Cannot initialize defined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot initialize defined key '%s'.") (String.concat "/" key_value)
  | Corrupted_data key_value
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Failed to parse the data at '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Failed to parse the data at '%s'.") (String.concat "/" key_value)
  end.

Init function; without side-effects in Coq
Definition init_module5 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent "context.storage_error"
    "Storage error (fatal internal error)"
    "An error that should never happen unless something has been deleted or corrupted in the database."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (err : storage_error) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Formatting_gen
                (CamlinternalFormatBasics.Open_box
                  (CamlinternalFormatBasics.Format
                    (CamlinternalFormatBasics.String_literal "<v 2>"
                      CamlinternalFormatBasics.End_of_format) "<v 2>"))
                (CamlinternalFormatBasics.String_literal "Storage error:"
                  (CamlinternalFormatBasics.Formatting_lit
                    (CamlinternalFormatBasics.Break "@ " 1 0)
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Formatting_lit
                        CamlinternalFormatBasics.Close_box
                        CamlinternalFormatBasics.End_of_format)))))
              "@[<v 2>Storage error:@ %a@]") pp_storage_error err))
    storage_error_encoding
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Storage_error" then
          let err := cast storage_error payload in
          Some err
        else None
      end)
    (fun (err : storage_error) ⇒
      Build_extensible "Storage_error" storage_error err).

Definition storage_error_value {A : Set} (err : storage_error) : M? A :=
  Error_monad.error_value (Build_extensible "Storage_error" storage_error err).

Definition version_key : list string := [ "version" ].

Definition version_value : string := "alpha_current".

Definition version : string := "v1".

Definition cycle_eras_key : list string := [ version; "cycle_eras" ].

Definition constants_key : list string := [ version; "constants" ].

Definition protocol_param_key : list string := [ "protocol_parameters" ].

Definition get_cycle_eras (ctxt : Context.t) : M? Level_repr.cycle_eras :=
  let function_parameter := Context.find ctxt cycle_eras_key in
  match function_parameter with
  | Nonestorage_error_value (Missing_key cycle_eras_key Get)
  | Some bytes_value
    match
      Data_encoding.Binary.of_bytes_opt Level_repr.cycle_eras_encoding
        bytes_value with
    | Nonestorage_error_value (Corrupted_data cycle_eras_key)
    | Some cycle_erasreturn? cycle_eras
    end
  end.

Definition set_cycle_eras {A : Set}
  (ctxt : Context.t) (cycle_eras : Level_repr.cycle_eras)
  : Pervasives.result Context.t A :=
  let bytes_value :=
    Data_encoding.Binary.to_bytes_exn None Level_repr.cycle_eras_encoding
      cycle_eras in
  Error_monad.op_gtpipeeq (Context.add ctxt cycle_eras_key bytes_value)
    Error_monad.ok.

Init function; without side-effects in Coq
Definition init_module6 : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "context.failed_to_parse_parameter" "Failed to parse parameter"
      "The protocol parameters are not valid JSON."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (bytes_value : Bytes.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.Formatting_gen
                  (CamlinternalFormatBasics.Open_box
                    (CamlinternalFormatBasics.Format
                      (CamlinternalFormatBasics.String_literal "<v 2>"
                        CamlinternalFormatBasics.End_of_format) "<v 2>"))
                  (CamlinternalFormatBasics.String_literal
                    "Cannot parse the protocol parameter:"
                    (CamlinternalFormatBasics.Formatting_lit
                      (CamlinternalFormatBasics.Break "@ " 1 0)
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.Formatting_lit
                          CamlinternalFormatBasics.Close_box
                          CamlinternalFormatBasics.End_of_format)))))
                "@[<v 2>Cannot parse the protocol parameter:@ %s@]")
              (Bytes.to_string bytes_value)))
      (Data_encoding.obj1
        (Data_encoding.req None None "contents" Data_encoding.bytes_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Failed_to_parse_parameter" then
            let data := cast bytes payload in
            Some data
          else None
        end)
      (fun (data : Bytes.t) ⇒
        Build_extensible "Failed_to_parse_parameter" Bytes.t data) in
  Error_monad.register_error_kind Error_monad.Temporary
    "context.failed_to_decode_parameter" "Failed to decode parameter"
    "Unexpected JSON object."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : Data_encoding.json × string) ⇒
          let '(json_value, msg) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Formatting_gen
                (CamlinternalFormatBasics.Open_box
                  (CamlinternalFormatBasics.Format
                    (CamlinternalFormatBasics.String_literal "<v 2>"
                      CamlinternalFormatBasics.End_of_format) "<v 2>"))
                (CamlinternalFormatBasics.String_literal
                  "Cannot decode the protocol parameter:"
                  (CamlinternalFormatBasics.Formatting_lit
                    (CamlinternalFormatBasics.Break "@ " 1 0)
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      (CamlinternalFormatBasics.Formatting_lit
                        (CamlinternalFormatBasics.Break "@ " 1 0)
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.Formatting_lit
                            CamlinternalFormatBasics.Close_box
                            CamlinternalFormatBasics.End_of_format)))))))
              "@[<v 2>Cannot decode the protocol parameter:@ %s@ %a@]") msg
            Data_encoding.Json.pp json_value))
    (Data_encoding.obj2
      (Data_encoding.req None None "contents" Data_encoding.json_value)
      (Data_encoding.req None None "error" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Failed_to_decode_parameter" then
          let '(json_value, msg) :=
            cast (Data_encoding.json × string) payload in
          Some (json_value, msg)
        else None
      end)
    (fun (function_parameter : Data_encoding.json × string) ⇒
      let '(json_value, msg) := function_parameter in
      Build_extensible "Failed_to_decode_parameter"
        (Data_encoding.json × string) (json_value, msg)).

Definition get_proto_param (ctxt : Context.t)
  : M? (Parameters_repr.t × Context.t) :=
  let function_parameter := Context.find ctxt protocol_param_key in
  match function_parameter with
  | NonePervasives.failwith "Missing protocol parameters."
  | Some bytes_value
    match Data_encoding.Binary.of_bytes_opt Data_encoding.json_value bytes_value
      with
    | None
      Error_monad.fail
        (Build_extensible "Failed_to_parse_parameter" Context.value bytes_value)
    | Some json_value
      let ctxt := Context.remove ctxt protocol_param_key in
      let 'param :=
        Data_encoding.Json.destruct None Parameters_repr.encoding json_value in
      let? '_ := Parameters_repr.check_params param in
      return? (param, ctxt)
    end
  end.

Definition add_constants
  (ctxt : Context.t) (constants : Constants_repr.parametric) : Context.t :=
  let bytes_value :=
    Data_encoding.Binary.to_bytes_exn None Constants_repr.parametric_encoding
      constants in
  Context.add ctxt constants_key bytes_value.

Definition get_constants {A : Set} (ctxt : Context.t)
  : Pervasives.result Constants_repr.parametric A :=
  let function_parameter := Context.find ctxt constants_key in
  match function_parameter with
  | None
    Pervasives.failwith "Internal error: cannot read constants in context."
  | Some bytes_value
    match
      Data_encoding.Binary.of_bytes_opt Constants_repr.parametric_encoding
        bytes_value with
    | None
      Pervasives.failwith "Internal error: cannot parse constants in context."
    | Some constantsreturn? constants
    end
  end.

Definition patch_constants
  (ctxt : t) (f_value : Constants_repr.parametric Constants_repr.parametric)
  : t :=
  let constants := f_value (constants ctxt) in
  let context_value := add_constants (context_value ctxt) constants in
  let ctxt := update_context ctxt context_value in
  update_constants ctxt constants.

Definition check_inited (ctxt : Context.t) : M? unit :=
  let function_parameter := Context.find ctxt version_key in
  match function_parameter with
  | NonePervasives.failwith "Internal error: un-initialized context."
  | Some bytes_value
    let s_value := Bytes.to_string bytes_value in
    if Compare.String.(Compare.S.op_eq) s_value version_value then
      Result.return_unit
    else
      storage_error_value (Incompatible_protocol_version s_value)
  end.

Definition check_cycle_eras
  (cycle_eras : Level_repr.cycle_eras) (constants : Constants_repr.parametric)
  : unit :=
  let current_era := Level_repr.current_era cycle_eras in
  let '_ :=
    (* ❌ Assert instruction is not handled. *)
    assert unit
      (current_era.(Level_repr.cycle_era.blocks_per_cycle) =i32
      constants.(Constants_repr.parametric.blocks_per_cycle)) in
  (* ❌ Assert instruction is not handled. *)
  assert unit
    (current_era.(Level_repr.cycle_era.blocks_per_commitment) =i32
    constants.(Constants_repr.parametric.blocks_per_commitment)).

Definition prepare
  (level : int32) (predecessor_timestamp : Time.t) (timestamp : Time.t)
  (ctxt : Context.t) : M? t :=
  let? level := Raw_level_repr.of_int32 level in
  let? '_ := check_inited ctxt in
  let? constants := get_constants ctxt in
  let? round_durations :=
    Round_repr.Durations.create
      constants.(Constants_repr.parametric.minimal_block_delay)
      constants.(Constants_repr.parametric.delay_increment_per_round) in
  let? cycle_eras := get_cycle_eras ctxt in
  let '_ := check_cycle_eras cycle_eras constants in
  let level := Level_repr.level_from_raw cycle_eras level in
  return?
    {| t.remaining_operation_gas := Gas_limit_repr.Arith.zero;
      t.back :=
        {| back.context := ctxt; back.constants := constants;
          back.round_durations := round_durations;
          back.cycle_eras := cycle_eras; back.level := level;
          back.predecessor_timestamp := predecessor_timestamp;
          back.timestamp := timestamp; back.fees := Tez_repr.zero;
          back.origination_nonce := None;
          back.temporary_lazy_storage_ids :=
            Lazy_storage_kind.Temp_ids.init_value; back.internal_nonce := 0;
          back.internal_nonces_used := Int_set.(_Set.S.empty);
          back.remaining_block_gas :=
            Gas_limit_repr.Arith.fp_value
              constants.(Constants_repr.parametric.hard_gas_limit_per_block);
          back.unlimited_operation_gas := true;
          back.consensus := Raw_consensus.empty;
          back.non_consensus_operations_rev := nil;
          back.sampler_state := Cycle_repr.Map.(Map.S.empty);
          back.stake_distribution_for_current_cycle := None;
          back.tx_rollup_current_messages := Tx_rollup_repr.Map.(Map.S.empty);
          back.sc_rollup_current_messages :=
            Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.empty); |}; |}.

Inductive previous_protocol : Set :=
| Genesis : Parameters_repr.t previous_protocol
| Ithaca_012 : previous_protocol.

Definition check_and_update_protocol_version (ctxt : Context.t)
  : M? (previous_protocol × Context.t) :=
  let? '(previous_proto, ctxt) :=
    let function_parameter := Context.find ctxt version_key in
    match function_parameter with
    | None
      Pervasives.failwith
        "Internal error: un-initialized context in check_first_block."
    | Some bytes_value
      let s_value := Bytes.to_string bytes_value in
      if Compare.String.(Compare.S.op_eq) s_value version_value then
        Pervasives.failwith "Internal error: previously initialized context."
      else
        if Compare.String.(Compare.S.op_eq) s_value "genesis" then
          let? '(param, ctxt) := get_proto_param ctxt in
          return? ((Genesis param), ctxt)
        else
          if Compare.String.(Compare.S.op_eq) s_value "ithaca_012" then
            return? (Ithaca_012, ctxt)
          else
            storage_error_value (Incompatible_protocol_version s_value)
    end in
  let ctxt := Context.add ctxt version_key (Bytes.of_string version_value) in
  return? (previous_proto, ctxt).

Definition get_previous_protocol_constants (ctxt : Context.t)
  : Constants_repr.Proto_previous.parametric :=
  let function_parameter := Context.find ctxt constants_key in
  match function_parameter with
  | None
    Pervasives.failwith
      "Internal error: cannot read previous protocol constants in context."
  | Some bytes_value
    match
      Data_encoding.Binary.of_bytes_opt
        Constants_repr.Proto_previous.parametric_encoding bytes_value with
    | None
      Pervasives.failwith
        "Internal error: cannot parse previous protocol constants in context."
    | Some constantsconstants
    end
  end.

Definition prepare_first_block
  (level : int32) (timestamp : Time.t) (ctxt : Context.t)
  : M? (previous_protocol × t) :=
  let? '(previous_proto, ctxt) := check_and_update_protocol_version ctxt in
  let? ctxt :=
    match previous_proto with
    | Genesis param
      let? first_level := Raw_level_repr.of_int32 level in
      let cycle_era :=
        {| Level_repr.cycle_era.first_level := first_level;
          Level_repr.cycle_era.first_cycle := Cycle_repr.root_value;
          Level_repr.cycle_era.blocks_per_cycle :=
            param.(Parameters_repr.t.constants).(Constants_repr.parametric.blocks_per_cycle);
          Level_repr.cycle_era.blocks_per_commitment :=
            param.(Parameters_repr.t.constants).(Constants_repr.parametric.blocks_per_commitment);
          |} in
      let? cycle_eras := Level_repr.create_cycle_eras [ cycle_era ] in
      let? ctxt := set_cycle_eras ctxt cycle_eras in
      Error_monad.op_gtpipeeq
        (add_constants ctxt param.(Parameters_repr.t.constants)) Error_monad.ok
    | Ithaca_012
      let c_value := get_previous_protocol_constants ctxt in
      let cycles_per_voting_period :=
        c_value.(Constants_repr.Proto_previous.parametric.blocks_per_voting_period)
        /i32 c_value.(Constants_repr.Proto_previous.parametric.blocks_per_cycle)
        in
      let tx_rollup_finality_period := 60000 in
      let constants :=
        {|
          Constants_repr.parametric.preserved_cycles :=
            c_value.(Constants_repr.Proto_previous.parametric.preserved_cycles);
          Constants_repr.parametric.blocks_per_cycle :=
            c_value.(Constants_repr.Proto_previous.parametric.blocks_per_cycle);
          Constants_repr.parametric.blocks_per_commitment :=
            c_value.(Constants_repr.Proto_previous.parametric.blocks_per_commitment);
          Constants_repr.parametric.blocks_per_stake_snapshot :=
            c_value.(Constants_repr.Proto_previous.parametric.blocks_per_stake_snapshot);
          Constants_repr.parametric.cycles_per_voting_period :=
            cycles_per_voting_period;
          Constants_repr.parametric.hard_gas_limit_per_operation :=
            c_value.(Constants_repr.Proto_previous.parametric.hard_gas_limit_per_operation);
          Constants_repr.parametric.hard_gas_limit_per_block :=
            c_value.(Constants_repr.Proto_previous.parametric.hard_gas_limit_per_block);
          Constants_repr.parametric.proof_of_work_threshold :=
            c_value.(Constants_repr.Proto_previous.parametric.proof_of_work_threshold);
          Constants_repr.parametric.tokens_per_roll :=
            c_value.(Constants_repr.Proto_previous.parametric.tokens_per_roll);
          Constants_repr.parametric.seed_nonce_revelation_tip :=
            c_value.(Constants_repr.Proto_previous.parametric.seed_nonce_revelation_tip);
          Constants_repr.parametric.origination_size :=
            c_value.(Constants_repr.Proto_previous.parametric.origination_size);
          Constants_repr.parametric.baking_reward_fixed_portion :=
            c_value.(Constants_repr.Proto_previous.parametric.baking_reward_fixed_portion);
          Constants_repr.parametric.baking_reward_bonus_per_slot :=
            c_value.(Constants_repr.Proto_previous.parametric.baking_reward_bonus_per_slot);
          Constants_repr.parametric.endorsing_reward_per_slot :=
            c_value.(Constants_repr.Proto_previous.parametric.endorsing_reward_per_slot);
          Constants_repr.parametric.cost_per_byte :=
            c_value.(Constants_repr.Proto_previous.parametric.cost_per_byte);
          Constants_repr.parametric.hard_storage_limit_per_operation :=
            c_value.(Constants_repr.Proto_previous.parametric.hard_storage_limit_per_operation);
          Constants_repr.parametric.quorum_min :=
            c_value.(Constants_repr.Proto_previous.parametric.quorum_min);
          Constants_repr.parametric.quorum_max :=
            c_value.(Constants_repr.Proto_previous.parametric.quorum_max);
          Constants_repr.parametric.min_proposal_quorum :=
            c_value.(Constants_repr.Proto_previous.parametric.min_proposal_quorum);
          Constants_repr.parametric.liquidity_baking_subsidy :=
            c_value.(Constants_repr.Proto_previous.parametric.liquidity_baking_subsidy);
          Constants_repr.parametric.liquidity_baking_sunset_level :=
            c_value.(Constants_repr.Proto_previous.parametric.liquidity_baking_sunset_level);
          Constants_repr.parametric.liquidity_baking_toggle_ema_threshold :=
            1000000000;
          Constants_repr.parametric.max_operations_time_to_live :=
            c_value.(Constants_repr.Proto_previous.parametric.max_operations_time_to_live);
          Constants_repr.parametric.minimal_block_delay :=
            c_value.(Constants_repr.Proto_previous.parametric.minimal_block_delay);
          Constants_repr.parametric.delay_increment_per_round :=
            c_value.(Constants_repr.Proto_previous.parametric.delay_increment_per_round);
          Constants_repr.parametric.minimal_participation_ratio :=
            c_value.(Constants_repr.Proto_previous.parametric.minimal_participation_ratio);
          Constants_repr.parametric.consensus_committee_size :=
            c_value.(Constants_repr.Proto_previous.parametric.consensus_committee_size);
          Constants_repr.parametric.consensus_threshold :=
            c_value.(Constants_repr.Proto_previous.parametric.consensus_threshold);
          Constants_repr.parametric.max_slashing_period :=
            c_value.(Constants_repr.Proto_previous.parametric.max_slashing_period);
          Constants_repr.parametric.frozen_deposits_percentage :=
            c_value.(Constants_repr.Proto_previous.parametric.frozen_deposits_percentage);
          Constants_repr.parametric.double_baking_punishment :=
            c_value.(Constants_repr.Proto_previous.parametric.double_baking_punishment);
          Constants_repr.parametric.ratio_of_frozen_deposits_slashed_per_double_endorsement
            :=
            c_value.(Constants_repr.Proto_previous.parametric.ratio_of_frozen_deposits_slashed_per_double_endorsement);
          Constants_repr.parametric.initial_seed := None;
          Constants_repr.parametric.cache_script_size := 100000000;
          Constants_repr.parametric.cache_stake_distribution_cycles := 8;
          Constants_repr.parametric.cache_sampler_state_cycles := 8;
          Constants_repr.parametric.tx_rollup_enable := true;
          Constants_repr.parametric.tx_rollup_origination_size := 60000;
          Constants_repr.parametric.tx_rollup_hard_size_limit_per_inbox :=
            100000;
          Constants_repr.parametric.tx_rollup_hard_size_limit_per_message :=
            5000;
          Constants_repr.parametric.tx_rollup_commitment_bond :=
            Tez_repr.of_mutez_exn 10000000000;
          Constants_repr.parametric.tx_rollup_finality_period :=
            tx_rollup_finality_period;
          Constants_repr.parametric.tx_rollup_withdraw_period :=
            tx_rollup_finality_period;
          Constants_repr.parametric.tx_rollup_max_inboxes_count :=
            tx_rollup_finality_period +i 100;
          Constants_repr.parametric.tx_rollup_max_messages_per_inbox := 1010;
          Constants_repr.parametric.tx_rollup_max_commitments_count :=
            (2 ×i tx_rollup_finality_period) +i 100;
          Constants_repr.parametric.tx_rollup_cost_per_byte_ema_factor := 120;
          Constants_repr.parametric.tx_rollup_max_ticket_payload_size := 2048;
          Constants_repr.parametric.tx_rollup_max_withdrawals_per_batch := 15;
          Constants_repr.parametric.tx_rollup_rejection_max_proof_size := 30000;
          Constants_repr.parametric.tx_rollup_sunset_level := 3473409;
          Constants_repr.parametric.sc_rollup_enable := false;
          Constants_repr.parametric.sc_rollup_origination_size := 6314;
          Constants_repr.parametric.sc_rollup_challenge_window_in_blocks :=
            20160;
          Constants_repr.parametric.sc_rollup_max_available_messages := 1000000;
          |} in
      let ctxt := add_constants ctxt constants in
      return? ctxt
    end in
  let? ctxt := prepare level timestamp timestamp ctxt in
  return? (previous_proto, ctxt).

Definition activate (ctxt : t) (h_value : Protocol_hash.t) : t :=
  Error_monad.op_gtpipeeq (Updater.activate (context_value ctxt) h_value)
    (update_context ctxt).

Definition key : Set := list string.

Definition value : Set := bytes.

Definition tree : Set := Context.tree.

Definition T {t : Set} : Set :=
  Raw_context_intf.T (root := root) (t := t) (tree := tree).

Definition mem (ctxt : t) (k_value : Context.key) : bool :=
  Context.mem (context_value ctxt) k_value.

Definition mem_tree (ctxt : t) (k_value : Context.key) : bool :=
  Context.mem_tree (context_value ctxt) k_value.

Definition get (ctxt : t) (k_value : Context.key) : M? Context.value :=
  let function_parameter := Context.find (context_value ctxt) k_value in
  match function_parameter with
  | Nonestorage_error_value (Missing_key k_value Get)
  | Some v_valuereturn? v_value
  end.

Definition get_tree (ctxt : t) (k_value : Context.key) : M? Context.tree :=
  let function_parameter := Context.find_tree (context_value ctxt) k_value in
  match function_parameter with
  | Nonestorage_error_value (Missing_key k_value Get)
  | Some v_valuereturn? v_value
  end.

Definition find (ctxt : t) (k_value : Context.key) : option Context.value :=
  Context.find (context_value ctxt) k_value.

Definition find_tree (ctxt : t) (k_value : Context.key) : option Context.tree :=
  Context.find_tree (context_value ctxt) k_value.

Definition add (ctxt : t) (k_value : Context.key) (v_value : Context.value)
  : t :=
  Error_monad.op_gtpipeeq (Context.add (context_value ctxt) k_value v_value)
    (update_context ctxt).

Definition add_tree (ctxt : t) (k_value : Context.key) (v_value : Context.tree)
  : t :=
  Error_monad.op_gtpipeeq
    (Context.add_tree (context_value ctxt) k_value v_value)
    (update_context ctxt).

Definition init_value
  (ctxt : t) (k_value : Context.key) (v_value : Context.value) : M? t :=
  let function_parameter := Context.mem (context_value ctxt) k_value in
  match function_parameter with
  | truestorage_error_value (Existing_key k_value)
  | _
    let context_value := Context.add (context_value ctxt) k_value v_value in
    return? (update_context ctxt context_value)
  end.

Definition init_tree (ctxt : t) (k_value : Context.key) (v_value : Context.tree)
  : M? t :=
  let function_parameter := Context.mem_tree (context_value ctxt) k_value in
  match function_parameter with
  | truestorage_error_value (Existing_key k_value)
  | _
    let context_value := Context.add_tree (context_value ctxt) k_value v_value
      in
    return? (update_context ctxt context_value)
  end.

Definition update (ctxt : t) (k_value : Context.key) (v_value : Context.value)
  : M? t :=
  let function_parameter := Context.mem (context_value ctxt) k_value in
  match function_parameter with
  | falsestorage_error_value (Missing_key k_value _Set)
  | _
    let context_value := Context.add (context_value ctxt) k_value v_value in
    return? (update_context ctxt context_value)
  end.

Definition update_tree
  (ctxt : t) (k_value : Context.key) (v_value : Context.tree) : M? t :=
  let function_parameter := Context.mem_tree (context_value ctxt) k_value in
  match function_parameter with
  | falsestorage_error_value (Missing_key k_value _Set)
  | _
    let context_value := Context.add_tree (context_value ctxt) k_value v_value
      in
    return? (update_context ctxt context_value)
  end.

Definition remove_existing (ctxt : t) (k_value : Context.key) : M? t :=
  let function_parameter := Context.mem (context_value ctxt) k_value in
  match function_parameter with
  | falsestorage_error_value (Missing_key k_value Del)
  | _
    let context_value := Context.remove (context_value ctxt) k_value in
    return? (update_context ctxt context_value)
  end.

Definition remove_existing_tree (ctxt : t) (k_value : Context.key) : M? t :=
  let function_parameter := Context.mem_tree (context_value ctxt) k_value in
  match function_parameter with
  | falsestorage_error_value (Missing_key k_value Del)
  | _
    let context_value := Context.remove (context_value ctxt) k_value in
    return? (update_context ctxt context_value)
  end.

Definition remove (ctxt : t) (k_value : Context.key) : t :=
  Error_monad.op_gtpipeeq (Context.remove (context_value ctxt) k_value)
    (update_context ctxt).

Definition add_or_remove
  (ctxt : t) (k_value : Context.key) (function_parameter : option Context.value)
  : t :=
  match function_parameter with
  | Noneremove ctxt k_value
  | Some v_valueadd ctxt k_value v_value
  end.

Definition add_or_remove_tree
  (ctxt : t) (k_value : Context.key) (function_parameter : option Context.tree)
  : t :=
  match function_parameter with
  | Noneremove ctxt k_value
  | Some v_valueadd_tree ctxt k_value v_value
  end.

Definition list_value
  (ctxt : t) (offset : option int) (length : option int) (k_value : Context.key)
  : list (string × Context.tree) :=
  Context.list_value (context_value ctxt) offset length k_value.

Definition fold {A : Set}
  (depth : option Context.depth) (ctxt : t) (k_value : Context.key)
  (order : Variant.t) (init_value : A)
  (f_value : Context.key Context.tree A A) : A :=
  Context.fold depth (context_value ctxt) k_value order init_value f_value.

Definition config_value (ctxt : t) : Context.config :=
  Context.config_value (context_value ctxt).

Module Tree.
Inclusion of the module [Context.Tree]
  Definition mem := Context.Tree.(Context.TREE.mem).

  Definition mem_tree := Context.Tree.(Context.TREE.mem_tree).

  Definition find := Context.Tree.(Context.TREE.find).

  Definition find_tree := Context.Tree.(Context.TREE.find_tree).

  Definition list_value := Context.Tree.(Context.TREE.list_value).

  Definition length := Context.Tree.(Context.TREE.length).

  Definition add := Context.Tree.(Context.TREE.add).

  Definition add_tree := Context.Tree.(Context.TREE.add_tree).

  Definition remove := Context.Tree.(Context.TREE.remove).

  Definition fold {a : Set} := Context.Tree.(Context.TREE.fold) (a := a).

  Definition config_value := Context.Tree.(Context.TREE.config_value).

  (* Definition empty := Context.Tree.(Context.TREE.empty). *)

  Definition is_empty := Context.Tree.(Context.TREE.is_empty).

  Definition kind_value := Context.Tree.(Context.TREE.kind_value).

  Definition to_value := Context.Tree.(Context.TREE.to_value).

  Definition of_value := Context.Tree.(Context.TREE.of_value).

  Definition hash_value := Context.Tree.(Context.TREE.hash_value).

  Definition equal := Context.Tree.(Context.TREE.equal).

  Definition clear := Context.Tree.(Context.TREE.clear).

  Definition empty (ctxt : t) : Context.tree :=
    Context.Tree.(Context.TREE.empty) (context_value ctxt).

  Definition get (t_value : Context.tree) (k_value : Context.key)
    : M? Context.value :=
    let function_parameter := find t_value k_value in
    match function_parameter with
    | Nonestorage_error_value (Missing_key k_value Get)
    | Some v_valuereturn? v_value
    end.

  Definition get_tree (t_value : Context.tree) (k_value : Context.key)
    : M? Context.tree :=
    let function_parameter := find_tree t_value k_value in
    match function_parameter with
    | Nonestorage_error_value (Missing_key k_value Get)
    | Some v_valuereturn? v_value
    end.

  Definition init_value
    (t_value : Context.tree) (k_value : Context.key) (v_value : Context.value)
    : M? Context.tree :=
    let function_parameter := mem t_value k_value in
    match function_parameter with
    | truestorage_error_value (Existing_key k_value)
    | _Error_monad.op_gtpipeeq (add t_value k_value v_value) Error_monad.ok
    end.

  Definition init_tree
    (t_value : Context.tree) (k_value : Context.key) (v_value : Context.tree)
    : M? Context.tree :=
    let function_parameter := mem_tree t_value k_value in
    match function_parameter with
    | truestorage_error_value (Existing_key k_value)
    | _
      Error_monad.op_gtpipeeq (add_tree t_value k_value v_value) Error_monad.ok
    end.

  Definition update
    (t_value : Context.tree) (k_value : Context.key) (v_value : Context.value)
    : M? Context.tree :=
    let function_parameter := mem t_value k_value in
    match function_parameter with
    | falsestorage_error_value (Missing_key k_value _Set)
    | _Error_monad.op_gtpipeeq (add t_value k_value v_value) Error_monad.ok
    end.

  Definition update_tree
    (t_value : Context.tree) (k_value : Context.key) (v_value : Context.tree)
    : M? Context.tree :=
    let function_parameter := mem_tree t_value k_value in
    match function_parameter with
    | falsestorage_error_value (Missing_key k_value _Set)
    | _
      Error_monad.op_gtpipeeq (add_tree t_value k_value v_value) Error_monad.ok
    end.

  Definition remove_existing (t_value : Context.tree) (k_value : Context.key)
    : M? Context.tree :=
    let function_parameter := mem t_value k_value in
    match function_parameter with
    | falsestorage_error_value (Missing_key k_value Del)
    | _Error_monad.op_gtpipeeq (remove t_value k_value) Error_monad.ok
    end.

  Definition remove_existing_tree
    (t_value : Context.tree) (k_value : Context.key) : M? Context.tree :=
    let function_parameter := mem_tree t_value k_value in
    match function_parameter with
    | falsestorage_error_value (Missing_key k_value Del)
    | _Error_monad.op_gtpipeeq (remove t_value k_value) Error_monad.ok
    end.

  Definition add_or_remove
    (t_value : Context.tree) (k_value : Context.key)
    (function_parameter : option Context.value) : Context.tree :=
    match function_parameter with
    | Noneremove t_value k_value
    | Some v_valueadd t_value k_value v_value
    end.

  Definition add_or_remove_tree
    (t_value : Context.tree) (k_value : Context.key)
    (function_parameter : option Context.tree) : Context.tree :=
    match function_parameter with
    | Noneremove t_value k_value
    | Some v_valueadd_tree t_value k_value v_value
    end.

  (* Tree *)
  Definition module :=
    {|
      Raw_context_intf.TREE.mem := mem;
      Raw_context_intf.TREE.mem_tree := mem_tree;
      Raw_context_intf.TREE.get := get;
      Raw_context_intf.TREE.get_tree := get_tree;
      Raw_context_intf.TREE.find := find;
      Raw_context_intf.TREE.find_tree := find_tree;
      Raw_context_intf.TREE.list_value := list_value;
      Raw_context_intf.TREE.init_value := init_value;
      Raw_context_intf.TREE.init_tree := init_tree;
      Raw_context_intf.TREE.update := update;
      Raw_context_intf.TREE.update_tree := update_tree;
      Raw_context_intf.TREE.add := add;
      Raw_context_intf.TREE.add_tree := add_tree;
      Raw_context_intf.TREE.remove := remove;
      Raw_context_intf.TREE.remove_existing := remove_existing;
      Raw_context_intf.TREE.remove_existing_tree := remove_existing_tree;
      Raw_context_intf.TREE.add_or_remove := add_or_remove;
      Raw_context_intf.TREE.add_or_remove_tree := add_or_remove_tree;
      Raw_context_intf.TREE.fold _ := fold;
      Raw_context_intf.TREE.config_value := config_value;
      Raw_context_intf.TREE.empty := empty;
      Raw_context_intf.TREE.is_empty := is_empty;
      Raw_context_intf.TREE.kind_value := kind_value;
      Raw_context_intf.TREE.to_value := to_value;
      Raw_context_intf.TREE.hash_value := hash_value;
      Raw_context_intf.TREE.equal := equal;
      Raw_context_intf.TREE.clear := clear
    |}.
End Tree.
Definition Tree : Raw_context_intf.TREE (t := t) (tree := tree) := Tree.module.

Definition verify_tree_proof {A : Set}
  (proof : Context.Proof.t Context.Proof.tree)
  (f_value : Context.tree Context.tree × A)
  : Pervasives.result (Context.tree × A) Variant.t :=
  Context.verify_tree_proof proof f_value.

Definition verify_stream_proof {A : Set}
  (proof : Context.Proof.t Context.Proof.stream)
  (f_value : Context.tree Context.tree × A)
  : Pervasives.result (Context.tree × A) Variant.t :=
  Context.verify_stream_proof proof f_value.

Definition equal_config : Context.config Context.config bool :=
  Context.equal_config.

Definition project {A : Set} (x_value : A) : A := x_value.

Definition absolute_key {A B : Set} (function_parameter : A) : B B :=
  let '_ := function_parameter in
  fun (k_value : B) ⇒ k_value.

Definition description : Storage_description.t root :=
  Storage_description.create tt.

Definition fold_map_temporary_lazy_storage_ids {A : Set}
  (ctxt : t)
  (f_value : Lazy_storage_kind.Temp_ids.t Lazy_storage_kind.Temp_ids.t × A)
  : t × A :=
  (fun (function_parameter : Lazy_storage_kind.Temp_ids.t × A) ⇒
    let '(temporary_lazy_storage_ids, x_value) := function_parameter in
    ((update_temporary_lazy_storage_ids ctxt temporary_lazy_storage_ids),
      x_value)) (f_value (temporary_lazy_storage_ids ctxt)).

Definition map_temporary_lazy_storage_ids_s
  (ctxt : t)
  (f_value : Lazy_storage_kind.Temp_ids.t t × Lazy_storage_kind.Temp_ids.t)
  : t :=
  let '(ctxt, temporary_lazy_storage_ids) :=
    f_value (temporary_lazy_storage_ids ctxt) in
  update_temporary_lazy_storage_ids ctxt temporary_lazy_storage_ids.

Module Cache.
  Definition key : Set := Context.cache_key.

  Definition value : Set := Context.cache_value.

  Definition key_of_identifier : int string Context.cache_key :=
    Context.Cache.(Context.CACHE.key_of_identifier).

  Definition identifier_of_key : Context.cache_key string :=
    Context.Cache.(Context.CACHE.identifier_of_key).

  Definition pp (fmt : Format.formatter) (ctxt : t) : unit :=
    Context.Cache.(Context.CACHE.pp) fmt (context_value ctxt).

  Definition find (c_value : t) (k_value : Context.cache_key)
    : option Context.cache_value :=
    Context.Cache.(Context.CACHE.find) (context_value c_value) k_value.

  Definition set_cache_layout (c_value : t) (layout : list int) : t :=
    let ctxt :=
      Context.Cache.(Context.CACHE.set_cache_layout) (context_value c_value)
        layout in
    update_context c_value ctxt.

  Definition update
    (c_value : t) (k_value : Context.cache_key)
    (v_value : option (Context.cache_value × int)) : t :=
    update_context c_value
      (Context.Cache.(Context.CACHE.update) (context_value c_value) k_value
        v_value).

  Definition sync (c_value : t) (cache_nonce : Bytes.t) : t :=
    let ctxt :=
      Context.Cache.(Context.CACHE.sync) (context_value c_value) cache_nonce in
    update_context c_value ctxt.

  Definition clear (c_value : t) : t :=
    update_context c_value
      (Context.Cache.(Context.CACHE.clear) (context_value c_value)).

  Definition list_keys (c_value : t) (cache_index : int)
    : option (list (Context.cache_key × int)) :=
    Context.Cache.(Context.CACHE.list_keys) (context_value c_value) cache_index.

  Definition key_rank (c_value : t) (key_value : Context.cache_key)
    : option int :=
    Context.Cache.(Context.CACHE.key_rank) (context_value c_value) key_value.

  Definition cache_size_limit (c_value : t) (cache_index : int) : option int :=
    Context.Cache.(Context.CACHE.cache_size_limit) (context_value c_value)
      cache_index.

  Definition cache_size (c_value : t) (cache_index : int) : option int :=
    Context.Cache.(Context.CACHE.cache_size) (context_value c_value) cache_index.

  Definition future_cache_expectation (c_value : t) (time_in_blocks : int)
    : t :=
    update_context c_value
      (Context.Cache.(Context.CACHE.future_cache_expectation)
        (context_value c_value) time_in_blocks).

  (* Cache *)
  Definition module :=
    {|
      Context.CACHE.key_of_identifier := key_of_identifier;
      Context.CACHE.identifier_of_key := identifier_of_key;
      Context.CACHE.pp := pp;
      Context.CACHE.find := find;
      Context.CACHE.set_cache_layout := set_cache_layout;
      Context.CACHE.update := update;
      Context.CACHE.sync := sync;
      Context.CACHE.clear := clear;
      Context.CACHE.list_keys := list_keys;
      Context.CACHE.key_rank := key_rank;
      Context.CACHE.cache_size_limit := cache_size_limit;
      Context.CACHE.cache_size := cache_size;
      Context.CACHE.future_cache_expectation := future_cache_expectation
    |}.
End Cache.
Definition Cache := Cache.module.

Definition record_non_consensus_operation_hash
  (ctxt : t) (operation_hash : Operation_hash.t) : t :=
  update_non_consensus_operations_rev ctxt
    (cons operation_hash (non_consensus_operations_rev ctxt)).

Definition non_consensus_operations (ctxt : t) : list Operation_hash.t :=
  List.rev (non_consensus_operations_rev ctxt).

Definition init_sampler_for_cycle
  (ctxt : t) (cycle : Cycle_repr.t) (seed_value : Seed_repr.seed)
  (state_value : Sampler.t (Signature.public_key × Signature.public_key_hash))
  : M? t :=
  let map := sampler_state ctxt in
  if Cycle_repr.Map.(Map.S.mem) cycle map then
    Error_monad.error_value
      (Build_extensible "Sampler_already_set" Cycle_repr.t cycle)
  else
    let map := Cycle_repr.Map.(Map.S.add) cycle (seed_value, state_value) map in
    let ctxt := update_sampler_state ctxt map in
    return? ctxt.

Definition sampler_for_cycle {A : Set}
  (read :
    t
    Pervasives.result
      (Seed_repr.seed ×
        Sampler.t (Signature.public_key × Signature.public_key_hash)) A)
  (ctxt : t) (cycle : Cycle_repr.t)
  : Pervasives.result
    (t × Seed_repr.seed ×
      Sampler.t (Signature.public_key × Signature.public_key_hash)) A :=
  let map := sampler_state ctxt in
  match Cycle_repr.Map.(Map.S.find) cycle map with
  | Some (seed_value, state_value)return? (ctxt, seed_value, state_value)
  | None
    let? '(seed_value, state_value) := read ctxt in
    let map := Cycle_repr.Map.(Map.S.add) cycle (seed_value, state_value) map in
    let ctxt := update_sampler_state ctxt map in
    return? (ctxt, seed_value, state_value)
  end.

Definition stake_distribution_for_current_cycle (ctxt : t)
  : M?
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
      Tez_repr.t) :=
  match ctxt.(t.back).(back.stake_distribution_for_current_cycle) with
  | None
    Error_monad.error_value
      (Build_extensible "Stake_distribution_not_set" unit tt)
  | Some s_valuereturn? s_value
  end.

Definition init_stake_distribution_for_current_cycle
  (ctxt : t)
  (stake_distribution_for_current_cycle :
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
      Tez_repr.t) : t :=
  update_back ctxt
    (back.with_stake_distribution_for_current_cycle
      (Some stake_distribution_for_current_cycle) ctxt.(t.back)).

Module CONSENSUS.
  Record signature {t : Set} {slot_map : Set Set} {slot_set slot round : Set}
    : Set := {
    t := t;
    slot_map := slot_map;
    slot_set := slot_set;
    slot := slot;
    round := round;
    allowed_endorsements :
      t slot_map (Signature.public_key × Signature.public_key_hash × int);
    allowed_preendorsements :
      t slot_map (Signature.public_key × Signature.public_key_hash × int);
    current_endorsement_power : t int;
    initialize_consensus_operation :
      t slot_map (Signature.public_key × Signature.public_key_hash × int)
      slot_map (Signature.public_key × Signature.public_key_hash × int) t;
    record_grand_parent_endorsement : t Signature.public_key_hash M? t;
    record_endorsement : t slot int M? t;
    record_preendorsement : t slot int round M? t;
    endorsements_seen : t slot_set;
    get_preendorsements_quorum_round : t option round;
    set_preendorsements_quorum_round : t round t;
    locked_round_evidence : t option (round × int);
    set_endorsement_branch : t Block_hash.t × Block_payload_hash.t t;
    endorsement_branch : t option (Block_hash.t × Block_payload_hash.t);
    set_grand_parent_branch : t Block_hash.t × Block_payload_hash.t t;
    grand_parent_branch : t option (Block_hash.t × Block_payload_hash.t);
  }.
End CONSENSUS.
Definition CONSENSUS := @CONSENSUS.signature.
Arguments CONSENSUS {_ _ _ _ _}.

Module Consensus.
  Definition allowed_endorsements (ctxt : t)
    : Slot_repr.Map.(Map.S.t)
      (Signature.public_key × Signature.public_key_hash × int) :=
    ctxt.(t.back).(back.consensus).(Raw_consensus.t.allowed_endorsements).

  Definition allowed_preendorsements (ctxt : t)
    : Slot_repr.Map.(Map.S.t)
      (Signature.public_key × Signature.public_key_hash × int) :=
    ctxt.(t.back).(back.consensus).(Raw_consensus.t.allowed_preendorsements).

  Definition current_endorsement_power (ctxt : t) : int :=
    ctxt.(t.back).(back.consensus).(Raw_consensus.t.current_endorsement_power).

  Definition get_preendorsements_quorum_round (ctxt : t)
    : option Round_repr.t :=
    ctxt.(t.back).(back.consensus).(Raw_consensus.t.preendorsements_quorum_round).

  Definition locked_round_evidence (ctxt : t) : option (Round_repr.t × int) :=
    Raw_consensus.locked_round_evidence ctxt.(t.back).(back.consensus).

  Definition update_consensus_with
    (ctxt : t) (f_value : Raw_consensus.t Raw_consensus.t) : t :=
    t.with_back
      (back.with_consensus (f_value ctxt.(t.back).(back.consensus))
        ctxt.(t.back)) ctxt.

  Definition update_consensus_with_tzresult {A : Set}
    (ctxt : t)
    (f_value : Raw_consensus.t Pervasives.result Raw_consensus.t A)
    : Pervasives.result t A :=
    let? consensus := f_value ctxt.(t.back).(back.consensus) in
    return? (t.with_back (back.with_consensus consensus ctxt.(t.back)) ctxt).

  Definition initialize_consensus_operation
    (ctxt : t)
    (allowed_endorsements :
      Slot_repr.Map.(Map.S.t)
        (Signature.public_key × Signature.public_key_hash × int))
    (allowed_preendorsements :
      Slot_repr.Map.(Map.S.t)
        (Signature.public_key × Signature.public_key_hash × int)) : t :=
    update_consensus_with ctxt
      (Raw_consensus.initialize_with_endorsements_and_preendorsements
        allowed_endorsements allowed_preendorsements).

  Definition record_grand_parent_endorsement
    (ctxt : t) (pkh : Signature.public_key_hash) : M? t :=
    update_consensus_with_tzresult ctxt
      (fun (ctxt : Raw_consensus.t) ⇒
        Raw_consensus.record_grand_parent_endorsement ctxt pkh).

  Definition record_preendorsement
    (ctxt : t) (initial_slot : Slot_repr.t) (power : int) (round : Round_repr.t)
    : M? t :=
    update_consensus_with_tzresult ctxt
      (Raw_consensus.record_preendorsement initial_slot power round).

  Definition record_endorsement
    (ctxt : t) (initial_slot : Slot_repr.t) (power : int) : M? t :=
    update_consensus_with_tzresult ctxt
      (fun x_1Raw_consensus.record_endorsement x_1 initial_slot power).

  Definition endorsements_seen (ctxt : t) : Slot_repr._Set.(_Set.S.t) :=
    ctxt.(t.back).(back.consensus).(Raw_consensus.t.endorsements_seen).

  Definition set_preendorsements_quorum_round (ctxt : t) (round : Round_repr.t)
    : t :=
    update_consensus_with ctxt
      (Raw_consensus.set_preendorsements_quorum_round round).

  Definition endorsement_branch (ctxt : t)
    : option (Block_hash.t × Block_payload_hash.t) :=
    Raw_consensus.endorsement_branch ctxt.(t.back).(back.consensus).

  Definition set_endorsement_branch
    (ctxt : t) (branch : Block_hash.t × Block_payload_hash.t) : t :=
    update_consensus_with ctxt
      (fun (ctxt : Raw_consensus.t) ⇒
        Raw_consensus.set_endorsement_branch ctxt branch).

  Definition grand_parent_branch (ctxt : t)
    : option (Block_hash.t × Block_payload_hash.t) :=
    Raw_consensus.grand_parent_branch ctxt.(t.back).(back.consensus).

  Definition set_grand_parent_branch
    (ctxt : t) (branch : Block_hash.t × Block_payload_hash.t) : t :=
    update_consensus_with ctxt
      (fun (ctxt : Raw_consensus.t) ⇒
        Raw_consensus.set_grand_parent_branch ctxt branch).

  (* Consensus *)
  Definition module :=
    {|
      CONSENSUS.allowed_endorsements := allowed_endorsements;
      CONSENSUS.allowed_preendorsements := allowed_preendorsements;
      CONSENSUS.current_endorsement_power := current_endorsement_power;
      CONSENSUS.initialize_consensus_operation := initialize_consensus_operation;
      CONSENSUS.record_grand_parent_endorsement :=
        record_grand_parent_endorsement;
      CONSENSUS.record_endorsement := record_endorsement;
      CONSENSUS.record_preendorsement := record_preendorsement;
      CONSENSUS.endorsements_seen := endorsements_seen;
      CONSENSUS.get_preendorsements_quorum_round :=
        get_preendorsements_quorum_round;
      CONSENSUS.set_preendorsements_quorum_round :=
        set_preendorsements_quorum_round;
      CONSENSUS.locked_round_evidence := locked_round_evidence;
      CONSENSUS.set_endorsement_branch := set_endorsement_branch;
      CONSENSUS.endorsement_branch := endorsement_branch;
      CONSENSUS.set_grand_parent_branch := set_grand_parent_branch;
      CONSENSUS.grand_parent_branch := grand_parent_branch
    |}.
End Consensus.
Definition Consensus
  : CONSENSUS (t := t) (slot_map := fun (a : Set) ⇒ Slot_repr.Map.(Map.S.t) a)
    (slot_set := Slot_repr._Set.(_Set.S.t)) (slot := Slot_repr.t)
    (round := Round_repr.t) := Consensus.module.

Module Tx_rollup.
  Definition add_message
    (ctxt : t) (rollup : Tx_rollup_repr.Hash.t)
    (message : Tx_rollup_message_hash_repr.t)
    : t × Tx_rollup_inbox_repr.Merkle.root :=
    let root_value :=
      Pervasives.ref_value
        (Tx_rollup_inbox_repr.Merkle.root_value
          Tx_rollup_inbox_repr.Merkle.empty) in
    let updater (element : option Tx_rollup_inbox_repr.Merkle.tree)
      : option Tx_rollup_inbox_repr.Merkle.tree :=
      let tree_value :=
        Option.value_value element Tx_rollup_inbox_repr.Merkle.empty in
      let tree_value :=
        Tx_rollup_inbox_repr.Merkle.add_message tree_value message in
      let '_ :=
        Pervasives.op_coloneq root_value
          (Tx_rollup_inbox_repr.Merkle.root_value tree_value) in
      Some tree_value in
    let map :=
      Tx_rollup_repr.Map.(Map.S.update) rollup updater
        ctxt.(t.back).(back.tx_rollup_current_messages) in
    let back := back.with_tx_rollup_current_messages map ctxt.(t.back) in
    ((t.with_back back ctxt), (Pervasives.op_exclamation root_value)).
End Tx_rollup.

Module Sc_rollup_in_memory_inbox.
  Definition current_messages (ctxt : t) (rollup : Sc_rollup_repr.Address.t)
    : tree :=
    (fun (function_parameter : option Context.tree) ⇒
      match function_parameter with
      | NoneTree.(Raw_context_intf.TREE.empty) ctxt
      | Some tree_valuetree_value
      end)
      (Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.find) rollup
        ctxt.(t.back).(back.sc_rollup_current_messages)).

  Definition set_current_messages
    (ctxt : t) (rollup : Sc_rollup_repr.Address.t) (tree_value : Context.tree)
    : t :=
    let sc_rollup_current_messages :=
      Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.add) rollup tree_value
        ctxt.(t.back).(back.sc_rollup_current_messages) in
    let back :=
      back.with_sc_rollup_current_messages sc_rollup_current_messages
        ctxt.(t.back) in
    t.with_back back ctxt.
End Sc_rollup_in_memory_inbox.

Explicit module to present this file as a record in Coq and reduce the size of the generated Coq code.
Module M.
  Definition t : Set := root.

  Definition mem : t Context.key bool := mem.

  Definition mem_tree : t Context.key bool := mem_tree.

  Definition get : t Context.key M? Context.value := get.

  Definition get_tree : t Context.key M? Context.tree := get_tree.

  Definition find : t Context.key option Context.value := find.

  Definition find_tree : t Context.key option Context.tree := find_tree.

  Definition list_value
    : t option int option int Context.key
    list (string × Context.tree) := list_value.

  Definition init_value : t Context.key Context.value M? t :=
    init_value.

  Definition init_tree : t Context.key Context.tree M? t := init_tree.

  Definition update : t Context.key Context.value M? t := update.

  Definition update_tree : t Context.key Context.tree M? t :=
    update_tree.

  Definition add : t Context.key Context.value t := add.

  Definition add_tree : t Context.key Context.tree t := add_tree.

  Definition remove : t Context.key t := remove.

  Definition remove_existing : t Context.key M? t := remove_existing.

  Definition remove_existing_tree : t Context.key M? t :=
    remove_existing_tree.

  Definition add_or_remove : t Context.key option Context.value t :=
    add_or_remove.

  Definition add_or_remove_tree
    : t Context.key option Context.tree t := add_or_remove_tree.

  Definition fold {A : Set}
    : option Context.depth t Context.key Variant.t A
    (Context.key Context.tree A A) A := fold.

  Definition config_value : t Context.config := config_value.

  Definition Tree := Tree.

  Definition verify_tree_proof {A : Set}
    : Context.Proof.t Context.Proof.tree
    (Context.tree Context.tree × A)
    Pervasives.result (Context.tree × A) Variant.t := verify_tree_proof.

  Definition verify_stream_proof {A : Set}
    : Context.Proof.t Context.Proof.stream
    (Context.tree Context.tree × A)
    Pervasives.result (Context.tree × A) Variant.t := verify_stream_proof.

  Definition equal_config : Context.config Context.config bool :=
    equal_config.

  Definition project : t root := project.

  Definition absolute_key : t key key := absolute_key.

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

  Definition check_enough_gas : t Gas_limit_repr.cost M? unit :=
    check_enough_gas.

  Definition description : Storage_description.t t := description.

  (* M *)
  Definition module :=
    {|
      Raw_context_intf.T.mem := mem;
      Raw_context_intf.T.mem_tree := mem_tree;
      Raw_context_intf.T.get := get;
      Raw_context_intf.T.get_tree := get_tree;
      Raw_context_intf.T.find := find;
      Raw_context_intf.T.find_tree := find_tree;
      Raw_context_intf.T.list_value := list_value;
      Raw_context_intf.T.init_value := init_value;
      Raw_context_intf.T.init_tree := init_tree;
      Raw_context_intf.T.update := update;
      Raw_context_intf.T.update_tree := update_tree;
      Raw_context_intf.T.add := add;
      Raw_context_intf.T.add_tree := add_tree;
      Raw_context_intf.T.remove := remove;
      Raw_context_intf.T.remove_existing := remove_existing;
      Raw_context_intf.T.remove_existing_tree := remove_existing_tree;
      Raw_context_intf.T.add_or_remove := add_or_remove;
      Raw_context_intf.T.add_or_remove_tree := add_or_remove_tree;
      Raw_context_intf.T.fold _ := fold;
      Raw_context_intf.T.config_value := config_value;
      Raw_context_intf.T.Tree := Tree;
      Raw_context_intf.T.verify_tree_proof _ := verify_tree_proof;
      Raw_context_intf.T.verify_stream_proof _ := verify_stream_proof;
      Raw_context_intf.T.equal_config := equal_config;
      Raw_context_intf.T.project := project;
      Raw_context_intf.T.absolute_key := absolute_key;
      Raw_context_intf.T.consume_gas := consume_gas;
      Raw_context_intf.T.check_enough_gas := check_enough_gas;
      Raw_context_intf.T.description := description
    |}.
End M.
Definition M : T (t := root) := M.module.