Skip to main content

🧱 Block_header_repr.v

Proofs

See code, Gitlab , OCaml

Validity predicate for [Block_header_repr.contents].
  Module Valid.
    Import Proto_alpha.Block_header_repr.contents.

    Record t (x : Block_header_repr.contents) : Prop := {
      payload_round : Round_repr.Valid.t x.(payload_round);
      proof_of_work_nonce :
        Bytes.length x.(proof_of_work_nonce) =
        Constants_repr.proof_of_work_nonce_size;
    }.
  End Valid.
End contents.

Module Protocol_data.
Validity predicate for [Block_header_repr.protocol_data].
  Module Valid.
    Definition t (data : Block_header_repr.protocol_data) : Prop :=
      contents.Valid.t data.(Block_header_repr.protocol_data.contents).
  End Valid.
End Protocol_data.

Module Valid.
  Import Block_header_repr.t.
Validity predicate for [Block_header_repr.t].
Encoding [Block_header_repr.raw_encoding] is valid.
Lemma raw_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Block_header_repr.raw_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve raw_encoding_is_valid : Data_encoding_db.

Encoding [Block_header_repr.shell_header_encoding] is valid.
Lemma shell_header_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Block_header_repr.shell_header_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve shell_header_encoding_is_valid : Data_encoding_db.

Local Hint Unfold
  Bytes.get V7.String.get CoqOfOCaml.String.get Block_header_repr.to_watermark
  Block_header_repr.bytes_of_block_watermark Bytes.of_string cat Bytes.sub
  V7.String.sub Bytes.length V7.String.length CoqOfOCaml.String.length
  : watermark.

When [of_watermark w] returns [Some bw] then [to_watermark bw] must return the same [w].
Lemma to_watermark_of_watermark w :
  match w with
  | Custom bs
      Pervasives.Int.Valid.t
        (Z.pos (Pos.of_succ_nat (Strings.String.length bs) - 1))
  | _True
  end
  match Block_header_repr.of_watermark w with
  | Some bwBlock_header_repr.to_watermark bw = w
  | NoneTrue
  end.
Proof.
  intro Hvalid.
  destruct w as [| | | [|a s]]; simpl; trivial.
  autounfold with watermark in *;
    with_strategy opaque ["++"] simpl.
  destruct a eqn:Ea; do 8 (step; trivial).
  destruct Chain_id.of_bytes_opt eqn:Eobo;
    with_strategy opaque ["++"] simpl; trivial.
  simpl in *; unfold "-i" in ×.
  rewrite Pervasives.normalize_identity in Eobo; [|lia].
  replace
    (Z.to_nat (Z.pos (Pos.of_succ_nat (Strings.String.length s)) - 1))
    with (Strings.String.length s) in × by lia.
  (*rewrite Proofs.String.substring_of_s_l in Eobo;
    rewrite (Proofs.Chain_id.to_bytes_of_bytes_opt Eobo) in *;
    reflexivity.*)

Admitted.

When [to_watermark bw] returns [w] then [of_watermark w] must return the same block [bw].
Lemma of_watermark_to_watermark bw w :
  Block_header_repr.to_watermark bw = w
  (let 'Block_header_repr.Block_header t := bw in
  Pervasives.Int.Valid.t
    (Z.pos
       (Pos.of_succ_nat (Strings.String.length (Chain_id.to_bytes t))) - 1))
  Block_header_repr.of_watermark w = Some bw.
Proof.
  intros H H_valid; destruct bw as [t]; autounfold with watermark in ×.
  rewrite <- H; with_strategy opaque ["++"] simpl.
  (*destruct (_ >i 0) eqn:E;
    [|autounfold with watermark in *; cbn in *; discriminate].
  autounfold with watermark in *; simpl in *; unfold "-i".
  rewrite Pervasives.normalize_identity; [|lia].
  replace
    (Z.to_nat (Z.pos
      (Pos.of_succ_nat (Strings.String.length (Chain_id.to_bytes t))) - 1))
    with (Strings.String.length (Chain_id.to_bytes t)) by lia.
  rewrite String.substring_of_s_l, Chain_id.of_bytes_opt_to_bytes; reflexivity.*)

Admitted.

Encoding [Block_header_repr.contents_encoding] is valid.
Lemma contents_encoding_is_valid :
  Data_encoding.Valid.t contents.Valid.t Block_header_repr.contents_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  sauto lq: on.
Qed.
#[global] Hint Resolve contents_encoding_is_valid : Data_encoding_db.

Encoding [Block_header_repr.protocol_data_encoding] is valid.
Lemma protocol_data_encoding_is_valid :
  Data_encoding.Valid.t
    Protocol_data.Valid.t Block_header_repr.protocol_data_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve protocol_data_encoding_is_valid : Data_encoding_db.

Encoding [Block_header_repr.unsigned_encoding] is valid.
Lemma unsigned_encoding_is_valid :
  Data_encoding.Valid.t
    (fun pcontents.Valid.t (snd p)) Block_header_repr.unsigned_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve unsigned_encoding_is_valid : Data_encoding_db.

Encoding [Block_header_repr.encoding] is valid.
Lemma encoding_is_valid :
  Data_encoding.Valid.t
    (fun xProtocol_data.Valid.t x.(Block_header_repr.t.protocol_data))
    Block_header_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

The function [finalize_validate_block_header] is valid.
Lemma finalize_validate_block_header_is_valid
  block_header_contents round fitness checkable_payload_hash
  locked_round_evidence consensus_threshold :
  letP? _ :=
    Block_header_repr.finalize_validate_block_header
      block_header_contents round fitness checkable_payload_hash
      locked_round_evidence consensus_threshold in
  True.
Proof.
  unfold Block_header_repr.finalize_validate_block_header.
  unfold Error_monad.error_when, Error_monad.error_unless.
  destruct checkable_payload_hash; simpl;
    try destruct locked_round_evidence; simpl;
    repeat match goal with
    | |- context[if ?e then _ else _] ⇒ destruct e eqn:?; simpl
    end;
    try easy;
    apply Fitness_repr.check_locked_round_is_valid.
Qed.

The function [check_timestamp_is_valid] is valid
The function [begin_validate_block_header] is valid
The function [check_signature_is_valid] is valid