Skip to main content

🍬 Script_comparable.v

Proofs

See code, Gitlab , OCaml

[compare_address] 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.
    { eapply 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.

The canonical form of a Michelson comparable value. This function is the identity except for the signatures. In this case, we need to define a canonical form as signatures can be represented in various, but equivalent, ways.
Fixpoint canonize (t : Ty.t)
  (x : Ty.to_Set t)
  : Ty.to_Set t :=
  match t, x with
  | Ty.Unit, xx
  | Ty.Num _, xx
  | Ty.Signature, x
    let signature := Script_typed_ir.Script_signature.get x in
    Script_typed_ir.Script_signature.make (Signature.canonize signature)
  | Ty.String, xx
  | Ty.Bytes, xx
  | Ty.Mutez, xx
  | Ty.Key_hash, xx
  | Ty.Key, xx
  | Ty.Timestamp, xx
  | Ty.Address, xx
  | Ty.Tx_rollup_l2_address, xx
  | Ty.Bool, xx
  | Ty.Pair tl tr, (l, r)
    (canonize tl l, canonize tr r)
  | Ty.Union 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
  | Ty.Lambda _ _ , xx
  | Ty.Option t, x
    match x with
    | NoneNone
    | Some xSome (canonize t x)
    end
  | Ty.List _, xx
  | Ty.Set_ _, xx
  | Ty.Map _ _, xx
  | Ty.Big_map _ _, xx
  | Ty.Contract _, xx
  | Ty.Sapling_transaction, xx
  | Ty.Sapling_transaction_deprecated, xx
  | Ty.Sapling_state, xx
  | Ty.Operation, xx
  | Ty.Chain_id, xx
  | Ty.Never, xx
  | Ty.Bls12_381_g1, xx
  | Ty.Bls12_381_g2, xx
  | Ty.Bls12_381_fr, xx
  | Ty.Ticket _, xx
  | Ty.Chest_key, xx
  | Ty.Chest, xx
  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.
A lemma to unfold the use of the continuation. @TODO 22.November.2022 not sure if this fixpoint should be kept in new version of Michelson's verification 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. Proof. destruct t; simpl; trivial; destruct x, y; trivial; try (now step). repeat rewrite compare_comparable_continuation; simpl. hauto lq: on. Qed.
The comparison [dep_compare_comparable] 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. @TODO 22.November.2022 - this Fixpoint should be redefined according to new version of Michelson verification.
Fixpoint dep_compare_comparable_is_valid {t : Ty.t} : Script_family.Ty.is_Comparable t -> Compare.Valid.t (fun x => match With_family.of_value x with | Some x => Script_typed_ir.With_family.Valid.value x | None => False end ) (canonize t) (dep_compare_comparable t). Proof. intros H_t. destruct t; try destruct H_t; try apply Compare.wrap_compare_is_valid. { apply Compare.unit_is_valid. } { destruct_all Ty.Num.t. { apply Script_int.compare_is_valid. } { eapply Compare.implies. { apply Script_int.compare_is_valid. } all: hauto l: on. } } { apply Script_typed_ir.Script_signature.compare_is_valid. } { apply Script_string.compare_is_valid. } { apply Compare.string_is_valid. } { eapply Compare.implies. { apply Tez_repr.compare_is_valid. } all: hauto l: on. } { apply Signature.Public_key_hash_compare_is_valid. } { apply Signature.Public_key_compare_is_valid. } { apply Script_timestamp.compare_is_valid. } { apply compare_address_is_valid. } { eapply Compare.implies. { apply compare_tx_rollup_l2_address_is_valid. } all: hauto l: on. } { apply Compare.bool_is_valid. } { unfold dep_compare_comparable; simpl. eapply Compare.equality with (compare1 := Compare.lexicographic _ _ ). { intros [x1 x2] [y1 y2] ? ?. rewrite Compare_comparable.compare_comparable_continuation. reflexivity. } eapply Compare.implies. { eapply Compare.lexicographic_is_valid; apply dep_compare_comparable_is_valid; assumption. } all: sauto. } { eapply Compare.implies. { eapply Script_typed_ir.Union.compare_is_valid; fold @Ty.to_Set_aux @Ty.to_Set; apply dep_compare_comparable_is_valid; assumption. } all: hauto l: on. } { eapply Compare.implies. { eapply Compare.option_is_valid; apply dep_compare_comparable_is_valid; assumption. } all: hauto l: on. } { apply Script_typed_ir.Script_chain_id.compare_is_valid. } { easy. } Qed.