🧱 Block_header_repr.v
Translated 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.
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
| None ⇒ false
| 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_check ⇒ Result.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
| None ⇒ return? 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.
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
| None ⇒ false
| 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_check ⇒ Result.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
| None ⇒ return? 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.