Skip to main content

🖼️ Raw_context.v

Proofs

See code, See simulations, Gitlab , OCaml

Predicates for a [Single_data_storage.t _] type
The store is empty
  Definition empty {a : Set}
    (store : Storage_sigs.Single_data_storage.t a) : Prop :=
    store = None.
  Arguments empty _ /.
End Single_data_storage.

Predicates for a [Indexed_data_storage _ _] type
The key exists in the context
  Definition key_exists {k v : Set}
    {index : Path_encoding.S}
    (key : k)
    (map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
    : Prop :=
    (Storage_sigs.Indexed_map.Map index).(Map.S.mem) key map = true.
  Arguments key_exists _ _ _ /.

The value [value] with key [key] exists in the map and satisfies the given property [P].
  Definition value_exists {k v : Set}
    {index : Path_encoding.S}
    (P : v Prop)
    (key : k)
    (map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
    : Prop :=
    match (Storage_sigs.Indexed_map.Map index).(Map.S.find) key map with
    | Some valueP value
    | NoneFalse
    end.
  Arguments value_exists _ _ _ /.

If value [value] with key [key] exists in the map, then it satisfies the given the property [P].
  Definition if_value_exists {k v : Set}
    {index : Path_encoding.S}
    (P : v Prop)
    (key : k)
    (map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
    : Prop :=
    match (Storage_sigs.Indexed_map.Map index).(Map.S.find) key map with
    | Some valueP value
    | NoneTrue
    end.
  Arguments if_value_exists _ _ _ /.

[value_exists] implies [if_value_exits]
  Lemma exists_impl_if_exists {k v : Set}
    {index : Path_encoding.S (t := k)}
    (P : v Prop)
    (key : k)
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index) v) :
    value_exists P key map
    if_value_exists P key map.
  Proof.
    simpl in ×.
    now match goal with
    | |- match ?a with __ end match ?b with __ end
        change b with a; destruct a; simpl; [|contradiction]
    end.
  Qed.
End Indexed_data_storage.

Module Nested_indexed_data_storage.
The key and subkey exists in the context
  Definition key_exists {k k' v : Set}
    {index : Path_encoding.S (t := k)}
    {index' : Path_encoding.S (t := k')}
    (key : k) (subkey : k')
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
    : Prop :=
    Indexed_data_storage.value_exists
      (fun submap
         Indexed_data_storage.key_exists subkey submap)
      key map.
  Arguments key_exists _ _ _ /.

This is like [Indexed_data_storage.value_exists] but for nested maps. A value of type [v] exists with [key] and [subkey], and satisfies the given property [P]
  Definition value_exists {k k' v : Set}
    {index : Path_encoding.S (t := k)}
    {index' : Path_encoding.S (t := k')}
    (P : v Prop)
    (key : k) (subkey : k')
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
    : Prop :=
    Raw_context.Indexed_data_storage.value_exists
      (fun submap
         Raw_context.Indexed_data_storage.value_exists
           (fun valueP value) subkey submap)
      key map.
  Arguments value_exists _ _ _ _ /.

If the value [value] with key [key] and subkey [subkey] exists in the map and submap, then it satisfies the given the property [P].
  Definition if_value_exists {k k' v : Set}
    {index : Path_encoding.S (t := k)}
    {index' : Path_encoding.S (t := k')}
    (P : v Prop)
    (key : k) (subkey : k')
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
    : Prop :=
    Raw_context.Indexed_data_storage.if_value_exists
      (fun submap
         Raw_context.Indexed_data_storage.if_value_exists
           (fun valueP value) subkey submap)
      key map.
  Arguments if_value_exists _ _ _ _ /.

If a value exists, then a key also exists
  Lemma value_exists_impl_key_exists {k k' v : Set}
    {index : Path_encoding.S (t := k)}
    {index' : Path_encoding.S (t := k')}
    (P : v Prop)
    (key : k) (subkey : k')
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
    value_exists P key subkey map
    key_exists key subkey map.
  Proof.
    simpl.
    match goal with
    | |- match ?a with __ end match ?b with __ end
        change b with a; destruct a; simpl; [|contradiction]
    end.
    step; [|easy].
    apply Map.find_mem_eq in Heqo.
    intros _. easy.
  Qed.

If key exists then a value exists and it satisfies some unspecified property [P]
  Lemma key_exists_impl_value_exists {k k' v : Set}
    {index : Path_encoding.S (t := k)}
    {index' : Path_encoding.S (t := k')}
    (key : k) (subkey : k')
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
    key_exists key subkey map
     P, value_exists P key subkey map.
  Proof.
    simpl. intros H. eexists.
    match type of H with
    | match ?a with __ end
        match goal with
        | |- match ?b with __ end
        change b with a; destruct a; simpl; [|contradiction]
        end
    end.
    step.
    { instantiate (1 := fun _True). simpl. trivial. }
    { apply Map.find_eq_none_implies_mem_eq_false in Heqo.
      match goal with
      | H : ?a subkey m = true,
        H' : ?b subkey m = false |- _
          change b with a in H'; rewrite H' in H;
          discriminate
      end.
    }
  Qed.

If you have a [key_exists k k' m] and a [if_value_exists P k k' m] you can deduce [value_exists P k k' m]
  Lemma key_exists_and_if_value_exists_impl_value_exists {k k' v : Set}
    {index : Path_encoding.S (t := k)}
    {index' : Path_encoding.S (t := k')}
    (key : k) (subkey : k') (P : v Prop)
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
    key_exists key subkey map
    if_value_exists P key subkey map
    value_exists P key subkey map.
  Proof.
    simpl.
    step; cbn; [|easy].
    intros H_mem.
    step; cbn; [easy|].
    apply Map.find_eq_none_implies_mem_eq_false in Heqo0.
    match type of H_mem with
    | ?a subkey m = true
      match type of Heqo0 with
      | ?b subkey m = false
        change b with a in *;
        now rewrite H_mem in Heqo0
      end
    end.
  Qed.

[value_exists] implies [if_value_exists]
  Lemma exists_impl_if_exists {k k' v : Set}
    {index : Path_encoding.S (t := k)}
    {index' : Path_encoding.S (t := k')}
    (P : v Prop)
    (key : k) (subkey : k')
    (map :
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
    value_exists P key subkey map
    if_value_exists P key subkey map.
  Proof.
    simpl in ×.
    match goal with
    | |- match ?a with __ end match ?b with __ end
        change b with a; destruct a; simpl; [|contradiction]
    end.
    now step.
  Qed.
End Nested_indexed_data_storage.

Module Tenderbake.
  Import Raw_context.

Validity for the [Tenderbake] sub-store.
  Module Valid.
    Record t (x : Raw_context.t) : Prop := {
      First_level_of_protocol : x.(Tenderbake_First_level_of_protocol) None;
    }.
  End Valid.
End Tenderbake.

Module Vote.
  Import Raw_context.

Validity for the [Vote] sub-store.
  Module Valid.
    Record t (x : Raw_context.t) : Prop := {
      Current_period :
        match x.(Vote_Current_period) with
        | Some periodVoting_period_repr.Valid.t period
        | NoneFalse
        end;
      Pred_period_kind : x.(Vote_Pred_period_kind) None;
    }.
  End Valid.
End Vote.

Module Sc_rollup_Commitment_added.
  Import Raw_context_generated.

If a [commitment : Sc_rollup_commitment_repr.V1.t] exists in the context, then it is valid
  Module Valid.
    Definition t
      (commitment_added_projection : Storage_sigs.Indexed_map.t
      (of_description_index Sc_rollup_repr.Index)
      (Storage_sigs.Indexed_data_storage.t
        Sc_rollup_commitment_repr.Hash.Path_encoding_Make_hex_include
        Raw_level_repr.t))
      : Prop :=
       rollup index,
        Nested_indexed_data_storage.if_value_exists
          Raw_level_repr.Valid.t rollup index
          commitment_added_projection.
  End Valid.
End Sc_rollup_Commitment_added.

Module Sc_rollup_Commitments.
  Import Raw_context_generated.

If a [commitment : Sc_rollup_commitment_repr.V1.t] exists in the context, then it is valid
  Module Valid.
    Definition t
      (commitment_projection : Storage_sigs.Indexed_map.t
        (of_description_index Sc_rollup_repr.Index)
        (Storage_sigs.Indexed_data_storage.t
          Sc_rollup_commitment_repr.Hash.Path_encoding_Make_hex_include
          Sc_rollup_commitment_repr.t))
      : Prop :=
       rollup index,
        Nested_indexed_data_storage.if_value_exists
          Sc_rollup_commitment_repr.V1.Valid.t rollup index
          commitment_projection.
  End Valid.
End Sc_rollup_Commitments.

Module Sc_rollup_Game.
  Import Raw_context_generated.

If a [game : Sc_rollup_game_repr.t] exists in the context, then it is valid
  Module Valid.
    Definition t
      (game_projection : Storage_sigs.Indexed_map.t
        (of_description_index Sc_rollup_repr.Index)
        (Storage_sigs.Indexed_data_storage.t
          (of_functors_index
             Sc_rollup_Game_versioned_and_timeout_Index)
          Sc_rollup_game_repr.t))
      : Prop :=
         rollup index,
          Nested_indexed_data_storage.if_value_exists
            Sc_rollup_game_repr.V1.Valid.t
            rollup
            index
            game_projection.
  End Valid.
End Sc_rollup_Game.

Module Sc_rollup_Game_timeout.
  Import Raw_context_generated.

If [game_timeout : Sc_rollup_game_repr.timeout] exists in the context, then it valid
  Module Valid.
    Definition t
      (game_timeout_projection : Storage_sigs.Indexed_map.t
        (of_description_index Sc_rollup_repr.Index)
        (Storage_sigs.Indexed_data_storage.t
          (of_functors_index
             Sc_rollup_Game_versioned_and_timeout_Index)
          Sc_rollup_game_repr.timeout))
      : Prop :=
         rollup index,
          Nested_indexed_data_storage.if_value_exists
            Sc_rollup_game_repr.timeout.Valid.t
            rollup
            index
            game_timeout_projection.
  End Valid.
End Sc_rollup_Game_timeout.

Reading a value from the empty context always return [None].
Axiom find_empty_context : (k : key),
  Context.find Raw_context.empty_context k = None.

#[local] Open Scope list.

Module consensus_pk.
  Module Valid.
    Import Proto_alpha.Raw_context.consensus_pk.

Validity predicate for [consensus_pk].
    Record t (x : Raw_context.consensus_pk) : Prop := {
      consensus_pkh :
        x.(consensus_pkh) =
        Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
          x.(consensus_pk);
    }.
  End Valid.
End consensus_pk.

The encoding [consensus_pk_encoding] is valid.
Lemma consensus_pk_encoding_is_valid :
  Data_encoding.Valid.t consensus_pk.Valid.t Raw_context.consensus_pk_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros [] []; simpl in ×.
  step.
  { assert (consensus_pkh = delegate). {
      destruct Signature.Included_SIGNATURE_is_valid.
      destruct Public_key_hash.
      destruct Compare_S0.
      destruct is_Make.
      rewrite equal in Heqb; simpl in Heqb.
      apply Signature.Included_SIGNATURE_is_valid; trivial; simpl.
      lia.
    }
    sfirstorder.
  }
  { sfirstorder. }
Qed.
#[global] Hint Resolve consensus_pk_encoding_is_valid : Data_encoding_db.

Module Raw_consensus.
Validity predicate for [Raw_consensus.t].
  Module Valid.
    Import Raw_context.Raw_consensus.t.

    Record t (x : Raw_context.Raw_consensus.t) : Prop := {
      current_endorsement_power :
      Pervasives.Int.Valid.t x.(current_endorsement_power);
      locked_round_evidence :
        Option.Forall
          (fun '(round, power)
            Round_repr.Valid.t round Pervasives.Int.Valid.t power
          )
          x.(locked_round_evidence);
      preendorsements_quorum_round :
        Option.Forall Round_repr.Valid.t x.(preendorsements_quorum_round);
    }.
  End Valid.

The function [initialize_with_endorsements_and_preendorsements] is valid.
  Lemma initialize_with_endorsements_and_preendorsements_is_valid
    allowed_endorsements allowed_preendorsements t_value
    (H_t_value : Valid.t t_value) :
    Valid.t (
      Raw_context.Raw_consensus.initialize_with_endorsements_and_preendorsements
        allowed_endorsements allowed_preendorsements t_value
    ).
  Proof.
    sauto lq: on.
  Qed.
End Raw_consensus.

Module config.
  Module Valid.
    Import Simulations.Raw_context_aux.config.

Validity predicate for the simulation of [Raw_context.back].
The validity predicate for the [Simulations.Raw_context.standalone] type
  Module Valid.
    Import Simulations.Raw_context_aux.standalone.

    Record simulation (x : Simulations.Raw_context_aux.standalone) : Prop := {
      cycle_eras : Level_repr.Cycle_eras.Valid.t x.(cycle_eras);
      constants : Constants_parametric_repr.Valid.t x.(constants);
      protocol_param :
        Option.Forall Parameters_repr.Valid.t x.(protocol_param);
    }.
  End Valid.
End standalone.

The validity predicate for the [Simulations.Raw_context.t] type
Validity predicate for [Raw_context.t] with a specific domain.
  Definition on (domain : Simulations.Raw_context.t Prop)
    (ctxt : Proto_alpha.Raw_context.t) : Prop :=
     sim_ctxt : Simulations.Raw_context.t,
    ctxt = Raw_context.to_t sim_ctxt
    simulation sim_ctxt
    domain sim_ctxt.

Validity predicate for [Raw_context.t].
  Definition t (ctxt : Proto_alpha.Raw_context.t) : Prop :=
    on (fun _True) ctxt.

Open the validity hypothesis about a context and do some rewrites.
  Ltac destruct_rewrite H :=
    let sim_ctxt := fresh "sim_ctxt" in
    let H_sim_ctxt_eq := fresh "H_sim_ctxt_eq" in
    let H_sim_ctxt := fresh "H_sim_ctxt" in
    let H_sim_ctxt_domain := fresh "H_sim_ctxt_domain" in
    let H_eq := fresh "H_eq" in
    (* We use [eqn:] to keep the hypothesis [H] alive *)
    destruct H
      as [sim_ctxt [H_sim_ctxt_eq [H_sim_ctxt H_sim_ctxt_domain]]] eqn:H_eq;
    clear H_eq;
    rewrite H_sim_ctxt_eq in ×.
End Valid.

A lemma to help find a simulation from a raw context.
Lemma to_t_inversion
  remaining_operation_gas standalone constants round_durations
  cycle_eras level predecessor_timestamp timestamp fees origination_nonce
  temporary_lazy_storage_ids internal_nonce internal_nonces_used
  remaining_block_gas unlimited_operation_gas consensus
  non_consensus_operations_rev dictator_proposal_seen sampler_state
  stake_distribution_for_current_cycle tx_rollup_current_messages
  sc_rollup_current_messages dal_slot_fee_market dal_attestation_slot_accountability
  dal_committee sim_ctxt :
  {|
    Proto_alpha.Raw_context.t.remaining_operation_gas :=
      remaining_operation_gas;
    Proto_alpha.Raw_context.t.back :=
      {|
        Proto_alpha.Raw_context.back.context := Raw_context.to_context standalone;
        Proto_alpha.Raw_context.back.constants := constants;
        Proto_alpha.Raw_context.back.round_durations := round_durations;
        Proto_alpha.Raw_context.back.cycle_eras := cycle_eras;
        Proto_alpha.Raw_context.back.level := level;
        Proto_alpha.Raw_context.back.predecessor_timestamp :=
          predecessor_timestamp;
        Proto_alpha.Raw_context.back.timestamp := timestamp;
        Proto_alpha.Raw_context.back.fees := fees;
        Proto_alpha.Raw_context.back.origination_nonce := origination_nonce;
        Proto_alpha.Raw_context.back.temporary_lazy_storage_ids :=
          temporary_lazy_storage_ids;
        Proto_alpha.Raw_context.back.internal_nonce := internal_nonce;
        Proto_alpha.Raw_context.back.internal_nonces_used :=
          internal_nonces_used;
        Proto_alpha.Raw_context.back.remaining_block_gas := remaining_block_gas;
        Proto_alpha.Raw_context.back.unlimited_operation_gas :=
          unlimited_operation_gas;
        Proto_alpha.Raw_context.back.consensus := consensus;
        Proto_alpha.Raw_context.back.non_consensus_operations_rev :=
          non_consensus_operations_rev;
        Proto_alpha.Raw_context.back.dictator_proposal_seen :=
          dictator_proposal_seen;
        Proto_alpha.Raw_context.back.sampler_state := sampler_state;
        Proto_alpha.Raw_context.back.stake_distribution_for_current_cycle :=
          stake_distribution_for_current_cycle;
        Proto_alpha.Raw_context.back.tx_rollup_current_messages :=
          tx_rollup_current_messages;
        Proto_alpha.Raw_context.back.sc_rollup_current_messages :=
          sc_rollup_current_messages;
        Proto_alpha.Raw_context.back.dal_slot_fee_market := dal_slot_fee_market;
        Proto_alpha.Raw_context.back.dal_attestation_slot_accountability :=
          dal_attestation_slot_accountability;
        Proto_alpha.Raw_context.back.dal_committee := dal_committee;
      |}
  |} =
  Raw_context.to_t {|
    Raw_context.config := {|
      Raw_context_aux.config.remaining_operation_gas :=
        remaining_operation_gas;
      Raw_context_aux.config.constants := constants;
      Raw_context_aux.config.round_durations := round_durations;
      Raw_context_aux.config.cycle_eras := cycle_eras;
      Raw_context_aux.config.level := level;
      Raw_context_aux.config.predecessor_timestamp :=
        predecessor_timestamp;
      Raw_context_aux.config.timestamp := timestamp;
      Raw_context_aux.config.fees := fees;
      Raw_context_aux.config.origination_nonce := origination_nonce;
      Raw_context_aux.config.temporary_lazy_storage_ids :=
        temporary_lazy_storage_ids;
      Raw_context_aux.config.internal_nonce := internal_nonce;
      Raw_context_aux.config.internal_nonces_used :=
        internal_nonces_used;
      Raw_context_aux.config.remaining_block_gas := remaining_block_gas;
      Raw_context_aux.config.unlimited_operation_gas :=
        unlimited_operation_gas;
      Raw_context_aux.config.consensus := consensus;
      Raw_context_aux.config.non_consensus_operations_rev :=
        non_consensus_operations_rev;
      Raw_context_aux.config.dictator_proposal_seen :=
        dictator_proposal_seen;
      Raw_context_aux.config.sampler_state := sampler_state;
      Raw_context_aux.config.stake_distribution_for_current_cycle :=
        stake_distribution_for_current_cycle;
      Raw_context_aux.config.tx_rollup_current_messages :=
        tx_rollup_current_messages;
      Raw_context_aux.config.sc_rollup_current_messages :=
        sc_rollup_current_messages;
      Raw_context_aux.config.dal_slot_fee_market :=
        dal_slot_fee_market;
      Raw_context_aux.config.dal_attestation_slot_accountability :=
        dal_attestation_slot_accountability;
      Raw_context_aux.config.dal_committee :=
        dal_committee;
    |};
    Raw_context.standalone := standalone;
    Raw_context.Block_round := sim_ctxt.(Raw_context.Block_round);
    Raw_context.Tenderbake_First_level_of_protocol :=
      sim_ctxt.(Raw_context.Tenderbake_First_level_of_protocol);
    Raw_context.Tenderbake_Endorsement_branch :=
      sim_ctxt.(Raw_context.Tenderbake_Endorsement_branch);
    Raw_context.Tenderbake_Grand_parent_branch :=
      sim_ctxt.(Raw_context.Tenderbake_Grand_parent_branch);
    Raw_context.Contract_Global_counter :=
      sim_ctxt.(Raw_context.Contract_Global_counter);
    Raw_context.Contract_Spendable_balance :=
      sim_ctxt.(Raw_context.Contract_Spendable_balance);
    Raw_context.Contract_Missed_endorsements :=
      sim_ctxt.(Raw_context.Contract_Missed_endorsements);
    Raw_context.Contract_Manager :=
      sim_ctxt.(Raw_context.Contract_Manager);
    Raw_context.Contract_Consensus_key :=
      sim_ctxt.(Raw_context.Contract_Consensus_key);
    Raw_context.Contract_Pending_consensus_keys :=
      sim_ctxt.(Raw_context.Contract_Pending_consensus_keys);
    Raw_context.Contract_Delegate :=
      sim_ctxt.(Raw_context.Contract_Delegate);
    Raw_context.Contract_Inactive_delegate :=
      sim_ctxt.(Raw_context.Contract_Inactive_delegate);
    Raw_context.Contract_Delegate_last_cycle_before_deactivation :=
      sim_ctxt
        .(Raw_context.Contract_Delegate_last_cycle_before_deactivation);
    Raw_context.Contract_Delegated :=
      sim_ctxt.(Raw_context.Contract_Delegated);
    Raw_context.Contract_Counter :=
      sim_ctxt.(Raw_context.Contract_Counter);
    Raw_context.Contract_Code :=
      sim_ctxt.(Raw_context.Contract_Code);
    Raw_context.Contract_Storage :=
      sim_ctxt.(Raw_context.Contract_Storage);
    Raw_context.Contract_Paid_storage_space :=
      sim_ctxt.(Raw_context.Contract_Paid_storage_space);
    Raw_context.Contract_Used_storage_space :=
      sim_ctxt.(Raw_context.Contract_Used_storage_space);
    Raw_context.Contract_Frozen_deposits :=
      sim_ctxt.(Raw_context.Contract_Frozen_deposits);
    Raw_context.Contract_Frozen_bonds :=
      sim_ctxt.(Raw_context.Contract_Frozen_bonds);
    Raw_context.Contract_Total_frozen_bonds :=
      sim_ctxt.(Raw_context.Contract_Total_frozen_bonds);
    Raw_context.Global_constants_Map :=
      sim_ctxt.(Raw_context.Global_constants_Map);
    Raw_context.Big_map_Next_Storage :=
      sim_ctxt.(Raw_context.Big_map_Next_Storage);
    Raw_context.Big_map_Total_bytes :=
      sim_ctxt.(Raw_context.Big_map_Total_bytes);
    Raw_context.Big_map_Key_type :=
      sim_ctxt.(Raw_context.Big_map_Key_type);
    Raw_context.Big_map_Value_type :=
      sim_ctxt.(Raw_context.Big_map_Value_type);
    Raw_context.Big_map_Contents :=
      sim_ctxt.(Raw_context.Big_map_Contents);
    Raw_context.Sapling_Next_Storage :=
      sim_ctxt.(Raw_context.Sapling_Next_Storage);
    Raw_context.Sapling_Total_bytes :=
      sim_ctxt.(Raw_context.Sapling_Total_bytes);
    Raw_context.Sapling_Commitments_size :=
      sim_ctxt.(Raw_context.Sapling_Commitments_size);
    Raw_context.Sapling_Memo_size :=
      sim_ctxt.(Raw_context.Sapling_Memo_size);
    Raw_context.Sapling_Commitments :=
      sim_ctxt.(Raw_context.Sapling_Commitments);
    Raw_context.Sapling_Ciphertexts :=
      sim_ctxt.(Raw_context.Sapling_Ciphertexts);
    Raw_context.Sapling_Nullifiers_size :=
      sim_ctxt.(Raw_context.Sapling_Nullifiers_size);
    Raw_context.Sapling_Nullifiers_ordered :=
      sim_ctxt.(Raw_context.Sapling_Nullifiers_ordered);
    Raw_context.Sapling_Nullifiers_hashed :=
      sim_ctxt.(Raw_context.Sapling_Nullifiers_hashed);
    Raw_context.Sapling_Roots :=
      sim_ctxt.(Raw_context.Sapling_Roots);
    Raw_context.Sapling_Roots_pos :=
      sim_ctxt.(Raw_context.Sapling_Roots_pos);
    Raw_context.Sapling_Roots_level :=
      sim_ctxt.(Raw_context.Sapling_Roots_level);
    Raw_context.Delegates :=
      sim_ctxt.(Raw_context.Delegates);
    Raw_context.Consensus_keys :=
      sim_ctxt.(Raw_context.Consensus_keys);
    Raw_context.Cycle_Slashed_deposits :=
      sim_ctxt.(Raw_context.Cycle_Slashed_deposits);
    Raw_context.Cycle_Selected_stake_distribution :=
      sim_ctxt.(Raw_context.Cycle_Selected_stake_distribution);
    Raw_context.Cycle_Total_active_stake :=
      sim_ctxt.(Raw_context.Cycle_Total_active_stake);
    Raw_context.Cycle_Delegate_sampler_state :=
      sim_ctxt.(Raw_context.Cycle_Delegate_sampler_state);
    Raw_context.Cycle_Nonce :=
      sim_ctxt.(Raw_context.Cycle_Nonce);
    Raw_context.Cycle_Seed :=
      sim_ctxt.(Raw_context.Cycle_Seed);
    Raw_context.Stake_Staking_balance :=
      sim_ctxt.(Raw_context.Stake_Staking_balance);
    Raw_context.Stake_Active_delegates_with_minimal_stake :=
      sim_ctxt.(Raw_context.Stake_Active_delegates_with_minimal_stake);
    Raw_context.Stake_Last_snapshot :=
      sim_ctxt.(Raw_context.Stake_Last_snapshot);
    Raw_context.Vote_Pred_period_kind :=
      sim_ctxt.(Raw_context.Vote_Pred_period_kind);
    Raw_context.Vote_Current_period :=
      sim_ctxt.(Raw_context.Vote_Current_period);
    Raw_context.Vote_Participation_ema :=
      sim_ctxt.(Raw_context.Vote_Participation_ema);
    Raw_context.Vote_Current_proposal :=
      sim_ctxt.(Raw_context.Vote_Current_proposal);
    Raw_context.Vote_Voting_power_in_listings :=
      sim_ctxt.(Raw_context.Vote_Voting_power_in_listings);
    Raw_context.Vote_Listings :=
      sim_ctxt.(Raw_context.Vote_Listings);
    Raw_context.Vote_Proposals :=
      sim_ctxt.(Raw_context.Vote_Proposals);
    Raw_context.Vote_Proposals_count :=
      sim_ctxt.(Raw_context.Vote_Proposals_count);
    Raw_context.Vote_Ballots :=
      sim_ctxt.(Raw_context.Vote_Ballots);
    Raw_context.Seed_status :=
      sim_ctxt.(Raw_context.Seed_status);
    Raw_context.Seed_VDF_setup :=
      sim_ctxt.(Raw_context.Seed_VDF_setup);
    Raw_context.Commitments :=
      sim_ctxt.(Raw_context.Commitments);
    Raw_context.Ramp_up_Rewards :=
      sim_ctxt.(Raw_context.Ramp_up_Rewards);
    Raw_context.Pending_migration_Balance_updates :=
      sim_ctxt.(Raw_context.Pending_migration_Balance_updates);
    Raw_context.Pending_migration_Operation_results :=
      sim_ctxt.(Raw_context.Pending_migration_Operation_results);
    Raw_context.Liquidity_baking_Toggle_ema :=
      sim_ctxt.(Raw_context.Liquidity_baking_Toggle_ema);
    Raw_context.Liquidity_baking_Cpmm_address :=
      sim_ctxt.(Raw_context.Liquidity_baking_Cpmm_address);
    Raw_context.Ticket_balance_Paid_storage_space :=
      sim_ctxt.(Raw_context.Ticket_balance_Paid_storage_space);
    Raw_context.Ticket_balance_Used_storage_space :=
      sim_ctxt.(Raw_context.Ticket_balance_Used_storage_space);
    Raw_context.Ticket_balance_Table :=
      sim_ctxt.(Raw_context.Ticket_balance_Table);
    Raw_context.Tx_rollup_State :=
      sim_ctxt.(Raw_context.Tx_rollup_State);
    Raw_context.Tx_rollup_Inbox :=
      sim_ctxt.(Raw_context.Tx_rollup_Inbox);
    Raw_context.Tx_rollup_Revealed_withdrawals :=
      sim_ctxt.(Raw_context.Tx_rollup_Revealed_withdrawals);
    Raw_context.Tx_rollup_Commitment :=
      sim_ctxt.(Raw_context.Tx_rollup_Commitment);
    Raw_context.Tx_rollup_Commitment_bond :=
      sim_ctxt.(Raw_context.Tx_rollup_Commitment_bond);
    Raw_context.Sc_rollup_PVM_kind :=
      sim_ctxt.(Raw_context.Sc_rollup_PVM_kind);
    Raw_context.Sc_rollup_Parameters_type :=
      sim_ctxt.(Raw_context.Sc_rollup_Parameters_type);
    Raw_context.Sc_rollup_Genesis_info :=
      sim_ctxt.(Raw_context.Sc_rollup_Genesis_info);
    Raw_context.Sc_rollup_Inbox :=
      sim_ctxt.(Raw_context.Sc_rollup_Inbox);
    Raw_context.Sc_rollup_Last_cemented_commitment :=
      sim_ctxt.(Raw_context.Sc_rollup_Last_cemented_commitment);
    Raw_context.Sc_rollup_Stakers :=
      sim_ctxt.(Raw_context.Sc_rollup_Stakers);
    Raw_context.Sc_rollup_Staker_count :=
      sim_ctxt.(Raw_context.Sc_rollup_Staker_count);
    Raw_context.Sc_rollup_Commitments :=
      sim_ctxt.(Raw_context.Sc_rollup_Commitments);
    Raw_context.Sc_rollup_Commitment_stake_count :=
      sim_ctxt.(Raw_context.Sc_rollup_Commitment_stake_count);
    Raw_context.Sc_rollup_Commitment_first_publication_level :=
      sim_ctxt.(Raw_context.Sc_rollup_Commitment_first_publication_level);
    Raw_context.Sc_rollup_Commitment_added :=
      sim_ctxt.(Raw_context.Sc_rollup_Commitment_added);
    Raw_context.Sc_rollup_Game_versioned :=
      sim_ctxt.(Raw_context.Sc_rollup_Game_versioned);
    Raw_context.Sc_rollup_Game :=
      sim_ctxt.(Raw_context.Sc_rollup_Game);
    Raw_context.Sc_rollup_Game_timeout :=
      sim_ctxt.(Raw_context.Sc_rollup_Game_timeout);
    Raw_context.Sc_rollup_Opponent :=
      sim_ctxt.(Raw_context.Sc_rollup_Opponent);
    Raw_context.Sc_rollup_Applied_outbox_messages :=
      sim_ctxt.(Raw_context.Sc_rollup_Applied_outbox_messages);
    Raw_context.Dal_Slot_Headers :=
      sim_ctxt.(Raw_context.Dal_Slot_Headers);
    Raw_context.Dal_Slot_History :=
      sim_ctxt.(Raw_context.Dal_Slot_History);
    Raw_context.Zk_rollup_Account :=
      sim_ctxt.(Raw_context.Zk_rollup_Account);
    Raw_context.Zk_rollup_Pending_list :=
      sim_ctxt.(Raw_context.Zk_rollup_Pending_list);
    Raw_context.Zk_rollup_Pending_operation :=
      sim_ctxt.(Raw_context.Zk_rollup_Pending_operation);
  |}.
Proof.
  reflexivity.
Qed.

Properties on the [Raw_context.T] signature.
Module T.
Helper to unfold [Raw_context] primitives on the storage.
  Module Unfold.
    Import Proto_alpha.Raw_context.

    Ltac all :=
            unfold
        mem, mem_tree,
        get, get_tree,
        find, find_tree,
        add, add_tree,
        init_value, init_tree,
        update, update_tree,
        remove_existing, remove_existing_tree,
        remove,
        add_or_remove, add_or_remove_tree,
        list_value, fold,
        project, absolute_key.
  End Unfold.

A [Raw_context] is valid when the fold operator respect the functional extentionality axiom.
  Module Valid.
    Import Raw_context_intf.T.

    Record t {t local_context} {C : Raw_context.T (t :=
      t) (local_context := local_context)} : Prop := {
      fold {a : Set} depth ctxt k order (acc : a) f1 f2 :
        ( k v acc, f1 k v acc = f2 k v acc)
        C.(fold) depth ctxt k order acc f1 =
        C.(fold) depth ctxt k order acc f2;
    }.
    Arguments t {_}.
  End Valid.

The equality between two [Raw_context.T].
  Module Eq.
    Import Raw_context_intf.T.
    Record t {t local_context : Set} {C1 C2 : Raw_context.T (t :=
      t) (local_context := local_context)} : Prop := {
      mem ctxt k : C1.(mem) ctxt k = C2.(mem) ctxt k;
      mem_tree ctxt k : C1.(mem_tree) ctxt k = C2.(mem_tree) ctxt k;
      get ctxt k : C1.(get) ctxt k = C2.(get) ctxt k;
      get_tree ctxt k : C1.(get_tree) ctxt k = C2.(get_tree) ctxt k;
      find ctxt k : C1.(find) ctxt k = C2.(find) ctxt k;
      find_tree ctxt k : C1.(find_tree) ctxt k = C2.(find_tree) ctxt k;
      list_value ctxt offset length k :
        C1.(list_value) ctxt offset length k =
        C2.(list_value) ctxt offset length k;
      init_value ctxt k v : C1.(init_value) ctxt k v = C2.(init_value) ctxt k v;
      init_tree ctxt k v : C1.(init_tree) ctxt k v = C2.(init_tree) ctxt k v;
      update ctxt k v : C1.(update) ctxt k v = C2.(update) ctxt k v;
      update_tree ctxt k v : C1.(update_tree) ctxt k v = C2.(update_tree) ctxt k v;
      add ctxt k v : C1.(add) ctxt k v = C2.(add) ctxt k v;
      add_tree ctxt k v : C1.(add_tree) ctxt k v = C2.(add_tree) ctxt k v;
      remove ctxt k : C1.(remove) ctxt k = C2.(remove) ctxt k;
      remove_existing ctxt k :
        C1.(remove_existing) ctxt k = C2.(remove_existing) ctxt k;
      remove_existing_tree ctxt k :
        C1.(remove_existing_tree) ctxt k = C2.(remove_existing_tree) ctxt k;
      add_or_remove ctxt k v :
        C1.(add_or_remove) ctxt k v = C2.(add_or_remove) ctxt k v;
      add_or_remove_tree ctxt k v :
        C1.(add_or_remove_tree) ctxt k v = C2.(add_or_remove_tree) ctxt k v;
      fold {a : Set} depth ctxt k order (acc : a) f :
        C1.(fold) depth ctxt k order acc f =
        C2.(fold) depth ctxt k order acc f;
      Tree : Raw_context_intf.TREE.Eq.t C1.(Tree) C2.(Tree);
      project ctxt : C1.(project) ctxt = C2.(project) ctxt;
      absolute_key ctxt k : C1.(absolute_key) ctxt k = C2.(absolute_key) ctxt k;
      (* We do not check [consume_gas], [check_enough_gas] and [description]. *)
    }.
    Arguments t {_ _}.
  End Eq.

A [Kernel] of primitive operations which are enough to describe a whole [Raw_context.T].
  Module Kernel.
    Record signature {t : Set} : Set := {
      
The path from the root of the context store. It may depend on the value of the context for indexed raw contexts.
      absolute_key : t Context.key;
      
Extract the root raw context.
      project : t Proto_alpha.Raw_context.t;
      
Update the root raw context part of the context, and keep everything else (typically, keeps the index for indexed raw contexts).
      update : t Proto_alpha.Raw_context.t t;
    }.
  End Kernel.
  Definition Kernel :=
      @Kernel.signature.
  Arguments Kernel {_}.

The equality between two raw kernels.
  Module Kernel_eq.
    Import Kernel.

    Record t {t} {K1 K2 : Kernel (t :=
      t)} : Prop := {
      absolute_key ctxt : K1.(absolute_key) ctxt = K2.(absolute_key) ctxt;
      project ctxt : K1.(project) ctxt = K2.(project) ctxt;
      update ctxt root_ctxt :
        K1.(update) ctxt root_ctxt = K2.(update) ctxt root_ctxt;
    }.
    Arguments t {_}.
  End Kernel_eq.

Define a whole raw context from its kernel.
  Definition of_kernel {t local_context} (K : Kernel (t :=
      t)) : Raw_context.T (t := t) (local_context := local_context) :=
    let '{|
      Kernel.absolute_key :=
      absolute_key;
      Kernel.project :=
      project;
      Kernel.update :=
      update
    |} :=
      K in
    let to_key ctxt k :=
            absolute_key ctxt ++ k in
    {|
      Raw_context_intf.T.mem ctxt k :=
              Raw_context.mem (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.mem_tree ctxt k :=
              Raw_context.mem_tree (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.get ctxt k :=
        Raw_context.get (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.get_tree ctxt k :=
        Raw_context.get_tree (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.find ctxt k :=
        Raw_context.find (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.find_tree ctxt k :=
        Raw_context.find_tree (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.list_value ctxt offset length k :=
        Raw_context.list_value (project ctxt) offset length (to_key ctxt k);
      Raw_context_intf.T.init_value ctxt k v :=
        let? root := Raw_context.init_value (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.init_tree ctxt k v :=
        let? root := Raw_context.init_tree (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.update ctxt k v :=
        let? root := Raw_context.update (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.update_tree ctxt k v :=
        let? root := Raw_context.update_tree (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.add ctxt k v :=
        let root := Raw_context.add (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.add_tree ctxt k v :=
        let root := Raw_context.add_tree (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.remove ctxt k :=
        let root := Raw_context.remove (project ctxt) (to_key ctxt k) in
        update ctxt root;
      Raw_context_intf.T.remove_existing ctxt k :=
        let? root :=
          Raw_context.remove_existing (project ctxt) (to_key ctxt k) in
        return? update ctxt root;
      Raw_context_intf.T.remove_existing_tree ctxt k :=
        let? root :=
          Raw_context.remove_existing_tree (project ctxt) (to_key ctxt k) in
        return? update ctxt root;
      Raw_context_intf.T.add_or_remove ctxt k v :=
        let root :=
          Raw_context.add_or_remove (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.add_or_remove_tree ctxt k v :=
        let root :=
          Raw_context.add_or_remove_tree (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.fold _ depth ctxt k order acc f :=
        Raw_context.fold depth (project ctxt) (to_key ctxt k) order acc f;
      Raw_context_intf.T.config_value :=
        axiom "config_value";
      Raw_context_intf.T.length :=
        axiom "length";
      Raw_context_intf.T.Tree :=
        {|
          Raw_context_intf.TREE.mem :=
            Raw_context.Tree.(Raw_context_intf.TREE.mem);
          Raw_context_intf.TREE.mem_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.mem_tree);
          Raw_context_intf.TREE.get :=
            Raw_context.Tree.(Raw_context_intf.TREE.get);
          Raw_context_intf.TREE.get_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.get_tree);
          Raw_context_intf.TREE.find :=
            Raw_context.Tree.(Raw_context_intf.TREE.find);
          Raw_context_intf.TREE.find_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.find_tree);
          Raw_context_intf.TREE.list_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.list_value);
          Raw_context_intf.TREE.init_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.init_value);
          Raw_context_intf.TREE.init_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.init_tree);
          Raw_context_intf.TREE.update :=
            Raw_context.Tree.(Raw_context_intf.TREE.update);
          Raw_context_intf.TREE.update_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.update_tree);
          Raw_context_intf.TREE.add :=
            Raw_context.Tree.(Raw_context_intf.TREE.add);
          Raw_context_intf.TREE.add_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.add_tree);
          Raw_context_intf.TREE.remove :=
            Raw_context.Tree.(Raw_context_intf.TREE.remove);
          Raw_context_intf.TREE.remove_existing :=
            Raw_context.Tree.(Raw_context_intf.TREE.remove_existing);
          Raw_context_intf.TREE.remove_existing_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.remove_existing_tree);
          Raw_context_intf.TREE.add_or_remove :=
            Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove);
          Raw_context_intf.TREE.add_or_remove_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove_tree);
          Raw_context_intf.TREE.fold _ :=
            Raw_context.Tree.(Raw_context_intf.TREE.fold);
          Raw_context_intf.TREE.config_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.config_value);
          Raw_context_intf.TREE.length :=
            Raw_context.Tree.(Raw_context_intf.TREE.length);
          (* The definition of the [Tree] is very long and differs only on this
             field. *)

          Raw_context_intf.TREE.empty ctxt :=
            Raw_context.Tree.empty (project ctxt);
          Raw_context_intf.TREE.is_empty :=
            Raw_context.Tree.(Raw_context_intf.TREE.is_empty);
          Raw_context_intf.TREE.kind_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.kind_value);
          Raw_context_intf.TREE.to_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.to_value);
          Raw_context_intf.TREE.hash_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.hash_value);
          Raw_context_intf.TREE.equal :=
            Raw_context.Tree.(Raw_context_intf.TREE.equal);
          Raw_context_intf.TREE.clear :=
            Raw_context.Tree.(Raw_context_intf.TREE.clear);
        |};
      Raw_context_intf.T.verify_tree_proof ctxt :=
        axiom "verify_tree_proof";
      Raw_context_intf.T.verify_stream_proof ctxt :=
        axiom "verify_stream_proof";
      Raw_context_intf.T.equal_config :=
        axiom "equal_config";
      Raw_context_intf.T.project ctxt :=
        project ctxt;
      Raw_context_intf.T.absolute_key ctxt k :=
        to_key ctxt k;
      Raw_context_intf.T.consume_gas :=
        axiom "consume_gas";
      Raw_context_intf.T.check_enough_gas :=
        axiom "check_enough_gas";
      Raw_context_intf.T.description :=
        axiom "description";
      Raw_context_intf.T.with_local_context := axiom "with_local_context";
      Raw_context_intf.T.Local_context := axiom "Local_context";
    |}.

Generating contexts from two equal kernels yields two equal raw contexts.
  Lemma from_kernel_implies_eq {t local_context : Set} (K1 K2 : Kernel (t := t)) :
    Kernel_eq.t K1 K2
    Eq.t (local_context := local_context) (of_kernel K1) (of_kernel K2).
  Proof.
    intros []; repeat constructor; intros; simpl;
      repeat match goal with
      | |- context [let? _ := ?e in _] ⇒
        destruct e eqn:?;
        simpl
      end;
      repeat match goal with
      | H : _ |- _rewrite H in ×
      end;
      congruence.
  Qed.

If a raw context is described by a given kernel.
  Definition is_from_kernel {t local_context} (C : Raw_context.T (t := t) (local_context := local_context))
    (K : Kernel (t := t)) : Prop :=
    Eq.t C (of_kernel K).

The kernel of the root raw context.
  Definition M_kernel : Kernel (t := Proto_alpha.Raw_context.t) := {|
    Kernel.absolute_key _ := [];
    Kernel.project ctxt := ctxt;
    Kernel.update _ root := root;
  |}.

The main raw context can be expressed from a kernel.
  Lemma M_is_from_kernel : is_from_kernel Raw_context.M M_kernel.
  Proof.
    repeat constructor; intros; simpl; try reflexivity;
      match goal with
      | |- context [let? _ := ?e in _] ⇒
        destruct e eqn:?;
        simpl
      end;
      sfirstorder.
  Qed.
End T.

The value of [get_constants] for a valid context.
Lemma get_constants_eq {A : Set} standalone :
  standalone.Valid.simulation standalone
  Raw_context.get_constants (A := A) (Raw_context.to_context standalone) =
  return? standalone.(Raw_context_aux.standalone.constants).
Proof.
  intros [].
  unfold Raw_context.get_constants, Raw_context.to_context;
  repeat destruct Binary.to_bytes_opt eqn:? in |- *;
    repeat Context.rewrite_find_add;
    repeat rewrite Raw_context.find_empty_context;
    destruct Constants_parametric_repr.encoding_is_valid as [H_of_to H_to_of];
    pose proof (H_of_to standalone.(Raw_context_aux.standalone.constants)) as H_encoding;
    hauto l: on.
Qed.

The function [check_inited] always succeeds on the simulated context.
Lemma check_inited_eq (standalone : Raw_context_aux.standalone) :
  Raw_context.check_inited (Raw_context.to_context standalone) = return? tt.
Proof.
  unfold Raw_context.check_inited, Raw_context.to_context;
  repeat destruct Binary.to_bytes_opt eqn:? in |- *;
    repeat Context.rewrite_find_add;
    reflexivity.
Qed.

@TODO fix proof
Lemma check_cycle_eras_eq standalone :
  standalone.Valid.simulation standalone
  Raw_context.check_cycle_eras
    standalone.(Raw_context_aux.standalone.cycle_eras)
    standalone.(Raw_context_aux.standalone.constants) =
  return? tt.
Proof.
  intros [].
  unfold Raw_context.check_cycle_eras, Level_repr.current_era.
  step; simpl.
  { inversion cycle_eras. cbn in ×. contradiction. }
  { (* TODO add this to the Level_repr.current_era_is_valid *)
    assert (H : c.(Level_repr.cycle_era.blocks_per_cycle) =
     standalone.(Raw_context_aux.standalone.constants)
       .(Constants_parametric_repr.t.blocks_per_cycle)
     c.(Level_repr.cycle_era.blocks_per_commitment) =
       standalone.(Raw_context_aux.standalone.constants)
       .(Constants_parametric_repr.t.blocks_per_commitment))
           by admit.
    destruct H as [H H'].
    step.
    { step; cbn; [reflexivity|].
      rewrite Z.eqb_neq in Heqb0.
      contradiction Heqb0.
    }
    { rewrite Z.eqb_neq in Heqb.
         contradiction H.
    }
Admitted.

Context contains an origination nonce
The context has one [Level_repr.cycle_era] and [level] is greather than this era
Module Has_one_era.
  Definition t (ctxt : Proto_alpha.Raw_context.t)
             (era : Level_repr.cycle_era) : Prop :=
    Raw_context.cycle_eras ctxt = [era].
End Has_one_era.

The encoding [storage_error_encoding] is valid.
Lemma storage_error_encoding_is_valid :
  Data_encoding.Valid.t (fun _True)
    Raw_context.storage_error_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  sauto l: on.
Qed.
#[global] Hint Resolve storage_error_encoding_is_valid : Data_encoding_db.

[check_inited] never returns an internal error
ensures that [level] is greater than the levels inside [ctxt] @TODO This predicate can probably be simplified when [ctxt] is valid because level decrease.
  Definition level_valid_for_context standalone
  (level : Raw_level_repr.t) : Prop :=
    letP? _ := Level_repr.level_from_raw
      standalone.(Raw_context_aux.standalone.cycle_eras) level
    in True.
End ToMove.

(* @TODO? should we also check that predecessor_timestamp
  is less than timestamp in the input of prepare?*)


under the expected validity conditions, [prepare] never returns an internal error, provided that [level] (aka [Int32.succ pred_level]) is greater than the first level of [ctxt]. Note: this hypothesis can probably be simplified, since the validity of [ctxt] ensures that the levels of ctxt are decreasing. @TODO fix proof
rewrite Raw_context.get_cycle_eras_eq by assumption; simpl. rewrite Raw_context.check_cycle_eras_eq by assumption; simpl. apply no_internal_errors_let. (** Note: the tactic no_internal_errors_lets
     would create three non-trivial subgoals, including the first one here  *)

assumption. intro. exact I. Qed.
Admitted.

[Raw_context.sampler] is valid
Simulation [to_t] is injective
Lemma to_t_is_injective c1 c2 :
  Raw_context.to_t c1 = Raw_context.to_t c2 c1 = c2.
Proof.
Admitted.

[fees] is valid
Lemma fees_is_valid ctxt :
  Valid.t ctxt
  Tez_repr.Valid.t (Raw_context.fees ctxt).
Proof.
  intro Hv.
  unfold Raw_context.fees.
  destruct ctxt; simpl.
  unfold Valid.t in Hv.
  unfold Valid.on in Hv.
  destruct Hv as [sc Hsc].
  destruct Hsc as [Heq [Hv _]].
  unfold Raw_context.to_t in Heq.
  inversion Heq.
  destruct Hv.
  unfold Raw_context.to_back; simpl.
  destruct config.
  exact fees.
Qed.

[update_back] is valid
[get_collected_fees_only_call_from_token] is valid
[update_fees] is valid
Lemma update_fees_is_valid ctxt t :
  Valid.t ctxt
  Tez_repr.Valid.t t
  Valid.t (Raw_context.update_fees ctxt t).
Proof.
Admitted.

[credit_collected_fees_only_call_from_token] is valid
[spend_collected_fees_only_call_from_token] is valid
Lemma spend_collected_fees_only_call_from_token_is_valid ctxt fees :
  Valid.t ctxt
  Tez_repr.Valid.t fees
  letP? t1 := Raw_context.spend_collected_fees_only_call_from_token
    ctxt fees in Valid.t t1.
Proof.
  intros Hctxt Hfees.
  unfold Raw_context.spend_collected_fees_only_call_from_token.
  eapply Error.split_letP.
  2:{ intros.
      simpl.
      apply update_fees_is_valid; eauto.
    }
  epose proof (Tez_repr.op_minusquestion_is_valid
    (get_collected_fees_is_valid _ Hctxt)
    Hfees).
  destruct Raw_context.get_collected_fees.
  destruct fees.
  destruct Tez_repr.op_minusquestion eqn:Hminus.
  { destruct t; tauto. }
  { unfold Tez_repr.op_minusquestion in Hminus.
    destruct (_ i64 _); [discriminate|].
    simpl in ×.
    now inversion Hminus.
  }
Qed.

[init_origination_nonce] is valid
[increment_origination_nonce] is valid
[origination_nonce] is valid
[get_origination_nonce] is valid
Lemma get_origination_nonce_is_valid ctxt :
  Valid.t ctxt
  letP? 'o := Raw_context.get_origination_nonce
    ctxt in
  Origination_nonce.Valid.t o.
Proof.
  intro.
  unfold Raw_context.get_origination_nonce.
  destruct Raw_context.origination_nonce eqn:?; [|reflexivity].
  eapply origination_nonce_is_valid; eauto.
Qed.

The function [unset_origination_nonce] is valid.
The function [remaining_operation_gas] is valid.
The function [gas_level] is valid.
Lemma gas_level_is_valid ctxt :
  Valid.t ctxt
  let gas := Raw_context.gas_level ctxt in
  Gas_limit_repr.Valid.t gas.
Proof.
  intro.
  unfold Raw_context.gas_level.
  destruct Raw_context.unlimited_operation_gas eqn:?; [exact I|].
  now apply remaining_operation_gas_is_valid.
Qed.

The function [remaining_block_gas] is valid.
The function [block_gas_level] is valid.
The function [consume_gas_limit_in_block] is valid.
Lemma consume_gas_limit_in_block_is_valid ctxt gas_limit :
  Valid.t ctxt
  Gas_limit_repr.Arith.Integral.Valid.t gas_limit
  letP? ctxt := Raw_context.consume_gas_limit_in_block ctxt gas_limit in
  Raw_context.Valid.t ctxt.
Proof.
  intros.
  unfold Raw_context.consume_gas_limit_in_block.
  eapply Error.split_letP.
  { apply Gas_limit_repr.check_gas_limit_is_valid.
    { admit. }
    { auto. }
  }
  { intros _ _.
    destruct (Gas_limit_repr.Arith.op_gt).
    { reflexivity. }
    { now apply update_back_is_valid. }
  }
Admitted.

The function [with_remaining_operation_gas] is valid.
The function [set_gas_limit] is valid.
The function [set_gas_unlimited] is valid.
Lemma set_gas_unlimited_is_valid ctxt :
  Valid.t ctxt
  let ctxt := Raw_context.set_gas_unlimited ctxt in
  Raw_context.Valid.t ctxt.
Proof.
  simpl; intro.
  now apply update_back_is_valid.
Qed.

The function [raw_consume] is valid.
The function [consume_gas] is valid.
Lemma consume_gas_is_valid ctxt cost :
  Valid.t ctxt
  Saturation_repr.Valid.t cost
  letP? ctxt := Raw_context.consume_gas ctxt cost in
  Raw_context.Valid.t ctxt.
Proof.
  intros Hctxt Hcost.
  unfold Raw_context.consume_gas.
  destruct Gas_limit_repr.raw_consume eqn:Heq.
  { simpl.
    unfold Raw_context.update_remaining_operation_gas.
    apply with_remaining_operation_gas_is_valid; [auto|].
    apply (raw_consume_is_valid
      (Raw_context.remaining_operation_gas ctxt)
      cost); auto.
    pose (remaining_operation_gas_is_valid _ Hctxt).
    unfold Saturation_repr.Strictly_valid.t in ×.
    unfold Saturation_repr.Valid.t; lia.
  }
  { destruct Raw_context.unlimited_operation_gas; [auto|].
    reflexivity.
  }
Qed.

The function [activate] is valid
Lemma activate_is_valid ctxt h :
  Raw_context.Valid.t ctxt
  Raw_context.Valid.t (Raw_context.activate ctxt h).
Proof.
  intro.
  now apply update_back_is_valid.
Qed.

Module Cache.
The function [sync] is valid.
The function [update_consensus_with] is valid.
  Lemma update_consensus_with_is_valid ctxt f
    (H_ctxt : Raw_context.Valid.t ctxt)
    (H_f : consensus,
      Raw_consensus.Valid.t consensus
      Raw_consensus.Valid.t (f consensus)
    ) :
    let ctxt := Raw_context.Consensus.update_consensus_with ctxt f in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [initialize_consensus_operation] is valid.
The function [add_message] is valid.
  Lemma add_message_is_valid ctxt rollup message :
    Raw_context.Valid.t ctxt
    let '(ctxt, _) := Raw_context.Tx_rollup.add_message ctxt rollup message in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.
End Tx_rollup.

Module Sc_rollup_in_memory_inbox.
The function [current_messages] is valid.
  (*
  Lemma current_messages ctxt rollup :
    Raw_context.Valid.t ctxt ->
    letP? '(_, ctxt) :=
      Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt rollup in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

  (** The function [set_current_messages] is valid. *)
  Lemma set_current_messages ctxt rollup tree_value :
    Raw_context.Valid.t ctxt ->
    letP? ctxt :=
      Raw_context.Sc_rollup_in_memory_inbox.set_current_messages
        ctxt rollup tree_value in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted. *)

End Sc_rollup_in_memory_inbox.

Module Dal.
The function [record_available_shards] is valid.
  (*
  Lemma record_available_shards_is_valid ctxt slots shards
    (H_ctxt : Raw_context.Valid.t ctxt)
    (H_slots : Dal_endorsement_repr.Valid.t slots)
    (H_shards :
      List.Forall Dal_endorsement_repr.Accountability.shard.Valid.t shards) :
    let ctxt := Raw_context.Dal.record_available_shards ctxt slots shards in
    Raw_context.Valid.t ctxt.
  Proof.
    unfold Raw_context.Dal.record_available_shards.
    destruct H_ctxt as [sim_ctxt [H_sim_ctxt_eq [H_sim_ctxt]]].
    rewrite H_sim_ctxt_eq; simpl.
    destruct sim_ctxt; simpl.
    destruct config; simpl.
    unfold Raw_context.to_t,
      Raw_context.to_back,
      Proto_alpha.Raw_context.t.with_back,
      Raw_context.back.with_dal_endorsement_slot_accountability;
      simpl.
    cbn.
    eexists.
    split; [|split; trivial].
    { apply to_t_inversion. }
    {
      destruct H_sim_ctxt, config, standalone0. simpl in *.
      match type of H_sim_ctxt_eq with
      | _ = Raw_context.to_t ?sim_ctxt' =>
          instantiate (1 := sim_ctxt')
      end.
      constructor; simpl; try (constructor; simpl); trivial;
        destruct Tenderbake, Vote; [|easy..].
      now apply
        Dal_endorsement_repr.Accountability
          .record_shards_availability_is_valid.
    }
  Qed.

  (** The function [register_slot] is valid. *)
  Lemma register_slot_is_valid ctxt slot
    (H_ctxt : Raw_context.Valid.t ctxt)
    (H_slot : Dal_slot_repr.Valid.t slot) :
    letP? '(ctxt, _) := Raw_context.Dal.register_slot ctxt slot in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

  (** The function [candidates] is valid. *)
  Lemma candidates_is_valid ctxt
    (H_ctxt : Raw_context.Valid.t ctxt) :
    let slots := Raw_context.Dal.candidates ctxt in
    List.Forall Dal_slot_repr.Valid.t slots.
  Proof.
  Admitted.

  (** The function [shards] is valid. *)
  Lemma shards_is_valid ctxt endorser
    (H_ctxt : Raw_context.Valid.t ctxt) :
    let slots := Raw_context.Dal.shards ctxt endorser in
    List.Forall
      Dal_endorsement_repr.Accountability.shard.Valid.t
      (Raw_context.Dal.shards ctxt endorser).
  Proof.
  Admitted.
*)

End Dal.

[on domain ctxt] implies [t ctxt]
Lemma on_impl_t ctxt domain :
  Raw_context.Valid.on domain ctxt
  Raw_context.Valid.t ctxt.
Proof.
  unfold Raw_context.Valid.t. intros H_ctxt.
  unfold Raw_context.Valid.on in ×.
  destruct H_ctxt as [ctxt'].
   ctxt'.
  Tactics.destruct_conjs.
  now split_conj.
Qed.

If a context simulation [sim_ctxt] is valid in the trivial domain [fun _ => True], then for every projection [p] and every function [f], [sim_ctxt <| p := f sim_ctxt.(p) |>] is also valid.
[record <| projection := value |>] is the update notation for records.
If [domain1] implies [domain2] for every simulated context [sim_ctxt], then [Raw_context.Valid.on domain1 ctxt] implies [Raw_context.Valid.on domain2 ctxt]
Lemma domain_impl_ctxt (domain1 domain2 : Raw_context.t Prop)
  ctxt :
  ( sim_ctxt, domain1 sim_ctxt domain2 sim_ctxt)
  Raw_context.Valid.on domain1 ctxt
  Raw_context.Valid.on domain2 ctxt.
Proof.
  intros H_domain H_ctxt.
  Raw_context.Valid.destruct_rewrite H_ctxt.
  specialize (H_domain sim_ctxt).
  unfold Raw_context.Valid.on in ×.
  eauto.
Qed.

If [domain1] implies [domain2] for the specific simulated context [sim_ctxt], then [Raw_context.Valid.on domain1 ctxt] implies [Raw_context.Valid.on domain2 ctxt]
Lemma domain_impl_sim_ctxt (domain1 domain2 : Raw_context.t Prop)
  sim_ctxt :
  (domain1 sim_ctxt domain2 sim_ctxt)
  Raw_context.Valid.on domain1 (Raw_context.to_t sim_ctxt)
  Raw_context.Valid.on domain2 (Raw_context.to_t sim_ctxt).
Proof.
  intros H_domain H_ctxt.
  unfold Raw_context.Valid.on in ×.
  Raw_context.Valid.destruct_rewrite H_ctxt.
  destruct H_ctxt as [sim_ctxt' H_ctxt'].
  destruct H_ctxt' as [H_sim_ctxt_eq' ?].
  apply Raw_context.to_t_is_injective in H_sim_ctxt_eq'.
  subst sim_ctxt0.
   sim_ctxt'.
  split_conj; [reflexivity|assumption|].
  apply Raw_context.to_t_is_injective in H_sim_ctxt_eq.
  subst sim_ctxt'.
  now apply H_domain.
Qed.

This tactic makes it easier to apply the lemma [domain_impl_sim_ctxt] by searching the domains in the proof context and the current goal. It expects a goal in the form [Raw_context.Valid.on domain2 (Raw_context.to_t sim_ctxt)] and [H_ctxt] should also have the same form.
Ltac apply_domain_impl_sim_ctxt H_ctxt :=
  match type of H_ctxt with
  | Raw_context.Valid.on ?domain1 (Raw_context.to_t ?sim_ctxt) ⇒
      match goal with
      | |- Raw_context.Valid.on
            ?domain2 (Raw_context.to_t ?sim_ctxt) ⇒
          apply (Raw_context.domain_impl_sim_ctxt domain1 domain2
            sim_ctxt); [|assumption]
      end
  end.

If you have two domains [domain1] and [domain2], you can glue them together into a conjunction [fun sim_ctxt => domain1 sim_ctxt /\ domain2 sim_ctxt]
Lemma domain_conj {ctxt domain1 domain2} :
  Raw_context.Valid.on domain1 ctxt
  Raw_context.Valid.on domain2 ctxt
  Raw_context.Valid.on
    (fun sim_ctxtdomain1 sim_ctxt domain2 sim_ctxt) ctxt.
Proof.
  intros H1 H2.
  Raw_context.Valid.destruct_rewrite H1.
  unfold Raw_context.Valid.on.
   sim_ctxt; split_conj; try easy.
  Raw_context.Valid.destruct_rewrite H2.
  apply Raw_context.to_t_is_injective in H_sim_ctxt_eq0.
  subst sim_ctxt. easy.
Qed.

If `sim_ctxt` is in the domains [fun sim_ctxt => key_exists key subkey sim_ctxt.(projection)] and [fun sim_ctxt => if_value_exists P key subkey sim_ctxt.(projection)] then `sim_ctxt` is also in the domain [fun sim_ctxt => value_exists P key subkey sim_ctxt.(projection)]
Lemma key_exists_impl_value_exists
  {k k' v : Set}
  {index : Path_encoding.S (t := k)}
  {index' : Path_encoding.S (t := k')}
  {proj1 :
    Raw_context.t
      Map.Make_t (Storage_sigs.Indexed_map.Ord index)
        (Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)}
  (key : k) (subkey : k')
  (ctxt : Proto_alpha.Raw_context.t)
  (P : v Prop) :
  Raw_context.Valid.on
    (fun sim_ctxt
       Raw_context.Nested_indexed_data_storage.key_exists
         key subkey sim_ctxt.(proj1)) ctxt
  Raw_context.Valid.on
    (fun sim_ctxt
       Raw_context.Nested_indexed_data_storage.if_value_exists P
         key subkey sim_ctxt.(proj1)) ctxt
  Raw_context.Valid.on
    (fun sim_ctxt
       Raw_context.Nested_indexed_data_storage.value_exists
         P key subkey sim_ctxt.(proj1))
    ctxt.
Proof.
  intros H_ctxt1 H_ctxt2.
  Raw_context.Valid.destruct_rewrite H_ctxt1.
  Raw_context.Valid.destruct_rewrite H_ctxt2.
  apply Raw_context.to_t_is_injective in H_sim_ctxt_eq0.
  subst sim_ctxt0.
   sim_ctxt; split_conj; try easy.
  now apply Raw_context.Nested_indexed_data_storage
    .key_exists_and_if_value_exists_impl_value_exists.
Qed.