Skip to main content

🪙 Tez_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Tez_repr.

Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Int64.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Utils.

Module Repr.
  Module Valid.
    Definition t (tz : Tez_repr.repr) :=
      0 tz Int64.max_int.
    #[global] Hint Unfold t : tezos_z.
  End Valid.
End Repr.

Module Valid.
  Definition t (tz : Tez_repr.t) :=
    let 'Tez_repr.Tez_tag repr := tz in
    Repr.Valid.t repr.
  #[global] Hint Unfold t : tezos_z.
End Valid.

#[global] Hint Unfold
     Tez_repr.op_minusquestion
     Tez_repr.op_plusquestion
     Tez_repr.op_starquestion
     Tez_repr.op_divquestion
     Tez_repr.sub_opt
     Tez_repr.of_mutez
     Tez_repr.to_mutez
     Tez_repr.op_lteq
     Tez_repr.op_lt
     Tez_repr.op_eq
     Tez_repr.op_gt
     Tez_repr.of_string
  : tezos_z.

Lemma op_minusquestion_is_valid : {t1 t2 : Tez_repr.t},
    Valid.t t1
    Valid.t t2
    let 'Tez_repr.Tez_tag t1' := t1 in
    let 'Tez_repr.Tez_tag t2' := t2 in
    match Tez_repr.op_minusquestion t1 t2 with
    | Pervasives.Ok t
        let 'Tez_repr.Tez_tag t' := t in
        t1' t2' Valid.t t t' = t1' - t2'
    | Pervasives.Error _t1' < t2'
    end.
Proof.
  intros; unfold Tez_repr.op_minusquestion.
  destruct_all Tez_repr.t.
  destruct (_ i64 _) eqn:?; simpl; lia.
Qed.

Tez_repr.op_minusquestion equals to subtraction in Z
Lemma op_minusquestion_eq : t1 t2,
  Valid.t (Tez_repr.Tez_tag t1)
  Valid.t (Tez_repr.Tez_tag t2)
  match
    Tez_repr.op_minusquestion (Tez_repr.Tez_tag t1) (Tez_repr.Tez_tag t2)
  with
  | Pervasives.Ok (Tez_repr.Tez_tag t) ⇒ t = t1 - t2
  | Pervasives.Error _True
  end.
Proof.
  intros.
  unfold Tez_repr.op_minusquestion.
  destruct (_ i64 _) eqn:?; simpl; trivial.
  lia.
Qed.

Lemma sub_opt_is_valid : {t1 t2 : Tez_repr.t},
    Valid.t t1
    Valid.t t2
    let 'Tez_repr.Tez_tag t1' := t1 in
    let 'Tez_repr.Tez_tag t2' := t2 in
    match Tez_repr.sub_opt t1 t2 with
    | Some t
      let 'Tez_repr.Tez_tag t' := t in
      t1' t2' Valid.t t t' = t1' - t2'
    | Nonet1' < t2'
    end.
Proof.
  intros; unfold Tez_repr.sub_opt.
  destruct_all Tez_repr.t.
  destruct (_ i64 _) eqn:?; simpl; lia.
Qed.

Tez_repr.sub_opt equals to subtraction in Z
Lemma sub_opt_eq : t t1 t2,
    Valid.t (Tez_repr.Tez_tag t1)
    Valid.t (Tez_repr.Tez_tag t2)
    Tez_repr.sub_opt
      (Tez_repr.Tez_tag t1)
      (Tez_repr.Tez_tag t2) = Some (Tez_repr.Tez_tag t)
    t = t1 - t2.
Proof.
  Utils.tezos_z_autounfold. unfold "return?". simpl.
  intros t t1 t2 H1 H2.
  destruct (_ <=? _) eqn:H_le; [hauto l: on drew: off|sauto q: on].
Qed.

Lemma op_plusquestion_is_valid : {t1 t2 : Tez_repr.t},
    Valid.t t1
    Valid.t t2
    let 'Tez_repr.Tez_tag t1' := t1 in
    let 'Tez_repr.Tez_tag t2' := t2 in
    match Tez_repr.op_plusquestion t1 t2 with
    | Pervasives.Ok tValid.t t
    | Pervasives.Error _t1' + t2' > Int64.max_int
    end.
Proof.
  intros; unfold Tez_repr.op_plusquestion.
  destruct_all Tez_repr.t.
  destruct (_ <i64 _) eqn:?; simpl; lia.
Qed.

Tez_repr.op_plusquestion equals to addition in Z
Lemma op_plusquestion_eq : t t1 t2,
  Valid.t (Tez_repr.Tez_tag t1)
  Valid.t (Tez_repr.Tez_tag t2)
  Tez_repr.op_plusquestion
    (Tez_repr.Tez_tag t1)
    (Tez_repr.Tez_tag t2) = return? (Tez_repr.Tez_tag t)
  t = t1 +Z t2.
Proof.
  Utils.tezos_z_autounfold. simpl.
  intros t t1 t2 H1 H2.
  destruct (_ <? _) eqn:H_lt; hfcrush.
Qed.

Lemma mul_pos_is_valid : {t1 t2 : Z.t},
    Int64.Valid.non_negative t1
    Int64.Valid.positive t2
    t1 Int64.max_int / t2 Int64.Valid.t (t1 × t2)%Z.
  intros t1 t2 [Ht11 Ht12] [Ht21 Ht22] H__t1t3;
    unfold Int64.Valid.t, min_int; split; [lia|];
    replace (t1 × t2)%Z with (t2 × t1)%Z by lia;
    replace max_int with (max_int × 1)%Z by lia;
    replace 1 with (t2 / t2) by (apply Z_div_same; lia).
    assert(t2 × t1 t2 × (max_int / t2))
      by (apply Zmult_le_compat_l; [assumption|lia]).
    assert(t2 × (max_int / t2) max_int × (t2 / t2))
      by (
          replace (max_int × (t2 / t2))%Z
            with (max_int × t2 / t2)%Z
            by (rewrite Z_div_mult, Z_div_same; lia);
          replace (max_int × t2)%Z
            with (t2 × max_int)%Z by lia;
          apply Zdiv_mult_le; lia
        ); lia.
Qed.

Lemma op_starquestion_is_valid : {t1 t2 : Tez_repr.t},
    Valid.t t1
    Valid.t t2
    let 'Tez_repr.Tez_tag t1' := t1 in
    let 'Tez_repr.Tez_tag t2' := t2 in
    (t2' = 0
    Tez_repr.op_starquestion t1 t2' = Pervasives.Ok (Tez_repr.Tez_tag 0)
    Valid.t (Tez_repr.Tez_tag 0))
    (t2' 0
     match Tez_repr.op_starquestion t1 t2' with
     | Pervasives.Ok tValid.t t t1' (Int64.max_int / t2')
     | Pervasives.Error _t1' > Int64.max_int / t2'
     end).
Proof.
  autounfold with tezos_z; simpl; intros t1 t2 Ht11 Ht12;
    destruct t1 as [t1];
    destruct t2 as [t2];
    destruct (Z.eq_decidable t2 0).
  - left; split; [assumption|]; split; [|lia];
    destruct (Z.ltb_spec0 t2 0); [lia|];
    destruct (Z.eqb_spec t2 0); [reflexivity|lia].
  - right; split; [assumption|];
    destruct (Z.ltb_spec0 t2 0); simpl; repeat split; simpl in *; [lia|];
    destruct (Z.compare_spec t2 0); [subst;rewrite Z.eqb_refl; split|..];
    [lia..|]; destruct (Z.eqb_spec t2 0); simpl; [split; lia|].
    autounfold with tezos_z; remember
       ((9223372036854775807 / t2 + 9223372036854775808) mod
         18446744073709551616 - 9223372036854775808) as t3.

    (* hypothesis name includes t3 due to equality below *)
    assert(Hv_t3 : Int64.Valid.t (9223372036854775807 / t2)).
    { autounfold with tezos_z; split; [lia|];
      apply Z.div_le_upper_bound; [lia|];
      replace 9223372036854775807
        with ((1 × 9223372036854775807)%Z) at 1 by lia;
      apply Zmult_le_compat_r; lia.
    }
    assert(Heq_t3 : t3 = 9223372036854775807 / t2).
    { specialize (Int64.normalize_identity (9223372036854775807 / t2)) as Hni;
        subst t3; apply Hni; assumption.
    }
    clear Heqt3.

    destruct (Z.le_decidable t1 t3).
    + destruct (_ >? _) eqn:?; simpl; try split; nia.
    + destruct (_ >? _) eqn:?; simpl; lia.
Qed.

Lemma op_starquestion_eq_helper : t t1 i,
  Repr.Valid.t t1
  Int64.Valid.positive i
  t1 (max_int /i64 i)
  t1 ×i64 i = t
  t = t1 ×Z i.
Proof.
  autounfold with tezos_z in ×.
  intros t t1 i H1 H2.
  rewrite normalize_identity; [|lia].
  unfold normalize_int64. autounfold with tezos_z.
  nia.
Qed.

Tez_repr.op_starquestion equals to mutiplication in Z
Lemma op_starquestion_eq : {t t1 i : int64},
  Int64.Valid.non_negative i
  Valid.t (Tez_repr.Tez_tag t1)
  Tez_repr.op_starquestion (Tez_repr.Tez_tag t1) i = return? (Tez_repr.Tez_tag t)
  t = t1 ×Z i.
Proof.
  unfold Tez_repr.op_starquestion.
  intros t t1 i Hi H1.
  repeat match goal with
         | |- context [if ?e then _ else _] ⇒ destruct e eqn:?
         end; [sauto q: on | hauto l: on | sauto q: on | ].
  simpl in *;
  unfold "return?"; intros H; injection H.
  apply op_starquestion_eq_helper; lia.
Qed.

Lemma op_divquestion_is_valid : {t1 t2 : Tez_repr.t},
    Valid.t t1
    Valid.t t2
    let 'Tez_repr.Tez_tag t1' := t1 in
    let 'Tez_repr.Tez_tag t2' := t2 in
    match Tez_repr.op_divquestion t1 t2' with
    | Pervasives.Ok tt2' 0 Valid.t t
    | Pervasives.Error _t2' = 0
    end.
  intros [t1] [t2].
  unfold Tez_repr.op_divquestion.
  destruct (_ i64 _) eqn:?; simpl; [lia|].
  split; [lia|].
  assert (0 t1 / t2 t1) by nia.
  lia.
Qed.

Lemma op_divquestion_eq_helper : r i t,
  Valid.t (Tez_repr.Tez_tag r)
  Int64.Valid.positive i
  r /i64 i = t
  t = r / i.
Proof.
  autounfold with tezos_z.
  intros.
  rewrite normalize_identity in *; nia.
Qed.

Tez_repr.op_divquestion equals to division in Z
Lemma op_divquestion_eq : {t i : int64} {t1 : Tez_repr.t},
  Int64.Valid.t i
  Valid.t t1
  Tez_repr.op_divquestion t1 i = return? (Tez_repr.Tez_tag t)
  let 'Tez_repr.Tez_tag t1' := t1 in
  t = t1' / i.
Proof.
  unfold Tez_repr.op_divquestion. simpl.
  intros t i t1 Hi H.
  destruct (_ <=? 0) eqn:?; [sauto q: on|].
  destruct t1. unfold "return?".
  intros Hok. injection Hok.
  apply op_divquestion_eq_helper; lia.
Qed.

Lemma of_mutez_is_valid : {t1 : Tez_repr.t},
    Valid.t t1
    let 'Tez_repr.Tez_tag t1' := t1 in
    Tez_repr.of_mutez t1' = Some t1.
  autounfold with tezos_z; intros t1 H1; destruct t1 as [t1]; simpl.
  destruct (Z.ltb_spec t1 0); auto; lia.
Qed.

Tez_repr.of_mutez identity in Z
Lemma of_mutez_eq : {i i' : int64},
  Int64.Valid.non_negative i
  Tez_repr.of_mutez i = Some (Tez_repr.Tez_tag i')
  i = i'.
Proof.
  autounfold with tezos_z; simpl; hauto q: on.
Qed.

Lemma of_string_is_valid : (s_value : string),
    match Tez_repr.of_string s_value with
    | Some (Tez_repr.Tez_tag t) ⇒ Int64.Valid.t t
    | NoneTrue
    end.
  intros.
  unfold Tez_repr.of_string.
  destruct (String.split_on_char _ _); [easy|].
  repeat match goal with
         | l : list string |- context[match l with __ end] ⇒ destruct l
         | |- context[if ?e then _ else _] ⇒ destruct e
         | |- match Option.map _ ?e with __ end
           destruct e eqn:Hoptmatch; simpl; [|easy];
           apply Int64.of_string_eq_some_implies_valid in Hoptmatch;
           easy
         | |- match ?t with Tez_repr.Tez_tag t'Int64.Valid.t t' enddestruct t
         end; trivial.
Qed.

Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Tez_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros [x].
  Utils.tezos_z_autounfold.
  simpl.
  unfold Valid.t, Json.wrap_error, to_int64, of_int64. intros.
  split; [lia|]; f_equal; lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma compare_is_valid : Compare.Valid.t (fun _True) id Tez_repr.compare.
Proof.
  apply (Compare.equality (
    let proj '(Tez_repr.Tez_tag t) := t in
    Compare.projection proj Compare.Int64.(Compare.S.compare)
  )); [sauto lq: on|].
  eapply Compare.implies.
  { eapply Compare.projection_is_valid.
    apply Compare.int64_is_valid.
  }
  { trivial. }
  { sauto q: on. }
Qed.

[op_minusquestion] with [Tez_repr.zero] forms an identity
Lemma op_minusquestion_zero_id
      (t : Tez_repr.t) :
  Tez_repr.Valid.t t
  Tez_repr.op_minusquestion t Tez_repr.zero = Pervasives.Ok t.
Proof.
  intros. unfold Tez_repr.zero. destruct t.
  unfold Tez_repr.Valid.t, Tez_repr.Repr.Valid.t in H.
  unfold Tez_repr.op_minusquestion. simpl.
  replace (BinInt.Z.leb BinNums.Z0 r) with true by lia.
  unfold "-i64".
  rewrite Int64.normalize_identity; [|lia].
  now replace (r - 0) with r by lia.
Qed.