Script_comparable.v

Source: src/Proto_alpha/Proofs/Script_comparable.v

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.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.

This comparison function is valid.

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.

Lemma compare_comparable_is_pre_valid t
  : Compare.Pre_valid.t (a := Script_typed_ir.Comparable_ty.to_Set t)
    (canonize t) (Script_comparable.compare_comparable t).
  apply (Compare.Pre_valid.equality (compare1 :=
    compare_comparable_without_gadts t
  )).
  { intros; now rewrite compare_comparable_without_gadts_eq. }
  { apply compare_comparable_without_gadts_is_pre_valid. }
Qed.