Skip to main content

🧱 Block_header_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Time_repr.

Module contents.
  Record record : Set := Build {
    payload_hash : Block_payload_hash.t;
    payload_round : Round_repr.t;
    seed_nonce_hash : option Nonce_hash.t;
    proof_of_work_nonce : bytes;
    liquidity_baking_toggle_vote :
      Liquidity_baking_repr.liquidity_baking_toggle_vote;
  }.
  Definition with_payload_hash payload_hash (r : record) :=
    Build payload_hash r.(payload_round) r.(seed_nonce_hash)
      r.(proof_of_work_nonce) r.(liquidity_baking_toggle_vote).
  Definition with_payload_round payload_round (r : record) :=
    Build r.(payload_hash) payload_round r.(seed_nonce_hash)
      r.(proof_of_work_nonce) r.(liquidity_baking_toggle_vote).
  Definition with_seed_nonce_hash seed_nonce_hash (r : record) :=
    Build r.(payload_hash) r.(payload_round) seed_nonce_hash
      r.(proof_of_work_nonce) r.(liquidity_baking_toggle_vote).
  Definition with_proof_of_work_nonce proof_of_work_nonce (r : record) :=
    Build r.(payload_hash) r.(payload_round) r.(seed_nonce_hash)
      proof_of_work_nonce r.(liquidity_baking_toggle_vote).
  Definition with_liquidity_baking_toggle_vote liquidity_baking_toggle_vote
    (r : record) :=
    Build r.(payload_hash) r.(payload_round) r.(seed_nonce_hash)
      r.(proof_of_work_nonce) liquidity_baking_toggle_vote.
End contents.
Definition contents := contents.record.

Module protocol_data.
  Record record : Set := Build {
    contents : contents;
    signature : Signature.t;
  }.
  Definition with_contents contents (r : record) :=
    Build contents r.(signature).
  Definition with_signature signature (r : record) :=
    Build r.(contents) signature.
End protocol_data.
Definition protocol_data := protocol_data.record.

Module t.
  Record record : Set := Build {
    shell : Block_header.shell_header;
    protocol_data : protocol_data;
  }.
  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.

Definition block_header : Set := t.

Definition raw : Set := Block_header.t.

Definition shell_header : Set := Block_header.shell_header.

Definition raw_encoding : Data_encoding.t Block_header.t :=
  Block_header.encoding.

Definition shell_header_encoding : Data_encoding.t Block_header.shell_header :=
  Block_header.shell_header_encoding.

Inductive block_watermark : Set :=
| Block_header : Chain_id.t block_watermark.

Definition bytes_of_block_watermark (function_parameter : block_watermark)
  : bytes :=
  let 'Block_header chain_id := function_parameter in
  Bytes.cat (Bytes.of_string (String.String "017" ""))
    (Chain_id.to_bytes chain_id).

Definition to_watermark (b_value : block_watermark) : Signature.watermark :=
  Signature.Custom (bytes_of_block_watermark b_value).

Definition of_watermark (function_parameter : Signature.watermark)
  : option block_watermark :=
  match function_parameter with
  | Signature.Custom b_value
    if (Bytes.length b_value) >i 0 then
      match Bytes.get b_value 0 with
      | "017" % char
        Option.map (fun (chain_id : Chain_id.t) ⇒ Block_header chain_id)
          (Chain_id.of_bytes_opt
            (Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
      | _None
      end
    else
      None
  | _None
  end.

Definition contents_encoding : Data_encoding.encoding contents :=
  Data_encoding.def "block_header.alpha.unsigned_contents" None None
    (Data_encoding.conv
      (fun (function_parameter : contents) ⇒
        let '{|
          contents.payload_hash := payload_hash;
            contents.payload_round := payload_round;
            contents.seed_nonce_hash := seed_nonce_hash;
            contents.proof_of_work_nonce := proof_of_work_nonce;
            contents.liquidity_baking_toggle_vote :=
              liquidity_baking_toggle_vote
            |} := function_parameter in
        (payload_hash, payload_round, proof_of_work_nonce, seed_nonce_hash,
          liquidity_baking_toggle_vote))
      (fun (function_parameter :
        Block_payload_hash.t × Round_repr.t × Bytes.t × option Nonce_hash.t ×
          Liquidity_baking_repr.liquidity_baking_toggle_vote) ⇒
        let
          '(payload_hash, payload_round, proof_of_work_nonce, seed_nonce_hash,
            liquidity_baking_toggle_vote) := function_parameter in
        {| contents.payload_hash := payload_hash;
          contents.payload_round := payload_round;
          contents.seed_nonce_hash := seed_nonce_hash;
          contents.proof_of_work_nonce := proof_of_work_nonce;
          contents.liquidity_baking_toggle_vote := liquidity_baking_toggle_vote;
          |}) None
      (Data_encoding.obj5
        (Data_encoding.req None None "payload_hash" Block_payload_hash.encoding)
        (Data_encoding.req None None "payload_round" Round_repr.encoding)
        (Data_encoding.req None None "proof_of_work_nonce"
          (Data_encoding.Fixed.bytes_value
            Constants_repr.proof_of_work_nonce_size))
        (Data_encoding.opt None None "seed_nonce_hash" Nonce_hash.encoding)
        (Data_encoding.req None None "liquidity_baking_toggle_vote"
          Liquidity_baking_repr.liquidity_baking_toggle_vote_encoding))).

Definition protocol_data_encoding : Data_encoding.encoding protocol_data :=
  Data_encoding.def "block_header.alpha.signed_contents" None None
    (Data_encoding.conv
      (fun (function_parameter : protocol_data) ⇒
        let '{|
          protocol_data.contents := contents;
            protocol_data.signature := signature
            |} := function_parameter in
        (contents, signature))
      (fun (function_parameter : contents × Signature.t) ⇒
        let '(contents, signature) := function_parameter in
        {| protocol_data.contents := contents;
          protocol_data.signature := signature; |}) None
      (Data_encoding.merge_objs contents_encoding
        (Data_encoding.obj1
          (Data_encoding.req None None "signature" Signature.encoding)))).

Definition raw_value (function_parameter : t) : Block_header.t :=
  let '{| t.shell := shell; t.protocol_data := protocol_data |} :=
    function_parameter in
  let protocol_data :=
    Data_encoding.Binary.to_bytes_exn None protocol_data_encoding protocol_data
    in
  {| Block_header.t.shell := shell;
    Block_header.t.protocol_data := protocol_data; |}.

Definition unsigned_encoding
  : Data_encoding.encoding (Block_header.shell_header × contents) :=
  Data_encoding.merge_objs Block_header.shell_header_encoding contents_encoding.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.def "block_header.alpha.full_header" None None
    (Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{| t.shell := shell; t.protocol_data := protocol_data |} :=
          function_parameter in
        (shell, protocol_data))
      (fun (function_parameter : Block_header.shell_header × protocol_data) ⇒
        let '(shell, protocol_data) := function_parameter in
        {| t.shell := shell; t.protocol_data := protocol_data; |}) None
      (Data_encoding.merge_objs Block_header.shell_header_encoding
        protocol_data_encoding)).

Definition max_header_length : int :=
  let fake_level := Raw_level_repr.root_value in
  let fake_round := Round_repr.zero in
  let fake_fitness :=
    Fitness_repr.create_without_locked_round fake_level fake_round fake_round in
  let fake_shell : Block_header.shell_header :=
    {| Block_header.shell_header.level := 0;
      Block_header.shell_header.proto_level := 0;
      Block_header.shell_header.predecessor := Block_hash.zero;
      Block_header.shell_header.timestamp := Time.of_seconds 0;
      Block_header.shell_header.validation_passes := 0;
      Block_header.shell_header.operations_hash :=
        Operation_list_list_hash.zero;
      Block_header.shell_header.fitness := Fitness_repr.to_raw fake_fitness;
      Block_header.shell_header.context := Context_hash.zero; |}
  in let fake_contents : contents :=
    {| contents.payload_hash := Block_payload_hash.zero;
      contents.payload_round := Round_repr.zero;
      contents.seed_nonce_hash := Some Nonce_hash.zero;
      contents.proof_of_work_nonce :=
        Bytes.make Constants_repr.proof_of_work_nonce_size "0" % char;
      contents.liquidity_baking_toggle_vote := Liquidity_baking_repr.LB_pass; |}
    in
  Data_encoding.Binary.length encoding
    {| t.shell := fake_shell;
      t.protocol_data :=
        {| protocol_data.contents := fake_contents;
          protocol_data.signature := Signature.zero; |}; |}.

Definition hash_raw : Block_header.t Block_hash.t := Block_header.hash_value.

Definition hash_value (function_parameter : t) : Block_hash.t :=
  let '{| t.shell := shell; t.protocol_data := protocol_data |} :=
    function_parameter in
  Block_header.hash_value
    {| Block_header.t.shell := shell;
      Block_header.t.protocol_data :=
        Data_encoding.Binary.to_bytes_exn None protocol_data_encoding
          protocol_data; |}.

Module locked_round_evidence.
  Record record : Set := Build {
    preendorsement_round : Round_repr.t;
    preendorsement_count : int;
  }.
  Definition with_preendorsement_round preendorsement_round (r : record) :=
    Build preendorsement_round r.(preendorsement_count).
  Definition with_preendorsement_count preendorsement_count (r : record) :=
    Build r.(preendorsement_round) preendorsement_count.
End locked_round_evidence.
Definition locked_round_evidence := locked_round_evidence.record.

Module Invalid_payload_hash.
  Record record : Set := Build {
    expected : Block_payload_hash.t;
    provided : Block_payload_hash.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Invalid_payload_hash.
Definition Invalid_payload_hash := Invalid_payload_hash.record.

Module Locked_round_after_block_round.
  Record record : Set := Build {
    locked_round : Round_repr.t;
    round : Round_repr.t;
  }.
  Definition with_locked_round locked_round (r : record) :=
    Build locked_round r.(round).
  Definition with_round round (r : record) :=
    Build r.(locked_round) round.
End Locked_round_after_block_round.
Definition Locked_round_after_block_round :=
  Locked_round_after_block_round.record.

Module Invalid_payload_round.
  Record record : Set := Build {
    payload_round : Round_repr.t;
    round : Round_repr.t;
  }.
  Definition with_payload_round payload_round (r : record) :=
    Build payload_round r.(round).
  Definition with_round round (r : record) :=
    Build r.(payload_round) round.
End Invalid_payload_round.
Definition Invalid_payload_round := Invalid_payload_round.record.

Module Insufficient_locked_round_evidence.
  Record record : Set := Build {
    voting_power : int;
    consensus_threshold : int;
  }.
  Definition with_voting_power voting_power (r : record) :=
    Build voting_power r.(consensus_threshold).
  Definition with_consensus_threshold consensus_threshold (r : record) :=
    Build r.(voting_power) consensus_threshold.
End Insufficient_locked_round_evidence.
Definition Insufficient_locked_round_evidence :=
  Insufficient_locked_round_evidence.record.

Module Invalid_commitment.
  Record record : Set := Build {
    expected : bool;
  }.
  Definition with_expected expected (r : record) :=
    Build expected.
End Invalid_commitment.
Definition Invalid_commitment := Invalid_commitment.record.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block_header.invalid_block_signature" "Invalid block signature"
      "A block was not signed with the expected private key."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Block_hash.t × Signature.public_key_hash) ⇒
            let '(block, pkh) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid signature for block "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ". Expected: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Char_literal "." % char
                          CamlinternalFormatBasics.End_of_format)))))
                "Invalid signature for block %a. Expected: %a.")
              Block_hash.pp_short block
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
              pkh))
      (Data_encoding.obj2
        (Data_encoding.req None None "block" Block_hash.encoding)
        (Data_encoding.req None None "expected"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_block_signature" then
            let '(block, pkh) :=
              cast (Block_hash.t × Signature.public_key_hash) payload in
            Some (block, pkh)
          else None
        end)
      (fun (function_parameter : Block_hash.t × Signature.public_key_hash) ⇒
        let '(block, pkh) := function_parameter in
        Build_extensible "Invalid_block_signature"
          (Block_hash.t × Signature.public_key_hash) (block, pkh)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block_header.invalid_stamp" "Insufficient block proof-of-work stamp"
      "The block's proof-of-work stamp is insufficient"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Insufficient proof-of-work stamp"
                  CamlinternalFormatBasics.End_of_format)
                "Insufficient proof-of-work stamp"))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_stamp" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_stamp" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block_header.invalid_payload_hash" "Invalid payload hash"
      "Invalid payload hash."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t)
            ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid payload hash (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Invalid payload hash (expected: %a, provided: %a).")
              Block_payload_hash.pp_short expected Block_payload_hash.pp_short
              provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Block_payload_hash.encoding)
        (Data_encoding.req None None "provided" Block_payload_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_payload_hash" then
            let '{|
              Invalid_payload_hash.expected := expected;
                Invalid_payload_hash.provided := provided
                |} := cast Invalid_payload_hash payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t) ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Invalid_payload_hash" Invalid_payload_hash
          {| Invalid_payload_hash.expected := expected;
            Invalid_payload_hash.provided := provided; |}) in
  let '_ := tt in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block_header.locked_round_after_block_round"
      "Locked round after block round" "Locked round after block round."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
            let '(locked_round, round) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Locked round ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      ") is after the block round ("
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Locked round (%a) is after the block round (%a).")
              Round_repr.pp locked_round Round_repr.pp round))
      (Data_encoding.obj2
        (Data_encoding.req None None "locked_round" Round_repr.encoding)
        (Data_encoding.req None None "round" Round_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Locked_round_after_block_round" then
            let '{|
              Locked_round_after_block_round.locked_round := locked_round;
                Locked_round_after_block_round.round := round
                |} := cast Locked_round_after_block_round payload in
            Some (locked_round, round)
          else None
        end)
      (fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
        let '(locked_round, round) := function_parameter in
        Build_extensible "Locked_round_after_block_round"
          Locked_round_after_block_round
          {| Locked_round_after_block_round.locked_round := locked_round;
            Locked_round_after_block_round.round := round; |}) in
  let '_ := tt in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block_header.invalid_payload_round" "Invalid payload round"
      "The given payload round is invalid."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
            let '(payload_round, round) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The provided payload round ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      ") is after the block round ("
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "The provided payload round (%a) is after the block round (%a).")
              Round_repr.pp payload_round Round_repr.pp round))
      (Data_encoding.obj2
        (Data_encoding.req None None "payload_round" Round_repr.encoding)
        (Data_encoding.req None None "round" Round_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_payload_round" then
            let '{|
              Invalid_payload_round.payload_round := payload_round;
                Invalid_payload_round.round := round
                |} := cast Invalid_payload_round payload in
            Some (payload_round, round)
          else None
        end)
      (fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
        let '(payload_round, round) := function_parameter in
        Build_extensible "Invalid_payload_round" Invalid_payload_round
          {| Invalid_payload_round.payload_round := payload_round;
            Invalid_payload_round.round := round; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block_header.insufficient_locked_round_evidence"
      "Insufficient locked round evidence" "Insufficient locked round evidence."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : int × int) ⇒
            let '(voting_power, consensus_threshold) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The provided locked round evidence is not sufficient: provided "
                  (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.String_literal
                      " voting power but was expecting at least "
                      (CamlinternalFormatBasics.Int
                        CamlinternalFormatBasics.Int_d
                        CamlinternalFormatBasics.No_padding
                        CamlinternalFormatBasics.No_precision
                        (CamlinternalFormatBasics.Char_literal "." % char
                          CamlinternalFormatBasics.End_of_format)))))
                "The provided locked round evidence is not sufficient: provided %d voting power but was expecting at least %d.")
              voting_power consensus_threshold))
      (Data_encoding.obj2
        (Data_encoding.req None None "voting_power" Data_encoding.int31)
        (Data_encoding.req None None "consensus_threshold" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Insufficient_locked_round_evidence" then
            let '{|
              Insufficient_locked_round_evidence.voting_power := voting_power;
                Insufficient_locked_round_evidence.consensus_threshold :=
                  consensus_threshold
                |} := cast Insufficient_locked_round_evidence payload in
            Some (voting_power, consensus_threshold)
          else None
        end)
      (fun (function_parameter : int × int) ⇒
        let '(voting_power, consensus_threshold) := function_parameter in
        Build_extensible "Insufficient_locked_round_evidence"
          Insufficient_locked_round_evidence
          {| Insufficient_locked_round_evidence.voting_power := voting_power;
            Insufficient_locked_round_evidence.consensus_threshold :=
              consensus_threshold; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block_header.invalid_commitment" "Invalid commitment in block header"
      "The block header has invalid commitment."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (expected : bool) ⇒
            if expected then
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal
                    "Missing seed's nonce commitment in block header."
                    CamlinternalFormatBasics.End_of_format)
                  "Missing seed's nonce commitment in block header.")
            else
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal
                    "Unexpected seed's nonce commitment in block header."
                    CamlinternalFormatBasics.End_of_format)
                  "Unexpected seed's nonce commitment in block header.")))
      (Data_encoding.obj1
        (Data_encoding.req None None "expected" Data_encoding.bool_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_commitment" then
            let '{| Invalid_commitment.expected := expected |} :=
              cast Invalid_commitment payload in
            Some expected
          else None
        end)
      (fun (expected : bool) ⇒
        Build_extensible "Invalid_commitment" Invalid_commitment
          {| Invalid_commitment.expected := expected; |}) in
  Error_monad.register_error_kind Error_monad.Permanent
    "block_header.wrong_timestamp" "Wrong timestamp"
    "Block timestamp not the expected one."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : Time.t × Time.t) ⇒
          let '(block_ts, expected_ts) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Wrong timestamp: block timestamp ("
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    ") not the expected one ("
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Char_literal ")" % char
                        CamlinternalFormatBasics.End_of_format)))))
              "Wrong timestamp: block timestamp (%a) not the expected one (%a)")
            Time.pp_hum block_ts Time.pp_hum expected_ts))
    (Data_encoding.obj2
      (Data_encoding.req None None "block_timestamp" Time.encoding)
      (Data_encoding.req None None "expected_timestamp" Time.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Wrong_timestamp" then
          let '(t1, t2) := cast (Time.t × Time.t) payload in
          Some (t1, t2)
        else None
      end)
    (fun (function_parameter : Time.t × Time.t) ⇒
      let '(t1, t2) := function_parameter in
      Build_extensible "Wrong_timestamp" (Time.t × Time.t) (t1, t2)).

Definition check_signature
  (block : t) (chain_id : Chain_id.t) (key_value : Signature.public_key)
  : M? unit :=
  let check_signature
    (key_value : Signature.public_key) (function_parameter : t) : bool :=
    let '{|
      t.shell := shell;
        t.protocol_data := {|
          protocol_data.contents := contents;
            protocol_data.signature := signature
            |}
        |} := function_parameter in
    let unsigned_header :=
      Data_encoding.Binary.to_bytes_exn None unsigned_encoding (shell, contents)
      in
    Signature.check (Some (to_watermark (Block_header chain_id))) key_value
      signature unsigned_header in
  if check_signature key_value block then
    return? tt
  else
    Error_monad.error_value
      (Build_extensible "Invalid_block_signature"
        (Block_hash.t × Signature.public_key_hash)
        ((hash_value block),
          (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) key_value))).

Definition check_payload_round
  (round : Round_repr.t) (payload_round : Round_repr.t) : M? unit :=
  Error_monad.error_when (Round_repr.op_gt payload_round round)
    (Build_extensible "Invalid_payload_round" Invalid_payload_round
      {| Invalid_payload_round.payload_round := payload_round;
        Invalid_payload_round.round := round; |}).

Definition check_timestamp
  (round_durations : Round_repr.Durations.t) (timestamp : Time_repr.t)
  (round : Round_repr.t) (predecessor_timestamp : Time_repr.t)
  (predecessor_round : Round_repr.t) : M? unit :=
  let? expected_timestamp :=
    Round_repr.timestamp_of_round round_durations predecessor_timestamp
      predecessor_round round in
  if Time_repr.op_eq expected_timestamp timestamp then
    return? tt
  else
    Error_monad.error_value
      (Build_extensible "Wrong_timestamp" (Time_repr.t × Time_repr.t)
        (timestamp, expected_timestamp)).

Module Proof_of_work.
  Definition check_hash
    (hash_value : Block_hash.t) (stamp_threshold : Compare.Uint64.(Compare.S.t))
    : bool :=
    let bytes_value := Block_hash.to_bytes hash_value in
    let word := TzEndian.get_int64 bytes_value 0 in
    Compare.Uint64.(Compare.S.op_lteq) word stamp_threshold.

  Definition check_header_proof_of_work_stamp
    (shell : Block_header.shell_header) (contents : contents)
    (stamp_threshold : Compare.Uint64.(Compare.S.t)) : bool :=
    let hash_value :=
      hash_value
        {| t.shell := shell;
          t.protocol_data :=
            {| protocol_data.contents := contents;
              protocol_data.signature := Signature.zero; |}; |} in
    check_hash hash_value stamp_threshold.

  Definition check_proof_of_work_stamp
    (proof_of_work_threshold : Compare.Uint64.(Compare.S.t)) (block : t)
    : M? unit :=
    if
      check_header_proof_of_work_stamp block.(t.shell)
        block.(t.protocol_data).(protocol_data.contents)
        proof_of_work_threshold
    then
      return? tt
    else
      Error_monad.error_value (Build_extensible "Invalid_stamp" unit tt).
End Proof_of_work.

Definition begin_validate_block_header
  (block_header : t) (chain_id : Chain_id.t) (predecessor_timestamp : Time.t)
  (predecessor_round : Round_repr.t) (fitness : Fitness_repr.t)
  (timestamp : Time.t) (delegate_pk : Signature.public_key)
  (round_durations : Round_repr.Durations.t) (proof_of_work_threshold : int64)
  (expected_commitment : bool) : M? unit :=
  let '{|
    contents.payload_round := payload_round;
      contents.seed_nonce_hash := seed_nonce_hash
      |} := block_header.(t.protocol_data).(protocol_data.contents) in
  let raw_level := block_header.(t.shell).(Block_header.shell_header.level) in
  let? '_ :=
    Proof_of_work.check_proof_of_work_stamp proof_of_work_threshold block_header
    in
  let? level := Raw_level_repr.of_int32 raw_level in
  let? '_ := check_signature block_header chain_id delegate_pk in
  let round := Fitness_repr.round fitness in
  let? '_ := check_payload_round round payload_round in
  let? '_ :=
    check_timestamp round_durations timestamp round predecessor_timestamp
      predecessor_round in
  let? '_ :=
    Fitness_repr.check_except_locked_round fitness level predecessor_round in
  let has_commitment :=
    match seed_nonce_hash with
    | Nonefalse
    | Some _true
    end in
  Error_monad.error_unless
    (Compare.Bool.(Compare.S.op_eq) has_commitment expected_commitment)
    (Build_extensible "Invalid_commitment" Invalid_commitment
      {| Invalid_commitment.expected := expected_commitment; |}).

Inductive checkable_payload_hash : Set :=
| No_check : checkable_payload_hash
| Expected_payload_hash : Block_payload_hash.t checkable_payload_hash.

Definition finalize_validate_block_header
  (block_header_contents : contents) (round : Round_repr.t)
  (fitness : Fitness_repr.t) (checkable_payload_hash : checkable_payload_hash)
  (locked_round_evidence : option locked_round_evidence)
  (consensus_threshold : int) : M? unit :=
  let '{|
    contents.payload_hash := actual_payload_hash;
      contents.seed_nonce_hash := _;
      contents.proof_of_work_nonce := _
      |} := block_header_contents in
  let? '_ :=
    match checkable_payload_hash with
    | No_checkResult.return_unit
    | Expected_payload_hash bph
      Error_monad.error_unless
        (Block_payload_hash.equal actual_payload_hash bph)
        (Build_extensible "Invalid_payload_hash" Invalid_payload_hash
          {| Invalid_payload_hash.expected := bph;
            Invalid_payload_hash.provided := actual_payload_hash; |})
    end in
  let? locked_round :=
    match locked_round_evidence with
    | Nonereturn? None
    |
      Some {|
        locked_round_evidence.preendorsement_round := preendorsement_round;
          locked_round_evidence.preendorsement_count := preendorsement_count
          |} ⇒
      let? '_ :=
        Error_monad.error_when (Round_repr.op_gteq preendorsement_round round)
          (Build_extensible "Locked_round_after_block_round"
            Locked_round_after_block_round
            {|
              Locked_round_after_block_round.locked_round :=
                preendorsement_round;
              Locked_round_after_block_round.round := round; |}) in
      let? '_ :=
        Error_monad.error_when (preendorsement_count <i consensus_threshold)
          (Build_extensible "Insufficient_locked_round_evidence"
            Insufficient_locked_round_evidence
            {|
              Insufficient_locked_round_evidence.voting_power :=
                preendorsement_count;
              Insufficient_locked_round_evidence.consensus_threshold :=
                consensus_threshold; |}) in
      return? (Some preendorsement_round)
    end in
  Fitness_repr.check_locked_round fitness locked_round.