Skip to main content

🪜 Level_repr.v

Proofs

See code, Gitlab , OCaml

These conditions are used on the [Level_repr.level_from_level_raw_with_era] to build a level from an [int] and a [Level_repr.cycle_era]
    Record t (l : Level_repr.t)
           (era : Level_repr.cycle_era) : Prop := {
        level_position :
          (l.(level) -Z era.(Level_repr.cycle_era.first_level) =
            l.(level_position))
          Int32.Valid.t (
              l.(level) -Z era.(Level_repr.cycle_era.first_level));
        cycle :
          (l.(cycle) = era.(Level_repr.cycle_era.first_cycle) +Z
              (l.(level) -Z era.(Level_repr.cycle_era.first_level)) /Z
                 era.(Level_repr.cycle_era.blocks_per_cycle))
          Int32.Valid.t (l.(level) -Z
             era.(Level_repr.cycle_era.first_level))
          Int32.Valid.t
            ((l.(level) -Z era.(Level_repr.cycle_era.first_level)) /Z
               era.(Level_repr.cycle_era.blocks_per_cycle))
          Int32.Valid.t
            (era.(Level_repr.cycle_era.first_cycle) +Z
              (l.(level) -Z era.(Level_repr.cycle_era.first_level)) /Z
                era.(Level_repr.cycle_era.blocks_per_cycle));
        cycle_position :
          (l.(cycle_position) =
            rem (l.(level) -Z era.(Level_repr.cycle_era.first_level))
              era.(Level_repr.cycle_era.blocks_per_cycle))
          Int32.Valid.t
            (rem (l.(level) -Z era.(Level_repr.cycle_era.first_level))
               era.(Level_repr.cycle_era.blocks_per_cycle));
        exoected_commitment :
          (l.(expected_commitment) =
            (rem
               (rem (l.(level) -Z era.(Level_repr.cycle_era.first_level))
                  era.(Level_repr.cycle_era.blocks_per_cycle))
                era.(Level_repr.cycle_era.blocks_per_commitment) =?
              era.(Level_repr.cycle_era.blocks_per_commitment) -Z 1))
          Int32.Valid.t
            (era.(Level_repr.cycle_era.blocks_per_commitment) -Z 1)
          Int32.Valid.t
            (rem
               (rem (l.(level) -Z era.(Level_repr.cycle_era.first_level))
               era.(Level_repr.cycle_era.blocks_per_cycle))
            era.(Level_repr.cycle_era.blocks_per_commitment));
      }.
  End level_from_raw_with_era_invariants.

  Record t (l : Level_repr.t) : Prop := {
    level : Raw_level_repr.Valid.t l.(level);
    level_position : Int32.Valid.t l.(level_position);
    cycle : Int32.Valid.t l.(cycle);
    cycle_position : Int32.Valid.t l.(cycle_position);
  }.
End Valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Level_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma diff_value_eq_zero : l, Level_repr.diff_value l l = 0.
  intro l; unfold Level_repr.diff_value, Raw_level_repr.to_int32.
  autounfold with tezos_z.
  now rewrite Z.sub_diag.
Qed.

Given the [Level_repr.Valid.invariants], [level_from_raw_with_era] reconstruct the same level
Lemma level_from_raw_with_era_id :
   (era : _) (level : Level_repr.t),
    Level_repr.Valid.level_from_raw_with_era_invariants.t level era
    Level_repr.level_from_raw_with_era era era.(Level_repr.cycle_era.first_level)
      level.(Level_repr.t.level) = level.
Proof.
  intros.
  destruct H.
  unfold Level_repr.level_from_raw_with_era.
  destruct level eqn:?. f_equal; simpl in ×.
  { unfold Raw_level_repr.diff_value.
    unfold "-i32".
    rewrite Int32.normalize_identity; easy. }
  { unfold Int32.to_int.
    unfold Raw_level_repr.diff_value.
    unfold Cycle_repr.add.
    unfold "-i32", "/i32", "+i32".
    repeat rewrite Int32.normalize_identity; easy. }
  { unfold Int32.rem. unfold Raw_level_repr.diff_value.
    unfold "-i32". repeat rewrite Int32.normalize_identity; easy. }
  { unfold Int32.rem, Int32.pred, Raw_level_repr.diff_value.
    unfold "-i32".
    repeat rewrite Int32.normalize_identity; easy. }
Qed.

Module Cycle_era.
  Module Valid.
    Import Level_repr.cycle_era.

    Record t (cycle : Level_repr.cycle_era) : Prop := {
      first_level : Raw_level_repr.Valid.t cycle.(first_level);
      first_cycle : Int32.Valid.t cycle.(first_cycle);
      blocks_per_cycle : Int32.Valid.t cycle.(blocks_per_cycle);
      blocks_per_commitment : Int32.Valid.t cycle.(blocks_per_commitment);
    }.
  End Valid.
End Cycle_era.

Lemma cycle_era_encoding_is_valid :
  Data_encoding.Valid.t Cycle_era.Valid.t Level_repr.cycle_era_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.

Module Cycle_eras.
  Module Valid.
    Record t (cycle_eras : list Level_repr.cycle_era) : Prop := {
      can_create :
        match Level_repr.create_cycle_eras cycle_eras with
        | Pervasives.Ok cycle_eras'cycle_eras' = cycle_eras
        | Pervasives.Error _False
        end;
      cycle_era : List.Forall Cycle_era.Valid.t cycle_eras;
    }.
  End Valid.
End Cycle_eras.

[level] is greater than the [cycle_era.first_level]
Module Level_in_era.
  Definition t (level : Level_repr.t) (era : Level_repr.cycle_era)
             : Prop :=
    let raw_level := level.(Level_repr.t.level) in
    raw_level era.(Level_repr.cycle_era.first_level).
End Level_in_era.

[cycle] is greather than [cycle_era.first_cycle]
Module Cycle_in_era.
  Definition t
    (cycle : Cycle_repr.t)
    (era : Level_repr.cycle_era)
    : Prop :=
  cycle era.(Level_repr.cycle_era.first_cycle).
End Cycle_in_era.

Lemma cycle_eras_encoding_is_valid :
  Data_encoding.Valid.t Cycle_eras.Valid.t Level_repr.cycle_eras_encoding.
  Data_encoding.Valid.data_encoding_auto.
  apply cycle_era_encoding_is_valid.
  intros x H; split.
  - apply H.
  - destruct H.
    destruct (Level_repr.create_cycle_eras _); [
      congruence | tauto
    ].
Qed.