🦏 Sc_rollup_inbox_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require Import TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Context.
Require TezosOfOCaml.Environment.V8.Proofs.Context_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Bounded_history_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_inbox_merkelized_payload_hashes_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Skip_list_repr.
Module Hash.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require Import TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Context.
Require TezosOfOCaml.Environment.V8.Proofs.Context_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Bounded_history_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_inbox_merkelized_payload_hashes_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Skip_list_repr.
Module Hash.
[hash_encoding] is valid
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_inbox_repr.Hash.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
End Hash.
#[global] Hint Resolve Hash.encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_inbox_repr.Hash.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
End Hash.
#[global] Hint Resolve Hash.encoding_is_valid : Data_encoding_db.
Validity of [old_level_messages]
Module old_levels_messages.
Module Valid.
Record t `{Skip_list_repr.Make.FArgs}
(r : Skip_list_repr.Make.cell.record
Sc_rollup_inbox_repr.Hash.t Sc_rollup_inbox_repr.Hash.t)
: Prop := {
back_pointers :
let bp := r.(Skip_list_repr.Make.cell.back_pointers) in
bp.(FallbackArray.t.default) = None ∧
Forall (fun x ⇒ x ≠ None) bp.(FallbackArray.t.items);
index : Pervasives.Int31.Valid.t r.(Skip_list_repr.Make.cell.index);
}.
End Valid.
End old_levels_messages.
Module V1.
Module Valid.
Record t `{Skip_list_repr.Make.FArgs}
(r : Skip_list_repr.Make.cell.record
Sc_rollup_inbox_repr.Hash.t Sc_rollup_inbox_repr.Hash.t)
: Prop := {
back_pointers :
let bp := r.(Skip_list_repr.Make.cell.back_pointers) in
bp.(FallbackArray.t.default) = None ∧
Forall (fun x ⇒ x ≠ None) bp.(FallbackArray.t.items);
index : Pervasives.Int31.Valid.t r.(Skip_list_repr.Make.cell.index);
}.
End Valid.
End old_levels_messages.
Module V1.
Validity of [Sc_rollup_inbox_repr.V1.t]
Module Valid.
Import Sc_rollup_inbox_repr.V1.t.
Record t (x : Sc_rollup_inbox_repr.V1.t) : Prop := {
level : Raw_level_repr.Valid.t x.(level);
nb_messages_in_commitment_period :
Int64.Valid.t x.(nb_messages_in_commitment_period);
}.
End Valid.
Lemma level_proof_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) V1.level_proof_encoding.
Proof.
Admitted.
#[global] Hint Resolve level_proof_encoding_is_valid : Data_encoding_db.
Lemma history_proof_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) V1.history_proof_encoding.
Proof.
Admitted.
#[global] Hint Resolve history_proof_encoding_is_valid : Data_encoding_db.
Import Sc_rollup_inbox_repr.V1.t.
Record t (x : Sc_rollup_inbox_repr.V1.t) : Prop := {
level : Raw_level_repr.Valid.t x.(level);
nb_messages_in_commitment_period :
Int64.Valid.t x.(nb_messages_in_commitment_period);
}.
End Valid.
Lemma level_proof_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) V1.level_proof_encoding.
Proof.
Admitted.
#[global] Hint Resolve level_proof_encoding_is_valid : Data_encoding_db.
Lemma history_proof_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) V1.history_proof_encoding.
Proof.
Admitted.
#[global] Hint Resolve history_proof_encoding_is_valid : Data_encoding_db.
[encoding] is valid
Lemma encoding_is_valid :
Data_encoding.Valid.t Valid.t Sc_rollup_inbox_repr.V1.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x H_valid.
repeat (split; try dtauto);
destruct_all Sc_rollup_inbox_repr.t;
destruct H_valid; simpl in *;
unfold Pervasives.Int.Valid.t in *;
f_equal.
now apply FunctionalExtensionality.functional_extensionality; intros [].
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End V1.
Data_encoding.Valid.t Valid.t Sc_rollup_inbox_repr.V1.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x H_valid.
repeat (split; try dtauto);
destruct_all Sc_rollup_inbox_repr.t;
destruct H_valid; simpl in *;
unfold Pervasives.Int.Valid.t in *;
f_equal.
now apply FunctionalExtensionality.functional_extensionality; intros [].
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End V1.
[inclusion_proof_encoding] is valid
Lemma inclusion_proof_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_inbox_repr.inclusion_proof_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
sfirstorder.
Qed.
#[global] Hint Resolve inclusion_proof_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_inbox_repr.inclusion_proof_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
sfirstorder.
Qed.
#[global] Hint Resolve inclusion_proof_encoding_is_valid : Data_encoding_db.
[add_message] is valid.
Lemma add_message_is_valid
inbox_value payload level_tree_history level_tree :
letP? res := add_message inbox_value payload level_tree_history level_tree in True.
Proof.
unfold add_message.
eapply Error.split_letP.
apply Sc_rollup_inbox_merkelized_payload_hashes_repr.add_payload_is_valid.
hauto l: on.
Qed.
inbox_value payload level_tree_history level_tree :
letP? res := add_message inbox_value payload level_tree_history level_tree in True.
Proof.
unfold add_message.
eapply Error.split_letP.
apply Sc_rollup_inbox_merkelized_payload_hashes_repr.add_payload_is_valid.
hauto l: on.
Qed.
[form_history_proof] is valid.
Lemma form_history_proof_is_valid history_value
inbox_value :
letP? res := form_history_proof history_value inbox_value in True.
Proof.
unfold form_history_proof. simpl.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
apply Bounded_history_repr.Make.remember_is_valid.
intros. reflexivity.
Qed.
inbox_value :
letP? res := form_history_proof history_value inbox_value in True.
Proof.
unfold form_history_proof. simpl.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
apply Bounded_history_repr.Make.remember_is_valid.
intros. reflexivity.
Qed.
[initialize_level_tree_when_needed] is valid.
Lemma initialize_level_tree_when_needed_is_valid level_tree_history
inbox_value level_tree payloads :
letP? res := initialize_level_tree_when_needed level_tree_history
inbox_value level_tree payloads in True.
Proof.
unfold initialize_level_tree_when_needed.
step; [hauto l: on |].
step.
{ apply Error.split_letP with (P:=(fun _ ⇒ True)); [hauto lq: on |].
intros.
step.
eapply Error.split_letP;
[apply Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis_is_valid |].
intros.
hauto l: on.
}
{ simpl.
eapply Error.split_letP;
[apply Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis_is_valid |].
intros.
hauto l: on.
}
Qed.
inbox_value level_tree payloads :
letP? res := initialize_level_tree_when_needed level_tree_history
inbox_value level_tree payloads in True.
Proof.
unfold initialize_level_tree_when_needed.
step; [hauto l: on |].
step.
{ apply Error.split_letP with (P:=(fun _ ⇒ True)); [hauto lq: on |].
intros.
step.
eapply Error.split_letP;
[apply Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis_is_valid |].
intros.
hauto l: on.
}
{ simpl.
eapply Error.split_letP;
[apply Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis_is_valid |].
intros.
hauto l: on.
}
Qed.
[archive_if_needed] is valid.
Lemma archive_if_needed_is_valid level_tree_history history_value
inbox_value new_level level_tree payloads :
letP? res := archive_if_needed level_tree_history history_value
inbox_value new_level level_tree payloads in True.
Proof.
unfold archive_if_needed.
step. {
step; [hauto l: on |].
eapply Error.split_letP;
[apply initialize_level_tree_when_needed_is_valid | hauto l: on].
}
{ apply Error.split_letP with (P:=(fun _ ⇒ True));
[apply form_history_proof_is_valid |].
intros.
step.
eapply Error.split_letP;
[apply initialize_level_tree_when_needed_is_valid | hauto l: on].
}
Qed.
inbox_value new_level level_tree payloads :
letP? res := archive_if_needed level_tree_history history_value
inbox_value new_level level_tree payloads in True.
Proof.
unfold archive_if_needed.
step. {
step; [hauto l: on |].
eapply Error.split_letP;
[apply initialize_level_tree_when_needed_is_valid | hauto l: on].
}
{ apply Error.split_letP with (P:=(fun _ ⇒ True));
[apply form_history_proof_is_valid |].
intros.
step.
eapply Error.split_letP;
[apply initialize_level_tree_when_needed_is_valid | hauto l: on].
}
Qed.
[add_messages] is valid.
Lemma add_messages_is_valid level_tree_history history_value inbox_value
level payloads level_tree :
letP? res := add_messages level_tree_history history_value inbox_value
level payloads level_tree in True.
Proof.
unfold add_messages.
apply Error.split_letP with (P:=(fun _ ⇒ True)); [hauto l: on |].
intros.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
{ cbn.
unfold error_when.
step; reflexivity.
}
{ intros.
eapply Error.split_letP; [apply archive_if_needed_is_valid |].
intros.
do 4 step.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
{ admit.
level payloads level_tree :
letP? res := add_messages level_tree_history history_value inbox_value
level payloads level_tree in True.
Proof.
unfold add_messages.
apply Error.split_letP with (P:=(fun _ ⇒ True)); [hauto l: on |].
intros.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
{ cbn.
unfold error_when.
step; reflexivity.
}
{ intros.
eapply Error.split_letP; [apply archive_if_needed_is_valid |].
intros.
do 4 step.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
{ admit.
@TODO induction by payloads with generalization
}
{ intros.
hauto l: on.
}
Admitted.
{ intros.
hauto l: on.
}
Admitted.
[add_messages_no_history] is valid.
Lemma add_messages_no_history_is_valid
inbox_value level payloads level_tree :
letP? res := add_messages_no_history inbox_value level
payloads level_tree in True.
Proof.
unfold add_messages_no_history.
unfold Result_syntax.op_letplus.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
apply add_messages_is_valid.
intros.
reflexivity.
Qed.
inbox_value level payloads level_tree :
letP? res := add_messages_no_history inbox_value level
payloads level_tree in True.
Proof.
unfold add_messages_no_history.
unfold Result_syntax.op_letplus.
apply Error.split_letP with (P:=(fun _ ⇒ True)).
apply add_messages_is_valid.
intros.
reflexivity.
Qed.
[verify_proof] is valid.
Lemma verify_proof_is_valid function_parameter history_proof proof :
letP? res := verify_proof function_parameter history_proof proof in True.
Proof.
Admitted.
letP? res := verify_proof function_parameter history_proof proof in True.
Proof.
Admitted.