Skip to main content

🧾 Receipt_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.

Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.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.

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 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_rewardsSome tt
    | _None
    end in
  let proj_sc_rrp_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Sc_rollup_refutation_punishmentsSome tt
    | _None
    end in
  let proj_tx_rrr_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Tx_rollup_rejection_rewardsSome tt
    | _None
    end in
  let proj_tx_rrp_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Tx_rollup_rejection_punishmentsSome tt
    | _None
    end in
  let proj_fb (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Frozen_bonds c bSome (c, b)
    | _None
    end in
  let proj_minted_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.MintedSome tt
    | _None
    end in
  let proj_ic_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Initial_commitmentsSome tt
    | _None
    end in
  let proj_invoice_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.InvoiceSome tt
    | _None
    end in
  let proj_bootstrap_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.BootstrapSome tt
    | _None
    end in
  let proj_commitments (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Commitments xSome x
    | _None
    end in
  let proj_lbs_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Liquidity_baking_subsidiesSome tt
    | _None
    end in
  let proj_burned_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.BurnedSome tt
    | _None
    end in
  let proj_ler (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Lost_endorsing_rewards pkh p rSome (pkh, p, r)
    | _None
    end in
  let proj_dsp_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Double_signing_punishmentsSome tt
    | _None
    end in
  let proj_sf_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Storage_feesSome tt
    | _None
    end in
  let proj_bb_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Baking_bonusesSome tt
    | _None
    end in
  let proj_br_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Baking_rewardsSome tt
    | _None
    end in
  let proj_er_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Endorsing_rewardsSome tt
    | _None
    end in
  let proj_dser_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Double_signing_evidence_rewardsSome tt
    | _None
    end in
  let proj_nrr_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Nonce_revelation_rewardsSome tt
    | _None
    end in
  let proj_deposits (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Deposits xSome x
    | _None
    end in
  let proj_bf_u (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Block_feesSome tt
    | _None
    end in
  let proj_contract (b : Receipt_repr.balance) :=
    match b with
    | Receipt_repr.Contract xSome 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.tTrue)
    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].
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.

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.

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.

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.