🧾 Receipt_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Lemma balance_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Receipt_repr.balance_encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve balance_encoding_is_valid : Data_encoding_db.
Lemma is_not_zero_false : Receipt_repr.is_not_zero 0 = false.
reflexivity.
Qed.
Lemma is_not_zero_true : ∀ x, x ≠ 0 → Receipt_repr.is_not_zero x = true.
intro x; destruct x; easy.
Qed.
Module balance_update.
Module Valid.
Definition t (b : Receipt_repr.balance_update) : Prop :=
match b with
| Receipt_repr.Debited (Tez_repr.Tez_tag tz) ⇒ 0 < tz ≤ Int64.max_int
| Receipt_repr.Credited (Tez_repr.Tez_tag tz) ⇒ 0 ≤ tz ≤ Int64.max_int
end.
End Valid.
End balance_update.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Lemma balance_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Receipt_repr.balance_encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve balance_encoding_is_valid : Data_encoding_db.
Lemma is_not_zero_false : Receipt_repr.is_not_zero 0 = false.
reflexivity.
Qed.
Lemma is_not_zero_true : ∀ x, x ≠ 0 → Receipt_repr.is_not_zero x = true.
intro x; destruct x; easy.
Qed.
Module balance_update.
Module Valid.
Definition t (b : Receipt_repr.balance_update) : Prop :=
match b with
| Receipt_repr.Debited (Tez_repr.Tez_tag tz) ⇒ 0 < tz ≤ Int64.max_int
| Receipt_repr.Credited (Tez_repr.Tez_tag tz) ⇒ 0 ≤ tz ≤ Int64.max_int
end.
End Valid.
End balance_update.
The function [balance_update_encoding] is valid.
Lemma balance_update_encoding_is_valid :
Data_encoding.Valid.t balance_update.Valid.t Receipt_repr.balance_update_encoding.
Data_encoding.Valid.data_encoding_auto.
intros x H; simpl in *; split; trivial; unfold Json.wrap_error.
{ destruct x; simpl in *; autounfold with tezos_z in *;
destruct t; lia. }
{ destruct x, t; destruct H; autounfold with tezos_z in *;
unfold normalize_int64, two_pow_63, two_pow_64; simpl;
repeat match goal with
| |- context[if ?e then _ else _] ⇒ destruct e eqn:?
end;
hauto lq: on rew: off solve: lia.
}
Qed.
#[global] Hint Resolve balance_update_encoding_is_valid : Data_encoding_db.
Definition cuo_index (o_value : Receipt_repr.update_origin) : int :=
match o_value with
| Receipt_repr.Block_application ⇒ 0
| Receipt_repr.Protocol_migration ⇒ 1
| Receipt_repr.Subsidy ⇒ 2
| Receipt_repr.Simulation ⇒ 3
end.
Lemma compare_update_origin_is_valid :
Compare.Valid.t (fun _ ⇒ True) cuo_index Receipt_repr.compare_update_origin.
Proof.
apply (Compare.projection_is_valid cuo_index Compare.z_is_valid).
Qed.
#[global] Hint Resolve compare_update_origin_is_valid : Compare_db.
Lemma update_origin_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Receipt_repr.update_origin_encoding.
Data_encoding.Valid.data_encoding_auto;
intro x; destruct x; trivial; tauto.
Qed.
#[global] Hint Resolve update_origin_encoding_is_valid : Data_encoding_db.
Module balance_updates.
Module Valid.
Definition t (x : Receipt_repr.balance_updates) : Prop :=
List.Forall
(fun '(_, balance_update, _) ⇒ balance_update.Valid.t balance_update)
x.
End Valid.
End balance_updates.
Lemma balance_updates_encoding_is_valid :
Data_encoding.Valid.t
balance_updates.Valid.t
Receipt_repr.balance_updates_encoding.
Data_encoding.Valid.data_encoding_auto.
apply List.Forall_impl.
hauto l: on.
Qed.
#[global] Hint Resolve balance_updates_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t balance_update.Valid.t Receipt_repr.balance_update_encoding.
Data_encoding.Valid.data_encoding_auto.
intros x H; simpl in *; split; trivial; unfold Json.wrap_error.
{ destruct x; simpl in *; autounfold with tezos_z in *;
destruct t; lia. }
{ destruct x, t; destruct H; autounfold with tezos_z in *;
unfold normalize_int64, two_pow_63, two_pow_64; simpl;
repeat match goal with
| |- context[if ?e then _ else _] ⇒ destruct e eqn:?
end;
hauto lq: on rew: off solve: lia.
}
Qed.
#[global] Hint Resolve balance_update_encoding_is_valid : Data_encoding_db.
Definition cuo_index (o_value : Receipt_repr.update_origin) : int :=
match o_value with
| Receipt_repr.Block_application ⇒ 0
| Receipt_repr.Protocol_migration ⇒ 1
| Receipt_repr.Subsidy ⇒ 2
| Receipt_repr.Simulation ⇒ 3
end.
Lemma compare_update_origin_is_valid :
Compare.Valid.t (fun _ ⇒ True) cuo_index Receipt_repr.compare_update_origin.
Proof.
apply (Compare.projection_is_valid cuo_index Compare.z_is_valid).
Qed.
#[global] Hint Resolve compare_update_origin_is_valid : Compare_db.
Lemma update_origin_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Receipt_repr.update_origin_encoding.
Data_encoding.Valid.data_encoding_auto;
intro x; destruct x; trivial; tauto.
Qed.
#[global] Hint Resolve update_origin_encoding_is_valid : Data_encoding_db.
Module balance_updates.
Module Valid.
Definition t (x : Receipt_repr.balance_updates) : Prop :=
List.Forall
(fun '(_, balance_update, _) ⇒ balance_update.Valid.t balance_update)
x.
End Valid.
End balance_updates.
Lemma balance_updates_encoding_is_valid :
Data_encoding.Valid.t
balance_updates.Valid.t
Receipt_repr.balance_updates_encoding.
Data_encoding.Valid.data_encoding_auto.
apply List.Forall_impl.
hauto l: on.
Qed.
#[global] Hint Resolve balance_updates_encoding_is_valid : Data_encoding_db.
Compare [option] of [unit].
1 for [(None, Some tt)]
1 for [(Some tt, None)]
0 for other cases
We need this mostly for definition of [compare_balance_lgo].
A proof that [compare_opt_u] is valid.
Auxillary lemma in order to prove [compare_balance_lgo_is_valid].
Lemma compare_opt_u_is_valid_aux :
Compare.Valid.t (fun _ ⇒ True) id compare_opt_u.
Proof.
Compare.valid_auto.
sauto lq: on.
Qed.
#[local] Hint Resolve compare_opt_u_is_valid_aux : Compare_db.
Compare.Valid.t (fun _ ⇒ True) id compare_opt_u.
Proof.
Compare.valid_auto.
sauto lq: on.
Qed.
#[local] Hint Resolve compare_opt_u_is_valid_aux : Compare_db.
Compare balance in lexicographic order.
We need this definition in order to prove [compare_balance_is_valid].
The idea of the definition is to create a tuple of 22 optional values for
each argument, i.e. [(None, None, Some x, ..., None)]. And then compare
these 2 tuples from left to right using [Compare.Option.compare] with
appropriate comparison function (so, we will have something like
None vs Some x = -1, Some x vs None = 1, Some x vs Some y = compare x y..).
To implement this idea we use [Compare.projection] and
[Compare.lexicographic].
Auxillary definition in order to prove [compare_balance_lgo_is_valid].
(* TODO: update *)
Definition compare_balance_lgo (b1 b2 : Receipt_repr.balance) : int :=
let proj_sc_rrr_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Sc_rollup_refutation_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_sc_rrp_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Sc_rollup_refutation_punishments ⇒ Some tt
| _ ⇒ None
end in
let proj_tx_rrr_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Tx_rollup_rejection_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_tx_rrp_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Tx_rollup_rejection_punishments ⇒ Some tt
| _ ⇒ None
end in
let proj_fb (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Frozen_bonds c b ⇒ Some (c, b)
| _ ⇒ None
end in
let proj_minted_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Minted ⇒ Some tt
| _ ⇒ None
end in
let proj_ic_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Initial_commitments ⇒ Some tt
| _ ⇒ None
end in
let proj_invoice_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Invoice ⇒ Some tt
| _ ⇒ None
end in
let proj_bootstrap_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Bootstrap ⇒ Some tt
| _ ⇒ None
end in
let proj_commitments (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Commitments x ⇒ Some x
| _ ⇒ None
end in
let proj_lbs_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Liquidity_baking_subsidies ⇒ Some tt
| _ ⇒ None
end in
let proj_burned_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Burned ⇒ Some tt
| _ ⇒ None
end in
let proj_ler (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Lost_endorsing_rewards pkh p r ⇒ Some (pkh, p, r)
| _ ⇒ None
end in
let proj_dsp_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Double_signing_punishments ⇒ Some tt
| _ ⇒ None
end in
let proj_sf_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Storage_fees ⇒ Some tt
| _ ⇒ None
end in
let proj_bb_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Baking_bonuses ⇒ Some tt
| _ ⇒ None
end in
let proj_br_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Baking_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_er_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Endorsing_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_dser_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Double_signing_evidence_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_nrr_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Nonce_revelation_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_deposits (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Deposits x ⇒ Some x
| _ ⇒ None
end in
let proj_bf_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Block_fees ⇒ Some tt
| _ ⇒ None
end in
let proj_contract (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Contract x ⇒ Some x
| _ ⇒ None
end in
let proj b :=
(proj_sc_rrr_u b (* 23 *), proj_sc_rrp_u b (* 22 *),
proj_tx_rrr_u b (* 21 *), proj_tx_rrp_u b, proj_fb b, proj_minted_u b,
proj_ic_u b (* 17 *), proj_invoice_u b (* 16 *), proj_bootstrap_u b,
proj_commitments b, proj_burned_u b, proj_lbs_u b (* 12 *),
proj_ler b (* 11 *), proj_dsp_u b, proj_sf_u b, proj_bb_u b,
proj_br_u b (* 7 *), proj_er_u b (* 6 *), proj_dser_u b, proj_nrr_u b,
proj_deposits b, proj_bf_u b (* 2 *), proj_contract b (* 1 *))
in
Compare.projection
proj
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
compare_opt_u (* 23 *)
compare_opt_u) (* 22 *)
compare_opt_u) (* 21 *)
compare_opt_u)
(Compare.Option.compare
(fun '(ca, ra) '(cb, rb) ⇒
let c_value := Contract_repr.compare ca cb in
if Receipt_repr.is_not_zero c_value
then c_value
else Bond_id_repr.compare ra rb)))
compare_opt_u)
compare_opt_u) (* 17 *)
compare_opt_u) (* 16 *)
compare_opt_u)
(Compare.Option.compare Blinded_public_key_hash.compare))
compare_opt_u)
compare_opt_u) (* 12 *)
(Option.compare (fun '(pkha, pa, ra) '(pkhb, pb, rb) ⇒
let c_value :=
Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb in
if Receipt_repr.is_not_zero c_value
then c_value
else
let c_value0 := Bool.(Compare.S.compare) pa pb in
if Receipt_repr.is_not_zero c_value0
then c_value0
else Bool.(Compare.S.compare) ra rb))) (* 11 *)
compare_opt_u)
compare_opt_u)
compare_opt_u)
compare_opt_u) (* 7 *)
compare_opt_u) (* 6 *)
compare_opt_u)
compare_opt_u)
(Option.compare Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare)))
compare_opt_u) (* 2 *)
(Compare.Option.compare Contract_repr.compare)) (* 1 *)
b1 b2.
Definition compare_balance_lgo (b1 b2 : Receipt_repr.balance) : int :=
let proj_sc_rrr_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Sc_rollup_refutation_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_sc_rrp_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Sc_rollup_refutation_punishments ⇒ Some tt
| _ ⇒ None
end in
let proj_tx_rrr_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Tx_rollup_rejection_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_tx_rrp_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Tx_rollup_rejection_punishments ⇒ Some tt
| _ ⇒ None
end in
let proj_fb (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Frozen_bonds c b ⇒ Some (c, b)
| _ ⇒ None
end in
let proj_minted_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Minted ⇒ Some tt
| _ ⇒ None
end in
let proj_ic_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Initial_commitments ⇒ Some tt
| _ ⇒ None
end in
let proj_invoice_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Invoice ⇒ Some tt
| _ ⇒ None
end in
let proj_bootstrap_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Bootstrap ⇒ Some tt
| _ ⇒ None
end in
let proj_commitments (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Commitments x ⇒ Some x
| _ ⇒ None
end in
let proj_lbs_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Liquidity_baking_subsidies ⇒ Some tt
| _ ⇒ None
end in
let proj_burned_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Burned ⇒ Some tt
| _ ⇒ None
end in
let proj_ler (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Lost_endorsing_rewards pkh p r ⇒ Some (pkh, p, r)
| _ ⇒ None
end in
let proj_dsp_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Double_signing_punishments ⇒ Some tt
| _ ⇒ None
end in
let proj_sf_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Storage_fees ⇒ Some tt
| _ ⇒ None
end in
let proj_bb_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Baking_bonuses ⇒ Some tt
| _ ⇒ None
end in
let proj_br_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Baking_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_er_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Endorsing_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_dser_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Double_signing_evidence_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_nrr_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Nonce_revelation_rewards ⇒ Some tt
| _ ⇒ None
end in
let proj_deposits (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Deposits x ⇒ Some x
| _ ⇒ None
end in
let proj_bf_u (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Block_fees ⇒ Some tt
| _ ⇒ None
end in
let proj_contract (b : Receipt_repr.balance) :=
match b with
| Receipt_repr.Contract x ⇒ Some x
| _ ⇒ None
end in
let proj b :=
(proj_sc_rrr_u b (* 23 *), proj_sc_rrp_u b (* 22 *),
proj_tx_rrr_u b (* 21 *), proj_tx_rrp_u b, proj_fb b, proj_minted_u b,
proj_ic_u b (* 17 *), proj_invoice_u b (* 16 *), proj_bootstrap_u b,
proj_commitments b, proj_burned_u b, proj_lbs_u b (* 12 *),
proj_ler b (* 11 *), proj_dsp_u b, proj_sf_u b, proj_bb_u b,
proj_br_u b (* 7 *), proj_er_u b (* 6 *), proj_dser_u b, proj_nrr_u b,
proj_deposits b, proj_bf_u b (* 2 *), proj_contract b (* 1 *))
in
Compare.projection
proj
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
(Compare.lexicographic
compare_opt_u (* 23 *)
compare_opt_u) (* 22 *)
compare_opt_u) (* 21 *)
compare_opt_u)
(Compare.Option.compare
(fun '(ca, ra) '(cb, rb) ⇒
let c_value := Contract_repr.compare ca cb in
if Receipt_repr.is_not_zero c_value
then c_value
else Bond_id_repr.compare ra rb)))
compare_opt_u)
compare_opt_u) (* 17 *)
compare_opt_u) (* 16 *)
compare_opt_u)
(Compare.Option.compare Blinded_public_key_hash.compare))
compare_opt_u)
compare_opt_u) (* 12 *)
(Option.compare (fun '(pkha, pa, ra) '(pkhb, pb, rb) ⇒
let c_value :=
Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb in
if Receipt_repr.is_not_zero c_value
then c_value
else
let c_value0 := Bool.(Compare.S.compare) pa pb in
if Receipt_repr.is_not_zero c_value0
then c_value0
else Bool.(Compare.S.compare) ra rb))) (* 11 *)
compare_opt_u)
compare_opt_u)
compare_opt_u)
compare_opt_u) (* 7 *)
compare_opt_u) (* 6 *)
compare_opt_u)
compare_opt_u)
(Option.compare Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare)))
compare_opt_u) (* 2 *)
(Compare.Option.compare Contract_repr.compare)) (* 1 *)
b1 b2.
A proof that the compare function taken from the definition of
[compare_balance_lgo] above is valid.
Auxillary lemma in order to prove [compare_balance_lgo_is_valid].
The idea is to show that given compare function definition equals to
[Compare.lexicographic Contract_repr.compare Bond_id_repr.compare], which
in order can be easily proved by using [Compare.lexicographic_is_valid].
Lemma compare_contract_bond_id_is_valid_aux :
Compare.Valid.t
(fun _ : Contract_repr.t × Bond_id_repr.t ⇒ True)
id
(fun '(ca, ra) '(cb, rb) ⇒
let c_value := Contract_repr.compare ca cb in
if Receipt_repr.is_not_zero c_value
then c_value
else Bond_id_repr.compare ra rb).
Proof.
eapply Compare.equality
with (compare1 :=
(Compare.lexicographic Contract_repr.compare Bond_id_repr.compare)).
intros [] [] _ _; simpl in *; step; simpl; reflexivity.
Compare.valid_auto.
Qed.
#[local] Hint Resolve compare_contract_bond_id_is_valid_aux : Compare_db.
Compare.Valid.t
(fun _ : Contract_repr.t × Bond_id_repr.t ⇒ True)
id
(fun '(ca, ra) '(cb, rb) ⇒
let c_value := Contract_repr.compare ca cb in
if Receipt_repr.is_not_zero c_value
then c_value
else Bond_id_repr.compare ra rb).
Proof.
eapply Compare.equality
with (compare1 :=
(Compare.lexicographic Contract_repr.compare Bond_id_repr.compare)).
intros [] [] _ _; simpl in *; step; simpl; reflexivity.
Compare.valid_auto.
Qed.
#[local] Hint Resolve compare_contract_bond_id_is_valid_aux : Compare_db.
Definition of compare function which equals to definition which can be
found in [compare_balance_lgo] using lexicographic order.
Auxillary definition in order to prove [compare_balance_lgo_is_valid].
Definition compare_pkh_b_b_lgo :=
Compare.lexicographic
(@Compare.lexicographic public_key_hash _
Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare)
Bool.(Compare.S.compare))
Bool.(Compare.S.compare).
Compare.lexicographic
(@Compare.lexicographic public_key_hash _
Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare)
Bool.(Compare.S.compare))
Bool.(Compare.S.compare).
A proof that [compare_pkh_b_b_lgo] function defined above is valid.
Auxillary lemma in order to prove
[compare_public_key_hash_bool_bool_is_valid_aux].
Lemma compare_pkh_b_b_lgo_is_valid_aux :
Compare.Valid.t (fun _ ⇒ True) id compare_pkh_b_b_lgo.
Proof.
Compare.valid_auto.
Qed.
#[local] Hint Resolve compare_pkh_b_b_lgo_is_valid_aux : Compare_db.
Compare.Valid.t (fun _ ⇒ True) id compare_pkh_b_b_lgo.
Proof.
Compare.valid_auto.
Qed.
#[local] Hint Resolve compare_pkh_b_b_lgo_is_valid_aux : Compare_db.
A proof that the compare function taken from the definition of
[compare_balance_lgo] above is valid.
Auxillary lemma in order to prove [compare_balance_lgo_is_valid].
The idea is to show that given compare function definition equals to
[compare_pkh_b_b_lgo], which in order can be easily proved by
using [Compare.lexicographic_is_valid].
Lemma compare_public_key_hash_bool_bool_is_valid_aux :
Compare.Valid.t (fun _ ⇒ True) id
(fun '(pkha, pa, ra) '(pkhb, pb, rb) ⇒
let c_value := Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb in
if Receipt_repr.is_not_zero c_value
then c_value
else
let c_value0 := Bool.(Compare.S.compare) pa pb in
if Receipt_repr.is_not_zero c_value0 then c_value0 else Bool.(Compare.S.compare) ra rb).
Proof.
eapply Compare.equality with (compare1 := compare_pkh_b_b_lgo).
intros [[]] [[]] _ _; simpl.
repeat (step; simpl); reflexivity.
apply compare_pkh_b_b_lgo_is_valid_aux.
Qed.
#[local] Hint Resolve compare_public_key_hash_bool_bool_is_valid_aux : Compare_db.
Compare.Valid.t (fun _ ⇒ True) id
(fun '(pkha, pa, ra) '(pkhb, pb, rb) ⇒
let c_value := Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb in
if Receipt_repr.is_not_zero c_value
then c_value
else
let c_value0 := Bool.(Compare.S.compare) pa pb in
if Receipt_repr.is_not_zero c_value0 then c_value0 else Bool.(Compare.S.compare) ra rb).
Proof.
eapply Compare.equality with (compare1 := compare_pkh_b_b_lgo).
intros [[]] [[]] _ _; simpl.
repeat (step; simpl); reflexivity.
apply compare_pkh_b_b_lgo_is_valid_aux.
Qed.
#[local] Hint Resolve compare_public_key_hash_bool_bool_is_valid_aux : Compare_db.
A proof that [compare_balance_lgo] is valid.
Auxillary lemma in order to prove [compare_balance_is_valid].
[compare_balance_lgo] is essensially the composition of lexicographic
comparisons (and also comparisons which are proved to be equal to
the lexicographic). So, we mainly use the
[Compare.lexicographic_is_valid] to prove the validity, and then
appropriate lemmas proved ealier (including auxillary lemmas above).
Lemma compare_balance_lgo_is_valid_aux :
Compare.Valid.t (fun _ ⇒ True) id compare_balance_lgo.
Proof.
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
repeat eapply Compare.lexicographic_is_valid;
try apply compare_opt_u_is_valid_aux;
eapply Compare.option_is_valid.
{ apply compare_contract_bond_id_is_valid_aux. }
{ apply Blinded_public_key_hash.compare_is_valid. }
{ apply compare_public_key_hash_bool_bool_is_valid_aux. }
{ apply Signature.Public_key_hash_compare_is_valid. }
{ apply Contract_repr.compare_is_valid. }
}
intros []; repeat split; trivial.
cbv delta [id]; intros x1 x2 _ _; split; intros H;
destruct x1, x2; try discriminate H; try reflexivity.
all :
qauto.
Qed.
#[local] Hint Resolve compare_balance_lgo_is_valid_aux : Compare_db.
Compare.Valid.t (fun _ ⇒ True) id compare_balance_lgo.
Proof.
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
repeat eapply Compare.lexicographic_is_valid;
try apply compare_opt_u_is_valid_aux;
eapply Compare.option_is_valid.
{ apply compare_contract_bond_id_is_valid_aux. }
{ apply Blinded_public_key_hash.compare_is_valid. }
{ apply compare_public_key_hash_bool_bool_is_valid_aux. }
{ apply Signature.Public_key_hash_compare_is_valid. }
{ apply Contract_repr.compare_is_valid. }
}
intros []; repeat split; trivial.
cbv delta [id]; intros x1 x2 _ _; split; intros H;
destruct x1, x2; try discriminate H; try reflexivity.
all :
qauto.
Qed.
#[local] Hint Resolve compare_balance_lgo_is_valid_aux : Compare_db.
Validity of [Receipt_repr.compare_balance] comparison function.
The idea of proof is to
1) create equal definition using [Compare.lexicographic] (the equal
definition [compare_balance_lgo] can be found above).
2) prove that equal definition is valid (lemma
[compare_balance_lgo_is_valid] above).
3) prove the equality (using [Compare.equality] and
[Compare.lexicographic_option_right_neutral].
Lemma compare_balance_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Receipt_repr.compare_balance.
Proof.
apply Compare.equality with (compare1 := compare_balance_lgo).
intros [] [] _ _; try reflexivity;
unfold compare_balance_lgo, Compare.projection, compare_opt_u;
repeat rewrite Compare.lexicographic_option_right_neutral; reflexivity.
apply compare_balance_lgo_is_valid_aux.
Qed.
#[global] Hint Resolve compare_balance_is_valid : Compare_db.
Compare.Valid.t (fun _ ⇒ True) id Receipt_repr.compare_balance.
Proof.
apply Compare.equality with (compare1 := compare_balance_lgo).
intros [] [] _ _; try reflexivity;
unfold compare_balance_lgo, Compare.projection, compare_opt_u;
repeat rewrite Compare.lexicographic_option_right_neutral; reflexivity.
apply compare_balance_lgo_is_valid_aux.
Qed.
#[global] Hint Resolve compare_balance_is_valid : Compare_db.