🍬 Comparable_ty.v

Proofs

Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_typed_ir.

Require TezosOfOCaml.Proto_alpha.Michocoq.syntax_type.

Compute the [Set] representing a [Script_typed_ir.ty].

Fixpoint to_Set (ty : Script_typed_ir.ty) : Set :=
  match ty with
  | Script_typed_ir.Unit_t ⇒ unit
  | Script_typed_ir.Never_t ⇒ Script_typed_ir.never
  | Script_typed_ir.Int_t ⇒ Alpha_context.Script_int.num
  | Script_typed_ir.Nat_t ⇒ Alpha_context.Script_int.num
  | Script_typed_ir.Signature_t ⇒ Script_typed_ir.Script_signature.t
  | Script_typed_ir.String_t ⇒ Alpha_context.Script_string.t
  | Script_typed_ir.Bytes_t ⇒ Bytes.t
  | Script_typed_ir.Mutez_t ⇒ Alpha_context.Tez.t
  | Script_typed_ir.Bool_t ⇒ bool
  | Script_typed_ir.Key_hash_t ⇒ public_key_hash
  | Script_typed_ir.Key_t ⇒ public_key
  | Script_typed_ir.Timestamp_t ⇒ Alpha_context.Script_timestamp.t
  | Script_typed_ir.Chain_id_t ⇒ Script_typed_ir.Script_chain_id.t
  | Script_typed_ir.Address_t ⇒ Script_typed_ir.address
  | Script_typed_ir.Tx_rollup_l2_address_t ⇒
    Script_typed_ir.tx_rollup_l2_address
  | Script_typed_ir.Pair_t ty1 ty2 _ _ ⇒ to_Set ty1 × to_Set ty2
  | Script_typed_ir.Union_t ty1 ty2 _ _ ⇒
    Script_typed_ir.union (to_Set ty1) (to_Set ty2)
  | Script_typed_ir.Option_t ty _ _ ⇒ option (to_Set ty)
  | _ ⇒ unit
  end.

Get the canonical form of a comparable type, erasing the metadata.

Fixpoint get_canonical (ty : Script_typed_ir.ty)
  : Script_typed_ir.ty :=
  match ty with
  | Script_typed_ir.Unit_t ⇒
    Script_typed_ir.Unit_t
  | Script_typed_ir.Never_t ⇒
    Script_typed_ir.Never_t
  | Script_typed_ir.Int_t ⇒
    Script_typed_ir.Int_t
  | Script_typed_ir.Nat_t ⇒
    Script_typed_ir.Nat_t
  | Script_typed_ir.Signature_t ⇒
    Script_typed_ir.Signature_t
  | Script_typed_ir.String_t ⇒
    Script_typed_ir.String_t
  | Script_typed_ir.Bytes_t ⇒
    Script_typed_ir.Bytes_t
  | Script_typed_ir.Mutez_t ⇒
    Script_typed_ir.Mutez_t
  | Script_typed_ir.Bool_t ⇒
    Script_typed_ir.Bool_t
  | Script_typed_ir.Key_hash_t ⇒
    Script_typed_ir.Key_hash_t
  | Script_typed_ir.Key_t ⇒
    Script_typed_ir.Key_t
  | Script_typed_ir.Timestamp_t ⇒
    Script_typed_ir.Timestamp_t
  | Script_typed_ir.Chain_id_t ⇒
    Script_typed_ir.Chain_id_t
  | Script_typed_ir.Address_t ⇒
    Script_typed_ir.Address_t
  | Script_typed_ir.Tx_rollup_l2_address_t ⇒
    Script_typed_ir.Tx_rollup_l2_address_t
  | Script_typed_ir.Pair_t ty1 ty2 _ _ ⇒
    let ty1 := get_canonical ty1 in
    let ty2 := get_canonical ty2 in
    Script_typed_ir.Pair_t ty1 ty2 Ty_metadata.default Dependent_bool.YesYes
  | Script_typed_ir.Union_t ty1 ty2 _ _ ⇒
    let ty1 := get_canonical ty1 in
    let ty2 := get_canonical ty2 in
    Script_typed_ir.Union_t ty1 ty2 Ty_metadata.default Dependent_bool.YesYes
  | Script_typed_ir.Option_t ty _ _ ⇒
    let ty := get_canonical ty in
    Script_typed_ir.Option_t ty Ty_metadata.default Dependent_bool.Yes
  | _ ⇒ Script_typed_ir.Unit_t
  end.

Getting a canonical term is involutive.

Fixpoint get_canonical_is_involutive ty
  : get_canonical (get_canonical ty) = get_canonical ty.
  destruct ty; try reflexivity; simpl;
    repeat match goal with
    | [x : Script_typed_ir.ty × _ |- _] ⇒ destruct x
    end;
    simpl; now repeat rewrite get_canonical_is_involutive.
Qed.

Convert the comparable types to Mi-Cho-Coq for the case of simple comparable types. This does not cover all the cases so we use an option type.

Definition to_Michocoq_simple (ty : Script_typed_ir.ty)
  : option syntax_type.simple_comparable_type :=
  match ty with
  | Script_typed_ir.Unit_t ⇒ Some syntax_type.unit
  | Script_typed_ir.Never_t ⇒ Some syntax_type.never
  | Script_typed_ir.Int_t ⇒ Some syntax_type.int
  | Script_typed_ir.Nat_t ⇒ Some syntax_type.nat
  | Script_typed_ir.Signature_t ⇒ Some syntax_type.signature
  | Script_typed_ir.String_t ⇒ Some syntax_type.string
  | Script_typed_ir.Bytes_t ⇒ Some syntax_type.bytes
  | Script_typed_ir.Mutez_t ⇒ Some syntax_type.mutez
  | Script_typed_ir.Bool_t ⇒ Some syntax_type.bool
  | Script_typed_ir.Key_hash_t ⇒ Some syntax_type.key_hash
  | Script_typed_ir.Key_t ⇒ Some syntax_type.key
  | Script_typed_ir.Timestamp_t ⇒ Some syntax_type.timestamp
  | Script_typed_ir.Chain_id_t ⇒ Some syntax_type.chain_id
  | Script_typed_ir.Address_t ⇒ Some syntax_type.address
  | Script_typed_ir.Tx_rollup_l2_address_t ⇒ None
  | Script_typed_ir.Pair_t _ _ _ _ ⇒ None
  | Script_typed_ir.Union_t _ _ _ _ ⇒ None
  | Script_typed_ir.Option_t _ _ _ ⇒ None
  |_ ⇒ Some syntax_type.unit
  end.

The [to_Michocoq_simple] function does not depend on the metadata.

Lemma to_Michocoq_simple_canonical_eq ty
  : to_Michocoq_simple (get_canonical ty) = to_Michocoq_simple ty.
Proof.
  destruct ty; try reflexivity; simpl;
    now repeat match goal with
    | [x : _ × _ |- _] ⇒ destruct x
    end.
Qed.

Import a simple comparable type from Mi-Cho-Coq, using the default metadata.

Definition of_Michocoq_simple (ty : syntax_type.simple_comparable_type)
  : Script_typed_ir.ty :=
  match ty with
  | syntax_type.string ⇒ Script_typed_ir.String_t
  | syntax_type.nat ⇒ Script_typed_ir.Nat_t
  | syntax_type.int ⇒ Script_typed_ir.Int_t
  | syntax_type.bytes ⇒ Script_typed_ir.Bytes_t
  | syntax_type.bool ⇒ Script_typed_ir.Bool_t
  | syntax_type.mutez ⇒ Script_typed_ir.Mutez_t
  | syntax_type.address ⇒ Script_typed_ir.Address_t
  | syntax_type.key_hash ⇒ Script_typed_ir.Key_hash_t
  | syntax_type.timestamp ⇒ Script_typed_ir.Timestamp_t
  | syntax_type.never ⇒ Script_typed_ir.Never_t
  | syntax_type.key ⇒ Script_typed_ir.Key_t
  | syntax_type.unit ⇒ Script_typed_ir.Unit_t
  | syntax_type.signature ⇒ Script_typed_ir.Signature_t
  | syntax_type.chain_id ⇒ Script_typed_ir.Chain_id_t
  end.

The function [of_Michocoq_simple] produces terms which are already in a canonical form.

Lemma of_Michocoq_simple_is_canonical ty
  : of_Michocoq_simple ty = get_canonical (of_Michocoq_simple ty).
Proof.
  destruct ty; reflexivity.
Qed.

[to_Michocoq_simple] is the inverse of [of_Michocoq_simple].

Lemma to_Michocoq_simple_of_Michocoq_simple ty
  : to_Michocoq_simple (of_Michocoq_simple ty) = Some ty.
Proof.
  destruct ty; reflexivity.
Qed.

[of_Michocoq_simple] is the inverse of [to_Michocoq_simple].

Lemma of_Michocoq_simple_to_Michocoq_simple ty
  : match to_Michocoq_simple ty with
    | Some ty' ⇒ of_Michocoq_simple ty' = get_canonical ty
    | None ⇒ True
    end.
Proof.
  destruct ty; try exact I; reflexivity.
Qed.

Convert comparable types to Mi-Cho-Coq. We use an option type for the cases which are not covered.

Fixpoint to_Michocoq (ty : Script_typed_ir.ty)
  : option syntax_type.comparable_type :=
  match ty with
  | Script_typed_ir.Unit_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.unit)
  | Script_typed_ir.Never_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.never)
  | Script_typed_ir.Int_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.int)
  | Script_typed_ir.Nat_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.nat)
  | Script_typed_ir.Signature_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.signature)
  | Script_typed_ir.String_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.string)
  | Script_typed_ir.Bytes_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.bytes)
  | Script_typed_ir.Mutez_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.mutez)
  | Script_typed_ir.Bool_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.bool)
  | Script_typed_ir.Key_hash_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.key_hash)
  | Script_typed_ir.Key_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.key)
  | Script_typed_ir.Timestamp_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.timestamp)
  | Script_typed_ir.Chain_id_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.chain_id)
  | Script_typed_ir.Address_t ⇒
    Some (syntax_type.Comparable_type_simple syntax_type.address)
  | Script_typed_ir.Tx_rollup_l2_address_t ⇒ None
  | Script_typed_ir.Pair_t ty1 ty2 _ _ ⇒
    let× ty1 := to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.Cpair ty1 ty2)
  | Script_typed_ir.Union_t ty1 ty2 _ _ ⇒
    let× ty1 := to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.Cor ty1 ty2)
  | Script_typed_ir.Option_t ty _ _ ⇒
    let× ty := to_Michocoq ty in
    Some (syntax_type.Coption ty)
  | _ ⇒ Some (syntax_type.Comparable_type_simple syntax_type.unit)
  end.

The [to_Michocoq] function does not depend on the metadata.

Fixpoint to_Michocoq_canonical_eq ty
  : to_Michocoq (get_canonical ty) = to_Michocoq ty.
  destruct ty; try reflexivity; simpl;
  repeat rewrite to_Michocoq_canonical_eq;
  reflexivity.
Qed.

Import a comparable type from Mi-Cho-Coq, using the default metadata.

Fixpoint of_Michocoq (ty : syntax_type.comparable_type)
  : Script_typed_ir.ty :=
  match ty with
  | syntax_type.Comparable_type_simple ty ⇒ of_Michocoq_simple ty
  | syntax_type.Cpair ty1 ty2 ⇒
    let ty1 := of_Michocoq ty1 in
    let ty2 := of_Michocoq ty2 in
    Script_typed_ir.Pair_t ty1 ty2 Ty_metadata.default Dependent_bool.YesYes
  | syntax_type.Coption ty ⇒
    let ty := of_Michocoq ty in
    Script_typed_ir.Option_t ty Ty_metadata.default Dependent_bool.Yes
  | syntax_type.Cor ty1 ty2 ⇒
    let ty1 := of_Michocoq ty1 in
    let ty2 := of_Michocoq ty2 in
    Script_typed_ir.Union_t ty1 ty2 Ty_metadata.default Dependent_bool.YesYes
  end.

The function [of_Michocoq] produces terms which are already in a canonical form.

Fixpoint of_Michocoq_is_canonical ty
  : of_Michocoq ty = get_canonical (of_Michocoq ty).
  destruct ty; simpl; f_equal;
  try apply of_Michocoq_is_canonical.
  apply of_Michocoq_simple_is_canonical.
Qed.

Lemma to_Michocoq_simple_of_Michocoq : ∀ ty ty', to_Michocoq_simple (of_Michocoq ty) = Some ty'
  → ty = syntax_type.Comparable_type_simple ty'.
  induction ty; simpl; intros ty' Heq.
Proof.
  { rewrite to_Michocoq_simple_of_Michocoq_simple in Heq.
    inversion Heq; reflexivity. }
  { discriminate. }
  { discriminate. }
  { discriminate. }
Qed.

[to_Michocoq] is the inverse of [of_Michocoq].

Fixpoint to_Michocoq_of_Michocoq ty
  : to_Michocoq (of_Michocoq ty) = Some ty.
  destruct ty; simpl; sauto lq: on.
Qed.

[of_Michocoq] is the inverse of [to_Michocoq].

Fixpoint of_Michocoq_to_Michocoq_match ty :
  match to_Michocoq ty with
  | Some ty' ⇒ of_Michocoq ty' = get_canonical ty
  | None ⇒ True
  end.
Proof.
  destruct ty; simpl; try reflexivity; hfcrush.
Qed.

Lemma of_Michocoq_to_Michocoq ty ty' :
  to_Michocoq ty = Some ty' →
  of_Michocoq ty' = get_canonical ty.
Proof.
  hfcrush use: of_Michocoq_to_Michocoq_match.
Qed.