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.

In some definitions we need the period to be non-zero.
  Definition non_zero (period : Period_repr.t) : Prop :=
    1 period Int64.max_int.

  #[global] Hint Unfold t non_zero : tezos_z.

[non_zero] is a particular case of [Valid.t].
  Lemma non_zero_implies_t (period : Period_repr.t) :
    non_zero period t period.
  Proof.
    lia.
  Qed.
End Valid.

Module Internal.
  #[global] Hint Unfold
    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.
  Proof.
    intros.
    unfold Period_repr.Internal.mult_, Period_repr.Internal.op_ltgt; simpl.
    destruct negb eqn:?; [|lia].
    destruct negb eqn:? in |- *; [trivial|].
    assert ((a ×i64 b) /i64 a = (a ×i64 b) ÷ a)
      by (apply Int64.normalize_identity; nia).
    assert (a ×i64 b = a ×Z b) by lia.
    lia.
  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).
  Proof.
    intros.
    unfold Period_repr.Internal.mult_, Period_repr.Internal.op_ltgt; simpl.
    destruct negb eqn:?.
    { replace ((a ×i64 b) /i64 a) with ((a ×i64 b) ÷ a)
        by (rewrite <- Int64.normalize_identity; nia).
      replace (a ×i64 b) with (a ×Z b) by lia.
      destruct negb eqn:H_neq in |- *; [|trivial].
      nia.
    }
    { now replace a with 0 by 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.

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

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.