🦏 Sc_rollups.v

Proofs

See code, Gitlab , OCaml

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.