🥊 Round_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.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 r ⇒ Valid.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 i ⇒ Round_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 r ⇒ Round_repr.to_int r = return? i
| Pervasives.Error _ ⇒ True
end.
intros.
rewrite of_int_eq by trivial; simpl.
apply to_int_eq; lia.
Qed.
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 r ⇒ Valid.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 i ⇒ Round_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 r ⇒ Round_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 durations ⇒ Valid.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 durations ⇒ Valid.t durations
| None ⇒ True
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.
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 durations ⇒ Valid.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 durations ⇒ Valid.t durations
| None ⇒ True
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.
: 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.
Lemma round_of_timestamp_is_valid
round_durations predecessor_timestamp predecessor_round timestamp
(H_round_durations : Durations.Valid.t round_durations)
(H_predecessor_timestamp : Time.Valid.t predecessor_timestamp)
(H_predecessor_round : Valid.t predecessor_round)
(H_timestamp : Time.Valid.t timestamp) :
letP? round :=
Round_repr.round_of_timestamp
round_durations predecessor_timestamp predecessor_round timestamp in
Valid.t round.
Proof.
Admitted.
round_durations predecessor_timestamp predecessor_round timestamp
(H_round_durations : Durations.Valid.t round_durations)
(H_predecessor_timestamp : Time.Valid.t predecessor_timestamp)
(H_predecessor_round : Valid.t predecessor_round)
(H_timestamp : Time.Valid.t timestamp) :
letP? round :=
Round_repr.round_of_timestamp
round_durations predecessor_timestamp predecessor_round timestamp in
Valid.t round.
Proof.
Admitted.