Skip to main content

🪙 Tez_repr.v

Proofs

See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require Import TezosOfOCaml.Environment.V8.Proofs.Utils.

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

    Definition positive (tz : Tez_repr.repr) :=
      0 < tz Int64.max_int.
    #[global] Hint Unfold positive : 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.

  Definition positive (tz : Tez_repr.t) :=
    let 'Tez_repr.Tez_tag repr := tz in
    Repr.Valid.positive repr.
    #[global] Hint Unfold positive : 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.

[Tez_repr.op_minusquestion] is valid
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.

[Tez_repr.sub_opt] is valid
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] computes 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.
  simpl.
  intros.
  destruct (_ <=? _) eqn:?; [| discriminate].
  unfold "-i64" in *; rewrite Int64.normalize_identity in × by lia.
  congruence.
Qed.

The function [op_plusquestion] is valid
Lemma op_plusquestion_is_valid x1 x2 :
  Tez_repr.Valid.t x1
  letP? x3 := Tez_repr.op_plusquestion x1 x2 in
  Tez_repr.Valid.t x3.
Proof.
  intros.
  unfold Tez_repr.op_plusquestion.
  destruct x1, x2; cbn.
  step; cbn; [easy|].
  lia.
Qed.

@Q is this lemma useful? When the first parameter is positive, [op_plus_question] outputs a positive integer.
Lemma op_plusquestion_is_valid_positive x1 x2 :
  Tez_repr.Valid.positive x1
  letP? x3 := Tez_repr.op_plusquestion x1 x2 in
  Tez_repr.Valid.positive x3.
Proof.
  intros.
  unfold Tez_repr.op_plusquestion.
  destruct x1, x2; cbn.
  step; cbn; [easy|].
  split ; lia.
Qed.

[Tez_repr.op_plusquestion] computes 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.
  simpl; intros.
  destruct (_ <? _) eqn:?; [discriminate | ].
  unfold "+i64" in *; rewrite Int64.normalize_identity in × by lia.
  sauto q: on.
Qed.

[Tez_repr.mul_pos] is valid
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.

[Tez_repr.op_starquestion] is valid
Lemma op_starquestion_is_valid (t1 : Tez_repr.t) (t2 : int64) :
  Valid.t t1
  Int64.Valid.t t2
  letP? t := Tez_repr.op_starquestion t1 t2 in
  Valid.t t.
Proof.
  intros.
  unfold Tez_repr.op_starquestion.
  destruct t1.
  destruct (_ <i64 _) eqn:?; simpl; [easy | ].
  destruct (_ =? _) eqn:?; simpl; [lia | ].
  destruct (_ >? _) eqn:H_div64; simpl; [easy | ].
  assert (Int64.Valid.t (max_int ÷ t2)) as H_div by nia.
  unfold "/i64" in H_div64.
  rewrite (Int64.normalize_identity _ H_div) in H_div64.
  nia.
Qed.

[Tez_repr.op_starquestion] auxiliary function
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.
  intros.
  unfold "/i64" in ×.
  rewrite Int64.normalize_identity in × by nia.
  nia.
Qed.

[Tez_repr.op_starquestion] computes multiplication 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.

[Tez_repr.op_divquestion] is valid
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.

The function [op_divquestion] is valid (alternative version)
Lemma op_divquestion_is_valid' a b :
  Tez_repr.Valid.t a
  Int64.Valid.t b
  letP? x := Tez_repr.op_divquestion a b in
  Tez_repr.Valid.t x.
Proof.
  intros H_a H_b.
  unfold Tez_repr.op_divquestion.
  destruct a.
  step; [easy|]. simpl.
  assert (b > 0) by lia.
  unfold "/i64".
  rewrite Int64.normalize_identity by nia.
  nia.
Qed.

[Tez_repr.op_divquestion] auxiliary function
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 Int64.normalize_identity in *; nia.
Qed.

[Tez_repr.op_divquestion] computes 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.

Tez_repr.op_mutez is valid
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] wraps the identity on positive integers
Lemma of_mutez_eq : {i : int64},
  Int64.Valid.non_negative i
  Tez_repr.of_mutez i = Some (Tez_repr.Tez_tag i).
Proof.
  intros.
  unfold Tez_repr.of_mutez.
  destruct (_ <i64 _) eqn:?; lia.
Qed.

[Tez_repr.of_string] is valid
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.

[Tez_repr.encoding] is valid
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Tez_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros.
  destruct_all Tez_repr.t; simpl.
  unfold Z.of_int64.
  unfold Json.wrap_error.
  rewrite Z.to_int64_eq by lia.
  split; [lia | reflexivity].
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[Tez_repr.compare] is valid
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.