Skip to main content

🍃 Signature.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Chain_id.
Require Proto_alpha.Environment.Ed25519.
Require Proto_alpha.Environment.P256.
Require Proto_alpha.Environment.S.
Require Proto_alpha.Environment.Secp256k1.

Inductive public_key_hash : Set :=
| Ed25519Hash :
  Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) public_key_hash
| Secp256k1Hash :
  Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) public_key_hash
| P256Hash :
  P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) public_key_hash.

Inductive public_key : Set :=
| Ed25519 : Ed25519.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) public_key
| Secp256k1 : Secp256k1.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) public_key
| P256 : P256.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) public_key.

Inductive watermark : Set :=
| Block_header : Chain_id.t watermark
| Endorsement : Chain_id.t watermark
| Generic_operation : watermark
| Custom : bytes watermark.

Parameter Included_SIGNATURE_Public_key_hash_Set_t : Set.

Parameter Included_SIGNATURE_Public_key_hash_Map_t : Set Set.

Parameter Included_SIGNATURE_t : Set.

Parameter Included_SIGNATURE :
  S.SIGNATURE (Public_key_hash_t := public_key_hash)
    (Public_key_hash_Set_t := Included_SIGNATURE_Public_key_hash_Set_t)
    (Public_key_hash_Map_t := Included_SIGNATURE_Public_key_hash_Map_t)
    (Public_key_t := public_key) (t := Included_SIGNATURE_t)
    (watermark := watermark).

Definition Public_key_hash :=
  Included_SIGNATURE.(S.SIGNATURE.Public_key_hash).

Definition Public_key := Included_SIGNATURE.(S.SIGNATURE.Public_key).

Definition t := Included_SIGNATURE.(S.SIGNATURE.t).

Definition pp : Format.formatter t unit :=
  Included_SIGNATURE.(S.SIGNATURE.pp).

Definition size_value : int := Included_SIGNATURE.(S.SIGNATURE.size_value).

Definition to_bytes : t bytes := Included_SIGNATURE.(S.SIGNATURE.to_bytes).

Definition of_bytes_opt : bytes option t :=
  Included_SIGNATURE.(S.SIGNATURE.of_bytes_opt).

Definition of_bytes_exn : bytes t :=
  Included_SIGNATURE.(S.SIGNATURE.of_bytes_exn).

Definition op_eq : t t bool := Included_SIGNATURE.(S.SIGNATURE.op_eq).

Definition op_ltgt : t t bool :=
  Included_SIGNATURE.(S.SIGNATURE.op_ltgt).

Definition op_lt : t t bool := Included_SIGNATURE.(S.SIGNATURE.op_lt).

Definition op_lteq : t t bool :=
  Included_SIGNATURE.(S.SIGNATURE.op_lteq).

Definition op_gteq : t t bool :=
  Included_SIGNATURE.(S.SIGNATURE.op_gteq).

Definition op_gt : t t bool := Included_SIGNATURE.(S.SIGNATURE.op_gt).

Definition compare : t t int :=
  Included_SIGNATURE.(S.SIGNATURE.compare).

Definition equal : t t bool := Included_SIGNATURE.(S.SIGNATURE.equal).

Definition max : t t t := Included_SIGNATURE.(S.SIGNATURE.max).

Definition min : t t t := Included_SIGNATURE.(S.SIGNATURE.min).

Definition to_b58check : t string :=
  Included_SIGNATURE.(S.SIGNATURE.to_b58check).

Definition to_short_b58check : t string :=
  Included_SIGNATURE.(S.SIGNATURE.to_short_b58check).

Definition of_b58check_exn : string t :=
  Included_SIGNATURE.(S.SIGNATURE.of_b58check_exn).

Definition of_b58check_opt : string option t :=
  Included_SIGNATURE.(S.SIGNATURE.of_b58check_opt).

Definition b58check_encoding : Base58.encoding t :=
  Included_SIGNATURE.(S.SIGNATURE.b58check_encoding).

Definition encoding : Data_encoding.t t :=
  Included_SIGNATURE.(S.SIGNATURE.encoding).

Definition rpc_arg : RPC_arg.t t := Included_SIGNATURE.(S.SIGNATURE.rpc_arg).

Definition zero : t := Included_SIGNATURE.(S.SIGNATURE.zero).

Definition check : option watermark public_key t bytes bool :=
  Included_SIGNATURE.(S.SIGNATURE.check).