Skip to main content

🥊 Round_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Round_repr.

Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.Time.
Require TezosOfOCaml.Proto_alpha.Proofs.Period_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Slot_repr.

#[global] Hint Unfold
  Round_repr.round
  Round_repr.t
  Round_repr.op_eq
  Round_repr.op_ltgt
  Round_repr.op_lt
  Round_repr.op_lteq
  Round_repr.op_gteq
  Round_repr.op_gt
  Round_repr.compare
  Round_repr.equal
  Round_repr.max
  Round_repr.min
  Round_repr.zero
  Round_repr.to_int32
  : tezos_z.

Module Valid.
  Definition t (n : Round_repr.t) : Prop :=
    0 n Int32.max_int.
    #[global] Hint Unfold t : tezos_z.
End Valid.

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

Lemma succ_eq (r : Round_repr.t) :
  Valid.t r
  r Int32.max_int
  Round_repr.succ r = (r + 1)%Z.
  intros.
  unfold Round_repr.succ; simpl.
  destruct (_ =? _) eqn:?; [lia|].
  unfold Int32.succ, "+i32".
  rewrite Int32.normalize_identity; lia.
Qed.

Lemma succ_is_valid (r : Round_repr.t) :
  Valid.t r
  r Int32.max_int
  Valid.t (Round_repr.succ r).
  intros; rewrite succ_eq; lia.
Qed.

Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Round_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
  unfold Round_repr.of_int32.
  autounfold with tezos_z; simpl.
  hauto lq: on solve: lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma of_int32_is_valid (i : int32) :
  Int32.Valid.t i
  letP? round := Round_repr.of_int32 i in
  Valid.t round.
Proof.
  unfold Round_repr.of_int32.
  destruct Round_repr.op_gteq eqn:?; [|easy].
  autounfold with tezos_z in *; simpl in *; lia.
Qed.

Lemma of_int32_to_int32 (n : Round_repr.t) :
  Valid.t n
  Round_repr.of_int32 (Round_repr.to_int32 n) = return? n.
  intros H.
  destruct H.
  autounfold with tezos_z;
  unfold Round_repr.of_int32, Round_repr.op_gteq; simpl.
  replace (n >=? 0) with true; [reflexivity|]; lia.
Qed.

Lemma to_int32_of_int32 (n : int32) :
  Valid.t n
  Round_repr.to_int32 (Round_repr.of_int32 n) = return? n.
  apply of_int32_to_int32.
Qed.

Lemma pred_is_valid (r : Round_repr.t) :
  Valid.t r
  match Round_repr.pred r with
  | Pervasives.Ok r'Valid.t r'
  | Pervasives.Error _True
  end.
  intros.
  unfold Round_repr.pred, Round_repr.of_int32.
  match goal with
  | |- context[if ?e then _ else _] ⇒ destruct e eqn:?; simpl; lia
  end.
Qed.

Lemma pred_eq (r : Round_repr.t) :
  Valid.t r
  r 0
  Round_repr.pred r = return? (r - 1).
  intros.
  unfold Round_repr.pred, Round_repr.of_int32.
  match goal with
  | |- context[if ?e then _ else _] ⇒ destruct e eqn:?; simpl; [|lia]
  end.
  unfold "return?"; f_equal; lia.
Qed.

Lemma of_int_is_valid (i : int) :
  match Round_repr.of_int i with
  | Pervasives.Ok rValid.t r
  | Pervasives.Error _True
  end.
  unfold Round_repr.of_int.
  step; simpl; [lia|].
  unfold Int32.to_int, Int32.of_int.
  step; simpl; lia.
Qed.

Lemma of_int_eq (i : int) :
  Valid.t i
  Round_repr.of_int i = return? i.
  intros; unfold Round_repr.of_int.
  step; simpl; [lia|].
  rewrite Int32.to_int_of_int by lia.
  step; [|lia].
  rewrite Int32.of_int_eq; lia.
Qed.

Lemma to_int_eq (r : Round_repr.t) :
  Int32.Valid.t r
  Round_repr.to_int r = return? r.
  intros; unfold Round_repr.to_int.
  destruct Int32.equal eqn:?; simpl; lia.
Qed.

Lemma of_int_to_int (r : Round_repr.t) :
  Valid.t r
  match Round_repr.to_int r with
  | Pervasives.Ok iRound_repr.of_int i = return? r
  | Pervasives.Error _False
  end.
  intros.
  rewrite to_int_eq by lia; simpl.
  now rewrite of_int_eq.
Qed.

Lemma to_int_of_int (i : int) :
  Valid.t i
  match Round_repr.of_int i with
  | Pervasives.Ok rRound_repr.to_int r = return? i
  | Pervasives.Error _True
  end.
  intros.
  rewrite of_int_eq by trivial; simpl.
  apply to_int_eq; lia.
Qed.

The function [to_slot_is_valid] is valid
Lemma to_slot_is_valid
  round committee_size :
  Int32.Valid.t round
  Pervasives.Int.Valid.t committee_size
  letP? x := Round_repr.to_slot round committee_size in
    Slot_repr.Valid.t x.
Proof.
Admitted.

Module Durations.
  Module Valid.
    Import Proto_alpha.Round_repr.Durations.t.

    Record t (durations : Round_repr.Durations.t) : Prop := {
      first_round_duration :
        Period_repr.Valid.non_zero durations.(first_round_duration);
      delay_increment_per_round :
        Period_repr.Valid.non_zero durations.(delay_increment_per_round);
    }.
  End Valid.

  Lemma create_is_valid
    (first_round_duration delay_increment_per_round : Period_repr.t) :
    Int64.Valid.t first_round_duration
    Int64.Valid.t delay_increment_per_round
    match
      Round_repr.Durations.create first_round_duration delay_increment_per_round
    with
    | Pervasives.Ok durationsValid.t durations
    | Pervasives.Error _True
    end.
    unfold Round_repr.Durations.create, Period_repr.to_seconds.
    repeat match goal with
    | |- context[error_when ?e] ⇒ destruct e eqn:?; simpl; trivial
    end.
    constructor; simpl; lia.
  Qed.

  Lemma create_eq
    (first_round_duration delay_increment_per_round : Period_repr.t) :
    Period_repr.Valid.non_zero first_round_duration
    Period_repr.Valid.non_zero delay_increment_per_round
    Round_repr.Durations.create first_round_duration delay_increment_per_round =
    return? {|
      Round_repr.Durations.t.first_round_duration :=
        first_round_duration;
      Round_repr.Durations.t.delay_increment_per_round :=
        delay_increment_per_round;
    |}.
  Proof.
    intros ? []; unfold Round_repr.Durations.create, Period_repr.to_seconds.
    repeat match goal with
    | |- context[error_when ?e] ⇒ destruct e eqn:?; simpl in *; trivial
    end; lia.
  Qed.

  Lemma create_opt_is_valid
    (first_round_duration delay_increment_per_round : Period_repr.t) :
    Int64.Valid.t first_round_duration
    Int64.Valid.t delay_increment_per_round
    match
      Round_repr.Durations.create_opt
        first_round_duration delay_increment_per_round
    with
    | Some durationsValid.t durations
    | NoneTrue
    end.
  Proof.
    intros; unfold Round_repr.Durations.create_opt.
    specialize
      (create_is_valid first_round_duration delay_increment_per_round); intros.
    destruct Round_repr.Durations.create; tauto.
  Qed.

  Lemma create_opt_eq
    (first_round_duration delay_increment_per_round : Period_repr.t) :
    Period_repr.Valid.non_zero first_round_duration
    Period_repr.Valid.non_zero delay_increment_per_round
    Round_repr.Durations.create_opt
      first_round_duration delay_increment_per_round =
    Some {|
      Round_repr.Durations.t.first_round_duration :=
        first_round_duration;
      Round_repr.Durations.t.delay_increment_per_round :=
        delay_increment_per_round;
    |}.
  Proof.
    intros; unfold Round_repr.Durations.create_opt.
    now rewrite create_eq.
  Qed.

The encoding [Round_repr.Durations.encoding] is valid.
  Lemma encoding_is_valid
    : Data_encoding.Valid.t Valid.t Round_repr.Durations.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros [] []; simpl in ×.
    rewrite create_opt_eq;
      hauto l: on use: Period_repr.Valid.non_zero_implies_t.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Durations.

The function [round_of_timestamp] is valid.