Skip to main content

🍃 Block_header.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Block_hash.
Require Proto_alpha.Environment.Bytes.
Require Proto_alpha.Environment.Context_hash.
Require Proto_alpha.Environment.Int32.
Require Proto_alpha.Environment.Operation_list_list_hash.
Require Proto_alpha.Environment.Time.

Module shell_header.
  Record record : Set := Build {
    level : Int32.t;
    proto_level : int;
    predecessor : Block_hash.t;
    timestamp : Time.t;
    validation_passes : int;
    operations_hash : Operation_list_list_hash.t;
    fitness : list Bytes.t;
    context : Context_hash.t }.
  Definition with_level level (r : record) :=
    Build level r.(proto_level) r.(predecessor) r.(timestamp)
      r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
  Definition with_proto_level proto_level (r : record) :=
    Build r.(level) proto_level r.(predecessor) r.(timestamp)
      r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
  Definition with_predecessor predecessor (r : record) :=
    Build r.(level) r.(proto_level) predecessor r.(timestamp)
      r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
  Definition with_timestamp timestamp (r : record) :=
    Build r.(level) r.(proto_level) r.(predecessor) timestamp
      r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
  Definition with_validation_passes validation_passes (r : record) :=
    Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
      validation_passes r.(operations_hash) r.(fitness) r.(context).
  Definition with_operations_hash operations_hash (r : record) :=
    Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
      r.(validation_passes) operations_hash r.(fitness) r.(context).
  Definition with_fitness fitness (r : record) :=
    Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
      r.(validation_passes) r.(operations_hash) fitness r.(context).
  Definition with_context context (r : record) :=
    Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
      r.(validation_passes) r.(operations_hash) r.(fitness) context.
End shell_header.
Definition shell_header := shell_header.record.

Parameter shell_header_encoding : Data_encoding.t shell_header.

Module t.
  Record record : Set := Build {
    shell : shell_header;
    protocol_data : bytes }.
  Definition with_shell shell (r : record) :=
    Build shell r.(protocol_data).
  Definition with_protocol_data protocol_data (r : record) :=
    Build r.(shell) protocol_data.
End t.
Definition t := t.record.

Parameter Included_HASHABLE : S.HASHABLE (t := t) (hash := Block_hash.t).

Definition op_eq : t t bool := Included_HASHABLE.(S.HASHABLE.op_eq).

Definition op_ltgt : t t bool := Included_HASHABLE.(S.HASHABLE.op_ltgt).

Definition op_lt : t t bool := Included_HASHABLE.(S.HASHABLE.op_lt).

Definition op_lteq : t t bool := Included_HASHABLE.(S.HASHABLE.op_lteq).

Definition op_gteq : t t bool := Included_HASHABLE.(S.HASHABLE.op_gteq).

Definition op_gt : t t bool := Included_HASHABLE.(S.HASHABLE.op_gt).

Definition compare : t t int := Included_HASHABLE.(S.HASHABLE.compare).

Definition equal : t t bool := Included_HASHABLE.(S.HASHABLE.equal).

Definition max : t t t := Included_HASHABLE.(S.HASHABLE.max).

Definition min : t t t := Included_HASHABLE.(S.HASHABLE.min).

Definition pp : Format.formatter t unit :=
  Included_HASHABLE.(S.HASHABLE.pp).

Definition encoding : Data_encoding.t t :=
  Included_HASHABLE.(S.HASHABLE.encoding).

Definition to_bytes : t bytes := Included_HASHABLE.(S.HASHABLE.to_bytes).

Definition of_bytes : bytes option t :=
  Included_HASHABLE.(S.HASHABLE.of_bytes).

Definition hash_value : t Block_hash.t :=
  Included_HASHABLE.(S.HASHABLE.hash_value).

Definition hash_raw : bytes Block_hash.t :=
  Included_HASHABLE.(S.HASHABLE.hash_raw).