🍃 Block_header.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Block_hash.
Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Context_hash.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Operation_list_list_hash.
Require TezosOfOCaml.Environment.Structs.V0.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).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Block_hash.
Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Context_hash.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Operation_list_list_hash.
Require TezosOfOCaml.Environment.Structs.V0.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).