Skip to main content

🍃 Protocol.v

Environment

Gitlab , OCaml

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

Require Proto_alpha.Environment.Data_encoding.
Require Proto_alpha.Environment.Protocol_hash.
Require Proto_alpha.Environment.S.

Module component.
  Record record {name interface implementation : Set} : Set := Build {
    name : name;
    interface : interface;
    implementation : implementation }.
  Arguments record : clear implicits.
  Definition with_name {t_name t_interface t_implementation} name
    (r : record t_name t_interface t_implementation) :=
    Build t_name t_interface t_implementation name r.(interface)
      r.(implementation).
  Definition with_interface {t_name t_interface t_implementation} interface
    (r : record t_name t_interface t_implementation) :=
    Build t_name t_interface t_implementation r.(name) interface
      r.(implementation).
  Definition with_implementation {t_name t_interface t_implementation}
    implementation (r : record t_name t_interface t_implementation) :=
    Build t_name t_interface t_implementation r.(name) r.(interface)
      implementation.
End component.
Definition component_skeleton := component.record.

Module t.
  Record record {expected_env components : Set} : Set := Build {
    expected_env : expected_env;
    components : components }.
  Arguments record : clear implicits.
  Definition with_expected_env {t_expected_env t_components} expected_env
    (r : record t_expected_env t_components) :=
    Build t_expected_env t_components expected_env r.(components).
  Definition with_components {t_expected_env t_components} components
    (r : record t_expected_env t_components) :=
    Build t_expected_env t_components r.(expected_env) components.
End t.
Definition t_skeleton := t.record.

Reserved Notation "'t".
Reserved Notation "'component".

Inductive env_version : Set :=
| V0 : env_version
| V1 : env_version
| V2 : env_version
| V3 : env_version
| V4 : env_version
| V5 : env_version

where "'component" := (component_skeleton string (option string) string)
and "'t" := (t_skeleton env_version (list 'component)).

Definition t := 't.
Definition component := 'component.

Parameter component_encoding : Data_encoding.t component.

Parameter env_version_encoding : Data_encoding.t env_version.

Parameter Included_HASHABLE : S.HASHABLE (t := t) (hash := Protocol_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 Protocol_hash.t :=
  Included_HASHABLE.(S.HASHABLE.hash_value).

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