Skip to main content

💸 Operation_repr.v

Proofs

See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Ed25519.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Operation.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Operation_hash.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Protocol_hash.
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.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_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.Tx_rollup_commitment_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.Vote_repr.

Consensus content


Module Consensus_content.
  Module Valid.
    Import 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.

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's GADT

We emulate the contraints given by the OCaml's GADT on manager operations.

Module Manager.
A tag to emulate the filtering over manager operations in the OCaml's GADT of the operations.
  Module Operation_kind.
    Inductive t : Set :=
    | Any : t
    | Manager : t.
  End Operation_kind.

  Module Contents.
    Module Valid.
      Definition t (kind : Operation_kind.t)
        (contents : Operation_repr.contents) : Prop :=
        match kind, contents with
        | Operation_kind.Any, _True
        | Operation_kind.Manager, Manager_operation _True
        | Operation_kind.Manager, _False
        end.

      Lemma manager_implies_any contents :
        t Operation_kind.Manager contents
        t Operation_kind.Any contents.
        now destruct contents.
      Qed.
    End Valid.
  End Contents.

  Module Contents_list.
    Module Valid.
      Fixpoint t (kind : Operation_kind.t)
        (contents_list : Operation_repr.contents_list) : Prop :=
        match contents_list with
        | Single contentsContents.Valid.t kind contents
        | Cons contents contents_list
          Contents.Valid.t Operation_kind.Manager contents
          t Operation_kind.Manager contents_list
        end.

      Lemma manager_implies_any contents_list :
        t Operation_kind.Manager contents_list
        t Operation_kind.Any contents_list.
        now destruct contents_list.
      Qed.
    End Valid.
  End Contents_list.

  Module Protocol_data.
    Module Valid.
      Definition t (kind : Operation_kind.t)
        (protocol_data : Operation_repr.protocol_data) : Prop :=
        Contents_list.Valid.t kind protocol_data.(protocol_data.contents).

      Lemma manager_implies_any protocol_data :
        t Operation_kind.Manager protocol_data
        t Operation_kind.Any protocol_data.
        sfirstorder use: Contents_list.Valid.manager_implies_any.
      Qed.
    End Valid.
  End Protocol_data.

  Module Packed_contents_list.
    Module Valid.
      Definition t (kind : Operation_kind.t)
        (packed_contents_list : Operation_repr.packed_contents_list) : Prop :=
        let 'Contents_list contents_list := packed_contents_list in
        Contents_list.Valid.t kind contents_list.

      Lemma manager_implies_any packed_contents_list :
        t Operation_kind.Manager packed_contents_list
        t Operation_kind.Any packed_contents_list.
        destruct packed_contents_list; simpl.
        apply Contents_list.Valid.manager_implies_any.
      Qed.
    End Valid.
  End Packed_contents_list.

  Module Packed_protocol_data.
    Module Valid.
      Definition t (kind : Operation_kind.t)
        (packed_protocol_data : Operation_repr.packed_protocol_data) : Prop :=
        let 'Operation_data protocol_data := packed_protocol_data in
        Protocol_data.Valid.t kind protocol_data.

      Lemma manager_implies_any packed_protocol_data :
        t Operation_kind.Manager packed_protocol_data
        t Operation_kind.Any packed_protocol_data.
        sauto lq: on use: Protocol_data.Valid.manager_implies_any.
      Qed.
    End Valid.
  End Packed_protocol_data.

  Module Packed_operation.
    Module Valid.
      Definition t (kind : Operation_kind.t)
        (packed_operation : Operation_repr.packed_operation) : Prop :=
        Packed_protocol_data.Valid.t kind
          packed_operation.(packed_operation.protocol_data).

      Lemma manager_implies_any packed_operation :
        t Operation_kind.Manager packed_operation
        t Operation_kind.Any packed_operation.
        sfirstorder use: Packed_protocol_data.Valid.manager_implies_any.
      Qed.
    End Valid.
  End Packed_operation.
End Manager.

General validity predicates


Module Manager_operation.
  Module Transaction.
    Module Valid.
      Import transaction.

      Record t (x : 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 origination.

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

  Module Tx_rollup_commit.
    Module Valid.
      Import manager_operation.Tx_rollup_commit.

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

  Module Tx_rollup_submit_batch.
    Module Valid.
      Import 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);
      }.
    End Valid.
  End Tx_rollup_submit_batch.

  Module Tx_rollup_rejection.
    Module Valid.
      Import 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 manager_operation.Sc_rollup_publish.

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

  Module Valid.
    Definition t (x : 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
      | 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 xTrue
      | Transfer_ticket xTrue
      | Sc_rollup_originate _True
      | Sc_rollup_add_messages _True
      | Sc_rollup_cement _True
      | Sc_rollup_publish xSc_rollup_publish.Valid.t x
      end.
  End Valid.
End Manager_operation.

Module Packed_manager_operation.
  Module Valid.
    Definition t (x : Operation_repr.packed_manager_operation) : Prop :=
      let 'Manager x := x in
      Manager_operation.Valid.t x.
  End Valid.
End Packed_manager_operation.

Module Preendorsement_operation.
  Module 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.
    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.

Module Packed_contents.
  Module Valid.
    Definition t (x : Operation_repr.packed_contents) : Prop :=
      let 'Contents x := x in
      match x with
      | Preendorsement xConsensus_content.Valid.t x
      | Endorsement xConsensus_content.Valid.t x
      | Seed_nonce_revelation x
        Raw_level_repr.Valid.t x.(contents.Seed_nonce_revelation.level)
        Seed_repr.Nonce.Valid.t x.(contents.Seed_nonce_revelation.nonce)
      | Double_preendorsement_evidence x
        Preendorsement_operation.Valid.t
          x.(contents.Double_preendorsement_evidence.op1)
        Preendorsement_operation.Valid.t
          x.(contents.Double_preendorsement_evidence.op2)
      | Double_endorsement_evidence x
        Endorsement_operation.Valid.t
          x.(contents.Double_endorsement_evidence.op1)
        Endorsement_operation.Valid.t
          x.(contents.Double_endorsement_evidence.op2)
      | Double_baking_evidence x
        Block_header_repr.Protocol_data.Valid.t
          x.(contents.Double_baking_evidence.bh1)
            .(Block_header_repr.t.protocol_data)
        Block_header_repr.Protocol_data.Valid.t
          x.(contents.Double_baking_evidence.bh2)
            .(Block_header_repr.t.protocol_data)
      | Activate_account x
        Blinded_public_key_hash.Activation_code.Valid.t
          x.(contents.Activate_account.activation_code)
      | Proposals xInt32.Valid.t x.(contents.Proposals.period)
      | Ballot xInt32.Valid.t x.(contents.Ballot.period)
      | Failing_noop _True
      | Manager_operation x
        Tez_repr.Valid.t x.(contents.Manager_operation.fee)
        0 x.(contents.Manager_operation.counter)
        Packed_manager_operation.Valid.t
          (Manager x.(contents.Manager_operation.operation))
        Saturation_repr.Valid.t x.(contents.Manager_operation.gas_limit)
        Gas_limit_repr.Is_rounded.t x.(contents.Manager_operation.gas_limit)
        0 x.(contents.Manager_operation.storage_limit)
      end.
  End Valid.
End Packed_contents.

Module Packed_contents_list.
  Module Valid.
    Definition t (x : Operation_repr.packed_contents_list) : Prop :=
      Manager.Packed_contents_list.Valid.t Manager.Operation_kind.Any x
      List.Forall Packed_contents.Valid.t (Operation_repr.to_list x).
  End Valid.
End Packed_contents_list.

Module Optional_signature.
  Module Valid.
    Definition t (x : option Signature.t) : Prop :=
      match x with
      | Some xx Signature.zero
      | NoneTrue
      end.
  End Valid.
End Optional_signature.

Module Packed_protocol_data.
  Module Valid.
    Definition t (x : Operation_repr.packed_protocol_data) : Prop :=
      let 'Operation_data x := x in
      Packed_contents_list.Valid.t
        (Contents_list x.(protocol_data.contents))
      Optional_signature.Valid.t x.(protocol_data.signature).
  End Valid.
End Packed_protocol_data.

Module Packed_operation.
  Module Valid.
    Definition t (x : Operation_repr.packed_operation) : Prop :=
      Packed_protocol_data.Valid.t 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.

Fixpoint of_list_internal_is_valid (l : list Operation_repr.packed_contents) :
  match Operation_repr.of_list_internal l with
  | Pervasives.Ok packed_l
    Manager.Packed_contents_list.Valid.t Manager.Operation_kind.Any packed_l
  | Pervasives.Error _True
  end.
  destruct l as [|[c1] l]; simpl; [easy|].
  destruct l eqn:H_l; simpl; [easy|].
  assert (H := of_list_internal_is_valid l).
  rewrite H_l in H; simpl in H.
  match goal with
  | |- context[let? _ := ?e in _] ⇒ destruct e; sauto
  end.
Qed.

Lemma of_list_is_valid (l : list Operation_repr.packed_contents) :
  match Operation_repr.of_list l with
  | Pervasives.Ok packed_l
    Manager.Packed_contents_list.Valid.t Manager.Operation_kind.Any packed_l
  | Pervasives.Error _True
  end.
  unfold Operation_repr.of_list.
  hfcrush use: of_list_internal_is_valid.
Qed.

Lemma of_list_internal_to_list (l : Operation_repr.packed_contents_list) :
   kind,
  Manager.Packed_contents_list.Valid.t kind l
  Operation_repr.of_list_internal (Operation_repr.to_list l) = return? l.
  destruct l as [l]; simpl.
  induction l as [|c ? IHl]; simpl in *; [easy|]; intros ? [H_c H_l].
  destruct c; try tauto; clear H_c.
  assert (IH := IHl _ H_l); clear IHl.
  destruct (Operation_repr.contents_list_to_list _) as [|[o] os]; simpl in *;
    [sauto q: on|].
  destruct os; simpl in ×.
  { inversion IH; hauto lq: on rew: off. }
  { destruct (Operation_repr.of_list_internal _) as [[]|]; simpl in *;
      sauto q: on.
  }
Qed.

Lemma of_list_to_list (l : Operation_repr.packed_contents_list) :
   kind,
  Manager.Packed_contents_list.Valid.t kind l
  Operation_repr.of_list (Operation_repr.to_list l) = return? l.
  unfold Operation_repr.of_list.
  hauto lq: on use: of_list_internal_to_list.
Qed.

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.
  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.

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.
  unfold Operation_repr.of_list.
  hfcrush use: to_list_of_list_internal.
Qed.

Encodings


Module Encoding.
  Module Manager_operations.
    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.

  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.

  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.

  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.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.
  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 (Packed_contents.Valid.t 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.
      sauto.
    }
  Qed.

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

  Lemma contents_encoding_is_valid :
    Data_encoding.Valid.t Packed_contents.Valid.t
      Operation_repr.Encoding.contents_encoding.
  Proof.
  Admitted.
  #[global] Hint Resolve contents_encoding_is_valid : Data_encoding_db.

  Lemma contents_list_encoding_is_valid :
    Data_encoding.Valid.t Packed_contents_list.Valid.t
      Operation_repr.Encoding.contents_list_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    hauto lq: on use: of_list_internal_to_list.
  Qed.
  #[global] Hint Resolve contents_list_encoding_is_valid : Data_encoding_db.

  Lemma optional_signature_encoding_is_valid :
    Data_encoding.Valid.t Optional_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.

  Lemma protocol_data_encoding_is_valid :
    Data_encoding.Valid.t Packed_protocol_data.Valid.t
      Operation_repr.Encoding.protocol_data_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    hauto lq: on.
  Qed.
  #[global] Hint Resolve protocol_data_encoding_is_valid : Data_encoding_db.

  Lemma operation_encoding_is_valid :
    Data_encoding.Valid.t Packed_operation.Valid.t
      Operation_repr.Encoding.operation_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve operation_encoding_is_valid : Data_encoding_db.

  Lemma unsigned_operation_encoding_is_valid :
    Data_encoding.Valid.t (fun '(_, x)Packed_contents_list.Valid.t x)
      Operation_repr.Encoding.unsigned_operation_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve unsigned_operation_encoding_is_valid : Data_encoding_db.
End Encoding.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Packed_operation.Valid.t encoding.
Proof.
  exact Encoding.operation_encoding_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma contents_encoding_is_valid :
  Data_encoding.Valid.t Packed_contents.Valid.t contents_encoding.
Proof.
  exact Encoding.contents_encoding_is_valid.
Qed.
#[global] Hint Resolve contents_encoding_is_valid : Data_encoding_db.

Lemma contents_list_encoding_is_valid :
  Data_encoding.Valid.t Packed_contents_list.Valid.t contents_list_encoding.
Proof.
  exact Encoding.contents_list_encoding_is_valid.
Qed.
#[global] Hint Resolve contents_list_encoding_is_valid : Data_encoding_db.

Lemma protocol_data_encoding_is_valid :
  Data_encoding.Valid.t Packed_protocol_data.Valid.t
    protocol_data_encoding.
  exact Encoding.protocol_data_encoding_is_valid.
Qed.
#[global] Hint Resolve protocol_data_encoding_is_valid : Data_encoding_db.

Lemma unsigned_operation_encoding_is_valid :
  Data_encoding.Valid.t (fun '(_, x)Packed_contents_list.Valid.t x)
    unsigned_operation_encoding.
  exact Encoding.unsigned_operation_encoding_is_valid.
Qed.
#[global] Hint Resolve unsigned_operation_encoding_is_valid : Data_encoding_db.

The number of acceptable passes is either zero or one.
Lemma acceptable_passes_size kind (op : Operation_repr.packed_operation) :
  Manager.Packed_operation.Valid.t kind op
  let passes := Operation_repr.acceptable_passes op in
  List.length passes = 0 List.length passes = 1.
  destruct op; destruct protocol_data as [[contents]]; simpl.
  unfold Manager.Protocol_data.Valid.t; simpl.
  hauto q: on.
Qed.

Equalities


Lemma equal_manager_operation_kind_refl op
  : Operation_repr.equal_manager_operation_kind op op = Some Operation_repr.Eq.
  destruct op; reflexivity.
Qed.

Lemma equal_manager_operation_kind_implies_eq op1 op2
  : Operation_repr.equal_manager_operation_kind op1 op2 = Some Operation_repr.Eq
  Operation_repr.manager_kind op1 = Operation_repr.manager_kind op2.
  destruct op1, op2; cbv; congruence.
Qed.

Lemma equal_contents_kind_refl op
  : Operation_repr.equal_contents_kind op op = Some Operation_repr.Eq.
  destruct op; try reflexivity.
  unfold Operation_repr.equal_contents_kind.
  now rewrite equal_manager_operation_kind_refl.
Qed.

Fixpoint equal_contents_kind_list_refl op
  : Operation_repr.equal_contents_kind_list op op = Some Operation_repr.Eq.
  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.

Lemma equal_refl op
  : Operation_repr.equal op op = Some Operation_repr.Eq.
  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.