🦏 Sc_rollup_proof_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.

The encoding [reveal_proof_encoding] is valid.

Lemma reveal_proof_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_proof_repr.reveal_proof_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Admitted.
#[global] Hint Resolve reveal_proof_encoding_is_valid : Data_encoding_db.

Lemma input_proof_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_proof_repr.input_proof_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros.
  step; [| sfirstorder | sfirstorder].
  split; [| sfirstorder].
  split; [trivial |].
  split; [admit |].
  split; [admit | trivial].
Admitted.
#[global] Hint Resolve input_proof_encoding_is_valid : Data_encoding_db.

The encoding [encoding] is valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_proof_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros.
  repeat split.
  step; exact I.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[proof_error] is valid.

Lemma proof_error_is_valid {A : Set} reason_value :
  letP? res := Sc_rollup_proof_repr.proof_error (A:=A) reason_value in True.
Proof.
Admitted.

[check] is valid.

Lemma check_is_valid p_value reason_value :
  letP? res := Sc_rollup_proof_repr.check p_value reason_value in True.
Proof.
  unfold Sc_rollup_proof_repr.check.
  step; [sfirstorder |].
  apply proof_error_is_valid.
Qed.

[check true _] returns [Pervasives.Ok tt] and [check false _] returns [Pervasives.Error _]

Lemma check_eq (b : bool) (reason : string) :
  match Sc_rollup_proof_repr.check b reason with
  | Pervasives.Ok tt ⇒ b = true
  | Pervasives.Error _ ⇒ b = false
  end.
Proof.
  destruct b eqn:H_b; [easy|].
  cbv.
  (* @TODO Lwt_tzresult_syntax is opaque *)
  (* unfold V0.Error_monad.Lwt_tzresult_syntax.fail. *)
Admitted.

[cut_at_level level input] returns [Some input] when [level > input.(Sc_rollup_PVM_sem.input.inbox_level]

(* 
Lemma cut_at_level_gt_eq level input
  (H : 
    let input_level := input.(Sc_rollup_PVM_sig.input.inbox_level) in
    level > input_level) :
  Sc_rollup_proof_repr.cut_at_level level input = Some input.
Proof.
  unfold Sc_rollup_proof_repr.cut_at_level.
  step; [|reflexivity].
  simpl in *.
  unfold Raw_level_repr.op_lteq in *. simpl in *. lia.
Qed.
*)