💸 Operation_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Operation_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Ed25519.
Require TezosOfOCaml.Environment.V8.Proofs.Operation.
Require TezosOfOCaml.Environment.V8.Proofs.Operation_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Protocol_hash.
Require TezosOfOCaml.Environment.V8.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_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_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.
Require TezosOfOCaml.Proto_alpha.Proofs.Manager_counter_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Operation_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Ed25519.
Require TezosOfOCaml.Environment.V8.Proofs.Operation.
Require TezosOfOCaml.Environment.V8.Proofs.Operation_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Protocol_hash.
Require TezosOfOCaml.Environment.V8.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_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_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.
Require TezosOfOCaml.Proto_alpha.Proofs.Manager_counter_repr.
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.
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.
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.
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.
:= {
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.
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.
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'
| None ⇒ True
end
}.
End Valid.
End Sc_rollup_refute.
Module Sc_rollup_timeout.
Module Valid.
Import Proto_alpha.Operation_repr
.manager_operation.Sc_rollup_timeout.
refutation :
match x.(refutation) with
| Some refutation' ⇒
Sc_rollup_game_repr.refutation.Valid.t refutation'
| None ⇒ True
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 Zk_rollup_origination.
Module Valid.
Import Proto_alpha.Operation_repr
.manager_operation.Zk_rollup_origination.
stakers : Sc_rollup_game_repr.Index.Valid.t x.(stakers) ;
}.
End Valid.
End Sc_rollup_timeout.
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.
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 x ⇒ Transaction.Valid.t x
| Origination x ⇒ Origination.Valid.t x
| Delegation _ ⇒ True
| Register_global_constant _ ⇒ True
| Set_deposits_limit x ⇒ Option.Forall Tez_repr.Valid.t x
| Increase_paid_storage _ ⇒ True
| Update_consensus_key _ ⇒ True
| Tx_rollup_origination ⇒ True
| Tx_rollup_submit_batch x ⇒ Tx_rollup_submit_batch.Valid.t x
| Tx_rollup_return_bond _ ⇒ True
| Tx_rollup_finalize_commitment _ ⇒ True
| Tx_rollup_remove_commitment _ ⇒ True
| Tx_rollup_rejection x ⇒ Tx_rollup_rejection.Valid.t x
| Tx_rollup_commit x ⇒ True
| Tx_rollup_dispatch_tickets x ⇒
Tx_rollup_dispatch_tickets.Valid.t x
| Transfer_ticket x ⇒ Transfer_ticket.Valid.t x
| Dal_publish_slot_header x ⇒ True
| Sc_rollup_originate _ ⇒ True
| Sc_rollup_add_messages _ ⇒ True
| Sc_rollup_cement _ ⇒ True
| Sc_rollup_publish x ⇒ Sc_rollup_publish.Valid.t x
| Sc_rollup_refute x ⇒ Sc_rollup_refute.Valid.t x
| Sc_rollup_timeout x ⇒ Sc_rollup_timeout.Valid.t x
| Sc_rollup_execute_outbox_message _ ⇒ True
| Sc_rollup_recover_bond _ ⇒ True
| Zk_rollup_origination x ⇒ Zk_rollup_origination.Valid.t x
| Zk_rollup_publish x ⇒ True
| Zk_rollup_update x ⇒ True
end.
End Valid.
End manager_operation.
Definition t (x : Proto_alpha.Operation_repr.manager_operation)
: Prop :=
match x with
| Reveal _ ⇒ True
| Transaction x ⇒ Transaction.Valid.t x
| Origination x ⇒ Origination.Valid.t x
| Delegation _ ⇒ True
| Register_global_constant _ ⇒ True
| Set_deposits_limit x ⇒ Option.Forall Tez_repr.Valid.t x
| Increase_paid_storage _ ⇒ True
| Update_consensus_key _ ⇒ True
| Tx_rollup_origination ⇒ True
| Tx_rollup_submit_batch x ⇒ Tx_rollup_submit_batch.Valid.t x
| Tx_rollup_return_bond _ ⇒ True
| Tx_rollup_finalize_commitment _ ⇒ True
| Tx_rollup_remove_commitment _ ⇒ True
| Tx_rollup_rejection x ⇒ Tx_rollup_rejection.Valid.t x
| Tx_rollup_commit x ⇒ True
| Tx_rollup_dispatch_tickets x ⇒
Tx_rollup_dispatch_tickets.Valid.t x
| Transfer_ticket x ⇒ Transfer_ticket.Valid.t x
| Dal_publish_slot_header x ⇒ True
| Sc_rollup_originate _ ⇒ True
| Sc_rollup_add_messages _ ⇒ True
| Sc_rollup_cement _ ⇒ True
| Sc_rollup_publish x ⇒ Sc_rollup_publish.Valid.t x
| Sc_rollup_refute x ⇒ Sc_rollup_refute.Valid.t x
| Sc_rollup_timeout x ⇒ Sc_rollup_timeout.Valid.t x
| Sc_rollup_execute_outbox_message _ ⇒ True
| Sc_rollup_recover_bond _ ⇒ True
| Zk_rollup_origination x ⇒ Zk_rollup_origination.Valid.t x
| Zk_rollup_publish x ⇒ True
| Zk_rollup_update x ⇒ True
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.
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.
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.
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_attestation : 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.
Inductive t : Set :=
| Preendorsement : t
| Endorsement : t
| Dal_attestation : 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_attestation dal :
contents Operation_kind.Dal_attestation
(Dal_attestation 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)
: Operation_kind.t → Operation_repr.contents → Prop :=
| Preendoresement pe :
contents Operation_kind.Preendorsement (Preendorsement pe)
| Endorsement e :
contents Operation_kind.Endorsement (Endorsement e)
| Dal_attestation dal :
contents Operation_kind.Dal_attestation
(Dal_attestation 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
with contents_list :
Operation_kind.t → contents_list → Prop :=
| Cons c cs :
contents Operation_kind.Manager_operation c →
contents_list Operation_kind.Manager_operation cs →
contents_list Operation_kind.Manager_operation (Cons c cs)
| Single kind c :
contents kind c →
contents_list kind (Single c)
Operation_kind.t → contents_list → Prop :=
| Cons c cs :
contents Operation_kind.Manager_operation c →
contents_list Operation_kind.Manager_operation cs →
contents_list Operation_kind.Manager_operation (Cons c cs)
| Single kind c :
contents kind c →
contents_list kind (Single c)
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
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.
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.
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.
(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.
(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.
(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.
(x : Operation_repr.packed_operation) : Prop :=
packed_protocol_data.Valid.t kind
x.(packed_operation.protocol_data).
End Valid.
End packed_operation.
(* 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.
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.
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.
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
Lemma of_list_to_list (l : Operation_repr.packed_contents_list) :
∀ kind,
packed_contents_list.Valid.t kind l →
Operation_repr.of_list (Operation_repr.to_list l) = return? l.
Proof.
unfold Operation_repr.of_list.
hauto lq: on use: of_list_internal_to_list.
Qed.
∀ kind,
packed_contents_list.Valid.t kind l →
Operation_repr.of_list (Operation_repr.to_list l) = return? l.
Proof.
unfold Operation_repr.of_list.
hauto lq: on use: of_list_internal_to_list.
Qed.
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.
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.
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.
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.
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.
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.
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.
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.
unfold Manager_counter_repr.Valid.t.
lia.
hauto lq: on.
Qed.
#[global] Hint Resolve manager_encoding_is_valid : Data_encoding_db.
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.
unfold Manager_counter_repr.Valid.t.
lia.
hauto lq: on.
Qed.
#[global] Hint Resolve manager_encoding_is_valid : Data_encoding_db.
Experimental module to verify cases from [contents_encoding]
independently.
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.
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.
(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.
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. *)
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.
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 x ⇒ packed_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.
Data_encoding.Valid.t (fun x ⇒ packed_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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Lemma equal_manager_operation_kind_refl op
: Operation_repr.equal_manager_operation_kind op op = Some Operation_repr.Eq.
Proof.
destruct op; reflexivity.
Qed.
: 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]
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.
Proof.
destruct op1, op2; cbv; congruence.
Qed.
: Operation_repr.equal_manager_operation_kind op1 op2 = Some Operation_repr.Eq →
Operation_repr.manager_kind op1 = Operation_repr.manager_kind op2.
Proof.
destruct op1, op2; cbv; congruence.
Qed.
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.
: 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.
: 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.is_Make).(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.
: 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.is_Make).(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
Lemma check_signature_is_valid consensus_pk chain_id op :
letP? x := Operation_repr.check_signature consensus_pk chain_id op in
True.
Proof.
Admitted.
letP? x := Operation_repr.check_signature consensus_pk chain_id op in
True.
Proof.
Admitted.