🍬 Script_comparable.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_comparable.
Require TezosOfOCaml.Environment.V8.Proofs.Chain_id.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_int.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_string.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_family.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
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_family.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_comparable.
Require TezosOfOCaml.Environment.V8.Proofs.Chain_id.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_int.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_string.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_family.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
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_family.
[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.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.
: 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, 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.
(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.
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.
Lemma compare_comparable_is_valid {a aty} :
Script_typed_ir.ty.Valid.proj_rel a aty →
Compare.Valid.t (a := Ty.to_Set a) (fun _ ⇒ True) id (Script_comparable.compare_comparable aty).
Proof. Admitted.