🍬 Script_ir_translator.v

Proofs

destructs [Alpha_context.Gas.consume ctxt] expression in the goal

Ltac consume_gas :=
destruct Alpha_context.Gas.consume eqn:?H_gc in |- *; simpl; trivial.

destructs [Gas_monad.run ctxt m] expression in the goal

Ltac run_gas_monad := destruct Gas_monad.run eqn:?H_gmr in |- ×.

Conversion back to [eq] of OCaml.

Definition to_eq {Family : Set} {a b : Family} (_ : a = b) : eq := Eq.

Lemma kind_equal_eq : ∀ (a b : Script_tc_errors.kind),
    kind_equal a b = true → a = b.
Proof. now intros [] []. Qed.

Lemma kind_equal_refl : ∀ x, kind_equal x x = true.
Proof. now intros []. Qed.

(* [unparse_ty_and_entrypoints_uncarbonated] can only return [Prim] constructor *)
Lemma only_Prim {lc : Set} : ∀ loc ty,
  match Script_ir_unparser.unparse_ty_and_entrypoints_uncarbonated
          (loc := lc) loc ty Script_typed_ir.no_entrypoints with
  | Prim _ _ _ _ ⇒ True
  | _ ⇒ False
  end.
Proof.
  intros.
  unfold Script_ir_unparser.unparse_ty_and_entrypoints_uncarbonated.
  destruct ty; trivial. step; trivial. step; trivial. step; trivial.
  simpl; trivial.
Qed.

(* Auxiliary lemma, states that if we remove annotation from the node,
   node's contents (ty) stays the same.  *)
Lemma remove_field_annot_node : ∀ nd n,
    Script_ir_annot.remove_field_annot nd = V0.Pervasives.Ok n → nd = n.
Proof.
Admitted.

(* Auxiliary lemma, states that : parse_ty_aux (unparse_ty_uncarbonated ty) = ty
   We go by path : Don't_parse_entrypoins (it is not our choice, it's the way
   [parse_ty_aux] is called by [parse_ty])  *)
Fixpoint parse_ty_aux_unparse_ty_uncarbonated_compatible loc ctxt ty a b c d e
  stack_depth
  (H : Script_typed_ir.ty.Valid.t ty) {struct ty} :
  match
    parse_ty_aux ctxt stack_depth a b c d e Don't_parse_entrypoints
      (Script_ir_unparser.unparse_ty_uncarbonated loc ty)
  with
  | V0.Pervasives.Ok (Script_typed_ir.Ex_ty ty', _) ⇒ ty = ty'
  | V0.Pervasives.Error _ ⇒ True
  end.
Proof.
  destruct ty eqn:TY.
  all : simpl.
  (* @TODO : metadata computation is missing in the validity predicate. *)
  14, 16 - 25, 32 : admit.
  1 - 13 : destruct Alpha_context.Gas.consume; simpl; trivial;
  try (destruct (_ >i _); simpl; trivial);
  try (destruct Alpha_context.Constants.tx_rollup_enable; simpl; trivial);
  try (destruct Script_ir_annot.check_type_annot; simpl; trivial);
  try rewrite cast_eval;
  try reflexivity.
  (* Union *)
  { destruct Alpha_context.Gas.consume; simpl; trivial.
    (* t : Proto_alpha.Raw_tontext.t appeared, will be given to t1 *)
    destruct (_ >i _); simpl; trivial.
Admitted.
    (* destruct H as [metadata_size [metadata_max [Valid_t1 [Valid_t2 Dep_bool]]]].
    pose proof parse_ty_aux_unparse_ty_uncarbonated_compatible
      loc t t1 a b c d e (stack_depth +i 1) Valid_t1 as H.
    unfold Script_ir_unparser.unparse_ty_uncarbonated in H.
    pose proof (only_Prim loc t1) as OnlyPrim_for_t1.
    destruct Script_ir_unparser.unparse_ty_and_entrypoints_uncarbonated;
      try inversion OnlyPrim_for_t1.
    clear OnlyPrim_for_t1.
    destruct (Script_ir_annot.remove_field_annot (Prim l p l0 a0)) eqn:n1;
      simpl; trivial.
    apply remove_field_annot_node in n1.
    destruct Script_ir_annot.remove_field_annot eqn:n2; simpl; trivial.
    apply remove_field_annot_node in n2.
    rewrite n1 in H.
    destruct (parse_ty_aux t) eqn:Parse_node_n; simpl; trivial.
    destruct p0.
    pose proof parse_ty_aux_unparse_ty_uncarbonated_compatible
      loc c0 t2 a b c d e (stack_depth +i 1) Valid_t2 as H0.
    unfold Script_ir_unparser.unparse_ty_uncarbonated in H0.
    rewrite n2 in H0.
    destruct (parse_ty_aux c0); simpl; trivial.
    destruct p0.
    destruct Script_ir_annot.check_type_annot; simpl; trivial.
    rewrite cast_eval.
    destruct e0. (* H  : t1 = t0 , we proved that left and right types
                                   in Union are recursively equal
                                    *)
    destruct e1. (* H0 : t2 = t4 , we will rewrite it in the goal,
                                   for the reflexivity *)
    rewrite H.
    rewrite H0.
    unfold Script_typed_ir.union_t.
    simpl.
    unfold Script_typed_ir.Type_size.compound2.
    unfold Script_typed_ir.Type_size.of_int.
    destruct (_ <=i _); simpl; trivial.
    rewrite H in Dep_bool.
    rewrite H0 in Dep_bool.
    simpl in Dep_bool.
    destruct Dependent_bool.dand_value.
    simpl.
    rewrite Dep_bool.
    rewrite metadata_size.
    rewrite H.
    rewrite H0.
    reflexivity.
  }
  1 - 8 : destruct Alpha_context.Gas.consume; simpl; trivial;
  try (destruct (_ >i _); simpl; trivial);
  try (destruct Script_ir_annot.check_type_annot; simpl; trivial);
  try rewrite cast_eval;
  try (destruct c; simpl; trivial);
  try (destruct a; simpl; trivial);
  try reflexivity.
Admitted. *)

Top-level [lemma parse (unparse ty) = ty]. We use all the above lemmas as helps, according to the proto_alpha structure.

Lemma parse_unparse_ty_compatible : ∀ loc ctxt ty a b c d e,
    Script_typed_ir.ty.Valid.t ty →
    match Script_ir_unparser.unparse_ty loc ctxt ty with
    | Pervasives.Ok (node, ctxt) ⇒
        match parse_ty ctxt a b c d e node with
        | Pervasives.Ok (Script_typed_ir.Ex_ty ty', ctxt) ⇒ ty = ty'
        | Pervasives.Error _ ⇒ True
        end
    | Pervasives.Error _ ⇒ True
    end.
Proof.
  intros.
  unfold Script_ir_unparser.unparse_ty, parse_ty.
  destruct Alpha_context.Gas.consume; simpl; [| trivial].
  apply parse_ty_aux_unparse_ty_uncarbonated_compatible.
  apply H.
Qed.

We prove that [parse (unparse comparable_ty) = comparable_ty] (skipping annotations). Here we prove this statement for auxillary functions. We require metadata of given comparable_ty to be correct in sense described above ([Valid.t] predicate). The most part of proof is by case analysis. So, we unfold definitions, check every possible case for comparable_ty, and show the required equaliy.

Recursive cases are proved with inductive hypos.

We do not check error cases, go through success case only.

(* #[bypass_check(guard)] *)
Fixpoint parse_comparable_ty_aux_unparse_comparable_ty_uncarbonated
  loc ty ctxt n
  (H_comparable : Script_typed_ir.ty.Comparable.t ty)
  (H_valid : Script_typed_ir.ty.Valid.t ty)
  (* max stack_depth = 10000 as per original code*)
  (H_stack_depth : 0 ≤ n ≤ 10000)
  {struct ty} :
  let node := Script_ir_unparser.unparse_ty_uncarbonated loc ty in
  match parse_comparable_ty_aux ctxt n node with
  | V7.Pervasives.Ok (Ex_comparable_ty ty', _) ⇒ ty = ty'
  | V7.Pervasives.Error _ ⇒ True
  end.
Proof.
  destruct ty eqn:TY; simpl; try inversion H'_valid.
  all : destruct n eqn:D_N; simpl; try lia.
  all : try (destruct (Alpha_context.Gas.consume); simpl; [| apply I]);
        try (destruct Script_ir_annot.check_type_annot; simpl;
          [| try reflexivity; try (apply I)]); try rewrite cast_eval;
            simpl; try reflexivity.
  all : try destruct (_ >i _) eqn:D_IF; simpl; try apply I; try reflexivity.
  all : try (destruct Alpha_context.Constants.tx_rollup_enable; simpl;
             [| apply I]); try reflexivity.
  (* Pairs *)
  { simpl.
    unfold Script_ir_unparser.unparse_ty_uncarbonated.
    simpl. admit. }
    Admitted.

We prove that [parse (unparse comparable_ty) = comparable_ty] (skipping annotations). We require metadata of given [comparable_ty] to be correct in sense described above ([Valid.t] predicate). For proof here we unfold definitions and perform case analysis for some simple cases until we are able to use lemma for auxillary functions which is proved above. We do not check error cases, go through success case only. Since we do both directions ([parse (unparse t)] and [unparse (parse t)]), we can be sure either both functions work right or they both have errors on the same cases with same results (kind of symmetric saying a bit more accurate..), so, these are most likely specification errors and we will likely just repeat them while building the error checking from function implementations.

Lemma parse_unparse_comparable_ty :
  ∀ cty loc ctxt,
    Script_typed_ir.ty.Valid.t cty →
    Script_typed_ir.ty.Comparable.t cty →
    match Script_ir_unparser.unparse_ty loc ctxt cty with
    | Pervasives.Ok (node', ctxt') ⇒
      match parse_comparable_ty ctxt' node' with
      | Pervasives.Ok (Ex_comparable_ty cty'', ctxt'') ⇒ cty = cty''
      | Pervasives.Error _ ⇒ True
      end
    | Pervasives.Error _ ⇒ True
    end.
Proof.
  intros cty loc ctxt H H1;
    unfold parse_comparable_ty, Script_ir_unparser.unparse_ty.
  destruct Alpha_context.Gas.consume eqn:Egc; simpl;
    [|trivial].
Admitted.

Module Node.
  Module Valid.
    Fixpoint t (node : Alpha_context.Script.node)
             (loc : Alpha_context.Script.location) : Prop :=
      match node with
      | Prim l Michelson_v1_primitives.T_option [n] annot ⇒
          l = loc ∧ t n loc
      | Prim l Michelson_v1_primitives.T_or [n;n0] annot ⇒
          l = loc ∧ t n loc ∧ t n0 loc
      | Prim l Michelson_v1_primitives.T_pair [n;n0] annot ⇒
          l = loc ∧ t n loc ∧ t n0 loc
      | Prim l _ _ _ ⇒ l = loc
      | _ ⇒ True
      end.
  End Valid.
End Node.

Fixpoint unparse_comparable_ty_uncarbonated_parse_comparable_ty_aux
  (node : Alpha_context.Script.node ) (ctxt : Alpha_context.t)
  (stack_depth : int) loc {struct node} :
  Node.Valid.t node loc →
  match parse_comparable_ty_aux ctxt stack_depth node with
  | Pervasives.Ok (Ex_comparable_ty comp_ty, _) ⇒
      let node' :=
        Script_ir_unparser.unparse_comparable_ty_uncarbonated loc comp_ty in
      Alpha_context.Script.strip_annotations node' =
      Alpha_context.Script.strip_annotations node
  | Pervasives.Error _ ⇒ True
  end.
Proof.
Admitted.

Opposite lemma. We prove that [unparse (parse comparable_ty) = comparable_ty]. Unions and pairs cases in auxillary fixpoint admitted due to annotations

Fixpoint unparse_parse_comparable_ty
    node loc ctxt :
    Node.Valid.t node loc →
    match parse_comparable_ty ctxt node with
    | Pervasives.Ok (Ex_comparable_ty comp_ty, ctxt') ⇒
        match Script_ir_unparser.unparse_ty loc ctxt' comp_ty with
        | Pervasives.Ok (node', ctxt'') ⇒
        Alpha_context.Script.strip_annotations node' =
        Alpha_context.Script.strip_annotations node
        | Pervasives.Error _ ⇒ True
        end
    | Pervasives.Error _ ⇒ True
    end.
Proof.
  intros.
  ez destruct (parse_comparable_ty _ _ ) eqn:?H_parse_comparable_ty.
  Tactics.destruct_pairs.
  do 2 step_outer; [|easy].
  Tactics.destruct_pairs.
  f_equal.
  revert H_parse_comparable_ty Heqt.
  destruct node;
  match goal with
  | |- context [Prim _ _ _ _] ⇒ idtac
  | |- _ ⇒ cbn; now destruct (Alpha_context.Gas.consume _ _)
  end.
  cbn. destruct (Alpha_context.Gas.consume _ _); [cbn|easy].
  destruct_all Michelson_v1_primitives.prim; cbn; try scongruence;
  try rewrite cast_eval.
  step; [|scongruence]. step; [simpl|scongruence].
  intros. unfold "return?" in H_parse_comparable_ty.
  injection H_parse_comparable_ty as H_parse_comparable_ty.
  rewrite <- H_parse_comparable_ty in Heqt.
  unfold Script_ir_unparser.unparse_ty in Heqt.
  (* @TODO Proofs: Finish this proof. *)
Admitted.

Definition z_number_10000 : Z.t := 10000.
Opaque z_number_10000.

Global Hint Unfold Script_ir_unparser.z_number_10001 : tezos_z.

Ltac tr_lia :=
  with_strategy transparent [Script_ir_unparser.z_number_10001] lia.

[fuel_to_stack_depth] and [stack_depth_to_fuel] are inverses.

(* @TODO 22.November.2022, redo for new ver. of Michelson verification
Lemma fuel_to_stack_depth_to_fuel fuel :
  0 <= Z.of_nat fuel <= Script_ir_unparser.z_number_10001 ->
  Script_ir_unparser.stack_depth_to_fuel
    (Script_ir_unparser.fuel_to_stack_depth fuel) =
  fuel.
Proof.
  unfold Script_ir_unparser.fuel_to_stack_depth,
    Script_ir_unparser.stack_depth_to_fuel.
  lia.
Qed.
*)

The function [dep_parse_comparable_ty] is valid

Lemma parse_comparable_data_is_valid {a : Script_family.Ty.t} opt ctxt ty node_val :
  Raw_context.Valid.t ctxt →
  a = Script_typed_ir.ty.Valid.to_Ty_t ty →
  letP ? '(val ,ctxt') := Script_ir_translator.parse_comparable_data
    (A := Ty.to_Set a) opt ctxt ty node_val in
  Raw_context.Valid.t ctxt' ∧
  Script_typed_ir.Valid.value a val.
Proof.
Admitted.

(* [unparse_data] is valid *)
Lemma unparse_data_is_valid (a : Ty.t) (ctxt : Alpha_context.context)
  (mode : Script_ir_unparser.unparsing_mode) ty
  (A : Ty.to_Set a) :
  Raw_context.Valid.t ctxt →
  a = Script_typed_ir.ty.Valid.to_Ty_t ty →
  Script_typed_ir.Valid.value a A →
  letP ? ' ( _ , ctxt ) := Script_ir_translator.unparse_data ctxt
  mode ty A
  in Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt H_ty H_v. subst a.
  assert (H_0 : Pervasives.Int.Valid.non_negative 0) by lia.
  eapply Script_ir_unparser.Data_unparser.unparse_data_aux_is_valid;
    try reflexivity; try assumption.
Qed.

Lemma unparse_data_aux_is_valid
  (F : Proto_alpha.Script_ir_unparser.Data_unparser.FArgs) (a : Ty.t)
  (ctxt : Alpha_context.context) (stack_depth : int)
  (mode : Script_ir_unparser.unparsing_mode) ty
  (v : Ty.to_Set a) :

Some validity predicate on [F]

  Raw_context.Valid.t ctxt →
  Pervasives.Int.Valid.non_negative stack_depth →
  a = Script_typed_ir.ty.Valid.to_Ty_t ty →
  Script_typed_ir.Valid.value a v →
  letP ? ' ( _ , ctxt ) := Script_ir_unparser.Data_unparser.unparse_data_aux
  ctxt stack_depth mode ty v
  in Raw_context.Valid.t ctxt.
Proof.
Admitted.

[unparse_code] is valid. Currently, no pre-condition on [mode] and [n] and no post-condition on the first projection of the output, which is a [node]

Lemma unparse_code_is_valid {a : Set} (ctxt : Alpha_context.t)
  (mode: Script_ir_unparser.unparsing_mode)
  (n : node a Alpha_context.Script.prim) :
  Raw_context.Valid.t ctxt →
  letP ? ' (_ , ctxt ) := Script_ir_translator.unparse_code ctxt mode n
  in Raw_context.Valid.t ctxt.
Proof.
Admitted.

Given a valid [t : With_family.ty _], on success [dep_parse_contract_for_script] preserves the validity of [t] @TODO fix definition (or remove it)

(*
Lemma dep_parse_contract_for_script_is_valid :
  forall (a : Ty.t) (gas_counter : Local_gas_counter.local_gas_counter)
    (outdated_context : Local_gas_counter.outdated_context)
    (location : Alpha_context.Script.location)
    (t : With_family.ty a) (accu : Script_typed_ir.address.record)
    (s1 : Alpha_context.Entrypoint.t)
    (c : Alpha_context.context) (t' : With_family.ty a)
    (addr : Script_typed_ir.address),
  Script_typed_ir.With_family.Valid.ty t ->
  Script_ir_translator.dep_parse_contract_for_script
    (Local_gas_counter.update_context gas_counter outdated_context)
    location t accu.(Script_typed_ir.address.destination) s1 =
    Pervasives.Ok (c, Some (With_family.Typed_contract t' addr)) ->
  Script_typed_ir.With_family.Valid.ty t'.
Proof.
  (* @TODO Simulation: Complete the simulatin of dep_parse_contract_for_script *)
Admitted.
*)

@TODO, 22.November.2022 : redo for [parse_code] [dep_parse_code] is valid

(*
Lemma dep_parse_code_is_valid type_logger_value ctxt ctxt' legacy code d :
  dep_parse_code type_logger_value ctxt legacy code = V7.Pervasives.Ok (d, ctxt') ->
  Dep_ex_code.Valid.t d.
Proof. *)
  (* TODO Proofs, not tried yet, created to introduce
     Script_typed_ir.With_family.Valid.ty storage_type in the context of
     dep_parse_script_eq. Admitted.*)

@TODO : 22 November 2022, write this validity predicate Module ex_script. Module Valid. (** Validity predicate for [ex_script]. *)
Definition t (x : ex_script) : Prop := match x with | Ex_script script => (* Script_typed_ir.script.Valid.t script *)
end. End Valid. End ex_script.

[parse_script] is valid.

Lemma parse_script_is_valid (elab_conf : Script_ir_translator.elab_conf)
  (ctxt : Proto_alpha.Raw_context.t) (allow_forged_in_storage : bool)
  (function_parameter : Script_repr.t) :
  Raw_context.Valid.t ctxt → letP ? '(script , ctxt ):= parse_script elab_conf ctxt
    allow_forged_in_storage function_parameter
  in Raw_context.Valid.t ctxt (* /\ ex_script.Valid.t script *).
Proof.

@TODO use the two previous lemmas

Admitted.

[collect_lazy_storage] is valid. No post-condition in the ouput for to_duplicate

Lemma collect_lazy_storage_is_valid (a : Ty.t) (ctxt : Alpha_context.context)
  storage_type
  (storage_value : Script_family.Ty.to_Set a) :
  Raw_context.Valid.t ctxt →
  Script_typed_ir.ty.Valid.proj_rel a storage_type
  → Script_typed_ir.Valid.value a storage_value →
  letP ? ' (to_duplicate , ctxt ) :=
  Script_ir_translator.collect_lazy_storage ctxt
  storage_type storage_value
  in Raw_context.Valid.t ctxt.
Proof.
  intros H H1 H2.
  unfold collect_lazy_storage.
  eapply Error.split_letP.
Admitted.

[extract_lazy_storage_diff] is valid. Currently, no pre-condition on [Script_ir_unparser.unparsing_mode], [bool] and Alpha_context.Lazy_storage.IdSet.t

Currently, shortcuts simulations with an existential in the conclusion,

which states that [storage_value] is a [to_value] of something (this is necessary for some proofs). This post-condition allows not specifying the computation of [storage_value] temporarily

Lemma extract_lazy_storage_diff_is_valid (a : Ty.t)
  (ctxt : Alpha_context.context) (mode : Script_ir_unparser.unparsing_mode)
  (temporary : bool)
  (to_duplicate to_update : Alpha_context.Lazy_storage.IdSet.t)
  ty
  (v : Script_family.Ty.to_Set a) :
  Raw_context.Valid.t ctxt →
  Script_typed_ir.ty.Valid.proj_rel a ty →
  Script_typed_ir.Valid.value a v →
  letP ? ' (storage_value , lazy_storage_diff , ctxt )
    := Script_ir_translator.extract_lazy_storage_diff
    ctxt mode temporary to_duplicate to_update ty
    v
  in Raw_context.Valid.t ctxt ∧
      Script_typed_ir.Valid.value a storage_value.
Proof.
Admitted.

Module Fold_lazy_storage.
  Module Valid.

The result of [fold_lazy_storage] is *invalid* if has the shape [Pervasives.OK (Fold_lazy_storage.Error, _)], otherwise is valid. We need this to eliminate [unrechable_gadt_branch] inside [fold_lazy_storage]

    Definition t {A B : Set} (fls : M ? (Fold_lazy_storage.result A × B )) :=
      match fls with
      | Pervasives.Ok (Fold_lazy_storage.Error, _) ⇒ False
      | _ ⇒ True
      end.

The result of [Alpha_context.Lazy_storage.IdSet.fold_f] is OK when has the shape [Fold_lazy_storage.Ok _]. We need this to eliminate [unreachable_gadt_branch] inside [fold_f] function

    Definition is_ok {A : Set} (fls : (Fold_lazy_storage.result A)) :=
      match fls with
      | Fold_lazy_storage.Ok _ ⇒ True
      | Fold_lazy_storage.Error ⇒ False
      end.
  End Valid.
End Fold_lazy_storage.

[fold_lazy_storage] never returns invalid results

Fixpoint dep_fold_lazy_storage_is_valid
  {a} {acc : Set}
  (f_value :
    Alpha_context.Lazy_storage.IdSet.fold_f (Fold_lazy_storage.result acc))
  (init_value : acc) (ctxt : Alpha_context.context) ty
  (x_value : Script_family.Ty.to_Set a)
  (has_lazy_storage_value : has_lazy_storage) :
  Script_typed_ir.ty.Valid.proj_rel a ty →
  (* @TODO 22 November,2022 : write validity predicate for Has_lazy_storage
     we used to have it for old ver. of of Michelson verification.

     Has_lazy_storage.Valid.t has_lazy_storage_value ty -> *)
  (* [f_value] returns [Fold_lazy_storage.Ok] *)
  (∀ {B : Set} (a : Alpha_context.Lazy_storage.Kind.t)
    (b : B)
    (acc' : acc),
    Fold_lazy_storage.Valid.is_ok
      (f_value.(Alpha_context.Lazy_storage.IdSet.fold_f.f)
         a b (Fold_lazy_storage.Ok acc'))) →
  Fold_lazy_storage.Valid.t
    (fold_lazy_storage f_value init_value ctxt ty x_value
       has_lazy_storage_value).
Proof.
  intros H_hls_valid H_f_is_ok.
(*  destruct has_lazy_storage_value, ty; simpl in *;
    try (match goal with
    | H : False |- _ => destruct H
    | |- Fold_lazy_storage.Valid.t
        (let? ' _ := Alpha_context.Gas.consume _ _ in
         return? (Fold_lazy_storage.Ok _, _)) => step; trivial
    end);
    remaining_goals 7.
  all :
    try (
    do 4 step; simpl; trivial; step; simpl; trivial;
    match goal with
    | |- match ?f ?a ?b ?c with _ => _ end =>
        let t := type of b in
        specialize (H_f_is_ok t a b); apply H_f_is_ok
    end).
  { step_let?. destruct x_value. step; try easy;
    destruct p eqn:?, r eqn:?; try easy.
    { apply dep_fold_lazy_storage_is_valid; easy. }
    { match goal with
      | H : dep_fold_lazy_storage ?f_value ?init_value ?t0
        ?ty1 ?t3 ?has_lazy_storage_value1 =
        Pervasives.Ok (Fold_lazy_storage.Error, _) |- _ =>
        specialize (dep_fold_lazy_storage_is_valid _ _
          f_value init_value t0 ty1 t3 has_lazy_storage_value1)
      end;
      rewrite Heqt5 in dep_fold_lazy_storage_is_valid;
      destruct H_hls_valid as [H_hls_valid _];
      now apply (dep_fold_lazy_storage_is_valid H_hls_valid). } }
  all : try (apply dep_fold_lazy_storage_is_valid; easy).
  all : try (do 2 step; simpl; trivial; apply dep_fold_lazy_storage_is_valid; easy).
  (* @TODOs Proofs *)
  { step_let?.
    match goal with
    | |- context [fold_left_e ?f' ?acc' _] =>
        set (f := f'); set (acc_arg := acc')
    end.
    destruct x_value; simpl.
    assert (TODO_fold_left_e :
      Fold_lazy_storage.Valid.t (
        fold_left_e f acc_arg elements)) by admit.
    apply TODO_fold_left_e. }
  { destruct x_value.
    { step_let?.
      match goal with
      | |- context [Script_map.dep_fold ?f' ?x' ?acc'] =>
          assert (TODO_Script_map_dep_fold :
            x' = [] ->
           Script_map.dep_fold f' x' acc' = acc') by admit
      end.
      now rewrite TODO_Script_map_dep_fold. }
    { step_let?.
      match goal with
      | |- context [Script_map.dep_fold ?f ?x ?acc] =>
          assert (TODO_Script_dep_fold :
            Fold_lazy_storage.Valid.t (Script_map.dep_fold f x acc)) by admit
      end.
      apply TODO_Script_dep_fold. } }
  all : remaining_goals 0.
Admitted.
*)

(* @TODO Proofs *)

[fold_lazy_storage f1 a b c d] is equal to [fold_lazy_storage f2 a b c d] if [f1] is pointwise equal to [f2] assumming that [Fold_lazy_storage.ok d] holds.

Admitted.

The function [parse_data] is valid.

Lemma parse_data_is_valid {a : Ty.t}
  elab_conf ctxt allow_forged ty expr :
  Raw_context.Valid.t ctxt →
  a = Script_typed_ir.ty.Valid.to_Ty_t ty →
  letP ? '(result , ctxt ) :=
    parse_data (A := Ty.to_Set a) elab_conf ctxt allow_forged ty expr in
  Raw_context.Valid.t ctxt ∧ Script_typed_ir.Valid.value a result.
Proof.
  intros H H1.
  unfold parse_data.
  unfold parse_data_aux.
Admitted.

(* @TODO already exists above and proved. Compare them and remove one of them  *)

The simulation [dep_unparse_data] is valid.

Lemma unparse_data_is_valid' {t}
  ctxt mode ty a_value :
  Raw_context.Valid.t ctxt →
  Script_typed_ir.ty.Valid.proj_rel t ty →
  Script_typed_ir.Valid.value t a_value →
  letP ? '(_, ctxt ) :=
    Script_ir_translator.unparse_data ctxt mode ty a_value in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [parse_comparable_ty] is valid

Lemma parse_comparable_ty_is_valid {a} ctxt node_val :
  Raw_context.Valid.t ctxt →
  letP ? '(Ex_comparable_ty ty , ctxt') :=
  Script_ir_translator.parse_comparable_ty ctxt node_val in
  Raw_context.Valid.t ctxt' ∧
  a = Script_typed_ir.ty.Valid.to_Ty_t ty ∧
  Script_family.Ty.is_Comparable a.
Proof.
  intro H.
  unfold parse_comparable_ty.
  unfold parse_comparable_ty_aux.
  eapply Error.split_letP.
Admitted.

The function [parse_big_map_value_ty] is valid.

Lemma parse_big_map_value_ty_is_valid ctxt legacy node_value :
  Raw_context.Valid.t ctxt →
  letP ? '(result , ctxt ) := parse_big_map_value_ty ctxt legacy node_value in
  Script_typed_ir.ex_ty.Valid.t result ∧
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [parse_views] is valid

Lemma parse_views_is_valid elab_conf ctxt storage_type function_parameter :
  Raw_context.Valid.t ctxt →
    letP ? '( _ , ctxt ) := parse_views elab_conf ctxt storage_type
      function_parameter
    in Raw_context.Valid.t ctxt.
Proof.
  intro H.
  unfold parse_views.
  unfold Script_map.map_es_in_context.
  destruct function_parameter.
  destruct s.
  eapply Error.split_letP.
Admitted.

The function [parse_data_aux] is valid

#[bypass_check(guard)]
Lemma parse_data_aux_is_valid {a : Ty.t} elab_conf stack_depth ctxt allow_forged ty_value
  script_data :
  Raw_context.Valid.t ctxt →
  Script_typed_ir.ty.Valid.proj_rel a ty_value →
  letP ? '( val , ctxt') := parse_data_aux (a := Ty.to_Set a)
    elab_conf stack_depth ctxt allow_forged ty_value script_data
  in Raw_context.Valid.t ctxt'. (* /\ Script_typed_ir.Valid.value a val. *)
Proof.
Admitted.

Lemma parse_parameter_ty_and_entrypoints_is_valid ctxt b node :
  Raw_context.Valid.t ctxt →
  letP ? '( _ , ctxt') := Script_ir_translator.parse_parameter_ty_and_entrypoints
    ctxt b node
  in Raw_context.Valid.t ctxt'.
Proof.
Admitted.