🐆 Tx_rollup_parameters.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_parameters.

Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_scanner.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

Module deposit_parameters.
  Import Proto_alpha.Tx_rollup_parameters.deposit_parameters.

Validity for the type [deposit_parameters].

  Module Valid.
    Record t (x : Tx_rollup_parameters.deposit_parameters) : Prop := {
      ex_ticket : Ticket_scanner.ex_ticket.Valid.t x.(ex_ticket);
      l2_destination :
        Script_typed_ir.tx_rollup_l2_address.Valid.t x.(l2_destination);
    }.
  End Valid.
End deposit_parameters.

The function [get_deposit_parameters] is valid.

Lemma get_deposit_parameters_is_valid {a : Ty.t} :
  let t : Ty.t := Ty.Pair (Ty.Ticket a) Ty.Tx_rollup_l2_address in
  ∀ ty value,
  Script_typed_ir.ty.Valid.t ty →
  t = Script_typed_ir.ty.Valid.to_Ty_t ty →
  Script_typed_ir.Valid.value t value →
  let params :=
    Tx_rollup_parameters.get_deposit_parameters (a := Ty.to_Set a) ty value
  in deposit_parameters.Valid.t params.
(* 
Lemma get_deposit_parameters_is_valid {a : Ty.t} :
  let t : Ty.t := Ty.Pair (Ty.Ticket a) Ty.Tx_rollup_l2_address in
  forall (ty : With_family.ty t) (value : With_family.ty_to_dep_Set t),
  Script_typed_ir.With_family.Valid.ty ty ->
  Script_typed_ir.With_family.Valid.value value ->
  let params :=
    Tx_rollup_parameters.get_deposit_parameters (a := Ty.to_Set a)
      (With_family.to_ty ty)
      (With_family.to_value value) in
  deposit_parameters.Valid.t params. *)
Proof.
  intros t ty value Hty Htycase Hvalue.
  unfold Tx_rollup_parameters.get_deposit_parameters in ×.
  destruct ty eqn:eq_ty ; ( inversion Htycase).
  simpl in Htycase.
  assert (Ht01 : ∃ ty_value dummy, t0_1 =
    Script_typed_ir.Ticket_t ty_value dummy).
  { clear -Htycase. destruct t0_1 eqn:eq01 ; try inversion Htycase.
    ∃ t0. ∃ t1. reflexivity. }
  assert (Ht02 : t0_2 = Script_typed_ir.Tx_rollup_l2_address_t).
  { clear -Htycase. destruct t0_2 eqn:eq02 ; try inversion Htycase.
    reflexivity. }
  destruct Ht01 as [ty_value [dummy HTick]].
  rewrite HTick. rewrite Ht02.
  destruct value.
  subst t0_1. subst t0_2. simpl.
  assert (eqa : a = Script_typed_ir.ty.Valid.to_Ty_t ty_value).
  { clear -eq_ty t Htycase.
    assert (aux_t : t = Ty.Pair (Ty.Ticket a) Ty.Tx_rollup_l2_address)
    by reflexivity.
    rewrite aux_t in Htycase.
    inversion Htycase. reflexivity.
  }
  subst a.
  assert (case_aux0 :
  ∀ ty1 meta1 meta2 d ty,
    ty =
    Script_typed_ir.Pair_t (Script_typed_ir.Ticket_t ty1 meta1)
      Script_typed_ir.Tx_rollup_l2_address_t meta2 d →
      Script_typed_ir.ty.Valid.t ty →
      Script_typed_ir.ty.Comparable.t ty1 ∧ Script_typed_ir.ty.Valid.t ty1
  ).
  { clear. intros ty1 meta1 meta2 d ty eq_ty Hty. rewrite eq_ty in Hty.
    simpl in Hty.
    unfold Script_typed_ir.ty.Valid.t in Hty. fold Script_typed_ir.ty.Valid.t
    in Hty.
    destruct Hty as [ [ ? ?] [? [ [? [ ? ?]] ?] ] ].
   split ; assumption.
  }
  rewrite <- eq_ty in Hty.
  apply case_aux0 in eq_ty; [| assumption ].
  destruct eq_ty as [Hty_val1 Hty_val2].
  dep_destruct Hvalue.
  dep_destruct t1.
  dep_destruct X1.
  dep_destruct X2.
  constructor ; simpl. constructor ; simpl.
  all: try assumption. constructor ; assumption.
Qed.