🍬 Script_comparable.v

Proofs

See code, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Script_comparable.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Chain_id.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_int_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_string_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_timestamp_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.Comparable_ty.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.Never.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.Union.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_address.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_comparable.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_typed_ir.

This comparison function is valid.

Lemma compare_address_is_valid
  : Compare.Valid.t (fun _ ⇒ True) id Script_comparable.compare_address.
Proof.
  apply (Compare.equality (
    let proj '(Script_typed_ir.address.Build contract entrypoint) :=
      (contract, entrypoint) in
    Compare.projection proj (Compare.lexicographic
      Destination_repr.compare Entrypoint_repr.compare)
  )); [
    unfold Compare.projection, Script_comparable.compare_address;
    hauto lq: on|].
  eapply Compare.implies.
  { eapply Compare.projection_is_valid.
    eapply Compare.lexicographic_is_valid.
    { apply Destination_repr.compare_is_valid. }
    { apply Entrypoint_repr.compare_is_valid. }
  }
  all: sauto q: on.
Qed.
#[global] Hint Resolve compare_address_is_valid : Compare_db.

[compare_tx_rollup_l2_address] function is valid.

Lemma compare_tx_rollup_l2_address_is_valid
  : Compare.Valid.t
      Indexable.Value.Valid.t id Script_comparable.compare_tx_rollup_l2_address.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_tx_rollup_l2_address_is_valid : Compare_db.

Fixpoint canonize (t : Ty.t)
  (x : Ty.to_Set t)
  : Ty.to_Set t :=
  match t, x with
  | Ty.Unit, x ⇒ x
  | Ty.Num _, x ⇒ x
  | Ty.Signature, x ⇒
    let signature := Script_typed_ir.Script_signature.get x in
    Script_typed_ir.Script_signature.make (Signature.canonize signature)
  | Ty.String, x ⇒ x
  | Ty.Bytes, x ⇒ x
  | Ty.Mutez, x ⇒ x
  | Ty.Key_hash, x ⇒ x
  | Ty.Key, x ⇒ x
  | Ty.Timestamp, x ⇒ x
  | Ty.Address, x ⇒ x
  | Ty.Tx_rollup_l2_address, x ⇒ x
  | Ty.Bool, x ⇒ x
  | Ty.Pair tl tr, (l, r) ⇒
    (canonize tl l, canonize tr r)
  | Ty.Union tl tr, x ⇒
    match x with
    | Script_typed_ir.L x ⇒ Script_typed_ir.L (canonize tl x)
    | Script_typed_ir.R x ⇒ Script_typed_ir.R (canonize tr x)
    end
  | Ty.Lambda _ _ , x ⇒ x
  | Ty.Option t, x ⇒
    match x with
    | None ⇒ None
    | Some x ⇒ Some (canonize t x)
    end
  | Ty.List _, x ⇒ x
  | Ty.Set_ _, x ⇒ x
  | Ty.Map _ _, x ⇒ x
  | Ty.Big_map _ _, x ⇒ x
  | Ty.Contract _, x ⇒ x
  | Ty.Sapling_transaction, x ⇒ x
  | Ty.Sapling_transaction_deprecated, x ⇒ x
  | Ty.Sapling_state, x ⇒ x
  | Ty.Operation, x ⇒ x
  | Ty.Chain_id, x ⇒ x
  | Ty.Never, x ⇒ x
  | Ty.Bls12_381_g1, x ⇒ x
  | Ty.Bls12_381_g2, x ⇒ x
  | Ty.Bls12_381_fr, x ⇒ x
  | Ty.Ticket _, x ⇒ x
  | Ty.Chest_key, x ⇒ x
  | Ty.Chest, x ⇒ x
  end.

We first re-define the comparison function without GADTs casts. We also pre-evaluate the continuation, so that the termination criteria for fixpoints is valid.

Module Compare_comparable.

This definition is equivalent to the original one.

  Fixpoint dep_compare_comparable_eq t k x y
    (ty : With_family.ty t)
    {struct ty}
    : Script_typed_ir.With_family.is_Comparable ty →
      Script_comparable.Compare_comparable.compare_comparable
        (With_family.to_ty ty) k x y =
      let k_result :=
        match k with
        | Script_comparable.Compare_comparable_return ⇒ 0
        | Script_comparable.Compare_comparable t x y k ⇒
          Script_comparable.Compare_comparable.compare_comparable t k x y
        end in
      Compare_comparable.dep_compare_comparable t k_result x y.
  Proof.
    destruct ty; simpl in *; repeat rewrite cast_eval; try easy;
      destruct_all Dependent_bool.dand;
      destruct_all Dependent_bool.dbool;
      try easy;
      cbn in *;
      intros; try rewrite_cast_exists;
      repeat step;
      repeat rewrite dep_compare_comparable_eq; try easy.
  Qed.

A lemma to unfold the use of the continuation.

  (* Fixpoint compare_comparable_continuation t t' k
    (x y : Ty.to_Set t)
    (x' y' : Ty.to_Set t')
    {struct t}
    : Compare_comparable.dep_compare_comparable 
        t
        (Compare_comparable.dep_compare_comparable t' k x' y') x y =
      let res := Compare_comparable.dep_compare_comparable t 0 x y in
      match res with
      | 0 => Compare_comparable.dep_compare_comparable t' k x' y'
      | _ => res
      end.
    destruct t; simpl; trivial;
      try match goal with
      | [|- match ?e with _ => _ end = _] => try now destruct e
      end;
      repeat match goal with
      | [p : Script_typed_ir.comparable_ty * _ |- _] => destruct p
      end.
      destruct x, y; try easy; step; admit.
    (* repeat (rewrite compare_comparable_continuation; try simpl; try step); try reflexivity.
    hauto drew: off.
    hauto drew: off. *)
  Admitted. *)
End Compare_comparable.

The simulation [dep_compare_comparable] is valid.

Lemma dep_compare_comparable_eq t (ty : With_family.ty t) :
  Script_typed_ir.With_family.is_Comparable ty →
  Script_comparable.dep_compare_comparable t =
  Script_comparable.compare_comparable (With_family.to_ty ty).
Proof.
  intros.
  unfold Script_comparable.compare_comparable.
  repeat (apply FunctionalExtensionality.functional_extensionality_dep; intro).
  now rewrite Compare_comparable.dep_compare_comparable_eq.
Qed.

(*
Definition compare_comparable_without_gadts
  (t : Script_typed_ir.comparable_ty)
  : Script_typed_ir.Comparable_ty.to_Set t ->
    Script_typed_ir.Comparable_ty.to_Set t ->
    int :=
  Compare_comparable_without_gadts.compare_comparable t 0.

(** We show that the comparison without GADTs is valid. In this proof, we mainly
    use lemma about the various comparison functions which we call. For the pair
    case, we first unfold the continuation and then show that it is like the
    lexicographic order. *)
Fixpoint compare_comparable_without_gadts_is_pre_valid t :
  Compare.Valid.t (fun _ => True) (canonize t)
    (compare_comparable_without_gadts t).
Proof.
  destruct t;
    try apply Signature.compare_is_valid;
    try apply Compare.wrap_compare_is_valid;
    try first [
      apply Compare.unit_is_valid |
      apply Script_typed_ir.Never.compare_is_valid |
      apply Script_int_repr.compare_is_valid |
      apply Script_string_repr.compare_is_valid |
      apply Compare.string_is_valid |
      apply Signature.Public_key_hash_compare_is_valid |
      apply Signature.Public_key_compare_is_valid |
      apply Signature.compare_is_valid |
      apply Script_typed_ir.Script_chain_id.compare_is_valid |
      apply Compare.bool_is_valid |
      apply compare_address_is_valid |
      apply Script_typed_ir.Script_signature.compare_is_valid |
      apply Tez_repr.compare_is_valid |
      apply Script_timestamp_repr.compare_is_valid |
      apply Tx_rollup_l2_address.Indexable.compare_values_is_valid
    ];
    repeat match goal with
    | [p : Script_typed_ir.comparable_ty * _ |- _] => destruct p
    end;
    try (
      apply Script_typed_ir.Union.compare_is_valid;
      apply compare_comparable_without_gadts_is_pre_valid
    ).
  { apply (Compare.equality (
      Compare.lexicographic_compare
        (compare_comparable_without_gadts _)
        (compare_comparable_without_gadts _)
    )).
    { intros; destruct x, y.
      unfold compare_comparable_without_gadts; simpl.
      rewrite Compare_comparable_without_gadts.compare_comparable_continuation.
      reflexivity.
    }
    { eapply Compare.implies.
      { eapply Compare.lexicographic_is_valid;
          apply compare_comparable_without_gadts_is_pre_valid.
      }
      all: hauto l: on.
    }
  }
  {
    eapply Compare.implies.
    { eapply Compare.option_is_valid.
      apply compare_comparable_without_gadts_is_pre_valid.
    }
    all: hauto l: on.
  }
Qed.

(** We conclude that the original comparison function with GADTs is valid. *)
Lemma compare_comparable_is_pre_valid t :
  Compare.Valid.t (a := Script_typed_ir.Comparable_ty.to_Set t)
    (fun _ => True) (canonize t) (Script_comparable.compare_comparable t).
Proof.
  apply (Compare.equality (compare_comparable_without_gadts t)).
  { intros; now rewrite compare_comparable_without_gadts_eq. }
  { apply compare_comparable_without_gadts_is_pre_valid. }
Qed.
 *)