🏋️ Fitness_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.String.
Require TezosOfOCaml.Environment.V8.Proofs.TzEndian.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.

Module Valid.
  Import Fitness_repr.t.

  Record t (p : Fitness_repr.t) : Prop := {
    level : Raw_level_repr.Valid.t p.(level);
    locked_round :
      match p.(locked_round) with
      | Some locked_round ⇒
        locked_round < p.(round) ∧ Round_repr.Valid.t locked_round
      | None ⇒ True
      end;
    predecessor_round : Round_repr.Valid.t p.(predecessor_round);
    round : Round_repr.Valid.t p.(round) }.
End Valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Fitness_repr.encoding.
    Data_encoding.Valid.data_encoding_auto.
    intros x H.
    repeat try split; try sauto.
    destruct x.
    destruct locked_round; trivial.
    destruct H.
    autounfold with tezos_z in *; simpl in ×.
    replace (round <=? t) with false by lia; trivial.
Qed.

Lemma create_without_locked_round_is_valid level predecessor_round round :
  Raw_level_repr.Valid.t level →
  Round_repr.Valid.t predecessor_round →
  Round_repr.Valid.t round →
  Valid.t (
    Fitness_repr.create_without_locked_round level predecessor_round round
  ).
  easy.
Qed.

The function [create] is valid.

Lemma create_is_valid level locked_round predecessor_round round :
  Raw_level_repr.Valid.t level →
  Option.Forall Round_repr.Valid.t locked_round →
  Round_repr.Valid.t predecessor_round →
  Round_repr.Valid.t round →
  letP? fitness :=
    Fitness_repr.create level locked_round predecessor_round round in
  Valid.t fitness.
Proof.
  intros; destruct locked_round;
    [|now apply create_without_locked_round_is_valid];
    simpl.
  autounfold with tezos_z; simpl.
  destruct (_ <=? _) eqn:?; simpl; [easy|].
  constructor; simpl; intuition lia.
Qed.

Lemma create_eq level locked_round predecessor_round round :
  Fitness_repr.create level locked_round predecessor_round round =
  let? _ :=
    match locked_round with
    | Some locked_round ⇒
      if locked_round <? round then
        return? tt
      else
        Error_monad.error_value (
          Build_extensible "Locked_round_not_less_than_round"
          Fitness_repr.Locked_round_not_less_than_round
          (Fitness_repr.Locked_round_not_less_than_round.Build
            round locked_round)
        )
    | None ⇒ return? tt
    end in
  return? Fitness_repr.t.Build level locked_round predecessor_round round.
  destruct locked_round; simpl; trivial.
  destruct Round_repr.op_lteq eqn:?, (_ <? _) eqn:?;
    autounfold with tezos_z in *; simpl in *; trivial; lia.
Qed.

Length of [int32_to_bytes].

Axiom int32_to_bytes_length : ∀ (n : int32),
  Bytes.length (Fitness_repr.int32_to_bytes n) = 4.

The function [int32_of_bytes] is valid.

Axiom int32_of_bytes_is_valid : ∀ (b : bytes),
  letP? n := Fitness_repr.int32_of_bytes b in
  Int32.Valid.t n.

[int32_of_bytes] is the inverse of [int32_to_bytes].

Axiom int32_of_bytes_int32_to_bytes : ∀ (n : int32),
  Fitness_repr.int32_of_bytes
    (Fitness_repr.int32_to_bytes n) = return? n.

[int32_to_bytes] is the inverse of [int32_of_bytes].

Axiom int32_to_bytes_int32_of_bytes : ∀ (b : bytes),
  match Fitness_repr.int32_of_bytes b with
  | Pervasives.Ok n ⇒ Fitness_repr.int32_to_bytes n = b
  | Pervasives.Error n ⇒ True
  end.

The function [locked_round_of_bytes] is valid.

Lemma locked_round_of_bytes_is_valid (b : bytes) :
  letP? locked_round := Fitness_repr.locked_round_of_bytes b in
  Option.Forall Round_repr.Valid.t locked_round.
Proof.
  unfold Fitness_repr.locked_round_of_bytes; simpl.
  step; simpl; trivial.
  step; simpl; [|easy].
  assert (H_int32 := TzEndian.get_int32_is_valid b 0).
  assert (H_round := Round_repr.of_int32_is_valid (TzEndian.get_int32 b 0)).
  destruct Round_repr.of_int32; simpl in *; apply H_round; lia.
Qed.

Lemma locked_round_to_bytes_locked_round_of_bytes (b : bytes) :
  String.Int_length.t b →
  match Fitness_repr.locked_round_of_bytes b with
  | Pervasives.Ok locked_round ⇒
    Fitness_repr.locked_round_to_bytes locked_round = b
  | Pervasives.Error _ ⇒ True
  end.
Proof.
  intros H.
  unfold Fitness_repr.locked_round_of_bytes, Bytes.length; rewrite H.
  step; simpl; [rewrite String.length_zero_implies_empty; lia|].
  step; [|easy].
  assert (H_to_of := int32_to_bytes_int32_of_bytes b).
  unfold Fitness_repr.int32_of_bytes, Bytes.length in H_to_of.
  rewrite H in H_to_of.
  revert H_to_of.
  step; simpl.
  { lia. }
  { unfold Round_repr.of_int32, Round_repr.op_gteq.
    hauto l: on.
  }
Qed.

Lemma locked_round_of_bytes_locked_round_to_bytes
  (locked_round : option Round_repr.t) :
    Option.Forall Round_repr.Valid.t locked_round →
    Fitness_repr.locked_round_of_bytes
      (Fitness_repr.locked_round_to_bytes locked_round) = return? locked_round.
Proof.
  destruct locked_round as [round|] eqn:?; simpl; [|reflexivity].
  assert (H := int32_of_bytes_int32_to_bytes round).
  unfold Round_repr.to_int32, Fitness_repr.locked_round_of_bytes.
  unfold Fitness_repr.int32_of_bytes in H.
  rewrite int32_to_bytes_length in *; simpl in ×.
  replace (get_int32 _ _) with round by hauto lq: on.
  unfold Round_repr.of_int32; autounfold with tezos_z; simpl.
  hauto lq: on solve: lia.
Qed.

Lemma predecessor_round_of_bytes_is_valid (b : bytes) :
  letP? locked_round := Fitness_repr.predecessor_round_of_bytes b in
  Round_repr.Valid.t locked_round.
Proof.
  unfold Fitness_repr.predecessor_round_of_bytes.
  specialize (int32_of_bytes_is_valid b); intro.
  destruct Fitness_repr.int32_of_bytes; simpl in *; trivial.
  pose proof (Round_repr.of_int32_is_valid (Int32.pred (Int32.neg i)))
    as H_round.
  destruct Round_repr.of_int32;
    repeat (autounfold with tezos_z in *; unfold normalize_int32 in *);
    try apply H_round;
    lia.
Qed.

Lemma round_of_bytes_is_valid (b : bytes) :
  letP? round := Fitness_repr.round_of_bytes b in
  Round_repr.Valid.t round.
Proof.
  unfold Fitness_repr.round_of_bytes.
  specialize (int32_of_bytes_is_valid b); intro.
  destruct Fitness_repr.int32_of_bytes as [i|]; simpl; trivial.
  specialize (Round_repr.of_int32_is_valid i); intro.
  destruct Round_repr.of_int32; tauto.
Qed.

Lemma from_raw_is_valid (lb : list bytes) :
  letP? fitness := Fitness_repr.from_raw lb in
  Valid.t fitness.
Proof.
  refine (
    match lb with
    | [version; level; locked_round; neg_predecessor_round; round] ⇒ _
    | _ ⇒ _
    end
  ); try easy;
    clear lb; unfold Fitness_repr.from_raw; simpl.
  { now destruct (_ <? _). }
  { destruct (_ =? _) eqn:?; [|easy].
    specialize (int32_of_bytes_is_valid level); intro.
    destruct Fitness_repr.int32_of_bytes as [int32_level|] eqn:?; simpl; trivial.
    specialize (Raw_level_repr.of_int32_is_valid int32_level); intro.
    destruct Raw_level_repr.of_int32 as [raw_level|] eqn:?; [|tauto].
    specialize (locked_round_of_bytes_is_valid locked_round); intro.
    destruct Fitness_repr.locked_round_of_bytes eqn:?; simpl; trivial.
    specialize (predecessor_round_of_bytes_is_valid neg_predecessor_round); intro.
    destruct Fitness_repr.predecessor_round_of_bytes eqn:?; simpl; trivial.
    specialize (round_of_bytes_is_valid round); intro.
    destruct Fitness_repr.round_of_bytes eqn:?; simpl; trivial.
    apply create_is_valid; tauto.
  }
Qed.

Lemma from_raw_to_raw (t : option Fitness_repr.t) :
  Option.Forall Valid.t t →
  match t with
  | Some x ⇒ Fitness_repr.from_raw (Fitness_repr.to_raw x) = return? x
  | _ ⇒ True
  end.
  intros H;
  destruct t eqn:?; [|easy].
  unfold Fitness_repr.to_raw, Fitness_repr.from_raw; simpl;
  rewrite int32_of_bytes_int32_to_bytes; simpl;
  rewrite Raw_level_repr.of_int32_to_int32; simpl; [|sauto lq: on].
  rewrite locked_round_of_bytes_locked_round_to_bytes; simpl; [|sauto lq: on rew: off ].
  unfold Fitness_repr.predecessor_round_of_bytes.
  unfold Fitness_repr.round_of_bytes.
  rewrite int32_of_bytes_int32_to_bytes.
  rewrite int32_of_bytes_int32_to_bytes.
  destruct H, round, predecessor_round, t0; simpl in ×.
  rewrite Int32.pred_neg_pred_neg_inverse;
    [|autounfold with tezos_z in *; lia];
  rewrite Round_repr.of_int32_to_int32;
    [|autounfold with tezos_z in *; lia];
  rewrite Round_repr.of_int32_to_int32;
    [|autounfold with tezos_z in *; lia];
  simpl in ×.
  unfold Fitness_repr.create;
  destruct locked_round0 eqn:?;
  destruct locked_round eqn:?;
  unfold Round_repr.op_lteq; simpl in *;
  try replace (round <=? t0) with false by lia; reflexivity.
Qed.

Lemma to_raw_from_raw (lb : list bytes) :
  match Fitness_repr.from_raw lb with
  | Pervasives.Ok b ⇒ Fitness_repr.to_raw b = lb
  | Pervasives.Error b ⇒ True
  end.
  destruct lb
    as [|version [|level [|locked_round [|neg_predecessor_round [|round []]]]]];
    simpl; trivial; unfold Fitness_repr.from_raw.
  { now destruct (_ <s _). }
  { destruct (_ =s _) eqn:?; simpl; trivial.
    destruct Fitness_repr.int32_of_bytes eqn:?; simpl; trivial.
    destruct Raw_level_repr.of_int32 eqn:?; simpl; trivial.
    destruct Fitness_repr.locked_round_of_bytes eqn:?; simpl; trivial.
    unfold Fitness_repr.predecessor_round_of_bytes.
    destruct Fitness_repr.int32_of_bytes eqn:? in |- *; simpl; trivial.
    destruct Round_repr.of_int32 eqn:?; simpl; trivial.
    unfold Fitness_repr.round_of_bytes.
    destruct Fitness_repr.int32_of_bytes eqn:? in |- *; simpl; trivial.
    destruct Round_repr.of_int32 eqn:? in |- *; simpl; trivial.
    rewrite create_eq.
    match goal with
    | |- context[let? _ := ?e in _] ⇒ destruct e; simpl; trivial
    end.
    unfold Fitness_repr.to_raw; repeat f_equal;
      unfold Raw_level_repr.to_int32, Round_repr.to_int32.
    { unfold Bytes.of_string, Bytes.to_string in ×.
      simpl (_ =s _) in ×.
      symmetry.
      apply String.compare_eq_iff.
      lia.
    }
    { hecrush use: int32_to_bytes_int32_of_bytes. }
    { admit. }
    { unfold Round_repr.of_int32 in ×.
      destruct Round_repr.op_gteq;
        unfold Error_monad.error_value in *; try congruence.
      inversion Heqt3.
      rewrite Int32.pred_neg_pred_neg_inverse.
      { hecrush use: int32_to_bytes_int32_of_bytes. }
      { specialize (int32_of_bytes_is_valid neg_predecessor_round).
        now rewrite Heqt2.
      }
    }
    { hecrush use: int32_to_bytes_int32_of_bytes. }
  }
Admitted.

Lemma round_from_raw_is_valid (lb : list bytes) :
  letP? r := Fitness_repr.round_from_raw lb in
  Round_repr.Valid.t r.
Proof.
  refine (
    match lb with
    | [version; _; _; _; round] ⇒ _
    | _ ⇒ _
    end
  ); simpl; try easy; unfold Fitness_repr.round_from_raw.
  { now destruct (_ <s _). }
  { destruct (_ =s _); simpl; [|easy].
    apply Fitness_repr.round_of_bytes_is_valid.
  }
Qed.

Lemma predecessor_round_from_raw_is_valid (lb : list bytes) :
  letP? r := Fitness_repr.predecessor_round_from_raw lb in
  Round_repr.Valid.t r.
Proof.
  refine (
    match lb with
    | [version; _; _; neg_predecessor_round; _] ⇒ _
    | _ ⇒ _
    end
  ); simpl; try easy; unfold Fitness_repr.predecessor_round_from_raw.
  { now destruct (_ <s _). }
  { destruct (_ =s _); [|easy].
    apply Fitness_repr.predecessor_round_of_bytes_is_valid.
  }
Qed.

Lemma level_is_valid (f : Fitness_repr.t) :
  Valid.t f →
  Raw_level_repr.Valid.t (Fitness_repr.level f).
  dtauto.
Qed.

Lemma round_is_valid (f : Fitness_repr.t) :
  Valid.t f →
  Round_repr.Valid.t (Fitness_repr.round f).
  dtauto.
Qed.

Lemma locked_round_is_valid (f : Fitness_repr.t) :
  Valid.t f →
  Option.Forall Round_repr.Valid.t (Fitness_repr.locked_round f).
  sauto lq: on rew: off.
Qed.

Lemma predecessor_round_is_valid (f : Fitness_repr.t) :
  Valid.t f →
  Round_repr.Valid.t (Fitness_repr.predecessor_round f).
  dtauto.
Qed.

The function [check_locked_round] is valid.

Lemma check_locked_round_is_valid fitness locked_round :
  letP? _ := Fitness_repr.check_locked_round fitness locked_round in
  True.
Proof.
  unfold Fitness_repr.check_locked_round, Error_monad.error_unless.
  now repeat step.
Qed.