🍬 Script_ir_unparser.v
Proofs
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.
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.
(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.
(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
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.
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.
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
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.
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.
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.
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.
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.
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.
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.
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.
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. *)
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.
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.
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.
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.
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.
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.
(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.
(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.
(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.