🎫 Ticket_scanner.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Proofs.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_costs.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Import Error.Tactics_letP.
Module ex_ticket.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Proofs.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_costs.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Import Error.Tactics_letP.
Module ex_ticket.
The validity predicate for the type [ex_ticket].
Module Valid.
Inductive t : Ticket_scanner.ex_ticket → Prop :=
| Intro
(ty : Script_typed_ir.ty)
(ticket : Script_typed_ir.ticket
(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty))) :
Script_typed_ir.ty.Comparable.t ty →
Script_typed_ir.ty.Valid.t ty →
Script_typed_ir.ticket.Valid.t
(Script_typed_ir.ty.Valid.to_Ty_t ty) ticket →
t (Ticket_scanner.Ex_ticket
ty ticket).
End Valid.
End ex_ticket.
Module Ticket_inspection.
Import Proto_alpha.Ticket_scanner.Ticket_inspection.
Module has_tickets.
Module Valid.
Inductive t : Ticket_scanner.ex_ticket → Prop :=
| Intro
(ty : Script_typed_ir.ty)
(ticket : Script_typed_ir.ticket
(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty))) :
Script_typed_ir.ty.Comparable.t ty →
Script_typed_ir.ty.Valid.t ty →
Script_typed_ir.ticket.Valid.t
(Script_typed_ir.ty.Valid.to_Ty_t ty) ticket →
t (Ticket_scanner.Ex_ticket
ty ticket).
End Valid.
End ex_ticket.
Module Ticket_inspection.
Import Proto_alpha.Ticket_scanner.Ticket_inspection.
Module has_tickets.
Module Valid.
The validity of [has_tickets] given an expected [Ty.t] shape.
Fixpoint t (a : Ty.t) (ht : has_tickets) {struct ht} : Prop :=
match ht, a with
| True_ht, Ty.Ticket _ ⇒ True
| False_ht, _ ⇒ True
| Pair_ht ht1 ht2, Ty.Pair a1 a2 ⇒ t a1 ht1 ∧ t a2 ht2
| Union_ht ht1 ht2, Ty.Union a1 a2 ⇒ t a1 ht1 ∧ t a2 ht2
| Option_ht ht, Ty.Option a ⇒ t a ht
| List_ht ht, Ty.List a ⇒ t a ht
| Set_ht ht_k, Ty.Set_ a_k ⇒ t a_k ht_k
| Map_ht ht_k ht_v, Ty.Map a_k a_v ⇒ t a_k ht_k ∧ t a_v ht_v
| Big_map_ht ht_k ht_v, Ty.Big_map a_k a_v ⇒ t a_k ht_k ∧ t a_v ht_v
| _, _ ⇒ False
end.
End Valid.
End has_tickets.
match ht, a with
| True_ht, Ty.Ticket _ ⇒ True
| False_ht, _ ⇒ True
| Pair_ht ht1 ht2, Ty.Pair a1 a2 ⇒ t a1 ht1 ∧ t a2 ht2
| Union_ht ht1 ht2, Ty.Union a1 a2 ⇒ t a1 ht1 ∧ t a2 ht2
| Option_ht ht, Ty.Option a ⇒ t a ht
| List_ht ht, Ty.List a ⇒ t a ht
| Set_ht ht_k, Ty.Set_ a_k ⇒ t a_k ht_k
| Map_ht ht_k ht_v, Ty.Map a_k a_v ⇒ t a_k ht_k ∧ t a_v ht_v
| Big_map_ht ht_k ht_v, Ty.Big_map a_k a_v ⇒ t a_k ht_k ∧ t a_v ht_v
| _, _ ⇒ False
end.
End Valid.
End has_tickets.
The function [has_tickets_of_comparable] has a simpler expression.
Lemma has_tickets_of_comparable_eq {a : Ty.t} {ret : Set}
(key_ty : Script_typed_ir.ty) k_value :
a = Script_typed_ir.ty.Valid.to_Ty_t key_ty →
Script_typed_ir.ty.Comparable.t key_ty →
Ticket_scanner.Ticket_inspection.has_tickets_of_comparable (ret := ret)
key_ty k_value = k_value Ticket_scanner.Ticket_inspection.False_ht.
Proof.
intros Ha H_comp. subst a.
destruct key_ty eqn:eq_key_ty ; simpl in × ;
try destruct_all Dependent_bool.dand ;
try destruct_all Dependent_bool.dbool ; try reflexivity ; inversion H_comp.
Qed.
(key_ty : Script_typed_ir.ty) k_value :
a = Script_typed_ir.ty.Valid.to_Ty_t key_ty →
Script_typed_ir.ty.Comparable.t key_ty →
Ticket_scanner.Ticket_inspection.has_tickets_of_comparable (ret := ret)
key_ty k_value = k_value Ticket_scanner.Ticket_inspection.False_ht.
Proof.
intros Ha H_comp. subst a.
destruct key_ty eqn:eq_key_ty ; simpl in × ;
try destruct_all Dependent_bool.dand ;
try destruct_all Dependent_bool.dbool ; try reflexivity ; inversion H_comp.
Qed.
The function [has_tickets_of_ty_aux] is valid.
[domain] stands for a validity predicate on the generic type [ret].
Fixpoint has_tickets_of_ty_aux_is_valid {a : Ty.t} {ret : Set}
(domain : ret → Prop)
(ty_value : Script_typed_ir.ty) (k_value : continuation ret)
{struct ty_value} :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Script_typed_ir.ty.Valid.t ty_value →
(∀ ht,
has_tickets.Valid.t a ht →
letP? result := k_value ht in
domain result
) →
letP? result :=
Ticket_scanner.Ticket_inspection.has_tickets_of_ty_aux ty_value k_value
in domain result.
Proof.
intros Ha H_ty_value H_k_value.
destruct ty_value eqn:eq_ty; subst a; simpl in ×.
all: (try (apply H_k_value ; constructor)).
all:admit.
(domain : ret → Prop)
(ty_value : Script_typed_ir.ty) (k_value : continuation ret)
{struct ty_value} :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Script_typed_ir.ty.Valid.t ty_value →
(∀ ht,
has_tickets.Valid.t a ht →
letP? result := k_value ht in
domain result
) →
letP? result :=
Ticket_scanner.Ticket_inspection.has_tickets_of_ty_aux ty_value k_value
in domain result.
Proof.
intros Ha H_ty_value H_k_value.
destruct ty_value eqn:eq_ty; subst a; simpl in ×.
all: (try (apply H_k_value ; constructor)).
all:admit.
@TODO finish proof
The former proof (given at the end of these comments) was quite short.
Probably possible to do the same.Comment just below: a proof attempt, based on destructing [ht], [ht0]
[ty1] and [ty2]: far too much cases for something that is simple.
(* {
destruct H_ty_value as [H1 [ H2 H3]].
clear H3. (** [H3] is currently useless. *)
apply
has_tickets_of_ty_aux_is_valid with (a := Script_typed_ir.ty.Valid.to_Ty_t t1);
try assumption ; try reflexivity.
intros. try apply
has_tickets_of_ty_aux_is_valid with (a := Script_typed_ir.ty.Valid.to_Ty_t t2);
try assumption ; try reflexivity.
intros. apply H_k_value.
destruct ht eqn:eq_ht ; destruct ht0 eqn:eq_ht0 ; simpl in H ; simpl in H0.
} *)
destruct H_ty_value as [H1 [ H2 H3]].
clear H3. (** [H3] is currently useless. *)
apply
has_tickets_of_ty_aux_is_valid with (a := Script_typed_ir.ty.Valid.to_Ty_t t1);
try assumption ; try reflexivity.
intros. try apply
has_tickets_of_ty_aux_is_valid with (a := Script_typed_ir.ty.Valid.to_Ty_t t2);
try assumption ; try reflexivity.
intros. apply H_k_value.
destruct ht eqn:eq_ht ; destruct ht0 eqn:eq_ht0 ; simpl in H ; simpl in H0.
} *)
Former proof.
(* repeat (
(apply has_tickets_of_ty_aux_is_valid ; intros) ||
apply H_k_value ||
rewrite has_tickets_of_comparable_eq ||
apply has_tickets_of_ty_aux_is_valid ||
easy
).
all: unfold pair_has_tickets, map_has_tickets.
all: try destruct H_ty_value. all:try destruct H_k_value.
all: repeat (step ; try easy). *)
Admitted.
(apply has_tickets_of_ty_aux_is_valid ; intros) ||
apply H_k_value ||
rewrite has_tickets_of_comparable_eq ||
apply has_tickets_of_ty_aux_is_valid ||
easy
).
all: unfold pair_has_tickets, map_has_tickets.
all: try destruct H_ty_value. all:try destruct H_k_value.
all: repeat (step ; try easy). *)
Admitted.
The function [has_tickets_of_ty] is valid.
Lemma has_tickets_of_ty_is_valid {a : Ty.t }
ctxt (ty_value : Script_typed_ir.ty) :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Valid.t ty_value →
letP? '(ht, ctxt) := has_tickets_of_ty ctxt ty_value in
has_tickets.Valid.t a ht ∧
Raw_context.Valid.t ctxt.
Proof.
intros Ha H_ctxt H_ty_value.
unfold has_tickets_of_ty.
eapply Error.split_letP. {
apply Raw_context.consume_gas_is_valid; try assumption.
apply Ticket_costs.has_tickets_of_ty_cost_is_valid.
}
clear ctxt H_ctxt; intros ctxt H_ctxt.
eapply Error.split_letP with (P := has_tickets.Valid.t a). {
now apply (@has_tickets_of_ty_aux_is_valid a).
}
easy.
Qed.
End Ticket_inspection.
Module Ticket_collection.
Import Proto_alpha.Ticket_scanner.
Import Proto_alpha.Ticket_scanner.Ticket_collection.
ctxt (ty_value : Script_typed_ir.ty) :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Valid.t ty_value →
letP? '(ht, ctxt) := has_tickets_of_ty ctxt ty_value in
has_tickets.Valid.t a ht ∧
Raw_context.Valid.t ctxt.
Proof.
intros Ha H_ctxt H_ty_value.
unfold has_tickets_of_ty.
eapply Error.split_letP. {
apply Raw_context.consume_gas_is_valid; try assumption.
apply Ticket_costs.has_tickets_of_ty_cost_is_valid.
}
clear ctxt H_ctxt; intros ctxt H_ctxt.
eapply Error.split_letP with (P := has_tickets.Valid.t a). {
now apply (@has_tickets_of_ty_aux_is_valid a).
}
easy.
Qed.
End Ticket_inspection.
Module Ticket_collection.
Import Proto_alpha.Ticket_scanner.
Import Proto_alpha.Ticket_scanner.Ticket_collection.
The function [consume_gas_steps] is valid.
Lemma consume_gas_steps_is_valid ctxt cost :
Raw_context.Valid.t ctxt →
letP? ctxt :=
Ticket_scanner.Ticket_collection.consume_gas_steps ctxt cost
in Raw_context.Valid.t ctxt.
Proof.
intros H_ctxt.
unfold Ticket_scanner.Ticket_collection.consume_gas_steps.
apply Ticket_costs.consume_gas_steps_is_valid; try assumption.
apply Ticket_costs.Constants.cost_collect_tickets_step_is_valid.
Qed.
Module accumulator.
Module Valid.
Raw_context.Valid.t ctxt →
letP? ctxt :=
Ticket_scanner.Ticket_collection.consume_gas_steps ctxt cost
in Raw_context.Valid.t ctxt.
Proof.
intros H_ctxt.
unfold Ticket_scanner.Ticket_collection.consume_gas_steps.
apply Ticket_costs.consume_gas_steps_is_valid; try assumption.
apply Ticket_costs.Constants.cost_collect_tickets_step_is_valid.
Qed.
Module accumulator.
Module Valid.
Validity predicate for the type [accumulator].
Definition t (x : Ticket_scanner.Ticket_collection.accumulator) : Prop :=
List.Forall ex_ticket.Valid.t x.
End Valid.
End accumulator.
Module continuation.
Module Valid.
List.Forall ex_ticket.Valid.t x.
End Valid.
End accumulator.
Module continuation.
Module Valid.
Validity predicate for the type [continuation].
Definition t {a : Set}
(domain : a → Prop)
(k : Ticket_scanner.Ticket_collection.continuation a) :
Prop :=
∀ ctxt acc,
Raw_context.Valid.t ctxt →
accumulator.Valid.t acc →
letP? result := k ctxt acc in
domain result.
End Valid.
End continuation.
(domain : a → Prop)
(k : Ticket_scanner.Ticket_collection.continuation a) :
Prop :=
∀ ctxt acc,
Raw_context.Valid.t ctxt →
accumulator.Valid.t acc →
letP? result := k ctxt acc in
domain result.
End Valid.
End continuation.
The function [tickets_of_comparable] is valid.
Lemma tickets_of_comparable_is_valid {ret : Set}
(domain : ret → Prop)
ctxt (comp_ty : Script_typed_ir.ty) acc k :
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Comparable.t comp_ty →
accumulator.Valid.t acc →
continuation.Valid.t domain k →
letP? result :=
Ticket_scanner.Ticket_collection.tickets_of_comparable
ctxt comp_ty acc k in
domain result.
Proof.
intros H_ctxt H_comp_ty H_acc H_k.
destruct comp_ty; simpl in *;
destruct_all Dependent_bool.dand;
destruct_all Dependent_bool.dbool;
try apply H_k;
easy.
Qed.
(domain : ret → Prop)
ctxt (comp_ty : Script_typed_ir.ty) acc k :
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Comparable.t comp_ty →
accumulator.Valid.t acc →
continuation.Valid.t domain k →
letP? result :=
Ticket_scanner.Ticket_collection.tickets_of_comparable
ctxt comp_ty acc k in
domain result.
Proof.
intros H_ctxt H_comp_ty H_acc H_k.
destruct comp_ty; simpl in *;
destruct_all Dependent_bool.dand;
destruct_all Dependent_bool.dbool;
try apply H_k;
easy.
Qed.
The function [tickets_of_set] is valid. In OCaml, we have: [ticket_of_set : type a ret.
context -> a Script_typed_ir.comparable_ty -> a Script_typed_ir.set ->
accumulator -> ret continuation -> ret tzresult Lwt.t].
Note that [a Script_typed_ir.comparable_ty] and [a Script_typed_ir.set] are
processed differently in the lemma below:
The type [a Script_typed_ir.comparable_ty] of parameter [key_ty] below is
specified as the pre-condition [a = to_Ty_t key_ty]The type [a Script_typed_ir.set] of parameter [_set] below is directly
specified in the type [Script_typed_ir.set (Ty.to_Set a))]
Lemma tickets_of_set_is_valid {a : Ty.t} {ret : Set}
(domain : ret → Prop) ctxt (key_ty : Script_typed_ir.ty)
(_set : Script_typed_ir.set (Ty.to_Set a)) acc k :
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Comparable.t key_ty →
a = Script_typed_ir.ty.Valid.to_Ty_t key_ty →
accumulator.Valid.t acc →
continuation.Valid.t domain k →
letP? result :=
Ticket_scanner.Ticket_collection.tickets_of_set
(a := Ty.to_Set a)
ctxt key_ty _set acc k in
domain result.
Proof.
intros H_ctxt H_comp H_key_ty H_acc H_k.
unfold Ticket_scanner.Ticket_collection.tickets_of_set.
eapply Error.split_letP. {
now apply consume_gas_steps_is_valid.
}
clear ctxt H_ctxt; intros ctxt H_ctxt.
now apply tickets_of_comparable_is_valid.
Qed.
(domain : ret → Prop) ctxt (key_ty : Script_typed_ir.ty)
(_set : Script_typed_ir.set (Ty.to_Set a)) acc k :
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Comparable.t key_ty →
a = Script_typed_ir.ty.Valid.to_Ty_t key_ty →
accumulator.Valid.t acc →
continuation.Valid.t domain k →
letP? result :=
Ticket_scanner.Ticket_collection.tickets_of_set
(a := Ty.to_Set a)
ctxt key_ty _set acc k in
domain result.
Proof.
intros H_ctxt H_comp H_key_ty H_acc H_k.
unfold Ticket_scanner.Ticket_collection.tickets_of_set.
eapply Error.split_letP. {
now apply consume_gas_steps_is_valid.
}
clear ctxt H_ctxt; intros ctxt H_ctxt.
now apply tickets_of_comparable_is_valid.
Qed.
The function [tickets_of_value_aux] is valid.
Lemma tickets_of_value_aux_is_valid {a : Ty.t} {ret : Set}
(domain : ret → Prop) include_lazy ctxt hty ty_value x_value acc_value
k_value :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Ticket_inspection.has_tickets.Valid.t a hty →
Script_typed_ir.ty.Valid.t ty_value →
Script_typed_ir.Valid.value a x_value →
accumulator.Valid.t acc_value →
continuation.Valid.t domain k_value →
letP? res :=
@tickets_of_value_aux (Ty.to_Set a) ret include_lazy ctxt hty
ty_value x_value acc_value k_value
in domain res.
Proof.
induction hty ; intros
Ha H Hhty Hty_value Hx_value H_acc_value Hk_value ;
unfold continuation.Valid.t in Hk_value ; subst a ;
destruct ty_value.
(domain : ret → Prop) include_lazy ctxt hty ty_value x_value acc_value
k_value :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Ticket_inspection.has_tickets.Valid.t a hty →
Script_typed_ir.ty.Valid.t ty_value →
Script_typed_ir.Valid.value a x_value →
accumulator.Valid.t acc_value →
continuation.Valid.t domain k_value →
letP? res :=
@tickets_of_value_aux (Ty.to_Set a) ret include_lazy ctxt hty
ty_value x_value acc_value k_value
in domain res.
Proof.
induction hty ; intros
Ha H Hhty Hty_value Hx_value H_acc_value Hk_value ;
unfold continuation.Valid.t in Hk_value ; subst a ;
destruct ty_value.
The [try] below reduces 306 cases into 42.
all:(try (inversion Hhty)).
all:(try (unfold tickets_of_value_aux ;
esplit_letP ; [
apply Ticket_costs.consume_gas_steps_is_valid ; [ assumption | easy ]|
intros] )).
all:(try (unfold tickets_of_value_aux ;
esplit_letP ; [
apply Ticket_costs.consume_gas_steps_is_valid ; [ assumption | easy ]|
intros] )).
Proto_alpha@Lima: the [try] below elimnates 34 cases out of 42.
all:(try (apply Hk_value ; assumption)).
all:(unfold Script_typed_ir.comparable_ty).
{ grep @Script_typed_ir.Ticket_t.
simpl in ×.
rewrite_cast_exists.
apply Hk_value ; [ assumption |].
constructor ; [| assumption ].
destruct Hty_value as [[H1 H2] [H3 H4]].
destruct x_value.
dep_destruct Hx_value.
constructor ;
try assumption.
constructor ; assumption.
}
{ grep @Script_typed_ir.Pair_t.
Fail fold @tickets_of_value_aux (
Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value)).
(* Fail rewrite_cast_exists.
Print existT.
Check @Primitive.fst.
Check @cast_exists. *)
simpl.
(* unfold Script_typed_ir.ty.Valid.to_Ty_t. *)
(* replace (Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1))
with *)
assert (unif0 : Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1)
× Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)
=
([Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ),
Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)]).(Primitive.fst)
× ([(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ))
, (Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2))]).(Primitive.snd))
by reflexivity.
all:(unfold Script_typed_ir.comparable_ty).
{ grep @Script_typed_ir.Ticket_t.
simpl in ×.
rewrite_cast_exists.
apply Hk_value ; [ assumption |].
constructor ; [| assumption ].
destruct Hty_value as [[H1 H2] [H3 H4]].
destruct x_value.
dep_destruct Hx_value.
constructor ;
try assumption.
constructor ; assumption.
}
{ grep @Script_typed_ir.Pair_t.
Fail fold @tickets_of_value_aux (
Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value)).
(* Fail rewrite_cast_exists.
Print existT.
Check @Primitive.fst.
Check @cast_exists. *)
simpl.
(* unfold Script_typed_ir.ty.Valid.to_Ty_t. *)
(* replace (Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1))
with *)
assert (unif0 : Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1)
× Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)
=
([Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ),
Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)]).(Primitive.fst)
× ([(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ))
, (Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2))]).(Primitive.snd))
by reflexivity.
For some reason, the [rewrite] below fails.
Fail rewrite unif0.
(* assert (unif1 : Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1) =
([Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ),
Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)]).(Primitive.fst)).
reflexivity.
rewrite unif1. *)
(* assert (unif1 : Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1) =
([Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ),
Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)]).(Primitive.fst)).
reflexivity.
rewrite unif1. *)
For some reason, this below does not rewrite the goal.
(* match goal with
| |- context [Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 )
* Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)
] => replace
(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 )
* Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2) )
with (
([Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 )
, Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)]).(Primitive.fst)
* ([(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ))
, (Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2))]).(Primitive.snd))
end. *)
| |- context [Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 )
* Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)
] => replace
(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 )
* Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2) )
with (
([Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 )
, Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2)]).(Primitive.fst)
* ([(Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value1 ))
, (Ty.to_Set (Script_typed_ir.ty.Valid.to_Ty_t ty_value2))]).(Primitive.snd))
end. *)
The [replace] below fails because of an unification problem
which should have been solved by rewriting [unif0] (had it suceeded).
Fail match goal with
| |- context[@cast_exists ?A [Set ** Set] ?f ?v] ⇒
(* let x0 := eval hnf in (f A) in *)
replace (cast_exists f v) with (existT f _ v)
end.
admit.
}
Admitted.
| |- context[@cast_exists ?A [Set ** Set] ?f ?v] ⇒
(* let x0 := eval hnf in (f A) in *)
replace (cast_exists f v) with (existT f _ v)
end.
admit.
}
Admitted.
Keep this former proof while the above lemma (Lemma tickets_of_value_aux_is_valid)
is unproved The simulation [dep_tickets_of_value_aux] is equal.
(* Fixpoint dep_tickets_of_value_aux_eq {a : Ty.t} {ret : Set}
include_lazy allow_zero_amount_tickets ctxt hty
(ty_value : With_family.ty a)
(x_value : With_family.ty_to_dep_Set a)
acc_value k_value
{struct hty} :
allow_zero_amount_tickets = true ->
Ticket_inspection.has_tickets.Valid.t a hty ->
Script_typed_ir.With_family.Valid.ty ty_value ->
dep_tickets_of_value_aux (ret := ret)
include_lazy allow_zero_amount_tickets ctxt hty ty_value x_value acc_value
k_value =
tickets_of_value_aux (ret := ret)
include_lazy (* allow_zero_amount_tickets *)ctxt hty
(With_family.to_ty ty_value) (With_family.to_value x_value)
acc_value k_value. *)
(* Proof.
intros allow_zero_am_tick H_hty H_ty_value.
destruct hty; simpl;
try (destruct consume_gas_steps; simpl; [|easy]).
{ destruct ty_value; simpl in *; try easy.
cbn.
match goal with
| |- context[cast_exists (Es := Set) ?T ?x] =>
pose proof (cast_exists_eval_1 (T := T) (x := x) (E1 := Ty.to_Set a))
as H_cast
end.
match goal with
| |- context[cast_exists ?f ?v] =>
replace (cast_exists f v) with (existT f (Ty.to_Set a) v)
end.
clear H_cast.
match goal with
| |- context[fail_when ?b _] => destruct b eqn:EB
end; [| reflexivity].
apply Bool.andb_true_iff in EB.
destruct EB.
destruct H_ty_value as [? []].
unfold not in H.
apply Bool.negb_true_iff in H.
rewrite H in allow_zero_am_tick.
discriminate.
}
reflexivity.
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value.
rewrite dep_tickets_of_value_aux_eq by easy.
repeat f_equal.
repeat (apply FunctionalExtensionality.functional_extensionality; intro).
now apply dep_tickets_of_value_aux_eq.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value; now apply dep_tickets_of_value_aux_eq.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value; now try apply dep_tickets_of_value_aux_eq.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value.
revert t acc_value.
induction elements as [|elem elems]; simpl in *; [reflexivity|].
intros.
cbn; destruct Alpha_context.Gas.consume; simpl; [|easy].
rewrite dep_tickets_of_value_aux_eq by easy.
repeat f_equal.
repeat (apply FunctionalExtensionality.functional_extensionality; intro).
apply IHelems.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
match goal with
| |- context[cast_exists (Es := Set) ?T ?x] =>
pose proof (cast_exists_eval_1 (T := T) (x := x) (E1 := Ty.to_Set t0))
as H_cast
end.
match goal with
| |- context[cast_exists ?f ?v] =>
replace (cast_exists f v) with (existT f (Ty.to_Set t0) v)
end.
clear H_cast.
reflexivity.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
match goal with
| |- context[cast_exists (Es := [Set ** Set]) ?T ?x] =>
pose proof (cast_exists_eval_2 (T := T) (x := x)
(E1 := Ty.to_Set key)
(E2 := Ty.to_Set value)
) as H_cast
end.
match goal with
| |- context[cast_exists ?f ?v] =>
replace (cast_exists f v)
with (existT f [Ty.to_Set key, Ty.to_Set value] v)
end.
clear H_cast.
repeat f_equal.
repeat (apply FunctionalExtensionality.functional_extensionality; intro).
simpl.
destruct Alpha_context.Gas.consume; simpl; [|easy].
destruct consume_gas_steps; simpl; [|easy].
apply axiom. (* TODO *)
}
{ destruct ty_value; simpl in *; try easy.
apply axiom. (* TODO *)
}
Qed. *)
include_lazy allow_zero_amount_tickets ctxt hty
(ty_value : With_family.ty a)
(x_value : With_family.ty_to_dep_Set a)
acc_value k_value
{struct hty} :
allow_zero_amount_tickets = true ->
Ticket_inspection.has_tickets.Valid.t a hty ->
Script_typed_ir.With_family.Valid.ty ty_value ->
dep_tickets_of_value_aux (ret := ret)
include_lazy allow_zero_amount_tickets ctxt hty ty_value x_value acc_value
k_value =
tickets_of_value_aux (ret := ret)
include_lazy (* allow_zero_amount_tickets *)ctxt hty
(With_family.to_ty ty_value) (With_family.to_value x_value)
acc_value k_value. *)
(* Proof.
intros allow_zero_am_tick H_hty H_ty_value.
destruct hty; simpl;
try (destruct consume_gas_steps; simpl; [|easy]).
{ destruct ty_value; simpl in *; try easy.
cbn.
match goal with
| |- context[cast_exists (Es := Set) ?T ?x] =>
pose proof (cast_exists_eval_1 (T := T) (x := x) (E1 := Ty.to_Set a))
as H_cast
end.
match goal with
| |- context[cast_exists ?f ?v] =>
replace (cast_exists f v) with (existT f (Ty.to_Set a) v)
end.
clear H_cast.
match goal with
| |- context[fail_when ?b _] => destruct b eqn:EB
end; [| reflexivity].
apply Bool.andb_true_iff in EB.
destruct EB.
destruct H_ty_value as [? []].
unfold not in H.
apply Bool.negb_true_iff in H.
rewrite H in allow_zero_am_tick.
discriminate.
}
reflexivity.
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value.
rewrite dep_tickets_of_value_aux_eq by easy.
repeat f_equal.
repeat (apply FunctionalExtensionality.functional_extensionality; intro).
now apply dep_tickets_of_value_aux_eq.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value; now apply dep_tickets_of_value_aux_eq.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value; now try apply dep_tickets_of_value_aux_eq.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
rewrite_cast_exists.
destruct x_value.
revert t acc_value.
induction elements as [|elem elems]; simpl in *; [reflexivity|].
intros.
cbn; destruct Alpha_context.Gas.consume; simpl; [|easy].
rewrite dep_tickets_of_value_aux_eq by easy.
repeat f_equal.
repeat (apply FunctionalExtensionality.functional_extensionality; intro).
apply IHelems.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
match goal with
| |- context[cast_exists (Es := Set) ?T ?x] =>
pose proof (cast_exists_eval_1 (T := T) (x := x) (E1 := Ty.to_Set t0))
as H_cast
end.
match goal with
| |- context[cast_exists ?f ?v] =>
replace (cast_exists f v) with (existT f (Ty.to_Set t0) v)
end.
clear H_cast.
reflexivity.
}
{ destruct ty_value; simpl in *; try easy.
cbn.
match goal with
| |- context[cast_exists (Es := [Set ** Set]) ?T ?x] =>
pose proof (cast_exists_eval_2 (T := T) (x := x)
(E1 := Ty.to_Set key)
(E2 := Ty.to_Set value)
) as H_cast
end.
match goal with
| |- context[cast_exists ?f ?v] =>
replace (cast_exists f v)
with (existT f [Ty.to_Set key, Ty.to_Set value] v)
end.
clear H_cast.
repeat f_equal.
repeat (apply FunctionalExtensionality.functional_extensionality; intro).
simpl.
destruct Alpha_context.Gas.consume; simpl; [|easy].
destruct consume_gas_steps; simpl; [|easy].
apply axiom. (* TODO *)
}
{ destruct ty_value; simpl in *; try easy.
apply axiom. (* TODO *)
}
Qed. *)
The function [tickets_of_value] is valid.
Lemma tickets_of_value_is_valid {a : Ty.t}
ctxt include_lazy ht ty_value x_value :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Ticket_inspection.has_tickets.Valid.t a ht →
Script_typed_ir.ty.Valid.t ty_value →
Script_typed_ir.Valid.value a x_value →
letP? '(acc, ctxt) := @tickets_of_value (Ty.to_Set a) ctxt include_lazy ht ty_value x_value
in accumulator.Valid.t acc ∧ Raw_context.Valid.t ctxt.
Proof.
unfold tickets_of_value.
intros Ha H_ctxt H_ht Hty_value Hx_value. subst a.
destruct ht, ty_value; simpl in H_ht ; try contradiction.
simpl in ×.
all: try (apply tickets_of_value_aux_is_valid) ; try assumption ;
try constructor ; try assumption.
esplit_letP ; [
apply Ticket_costs.consume_gas_steps_is_valid ; [ assumption | easy ]|].
intros.
unfold Script_typed_ir.comparable_ty in ×.
rewrite_cast_exists.
split ; [| assumption].
constructor ; [| constructor ].
destruct Hty_value as [[? ?] [? ?]].
dep_destruct Hx_value.
constructor ; try assumption.
constructor ; try assumption.
all : destruct H1 as [type_size [comp_t valid_t]]; trivial.
Qed.
End Ticket_collection.
Module has_tickets.
ctxt include_lazy ht ty_value x_value :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Ticket_inspection.has_tickets.Valid.t a ht →
Script_typed_ir.ty.Valid.t ty_value →
Script_typed_ir.Valid.value a x_value →
letP? '(acc, ctxt) := @tickets_of_value (Ty.to_Set a) ctxt include_lazy ht ty_value x_value
in accumulator.Valid.t acc ∧ Raw_context.Valid.t ctxt.
Proof.
unfold tickets_of_value.
intros Ha H_ctxt H_ht Hty_value Hx_value. subst a.
destruct ht, ty_value; simpl in H_ht ; try contradiction.
simpl in ×.
all: try (apply tickets_of_value_aux_is_valid) ; try assumption ;
try constructor ; try assumption.
esplit_letP ; [
apply Ticket_costs.consume_gas_steps_is_valid ; [ assumption | easy ]|].
intros.
unfold Script_typed_ir.comparable_ty in ×.
rewrite_cast_exists.
split ; [| assumption].
constructor ; [| constructor ].
destruct Hty_value as [[? ?] [? ?]].
dep_destruct Hx_value.
constructor ; try assumption.
constructor ; try assumption.
all : destruct H1 as [type_size [comp_t valid_t]]; trivial.
Qed.
End Ticket_collection.
Module has_tickets.
@TODO Change this validity predicate so that it follows the [OCaml] code
and has [a : Ty.t] as an extra (first) parameter.
Do so for other types.
Validity predicate for [has_tickets].
Inductive t : Ticket_scanner.has_tickets → Prop :=
| Has_tickets ht (ty : Script_typed_ir.ty) :
let a := Script_typed_ir.ty.Valid.to_Ty_t ty in
Ticket_inspection.has_tickets.Valid.t a ht →
Script_typed_ir.ty.Valid.t ty →
t (Ticket_scanner.Has_tickets ht ty).
End Valid.
End has_tickets.
| Has_tickets ht (ty : Script_typed_ir.ty) :
let a := Script_typed_ir.ty.Valid.to_Ty_t ty in
Ticket_inspection.has_tickets.Valid.t a ht →
Script_typed_ir.ty.Valid.t ty →
t (Ticket_scanner.Has_tickets ht ty).
End Valid.
End has_tickets.
The function [type_has_tickets] is valid.
Lemma type_has_tickets_is_valid {a : Ty.t} ctxt ty_value :
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Valid.t ty_value →
letP? '(ht, ctxt) :=
Ticket_scanner.type_has_tickets ctxt ty_value in
has_tickets.Valid.t ht ∧
Raw_context.Valid.t ctxt ∧ (let 'Ticket_scanner.Has_tickets value ty_output :=
ht in ty_output = ty_value
).
Proof.
intros Ha H_ctxt H_ty_value.
unfold Ticket_scanner.type_has_tickets.
esplit_letP ; [
apply @Ticket_inspection.has_tickets_of_ty_is_valid with (a := a)
; try assumption ; try reflexivity |].
i_des_pairs.
subst a ; repeat split ; try assumption.
Qed.
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
Raw_context.Valid.t ctxt →
Script_typed_ir.ty.Valid.t ty_value →
letP? '(ht, ctxt) :=
Ticket_scanner.type_has_tickets ctxt ty_value in
has_tickets.Valid.t ht ∧
Raw_context.Valid.t ctxt ∧ (let 'Ticket_scanner.Has_tickets value ty_output :=
ht in ty_output = ty_value
).
Proof.
intros Ha H_ctxt H_ty_value.
unfold Ticket_scanner.type_has_tickets.
esplit_letP ; [
apply @Ticket_inspection.has_tickets_of_ty_is_valid with (a := a)
; try assumption ; try reflexivity |].
i_des_pairs.
subst a ; repeat split ; try assumption.
Qed.
The function [tickets_of_value] is valid.
Lemma tickets_of_value_is_valid
{a : Ty.t}
ctxt include_lazy function_parameter :
∀ ht ty_value,
(Ticket_scanner.Has_tickets ht ty_value = function_parameter) →
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
∀ (x_value : Ty.to_Set a),
Raw_context.Valid.t ctxt →
has_tickets.Valid.t function_parameter →
Script_typed_ir.Valid.value a x_value →
letP? '(acc, ctxt) :=
Ticket_scanner.tickets_of_value
ctxt include_lazy function_parameter x_value in
Ticket_collection.accumulator.Valid.t acc ∧
Raw_context.Valid.t ctxt.
Proof.
intros ht ty_value fun_par_eq Ha x_value H Hfun_par Hx_value.
subst a.
unfold Ticket_scanner.tickets_of_value.
destruct function_parameter as [ht' ty_value'] eqn:fun_par_eq'.
inversion fun_par_eq. subst ht' ty_value'.
dep_destruct Hfun_par.
apply Ticket_collection.tickets_of_value_is_valid ; try assumption ;
reflexivity.
Qed.
{a : Ty.t}
ctxt include_lazy function_parameter :
∀ ht ty_value,
(Ticket_scanner.Has_tickets ht ty_value = function_parameter) →
(a = Script_typed_ir.ty.Valid.to_Ty_t ty_value) →
∀ (x_value : Ty.to_Set a),
Raw_context.Valid.t ctxt →
has_tickets.Valid.t function_parameter →
Script_typed_ir.Valid.value a x_value →
letP? '(acc, ctxt) :=
Ticket_scanner.tickets_of_value
ctxt include_lazy function_parameter x_value in
Ticket_collection.accumulator.Valid.t acc ∧
Raw_context.Valid.t ctxt.
Proof.
intros ht ty_value fun_par_eq Ha x_value H Hfun_par Hx_value.
subst a.
unfold Ticket_scanner.tickets_of_value.
destruct function_parameter as [ht' ty_value'] eqn:fun_par_eq'.
inversion fun_par_eq. subst ht' ty_value'.
dep_destruct Hfun_par.
apply Ticket_collection.tickets_of_value_is_valid ; try assumption ;
reflexivity.
Qed.
The function [tickets_of_node] is valid.
Lemma tickets_of_node_is_valid {a : Ty.t}
ctxt include_lazy has_tickets_value expr :
Raw_context.Valid.t ctxt →
has_tickets.Valid.t has_tickets_value →
let 'Ticket_scanner.Has_tickets ht ty := has_tickets_value in
a = Script_typed_ir.ty.Valid.to_Ty_t ty →
letP? '(acc, ctxt) :=
Ticket_scanner.tickets_of_node (a := Ty.to_Set a)
ctxt include_lazy has_tickets_value expr in
Ticket_collection.accumulator.Valid.t acc ∧
Raw_context.Valid.t ctxt.
Proof.
intros H_ctxt H_has_tickets_value.
destruct has_tickets_value as [ht ty].
intro Ha. subst a.
unfold Ticket_scanner.tickets_of_node.
dep_destruct H_has_tickets_value. subst a.
ctxt include_lazy has_tickets_value expr :
Raw_context.Valid.t ctxt →
has_tickets.Valid.t has_tickets_value →
let 'Ticket_scanner.Has_tickets ht ty := has_tickets_value in
a = Script_typed_ir.ty.Valid.to_Ty_t ty →
letP? '(acc, ctxt) :=
Ticket_scanner.tickets_of_node (a := Ty.to_Set a)
ctxt include_lazy has_tickets_value expr in
Ticket_collection.accumulator.Valid.t acc ∧
Raw_context.Valid.t ctxt.
Proof.
intros H_ctxt H_has_tickets_value.
destruct has_tickets_value as [ht ty].
intro Ha. subst a.
unfold Ticket_scanner.tickets_of_node.
dep_destruct H_has_tickets_value. subst a.
With [a : Ty.t].
(* We solve the default case of the [match] once. *)
match goal with
| |- context[
match _ with
| Ticket_scanner.Ticket_inspection.True_ht ⇒ ?e
| _ ⇒ _
end
] ⇒
assert (
letP? '(acc, ctxt) := e in
Ticket_collection.accumulator.Valid.t acc ∧
Raw_context.Valid.t ctxt
)
end. {
eapply Error.split_letP ; [
apply Script_ir_translator.parse_data_is_valid ;
[assumption | reflexivity ] |].
i_des_pairs.
apply Ticket_collection.tickets_of_value_is_valid ; try assumption ;
try reflexivity.
}
destruct ht; simpl; try assumption.
hauto l: on.
Qed.
match goal with
| |- context[
match _ with
| Ticket_scanner.Ticket_inspection.True_ht ⇒ ?e
| _ ⇒ _
end
] ⇒
assert (
letP? '(acc, ctxt) := e in
Ticket_collection.accumulator.Valid.t acc ∧
Raw_context.Valid.t ctxt
)
end. {
eapply Error.split_letP ; [
apply Script_ir_translator.parse_data_is_valid ;
[assumption | reflexivity ] |].
i_des_pairs.
apply Ticket_collection.tickets_of_value_is_valid ; try assumption ;
try reflexivity.
}
destruct ht; simpl; try assumption.
hauto l: on.
Qed.
The function [ex_ticket_size] is valid.
Lemma ex_ticket_size_is_valid ctxt ticket :
Raw_context.Valid.t ctxt →
Ticket_scanner.ex_ticket.Valid.t ticket →
letP? '(size,ctxt) :=
Ticket_scanner.ex_ticket_size ctxt ticket in
Pervasives.Int.Valid.t size ∧ Raw_context.Valid.t ctxt .
Proof.
intros H_ctxt H_ticket.
unfold Ticket_scanner.ex_ticket_size.
destruct H_ticket as [ty ticket].
eapply Error.split_letP ; [
apply Script_typed_ir.ticket_t_is_valid ; assumption |].
iesplit_letP ; [
apply @Script_ir_unparser.unparse_ty_is_valid ; assumption |].
i_des_pairs.
destruct ticket. inversion H1. simpl in amount0.
match goal with
| |- context[Script_typed_ir_size.node_size ?ty] ⇒
pose proof (Cache_memory_helpers.node_size_is_valid ty) as Hnode_size1
end.
step.
destruct Hnode_size1.
esplit_letP. {
apply Alpha_context.Gas.consume_is_valid ; [ assumption |].
apply Script_typed_ir_size_costs.nodes_cost_is_valid. assumption.
}
intros.
step.
esplit_letP. {
apply Alpha_context.Gas.consume_is_valid ; try assumption.
apply Script_typed_ir_size_costs.nodes_cost_is_valid.
match goal with
| _ : context[Script_typed_ir_size.value_size ?ty ?v] |- _ ⇒
pose proof (Script_typed_ir_size.value_size_is_valid ty v)
as Hnode_size2
end.
destruct Script_typed_ir_size.value_size.
destruct Hnode_size2.
(* We see that [i1 = i0], thanks to [Heqn]. *)
inversion Heqn. subst i0.
assumption.
}
intros.
split ; [| assumption ].
Admitted.
Raw_context.Valid.t ctxt →
Ticket_scanner.ex_ticket.Valid.t ticket →
letP? '(size,ctxt) :=
Ticket_scanner.ex_ticket_size ctxt ticket in
Pervasives.Int.Valid.t size ∧ Raw_context.Valid.t ctxt .
Proof.
intros H_ctxt H_ticket.
unfold Ticket_scanner.ex_ticket_size.
destruct H_ticket as [ty ticket].
eapply Error.split_letP ; [
apply Script_typed_ir.ticket_t_is_valid ; assumption |].
iesplit_letP ; [
apply @Script_ir_unparser.unparse_ty_is_valid ; assumption |].
i_des_pairs.
destruct ticket. inversion H1. simpl in amount0.
match goal with
| |- context[Script_typed_ir_size.node_size ?ty] ⇒
pose proof (Cache_memory_helpers.node_size_is_valid ty) as Hnode_size1
end.
step.
destruct Hnode_size1.
esplit_letP. {
apply Alpha_context.Gas.consume_is_valid ; [ assumption |].
apply Script_typed_ir_size_costs.nodes_cost_is_valid. assumption.
}
intros.
step.
esplit_letP. {
apply Alpha_context.Gas.consume_is_valid ; try assumption.
apply Script_typed_ir_size_costs.nodes_cost_is_valid.
match goal with
| _ : context[Script_typed_ir_size.value_size ?ty ?v] |- _ ⇒
pose proof (Script_typed_ir_size.value_size_is_valid ty v)
as Hnode_size2
end.
destruct Script_typed_ir_size.value_size.
destruct Hnode_size2.
(* We see that [i1 = i0], thanks to [Heqn]. *)
inversion Heqn. subst i0.
assumption.
}
intros.
split ; [| assumption ].
Admitted.