Skip to main content

Script_comparable.v

Source: src/Proto_alpha/Proofs/Script_comparable.v

This comparison function is valid.
Lemma compare_address_is_valid
  : Compare.Valid.t (Compare.wrap_compare Script_comparable.compare_address).
  apply (Compare.Valid.equality (compare1 :=
    Compare.lexicographic_compare
      (Compare.wrap_compare Alpha_context.Contract.compare)
      (Compare.wrap_compare Compare.String.(Compare.S.compare))
  )).
  { intros.
    destruct x, y.
    unfold Compare.wrap_compare, Compare.lexicographic_compare,
      Script_comparable.compare_address.
    now destruct (Alpha_context.Contract.compare _ _).
  }
  { apply Compare.Valid.lexicographic_compare;
      try apply Contract_repr.compare_is_valid;
      try apply Compare.Valid.string.
  }
Qed.

Fixpoint canonize (t : Script_typed_ir.comparable_ty)
  (x : Script_typed_ir.Comparable_ty.to_Set t)
  : Script_typed_ir.Comparable_ty.to_Set t :=
  match t, x with
  | Script_typed_ir.Unit_key _, _x
  | Script_typed_ir.Never_key _, xx
  | Script_typed_ir.Signature_key _, xSignature.canonize x
  | Script_typed_ir.String_key _, xx
  | Script_typed_ir.Bool_key _, xx
  | Script_typed_ir.Mutez_key _, xx
  | Script_typed_ir.Key_hash_key _, xx
  | Script_typed_ir.Key_key _, xx
  | Script_typed_ir.Int_key _, xx
  | Script_typed_ir.Nat_key _, xx
  | Script_typed_ir.Timestamp_key _, xx
  | Script_typed_ir.Address_key _, xx
  | Script_typed_ir.Bytes_key _, xx
  | Script_typed_ir.Chain_id_key _, xx
  | Script_typed_ir.Pair_key (tl, _) (tr, _) _, (l, r)
    (canonize tl l, canonize tr r)
  | Script_typed_ir.Union_key (tl, _) (tr, _) _, x
    match x with
    | Script_typed_ir.L xScript_typed_ir.L (canonize tl x)
    | Script_typed_ir.R xScript_typed_ir.R (canonize tr x)
    end
  | Script_typed_ir.Option_key t _, x
    match x with
    | NoneNone
    | Some xSome (canonize t x)
    end
  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_without_gadts.
  Reserved Notation "'apply".

  Fixpoint compare_comparable
    (t : Script_typed_ir.comparable_ty)
    (k : int)
    (x y : Script_typed_ir.Comparable_ty.to_Set t)
    {struct t}
    : int :=
    let apply := 'apply in
    match t, x, y with
    | Script_typed_ir.Unit_key _, _, _
      apply 0 k

    | Script_typed_ir.Never_key _, impossible, _
      apply 0 k

    | Script_typed_ir.Signature_key _, x, y
      apply (Signature.compare x y) k

    | Script_typed_ir.String_key _, x, y
      apply (Alpha_context.Script_string.compare x y) k

    | Script_typed_ir.Bool_key _, x, y
      apply (Compare.Bool.(Compare.S.compare) x y) k

    | Script_typed_ir.Mutez_key _, x, y
      apply (Alpha_context.Tez.compare x y) k

    | Script_typed_ir.Key_hash_key _, x, y
      apply
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) x y) k

    | Script_typed_ir.Key_key _, x, y
      apply (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.compare) x y) k

    | Script_typed_ir.Int_key _, x, y
      apply (Alpha_context.Script_int.compare x y) k

    | Script_typed_ir.Nat_key _, x, y
      apply (Alpha_context.Script_int.compare x y) k

    | Script_typed_ir.Timestamp_key _, x, y
      apply (Alpha_context.Script_timestamp.compare x y) k

    | Script_typed_ir.Address_key _, x, y
      apply (Script_comparable.compare_address x y) k

    | Script_typed_ir.Bytes_key _, x, y
      apply (Compare.Bytes.(Compare.S.compare) x y) k

    | Script_typed_ir.Chain_id_key _, x, y
      apply (Chain_id.compare x y) k

    | Script_typed_ir.Pair_key (tl, _) (tr, _) _, x, y
      let '(lx, rx) := x in
      let '(ly, ry) := y in
      compare_comparable tl (compare_comparable tr k rx ry) lx ly

    | Script_typed_ir.Union_key (tl, _) (tr, _) _, x, y
      match (x, y) with
      | (Script_typed_ir.L x, Script_typed_ir.L y)
        compare_comparable tl k x y
      | (Script_typed_ir.L _, Script_typed_ir.R _) ⇒ (-1)
      | (Script_typed_ir.R _, Script_typed_ir.L _) ⇒ 1
      | (Script_typed_ir.R x, Script_typed_ir.R y)
        compare_comparable tr k x y
      end

    | Script_typed_ir.Option_key t _, x, y
      match (x, y) with
      | (None, None)apply 0 k
      | (None, Some _) ⇒ (-1)
      | (Some _, None) ⇒ 1
      | (Some x, Some y)compare_comparable t k x y
      end
    end

  where "'apply" :=
    (fun (ret : int) (k : int) ⇒
      match ret with
      | 0 ⇒ k
      | ret
        if ret >i 0 then
          1
        else
          (-1)
      end).

  Definition apply := 'apply.

This definition is equivalent to the original one.
  Fixpoint compare_comparable_eq t k x y {struct t}
    : Script_comparable.Compare_comparable.compare_comparable t 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 t k_result x y.
    destruct t; simpl; repeat rewrite cast_eval; try easy;
      repeat match goal with
      | [p : Script_typed_ir.comparable_ty × _ |- _] ⇒ destruct p
      end;
      simpl in *;
      try match goal with
      | [_ : ?a × ?b |- _] ⇒ rewrite_cast_exists_eval_eq [a, b]
      | [_ : Script_typed_ir.union ?a ?b |- _] ⇒
        rewrite_cast_exists_eval_eq [a, b]
      | [_ : option ?a |- _] ⇒ rewrite_cast_exists_eval_eq a
      end;
      destruct x, y;
      now repeat rewrite compare_comparable_eq.
  Qed.

A lemma to unfold the use of the continuation.
  Fixpoint compare_comparable_continuation t t' k
    (x y : Script_typed_ir.Comparable_ty.to_Set t)
    (x' y' : Script_typed_ir.Comparable_ty.to_Set t') {struct t}
    : compare_comparable t (compare_comparable t' k x' y') x y =
      let res := compare_comparable t 0 x y in
      match res with
      | 0 ⇒ 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.
    repeat rewrite compare_comparable_continuation; simpl.
    match goal with
    | [|- match ?e with __ end = _] ⇒ now destruct e
    end.
  Qed.
End Compare_comparable_without_gadts.

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.Pre_valid.t (canonize t) (compare_comparable_without_gadts t).
  destruct t;
    try apply Signature.compare_is_pre_valid;
    try (
      try apply Compare.Valid.unit;
      try apply Script_typed_ir.Never.compare_is_valid;
      try apply Compare.Valid.int;
      try apply Compare.Valid.int64;
      try apply Compare.Valid.string;
      try apply Signature.Public_key_hash_compare_is_valid;
      try apply Signature.Public_key_compare_is_valid;
      try apply Chain_id.compare_is_valid;
      try apply Compare.Valid.bool;
      try apply compare_address_is_valid
    );
    repeat match goal with
    | [p : Script_typed_ir.comparable_ty × _ |- _] ⇒ destruct p
    end;
    try (
      apply Script_typed_ir.Union.compare_is_pre_valid;
      apply compare_comparable_without_gadts_is_pre_valid
    );
    try (
      apply Compare.Pre_valid.option;
      apply compare_comparable_without_gadts_is_pre_valid
    ).
  apply (Compare.Pre_valid.equality (compare1 :=
    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.
  }
  { now apply Compare.Pre_valid.lexicographic_compare. }
Qed.

Lemma compare_comparable_without_gadts_eq t x y
  : Script_comparable.compare_comparable t x y =
    compare_comparable_without_gadts t x y.
  apply Compare_comparable_without_gadts.compare_comparable_eq.
Qed.

We conclude that the original comparison function with GADTs is valid.