🌌 Alpha_context.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.

Require TezosOfOCaml.Environment.V8.Proofs.Error_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Init_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

Module Timestamp.

The function [current] is valid.

  Lemma current_is_valid ctxt :
    Raw_context.Valid.t ctxt →
    Time.Valid.t (Alpha_context.Timestamp.current ctxt).
  Proof.
  Admitted.

The function [predecessor] is valid.

  Lemma predecessor_is_valid ctxt :
    Raw_context.Valid.t ctxt →
    Time.Valid.t (Alpha_context.Timestamp.predecessor ctxt).
  Proof.
  Admitted.
End Timestamp.

Module Operation.

The encoding [Alpha_context.Operation.unsigned_encoding] is valid.

  Lemma unsigned_encoding_is_valid :
    ∀ kind,
    Data_encoding.Valid.t
    (fun '(_, x) ⇒ Operation_repr.packed_contents_list.Valid.t kind x)
    Alpha_context.Operation.unsigned_encoding.
  Proof.
    intros.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve unsigned_encoding_is_valid : Data_encoding_db.
End Operation.

Module First_level_of_protocol.

The function [get] is valid.

  Lemma get_is_valid ctxt :
    Raw_context.Valid.t ctxt →
    letP? level := Alpha_context.First_level_of_protocol.get ctxt in
    Raw_level_repr.Valid.t level.
  Proof.
  Admitted.
End First_level_of_protocol.

Module Constants.

The function [round_durations] is valid.

  Lemma round_durations_is_valid ctxt
    (H_ctxt : Raw_context.Valid.t ctxt) :
    let round := Alpha_context.Constants.round_durations ctxt in
    Round_repr.Durations.Valid.t round.
  Proof.
    Raw_context.Valid.destruct_rewrite H_ctxt.
    apply H_sim_ctxt.
  Qed.

The function [all] is valid.

  Lemma all_is_valid ctxt
    (H_ctxt : Raw_context.Valid.t ctxt) :
    let ctxt := Alpha_context.Constants.all ctxt in
    Constants_repr.Valid.t ctxt.
  Proof.
  Admitted.
End Constants.

Module Round.

The encoding [Alpha_context.Round.round_durations_encoding] is valid.

  Lemma round_durations_encoding_is_valid :
    Data_encoding.Valid.t
    Round_repr.Durations.Valid.t
    Alpha_context.Round.round_durations_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve round_durations_encoding_is_valid : Data_encoding_db.

The function [round_duration] is valid.

  Lemma round_duration_is_valid durations round :
    Round_repr.Durations.Valid.t durations →
    Round_repr.Valid.t round →
    Period_repr.Valid.t (Alpha_context.Round.round_duration durations round).
  Proof.
  Admitted.

The function [update] is valid.

  Lemma update_is_valid ctxt round :
    Raw_context.Valid.t ctxt →
    Round_repr.Valid.t round →
    letP? ctxt := Proto_alpha.Alpha_context.Round.update ctxt round in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [get] is valid.

  Lemma get_is_valid ctxt :
    Raw_context.Valid.t ctxt →
    letP? round := Proto_alpha.Alpha_context.Round.get ctxt in
    Round_repr.Valid.t round.
  Proof.
  Admitted.
End Round.

Module Gas.

The function [set_limit] is valid.

  Definition set_limit_is_valid := Raw_context.set_gas_limit_is_valid.

The function [consume_limit_in_block] is valid.

  Definition consume_limit_in_block_is_valid :=
    Raw_context.consume_gas_limit_in_block_is_valid.

The function [set_unlimited] is valid.

  Definition set_unlimited_is_valid :=
    Raw_context.set_gas_unlimited_is_valid.

The function [consume] is valid.

  Lemma consume_is_valid ctxt cost :
    Raw_context.Valid.t ctxt →
    Saturation_repr.Valid.t cost →
    letP? ctxt := Alpha_context.Gas.consume ctxt cost in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.
End Gas.

Module Script.

The function [force_decode_in_context] is valid.

  Lemma force_decode_in_context_is_valid consume_deserialization_gas ctxt lexpr
  : Raw_context.Valid.t ctxt →
    letP? '(_, ctxt') :=
      Alpha_context.Script.force_decode_in_context
        consume_deserialization_gas ctxt lexpr in
    Raw_context.Valid.t ctxt'.
  Proof.
    intros H. unfold Alpha_context.Script.force_decode_in_context.
    eapply Error.split_letP. {
      apply Raw_context.consume_gas_is_valid ; [ assumption |].
      destruct consume_deserialization_gas eqn:eq_cons ; [
      apply Script_repr.stable_force_decode_cost_is_valid|
      apply Script_repr.force_decode_cost_is_valid]. }
    clear ctxt H. intros ctxt H.
    eapply Error.split_letP with (fun x ⇒ True) ; [
      

@TODO the 2 lines below give the proof of a [force_decode_is_valid] Lemma

      destruct (@force_decode Script_repr.expr lexpr ) eqn:Hlexpr ;
      unfold Script_repr.force_decode ; rewrite Hlexpr ; easy|].
    intros expr' _. assumption.
  Qed.

The function [force_bytes_in_context] is valid.

  Lemma force_bytes_in_context_is_valid ctxt lexpr :
    Raw_context.Valid.t ctxt →
    letP? '(_, ctxt) :=
      Alpha_context.Script.force_bytes_in_context ctxt lexpr in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [consume_decoding_gas] is valid.

  Lemma consume_decoding_gas_is_valid available_gas lexpr :
    Saturation_repr.Valid.t available_gas →
    letP? gas :=
      Alpha_context.Script.consume_decoding_gas available_gas lexpr in
    Saturation_repr.Valid.t available_gas.
  Proof.
  Admitted.
End Script.

Module Origination_nonce.
  (* @TODO: validity of functions of this module *)
End Origination_nonce.

Module Contract.
  (* @TODO: validity of functions of this module *)
End Contract.

Module Tx_rollup_message.
  (* @TODO: validity of functions of this module *)
End Tx_rollup_message.

Module Big_map.
  Module Id.

The encoding [Alpha_context.Big_map.Id.encoding] is valid.

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

The function [get_opt] is valid.

  Lemma get_opt_is_valid ctxt m_value k_value :
    Raw_context.Valid.t ctxt →
    letP? '(ctxt, _) := Alpha_context.Big_map.get_opt ctxt m_value k_value in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [list_key_values] is valid.

  Lemma list_key_values_is_valid offset length ctxt m_value :
    Option.Forall Pervasives.Int.Valid.non_negative offset →
    Option.Forall Pervasives.Int.Valid.non_negative length →
    Raw_context.Valid.t ctxt →
    letP? '(ctxt, _) :=
      Alpha_context.Big_map.list_key_values offset length ctxt m_value in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [_exists] is valid.

  Lemma _exists_is_valid ctxt id :
    Raw_context.Valid.t ctxt →
    letP? '(ctxt, _) := Alpha_context.Big_map._exists ctxt id in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.
End Big_map.

Module Sapling.
  Module Id.

The encoding [Alpha_context.Sapling.Id.encoding] is valid.

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

Module Delegate.
  (* @TODO: validity of functions of this module *)
End Delegate.

Module Stake_distribution.
  (* @TODO: validity of functions of this module *)
End Stake_distribution.

Module Consensus.
  (* @TODO: validity of functions of this module *)
End Consensus.

The function [prepare_first_block] is valid. Lemma prepare_first_block_is_valid chain_id standalone typecheck level timestamp (H_standalone : Raw_context.standalone.Valid.simulation standalone) (H_typecheck : forall ctxt script, Raw_context.Valid.t ctxt -> letP? '(_, ctxt) := typecheck ctxt script in Raw_context.Valid.t ctxt ) (H_level : Int32.Valid.t level) (H_timestamp : Time.Valid.t timestamp) : letP? ctxt := Alpha_context.prepare_first_block chain_id (Raw_context.to_context standalone) typecheck level timestamp in Raw_context.Valid.t ctxt. Proof. now apply Init_storage.prepare_first_block_is_valid. Qed.

The function [prepare] is valid.

Lemma prepare_is_valid standalone level predecessor_timestamp timestamp
  (H_ctxt : Raw_context.standalone.Valid.simulation standalone)
  (H_level : Int32.Valid.t level)
  (H_predecessor_timestamp : Time.Valid.t predecessor_timestamp)
  (H_timestamp : Time.Valid.t timestamp) :
  letP? '(ctxt, updates, migrations) :=
    Alpha_context.prepare (Raw_context.to_context standalone)
      level predecessor_timestamp timestamp in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates ∧
  List.Forall Migration_repr.origination_result.Valid.t migrations.
Proof.
Admitted.

The function [finalize] is valid.

Lemma finalize_is_valid message ctxt fitness :
  Raw_context.Valid.t ctxt →
  letP? _ := Alpha_context.finalize message ctxt fitness in
  True.
Proof.
  intros.
  unfold Alpha_context.finalize.
  eapply Error.split_letP; [
    now apply Level_storage.last_allowed_fork_level_is_valid |
    easy
  ].
Qed.

The function [Alpha_context.record_dictator_proposal_seen] is valid.

Lemma record_dictator_proposal_seen_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  let res := Alpha_context.record_dictator_proposal_seen ctxt in
  Raw_context.Valid.t res.
Proof.
Admitted.

The function [fresh_internal_nonce] is valid.

Lemma fresh_internal_nonce_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt,i) := Alpha_context.fresh_internal_nonce ctxt in
  Raw_context.Valid.t ctxt ∧
  Pervasives.Int.Valid.t i.
Proof.
Admitted.