🦏 Sc_rollups.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
(*
Lemma kind_of_of_kind kind :
Sc_rollups.kind_of (Sc_rollups.of_kind kind) = kind.
now destruct kind.
Qed.
Lemma kind_of_string_string_of_kind kind :
Sc_rollups.kind_of_string (Sc_rollups.string_of_kind kind) = Some kind.
now destruct kind.
Qed.
Lemma string_of_kind_kind_of_string s :
match Sc_rollups.kind_of_string s with
| Some kind => Sc_rollups.string_of_kind kind = s
| None => True
end.
refine (
match s with
| "arith" => _
| _ => _
end
); reflexivity.
Qed.
*)
Lemma wrapped_proof_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollups.wrapped_proof_encoding.
Proof.
Admitted.
#[global] Hint Resolve wrapped_proof_encoding_is_valid : Data_encoding_db.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
(*
Lemma kind_of_of_kind kind :
Sc_rollups.kind_of (Sc_rollups.of_kind kind) = kind.
now destruct kind.
Qed.
Lemma kind_of_string_string_of_kind kind :
Sc_rollups.kind_of_string (Sc_rollups.string_of_kind kind) = Some kind.
now destruct kind.
Qed.
Lemma string_of_kind_kind_of_string s :
match Sc_rollups.kind_of_string s with
| Some kind => Sc_rollups.string_of_kind kind = s
| None => True
end.
refine (
match s with
| "arith" => _
| _ => _
end
); reflexivity.
Qed.
*)
Lemma wrapped_proof_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollups.wrapped_proof_encoding.
Proof.
Admitted.
#[global] Hint Resolve wrapped_proof_encoding_is_valid : Data_encoding_db.