🕹️ Parameters_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Commitment_repr.

Require TezosOfOCaml.Proto_alpha.Parameters_repr.

Module bootstrap_account.
  Module Valid.
    Import Proto_alpha.Parameters_repr.bootstrap_account.

    Record t (b : Parameters_repr.bootstrap_account) : Prop := {
      public_key :
        match b.(public_key) with
        | Some public_key ⇒
            Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) public_key = b.(public_key_hash)
        | None ⇒ True
        end;
      amount : Tez_repr.Valid.t b.(amount);
      delegate_to :
        match b.(delegate_to), b.(consensus_key) with
        | Some _, Some _ ⇒ False
        | _, _ ⇒ True
        end;
      consensus_key :
        match
            b.(Parameters_repr.bootstrap_account.public_key),
            b.(consensus_key)
        with
        | None, Some _ ⇒ False
        | _, _ ⇒ True
        end;
    }.
  End Valid.
End bootstrap_account.

Module bootstrap_contract.
  Module Valid.
    Definition t c :=
      Tez_repr.Valid.t c.(Parameters_repr.bootstrap_contract.amount).
  End Valid.
End bootstrap_contract.

Module Valid.
  Import Parameters_repr.t.

  Record t (p : Parameters_repr.t) : Prop := {
    bootstrap_accounts :
      List.Forall bootstrap_account.Valid.t p.(bootstrap_accounts);
    bootstrap_contracts :
      List.Forall bootstrap_contract.Valid.t p.(bootstrap_contracts);
    commitments :
      List.Forall Commitment_repr.Valid.t p.(commitments);
    constants :
      Constants_parametric_repr.Valid.t p.(constants);
    security_deposit_ramp_up_cycles :
      Option.Forall Pervasives.Int31.Valid.t p.(security_deposit_ramp_up_cycles);
    no_reward_cycles :
      Option.Forall Pervasives.Int31.Valid.t p.(no_reward_cycles);
  }.
End Valid.

Lemma bootstrap_account_encoding_is_valid :
  Data_encoding.Valid.t
  bootstrap_account.Valid.t
  Parameters_repr.bootstrap_account_encoding.
Proof.
  unfold Parameters_repr.bootstrap_account_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros [] [].
  simpl in ×.
  repeat match goal with
  | v : option _ |- _ ⇒ destruct v
  end; sauto lq: on.
Qed.
#[global] Hint Resolve bootstrap_account_encoding_is_valid : Data_encoding_db.

Lemma bootstrap_contract_encoding_is_valid :
  Data_encoding.Valid.t bootstrap_contract.Valid.t Parameters_repr.bootstrap_contract_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  destruct x eqn:Eq_x, delegate eqn:Eq_delegate; tauto.
Qed.
#[global] Hint Resolve bootstrap_contract_encoding_is_valid : Data_encoding_db.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Parameters_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.