🧱 Block_header_repr.v

Proofs

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].

  Record t (x : Block_header_repr.t) : Prop := {
    protocol_data : Protocol_data.Valid.t x.(protocol_data);
    shell : Block_header.shell_header.Valid.t x.(shell);
  }.
End Valid.

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 String.get CoqOfOCaml.String.get Block_header_repr.to_watermark
  Block_header_repr.bytes_of_block_watermark Bytes.of_string cat Bytes.sub
  String.sub Bytes.length 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 bw ⇒ Block_header_repr.to_watermark bw = w
  | None ⇒ True
  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 p ⇒ contents.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 x ⇒ Protocol_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

Lemma check_timestamp_is_valid
  durations time1 round1 time2 round2 :
  letP ? _ := Block_header_repr.check_timestamp
    durations time1 round1 time2 round2 in
  True.
Proof.
Admitted.

The function [begin_validate_block_header] is valid

Lemma begin_validate_block_header_is_valid
  block chain time1 round fitness time2 public_key durations
  i b :
  letP ? _ := Block_header_repr.begin_validate_block_header
    block chain time1 round fitness time2 public_key durations
    i b in
  True.
Proof.
Admitted.

The function [check_signature_is_valid] is valid

Lemma check_signature_is_valid
  block chain_id public_key :
  letP ? _ := Block_header_repr.check_signature
    block chain_id public_key in
  True.
Proof.
Admitted.