Skip to main content

🍬 Script_ir_translator.v


See code, Gitlab , OCaml

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 [ ctxt m] expression in the goal
Ltac run_gas_monad := destruct 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
  unfold Script_ir_unparser.unparse_ty_and_entrypoints_uncarbonated.
  destruct ty; trivial. step; trivial. step; trivial. step; trivial.
  simpl; trivial.

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

(* 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
  (H : Script_typed_ir.ty.Valid.t ty) {struct ty} :
    parse_ty_aux ctxt stack_depth a b c d e Don't_parse_entrypoints
      (Script_ir_unparser.unparse_ty_uncarbonated loc ty)
  | V0.Pervasives.Ok (Script_typed_ir.Ex_ty ty', _)ty = ty'
  | V0.Pervasives.Error _True
  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.
    (* 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.
    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.
    rewrite Dep_bool.
    rewrite metadata_size.
    rewrite H.
    rewrite H0.
  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
    | Pervasives.Error _True
  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.

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

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
    | Pervasives.Error _True
  intros cty loc ctxt H H1;
    unfold parse_comparable_ty, Script_ir_unparser.unparse_ty.
  destruct Alpha_context.Gas.consume eqn:Egc; simpl;

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

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
    | Pervasives.Error _True
  ez destruct (parse_comparable_ty _ _ ) eqn:?H_parse_comparable_ty.
  do 2 step_outer; [|easy].
  revert H_parse_comparable_ty Heqt.
  destruct node;
  match goal with
  | |- context [Prim _ _ _ _] ⇒ idtac
  | |- _cbn; now destruct (Alpha_context.Gas.consume _ _)
  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. *)

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.fuel_to_stack_depth fuel) =
  unfold Script_ir_unparser.fuel_to_stack_depth,

The function [dep_parse_comparable_ty] is valid
Some validity predicate on [F]
[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]
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 ->
    (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'.
  (* @TODO Simulation: Complete the simulatin of dep_parse_contract_for_script *)

@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.
@TODO use the two previous lemmas

[collect_lazy_storage] is valid. No post-condition in the ouput for to_duplicate
[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
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

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.ErrorFalse
  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),
         a b (Fold_lazy_storage.Ok acc')))
    (fold_lazy_storage f_value init_value ctxt ty x_value
  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
    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
  { 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)
      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')
    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
      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
      apply TODO_Script_dep_fold. } }
  all : remaining_goals 0.

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

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.
  intros H H1.
  unfold parse_data.
  unfold parse_data_aux.

(* @TODO already exists above and proved. Compare them and remove one of them  *)
The simulation [dep_unparse_data] is valid.
The function [parse_comparable_ty] is valid
The function [parse_big_map_value_ty] is valid.
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
    in Raw_context.Valid.t ctxt.
  intro H.
  unfold parse_views.
  unfold Script_map.map_es_in_context.
  destruct function_parameter.
  destruct s.
  eapply Error.split_letP.

The function [parse_data_aux] is valid