🐆 Tx_rollup_parameters.v
Proofs
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.
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.
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.
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.