Skip to main content

🎫 Ticket_scanner.v

Proofs

See code, Gitlab , OCaml

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 a2t a1 ht1 t a2 ht2
        | Union_ht ht1 ht2, Ty.Union a1 a2t a1 ht1 t a2 ht2
        | Option_ht ht, Ty.Option at a ht
        | List_ht ht, Ty.List at a ht
        | Set_ht ht_k, Ty.Set_ a_kt a_k ht_k
        | Map_ht ht_k ht_v, Ty.Map a_k a_vt a_k ht_k t a_v ht_v
        | Big_map_ht ht_k ht_v, Ty.Big_map a_k a_vt 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.
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.