🍬 Script_ir_unparser.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import Coq.Program.Equality.

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Script_ir_unparser.

Require TezosOfOCaml.Environment.V8.Proofs.Error_monad.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Proofs.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_family.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.

(* Require TezosOfOCaml.Proto_alpha.Simulations.Script_tc_errors. *)
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

The function [unparse_ty] is valid.

Lemma unparse_ty_is_valid {A : Set}
  (loc_value : A) (ctxt : Alpha_context.context) ty :
  Raw_context.Valid.t ctxt →
  letP? '(script, ctxt) :=
    Script_ir_unparser.unparse_ty loc_value ctxt ty in
  Raw_context.Valid.t ctxt.
Proof.
  intros.
  unfold Script_ir_unparser.unparse_ty.
  Raw_context.Valid.destruct_rewrite H.
  eapply Error.split_letP; [|hauto l: on].
  unfold Alpha_context.Gas.consume,
         Raw_context.consume_gas,
         Gas_limit_repr.raw_consume,
         Unparse_costs.unparse_type.
  (* @TODO Question : Looks like this Lemma is unprovable, cos
                      [cost_UNPARSE_TYPE] is not necessarily zero.  *)
  Admitted.

Helper lemma

Lemma unparse_comparable_ty_uncarbonated_helper_eq {loc : Set}
  (loc_value : loc) ty :
  unparse_comparable_ty_uncarbonated loc_value ty =
  unparse_ty_and_entrypoints_uncarbonated loc_value ty
    Script_typed_ir.no_entrypoints.
Proof.
  sauto lq: on rew: off.
Qed.

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

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

The function [unparse_comparable_data] is valid.

Lemma unparse_comparable_data_is_valid {a} {loc : Set}
  ctxt mode ty (value : Ty.to_Set a) :
  Raw_context.Valid.t ctxt →
  Script_typed_ir.ty.Comparable.t ty →
  Script_typed_ir.ty.Valid.t ty →
  a = Script_typed_ir.ty.Valid.to_Ty_t ty →
  Script_typed_ir.Valid.value a value →
  letP? '(_, ctxt) :=
    Script_ir_unparser.unparse_comparable_data ctxt mode ty value in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

Definition z_number_10001 : Z.t := 10001.
#[global] Opaque z_number_10001.
(* @TODO 2022/11/22 : uncomment if we will need it in updated Michelson
(** [stack_depth_to_fuel] and [fuel_to_stack_depth] are inverses. *)
Lemma stack_depth_to_fuel_to_stack_depth stack_depth :
  0 <= stack_depth <= Script_ir_unparser.z_number_10001 ->
  Script_ir_unparser.fuel_to_stack_depth
    (Script_ir_unparser.stack_depth_to_fuel stack_depth) = stack_depth.
Proof.
  unfold Script_ir_unparser.fuel_to_stack_depth,
    Script_ir_unparser.stack_depth_to_fuel.
  lia.
Qed.
*)

Module Data_unparser.

[unparse_data_aux] is valid This lemma is used in [Script_ir_translator.v] to verify [unparse_data] No pre-condition on [mode] (should probably stay that way) *Missing* pre-condition on the functor [F]. No post-condition on the 1st element of the record.

  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.

The lemma [dep_unparse_data_aux_eq] above should be updated: 1. It does not contain validity condition 2. There are two functors parameters, whereas we *a priori* need only one

  Admitted.
End Data_unparser.

The function [unparse_timestamp] is valid.

Lemma unparse_timestamp_is_valid {A B : Set}
  loc_value ctxt mode t_value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_timestamp A B
      loc_value ctxt mode t_value in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_timestamp. step; trivial.
  apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)).
  apply Alpha_context.Gas.consume_is_valid; trivial; easy.
  intros. step; scongruence.
Qed.

The function [unparse_address] is valid.

Lemma unparse_address_is_valid {A B : Set}
  loc_value ctxt mode function_parameter :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_address A B
      loc_value ctxt mode function_parameter in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_address. step.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_tx_rollup_l2_address] is valid.

Lemma unparse_tx_rollup_l2_address_is_valid {A B : Set}
  loc_value ctxt mode tx_address :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_tx_rollup_l2_address A B
      loc_value ctxt mode tx_address in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_tx_rollup_l2_address. step.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_contract] is valid.

Lemma unparse_contract_is_valid {A B : Set}
  loc_value ctxt mode typed_contract :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_contract A B
      loc_value ctxt mode typed_contract in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_contract.
  apply unparse_address_is_valid; trivial; easy.
Qed.

The function [unparse_signature] is valid.

Lemma unparse_signature_is_valid {A B : Set}
  loc_value ctxt mode s_value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_signature A B
      loc_value ctxt mode s_value in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt; unfold unparse_signature; step.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_mutez] is valid.

Lemma unparse_mutez_is_valid {A _ C _: Set}
  loc_value ctxt v_value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_mutez A _ C _
      loc_value ctxt v_value in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_mutez; scongruence.
Qed.

The function [unparse_key] is valid.

Lemma unparse_key_is_valid {A B : Set}
  loc_value ctxt mode k_value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_key A B
      loc_value ctxt mode k_value in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_key; step.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_key_hash] is valid.

Lemma unparse_key_hash_is_valid {A B : Set}
  loc_value ctxt mode k_value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_key_hash A B
      loc_value ctxt mode k_value in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_key_hash; step.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_operation] is valid.

Lemma unparse_operation_is_valid {A B : Set}
  loc_value ctxt value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_operation A B
      loc_value ctxt value in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_operation.
  apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x));
    [|scongruence].
  apply Alpha_context.Gas.consume_is_valid; trivial.
Admitted. (* @TODO. Create auxiliary lemma. *)

The function [unparse_chain_id] is valid.

Lemma unparse_chain_id_is_valid {A B : Set}
  loc_value ctxt mode chain_id :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_chain_id A B
      loc_value ctxt mode chain_id in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_chain_id. step.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_bls12_381_g1] is valid.

Lemma unparse_bls12_381_g1_is_valid {A B : Set}
  loc_value ctxt x :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_bls12_381_g1 A B
      loc_value ctxt x in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_bls12_381_g1.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_bls12_381_g2] is valid.

Lemma unparse_bls12_381_g2_is_valid {A B : Set}
  loc_value ctxt x :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_bls12_381_g2 A B
      loc_value ctxt x in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_bls12_381_g2.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_bls12_381_fr] is valid.

Lemma unparse_bls12_381_fr_is_valid {A B : Set}
  loc_value ctxt x :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_bls12_381_fr A B
      loc_value ctxt x in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt. unfold unparse_bls12_381_fr.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; easy; scongruence).
Qed.

The function [unparse_with_data_encoding] is valid.

Lemma unparse_with_data_encoding_is_valid {A B C : Set}
  loc_value ctxt s unparse_cost encoding :
  Raw_context.Valid.t ctxt →
  Saturation_repr.Valid.t unparse_cost →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_with_data_encoding A B C
      loc_value ctxt s unparse_cost encoding in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt H_cost. unfold unparse_with_data_encoding.
  all :
    try (apply Error.split_letP with (P:=(fun x ⇒ Raw_context.Valid.t x)));
    try (apply Alpha_context.Gas.consume_is_valid; trivial);
    try (intros; scongruence).
Qed.

The function [unparse_pair] is valid.

Lemma unparse_pair_is_valid {A C E r : Set}
  (P : C → Prop)
  (Q : r → Prop)
  (loc_value : A)
  (unparse_l : Proto_alpha.Raw_context.t → C →
    M? (Micheline.node A Michelson_v1_primitives.prim ×
      Proto_alpha.Raw_context.t))
  (unparse_r : Proto_alpha.Raw_context.t → r →
    M? (Micheline.node A Michelson_v1_primitives.prim ×
      Proto_alpha.Raw_context.t))
  (ctxt : Proto_alpha.Raw_context.t)
  mode
  witness
  (parameter : C × r) :
  Raw_context.Valid.t ctxt →
  (∀ ctxt v,
    Raw_context.Valid.t ctxt →
    letP? '(_, ctxt) := unparse_l ctxt v in
    Raw_context.Valid.t ctxt
  ) →
  (∀ ctxt v,
    Raw_context.Valid.t ctxt →
    letP? '(_, ctxt) := unparse_r ctxt v in
    Raw_context.Valid.t ctxt
  ) →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_pair A _ C Proto_alpha.Raw_context.t _ r _
      loc_value unparse_l unparse_r ctxt mode witness parameter in
  Raw_context.Valid.t ctxt.
Proof.
  intros; unfold unparse_pair. step.
  eapply Error.split_letP.
  apply H0; trivial.
  intros. step. eapply Error.split_letP.
  apply H1; trivial.
  intros. step. simpl. trivial.
Qed.

The function [unparse_union] is valid.

Lemma unparse_union_is_valid {A C F : Set}
  (P : C → Prop)
  (Q : F → Prop)
  loc_value unparse_l unparse_r ctxt parameter :
  Raw_context.Valid.t ctxt →
  (∀ ctxt v,
    Raw_context.Valid.t ctxt →
    P v →
    letP? '(_, ctxt) := unparse_l ctxt v in
    Raw_context.Valid.t ctxt
  ) →
  (∀ ctxt v,
    Raw_context.Valid.t ctxt →
    Q v →
    letP? '(_, ctxt) := unparse_r ctxt v in
    Raw_context.Valid.t ctxt
  ) →
  ( match parameter with
    | Script_typed_ir.L l_value ⇒ P l_value
    | Script_typed_ir.R r_value ⇒ Q r_value
    end ) →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_union A _ C _ _ F
      loc_value unparse_l unparse_r ctxt parameter in
  Raw_context.Valid.t ctxt.
Proof.
  intros. unfold unparse_union.
  step.
  eapply Error.split_letP.
  apply H0; trivial.
  intros [] **.
  apply H3.
  eapply Error.split_letP.
  apply H1; trivial.
  intros [] **.
  apply H3.
Qed.

The function [unparse_option] is valid.

Lemma unparse_option_is_valid {A C : Set}
  (P : C → Prop)
  loc_value unparse_v ctxt v :
  Raw_context.Valid.t ctxt →
  (∀ ctxt v,
    Raw_context.Valid.t ctxt →
    P v →
    letP? '(_, ctxt) := unparse_v ctxt v in
    Raw_context.Valid.t ctxt
  ) →
  Option.Forall P v →
  letP? '(_, ctxt) :=
    @Script_ir_unparser.unparse_option A _ C _
      loc_value unparse_v ctxt v in
  Raw_context.Valid.t ctxt.
Proof.
  intros.
  unfold unparse_option. step; [|trivial].
  eapply Error.split_letP.
  apply H0; trivial.
  intros [] **.
  apply H2.
Qed.