🎫 Ticket_scanner.v

Proofs

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.

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.

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.

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.

@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.
    } *)

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.

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.

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.

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.

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.

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.

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.

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.

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] )).

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.

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. *)

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. *)

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.

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. *)

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.

@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.

Module Valid.

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.

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.

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.

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.

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.

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.