🎛️ Constants_repr.v

Proofs

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.

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.

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.

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.

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.

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.