Skip to main content

🕹️ Parameters_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.List.
Require TezosOfOCaml.Proto_alpha.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 BootstrapAccount.
  Module Valid.
    Import 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)
        | NoneTrue
        end;
      amount : Tez_repr.Valid.t b.(amount);
    }.
  End Valid.
End BootstrapAccount.

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

Module Valid.
  Import Parameters_repr.t.

  Record t (p : Parameters_repr.t) : Prop := {
    bootstrap_accounts :
      List.Forall BootstrapAccount.Valid.t p.(bootstrap_accounts);
    bootstrap_contracts :
      List.Forall BootstrapContract.Valid.t p.(bootstrap_contracts);
    commitments :
      List.Forall Commitment_repr.Valid.t p.(commitments);
    constants :
      Constants_repr.Parametric.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
  BootstrapAccount.Valid.t
  Parameters_repr.bootstrap_account_encoding.
  unfold Parameters_repr.bootstrap_account_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros.
  sauto lq: on rew: off.
Qed.
#[global] Hint Resolve bootstrap_account_encoding_is_valid : Data_encoding_db.

Lemma bootstrap_contract_encoding_is_valid :
  Data_encoding.Valid.t BootstrapContract.Valid.t Parameters_repr.bootstrap_contract_encoding.
  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.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.