Skip to main content

🕰️ Period_repr.v

Proofs

See code, Gitlab , OCaml

Simplifly hypothesis Valid.t to work with lia
#[local] Ltac simpl_tezos_z H :=
  repeat (simpl in H; autounfold with tezos_z in H);
  try (rewrite Bool.andb_true_iff in H; destruct H).

Module Valid.
  Definition t (period : Period_repr.t) : Prop :=
    0 period Int64.max_int.
End Valid.

Module Internal.
  #[global] Hint Unfold
    Valid.t
    Period_repr.Internal.create
    Period_repr.Internal.mult_
    Period_repr.Internal.add_
    Period_repr.Internal.op_ltgt
    Period_repr.Internal.op_eq
    Period_repr.Internal.op_lt
    Period_repr.Internal.op_gt
    Period_repr.Internal.op_lteq
    Period_repr.Internal.op_gteq
    Period_repr.Internal.zero
    Period_repr.Internal.one
    : tezos_z.

  Lemma encoding_is_valid
    : Data_encoding.Valid.t Valid.t Period_repr.Internal.encoding.
    Data_encoding.Valid.data_encoding_auto.
    autounfold with tezos_z.
    hauto q: on solve: lia.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[compare] function is valid
  Lemma compare_is_valid :
    Compare.Valid.t (fun _True) id Period_repr.Internal.compare.
  Proof. Compare.valid_auto. Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.

Helper lemmas
  Lemma create_eq : {i : int64},
      Valid.t i
      Period_repr.Internal.create i = Some i.
    repeat (autounfold with tezos_z; simpl).
    intros.
    assert (Hi : i >=? 0 = true) by lia.
    now rewrite Hi.
  Qed.

  Lemma create_eq_32 : {i : int32},
      Valid.t i
      Period_repr.Internal.create (Int64.of_int32 i) = Some i.
    unfold Int64.of_int32.
    intros.
    apply create_eq. assumption.
  Qed.

  Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Period_repr.Internal.rpc_arg.
    unfold Valid.t.
    simpl. autounfold with tezos_z.
    unfold Period_repr.Internal.rpc_arg.
    eapply RPC_arg.Valid.implies.
    apply RPC_arg.Valid.uint63. simpl.
    autounfold with tezos_z; lia.
  Qed.

  Lemma create_is_valid : {x : int64},
      Int64.Valid.t x
      match Period_repr.Internal.create x with
      | Some yValid.t y
      | NoneTrue
      end.
    Utils.tezos_z_autounfold. simpl.
    intros. unfold Period_repr.Internal.create.
    match goal with
    | [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
    end.
    simpl_tezos_z H.
    repeat simpl_tezos_z Heqb.
    repeat (autounfold with tezos_z; simpl).
    { lia. }
    { constructor. }
  Qed.

  Lemma mult__is_valid : {a b : Period_repr.t},
      Valid.t a
      Valid.t b
      match Period_repr.Internal.mult_ a b with
      | Some cValid.t c
      | NoneTrue
      end.
    #[local] Hint Unfold
         two_pow_63
         two_pow_64
         max_int : lia_fin.

    #[local] Hint Unfold normalize_int64 : tezos_z.

    unfold Int64, "/Z"; simpl.
    unfold
      Period_repr.Internal.mult_,
      Period_repr.Internal.op_ltgt,
      Period_repr.Internal.zero,
      Valid.t, Int64.mul, Int64.div, normalize_int64, mul, div; simpl.
    intros a b [Ha1 Ha2] [Hb1 Hb2].
    destruct (Z.eqb_spec a 0); simpl; [lia|].
    remember ((a × b + two_pow_63) mod two_pow_64 - two_pow_63) as ab64.
    remember ((ab64 / a + two_pow_63) mod two_pow_64 - two_pow_63) as aba64.
    destruct (Z.eqb_spec aba64 b); simpl; [|auto]; split;
      [|subst;autounfold with lia_fin; lia].
    assert(b + two_pow_63 (ab64/a + two_pow_63) mod two_pow_64) by lia.
    assert((ab64 / a + two_pow_63) mod two_pow_64 =
           ab64 / a + two_pow_63 -
                      two_pow_64 × ((ab64 / a + two_pow_63) / two_pow_64)).
    apply Z.mod_eq; [autounfold with lia_fin; lia].
    assert(ab64 / a + two_pow_63 0).
    {
      destruct(Z.leb_spec0 0 ab64).
      - assert(ab64 / a 0) by (apply Z_div_ge0; lia).
        unfold two_pow_63; lia.
      - assert( -two_pow_63 ab64).
        {
          specialize(Int64.normalize_is_valid (a × b)%Z).
          subst; autounfold with tezos_z; lia.
        }
        assert( -two_pow_63 ab64 / a ).
        {
          apply Zdiv_le_lower_bound; [lia|].
          assert(- two_pow_63 × a - two_pow_63)
            by (apply Z.le_mul_diag_l; [autounfold with lia_fin|]; lia); lia.
        }
        lia.
    }
    assert(0%Z two_pow_64 × ((ab64 / a + two_pow_63) / two_pow_64)).
    apply Z.mul_nonneg_nonneg; [autounfold with lia_fin; lia|].
    apply Zdiv_le_lower_bound; [autounfold with lia_fin|]; lia.
    nia.
  Qed.

  Lemma mult__eq : {a b : Period_repr.t},
    Valid.t a
    Valid.t b
    Int64.Valid.t (a × b)%Z
    Period_repr.Internal.mult_ a b = Some (a ×i64 b).

    Utils.tezos_z_autounfold. simpl. unfold "/Z".
    intros.
    match goal with
    | [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
    end.
    assert ((((a × b + 9223372036854775808) mod 18446744073709551616 -
      9223372036854775808) / a + 9223372036854775808)
      mod 18446744073709551616 - 9223372036854775808 = b).
    {
      assert (Hnon0 : a 0) by lia.
      clear Heqb0.
      rewrite Z.mod_eq.
      fold two_pow_63.
      fold two_pow_64.
      replace ((a × b + two_pow_63) mod two_pow_64 - two_pow_63)
        with (Pervasives.normalize_int64 (a × b)) by reflexivity.
      rewrite Int64.normalize_identity.
      rewrite (Z.mul_comm a b).
      rewrite (Z.div_mul).
      { Utils.tezos_z_auto. }
      { assumption. }
      { Utils.tezos_z_auto. }
      { lia. }
    }
    rewrite H2. rewrite Z.eqb_refl. simpl.
    { reflexivity. }
    { f_equal. lia. }
  Qed.

  Lemma add__is_valid : {a b : Period_repr.t},
      Valid.t a
      Valid.t b
      match Period_repr.Internal.add_ a b with
      | Some cValid.t c
      | NoneTrue
      end.
    unfold Period_repr.Internal.add_.
    Utils.tezos_z_autounfold. simpl.
    intros.
    repeat match goal with
    | [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
    end; try constructor; try lia.
    rewrite Bool.orb_false_iff in Heqb0.
    destruct Heqb0.
    lia.
  Qed.
End Internal.

Lemma of_seconds_is_valid : {secs : int64},
    Valid.t secs
    match Period_repr.of_seconds secs with
    | Pervasives.Ok yValid.t y
    | Pervasives.Error _True
    end.
  unfold Period_repr.of_seconds.
  repeat (Utils.tezos_z_autounfold; simpl).
  intros.
  match goal with
  | [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
  end; simpl; try constructor; try lia.
Qed.

Lemma of_seconds_exn_is_valid : {secs : int64},
    Valid.t secs
    Valid.t (Period_repr.of_seconds_exn secs).
  unfold Period_repr.of_seconds_exn.
  repeat (autounfold with tezos_z; simpl).
  intros. simpl_tezos_z H.
  match goal with
  | [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
  end; try lia.
Qed.

Lemma mult_eq : {i : int32} {p : int64},
    Valid.t i
    Valid.t p
    Int64.Valid.t (i × p)%Z
    Period_repr.mult i p = return? (i × p)%Z.
  intros i p Hi Hp Hip.
  unfold Period_repr.mult. simpl.
  rewrite Internal.create_eq_32; try assumption.
  rewrite Internal.mult__eq; trivial.
  autounfold with tezos_z.
  now rewrite Int64.normalize_identity.
Qed.

Lemma add_eq_helper : {p1 p2 : int64},
    Valid.t p1
    Valid.t p2
    (p1 + p2 <? p1) || (p1 + p2 <? p2) = false.
  autounfold with tezos_z. simpl.
  intros.
  simpl_tezos_z H.
  simpl_tezos_z H0.
  assert (H_p2 : p1 + p2 <? p1 = false) by lia.
  assert (H_p1 : p1 + p2 <? p2 = false) by lia.
  rewrite H_p2, H_p1.
  reflexivity.
Qed.

Lemma add_eq : {p1 p2 : int64},
    Valid.t p1
    Valid.t p2
    Int64.Valid.t (p1 + p2)%Z
    match Period_repr.add p1 p2 with
    | Pervasives.Ok yy = (p1 + p2)%Z
    | Pervasives.Error _False
    end.
  intros p1 p2 H1 H2 H3.
  unfold Period_repr.add.
  repeat (autounfold with tezos_z; simpl).
  repeat rewrite Int64.normalize_identity.
  assert (H : (p1 + p2 <? p1) || (p1 + p2 <? p2) = false).
  { apply add_eq_helper; assumption. }
  rewrite H. unfold "return?". constructor.
  assumption.
Qed.

Lemma one_second_is_valid : Valid.t Period_repr.one_second.
  cbv; intuition; discriminate H.
Qed.

Lemma one_minute_is_valid : Valid.t Period_repr.one_minute.
  cbv. intuition; discriminate H.
Qed.

Lemma one_hour_is_valid : Valid.t Period_repr.one_hour.
  cbv. intuition; discriminate H.
Qed.

Lemma encoding_is_valid
  : Data_encoding.Valid.t Valid.t Period_repr.encoding.
  exact Internal.encoding_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[compare] function is valid
Lemma compare_is_valid :
  Compare.Valid.t (fun _True) id Period_repr.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

#[local] Definition is_ok_valid (x : M? int64) :=
  match x with
  | Pervasives.Ok yValid.t y
  | Pervasives.Error _False
  end.
#[local] Hint Unfold is_ok_valid : tezos_z.

Lemma add_is_valid : {a b : int64},
  Valid.t a
  Valid.t b
  Valid.t (a + b)%Z
  is_ok_valid (Period_repr.add a b).

  Local Hint Unfold Period_repr.add : tezos_z.
  repeat (autounfold with tezos_z; simpl).
  intros.
  rewrite Int64.normalize_identity; try (repeat (autounfold with tezos_z; simpl); lia).
  rewrite add_eq_helper; lia.
Qed.

Lemma mult_is_valid : {a b : int64},
  Valid.t a
  Valid.t b
  Int64.Valid.t (a × b)%Z
  is_ok_valid (Period_repr.mult a b).

  #[local] Hint Unfold Period_repr.mult Int64.Valid.t normalize_int64 : tezos_z.

  autounfold with tezos_z; simpl;
  intros;
  rewrite Internal.create_eq; try (autounfold with tezos_z; lia);
  rewrite Internal.mult__eq; try (autounfold with tezos_z; lia);
  simpl; lia.
Qed.