Skip to main content

💸 Operation_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require Import TezosOfOCaml.Proto_alpha.Operation_repr.

Require TezosOfOCaml.Environment.V7.Proofs.Ed25519.
Require TezosOfOCaml.Environment.V7.Proofs.Operation.
Require TezosOfOCaml.Environment.V7.Proofs.Operation_hash.
Require TezosOfOCaml.Environment.V7.Proofs.Protocol_hash.
Require TezosOfOCaml.Environment.V7.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_endorsement_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_int.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_proof.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_reveal_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Zk_rollup_account_repr.

Consensus content


Module consensus_content.
  Module Valid.
    Import Proto_alpha.Operation_repr.consensus_content.

The validity predicate for the type [Operation_repr.consensus_content].
    Record t (x : Operation_repr.consensus_content) : Prop := {
      slot : Slot_repr.Valid.t x.(slot);
      level : Raw_level_repr.Valid.t x.(level);
      round : Round_repr.Valid.t x.(round);
    }.
  End Valid.
End consensus_content.

The encoding [consensus_content_encoding] is valid
Lemma consensus_content_encoding_is_valid :
  Data_encoding.Valid.t consensus_content.Valid.t
    Operation_repr.consensus_content_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve consensus_content_encoding_is_valid
  : Data_encoding_db.

Validity predicates for the [manager_operation] type
Module manager_operation.
  Module Transaction.
    Module Valid.
      Import Proto_alpha.Operation_repr.manager_operation.Transaction.

      Record t (x : manager_operation.Transaction) : Prop := {
        amount : Tez_repr.Valid.t x.(amount);
        entrypoint : Entrypoint_repr.Valid.t x.(entrypoint);
      }.
    End Valid.
  End Transaction.

  Module Origination.
    Module Valid.
      Import Proto_alpha.Operation_repr.manager_operation.Origination.

      Record t (x : manager_operation.Origination) : Prop := {
        credit : Tez_repr.Valid.t x.(credit);
      }.
    End Valid.
  End Origination.

  Module Tx_rollup_commit.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Tx_rollup_commit.

      Record t (x : manager_operation.Tx_rollup_commit) : Prop := {
        commitment :
          Tx_rollup_commitment_repr.Full.Valid.t x.(commitment);
      }.
    End Valid.
  End Tx_rollup_commit.

  Module Tx_rollup_submit_batch.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Tx_rollup_submit_batch.

      Record t (x : manager_operation.Tx_rollup_submit_batch) : Prop := {
        burn_limit : Option.Forall Tez_repr.Valid.t x.(burn_limit);
        content : String.Int_length.t x.(content) ;
      }.
    End Valid.
  End Tx_rollup_submit_batch.

  Module Tx_rollup_rejection.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Tx_rollup_rejection.

      Record t (x : manager_operation.Tx_rollup_rejection) : Prop := {
        level : Raw_level_repr.Valid.t x.(level);
        message : Tx_rollup_message_repr.Valid.t x.(message);
        message_position :
          Pervasives.Int31.Valid.non_negative x.(message_position);
      }.
    End Valid.
  End Tx_rollup_rejection.

  Module Sc_rollup_publish.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Sc_rollup_publish.

      Record t (x : manager_operation.Sc_rollup_publish) : Prop := {
        commitment :
          Sc_rollup_commitment_repr.V1.Valid.t x.(commitment);
      }.
    End Valid.
  End Sc_rollup_publish.

  Module Tx_rollup_dispatch_tickets.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Tx_rollup_dispatch_tickets.

Validity predicate for the [manager_operation.Tx_rollup_dispatch_tickets] type
      Record t (x : manager_operation.Tx_rollup_dispatch_tickets) : Prop
        := {
        level : Tx_rollup_level_repr.Valid.t x.(level) ;
        message_index : Pervasives.Int.Valid.t x.(message_index) ;
        tickets_info : Forall
          (fun tx_rollup_reveal
             Tx_rollup_reveal_repr.Valid.t tx_rollup_reveal)
          x.(tickets_info);
      }.
    End Valid.
  End Tx_rollup_dispatch_tickets.

  Module Transfer_ticket.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Transfer_ticket.

Validity predicate for the [manager_operation.Transfer_ticket] type
      Record t (x : manager_operation.Transfer_ticket) : Prop := {
        amount : Ticket_amount.Valid.t x.(amount);
      }.
    End Valid.
  End Transfer_ticket.

  Module Dal_publish_slot_header.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Dal_publish_slot_header.

Validity predicate for the [manager_operation.Dal_publish_slot_header] type
      Record t (x : manager_operation.Dal_publish_slot_header) : Prop := {
        slot : Dal_slot_repr.Valid.t x.(slot) ;
      }.
    End Valid.
  End Dal_publish_slot_header.

  Module Sc_rollup_refute.
    Module Valid.
    Import Proto_alpha.Operation_repr
      .manager_operation.Sc_rollup_refute.

Validity predicate for the [manager_operation.Sc_rollup_refute] type
      Record t (x : manager_operation.Sc_rollup_refute) : Prop := {
        refutation :
          match x.(refutation) with
          | Some refutation'
            Sc_rollup_game_repr.refutation.Valid.t refutation'
          | NoneTrue
          end
      }.
    End Valid.
  End Sc_rollup_refute.

  Module Sc_rollup_timeout.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Sc_rollup_timeout.

Validity predicate for the [manager_operation.Sc_rollup_timeout] type
    Record t (x : manager_operation.Sc_rollup_timeout) : Prop := {
      stakers : Sc_rollup_game_repr.Index.Valid.t x.(stakers) ;
    }.
    End Valid.
  End Sc_rollup_timeout.

  Module Sc_rollup_dal_slot_subscribe.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Sc_rollup_dal_slot_subscribe.

Validity predicate for the [manager_operation.Sc_rollup_dal_slot_subscribe] type
       Record t (x : manager_operation.Sc_rollup_dal_slot_subscribe)
         : Prop := {
         slot_index : Dal_slot_repr.Index.Valid.t x.(slot_index) ;
       }.
    End Valid.
  End Sc_rollup_dal_slot_subscribe.

  Module Zk_rollup_origination.
    Module Valid.
      Import Proto_alpha.Operation_repr
        .manager_operation.Zk_rollup_origination.

Validity predicate for the [manager_operation.Zk_rollup_origination] type @TODO [Valid] should perhaps be replaced with [non_negative], or positive (in the parent validity predicate [Zk_rollup_account_repr.static.Valid.t] as well).
      Record t (x : manager_operation.Zk_rollup_origination) : Prop := {
        state_length :
          Pervasives.Int31.Valid.t (Array.length x.(init_state));
        nb_ops : Pervasives.Int31.Valid.t x.(nb_ops) ;
      }.
    End Valid.
  End Zk_rollup_origination.

Validity predicate for the [Operation_repr.manager_operation] type.
  Module Valid.
    Definition t (x : Proto_alpha.Operation_repr.manager_operation)
      : Prop :=
      match x with
      | Reveal _True
      | Transaction xTransaction.Valid.t x
      | Origination xOrigination.Valid.t x
      | Delegation _True
      | Register_global_constant _True
      | Set_deposits_limit xOption.Forall Tez_repr.Valid.t x
      | Increase_paid_storage _True
      | Update_consensus_key _True
      | Tx_rollup_originationTrue
      | Tx_rollup_submit_batch xTx_rollup_submit_batch.Valid.t x
      | Tx_rollup_return_bond _True
      | Tx_rollup_finalize_commitment _True
      | Tx_rollup_remove_commitment _True
      | Tx_rollup_rejection xTx_rollup_rejection.Valid.t x
      | Tx_rollup_commit xTrue
      | Tx_rollup_dispatch_tickets x
          Tx_rollup_dispatch_tickets.Valid.t x
      | Transfer_ticket xTransfer_ticket.Valid.t x
      | Dal_publish_slot_header x
          Dal_publish_slot_header.Valid.t x
      | Sc_rollup_originate _True
      | Sc_rollup_add_messages _True
      | Sc_rollup_cement _True
      | Sc_rollup_publish xSc_rollup_publish.Valid.t x
      | Sc_rollup_refute xSc_rollup_refute.Valid.t x
      | Sc_rollup_timeout xSc_rollup_timeout.Valid.t x
      | Sc_rollup_execute_outbox_message _True
      | Sc_rollup_recover_bond _True
      | Sc_rollup_dal_slot_subscribe x
          Sc_rollup_dal_slot_subscribe.Valid.t x
      | Zk_rollup_origination xZk_rollup_origination.Valid.t x
      | Zk_rollup_publish xTrue
      end.
  End Valid.
End manager_operation.

Validity predicate for the [packed_manager_operation] type
Module packed_manager_operation.
  Module Valid.
    Definition t
      (x : Proto_alpha.Operation_repr.packed_manager_operation) : Prop :=
      let 'Manager x := x in
      manager_operation.Valid.t x.
  End Valid.
End packed_manager_operation.

Module contents.
Validity predicate for the [contents.Manager_operation] type
  Module Manager_operation.
    Module Valid.
      Import Proto_alpha.Operation_repr.contents.Manager_operation.
      Record t (mo : contents.Manager_operation) : Prop := {
        fee : Tez_repr.Valid.t mo.(fee);
        gas_limit : Gas_limit_repr.Arith.Integral.Valid.t
          mo.(gas_limit);
        operation : manager_operation.Valid.t mo.(operation);
      }.
    End Valid.
  End Manager_operation.

Validity predicate for the [contents.Double_baking_evidence] type
  Module Double_baking_evidence.
    Module Valid.
      Record t (e : contents.Double_baking_evidence) : Prop := {
        bh1 : Block_header_repr.Valid.t
          e.(contents.Double_baking_evidence.bh1);
        bh2 : Block_header_repr.Valid.t
          e.(contents.Double_baking_evidence.bh2);
      }.
    End Valid.
  End Double_baking_evidence.
End contents.

We emulate the contraints given by the OCaml's GADT on manager operations.
Module Operation_kind.
  Inductive t : Set :=
  | Preendorsement : t
  | Endorsement : t
  | Dal_slot_availability : t
  | Seed_nonce_revelation : t
  | Vdf_revelation : t
  | Double_preendorsement_evidence : t
  | Double_endorsement_evidence : t
  | Double_baking_evidence : t
  | Activate_account : t
  | Proposals : t
  | Ballot : t
  | Drain_delegate : t
  | Failing_noop : t
  | Manager_operation : t.
End Operation_kind.

Module Valid.
Validity predicate for [contents] type
  Inductive contents
    : Operation_kind.t Operation_repr.contents Prop :=
  | Preendoresement pe :
    contents Operation_kind.Preendorsement (Preendorsement pe)
  | Endorsement e :
    contents Operation_kind.Endorsement (Endorsement e)
  | Dal_slot_availability pkhash dal :
    Dal_endorsement_repr.Valid.t dal
    contents Operation_kind.Dal_slot_availability
      (Dal_slot_availability pkhash dal)
  | Seed_nonce_revelation s :
    Raw_level_repr.Valid.t s
      .(contents.Seed_nonce_revelation.level)
    contents Operation_kind.Seed_nonce_revelation
      (Seed_nonce_revelation s)
  | Vdf_revelation vdf :
    contents Operation_kind.Vdf_revelation
      (Vdf_revelation vdf)
  | Double_preendorsement_evidence e :
    operation
      Operation_kind.Double_preendorsement_evidence
      e.(contents.Double_preendorsement_evidence.op1)
    operation
      Operation_kind.Double_preendorsement_evidence
      e.(contents.Double_preendorsement_evidence.op2)
    contents Operation_kind.Double_preendorsement_evidence
      (Double_preendorsement_evidence e)
  | Double_endorsement_evidence e :
    operation
      Operation_kind.Double_endorsement_evidence
      e.(contents.Double_endorsement_evidence.op1)
    operation
      Operation_kind.Double_endorsement_evidence
      e.(contents.Double_endorsement_evidence.op2)
    contents Operation_kind.Double_endorsement_evidence
      (Double_endorsement_evidence e)
  | Double_baking_evidence e :
    contents.Double_baking_evidence.Valid.t e
    contents Operation_kind.Double_baking_evidence
      (Double_baking_evidence e)
  | Activate_account a :
      contents Operation_kind.Activate_account (Activate_account a)
  | Proposals p :
    contents Operation_kind.Proposals (Proposals p)
  | Ballot b :
    contents Operation_kind.Ballot (Ballot b)
  | Drain_delegate d :
    contents Operation_kind.Drain_delegate (Drain_delegate d)
  | Failing_noop f :
    contents Operation_kind.Failing_noop (Failing_noop f)
  | Manager_operation mo :
    contents.Manager_operation.Valid.t mo
    contents Operation_kind.Manager_operation (Manager_operation mo)

  
Validity predicate for [contents_list] type
Validity predicate for [protocol_data] type
  with protocol_data :
    Operation_kind.t protocol_data Prop :=
  | Protocol_data kind p :
    contents_list kind p.(protocol_data.contents)
    protocol_data kind p

  
Validity predicate for [operation] type
  with operation :
    Operation_kind.t operation Prop :=
  | Operation kind op :
    protocol_data kind op.(operation.protocol_data)
    operation kind op.

[contents_list kind c cs] implies that [c] is [Operation_repr.Manager_operation _], [kind] is [Operation_kind.Manager_operation], and [cs] is valid
  Lemma contents_list_is_valid kind c cs :
    contents_list kind (Operation_repr.Cons c cs)
    match c with
    | Operation_repr.Manager_operation mo
        kind = Operation_kind.Manager_operation
          contents_list Operation_kind.Manager_operation cs
    | _False
    end.
  Proof.
    intros.
    destruct c eqn:?, kind; cbn in *; inversion H; trivial;
      inversion H2.
    now split.
  Qed.
End Valid.

Module packed_contents.
  Module Valid.
Validity predicate for the [packed_contents] type
    Definition t (kind : Operation_kind.t)
      (x : Proto_alpha.Operation_repr.packed_contents) : Prop :=
      let 'Contents c := x in
      Valid.contents kind c.
  End Valid.
End packed_contents.

Module packed_contents_list.
  Module Valid.
Validity predicate for the [packed_contents_list] type
    Definition t (kind : Operation_kind.t)
      (x : Operation_repr.packed_contents_list) : Prop :=
      let 'Contents_list contents_list := x in
        Valid.contents_list kind contents_list.
  End Valid.
End packed_contents_list.

Module packed_protocol_data.
  Module Valid.
Validity predicate for the [packed_protocol_data] type
    Definition t (kind : Operation_kind.t)
      (x : Operation_repr.packed_protocol_data) : Prop :=
      let 'Operation_data x := x in
      packed_contents_list.Valid.t kind
        (Contents_list x.(protocol_data.contents))
      Option.Forall Signature.Valid.t x.(protocol_data.signature).
  End Valid.
End packed_protocol_data.

Module packed_operation.
  Module Valid.
Validity predicate for the [packed_operation] type
    Definition t (kind : Operation_kind.t)
      (x : Operation_repr.packed_operation) : Prop :=
      packed_protocol_data.Valid.t kind
        x.(packed_operation.protocol_data).
  End Valid.
End packed_operation.

Conversions to and from lists


(* This will simply proofs later by limiting unfolding. *)
Arguments Operation_repr.of_list_internal : simpl nomatch.

The function [of_list_internal] is valid
Fixpoint of_list_internal_is_valid l kind :
  List.Forall (packed_contents.Valid.t kind) l
  match Operation_repr.of_list_internal l with
  | Pervasives.Ok packed_l
    packed_contents_list.Valid.t kind packed_l
  | Pervasives.Error _True
  end.
Proof.
  intros H_valid.
  destruct l as [|[c1] l]; simpl; [easy|].
  destruct l eqn:H_l; simpl.
  { constructor. now inversion H_valid. }
  { assert (H := of_list_internal_is_valid l kind).
    rewrite H_l in H; simpl in H.
    match goal with
    | |- context[let? _ := ?e in _] ⇒ destruct e
    end; cbn; [|easy].
    do 2 step; trivial; cbn.
    step; cbn; [step; cbn in *; trivial|];
    destruct kind; cbn;
      try (inversion H_valid; inversion H2);
      sauto lq: on.
  }
Qed.

The function [of_list] is valid
Lemma of_list_is_valid (l : list Operation_repr.packed_contents) kind :
  List.Forall (packed_contents.Valid.t kind) l
  match Operation_repr.of_list l with
  | Pervasives.Ok packed_l
    packed_contents_list.Valid.t kind packed_l
  | Pervasives.Error _True
  end.
Proof.
  intros H_valid.
  unfold Operation_repr.of_list.
  specialize (of_list_internal_is_valid l) as H.
  step; cbn; hauto l:on.
Qed.

The functions [of_list_internal] and [to_list] are inverses
Lemma of_list_internal_to_list l kind :
  packed_contents_list.Valid.t kind l
  Operation_repr.of_list_internal (Operation_repr.to_list l) = return? l.
Proof.
  intros.
  destruct l. induction c; [easy|].
  cbn in ×.
  destruct (contents_list_to_list _); cbn in ×.
  { discriminate IHc; inversion H; sauto lq: on. }
  { destruct (of_list_internal _); cbn in *;
     [|discriminate IHc; inversion H; sauto lq: on].
    injection IHc as Hinj;
      [|sauto lq: on rew:off]. subst p0.
    pose proof (Valid.contents_list_is_valid _ _ _ H)
     as H_manager.
    destruct c; try contradiction.
    destruct H_manager as [H_manager H_manager'].
    subst kind. clear IHc.
    inversion H_manager'; [easy|].
    destruct c; inversion H0. easy.
  }
Qed.

The functions [of_list] and [to_list] are inverses
The functions [to_list] and [of_list_internal] are inverses
Lemma to_list_of_list_internal (l : list Operation_repr.packed_contents) :
  match Operation_repr.of_list_internal l with
  | Pervasives.Ok l'Operation_repr.to_list l' = l
  | Pervasives.Error _True
  end.
Proof.
  induction l as [|[o] os IHl]; simpl; [easy|].
  unfold Operation_repr.of_list_internal; fold Operation_repr.of_list_internal.
  destruct os eqn:H_os; [sfirstorder|].
  rewrite <- H_os in *; clear H_os.
  destruct (Operation_repr.of_list_internal _); hauto drew: off.
Qed.

The functions [to_list] and [of_list] are inverses
Lemma to_list_of_list (l : list Operation_repr.packed_contents) :
  match Operation_repr.of_list l with
  | Pervasives.Ok l'Operation_repr.to_list l' = l
  | Pervasives.Error _True
  end.
Proof.
  unfold Operation_repr.of_list.
  hfcrush use: to_list_of_list_internal.
Qed.

Encodings


Module Encoding.
  Module Manager_operations.
The [tx_rollup_batch_content] encoding is valid
    Lemma tx_rollup_batch_content_is_valid :
      Data_encoding.Valid.t (fun _True)
        Operation_repr.Encoding.Manager_operations.tx_rollup_batch_content.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve tx_rollup_batch_content_is_valid : Data_encoding_db.
  End Manager_operations.

  Module Preendorsement_operation.
    Module Valid.
Valid predicate for the [preendorsement_encoding_is_valid]
      Definition t (x : Operation_repr.operation) :=
        let x := x.(operation.protocol_data).(protocol_data.contents) in
        match x with
        | Single (Preendorsement x) ⇒ consensus_content.Valid.t x
        | _False
        end.
    End Valid.
  End Preendorsement_operation.

  Module Endorsement_operation.
    Module Valid.
Valid predicate for the [endorsement_encoding_is_valid]
      Definition t (x : Operation_repr.operation) :=
        let x := x.(operation.protocol_data).(protocol_data.contents) in
        match x with
        | Single (Endorsement x) ⇒ consensus_content.Valid.t x
        | _False
        end.
    End Valid.
  End Endorsement_operation.

The [preendorsement_encoding] encoding is valid
  Lemma preendorsement_encoding_is_valid :
    Data_encoding.Valid.t Preendorsement_operation.Valid.t
      Operation_repr.Encoding.preendorsement_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros x ?.
    destruct x, protocol_data, contents as [[]|]; try easy.
    hauto l: on.
  Qed.
  #[global] Hint Resolve preendorsement_encoding_is_valid : Data_encoding_db.

The [endorsement_encoding] encoding is valid
  Lemma endorsement_encoding_is_valid :
    Data_encoding.Valid.t Endorsement_operation.Valid.t
      Operation_repr.Encoding.endorsement_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros x ?.
    destruct x, protocol_data, contents as [[]|]; try easy.
    sauto.
  Qed.
  #[global] Hint Resolve endorsement_encoding_is_valid : Data_encoding_db.

The [manager_encoding] encoding is valid
  Lemma manager_encoding_is_valid :
    Data_encoding.Valid.t
      (fun '(_, fee, counter, gas_limit, storage_limit)
        Tez_repr.Valid.t fee
        0 counter
        Saturation_repr.Strictly_valid.t gas_limit
        Gas_limit_repr.Is_rounded.t gas_limit
        0 storage_limit
      )
      Operation_repr.Encoding.manager_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros x H.
    destruct x; destruct p; destruct p; destruct p.
    destruct H as [H1 [H2 [H3 H4]]].
    intuition. easy.
  Qed.
  #[global] Hint Resolve manager_encoding_is_valid : Data_encoding_db.

Experimental module to verify cases from [contents_encoding] independently.
  Module Make_manager_case.
    Module Valid.
The [make] function as extracted from [contents_encoding].
      Definition make : {A : Set},
        Encoding.case A Data_encoding.case packed_contents.
        match (
          eval cbv delta [Encoding.contents_encoding] in
          Encoding.contents_encoding
        ) with
        | let _ := ?f in _exact f
        end.
      Defined.

The validity of a single manager operation case.
      Definition t (title : string)
        (domain : packed_contents option Prop)
        (x : Encoding.Manager_operations.case) : Prop :=
         tag,
        let case := Encoding.make_manager_case tag x in
        Data_encoding.Valid.Case.t title tag domain (make case).
    End Valid.
  End Make_manager_case.

The validity domain of the [reveal_case].
  Definition reveal_case_domain (x : packed_contents) : option Prop :=
    match x with
    | Contents (Manager_operation {|
        contents.Manager_operation.operation := Reveal _
      |}) ⇒ Some ( kind, packed_contents.Valid.t kind x)
    | _None
    end.

The validity of the [reveal_case] encoding independently of the other cases.
  Lemma reveal_case_is_valid :
    Make_manager_case.Valid.t "Reveal" reveal_case_domain
      Encoding.Manager_operations.reveal_case.
  Proof.
    unfold Make_manager_case.Valid.t; intros.
    eapply Data_encoding.Valid.Case.intro_with_implies.
    { Data_encoding.Valid.data_encoding_auto. }
    { intros [[]]; simpl; trivial.
      destruct_all 'contents.Manager_operation; simpl.
      destruct_all manager_operation; trivial.
(* TODO: tactic fails
      sauto.
    }
  Qed.
*)

Admitted.

  (* @TODO: out of memory. I tried to verify things case by case but this is
     still very slow. *)

The [contents_encoding] encoding is valid
  Lemma contents_encoding_is_valid kind :
    Data_encoding.Valid.t (packed_contents.Valid.t kind)
      Operation_repr.Encoding.contents_encoding.
  Proof.
  Admitted.
  #[global] Hint Resolve contents_encoding_is_valid : Data_encoding_db.

The [contents_list_encoding] encoding is valid
  Lemma contents_list_encoding_is_valid kind :
    Data_encoding.Valid.t (fun xpacked_contents_list.Valid.t kind x)
      Operation_repr.Encoding.contents_list_encoding.
  Proof.
    intros.
    Data_encoding.Valid.data_encoding_auto.
    intros. split.
    { instantiate (1 := kind).
      destruct x, c as [|c' cs']; cbn.
      { cbn in ×. constructor; [|easy].
        cbn. now inversion H. }
      { constructor;
          [cbn in *; now inversion H|].
        induction cs' as [|? ? IHcs'];
          [sauto lq: on rew: off|].
        cbn in ×.
        constructor; [sauto lq: on rew: off|].
        apply IHcs'.
        inversion H. sauto lq: on rew: off.
      }
    }
    { now apply of_list_internal_to_list with (kind := kind). }
  Qed.
  #[global] Hint Resolve contents_list_encoding_is_valid : Data_encoding_db.

The [optional_signature_encoding] encoding is valid
  Lemma optional_signature_encoding_is_valid :
    Data_encoding.Valid.t (Option.Forall Signature.Valid.t)
      Operation_repr.Encoding.optional_signature_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros [] ?;
      match goal with
      | |- context[if ?e then _ else _] ⇒ destruct e eqn:?
      end;
      try tauto;
      try hauto use: Signature.equal_like_eq;
      sfirstorder use: Signature.equal_like_eq.
  Qed.
  #[global] Hint Resolve optional_signature_encoding_is_valid : Data_encoding_db.
The [protocol_data_encoding] encoding is valid
  Lemma protocol_data_encoding_is_valid kind :
     Data_encoding.Valid.t (packed_protocol_data.Valid.t kind)
      Operation_repr.Encoding.protocol_data_encoding.
  Proof.
    intros.
    Data_encoding.Valid.data_encoding_auto.
    hauto lq: on.
  Qed.
  #[global] Hint Resolve protocol_data_encoding_is_valid : Data_encoding_db.

The [operation_encoding] encoding is valid
  Lemma operation_encoding_is_valid kind :
    Data_encoding.Valid.t (packed_operation.Valid.t kind)
      Operation_repr.Encoding.operation_encoding.
  Proof.
    intros.
    Data_encoding.Valid.data_encoding_auto.
    intros. split_conj; [easy|..].
    { instantiate (1 := kind).
      apply H.
    }
    { split. }
  Qed.
  #[global] Hint Resolve operation_encoding_is_valid : Data_encoding_db.

The [unsigned_operation_encoding] encoding is valid
  Lemma unsigned_operation_encoding_is_valid kind :
    Data_encoding.Valid.t (fun '(_, x)packed_contents_list.Valid.t kind x)
      Operation_repr.Encoding.unsigned_operation_encoding.
  Proof.
    intros.
    Data_encoding.Valid.data_encoding_auto.
    intros. step; cbn; split; [easy|].
    eauto.
  Qed.
  #[global] Hint Resolve unsigned_operation_encoding_is_valid : Data_encoding_db.
End Encoding.

The [encoding] encoding is valid
Lemma encoding_is_valid kind :
  Data_encoding.Valid.t (packed_operation.Valid.t kind) encoding.
Proof.
  apply Encoding.operation_encoding_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

The [contents_encoding] encoding is valid
Lemma contents_encoding_is_valid kind :
  Data_encoding.Valid.t (packed_contents.Valid.t kind) contents_encoding.
Proof.
  apply Encoding.contents_encoding_is_valid.
Qed.
#[global] Hint Resolve contents_encoding_is_valid : Data_encoding_db.

The [contents_list_encoding] encoding is valid
Lemma contents_list_encoding_is_valid kind :
  Data_encoding.Valid.t (packed_contents_list.Valid.t kind) contents_list_encoding.
Proof.
  apply Encoding.contents_list_encoding_is_valid.
Qed.
#[global] Hint Resolve contents_list_encoding_is_valid : Data_encoding_db.

The [protocol_data_encoding] encoding is valid
Lemma protocol_data_encoding_is_valid kind :
  Data_encoding.Valid.t (packed_protocol_data.Valid.t kind)
    protocol_data_encoding.
  apply Encoding.protocol_data_encoding_is_valid.
Qed.
#[global] Hint Resolve protocol_data_encoding_is_valid : Data_encoding_db.

The [unsigned_operation_encoding] encoding is valid
Lemma unsigned_operation_encoding_is_valid kind :
  Data_encoding.Valid.t (fun '(_, x)packed_contents_list.Valid.t kind x)
    unsigned_operation_encoding.
  apply Encoding.unsigned_operation_encoding_is_valid.
Qed.
#[global] Hint Resolve unsigned_operation_encoding_is_valid : Data_encoding_db.

Equalities

The [equal_manager_operation_kind] is reflexive
Lemma equal_manager_operation_kind_refl op
  : Operation_repr.equal_manager_operation_kind op op = Some Operation_repr.Eq.
Proof.
  destruct op; reflexivity.
Qed.
The [Some Operation_repr.Eq] result from [equal_manager_operation_kind op1 op2] implies [op1 = op2]
The [equal_contents_kind] function is reflexive
Lemma equal_contents_kind_refl op
  : Operation_repr.equal_contents_kind op op = Some Operation_repr.Eq.
Proof.
  destruct op; try reflexivity.
  unfold Operation_repr.equal_contents_kind.
  now rewrite equal_manager_operation_kind_refl.
Qed.

The [equal_contents_kind_list] function is reflexive
Fixpoint equal_contents_kind_list_refl op
  : Operation_repr.equal_contents_kind_list op op = Some Operation_repr.Eq.
Proof.
  destruct op; unfold Operation_repr.equal_contents_kind_list.
  { apply equal_contents_kind_refl. }
  { rewrite equal_contents_kind_refl.
    fold Operation_repr.equal_contents_kind_list.
    now rewrite equal_contents_kind_list_refl.
  }
Qed.

The [equal] function is reflexive
Lemma equal_refl op
  : Operation_repr.equal op op = Some Operation_repr.Eq.
Proof.
  unfold Operation_repr.equal.
  assert (valid_compare :=
    Operation_hash.Included_HASH_is_valid
      .(S.HASH.Valid.MINIMAL_HASH)
      .(S.MINIMAL_HASH.Valid.Compare_S)).
  rewrite valid_compare.(Compare.S.Valid.eq).(Compare.S.Eq.equal).
  simpl.
  rewrite (Compare.Valid.refl (domain := fun _True) (f := id)); trivial.
  { now rewrite equal_contents_kind_list_refl. }
  { apply valid_compare.(Compare.S.Valid.compare). }
Qed.

The function [check_signature] is valid