🦏 Sc_rollup_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Bounded.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Module Address.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_repr.Address.encoding.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Bounded.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Module Address.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_repr.Address.encoding.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[compare] function is valid
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.Address.compare.
Proof. apply Blake2B.Make_is_valid. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.Address.compare.
Proof. apply Blake2B.Make_is_valid. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
Propositional equality and [equal] are equivalent on [Address.t].
Lemma equal_is_valid :
Compare.Equal.Valid.t (fun _ ⇒ True) Sc_rollup_repr.Address.equal.
Proof.
apply Blake2B.Make_equal_is_valid.
Qed.
Lemma of_b58_opt_to_b58_eq v :
Sc_rollup_repr.Address.of_b58check_opt
(Sc_rollup_repr.Address.to_b58check v) = return× v.
Proof.
unfold Make_t.
match goal with
| [v : Make_t ?R0 ?N0 |- _] ⇒ pose R0 as R ; pose N0 as N ;
destruct (Blake2B.Make_is_valid R N) as [ _ _ B58_DATA _]
end.
destruct B58_DATA. rewrite of_to_b58_check. reflexivity.
Qed.
Lemma to_b58_opt_of_b58_eq b58 :
match Sc_rollup_repr.Address.of_b58check_opt b58 with
| Some v ⇒ Sc_rollup_repr.Address.to_b58check v = b58
| None ⇒ True
end.
Proof.
unfold Sc_rollup_repr.Address.of_b58check_opt.
unfold Sc_rollup_repr.Address.H.
Compare.Equal.Valid.t (fun _ ⇒ True) Sc_rollup_repr.Address.equal.
Proof.
apply Blake2B.Make_equal_is_valid.
Qed.
Lemma of_b58_opt_to_b58_eq v :
Sc_rollup_repr.Address.of_b58check_opt
(Sc_rollup_repr.Address.to_b58check v) = return× v.
Proof.
unfold Make_t.
match goal with
| [v : Make_t ?R0 ?N0 |- _] ⇒ pose R0 as R ; pose N0 as N ;
destruct (Blake2B.Make_is_valid R N) as [ _ _ B58_DATA _]
end.
destruct B58_DATA. rewrite of_to_b58_check. reflexivity.
Qed.
Lemma to_b58_opt_of_b58_eq b58 :
match Sc_rollup_repr.Address.of_b58check_opt b58 with
| Some v ⇒ Sc_rollup_repr.Address.to_b58check v = b58
| None ⇒ True
end.
Proof.
unfold Sc_rollup_repr.Address.of_b58check_opt.
unfold Sc_rollup_repr.Address.H.
Now that [Sc_rollup_repr.Address.H.] has been unfolded *once*,
we can read the parameters of [Make_t] and fold them to clean
the proof.
match goal with
| |- context [Make_t ?R0 ?N0] ⇒ pose R0 as R ; pose N0 as N ;
destruct (Blake2B.Make_is_valid R N) as [ _ _ B58_DATA _]
end.
destruct B58_DATA.
unfold Sc_rollup_repr.Address.to_b58check.
unfold Sc_rollup_repr.Address.H.
fold R. fold N.
apply to_of_b58_check.
Qed.
Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True)
Sc_rollup_repr.Address.rpc_arg.
Proof.
apply Blake2B.Make_is_valid.
Qed.
End Address.
Module State_hash.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_repr.State_hash.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
| |- context [Make_t ?R0 ?N0] ⇒ pose R0 as R ; pose N0 as N ;
destruct (Blake2B.Make_is_valid R N) as [ _ _ B58_DATA _]
end.
destruct B58_DATA.
unfold Sc_rollup_repr.Address.to_b58check.
unfold Sc_rollup_repr.Address.H.
fold R. fold N.
apply to_of_b58_check.
Qed.
Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True)
Sc_rollup_repr.Address.rpc_arg.
Proof.
apply Blake2B.Make_is_valid.
Qed.
End Address.
Module State_hash.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_repr.State_hash.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[compare] function is valid
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.State_hash.compare.
Proof. apply Blake2B.Make_is_valid. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End State_hash.
Axiom of_b58_to_b58_eq : ∀ s,
Sc_rollup_repr.of_b58check
(Sc_rollup_repr.Address.to_b58check s) = return? s.
Axiom to_b58_of_b58_eq : ∀ b58,
match Sc_rollup_repr.of_b58check b58 with
| Pervasives.Ok v ⇒ Sc_rollup_repr.Address.to_b58check v = b58
| Pervasives.Error _ ⇒ True
end.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros; split; trivial.
apply of_b58_to_b58_eq.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True) Sc_rollup_repr.rpc_arg.
Proof.
constructor; intros; simpl.
{ rewrite of_b58_to_b58_eq; reflexivity. }
{ destruct (Sc_rollup_repr.of_b58check s) eqn:E; simpl; trivial.
specialize (to_b58_of_b58_eq s); rewrite E; trivial. }
Qed.
Lemma index_path_encoding_is_valid :
Path_encoding.S.Valid.t
(Storage_description.INDEX.to_Path Sc_rollup_repr.Index).
Proof.
constructor;
unfold
Sc_rollup_repr.Index,
Sc_rollup_repr.Index.module,
Sc_rollup_repr.Index.to_path,
Sc_rollup_repr.Index.of_path,
Binary.to_bytes_exn,
Sc_rollup_repr.Index.path_length; simpl.
{ intros; destruct (Hex.of_bytes _ _); reflexivity. }
{ intro v; destruct (Hex.of_bytes _ _) eqn:E;
rewrite <- E, Hex.to_bytes_of_bytes; clear E; simpl.
specialize
(Data_encoding.Valid.of_bytes_opt_to_bytes_opt encoding_is_valid v I).
destruct (Binary.to_bytes_opt _ _ _) eqn:E; [|contradiction];
intro Epath; rewrite Epath; reflexivity.
}
{ intro path; destruct path; simpl; trivial; destruct path; simpl; trivial.
destruct (Hex.to_bytes _) eqn:E; simpl; trivial;
specialize (Hex.of_bytes_to_bytes (Hex.Hex s)); rewrite E; intro;
specialize
(Data_encoding.Valid.to_bytes_opt_of_bytes_opt encoding_is_valid b);
destruct (Binary.of_bytes_opt _ _) eqn:E1; simpl; trivial.
hauto lq: on.
}
{ intros; destruct (Hex.of_bytes None _); reflexivity. }
Qed.
Module Index.
Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.State_hash.compare.
Proof. apply Blake2B.Make_is_valid. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End State_hash.
Axiom of_b58_to_b58_eq : ∀ s,
Sc_rollup_repr.of_b58check
(Sc_rollup_repr.Address.to_b58check s) = return? s.
Axiom to_b58_of_b58_eq : ∀ b58,
match Sc_rollup_repr.of_b58check b58 with
| Pervasives.Ok v ⇒ Sc_rollup_repr.Address.to_b58check v = b58
| Pervasives.Error _ ⇒ True
end.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros; split; trivial.
apply of_b58_to_b58_eq.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True) Sc_rollup_repr.rpc_arg.
Proof.
constructor; intros; simpl.
{ rewrite of_b58_to_b58_eq; reflexivity. }
{ destruct (Sc_rollup_repr.of_b58check s) eqn:E; simpl; trivial.
specialize (to_b58_of_b58_eq s); rewrite E; trivial. }
Qed.
Lemma index_path_encoding_is_valid :
Path_encoding.S.Valid.t
(Storage_description.INDEX.to_Path Sc_rollup_repr.Index).
Proof.
constructor;
unfold
Sc_rollup_repr.Index,
Sc_rollup_repr.Index.module,
Sc_rollup_repr.Index.to_path,
Sc_rollup_repr.Index.of_path,
Binary.to_bytes_exn,
Sc_rollup_repr.Index.path_length; simpl.
{ intros; destruct (Hex.of_bytes _ _); reflexivity. }
{ intro v; destruct (Hex.of_bytes _ _) eqn:E;
rewrite <- E, Hex.to_bytes_of_bytes; clear E; simpl.
specialize
(Data_encoding.Valid.of_bytes_opt_to_bytes_opt encoding_is_valid v I).
destruct (Binary.to_bytes_opt _ _ _) eqn:E; [|contradiction];
intro Epath; rewrite Epath; reflexivity.
}
{ intro path; destruct path; simpl; trivial; destruct path; simpl; trivial.
destruct (Hex.to_bytes _) eqn:E; simpl; trivial;
specialize (Hex.of_bytes_to_bytes (Hex.Hex s)); rewrite E; intro;
specialize
(Data_encoding.Valid.to_bytes_opt_of_bytes_opt encoding_is_valid b);
destruct (Binary.of_bytes_opt _ _) eqn:E1; simpl; trivial.
hauto lq: on.
}
{ intros; destruct (Hex.of_bytes None _); reflexivity. }
Qed.
Module Index.
[compare] function is valid
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.Index.compare.
Proof. apply Blake2B.Make_is_valid. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End Index.
Module Number_of_ticks.
Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.Index.compare.
Proof. apply Blake2B.Make_is_valid. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End Index.
Module Number_of_ticks.
The bounds [Number_of_ticks] are valid.
Lemma is_valid :
Bounded.S.Valid.t Int64.Valid.t
Sc_rollup_repr.Number_of_ticks.Bounded_Int64_include.
Proof.
apply Bounded.Int64_is_Valid.
constructor; simpl; lia.
Qed.
Bounded.S.Valid.t Int64.Valid.t
Sc_rollup_repr.Number_of_ticks.Bounded_Int64_include.
Proof.
apply Bounded.Int64_is_Valid.
constructor; simpl; lia.
Qed.
The corresponding encoding is valid.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_repr.Number_of_ticks.Bounded_Int64_include.(S.encoding).
Proof.
apply is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Number_of_ticks.
(* TODO: missing module Sc_rollup_repr.Kind
Module Kind.
Lemma encoding_is_valid
: Data_encoding.Valid.t (fun _ => True) Sc_rollup_repr.Kind.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Kind.
*)
Data_encoding.Valid.t (fun _ ⇒ True)
Sc_rollup_repr.Number_of_ticks.Bounded_Int64_include.(S.encoding).
Proof.
apply is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Number_of_ticks.
(* TODO: missing module Sc_rollup_repr.Kind
Module Kind.
Lemma encoding_is_valid
: Data_encoding.Valid.t (fun _ => True) Sc_rollup_repr.Kind.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Kind.
*)