💾 Storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage.

Require Import TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Storage_functors.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Block_hash.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.

Proofs for all the encodings in Storage.v

Module Encoding.

The First 4 validations are focused on [UInt16], [Int32], [Int64] and [Z] all of them are related to some form of integer encoding

  Module UInt16.
    Lemma encoding_is_valid : Data_encoding.Valid.t Pervasives.UInt16.Valid.t
      Storage.Encoding.UInt16.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End UInt16.

  Module Int32.
    Lemma encoding_is_valid : Data_encoding.Valid.t Int32.Valid.t
      Storage.Encoding.Int32.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Int32.

  Module Int64.
    Lemma encoding_is_valid : Data_encoding.Valid.t Int32.Valid.t
      Storage.Encoding.Int32.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Int64.

  Module Z.
    Lemma encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True)
      Storage.Encoding.Z.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Z.

  Module Tenderbake.
    Module Branch.

The encoding [Storage.Tenderbake.Branch.encoding] is valid

      Lemma encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True)
        Storage.Tenderbake.Branch.encoding.
      Proof.
        Data_encoding.Valid.data_encoding_auto.
      Qed.
      #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
    End Branch.
  End Tenderbake.

  Module Deposits.

The encoding [Storage.Deposits.encoding] is valid

    Module Valid.
      Import TezosOfOCaml.Proto_alpha.Storage.deposits.

      Record t (x : Storage.deposits) : Prop := {
        initial_amount : Tez_repr.Valid.t x.(initial_amount);
        current_amount : Tez_repr.Valid.t x.(current_amount)
      }.
    End Valid.

    Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
      Storage.Deposits.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Deposits.

  Module Missed_endorsements_info.

The encoding [Storage.Missed_endorsements_info.encoding] is valid

    Module Valid.
      Import TezosOfOCaml.Proto_alpha.Storage.missed_endorsements_info.

      Record t (x : Storage.missed_endorsements_info) : Prop := {
        remaining_slots : Pervasives.Int31.Valid.t x.(remaining_slots);
        missed_levels : Pervasives.Int31.Valid.t x.(missed_levels)
      }.
    End Valid.

    Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
      Storage.Missed_endorsements_info.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Missed_endorsements_info.

  Module Slashed_level.

The encoding [Storage.Slashed_level.encoding] is valid

    Lemma encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True)
      Storage.Slashed_level.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Slashed_level.

  Module Cycle.
    Module Public_key_with_ghost_hash.

The encoding [Storage.Cycle.public_key_with_ghost_encoding] is valid

      Module Valid.
        Definition t (x : Signature.public_key × Signature.public_key_hash) :=
          let '(public_key, public_key_hash) := x in
          public_key_hash =
          (Signature.Public_key.(SIGNATURE_PUBLIC_KEY.hash_value) public_key).
      End Valid.

      Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
        Storage.Cycle.public_key_with_ghost_hash_encoding.
      Proof.
        Data_encoding.Valid.data_encoding_auto.
        hauto l: on.
      Qed.
      #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
    End Public_key_with_ghost_hash.

    Module Nonce_status.

The encoding [Storage.Cycle.nonce_status_encoding] is valid

      Module Valid.
        Definition t (x : Storage.Cycle.nonce_status) : Prop :=
          match x with
          | Storage.Cycle.Unrevealed _ ⇒ True
          | Storage.Cycle.Revealed v ⇒ Seed_repr.Nonce.Valid.t v
          end.
      End Valid.

      Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
        Storage.Cycle.nonce_status_encoding.
      Proof.
        Data_encoding.Valid.data_encoding_auto.
      Qed.
      #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
    End Nonce_status.
  End Cycle.
End Encoding.

In this file we give a specification of the storage system. For now, we axiomatize many properties. We give a simulation between the storage and standard OCaml data structures like records, sets and maps.

For each sub-store, we give a state and a change type. We compose the state types in records, according to the sub-store names. The change types denode which changes can be applied to the state, in a way which can be computed both in the simulated state and the concrete storage. We give a [reduce] function to explicit the way to apply a change on a simulated state.

Then we assume two functions [parse] and [apply] to go to and from the simulated state, and axiomatize that they are compatible.

Finally, we state that the operations on each sub-store are equivalent to direct operations on the simulated state. We also set the sub-stores as opaque since from now on we should only use the simulation to reason about them. The opacity prevents evaluating the sub-stores when running a [simpl] tactic for example.

Lemma Make_index_is_valid {t : Set}
  (domain : t → Prop) (I : Storage_description.INDEX (t := t)) :
  Storage_description.INDEX.Valid.t domain I →
  Storage_functors.INDEX.Valid.t (Storage.Make_index I).
  intros; constructor.
  { sauto lq: on. }
  { intros; eexists (Storage_description.Dep_One _); reflexivity. }
Qed.

(* TODO: remove these axioms once we have the full definitions. *)
Axiom generic_compare : ∀ {a : Set}, a → a → int.
Axiom generic_Path_encoding : ∀ {a : Set}, Path_encoding.S (t := a).
Axiom absolute_key : Context.key.
Axiom parametrized_absolute_key : ∀ {C_t : Set}, C_t → Context.key.

Axiom generic_Path_encoding_Valid : ∀ {a}, Compare.Valid.t (fun _ ⇒ True)
  (fun x ⇒ x)
  (Storage_sigs.Indexed_data_storage.State.compare
     (@Storage.generic_Path_encoding a)).

Module Simulation.
  Unset Primitive Projections.
  Module Big_maps.
    Record State : Set := {
      next : Single_data_storage.State.t Storage.Big_map.id;
      total_bytes : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Storage.Big_map.id))
        int;
      key_type : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Storage.Big_map.id))
        Script_repr.expr;
      value_type : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Storage.Big_map.id))
        Script_repr.expr;
      contents : Non_iterable_indexed_carbonated_data_storage_with_values.State.t
        Script_expr_hash.t
        Script_repr.expr;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <next;total_bytes;key_type;value_type;contents>.

    Definition with_next next' r :=
      RecordSet.set next (fun _ ⇒ next') r.
    Definition with_total_bytes total_bytes' r :=
      RecordSet.set total_bytes (fun _ ⇒ total_bytes') r.
    Definition with_key_type key_type' r :=
      RecordSet.set key_type (fun _ ⇒ key_type') r.
    Definition with_value_type value_type' r :=
      RecordSet.set value_type (fun _ ⇒ value_type') r.
    Definition with_contents contents' r :=
      RecordSet.set contents (fun _ ⇒ contents') r.

    Inductive Change : Set :=
    | Next : Single_data_storage.Change.t Storage.Big_map.id → Change
    | Total_bytes :
      Indexed_data_storage.Change.t
        Storage.Big_map.id int → Change
    | Key_type :
      Indexed_data_storage.Change.t
        Storage.Big_map.id Script_repr.expr → Change
    | Value_type :
      Indexed_data_storage.Change.t
        Storage.Big_map.id Script_repr.expr → Change
    | Contents :
      Non_iterable_indexed_carbonated_data_storage_with_values.Change.t
        Script_expr_hash.t Script_repr.expr → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Next change ⇒
        with_next (Single_data_storage.reduce state.(next) change) state
      | Total_bytes change ⇒
        with_total_bytes
          (Indexed_data_storage.reduce state.(total_bytes) change) state
      | Key_type change ⇒
        with_key_type
          (Indexed_data_storage.reduce state.(key_type) change) state
      | Value_type change ⇒
        with_value_type
          (Indexed_data_storage.reduce state.(value_type) change) state
      | Contents change ⇒
        with_contents
          (Non_iterable_indexed_carbonated_data_storage_with_values.reduce
            state.(contents) change) state
      end.
  End Big_maps.

  Module Contracts.
    Record State : Set := {
      global_counter : Simple_single_data_storage.State.t int;
      balance : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Tez_repr.t;
      missed_endorsements : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Storage.missed_endorsements_info;
      legacy_frozen_deposits : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t))
        Tez_repr.t;
      legacy_frozen_fees : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t))
        Tez_repr.t;
      legacy_frozen_rewards : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t))
        Tez_repr.t;
      manager : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Manager_repr.t;
      delegate : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Storage.Public_key_hash.t;
      inactive_delegate : Data_set_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t));
      delegate_desactivation : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Cycle_repr.t;
      delegated : Data_set_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t));
      counter : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        int;
      code : Non_iterable_indexed_carbonated_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Script_repr.lazy_expr;
      storage : Non_iterable_indexed_carbonated_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Script_repr.lazy_expr;
      paid_storage_space : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        int;
      used_storage_space : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        int;
      frozen_deposits_limit : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Tez_repr.t;
      frozen_deposits : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Contract_repr.t))
        Storage.deposits;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <global_counter;balance;missed_endorsements;legacy_frozen_deposits;legacy_frozen_fees;legacy_frozen_rewards;manager;delegate;inactive_delegate;delegate_desactivation;delegated;counter;code;storage;paid_storage_space;used_storage_space;frozen_deposits_limit;frozen_deposits>.

    Definition with_global_counter global_counter' r :=
      RecordSet.set global_counter (fun _ ⇒ global_counter') r.
    Definition with_balance balance' r :=
      RecordSet.set balance (fun _ ⇒ balance') r.
    Definition with_missed_endorsements missed_endorsements' r :=
      RecordSet.set missed_endorsements (fun _ ⇒ missed_endorsements') r.
    Definition with_legacy_frozen_deposits legacy_frozen_deposits' r :=
      RecordSet.set legacy_frozen_deposits (fun _ ⇒ legacy_frozen_deposits') r.
    Definition with_legacy_frozen_fees legacy_frozen_fees' r :=
      RecordSet.set legacy_frozen_fees (fun _ ⇒ legacy_frozen_fees') r.
    Definition with_legacy_frozen_rewards legacy_frozen_rewards' r :=
      RecordSet.set legacy_frozen_rewards (fun _ ⇒ legacy_frozen_rewards') r.
    Definition with_manager manager' r :=
      RecordSet.set manager (fun _ ⇒ manager') r.
    Definition with_delegate delegate' r :=
      RecordSet.set delegate (fun _ ⇒ delegate') r.
    Definition with_inactive_delegate inactive_delegate' r :=
      RecordSet.set inactive_delegate (fun _ ⇒ inactive_delegate') r.
    Definition with_delegate_desactivation delegate_desactivation' r :=
      RecordSet.set delegate_desactivation (fun _ ⇒ delegate_desactivation') r.
    Definition with_delegated delegated' r :=
      RecordSet.set delegated (fun _ ⇒ delegated') r.
    Definition with_counter counter' r :=
      RecordSet.set counter (fun _ ⇒ counter') r.
    Definition with_code code' r :=
      RecordSet.set code (fun _ ⇒ code') r.
    Definition with_storage storage' r :=
      RecordSet.set storage (fun _ ⇒ storage') r.
    Definition with_paid_storage_space paid_storage_space' r :=
      RecordSet.set paid_storage_space (fun _ ⇒ paid_storage_space') r.
    Definition with_used_storage_space used_storage_space' r :=
      RecordSet.set used_storage_space (fun _ ⇒ used_storage_space') r.
    Definition with_frozen_deposits_limit frozen_deposits_limit' r :=
      RecordSet.set frozen_deposits_limit (fun _ ⇒ frozen_deposits_limit') r.
    Definition with_frozen_deposits frozen_deposits' r :=
      RecordSet.set frozen_deposits (fun _ ⇒ frozen_deposits') r.

    Inductive Change : Set :=
    | Global_counter : Simple_single_data_storage.Change.t int → Change
    | Balance : Indexed_data_storage.Change.t
      Contract_repr.t Tez_repr.t → Change
    | Missed_endorsements : Indexed_data_storage.Change.t
      Contract_repr.t Storage.missed_endorsements_info → Change
    | Legacy_frozen_deposits : Indexed_data_storage.Change.t
      Cycle_repr.t Tez_repr.t → Change
    | Legacy_frozen_fees : Indexed_data_storage.Change.t
      Cycle_repr.t Tez_repr.t → Change
    | Legacy_frozen_rewards : Indexed_data_storage.Change.t
      Cycle_repr.t Tez_repr.t → Change
    | Manager : Indexed_data_storage.Change.t
      Contract_repr.t Manager_repr.t → Change
    | Delegate : Indexed_data_storage.Change.t
      Contract_repr.t Storage.Public_key_hash.t → Change
    | Inactive_delegate : Data_set_storage.Change.t Contract_repr.t → Change
    | Delegate_desactivation : Indexed_data_storage.Change.t
      Contract_repr.t Cycle_repr.t → Change
    | Delegated : Data_set_storage.Change.t
      Contract_repr.t → Change
    | Counter : Indexed_data_storage.Change.t
      Contract_repr.t int → Change
    | Code : Non_iterable_indexed_carbonated_data_storage.Change.t
      Contract_repr.t Script_repr.lazy_expr → Change
    | Storage : Non_iterable_indexed_carbonated_data_storage.Change.t
      Contract_repr.t Script_repr.lazy_expr → Change
    | Paid_storage_space : Indexed_data_storage.Change.t
      Contract_repr.t int → Change
    | Used_storage_space : Indexed_data_storage.Change.t
      Contract_repr.t int → Change
    | Frozen_deposits_limit : Indexed_data_storage.Change.t
      Contract_repr.t Tez_repr.t → Change
    | Frozen_deposits : Indexed_data_storage.Change.t
      Contract_repr.t Storage.deposits → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Global_counter change ⇒
        with_global_counter
          (Simple_single_data_storage.reduce state.(global_counter) change) state
      | Balance change ⇒
        with_balance
          (Indexed_data_storage.reduce state.(balance) change) state
      | Missed_endorsements change ⇒
        with_missed_endorsements
          (Indexed_data_storage.reduce state.(missed_endorsements) change) state
      | Legacy_frozen_deposits change ⇒
        with_legacy_frozen_deposits
          (Indexed_data_storage.reduce state.(legacy_frozen_deposits) change) state
      | Legacy_frozen_fees change ⇒
        with_legacy_frozen_fees
          (Indexed_data_storage.reduce state.(legacy_frozen_fees) change) state
      | Legacy_frozen_rewards change ⇒
        with_legacy_frozen_rewards
          (Indexed_data_storage.reduce state.(legacy_frozen_rewards) change) state
      | Manager change ⇒
        with_manager
          (Indexed_data_storage.reduce state.(manager) change) state
      | Delegate change ⇒
        with_delegate
          (Indexed_data_storage.reduce state.(delegate) change) state
      | Inactive_delegate change ⇒
        with_inactive_delegate
          (Data_set_storage.reduce state.(inactive_delegate) change) state
      | Delegate_desactivation change ⇒
        with_delegate_desactivation
          (Indexed_data_storage.reduce
            state.(delegate_desactivation) change) state
      | Delegated change ⇒
        with_delegated
          (Data_set_storage.reduce state.(delegated) change) state
      | Counter change ⇒
        with_counter
          (Indexed_data_storage.reduce state.(counter) change) state
      | Code change ⇒
        with_code
          (Non_iterable_indexed_carbonated_data_storage.reduce
            state.(code) change) state
      | Storage change ⇒
        with_storage
          (Non_iterable_indexed_carbonated_data_storage.reduce
            state.(storage) change) state
      | Paid_storage_space change ⇒
        with_paid_storage_space
          (Indexed_data_storage.reduce state.(paid_storage_space) change) state
      | Used_storage_space change ⇒
        with_used_storage_space
          (Indexed_data_storage.reduce state.(used_storage_space) change) state
      | Frozen_deposits_limit change ⇒
        with_frozen_deposits_limit
          (Indexed_data_storage.reduce state.(frozen_deposits_limit) change) state
      | Frozen_deposits change ⇒
        with_frozen_deposits
          (Indexed_data_storage.reduce state.(frozen_deposits) change) state
      end.
  End Contracts.

  Module Cycles.
    Record State : Set := {
      delegate_sampler_state : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t))
        (Sampler.t (Signature.public_key × Signature.public_key_hash));
      slashed_deposits : Indexed_data_storage.State.t
        (generic_Path_encoding (a := int32 × public_key_hash ))
        Storage.slashed_level;
      total_active_stake : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t)) Tez_repr.t;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <delegate_sampler_state;slashed_deposits;total_active_stake>.

    Definition with_delegate_sampler_state delegate_sampler_state' r :=
      RecordSet.set delegate_sampler_state (fun _ ⇒ delegate_sampler_state') r.
    Definition with_slashed_deposits slashed_deposits' r :=
      RecordSet.set slashed_deposits (fun _ ⇒ slashed_deposits') r.
    Definition with_total_active_stake total_active_stake' r :=
      RecordSet.set total_active_stake (fun _ ⇒ total_active_stake') r.

    Inductive Change : Set :=
    | Delegate_sampler_state : Indexed_data_storage.Change.t Cycle_repr.t
      (Sampler.t (Signature.public_key × Signature.public_key_hash)) → Change
    | Slashed_deposits : Indexed_data_storage.Change.t
      (Raw_level_repr.t × Signature.public_key_hash)
      Storage.slashed_level → Change
    | Total_active_stake : Indexed_data_storage.Change.t
      Cycle_repr.t Tez_repr.t → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Delegate_sampler_state change ⇒
        with_delegate_sampler_state
          (Indexed_data_storage.reduce state.(delegate_sampler_state) change) state
      | Slashed_deposits change ⇒
        with_slashed_deposits
          (Indexed_data_storage.reduce state.(slashed_deposits) change) state
      | Total_active_stake change ⇒
        with_total_active_stake
          (Indexed_data_storage.reduce state.(total_active_stake) change) state
      end.
  End Cycles.

  Module Global_constants.
    Record State : Set := {
      map : Non_iterable_indexed_carbonated_data_storage.State.t
         (generic_Path_encoding (a := Script_expr_hash.t))
        Script_repr.expr;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <map>.

    Definition with_map map' r :=
      RecordSet.set map (fun _ ⇒ map') r.

    Inductive Change : Set :=
    | Map : Non_iterable_indexed_carbonated_data_storage.Change.t
        Script_expr_hash.t Script_repr.expr → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Map change ⇒
        with_map
          (Non_iterable_indexed_carbonated_data_storage.reduce
            state.(map) change) state
      end.
  End Global_constants.

  Module Liquidity_baking.
    Record State : Set := {
      toggle_ema : Single_data_storage.State.t int32;
      cpmm_address : Single_data_storage.State.t Contract_repr.t;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <toggle_ema;cpmm_address>.

    Definition with_toggle_ema toggle_ema' r :=
      RecordSet.set toggle_ema (fun _ ⇒ toggle_ema') r.
    Definition with_cpmm_address cpmm_address' r :=
      RecordSet.set cpmm_address (fun _ ⇒ cpmm_address') r.

    Inductive Change : Set :=
    | Toggle_ema : Single_data_storage.Change.t int32 → Change
    | Cpmm_address : Single_data_storage.Change.t Contract_repr.t → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Toggle_ema change ⇒
        with_toggle_ema
          (Single_data_storage.reduce state.(toggle_ema) change) state
      | Cpmm_address change ⇒
        with_cpmm_address
          (Single_data_storage.reduce state.(cpmm_address) change) state
      end.
  End Liquidity_baking.

  Module Pending_migrations.
    Record State : Set := {
      balance_updates : Single_data_storage.State.t
        Receipt_repr.balance_updates;
      operation_results : Single_data_storage.State.t
        (list Migration_repr.origination_result)
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <balance_updates;operation_results>.

    Definition with_balance_updates balance_updates' r :=
      RecordSet.set balance_updates (fun _ ⇒ balance_updates') r.
    Definition with_operation_results operation_results' r :=
      RecordSet.set operation_results (fun _ ⇒ operation_results') r.

    Inductive Change : Set :=
    | Balance_updates : Single_data_storage.Change.t
      Receipt_repr.balance_updates → Change
    | Operation_results : Single_data_storage.Change.t
      (list Migration_repr.origination_result) → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Balance_updates change ⇒
        with_balance_updates
          (Single_data_storage.reduce state.(balance_updates) change) state
      | Operation_results change ⇒
        with_operation_results
          (Single_data_storage.reduce state.(operation_results) change) state
      end.
  End Pending_migrations.

  Module Ramp_up.
    Record State : Set := {
      rewards : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t))
        Storage.Ramp_up.reward;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <rewards>.

    Definition with_rewards rewards' r :=
      RecordSet.set rewards (fun _ ⇒ rewards') r.

    Inductive Change : Set :=
    | Rewards : Indexed_data_storage.Change.t
      Cycle_repr.t Storage.Ramp_up.reward → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Rewards change ⇒
        with_rewards
          (Indexed_data_storage.reduce state.(rewards) change) state
      end.
  End Ramp_up.

  Module Sapling.
    Record State : Set := {
      next : Single_data_storage.State.t Storage.Sapling.id;
      total_bytes : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Storage.Sapling.id))
        int;
      commitments_size : Single_data_storage.State.t int64;
      memo_size : Single_data_storage.State.t int;
      commitments : Non_iterable_indexed_carbonated_data_storage.State.t
        (generic_Path_encoding (a := Sapling.Hash.t))
        int64;
      ciphertexts : Non_iterable_indexed_carbonated_data_storage.State.t
        (generic_Path_encoding (a := int64))
        Ciphertext.t;
      nullifiers_size : Single_data_storage.State.t int64;
      nullifiers_ordered : Non_iterable_indexed_data_storage.State.t
        (generic_Path_encoding (a := int64))
        Sapling.Nullifier.t;
      nullifiers_hashed : Carbonated_data_set_storage.State.t
        Sapling.Nullifier.t;
      roots : Non_iterable_indexed_data_storage.State.t
        (generic_Path_encoding (a := int32))
        Sapling.Hash.t;
      roots_pos : Single_data_storage.State.t int32;
      roots_level : Single_data_storage.State.t Raw_level_repr.t;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <next;total_bytes;commitments_size;memo_size;commitments;ciphertexts;nullifiers_size;nullifiers_ordered;nullifiers_hashed;roots;roots_pos;roots_level>.

    Definition with_next next' r :=
      RecordSet.set next (fun _ ⇒ next') r.
    Definition with_total_bytes total_bytes' r :=
      RecordSet.set total_bytes (fun _ ⇒ total_bytes') r.
    Definition with_commitments_size commitments_size' r :=
      RecordSet.set commitments_size (fun _ ⇒ commitments_size') r.
    Definition with_memo_size memo_size' r :=
      RecordSet.set memo_size (fun _ ⇒ memo_size') r.
    Definition with_commitments commitments' r :=
      RecordSet.set commitments (fun _ ⇒ commitments') r.
    Definition with_ciphertexts ciphertexts' r :=
      RecordSet.set ciphertexts (fun _ ⇒ ciphertexts') r.
    Definition with_nullifiers_size nullifiers_size' r :=
      RecordSet.set nullifiers_size (fun _ ⇒ nullifiers_size') r.
    Definition with_nullifiers_ordered nullifiers_ordered' r :=
      RecordSet.set nullifiers_ordered (fun _ ⇒ nullifiers_ordered') r.
    Definition with_nullifiers_hashed nullifiers_hashed' r :=
      RecordSet.set nullifiers_hashed (fun _ ⇒ nullifiers_hashed') r.
    Definition with_roots roots' r :=
      RecordSet.set roots (fun _ ⇒ roots') r.
    Definition with_roots_pos roots_pos' r :=
      RecordSet.set roots_pos (fun _ ⇒ roots_pos') r.
    Definition with_roots_level roots_level' r :=
      RecordSet.set roots_level (fun _ ⇒ roots_level') r.

    Inductive Change : Set :=
    | Next : Single_data_storage.Change.t Storage.Sapling.id → Change
    | Total_bytes : Indexed_data_storage.Change.t Storage.Sapling.id int → Change
    | Commitments_size : Single_data_storage.Change.t int64 → Change
    | Memo_size : Single_data_storage.Change.t int → Change
    | Commitments : Non_iterable_indexed_carbonated_data_storage.Change.t
      Sapling.Hash.t int64 → Change
    | Ciphertexts : Non_iterable_indexed_carbonated_data_storage.Change.t
      int64 Ciphertext.t → Change
    | Nullifiers_size : Single_data_storage.Change.t int64 → Change
    | Nullifiers_ordered : Non_iterable_indexed_data_storage.Change.t int64 Sapling.Nullifier.t → Change
    | Nullifiers_hashed : Carbonated_data_set_storage.Change.t
      Sapling.Nullifier.t → Change
    | Roots : Non_iterable_indexed_data_storage.Change.t int32 Sapling.Hash.t → Change
    | Roots_pos : Single_data_storage.Change.t int32 → Change
    | Roots_level : Single_data_storage.Change.t Raw_level_repr.t → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Next change ⇒
        with_next
          (Single_data_storage.reduce state.(next) change) state
      | Total_bytes change ⇒
        with_total_bytes
          (Indexed_data_storage.reduce state.(total_bytes) change) state
      | Commitments_size change ⇒
        with_commitments_size
          (Single_data_storage.reduce state.(commitments_size) change) state
      | Memo_size change ⇒
        with_memo_size
          (Single_data_storage.reduce state.(memo_size) change) state
      | Commitments change ⇒
        with_commitments
          (Non_iterable_indexed_carbonated_data_storage.reduce
            state.(commitments) change) state
      | Ciphertexts change ⇒
        with_ciphertexts
          (Non_iterable_indexed_carbonated_data_storage.reduce
            state.(ciphertexts) change) state
      | Nullifiers_size change ⇒
        with_nullifiers_size
          (Single_data_storage.reduce state.(nullifiers_size) change) state
      | Nullifiers_ordered change ⇒
        with_nullifiers_ordered
          (Non_iterable_indexed_data_storage.reduce
            state.(nullifiers_ordered) change) state
      | Nullifiers_hashed change ⇒
        with_nullifiers_hashed
          (Carbonated_data_set_storage.reduce
            state.(nullifiers_hashed) change) state
      | Roots change ⇒
        with_roots
          (Non_iterable_indexed_data_storage.reduce state.(roots) change) state
      | Roots_pos change ⇒
        with_roots_pos
          (Single_data_storage.reduce state.(roots_pos) change) state
      | Roots_level change ⇒
        with_roots_level
          (Single_data_storage.reduce state.(roots_level) change) state
      end.
  End Sapling.

  Module Sc_rollup.
    Record State : Set := {
      (* TODO: The correct field name is `state` but it was causing an error *)
      pvm_kind : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Sc_rollup_repr.t))
        Sc_rollup_repr.Kind.t;
      boot_sector : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Sc_rollup_repr.t))
        string;
      inbox : Non_iterable_indexed_carbonated_data_storage.State.t
        (generic_Path_encoding (a := Sc_rollup_repr.t))
        Sc_rollup_inbox_repr.t;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <pvm_kind;boot_sector;inbox>.

    Definition with_pvm_kind pvm_kind' r :=
      RecordSet.set pvm_kind (fun _ ⇒ pvm_kind') r.
    Definition with_boot_sector boot_sector' r :=
      RecordSet.set boot_sector (fun _ ⇒ boot_sector') r.
    Definition with_inbox inbox' r :=
      RecordSet.set inbox (fun _ ⇒ inbox') r.

    Inductive Change : Set :=
    | PVM_kind : Indexed_data_storage.Change.t
      Sc_rollup_repr.t Sc_rollup_repr.Kind.t → Change
    | Boot_sector : Indexed_data_storage.Change.t
      Sc_rollup_repr.t string → Change
    | Inbox : Non_iterable_indexed_carbonated_data_storage.Change.t
      Sc_rollup_repr.t Sc_rollup_inbox_repr.t → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | PVM_kind change ⇒
        with_pvm_kind
          (Indexed_data_storage.reduce state.(pvm_kind) change)
          state
      | Boot_sector change ⇒
        with_boot_sector
          (Indexed_data_storage.reduce state.(boot_sector) change)
          state
      | Inbox change ⇒
        with_inbox
          (Non_iterable_indexed_carbonated_data_storage.reduce state.(inbox) change)
          state
      end.
  End Sc_rollup.

  Module Seeds.
    Record State : Set := {
      nonce_legacy : Non_iterable_indexed_data_storage.State.t
        (generic_Path_encoding (a := Level_repr.t))
        Storage.Seed.nonce_status;
      nonce : Non_iterable_indexed_data_storage.State.t
        (generic_Path_encoding (a := Level_repr.t))
        Storage.Seed.nonce_status;
      for_cycle : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t))
        Seed_repr.seed;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <nonce_legacy;nonce;for_cycle>.

    Definition with_nonce_legacy nonce_legacy' r :=
      RecordSet.set nonce_legacy (fun _ ⇒ nonce_legacy') r.
    Definition with_nonce nonce' r :=
      RecordSet.set nonce (fun _ ⇒ nonce') r.
    Definition with_for_cycle for_cycle' r :=
      RecordSet.set for_cycle (fun _ ⇒ for_cycle') r.

    Inductive Change : Set :=
    | Nonce_legacy : Non_iterable_indexed_data_storage.Change.t
      Level_repr.t Storage.Seed.nonce_status → Change
    | Nonce : Non_iterable_indexed_data_storage.Change.t
      Level_repr.t Storage.Seed.nonce_status → Change
    | For_cycle : For_cycle.Change.t → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Nonce_legacy change ⇒
        with_nonce_legacy
          (Non_iterable_indexed_data_storage.reduce state.(nonce_legacy) change)
          state
      | Nonce change ⇒
        with_nonce
          (Non_iterable_indexed_data_storage.reduce state.(nonce) change)
          state
      | For_cycle change ⇒
        with_for_cycle
          (For_cycle.reduce state.(for_cycle) change)
          state
      end.
  End Seeds.

  Module Stakes.
    Record State : Set := {
      active_delegate_with_one_roll : Indexed_data_snapshotable_storage.State.t
        Storage.Public_key_hash.t unit int;
      last_snapshot : Single_data_storage.State.t int;
      selected_distribution_for_cycle : Indexed_data_storage.State.t
        (generic_Path_encoding (a := Cycle_repr.t))
        (list (Signature.public_key_hash × Tez_repr.t));
      staking_balance : Indexed_data_snapshotable_storage.State.t
        Storage.Public_key_hash.t Tez_repr.t int;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <active_delegate_with_one_roll;last_snapshot;selected_distribution_for_cycle;staking_balance>.

    Definition with_active_delegate_with_one_roll active_delegate_with_one_roll' r :=
      RecordSet.set active_delegate_with_one_roll (fun _ ⇒ active_delegate_with_one_roll') r.
    Definition with_last_snapshot last_snapshot' r :=
      RecordSet.set last_snapshot (fun _ ⇒ last_snapshot') r.
    Definition with_selected_distribution_for_cycle selected_distribution_for_cycle' r :=
      RecordSet.set selected_distribution_for_cycle (fun _ ⇒ selected_distribution_for_cycle') r.
    Definition with_staking_balance staking_balance' r :=
      RecordSet.set staking_balance (fun _ ⇒ staking_balance') r.

    Inductive Change : Set :=
    | Active_delegate_with_one_roll : Indexed_data_snapshotable_storage.Change.t
      Storage.Public_key_hash.t unit int → Change
    | Last_snapshot : Single_data_storage.Change.t int → Change
    | Selected_distribution_for_cycle : Indexed_data_storage.Change.t
      Cycle_repr.t (list (Signature.public_key_hash × Tez_repr.t)) → Change
    | Staking_balance : Indexed_data_snapshotable_storage.Change.t
      Storage.Public_key_hash.t Tez_repr.t int → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Active_delegate_with_one_roll change ⇒
        with_active_delegate_with_one_roll
          (Indexed_data_snapshotable_storage.reduce state.(active_delegate_with_one_roll) change) state
      | Last_snapshot change ⇒
        with_last_snapshot
          (Single_data_storage.reduce state.(last_snapshot) change) state
      | Selected_distribution_for_cycle change ⇒
        with_selected_distribution_for_cycle
          (Indexed_data_storage.reduce state.(selected_distribution_for_cycle) change) state
      | Staking_balance change ⇒
        with_staking_balance
          (Indexed_data_snapshotable_storage.reduce state.(staking_balance) change) state
      end.
  End Stakes.

  Module Tenderbake.
    Record State : Set := {
      first_level_legacy : Single_data_storage.State.t Raw_level_repr.t;
      endorsement_branch : Single_data_storage.State.t Storage.Tenderbake.Branch.t;
      grand_parent_branch : Single_data_storage.State.t Storage.Tenderbake.Branch.t;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <first_level_legacy;endorsement_branch;grand_parent_branch>.

    Definition with_first_level_legacy first_level_legacy' r :=
      RecordSet.set first_level_legacy (fun _ ⇒ first_level_legacy') r.
    Definition with_endorsement_branch endorsement_branch' r :=
      RecordSet.set endorsement_branch (fun _ ⇒ endorsement_branch') r.
    Definition with_grand_parent_branch grand_parent_branch' r :=
      RecordSet.set grand_parent_branch (fun _ ⇒ grand_parent_branch') r.

    Inductive Change : Set :=
    | First_level_legacy :
      Single_data_storage.Change.t Raw_level_repr.t → Change
    | Endorsement_branch :
      Single_data_storage.Change.t Storage.Tenderbake.Branch.t → Change
    | Grand_parent_branch :
      Single_data_storage.Change.t Storage.Tenderbake.Branch.t → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | First_level_legacy change ⇒
        with_first_level_legacy
          (Single_data_storage.reduce state.(first_level_legacy) change)
          state
      | Endorsement_branch change ⇒
        with_endorsement_branch
          (Single_data_storage.reduce state.(endorsement_branch) change) state
      | Grand_parent_branch change ⇒
        with_grand_parent_branch
          (Single_data_storage.reduce state.(grand_parent_branch) change) state
      end.
  End Tenderbake.

  Module Tickets_balance.
    Record State : Set := {
      table : Non_iterable_indexed_carbonated_data_storage.State.t
        (generic_Path_encoding (a := Ticket_hash_repr.t))
        int;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <table>.

    Definition with_table table' r :=
      RecordSet.set table (fun _ ⇒ table') r.

    Inductive Change : Set :=
    | Table : Non_iterable_indexed_carbonated_data_storage.Change.t
      Ticket_hash_repr.t int → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Table change ⇒
        with_table
          (Non_iterable_indexed_carbonated_data_storage.reduce state.(table) change)
          state
      end.
  End Tickets_balance.

  Module Tx_rollup.
    Record State : Set := {
      (* TODO: The correct field name is `state` but it was causing an error *)
      tx_state : Non_iterable_indexed_carbonated_data_storage.State.t
        (generic_Path_encoding (a := Tx_rollup_repr.t))
        Tx_rollup_state_repr.t;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <tx_state>.

    Definition with_tx_state tx_state' r :=
      RecordSet.set tx_state (fun _ ⇒ tx_state') r.

    Inductive Change : Set :=
    | Tx_state : Non_iterable_indexed_carbonated_data_storage.Change.t
      Tx_rollup_repr.t Tx_rollup_state_repr.t → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Tx_state change ⇒
        with_tx_state
          (Non_iterable_indexed_carbonated_data_storage.reduce state.(tx_state) change)
          state
      end.
  End Tx_rollup.

  Module Votes.
    Record State : Set := {
      pred_period_kind : Single_data_storage.State.t Voting_period_repr.kind;
      current_period : Single_data_storage.State.t Voting_period_repr.t;
      participation_ema : Single_data_storage.State.t int32;
      current_proposal : Single_data_storage.State.t Protocol_hash.t;
      listings_size : Single_data_storage.State.t int32;
      listings :
        Indexed_data_storage.State.t
          (generic_Path_encoding (a := public_key_hash))
          int32;
      proposals :
        Data_set_storage.State.t
          (generic_Path_encoding (a :=
            Protocol_hash.t × Signature.public_key_hash));
      proposals_count :
        Indexed_data_storage.State.t
          (generic_Path_encoding (a := public_key_hash))
          int;
      ballots :
        Indexed_data_storage.State.t
          (generic_Path_encoding (a := public_key_hash))
          Vote_repr.ballot;
    }.

    #[global] Instance etaState : Settable _ := settable!
      Build_State <pred_period_kind;current_period;participation_ema;current_proposal;listings_size;listings;proposals;proposals_count;ballots>.

    Definition with_pred_period_kind pred_period_kind' r :=
      RecordSet.set pred_period_kind (fun _ ⇒ pred_period_kind') r.
    Definition with_current_period current_period' r :=
      RecordSet.set current_period (fun _ ⇒ current_period') r.
    Definition with_participation_ema participation_ema' r :=
      RecordSet.set participation_ema (fun _ ⇒ participation_ema') r.
    Definition with_current_proposal current_proposal' r :=
      RecordSet.set current_proposal (fun _ ⇒ current_proposal') r.
    Definition with_listings_size listings_size' r :=
      RecordSet.set listings_size (fun _ ⇒ listings_size') r.
    Definition with_listings listings' r :=
      RecordSet.set listings (fun _ ⇒ listings') r.
    Definition with_proposals proposals' r :=
      RecordSet.set proposals (fun _ ⇒ proposals') r.
    Definition with_proposals_count proposals_count' r :=
      RecordSet.set proposals_count (fun _ ⇒ proposals_count') r.
    Definition with_ballots ballots' r :=
      RecordSet.set ballots (fun _ ⇒ ballots') r.

    Inductive Change : Set :=
    | Pred_period_kind :
      Single_data_storage.Change.t Voting_period_repr.kind → Change
    | Current_period :
      Single_data_storage.Change.t Voting_period_repr.t → Change
    | Participation_ema :
      Single_data_storage.Change.t int32 → Change
    | Current_proposal :
      Single_data_storage.Change.t Protocol_hash.t → Change
    | Listings_size :
      Single_data_storage.Change.t int32 → Change
    | Listings :
      Indexed_data_storage.Change.t
        Signature.public_key_hash int32 → Change
    | Proposals :
      Data_set_storage.Change.t
        (Protocol_hash.t × Signature.public_key_hash) → Change
    | Proposals_count :
      Indexed_data_storage.Change.t
        Signature.public_key_hash int → Change
    | Ballots :
      Indexed_data_storage.Change.t
        Signature.public_key_hash Vote_repr.ballot → Change.

    Definition reduce (state : State) (change : Change) : State :=
      match change with
      | Pred_period_kind change ⇒
        with_pred_period_kind
          (Single_data_storage.reduce state.(pred_period_kind) change) state
      | Current_period change ⇒
        with_current_period
          (Single_data_storage.reduce state.(current_period) change) state
      | Participation_ema change ⇒
        with_participation_ema
          (Single_data_storage.reduce state.(participation_ema) change) state
      | Current_proposal change ⇒
        with_current_proposal
          (Single_data_storage.reduce state.(current_proposal) change) state
      | Listings_size change ⇒
        with_listings_size
          (Single_data_storage.reduce state.(listings_size) change) state
      | Listings change ⇒
        with_listings
          (Indexed_data_storage.reduce state.(listings) change) state
      | Proposals change ⇒
        with_proposals (Data_set_storage.reduce state.(proposals) change) state
      | Proposals_count change ⇒
        with_proposals_count
          (Indexed_data_storage.reduce state.(proposals_count) change) state
      | Ballots change ⇒
        with_ballots
          (Indexed_data_storage.reduce state.(ballots) change) state
      end.
  End Votes.

  Record State : Set := {
    big_maps : Big_maps.State;
    block_round : Simple_single_data_storage.State.t int32;
    commitments : Indexed_data_storage.State.t
      (generic_Path_encoding (a := Blinded_public_key_hash.t))
      Tez_repr.t;
    contracts : Contracts.State;
    cycles : Cycles.State;
    delegates : Data_set_storage.State.t
      (generic_Path_encoding (a := Storage.Public_key_hash.t));
    global_constants : Global_constants.State;
    legacy_active_delegates_with_rolls : Data_set_storage.State.t
      (generic_Path_encoding (a := Storage.Public_key_hash.t));
    legacy_block_priority : Simple_single_data_storage.State.t int;
    legacy_delegates_with_frozen_balance : Data_set_storage.State.t
      (generic_Path_encoding (a := Storage.Public_key_hash.t));
    liquidity_baking : Liquidity_baking.State;
    pending_migrations : Pending_migrations.State;
    ramp_up : Ramp_up.State;
    sapling : Sapling.State;
    sc_rollup : Sc_rollup.State;
    seeds : Seeds.State;
    stakes : Stakes.State;
    tenderbake : Tenderbake.State;
    tickets_balance : Tickets_balance.State;
    tx_rollup : Tx_rollup.State;
    votes : Votes.State;
  }.

  #[global] Instance etaState : Settable _ := settable!
      Build_State <big_maps;block_round;commitments;contracts;cycles;delegates;global_constants;legacy_active_delegates_with_rolls;legacy_block_priority;legacy_delegates_with_frozen_balance;liquidity_baking;pending_migrations;ramp_up;sapling;sc_rollup;seeds;stakes;tenderbake;tickets_balance;tx_rollup;votes>.

  Definition with_big_maps big_maps' r :=
    RecordSet.set big_maps (fun _ ⇒ big_maps') r.
  Definition with_block_round block_round' r :=
    RecordSet.set block_round (fun _ ⇒ block_round') r.
  Definition with_commitments commitments' r :=
    RecordSet.set commitments (fun _ ⇒ commitments') r.
  Definition with_contracts contracts' r :=
    RecordSet.set contracts (fun _ ⇒ contracts') r.
  Definition with_cycles cycles' r :=
    RecordSet.set cycles (fun _ ⇒ cycles') r.
  Definition with_delegates delegates' r :=
    RecordSet.set delegates (fun _ ⇒ delegates') r.
  Definition with_global_constants global_constants' r :=
    RecordSet.set global_constants (fun _ ⇒ global_constants') r.
  Definition with_legacy_active_delegates_with_rolls legacy_active_delegates_with_rolls' r :=
    RecordSet.set legacy_active_delegates_with_rolls (fun _ ⇒ legacy_active_delegates_with_rolls') r.
  Definition with_legacy_block_priority legacy_block_priority' r :=
    RecordSet.set legacy_block_priority (fun _ ⇒ legacy_block_priority') r.
  Definition with_legacy_delegates_with_frozen_balance legacy_delegates_with_frozen_balance' r :=
    RecordSet.set legacy_delegates_with_frozen_balance (fun _ ⇒ legacy_delegates_with_frozen_balance') r.
  Definition with_liquidity_baking liquidity_baking' r :=
    RecordSet.set liquidity_baking (fun _ ⇒ liquidity_baking') r.
  Definition with_pending_migrations pending_migrations' r :=
    RecordSet.set pending_migrations (fun _ ⇒ pending_migrations') r.
  Definition with_ramp_up ramp_up' r :=
    RecordSet.set ramp_up (fun _ ⇒ ramp_up') r.
  Definition with_sapling sapling' r :=
    RecordSet.set sapling (fun _ ⇒ sapling') r.
  Definition with_sc_rollup sc_rollup' r :=
    RecordSet.set sc_rollup (fun _ ⇒ sc_rollup') r.
  Definition with_seeds seeds' r :=
    RecordSet.set seeds (fun _ ⇒ seeds') r.
  Definition with_stakes stakes' r :=
    RecordSet.set stakes (fun _ ⇒ stakes') r.
  Definition with_tenderbake tenderbake' r :=
    RecordSet.set tenderbake (fun _ ⇒ tenderbake') r.
  Definition with_tickets_balance tickets_balance' r :=
    RecordSet.set tickets_balance (fun _ ⇒ tickets_balance') r.
  Definition with_tx_rollup tx_rollup' r :=
    RecordSet.set tx_rollup (fun _ ⇒ tx_rollup') r.
  Definition with_votes votes' r :=
    RecordSet.set votes (fun _ ⇒ votes') r.

  Inductive Change : Set :=
  | Big_maps : Big_maps.Change → Change
  | Block_round : Simple_single_data_storage.Change.t int → Change
  | Commitments : Indexed_data_storage.Change.t
    Blinded_public_key_hash.t Tez_repr.t → Change
  | Contracts : Contracts.Change → Change
  | Cycles : Cycles.Change → Change
  | Delegates : Data_set_storage.Change.t Storage.Public_key_hash.t→ Change
  | Global_constants : Global_constants.Change → Change
  | Legacy_active_delegates_with_rolls : Data_set_storage.Change.t
    Storage.Public_key_hash.t→ Change
  | Legacy_block_priority : Simple_single_data_storage.Change.t int → Change
  | Legacy_delegates_with_frozen_balance : Data_set_storage.Change.t
    Storage.Public_key_hash.t→ Change
  | Liquidity_baking : Liquidity_baking.Change → Change
  | Pending_migrations : Pending_migrations.Change → Change
  | Ramp_up : Ramp_up.Change → Change
  | Sapling : Sapling.Change → Change
  | Sc_rollup : Sc_rollup.Change → Change
  | Seeds : Seeds.Change → Change
  | Stakes : Stakes.Change → Change
  | Tenderbake : Tenderbake.Change → Change
  | Tickets_balance : Tickets_balance.Change → Change
  | Tx_rollup : Tx_rollup.Change → Change
  | Votes : Votes.Change → Change.

  Definition reduce (state : State) (change : Change) : State :=
    match change with
    | Big_maps change ⇒
      with_big_maps (Big_maps.reduce state.(big_maps) change) state
    | Block_round change ⇒
      with_block_round
        (Simple_single_data_storage.reduce state.(block_round) change) state
    | Commitments change ⇒
      with_commitments
        (Indexed_data_storage.reduce state.(commitments) change) state
    | Contracts change ⇒
      with_contracts (Contracts.reduce state.(contracts) change) state
    | Cycles change ⇒ with_cycles (Cycles.reduce state.(cycles) change) state
    | Delegates change ⇒
      with_delegates (Data_set_storage.reduce state.(delegates) change) state
    | Global_constants change ⇒
      with_global_constants
        (Global_constants.reduce state.(global_constants) change) state
    | Legacy_active_delegates_with_rolls change ⇒
      with_legacy_active_delegates_with_rolls
        (Data_set_storage.reduce state.(legacy_active_delegates_with_rolls) change)
        state
    | Legacy_block_priority change ⇒
      with_legacy_block_priority
        (Simple_single_data_storage.reduce state.(legacy_block_priority) change)
        state
    | Legacy_delegates_with_frozen_balance change ⇒
      with_legacy_delegates_with_frozen_balance
        (Data_set_storage.reduce state.(legacy_delegates_with_frozen_balance) change)
        state
    | Liquidity_baking change ⇒
      with_liquidity_baking
        (Liquidity_baking.reduce state.(liquidity_baking) change) state
    | Pending_migrations change ⇒
      with_pending_migrations
        (Pending_migrations.reduce state.(pending_migrations) change) state
    | Ramp_up change ⇒
      with_ramp_up (Ramp_up.reduce state.(ramp_up) change) state
    | Sapling change ⇒
      with_sapling (Sapling.reduce state.(sapling) change) state
    | Sc_rollup change ⇒
      with_sc_rollup (Sc_rollup.reduce state.(sc_rollup) change) state
    | Seeds change ⇒ with_seeds (Seeds.reduce state.(seeds) change) state
    | Stakes change ⇒ with_stakes (Stakes.reduce state.(stakes) change) state
    | Tenderbake change ⇒
      with_tenderbake (Tenderbake.reduce state.(tenderbake) change) state
    | Tickets_balance change ⇒
      with_tickets_balance
        (Tickets_balance.reduce state.(tickets_balance) change) state
    | Tx_rollup change ⇒
      with_tx_rollup (Tx_rollup.reduce state.(tx_rollup) change) state
    | Votes change ⇒ with_votes (Votes.reduce state.(votes) change) state
    end.
  Set Primitive Projections.
End Simulation.

Parameter parse : Raw_context.t → Simulation.State.

Parameter apply : Raw_context.t → Simulation.Change → Raw_context.t.

Axiom parse_apply : ∀ ctxt change,
  parse (apply ctxt change) = Simulation.reduce (parse ctxt) change.

Ltac auto_parse_apply :=
  autounfold with storage_db;
  repeat rewrite parse_apply; simpl.

Module Eq.
  Import Simulation.

  Module Big_maps.
    Module Next.
      Definition parse ctxt :=
        (parse ctxt).(big_maps).(Big_maps.next).

      Definition apply ctxt change :=
        apply ctxt (Big_maps (Big_maps.Next change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Big_map.Next.Storage
        (Single_data_storage.Make parse apply ["big_maps"; "next"]).

      #[global] Opaque Storage.Big_map.Next.Storage.
      #[global] Hint Unfold parse apply : storage_db.
    End Next.

    Module Total_bytes.
      Definition parse ctxt :=
        (parse ctxt).(big_maps).(Big_maps.total_bytes).

      Definition apply ctxt change :=
        apply ctxt (Big_maps (Big_maps.Total_bytes change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Big_map.Total_bytes
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Big_map.Total_bytes.
      #[global] Hint Unfold parse apply : storage_db.
    End Total_bytes.

    Module Key_type.
      Definition parse ctxt :=
        (parse ctxt).(big_maps).(Big_maps.key_type).

      Definition apply ctxt change :=
        apply ctxt (Big_maps (Big_maps.Key_type change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Big_map.Key_type
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Big_map.Key_type.
      #[global] Hint Unfold parse apply : storage_db.
    End Key_type.

    Module Value_type.
      Definition parse ctxt :=
        (parse ctxt).(big_maps).(Big_maps.value_type).

      Definition apply ctxt change :=
        apply ctxt (Big_maps (Big_maps.Value_type change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Big_map.Value_type
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Big_map.Value_type.
      #[global] Hint Unfold parse apply : storage_db.
    End Value_type.

    Module Contents.
      Definition parse ctxt :=
        (parse ctxt).(big_maps).(Big_maps.contents).

      Definition apply ctxt change :=
        apply ctxt (Big_maps (Big_maps.Contents change)).

      (* TODO: This is due to Indexed_raw_context.
        The term "Storage.Big_map.Contents" has type
        "Storage_sigs.Non_iterable_indexed_carbonated_data_storage_with_values_with_values"
        while it is expected to have type
        "Storage_sigs.Non_iterable_indexed_carbonated_data_storage_with_values".
      *)
      (* Axiom eq : Non_iterable_indexed_carbonated_data_storage_with_values.Eq.t
        Storage.Big_map.Contents
        (Non_iterable_indexed_carbonated_data_storage_with_values.Make parse apply). *)

      #[global] Opaque Storage.Big_map.Contents.
      #[global] Hint Unfold parse apply : storage_db.
    End Contents.
  End Big_maps.

  Module Block_round.
    Definition parse ctxt :=
      (parse ctxt).(block_round).

    Definition apply ctxt change :=
      apply ctxt (Block_round change).

    Axiom eq : Simple_single_data_storage.Eq.t
      Storage.Block_round
      (Simple_single_data_storage.Make parse apply).

    #[global] Opaque Storage.Block_round.
    #[global] Hint Unfold parse apply : storage_db.
  End Block_round.

  Module Commitments.
    Definition parse ctxt :=
      (parse ctxt).(commitments).

    Definition apply ctxt change :=
      apply ctxt (Commitments change).

    Axiom eq : Indexed_data_storage.Eq.t
      Storage.Commitments
      (Indexed_data_storage.Make axiom parse apply).

    #[global] Opaque Storage.Commitments.
    #[global] Hint Unfold parse apply : storage_db.
  End Commitments.

  Module Contracts.
    Module Global_counter.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.global_counter).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Global_counter change)).

      Axiom eq : Simple_single_data_storage.Eq.t
        Storage.Contract.Global_counter
        (Simple_single_data_storage.Make parse apply).

      #[global] Opaque Storage.Contract.Global_counter.
      #[global] Hint Unfold parse apply : storage_db.
    End Global_counter.

    Module Balance.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.balance).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Balance change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Contract.Spendable_balance
          (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Contract.Spendable_balance.
      #[global] Hint Unfold parse apply : storage_db.
    End Balance.

    Module Missed_endorsements.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.missed_endorsements).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Missed_endorsements change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Contract.Missed_endorsements
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Contract.Missed_endorsements.
      #[global] Hint Unfold parse apply : storage_db.
    End Missed_endorsements.

    Module Manager.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.manager).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Manager change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Contract.Manager
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Contract.Manager.
      #[global] Hint Unfold parse apply : storage_db.
    End Manager.

    Module Delegate.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.delegate).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Delegate change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Contract.Delegate
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).

      #[global] Opaque Storage.Contract.Delegate.
      #[global] Hint Unfold parse apply : storage_db.
    End Delegate.

    Module Inactive_delegate.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.inactive_delegate).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Inactive_delegate change)).

      Axiom eq : Data_set_storage.Eq.t
        Storage.Contract.Inactive_delegate
        (Data_set_storage.Make parse apply).

      #[global] Opaque Storage.Contract.Inactive_delegate.
      #[global] Hint Unfold parse apply : storage_db.
    End Inactive_delegate.

    Module Delegate_desactivation.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.delegate_desactivation).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Delegate_desactivation change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Contract.Delegate_last_cycle_before_deactivation
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Contract.Delegate_last_cycle_before_deactivation.
      #[global] Hint Unfold parse apply : storage_db.
    End Delegate_desactivation.

    Module Delegated.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.delegated).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Delegated change)).
      (* TODO: Fix to use Raw_context.t * Contract_repr.t *)
      (* Axiom eq : Data_set_storage.Eq.t
        Storage.Contract.Delegated
        (Data_set_storage.Make parse apply). *)

      #[global] Opaque Storage.Contract.Delegated.
      #[global] Hint Unfold parse apply : storage_db.
    End Delegated.

    Module Counter.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.counter).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Counter change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Contract.Counter
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).

      #[global] Opaque Storage.Contract.Counter.
      #[global] Hint Unfold parse apply : storage_db.
    End Counter.

    Module Code.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.code).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Code change)).

      Axiom eq :
        Non_iterable_indexed_carbonated_data_storage.Eq.t
          Storage.Contract.Code
          (Non_iterable_indexed_carbonated_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Contract.Code.
      #[global] Hint Unfold parse apply : storage_db.
    End Code.

    Module Storage'.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.storage).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Storage change)).

      Axiom eq :
        Non_iterable_indexed_carbonated_data_storage.Eq.t
          Storage.Contract.Storage
          (Non_iterable_indexed_carbonated_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Contract.Storage.
      #[global] Hint Unfold parse apply : storage_db.
    End Storage'.

    Module Paid_storage_space.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.paid_storage_space).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Paid_storage_space change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Contract.Paid_storage_space
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).
      #[global] Opaque Storage.Contract.Paid_storage_space.
      #[global] Hint Unfold parse apply : storage_db.
    End Paid_storage_space.

    Module Used_storage_space.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.used_storage_space).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Used_storage_space change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Contract.Used_storage_space
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).
      #[global] Opaque Storage.Contract.Used_storage_space.
      #[global] Hint Unfold parse apply : storage_db.
    End Used_storage_space.

    Module Frozen_deposits_limit.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.frozen_deposits_limit).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Frozen_deposits_limit change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Contract.Frozen_deposits_limit
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).

      #[global] Opaque Storage.Contract.Frozen_deposits_limit.
      #[global] Hint Unfold parse apply : storage_db.
    End Frozen_deposits_limit.

    Module Frozen_deposits.
      Definition parse ctxt :=
        (parse ctxt).(contracts).(Contracts.frozen_deposits).

      Definition apply ctxt change :=
        apply ctxt (Contracts (Contracts.Frozen_deposits change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Contract.Frozen_deposits
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).

      #[global] Opaque Storage.Contract.Frozen_deposits.
      #[global] Hint Unfold parse apply : storage_db.
    End Frozen_deposits.
  End Contracts.

  Module Cycles.
    Module Slashed_deposits.
      Definition parse ctxt :=
        (parse ctxt).(cycles).(Cycles.slashed_deposits).

      Definition apply ctxt change :=
        apply ctxt (Cycles (Cycles.Slashed_deposits change)).

      (* TODO *)
      (* Axiom eq : Indexed_data_storage.Eq.t
        Storage.Cycle.Slashed_deposits
        (Indexed_data_storage.Make axiom parse apply). *)

      #[global] Opaque Storage.Cycle.Slashed_deposits.
      #[global] Hint Unfold parse apply : storage_db.
    End Slashed_deposits.

    Module Total_active_stake.
      Definition parse ctxt :=
        (parse ctxt).(cycles).(Cycles.slashed_deposits).

      Definition apply ctxt change :=
        apply ctxt (Cycles (Cycles.Total_active_stake change)).

      (* TODO *)
      (* Axiom eq : Indexed_data_storage.Eq.t
        Storage.Cycle.Total_active_stake
        (Indexed_data_storage.Make axiom parse apply). *)

      #[global] Opaque Storage.Cycle.Total_active_stake.
      #[global] Hint Unfold parse apply : storage_db.
    End Total_active_stake.

    Module Delegate_sampler_state.
      Definition parse ctxt :=
        (parse ctxt).(cycles).(Cycles.slashed_deposits).

      Definition apply ctxt change :=
        apply ctxt (Cycles (Cycles.Delegate_sampler_state change)).

      (* TODO *)
      (* Axiom eq : Indexed_data_storage.Eq.t
        Storage.Cycle.Delegate_sampler_state
        (Indexed_data_storage.Make axiom parse apply). *)

      #[global] Opaque Storage.Cycle.Delegate_sampler_state.
      #[global] Hint Unfold parse apply : storage_db.
    End Delegate_sampler_state.
  End Cycles.

  Module Delegates.
    Definition parse ctxt :=
      (parse ctxt).(delegates).

    Definition apply ctxt change :=
      apply ctxt (Delegates change).

    Axiom eq : Data_set_storage.Eq.t
      Storage.Delegates
      (Data_set_storage.Make parse apply).

    #[global] Opaque Storage.Delegates.
    #[global] Hint Unfold parse apply : storage_db.
  End Delegates.

  Module Global_constants.
    Module Map.
      Definition parse ctxt :=
        (parse ctxt).(global_constants).(Global_constants.map).

      Definition apply ctxt change :=
        apply ctxt (Global_constants (Global_constants.Map change)).

      Axiom eq :
        Non_iterable_indexed_carbonated_data_storage.Eq.t
          Storage.Global_constants.Map
          (Non_iterable_indexed_carbonated_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Global_constants.Map.
      #[global] Hint Unfold parse apply : storage_db.
    End Map.
  End Global_constants.

  Module Liquidity_baking.
    Module Toggle_ema.
      Definition parse ctxt :=
        (parse ctxt).(liquidity_baking).(Liquidity_baking.toggle_ema).

      Definition apply ctxt change :=
        apply ctxt (Liquidity_baking (Liquidity_baking.Toggle_ema change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Liquidity_baking.Toggle_ema
        (Single_data_storage.Make parse apply ["liquidity_baking";"toggle_ema"]).

      #[global] Opaque Storage.Liquidity_baking.Toggle_ema.
      #[global] Hint Unfold parse apply : storage_db.
    End Toggle_ema.

    Module Cpmm_address.
      Definition parse ctxt :=
        (parse ctxt).(liquidity_baking).(Liquidity_baking.cpmm_address ).

      Definition apply ctxt change :=
        apply ctxt (Liquidity_baking (Liquidity_baking.Cpmm_address change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Liquidity_baking.Cpmm_address
        (Single_data_storage.Make parse apply ["liquidity_baking";"cpmm_address "]).

      #[global] Opaque Storage.Liquidity_baking.Cpmm_address.
      #[global] Hint Unfold parse apply : storage_db.
    End Cpmm_address.
  End Liquidity_baking.

  Module Pending_migrations.
    Module Balance_updates.
      Definition parse ctxt :=
        (parse ctxt).(pending_migrations).(Pending_migrations.balance_updates).

      Definition apply ctxt change :=
        apply ctxt (Pending_migrations (Pending_migrations.Balance_updates change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Pending_migration.Balance_updates
        (Single_data_storage.Make parse apply ["pending_migrations";"balance_updates"]).

      #[global] Opaque Storage.Pending_migration.Balance_updates.
      #[global] Hint Unfold parse apply : storage_db.
    End Balance_updates.

    Module Operation_results.
      Definition parse ctxt :=
        (parse ctxt).(pending_migrations).(Pending_migrations.operation_results ).

      Definition apply ctxt change :=
        apply ctxt (Pending_migrations (Pending_migrations.Operation_results change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Pending_migration.Operation_results
        (Single_data_storage.Make parse apply ["pending_migrations";"operation_results "]).

      #[global] Opaque Storage.Pending_migration.Operation_results.
      #[global] Hint Unfold parse apply : storage_db.
    End Operation_results.
  End Pending_migrations.

  Module Ramp_up.
    Module Rewards.
      Definition parse ctxt :=
        (parse ctxt).(ramp_up).(Ramp_up.rewards).

      Definition apply ctxt change :=
        apply ctxt (Ramp_up (Ramp_up.Rewards change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Ramp_up.Rewards
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).

      #[global] Opaque Storage.Ramp_up.Rewards.
      #[global] Hint Unfold parse apply : storage_db.
    End Rewards.
  End Ramp_up.

  Module Sapling.
    Module Next.
      Definition parse ctxt :=
        (parse ctxt).(sapling).(Sapling.next).

      Definition apply ctxt change :=
        apply ctxt (Sapling (Sapling.Next change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Sapling.Next.Storage
        (Single_data_storage.Make parse apply ["sapling"; "next"]).

      #[global] Opaque Storage.Sapling.Next.Storage.
      #[global] Hint Unfold parse apply : storage_db.
    End Next.

    Module Total_bytes.
      Definition parse ctxt :=
        (parse ctxt).(sapling).(Sapling.total_bytes).

      Definition apply ctxt change :=
        apply ctxt (Sapling (Sapling.Total_bytes change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Sapling.Total_bytes
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Sapling.Total_bytes.
      #[global] Hint Unfold parse apply : storage_db.
    End Total_bytes.

    Module Commitments_size.
      Definition parse ctxt :=
        (parse ctxt).(sapling).(Sapling.commitments_size).

      Definition apply ctxt change :=
        apply ctxt (Sapling (Sapling.Commitments_size change)).

      (* TODO *)
      (* Axiom eq : Single_data_storage.Eq.t
        Storage.Sapling.Commitments_size
        (Single_data_storage.Make parse apply ["sapling"; "commitments_size"]). *)

      #[global] Opaque Storage.Sapling.Commitments_size.
      #[global] Hint Unfold parse apply : storage_db.
    End Commitments_size.

    Module Memo_size.
      Definition parse (ctxt : (Raw_context.t × int64)) :=
        (parse (fst ctxt)).(sapling).(Sapling.nullifiers_size).

      Definition apply (ctxt : (Raw_context.t × int64))
          (change : Single_data_storage.Change.t int64) :=
        apply (fst ctxt) (Sapling (Sapling.Nullifiers_size change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Sapling.Memo_size
        (Single_data_storage.Make parse apply ["sapling"; "memo_size"]).

      #[global] Opaque Storage.Sapling.Memo_size.
      #[global] Hint Unfold parse apply : storage_db.
    End Memo_size.

    Module Commitments.
      Definition parse ctxt :=
        (parse ctxt).(sapling).(Sapling.commitments).

      Definition apply ctxt change :=
        apply ctxt (Sapling (Sapling.Commitments change)).

      (* TODO *)
      (* Axiom eq : Non_iterable_indexed_carbonated_data_storage.Eq.t
        Storage.Sapling.Commitments
        (Non_iterable_indexed_carbonated_data_storage.Make parse apply). *)

      #[global] Opaque Storage.Sapling.Commitments.
      #[global] Hint Unfold parse apply : storage_db.
    End Commitments.

    Module Ciphertexts.
      Definition parse (arg : Raw_context.t × int64) :=
        (parse (fst arg)).(sapling).(Sapling.ciphertexts).

      Definition apply (arg : Raw_context.t × int64) change :=
        apply (fst arg) (Sapling (Sapling.Ciphertexts change)).

      Axiom eq : Non_iterable_indexed_carbonated_data_storage.Eq.t
        Storage.Sapling.Ciphertexts
        (Non_iterable_indexed_carbonated_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Sapling.Ciphertexts.
      #[global] Hint Unfold parse apply : storage_db.
    End Ciphertexts.

    Module Nullifiers_size.
      Definition parse (ctxt : (Raw_context.t × int64)) :=
        (parse (fst ctxt)).(sapling).(Sapling.nullifiers_size).

      Definition apply (ctxt : (Raw_context.t × int64))
          (change : Single_data_storage.Change.t int64) :=
        apply (fst ctxt) (Sapling (Sapling.Nullifiers_size change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Sapling.Nullifiers_size
        (Single_data_storage.Make parse apply ["sapling"; "nullifiers_size"]).

      #[global] Opaque Storage.Sapling.Nullifiers_size.
      #[global] Hint Unfold parse apply : storage_db.
    End Nullifiers_size.

    Module Nullifiers_ordered.
      Definition parse (ctxt : (Raw_context.t × Storage.Sapling.id)) :=
        (parse (fst ctxt)).(sapling).(Sapling.nullifiers_ordered).

      Definition apply (ctxt : (Raw_context.t × Storage.Sapling.id))
          (change : _) :=
        apply (fst ctxt) (Sapling (Sapling.Nullifiers_ordered change)).

      Axiom eq : Non_iterable_indexed_data_storage.Eq.t
        Storage.Sapling.Nullifiers_ordered
        (Non_iterable_indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Sapling.Nullifiers_ordered.
      #[global] Hint Unfold parse apply : storage_db.
    End Nullifiers_ordered.

    Module Nullifiers_hashed.
      Definition parse ctxt :=
        (parse ctxt).(sapling).(Sapling.nullifiers_hashed).

      Definition apply ctxt change :=
        apply ctxt (Sapling (Sapling.Nullifiers_hashed change)).

      (* TODO *)
      (* Axiom eq : Carbonated_data_set_storage.Eq.t
        Storage.Sapling.Nullifiers_hashed
        (Carbonated_data_set_storage.Make parse apply). *)

      #[global] Opaque Storage.Sapling.Nullifiers_hashed.
      #[global] Hint Unfold parse apply : storage_db.
    End Nullifiers_hashed.

    Module Roots.
      Definition parse (ctxt : Raw_context.t × Storage.Sapling.id) :=
        (parse (fst ctxt)).(sapling).(Sapling.roots).

      Definition apply (ctxt : Raw_context.t × Storage.Sapling.id) change :=
        apply (fst ctxt) (Sapling (Sapling.Roots change)).

      Axiom eq : Non_iterable_indexed_data_storage.Eq.t
        Storage.Sapling.Roots
        (Non_iterable_indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Sapling.Roots.
      #[global] Hint Unfold parse apply : storage_db.
    End Roots.

    Module Roots_pos.
      Definition parse (ctxt : Raw_context.t × int32) :=
        (parse (fst ctxt)).(sapling).(Sapling.roots_pos).

      Definition apply (ctxt : Raw_context.t × int32) change :=
        apply (fst ctxt) (Sapling (Sapling.Roots_pos change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Sapling.Roots_pos
        (Single_data_storage.Make parse apply ["sapling"; "roots_pos"]).

      #[global] Opaque Storage.Sapling.Roots_pos.
      #[global] Hint Unfold parse apply : storage_db.
    End Roots_pos.

    Module Roots_level.
      Definition parse (ctxt : Raw_context.t × int32) :=
        (parse (fst ctxt)).(sapling).(Sapling.roots_level).

      Definition apply (ctxt : Raw_context.t × int32) change :=
        apply (fst ctxt) (Sapling (Sapling.Roots_level change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Sapling.Roots_level
        (Single_data_storage.Make parse apply ["sapling"; "roots_level"]).

      #[global] Opaque Storage.Sapling.Roots_level.
      #[global] Hint Unfold parse apply : storage_db.
    End Roots_level.
  End Sapling.

  Module Sc_rollup.
    Module PVM_kind.
      Definition parse ctxt :=
        (parse ctxt).(sc_rollup).(Sc_rollup.pvm_kind).

      Definition apply ctxt change :=
        apply ctxt (Sc_rollup (Sc_rollup.PVM_kind change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Sc_rollup.PVM_kind
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Sc_rollup.PVM_kind.
      #[global] Hint Unfold parse apply : storage_db.
    End PVM_kind.

    Module Boot_sector.
      Definition parse ctxt :=
        (parse ctxt).(sc_rollup).(Sc_rollup.boot_sector).

      Definition apply ctxt change :=
        apply ctxt (Sc_rollup (Sc_rollup.Boot_sector change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Sc_rollup.Boot_sector
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Sc_rollup.Boot_sector.
      #[global] Hint Unfold parse apply : storage_db.
    End Boot_sector.

    Module Inbox.
      Definition parse ctxt :=
        (parse ctxt).(sc_rollup).(Sc_rollup.inbox).

      Definition apply ctxt change :=
        apply ctxt (Sc_rollup (Sc_rollup.Inbox change)).

      Axiom eq :
        Non_iterable_indexed_carbonated_data_storage.Eq.t
          Storage.Sc_rollup.Inbox
          (Non_iterable_indexed_carbonated_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Sc_rollup.Inbox.
      #[global] Hint Unfold parse apply : storage_db.
    End Inbox.
  End Sc_rollup.

  Module Seeds.
    Module Nonce.
      Definition parse ctxt :=
        (parse ctxt).(seeds).(Seeds.nonce).

      Definition apply ctxt change :=
        apply ctxt (Seeds (Seeds.Nonce change)).

      Axiom eq : Non_iterable_indexed_data_storage.Eq.t
        Storage.Seed.Nonce
        (Non_iterable_indexed_data_storage.Make absolute_key parse apply).

      #[global] Opaque Storage.Seed.Nonce.
      #[global] Hint Unfold parse apply : storage_db.
    End Nonce.

    Module For_cycle.
      Definition parse ctxt :=
        (parse ctxt).(seeds).(Seeds.for_cycle).

      Definition apply ctxt change :=
        apply ctxt (Seeds (Seeds.For_cycle change)).

      Axiom eq : ∀ (absolute_key : Context.key), @For_cycle.Eq.t
        Storage.Seed.For_cycle
        (For_cycle.Make absolute_key parse apply).

      #[global] Opaque Storage.Seed.For_cycle.
      #[global] Hint Unfold parse apply : storage_db.
    End For_cycle.
  End Seeds.

  Module Stakes.
    Module Staking_balance.
      Definition parse ctxt :=
        (parse ctxt).(stakes).(Stakes.staking_balance).

      Definition apply ctxt change :=
        apply ctxt (Stakes (Stakes.Staking_balance change)).

      (* TODO *)
      (* Axiom eq : Indexed_data_snapshotable_storage.Eq.t
        Storage.Stake.Staking_balance
        (Indexed_data_snapshotable_storage.Make parse apply). *)

      #[global] Opaque Storage.Stake.Staking_balance.
      #[global] Hint Unfold parse apply : storage_db.
    End Staking_balance.

    Module Active_delegate_with_one_roll.
      Definition parse ctxt :=
        (parse ctxt).(stakes).(Stakes.active_delegate_with_one_roll).

      Definition apply ctxt change :=
        apply ctxt (Stakes (Stakes.Active_delegate_with_one_roll change)).

      (* TODO *)
      (* Axiom eq : Indexed_data_snapshotable_storage.Eq.t
        Storage.Stake.Active_delegate_with_one_roll
        (Indexed_data_snapshotable_storage.Make parse apply). *)

      #[global] Opaque Storage.Stake.Active_delegate_with_one_roll.
      #[global] Hint Unfold parse apply : storage_db.
    End Active_delegate_with_one_roll.

    Module Selected_distribution_for_cycle.
      Definition parse ctxt :=
        (parse ctxt).(stakes).(Stakes.selected_distribution_for_cycle).

      Definition apply ctxt change :=
        apply ctxt (Stakes (Stakes.Selected_distribution_for_cycle change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Stake.Selected_distribution_for_cycle
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Stake.Selected_distribution_for_cycle.
      #[global] Hint Unfold parse apply : storage_db.
    End Selected_distribution_for_cycle.

    Module Last_snapshot.
      Definition parse ctxt :=
        (parse ctxt).(stakes).(Stakes.last_snapshot).

      Definition apply ctxt change :=
        apply ctxt (Stakes (Stakes.Last_snapshot change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Stake.Last_snapshot
        (Single_data_storage.Make parse apply ["stakes";"last_snapshot"]).

      #[global] Opaque Storage.Stake.Last_snapshot.
      #[global] Hint Unfold parse apply : storage_db.
    End Last_snapshot.
  End Stakes.

  Module Tenderbake.
    Module First_level_legacy.
      Definition parse ctxt :=
        (parse ctxt).(tenderbake).(Tenderbake.first_level_legacy).

      Definition apply ctxt change :=
        apply ctxt (Tenderbake (Tenderbake.First_level_legacy change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Tenderbake.First_level_legacy
        (Single_data_storage.Make parse apply ["tenderbake"; "first_level_legacy"]).

      #[global] Opaque Storage.Tenderbake.First_level_legacy.
      #[global] Hint Unfold parse apply : storage_db.
    End First_level_legacy.

    Module Endorsement_branch.
      Definition parse ctxt :=
        (parse ctxt).(tenderbake).(Tenderbake.endorsement_branch).

      Definition apply ctxt change :=
        apply ctxt (Tenderbake (Tenderbake.Endorsement_branch change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Tenderbake.Endorsement_branch
        (Single_data_storage.Make parse apply ["tenderbake"; "endorsement_branch"]).

      #[global] Opaque Storage.Tenderbake.Endorsement_branch.
      #[global] Hint Unfold parse apply : storage_db.
    End Endorsement_branch.

    Module Grand_parent_branch.
      Definition parse ctxt :=
        (parse ctxt).(tenderbake).(Tenderbake.grand_parent_branch).

      Definition apply ctxt change :=
        apply ctxt (Tenderbake (Tenderbake.Grand_parent_branch change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Tenderbake.Grand_parent_branch
        (Single_data_storage.Make parse apply ["tenderbake"; "grand_parent_branch"]).

      #[global] Opaque Storage.Tenderbake.Grand_parent_branch.
      #[global] Hint Unfold parse apply : storage_db.
    End Grand_parent_branch.
  End Tenderbake.

  Module Tickets_balance.
    Module Table.
      Definition parse ctxt :=
        (parse ctxt).(tickets_balance).(Tickets_balance.table).

      Definition apply ctxt change :=
        apply ctxt (Tickets_balance (Tickets_balance.Table change)).

      Axiom eq :
        Non_iterable_indexed_carbonated_data_storage.Eq.t
          Storage.Ticket_balance.Table
          (Non_iterable_indexed_carbonated_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Ticket_balance.Table.
      #[global] Hint Unfold parse apply : storage_db.
    End Table.
  End Tickets_balance.

  Module Tx_rollup.
    Module State.
      Definition parse ctxt :=
        (parse ctxt).(tx_rollup).(Tx_rollup.tx_state).

      Definition apply ctxt change :=
        apply ctxt (Tx_rollup (Tx_rollup.Tx_state change)).

      Axiom eq :
        Non_iterable_indexed_carbonated_data_storage.Eq.t
          Storage.Tx_rollup.State
          (Non_iterable_indexed_carbonated_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Tx_rollup.State.
      #[global] Hint Unfold parse apply : storage_db.
    End State.
  End Tx_rollup.

  Module Votes.
    Module Pred_period_kind.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.pred_period_kind).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Pred_period_kind change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Vote.Pred_period_kind
        (Single_data_storage.Make parse apply ["votes"; "pred_period_kind"]).

      #[global] Opaque Storage.Vote.Pred_period_kind.
      #[global] Hint Unfold parse apply : storage_db.
    End Pred_period_kind.

    Module Current_period.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.current_period).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Current_period change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Vote.Current_period
        (Single_data_storage.Make parse apply ["votes"; "current_period"]).

      #[global] Opaque Storage.Vote.Current_period.
      #[global] Hint Unfold parse apply : storage_db.
    End Current_period.

    Module Current_proposal.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.current_proposal).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Current_proposal change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Vote.Current_proposal
        (Single_data_storage.Make parse apply ["votes"; "current_proposal"]).

      #[global] Opaque Storage.Vote.Current_proposal.
      #[global] Hint Unfold parse apply : storage_db.
    End Current_proposal.

    Module Participation_ema.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.participation_ema).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Participation_ema change)).

      Axiom eq : Single_data_storage.Eq.t
        Storage.Vote.Participation_ema
        (Single_data_storage.Make parse apply ["votes"; "participation_ema"]).

      #[global] Opaque Storage.Vote.Participation_ema.
      #[global] Hint Unfold parse apply : storage_db.
    End Participation_ema.

    Module Listings_size.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.listings_size).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Listings_size change)).

      (* Axiom eq : Single_data_storage.Eq.t *)
      (*   Storage.Vote.Listings_size *)
      (*   (Single_data_storage.Make parse apply ["votes"; "listings_size"]). *)

      (* #[global] Opaque Storage.Vote.Listings_size. *)
      #[global] Hint Unfold parse apply : storage_db.
    End Listings_size.

    Module Listings.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.listings).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Listings change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Vote.Listings
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Vote.Listings.
      #[global] Hint Unfold parse apply : storage_db.
    End Listings.

    Module Proposals.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.proposals).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Proposals change)).

      Axiom eq : Data_set_storage.Eq.t
        Storage.Vote.Proposals
        (Data_set_storage.Make parse apply).

      #[global] Opaque Storage.Vote.Proposals.
      #[global] Hint Unfold parse apply : storage_db.
    End Proposals.

    Module Proposals_count.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.proposals_count).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Proposals_count change)).

      Axiom eq :
        Indexed_data_storage.Eq.t
          Storage.Vote.Proposals_count
          (Indexed_data_storage.Make parametrized_absolute_key parse apply).
      #[global] Opaque Storage.Vote.Proposals_count.
      #[global] Hint Unfold parse apply : storage_db.
    End Proposals_count.

    Module Ballots.
      Definition parse ctxt :=
        (parse ctxt).(votes).(Votes.ballots).

      Definition apply ctxt change :=
        apply ctxt (Votes (Votes.Ballots change)).

      Axiom eq : Indexed_data_storage.Eq.t
        Storage.Vote.Ballots
        (Indexed_data_storage.Make axiom parse apply).

      #[global] Opaque Storage.Vote.Ballots.
      #[global] Hint Unfold parse apply : storage_db.
    End Ballots.
  End Votes.
End Eq.