Skip to main content

🍬 Ty.v

Proofs

Gitlab

Set the metadata of a type to a default value.
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.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.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.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.Bool_t
    Script_typed_ir.Bool_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.Lambda_t ty1 ty2 _
    let ty1 := get_canonical ty1 in
    let ty2 := get_canonical ty2 in
    Script_typed_ir.Lambda_t ty1 ty2 Ty_metadata.default
  | 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.List_t ty _
    let ty := get_canonical ty in
    Script_typed_ir.List_t ty Ty_metadata.default
  | Script_typed_ir.Set_t ty _
    let ty := Comparable_ty.get_canonical ty in
    Script_typed_ir.Set_t ty Ty_metadata.default
  | Script_typed_ir.Map_t ty1 ty2 _
    let ty1 := Comparable_ty.get_canonical ty1 in
    let ty2 := get_canonical ty2 in
    Script_typed_ir.Map_t ty1 ty2 Ty_metadata.default
  | Script_typed_ir.Big_map_t ty1 ty2 _
    let ty1 := Comparable_ty.get_canonical ty1 in
    let ty2 := get_canonical ty2 in
    Script_typed_ir.Big_map_t ty1 ty2 Ty_metadata.default
  | Script_typed_ir.Contract_t ty _
    let ty := get_canonical ty in
    Script_typed_ir.Contract_t ty Ty_metadata.default
  | Script_typed_ir.Sapling_transaction_t memo_size
    Script_typed_ir.Sapling_transaction_t memo_size
  | Script_typed_ir.Sapling_transaction_deprecated_t memo_size
    Script_typed_ir.Sapling_transaction_deprecated_t memo_size
  | Script_typed_ir.Sapling_state_t memo_size
    Script_typed_ir.Sapling_state_t memo_size
  | Script_typed_ir.Operation_t
    Script_typed_ir.Operation_t
  | Script_typed_ir.Chain_id_t
    Script_typed_ir.Chain_id_t
  | Script_typed_ir.Never_t
    Script_typed_ir.Never_t
  | Script_typed_ir.Bls12_381_g1_t
    Script_typed_ir.Bls12_381_g1_t
  | Script_typed_ir.Bls12_381_g2_t
    Script_typed_ir.Bls12_381_g2_t
  | Script_typed_ir.Bls12_381_fr_t
    Script_typed_ir.Bls12_381_fr_t
  | Script_typed_ir.Ticket_t ty _
    let ty := Comparable_ty.get_canonical ty in
    Script_typed_ir.Ticket_t ty Ty_metadata.default
  | Script_typed_ir.Chest_key_t
    Script_typed_ir.Chest_key_t
  | Script_typed_ir.Chest_t
    Script_typed_ir.Chest_t
  end.

Getting the canonical value of a type 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 : _ × _ |- _] ⇒ destruct x
    end; simpl;
    repeat rewrite Comparable_ty.get_canonical_is_involutive;
    repeat rewrite get_canonical_is_involutive;
    reflexivity.
Qed.

Definition to_memo_size :
  Alpha_context.Sapling.Memo_size.t syntax_type.memo_size:=
  Z.to_nat. (* assuming memo_sizes are non-neg *)

Definition of_memo_size :
  syntax_type.memo_size Alpha_context.Sapling.Memo_size.t :=
  Z.of_nat.

Lemma to_memo_of_memo : sz,
  to_memo_size (of_memo_size sz) = sz.
  exact Nat2Z.id.
Qed.

Lemma of_memo_to_memo : sz,
  0 sz of_memo_size (to_memo_size sz) = sz.
  exact Z2Nat.id.
Qed.

Convert a type to Mi-Cho-Coq.
Fixpoint to_Michocoq (ty : Script_typed_ir.ty) : option syntax_type.type :=
  match ty with
  | Script_typed_ir.Unit_t
    Some (syntax_type.Comparable_type syntax_type.unit)
  | Script_typed_ir.Int_t
    Some (syntax_type.Comparable_type syntax_type.int)
  | Script_typed_ir.Nat_t
    Some (syntax_type.Comparable_type syntax_type.nat)
  | Script_typed_ir.Signature_t
    Some (syntax_type.Comparable_type syntax_type.signature)
  | Script_typed_ir.String_t
    Some (syntax_type.Comparable_type syntax_type.string)
  | Script_typed_ir.Bytes_t
    Some (syntax_type.Comparable_type syntax_type.bytes)
  | Script_typed_ir.Mutez_t
    Some (syntax_type.Comparable_type syntax_type.mutez)
  | Script_typed_ir.Key_hash_t
    Some (syntax_type.Comparable_type syntax_type.key_hash)
  | Script_typed_ir.Key_t
    Some (syntax_type.Comparable_type syntax_type.key)
  | Script_typed_ir.Timestamp_t
    Some (syntax_type.Comparable_type syntax_type.timestamp)
  | Script_typed_ir.Address_t
    Some (syntax_type.Comparable_type syntax_type.address)
  | Script_typed_ir.Tx_rollup_l2_address_t
    None
  | Script_typed_ir.Bool_t
    Some (syntax_type.Comparable_type syntax_type.bool)
  | Script_typed_ir.Pair_t ty1 ty2 _ _
    let× ty1 := to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.pair ty1 ty2)
  | Script_typed_ir.Union_t ty1 ty2 _ _
    let× ty1 := to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.or ty1 ty2)
  | Script_typed_ir.Lambda_t ty1 ty2 _
    let× ty1 := to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.lambda ty1 ty2)
  | Script_typed_ir.Option_t ty _ _
    let× ty := to_Michocoq ty in
    Some (syntax_type.option ty)
  | Script_typed_ir.List_t ty _
    let× ty := to_Michocoq ty in
    Some (syntax_type.list ty)
  | Script_typed_ir.Set_t ty _
    let× ty := Comparable_ty.to_Michocoq ty in
    Some (syntax_type.set ty)
  | Script_typed_ir.Map_t ty1 ty2 _
    let× ty1 := Comparable_ty.to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.map ty1 ty2)
  | Script_typed_ir.Big_map_t ty1 ty2 _
    let× ty1 := Comparable_ty.to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.big_map ty1 ty2)
  | Script_typed_ir.Contract_t ty _
    let× ty := to_Michocoq ty in
    Some (syntax_type.contract ty)
  | Script_typed_ir.Sapling_transaction_t sz
    Some (syntax_type.sapling_transaction (to_memo_size sz))
  | Script_typed_ir.Sapling_transaction_deprecated_t _
    None
  | Script_typed_ir.Sapling_state_t sz
    Some (syntax_type.sapling_state (to_memo_size sz))
  | Script_typed_ir.Operation_tSome syntax_type.operation
  | Script_typed_ir.Chain_id_t
    Some (syntax_type.Comparable_type syntax_type.chain_id)
  | Script_typed_ir.Never_t
    Some (syntax_type.Comparable_type syntax_type.never)
  | Script_typed_ir.Bls12_381_g1_t
    Some syntax_type.bls12_381_g1
  | Script_typed_ir.Bls12_381_g2_t
    Some syntax_type.bls12_381_g2
  | Script_typed_ir.Bls12_381_fr_t
    Some syntax_type.bls12_381_fr
  | Script_typed_ir.Ticket_t ty _
    let× ty := Comparable_ty.to_Michocoq ty in
    Some (syntax_type.ticket ty)
  | Script_typed_ir.Chest_key_tNone
  | Script_typed_ir.Chest_tNone
  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.
Proof.
  destruct ty; try reflexivity; simpl;
  repeat rewrite Comparable_ty.to_Michocoq_canonical_eq;
  repeat rewrite to_Michocoq_canonical_eq;
  reflexivity.
Qed.

Import a type from Mi-Cho-Coq.
Fixpoint of_Michocoq (ty : syntax_type.type) : Script_typed_ir.ty :=
  match ty with
  | syntax_type.Comparable_type ty
    match ty with
    | syntax_type.stringScript_typed_ir.String_t
    | syntax_type.natScript_typed_ir.Nat_t
    | syntax_type.intScript_typed_ir.Int_t
    | syntax_type.bytesScript_typed_ir.Bytes_t
    | syntax_type.boolScript_typed_ir.Bool_t
    | syntax_type.mutezScript_typed_ir.Mutez_t
    | syntax_type.addressScript_typed_ir.Address_t
    | syntax_type.key_hashScript_typed_ir.Key_hash_t
    | syntax_type.timestampScript_typed_ir.Timestamp_t
    | syntax_type.chain_idScript_typed_ir.Chain_id_t
    | syntax_type.signatureScript_typed_ir.Signature_t
    | syntax_type.unitScript_typed_ir.Unit_t
    | syntax_type.keyScript_typed_ir.Key_t
    | syntax_type.neverScript_typed_ir.Never_t
    end
  | syntax_type.ticket ty
    let ty := Comparable_ty.of_Michocoq ty in
    Script_typed_ir.Ticket_t ty Ty_metadata.default
  | syntax_type.option ty
    let ty := of_Michocoq ty in
    Script_typed_ir.Option_t ty Ty_metadata.default Dependent_bool.Yes
  | syntax_type.list ty
    let ty := of_Michocoq ty in
    Script_typed_ir.List_t ty Ty_metadata.default
  | syntax_type.set ty
    let ty := Comparable_ty.of_Michocoq ty in
    Script_typed_ir.Set_t ty Ty_metadata.default
  | syntax_type.contract ty
    let ty := of_Michocoq ty in
    Script_typed_ir.Contract_t ty Ty_metadata.default
  | syntax_type.operationScript_typed_ir.Operation_t
  | syntax_type.pair 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.or 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
  | syntax_type.lambda ty1 ty2
    let ty1 := of_Michocoq ty1 in
    let ty2 := of_Michocoq ty2 in
    Script_typed_ir.Lambda_t ty1 ty2 Ty_metadata.default
  | syntax_type.map ty1 ty2
    let ty1 := Comparable_ty.of_Michocoq ty1 in
    let ty2 := of_Michocoq ty2 in
    Script_typed_ir.Map_t ty1 ty2 Ty_metadata.default
  | syntax_type.big_map ty1 ty2
    let ty1 := Comparable_ty.of_Michocoq ty1 in
    let ty2 := of_Michocoq ty2 in
    Script_typed_ir.Big_map_t ty1 ty2 Ty_metadata.default
  | syntax_type.sapling_state sz
    Script_typed_ir.Sapling_state_t (of_memo_size sz)
  | syntax_type.sapling_transaction sz
    Script_typed_ir.Sapling_transaction_t
      (of_memo_size sz)
  | syntax_type.bls12_381_fr
    Script_typed_ir.Bls12_381_fr_t
  | syntax_type.bls12_381_g1
    Script_typed_ir.Bls12_381_g1_t
  | syntax_type.bls12_381_g2
    Script_typed_ir.Bls12_381_g2_t
  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).
Proof.
  destruct ty; simpl;
    repeat rewrite <- Comparable_ty.of_Michocoq_is_canonical;
    repeat rewrite <- of_Michocoq_is_canonical;
    try reflexivity.
    destruct_all syntax_type.simple_comparable_type; reflexivity.
Qed.

[to_Michocoq] is the inverse of [of_Michocoq].
Fixpoint to_Michocoq_of_Michocoq ty
  : to_Michocoq (of_Michocoq ty) = Some ty.
Proof.
  destruct ty; simpl;
    repeat rewrite Comparable_ty.to_Michocoq_of_Michocoq;
    repeat rewrite to_Michocoq_of_Michocoq;
    try reflexivity;
  destruct_all syntax_type.simple_comparable_type;
  try rewrite to_memo_of_memo; try reflexivity.
Qed.

Fixpoint all_memo_sizes_nonneg(ty : Script_typed_ir.ty) : Prop :=
  match ty with
  | Script_typed_ir.Sapling_transaction_t sz ⇒ 0 sz
  | Script_typed_ir.Sapling_transaction_deprecated_t sz ⇒ 0 sz
  | Script_typed_ir.Sapling_state_t sz ⇒ 0 sz
  | Script_typed_ir.Pair_t ty1 ty2 _ _
       all_memo_sizes_nonneg ty1
     all_memo_sizes_nonneg ty2
  | Script_typed_ir.Union_t ty1 ty2 _ _
       all_memo_sizes_nonneg ty1
     all_memo_sizes_nonneg ty2
  | Script_typed_ir.Lambda_t ty1 ty2 _
       all_memo_sizes_nonneg ty1
     all_memo_sizes_nonneg ty2
  | Script_typed_ir.Option_t ty _ _all_memo_sizes_nonneg ty
  | Script_typed_ir.List_t ty _all_memo_sizes_nonneg ty
  | Script_typed_ir.Contract_t ty _all_memo_sizes_nonneg ty
  | Script_typed_ir.Map_t _ ty _all_memo_sizes_nonneg ty
  | Script_typed_ir.Big_map_t _ ty _all_memo_sizes_nonneg ty
  | Script_typed_ir.Unit_t
  | Script_typed_ir.Int_t
  | Script_typed_ir.Nat_t
  | Script_typed_ir.Signature_t
  | Script_typed_ir.String_t
  | Script_typed_ir.Bytes_t
  | Script_typed_ir.Mutez_t
  | Script_typed_ir.Key_hash_t
  | Script_typed_ir.Key_t
  | Script_typed_ir.Timestamp_t
  | Script_typed_ir.Bool_t
  | Script_typed_ir.Set_t _ _
  | Script_typed_ir.Operation_t
  | Script_typed_ir.Chain_id_t
  | Script_typed_ir.Never_t
  | Script_typed_ir.Bls12_381_g1_t
  | Script_typed_ir.Bls12_381_g2_t
  | Script_typed_ir.Bls12_381_fr_t
  | Script_typed_ir.Ticket_t _ _
  | Script_typed_ir.Chest_key_t
  | Script_typed_ir.Chest_t
  | Script_typed_ir.Address_t
  | Script_typed_ir.Tx_rollup_l2_address_t
    ⇒ True
  end.

[of_Michocoq] is the inverse of [to_Michocoq].
Fixpoint of_Michocoq_to_Michocoq ty
  : all_memo_sizes_nonneg ty
    match to_Michocoq ty with
    | Some ty'of_Michocoq ty' = get_canonical ty
    | NoneTrue
    end.
Proof.
  intro nn.
  destruct ty; simpl; trivial;
    repeat match goal with
    | [x : _ × _ |- _] ⇒ destruct x
    end; simpl;
    repeat match goal with
    | [ty : _ |- _] ⇒
      let H := fresh "H" in
      (
        (assert (H := Comparable_ty.of_Michocoq_to_Michocoq ty);
        destruct (Comparable_ty.to_Michocoq ty)) ||
        (assert (H := of_Michocoq_to_Michocoq ty);
        destruct (to_Michocoq ty))
      );
      revert ty H;
      simpl; trivial
    end;
    try congruence.
  { destruct nn as [nn1 nn2].
    destruct (to_Michocoq ty1) eqn:G1;
    destruct (to_Michocoq ty2) eqn:G2; simpl; try tauto.
    pose (of_Michocoq_to_Michocoq ty1 nn1) as IH1.
    pose (of_Michocoq_to_Michocoq ty2 nn2) as IH2.
    rewrite G1 in IH1.
    rewrite G2 in IH2.
    congruence.
  }
  { destruct nn as [nn1 nn2].
    destruct (to_Michocoq ty1) eqn:G1;
    destruct (to_Michocoq ty2) eqn:G2; simpl; try tauto.
    pose (of_Michocoq_to_Michocoq _ nn1) as IH1.
    pose (of_Michocoq_to_Michocoq _ nn2) as IH2.
    rewrite G1 in IH1.
    rewrite G2 in IH2.
    congruence.
  }
  { destruct nn as [nn1 nn2].
    destruct (to_Michocoq ty1) eqn:G1;
    destruct (to_Michocoq ty2) eqn:G2; simpl; try tauto.
    pose (of_Michocoq_to_Michocoq _ nn1) as IH1.
    pose (of_Michocoq_to_Michocoq _ nn2) as IH2.
    rewrite G1 in IH1.
    rewrite G2 in IH2.
    congruence.
  }
  { destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    f_equal.
    simpl in nn.
    pose (of_Michocoq_to_Michocoq _ nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    f_equal.
    simpl in nn.
    pose (of_Michocoq_to_Michocoq _ nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    now erewrite Comparable_ty.of_Michocoq_to_Michocoq.
  }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    erewrite Comparable_ty.of_Michocoq_to_Michocoq by eassumption.
    f_equal; try apply Comparable_ty.of_Michocoq_to_Michocoq.
    pose (of_Michocoq_to_Michocoq ty nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    erewrite Comparable_ty.of_Michocoq_to_Michocoq by eassumption.
    f_equal; try apply Comparable_ty.of_Michocoq_to_Michocoq.
    pose (of_Michocoq_to_Michocoq ty nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    f_equal; try apply Comparable_ty.of_Michocoq_to_Michocoq.
    pose (of_Michocoq_to_Michocoq ty nn) as IH.
    rewrite G in IH; auto.
  }
  { f_equal. apply of_memo_to_memo; exact nn. }
  { f_equal. apply of_memo_to_memo; exact nn. }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    now erewrite Comparable_ty.of_Michocoq_to_Michocoq.
  }
Qed.