🎛️ Constants_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Period_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Period_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Encoding [fixed_encoding] is valid.
Lemma fixed_encoding_is_valid
: Data_encoding.Valid.t (fun _ ⇒ True) Constants_repr.fixed_encoding.
Data_encoding.Valid.data_encoding_auto.
intros []; now repeat constructor.
Qed.
#[global] Hint Resolve fixed_encoding_is_valid : Data_encoding_db.
: Data_encoding.Valid.t (fun _ ⇒ True) Constants_repr.fixed_encoding.
Data_encoding.Valid.data_encoding_auto.
intros []; now repeat constructor.
Qed.
#[global] Hint Resolve fixed_encoding_is_valid : Data_encoding_db.
The validity predicate for [Constants_repr.t].
Module Valid.
Definition t (x : Constants_repr.t) : Prop :=
Constants_parametric_repr.Valid.t x.(Constants_repr.t.parametric).
End Valid.
Definition t (x : Constants_repr.t) : Prop :=
Constants_parametric_repr.Valid.t x.(Constants_repr.t.parametric).
End Valid.
The function [all_of_parametric] is valid.
Lemma all_of_parametric_is_valid parametric_value :
Constants_parametric_repr.Valid.t parametric_value →
Valid.t (Constants_repr.all_of_parametric parametric_value).
Proof.
trivial.
Qed.
Constants_parametric_repr.Valid.t parametric_value →
Valid.t (Constants_repr.all_of_parametric parametric_value).
Proof.
trivial.
Qed.
Encoding [encoding] is valid.
Lemma encoding_is_valid
: Data_encoding.Valid.t Valid.t Constants_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
: Data_encoding.Valid.t Valid.t Constants_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
The function [check_constants] should always succeed.
Lemma check_constants_eq constants :
Constants_parametric_repr.Valid.t constants →
Constants_repr.check_constants constants =
return? tt.
Proof.
intros [].
repeat match goal with
| H : _ ∧ _ |- _ ⇒ destruct H
end.
unfold Constants_repr.check_constants.
destruct constants; simpl in ×.
assert (H_error_and : ∀ c1 c2 err (e : M? unit),
(let? '_ := Error_monad.error_unless (c1 && c2) err in e) =
(let? '_ := Error_monad.error_unless c1 err in
let? '_ := Error_monad.error_unless c2 err in
e)
) by (intros [] []; reflexivity).
repeat rewrite H_error_and; clear H_error_and.
unfold error_unless.
change Period_repr.zero with 0 in ×.
repeat (step; [|cbn in *; lia]); cbn.
destruct_all (Ratio_repr.Valid.t minimal_participation_ratio);
destruct minimal_participation_ratio; destruct denominator;
cbn in *; red in H4; cbn in H4.
do 6 (step; [|lia]).
step; cbn; [|
unfold Tez_repr.op_gteq in *; cbn in *;
destruct double_baking_punishment as []; cbn in *; lia].
do 2 (step; [|
destruct ratio_of_frozen_deposits_slashed_per_double_endorsement0;
cbn in *;
destruct ratio_of_frozen_deposits_slashed_per_double_endorsement
as [];
cbn in *;
lia]); cbn.
do 4 (step; [cbn|lia]).
match goal with
| |- context [if ?e then _ else _] ⇒
assert (H_vdf : e = true)
end.
{ cbn in ×. unfold Int64.of_int, Int64.of_int32, Int64.one.
clear - vdf_difficulty_invariant; step; lia.
}
rewrite H_vdf; cbn.
destruct sc_rollup, sc_rollup0, stake_amount0, dal; cbn in ×.
now repeat (step; [cbn|lia]).
Qed.
Constants_parametric_repr.Valid.t constants →
Constants_repr.check_constants constants =
return? tt.
Proof.
intros [].
repeat match goal with
| H : _ ∧ _ |- _ ⇒ destruct H
end.
unfold Constants_repr.check_constants.
destruct constants; simpl in ×.
assert (H_error_and : ∀ c1 c2 err (e : M? unit),
(let? '_ := Error_monad.error_unless (c1 && c2) err in e) =
(let? '_ := Error_monad.error_unless c1 err in
let? '_ := Error_monad.error_unless c2 err in
e)
) by (intros [] []; reflexivity).
repeat rewrite H_error_and; clear H_error_and.
unfold error_unless.
change Period_repr.zero with 0 in ×.
repeat (step; [|cbn in *; lia]); cbn.
destruct_all (Ratio_repr.Valid.t minimal_participation_ratio);
destruct minimal_participation_ratio; destruct denominator;
cbn in *; red in H4; cbn in H4.
do 6 (step; [|lia]).
step; cbn; [|
unfold Tez_repr.op_gteq in *; cbn in *;
destruct double_baking_punishment as []; cbn in *; lia].
do 2 (step; [|
destruct ratio_of_frozen_deposits_slashed_per_double_endorsement0;
cbn in *;
destruct ratio_of_frozen_deposits_slashed_per_double_endorsement
as [];
cbn in *;
lia]); cbn.
do 4 (step; [cbn|lia]).
match goal with
| |- context [if ?e then _ else _] ⇒
assert (H_vdf : e = true)
end.
{ cbn in ×. unfold Int64.of_int, Int64.of_int32, Int64.one.
clear - vdf_difficulty_invariant; step; lia.
}
rewrite H_vdf; cbn.
destruct sc_rollup, sc_rollup0, stake_amount0, dal; cbn in ×.
now repeat (step; [cbn|lia]).
Qed.
The function [check_constants] is valid.
Lemma check_constants_is_valid constants :
Constants_parametric_repr.Valid.t constants →
letP? _ := Constants_repr.check_constants constants in
True.
Proof.
intros.
now rewrite check_constants_eq.
Qed.
Constants_parametric_repr.Valid.t constants →
letP? _ := Constants_repr.check_constants constants in
True.
Proof.
intros.
now rewrite check_constants_eq.
Qed.