Skip to main content

🪜 Level_repr.v

Proofs

See code, Gitlab , OCaml

These conditions are used on the [Level_repr.level_from_raw_with_era] to build a level from an [int] and a [Level_repr.cycle_era] @TODO eliminate the output as a field of the record and prove suitable computation lemma @TODO put outside the Valid module
  Record t (era : Level_repr.cycle_era) (first_level_in_alpha_family level0 :
    Raw_level_repr.raw_level) (output_level : Level_repr.t): Prop := {
    level : Int32.Valid.t level0 output_level.(Level_repr.t.level) = level0 ;
    level_position_in_era : Int32.Valid.non_negative (
    level0 -Z era.(Level_repr.cycle_era.first_level));
    level_position: (level0 -Z first_level_in_alpha_family) =
      output_level.(level_position)
      Int32.Valid.non_negative ( level0 -Z first_level_in_alpha_family);
    cycle : (output_level.(cycle) = era.(Level_repr.cycle_era.first_cycle) +Z
      (level0 -Z era.(Level_repr.cycle_era.first_level)) /Z
        era.(Level_repr.cycle_era.blocks_per_cycle))
      Int32.Valid.t (level0 -Z era.(Level_repr.cycle_era.first_level))
      Int32.Valid.non_negative ((level0 -Z era.(Level_repr.cycle_era.first_level))
        /Z era.(Level_repr.cycle_era.blocks_per_cycle))
      Int32.Valid.non_negative (era.(Level_repr.cycle_era.first_cycle) +Z
        (level0 -Z era.(Level_repr.cycle_era.first_level)) /Z
        era.(Level_repr.cycle_era.blocks_per_cycle));
    cycle_position : (output_level.(cycle_position) =
      rem (level0 -Z era.(Level_repr.cycle_era.first_level))
        era.(Level_repr.cycle_era.blocks_per_cycle))
      Int32.Valid.t (rem (level0 -Z era.(Level_repr.cycle_era.first_level))
          era.(Level_repr.cycle_era.blocks_per_cycle));
    expected_commitment :
      (output_level.(expected_commitment) =
      (rem
          (rem (level0 -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 (level0 -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.

Module Valid.
  Import Level_repr.t.

  Record t (l : Level_repr.t) : Prop := {
@Q what the use of this record?
The encoding [encoding] is valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Level_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros [] H;
    repeat split; cbn; try apply H.
  destruct H; cbn in ×. clear - cycle0. lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma diff_value_eq_zero : l, Level_repr.diff_value l l = 0.
Proof.
  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 @TODO without the forall for uniformity
Lemma level_from_raw_with_era_id :
   (era : _) (level_in_alpha_family level : Raw_level_repr.raw_level)
  (output : Level_repr.t),
    level_from_raw_with_era_invariants.t era
    level_in_alpha_family level output
    Level_repr.level_from_raw_with_era era level_in_alpha_family
      level = return? output.
Proof.
  intros [] level_in_alpha_family level [] [].
  unfold
    Level_repr.level_from_raw_with_era,
    Raw_level_repr.diff_value;
    autounfold with tezos_z; cbn in × ;
  rewrite Int32.normalize_identity by lia.
  step; [|lia].
  unfold Cycle_repr.add;
    autounfold with tezos_z; cbn in ×.
  rewrite !Int32.normalize_identity by lia.
  step; [|lia]; cbn.
  now repeat f_equal.
Qed.

(* @Proto_alpha: [level_from_raw_level_from_raw] is an alias of [..._aux_exn] *)
Lemma level_from_raw_level_from_raw_aux_exn_eq :
  Level_repr.level_from_raw_aux_exn = Level_repr.level_from_raw.
Proof.
  unfold Level_repr.level_from_raw. reflexivity.
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.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.

Module Cycle_eras.
  Module Valid.
@TODO @Q write one's own [isSorted] predicates?
    (* @Q @TODO should we go tack to output [cycles = cycle_eras']
     in the second case? *)

    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;
      each_cycle_era_valid : List.Forall Cycle_era.Valid.t cycle_eras;
    }.
  End Valid.

[get_first_levels (cycle_eras)] outputs the lists of the [first_level]s of the [era]s in [cycle_eras] @TODO to be used with a predicate [is_sorted]
  Fixpoint get_first_levels (cycle_eras : list Level_repr.cycle_era)
  : list Raw_level_repr.t :=
    match cycle_eras with
    | [][]
    | era :: cycle_eras0era.(Level_repr.cycle_era.first_level)
        :: get_first_levels cycle_eras0
  end.

[get_first_levels (cycle_ers)] outputs the lists of the [first_cycle]s of the [era]s in [cycle_eras] @TODO to be used with a predicate [is_sorted]
  Fixpoint get_first_cycles (cycle_eras : list Level_repr.cycle_era)
  : list Cycle_repr.t :=
    match cycle_eras with
    | [][]
    | era :: cycle_eras0era.(Level_repr.cycle_era.first_cycle)
        :: get_first_cycles cycle_eras0
  end.

[ce_aux] is the internal fixpoint of create_cycle_eras] in @Proto_alpha
  Fixpoint ce_aux (era0 : Level_repr.cycle_era)
  (cycle_eras0 : list Level_repr.cycle_era) : M? unit :=
    let '{| Level_repr.cycle_era.first_level := first_level;
    Level_repr.cycle_era.first_cycle := first_cycle |} := era0 in
    match cycle_eras0 with
    | ({| Level_repr.cycle_era.first_level := first_level_of_previous_era;
    Level_repr.cycle_era.first_cycle := first_cycle_of_previous_era
          |} as previous_era) :: even_older_eras
      if (Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
        (Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
      then ce_aux previous_era even_older_eras
      else
        Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
    | []return? tt
  end.

  Lemma unfold_ce_aux (era0 : Level_repr.cycle_era)
  (cycle_eras0 : list Level_repr.cycle_era) :
  ce_aux era0 cycle_eras0 =
  let '{| Level_repr.cycle_era.first_level := first_level;
  Level_repr.cycle_era.first_cycle := first_cycle |} := era0 in
  match cycle_eras0 with
  | ({| Level_repr.cycle_era.first_level := first_level_of_previous_era;
  Level_repr.cycle_era.first_cycle := first_cycle_of_previous_era
        |} as previous_era) :: even_older_eras
    if (Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
      (Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
    then ce_aux previous_era even_older_eras
    else
      Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
  | []return? tt
  end.
  Proof. intros.
    destruct cycle_eras0.
    { reflexivity. }
    { unfold ce_aux. destruct (_ && _); reflexivity. }
  Qed.

Helps unfold [create_cycle_era] *without* using an anonymous fixpoint
  Lemma unfold_create_cycle_era (era0 : Level_repr.cycle_era)
    (cycle_eras0 : list Level_repr.cycle_era) :
    Level_repr.create_cycle_eras (era0 :: cycle_eras0) =
      let? '_ := ce_aux era0 cycle_eras0 in
      return? (era0 :: cycle_eras0).
  Proof.
    intros.
    reflexivity.
  Qed.

When [ce_aux era cycle_eras] is valid, then so is [create_cycle_eras (era :: cycle_eras)] and it [return?]s [(era :: cycle_eras)]
  Lemma ce_aux_valid_implies_create_valid
    (era : Level_repr.cycle_era) (cycle_eras : list Level_repr.cycle_era) :
      letP?relaxed _ := ce_aux era cycle_eras
      in Level_repr.create_cycle_eras (era :: cycle_eras)
          = return? (era :: cycle_eras).
  Proof.
    intros. destruct (ce_aux era cycle_eras) eqn:res0 ; hnf ;
    [rewrite unfold_create_cycle_era ; rewrite res0; reflexivity |
      constructor].
  Qed.

When [Level_repr.create_cycle_eras] is valid, so is [ce_aux] and it [return?]s [tt]
  Lemma create_valid_implies_ce_aux_valid (era : Level_repr.cycle_era)
  (cycle_eras : list Level_repr.cycle_era) :
    letP?relaxed _ := Level_repr.create_cycle_eras (era :: cycle_eras)
    in ce_aux era cycle_eras = return? tt.
  Proof.
    intros.
    destruct (ce_aux era cycle_eras) eqn:res0 ; hnf;
      rewrite unfold_create_cycle_era; rewrite res0 ; hnf;
      [apply f_equal ; destruct u ; reflexivity| constructor ].
  Qed.

(* When [create_cycles_eras] is valid, it outputs its parameter *)
  Lemma valid_create_cycle_era_outputs_input
    (cycle_eras l : list Level_repr.cycle_era) :
    Level_repr.create_cycle_eras (cycle_eras) = V0.Pervasives.Ok l
       l = cycle_eras.
  Proof.
    intros.
    destruct cycle_eras as [ | era0 ce0].
    { inversion H. }
    { specialize (create_valid_implies_ce_aux_valid era0 ce0) as H1.
      rewrite H in H1. hnf in H1.
      specialize (ce_aux_valid_implies_create_valid era0 ce0) as H2.
      rewrite H1 in H2. hnf in H2. unfold "return?" in H2.
      rewrite H in H2. inversion H2. reflexivity. }
  Qed.

When [cycle_eras] is valid then [Level_repr.create_cycle_eras cycle_eras] [return?]s [cycle_eras]
  Lemma valid_cycle_eras_implies_valid_cycle_create
  (cycle_eras : list Level_repr.cycle_era): Valid.t cycle_eras
     Level_repr.create_cycle_eras cycle_eras = V0.Pervasives.Ok cycle_eras.
  Proof.
    intros. destruct H.
    destruct (Level_repr.create_cycle_eras cycle_eras) eqn:res.
    { apply valid_create_cycle_era_outputs_input in res. apply f_equal.
      assumption. }
    { contradiction. }
  Qed.

When [cycle_eras] is valid then [Level_repr.create_cycle_eras cycle_eras] [return?]s [cycle_eras]
  Lemma valid_cycle_eras_implies_valid_ce_aux (era : Level_repr.cycle_era)
  (ce : list Level_repr.cycle_era): Valid.t (era :: ce)
     ce_aux era ce = V0.Pervasives.Ok tt.
  Proof.
    intros. destruct H.
    destruct (Level_repr.create_cycle_eras (era :: ce)) eqn:res0.
    { specialize (create_valid_implies_ce_aux_valid era ce) as res1.
     rewrite res0 in res1; hnf in res1. assumption. }
    { contradiction. }
  Qed.

  (* @TODO :
    1. rename
    2. spec *)

  Lemma valid_inductive_step_aux1 : (era0 era1 : Level_repr.cycle_era)
    (cycle_eras : list Level_repr.cycle_era),
    letP?relaxed _ := Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)
    in (Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level)
        era1.(Level_repr.cycle_era.first_level) = true)
      Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle)
        era1.(Level_repr.cycle_era.first_cycle) = true.
  Proof.
    intros.
    destruct (Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras))
    eqn:res ; simpl.
    { unfold Level_repr.create_cycle_eras in res.
      destruct (_ && _) eqn:cond_val in res.
      { rewrite Bool.andb_true_iff in cond_val. tauto. }
      { inversion res. } }
    { constructor. }
  Qed.

(* @TODO :
    1. rename
    2. spec *)

  Lemma valid_inductive_step_aux2 : (era0 era1 : Level_repr.cycle_era)
    (cycle_eras : list Level_repr.cycle_era),
    letP?relaxed _ := Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)
     in Level_repr.create_cycle_eras (era1 :: cycle_eras) =
        V0.Pervasives.Ok (era1 :: cycle_eras) .
  Proof.
    intros.
    destruct (Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)) eqn:res.
    { hnf. destruct (ce_aux era1 cycle_eras) eqn:ce_aux0.
      { rewrite unfold_create_cycle_era. hnf. rewrite ce_aux0. simpl.
        unfold "return?". reflexivity. }
      { rewrite unfold_create_cycle_era. rewrite ce_aux0. simpl.
        specialize (create_valid_implies_ce_aux_valid era0 (era1 :: cycle_eras))
        as H2 ; rewrite res in H2 ; hnf in H2.
        assert (H3: ce_aux era1 cycle_eras = V0.Pervasives.Ok tt).
        { inversion H2. destruct ( _ && _ ) eqn:bool_cond in H0.
          { assumption. } { inversion H0. } }
        rewrite H3 in ce_aux0. inversion ce_aux0. } }
    { constructor. }
  Qed.

  Lemma valid_inductive_step : (cycle_eras : list Level_repr.cycle_era),
    match cycle_eras with
    | era0 :: era1 :: cycle_eras1
      Valid.t cycle_eras
        (Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level)
        era1.(Level_repr.cycle_era.first_level) = true
        Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle)
        era1.(Level_repr.cycle_era.first_cycle) = true
        Cycle_era.Valid.t era0
         Valid.t (era1 :: cycle_eras1) )
    | [era]Cycle_era.Valid.t era Valid.t [era]
    | []Valid.t cycle_eras False
  end.
  Proof.
    (* destruct cycle_eras as [ | era0  ce0 ]. *)
    destruct cycle_eras as [ | era0 [ | era1 ce1 ]].
    { split ; intro H. { inversion H; compute in *; assumption. } { exfalso ;
    assumption. }}
    { split ; intro H.
      { constructor ; constructor. {apply H. } {constructor. } }
      { destruct H eqn:H0. inversion each_cycle_era_valid. assumption. } }
    { split ; intro H.
      { specialize (valid_inductive_step_aux1 era0 era1 ce1) as bool_cond.
        specialize (valid_inductive_step_aux2 era0 era1 ce1) as val_cond.
        destruct H.
        destruct (Level_repr.create_cycle_eras (era0 :: era1 :: ce1))
        eqn:res_create. destruct bool_cond as [level_cond cycle_cond].
        { assert (era0_valid : Cycle_era.Valid.t era0).
          { inversion each_cycle_era_valid. assumption. }
          destruct era0_valid as
          [era0_f_level era0_f_cycle era0_b_p_cycles era0_b_p_commit].
          destruct era0_f_level as [era0_fl1 era0_fl2].
          destruct era0_f_cycle as [era0_fc1 era0_fc2].
          destruct era0_b_p_cycles as [era0_bpcy1 era0_bpcy2].
          destruct era0_b_p_commit as [era0_bpco1 era0_bpco2].
          repeat split; try assumption.
          { hnf in val_cond. rewrite val_cond. constructor. }
          { inversion each_cycle_era_valid. assumption. }
        }
        { contradiction. } }
    { destruct H as [H1 [H2 [H3 H4]]].
      constructor.
      { rewrite unfold_create_cycle_era.
        apply valid_cycle_eras_implies_valid_ce_aux in H4.
        assert (H5: ce_aux era0 (era1 :: ce1) = V0.Pervasives.Ok tt).
        { rewrite unfold_ce_aux. cbn. destruct ( _ && _ ) eqn:H6.
          { assumption. }
          { exfalso. assert (H7: era0.(Level_repr.cycle_era.first_level) >?
              era1.(Level_repr.cycle_era.first_level)= true). { assumption. }
            assert (H8: era0.(Level_repr.cycle_era.first_cycle) >?
            era1.(Level_repr.cycle_era.first_cycle) = true). { assumption. }
            destruct era0. destruct era1. simpl in ×.
            rewrite H7 in H6. rewrite H8 in H6. inversion H6.
          } } (*** @TODO assert H5 should probably be a lemma *)
        rewrite H5; constructor. }
      { constructor; [ assumption |destruct H4 ; assumption ].
      }
    }
  }
  Qed.

a valid [cycle_eras] is non-empty.
  Lemma valid_cycle_eras_non_empty : (cycle_eras : list
  Level_repr.cycle_era), Valid.t cycle_eras cycle_eras [].
  Proof.
    unfold "~". intros. rewrite H0 in H. assert
    (H1 := (valid_inductive_step [])) ; simpl in H1.
    apply H1. apply H.
  Qed.

if [cycle_eras] is valid, then the [first_level] and [first_cycle] of its first [era] are greater than those of its last one, meaning than the last [era] is more ancient than the first one.
  Lemma valid_implies_first_gt_last : (cycle_eras : list
    Level_repr.cycle_era), let rev_c_e := rev cycle_eras in
    Valid.t cycle_eras match cycle_eras with
    | era0 :: _match rev_c_e with
      | last_era :: _
          Raw_level_repr.op_gteq
            era0.(Level_repr.cycle_era.first_level)
            last_era.(Level_repr.cycle_era.first_level) = true
          Cycle_repr.op_gteq
            era0.(Level_repr.cycle_era.first_cycle)
            last_era.(Level_repr.cycle_era.first_cycle) = true
      | []False
      end
    | []False
  end.
  Proof.
    induction cycle_eras as [ | era0 ce0 H].
    { simpl. intro H. apply valid_cycle_eras_non_empty in H. apply H.
      reflexivity. }
    { simpl in H. destruct ce0 as [ | era1 ce1].
      { simpl. intro. split ; lia. }
      { specialize (valid_inductive_step (era0 :: era1 ::ce1)) as ind_step ;
      hnf in ind_step.
      simpl. intro val_cond. apply ind_step in
      val_cond. clear ind_step.
      unfold rev, rev' in *; simpl in ×.
      destruct val_cond as [H1 [H2 [H3 H4]]].
      apply H in H4. clear H.
      simpl.
      destruct (Lists.List.rev_append ce1 [era1]) eqn:rev_ce0.
      { contradiction. }
      { destruct (Lists.List.rev_append ce1 [era1; era0]) eqn:rev_ce.
        specialize (List.rev_append_not_empty2 ce1 [era1; era0]) as contrad.
        apply contrad. { intro. inversion H. } { assumption. }
        assert (H5 : c0 = c).
        { specialize (@List.same_last_element_rev_append Level_repr.cycle_era
          era1 [ ] [era0] ce1)
          as H6.
          rewrite rev_ce0 in H6. rewrite rev_ce in H6.
          inversion H6. reflexivity.
        }
        subst. lia.
      }
    }
  }
  Qed.

@TODO : prove the full decreasing pre-condition of valid [cycle_eras]
  (* Lemma valid_implies_sorted_levels_and_cyles : forall (cycle_eras
     : list Level_repr.cycle_era),
     Valid.t cycle_eras <-> list Level_repr.cycle_era
     (Sorted.Sorted (fun l1 l2 =>
        (Raw_level_repr.op_gt
        l1 l2 = true))). *)


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 greater 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.
Proof.
  apply cycle_era_encoding_is_valid.
  intros x H; split.
  - apply H.
  - destruct H.
    destruct (Level_repr.create_cycle_eras _); [
      congruence | tauto ].
Qed.

The function [first_level_in_cycle_from_eras] is valid.
Lemma first_level_in_cycle_from_eras_is_valid cycle_eras cycle :
  Cycle_eras.Valid.t cycle_eras
  Cycle_repr.Valid.t cycle
  letP? level := Level_repr.first_level_in_cycle_from_eras cycle_eras cycle in
  Valid.t level.
Proof.
  (* intros.
  destruct (Level_repr.first_level_in_cycle_from_eras cycle_eras cycle) eqn:res.
  { unfold Level_repr.first_level_in_cycle_from_eras in res. admit. }
  { admit. } *)

Admitted.

The function [create_cycle_eras] is valid
Lemma create_cycle_eras_is_valid cs :
  cs []
  letP? cs' := Level_repr.create_cycle_eras cs in
  cs' = cs.
Proof.
  intros.
  induction cs; cbn.
  { contradiction. }
  { destruct cs; cbn; [easy|].
    step; cbn; [|reflexivity].
    match goal with
    | |- context [
          let? ' _ := ?f' _ _ in _] ⇒
        set (aux := f')
    end.
    intros.
    destruct (aux c cs) eqn:?; cbn; [easy|].
    assert (H_aux_is_valid : e c cs, aux c cs =
      Pervasives.Error e
      Error.not_internal e).
    { clear.
      intros ? ? ?.
      subst aux.
      generalize c.
      induction cs; [discriminate|].
      intros ?.
      step; cbn.
      { apply IHcs. }
      { inj. subst e. reflexivity. }
    }
    now apply H_aux_is_valid in Heqt.
  }
Qed.

Predicate stating that [level] belongs to [cycle_eras]
Module level_belongs_to_cycle_eras.
  Module Valid.
    Fixpoint t (cycle_eras : list Level_repr.cycle_era)
      (raw_level : Z.t) : Prop :=
      match cycle_eras with
      | []False
      | cycle_era :: cycle_eras
          raw_level cycle_era.(Level_repr.cycle_era.first_level)
            t cycle_eras raw_level
      end.
  End Valid.
End level_belongs_to_cycle_eras.

The function [era_of_level] is valid
Lemma era_of_level_is_valid cycle_eras raw_level :
  List.Forall Level_repr.Cycle_era.Valid.t cycle_eras
  level_belongs_to_cycle_eras.Valid.t cycle_eras raw_level
  Raw_level_repr.Valid.t raw_level
  letP? era := Level_repr.era_of_level cycle_eras raw_level in
  Level_repr.Cycle_era.Valid.t era
    era.(Level_repr.cycle_era.first_level) raw_level.
Proof.
  intros H_cycle_eras' H_cycle_eras H_level.
  red in H_cycle_eras.
  induction cycle_eras.
  { contradiction. }
  { destruct H_cycle_eras.
    { cbn.
      replace (_ >=? _) with true
        by (destruct a; cbn in *; lia).
      cbn. split_conj.
      { now inversion H_cycle_eras'. }
      { lia. }
    }
    { cbn.
      step.
      { cbn. split.
        { now inversion H_cycle_eras'. }
        { destruct a; cbn in ×.
          { lia. }
        }
      }
      { apply IHcycle_eras.
        { now inversion H_cycle_eras'. }
        { easy. }
      }
    }
  }
Qed.

The function [level_from_raw_with_era] is valid
Lemma level_from_raw_with_era_is_valid cycle_era
  first_level_in_alpha_family level output_level :
  Level_repr.level_from_raw_with_era_invariants.t cycle_era
    first_level_in_alpha_family level output_level
  Level_repr.Cycle_era.Valid.t cycle_era
  Raw_level_repr.Valid.t first_level_in_alpha_family
  Raw_level_repr.Valid.t level
  cycle_era.(Level_repr.cycle_era.first_level) level
  letP? ' y := Level_repr.level_from_raw_with_era
    cycle_era first_level_in_alpha_family level in
  Level_repr.Valid.t y.
Proof.
  intros.
  unfold Level_repr.level_from_raw_with_era.
  rewrite Raw_level_repr.diff_value_is_non_negative;
    [|try easy || apply H..].
  eapply Error.split_letP with (P := Cycle_repr.Valid.t); [|intros]. {
    unfold Int32.to_int.
    unfold Raw_level_repr.diff_value, "/i32", "-i32".
    destruct H.
    unfold Cycle_repr.add; cbn.
    repeat rewrite Int32.normalize_identity;
      Tactics.destruct_conjs.
    { red in H10. unfold "-Z", "/Z" in H10.
      match goal with
      | |- context [if ?e then _ else _] ⇒
          set (cond := e)
      end.
      assert (H_cond_pos : cond = true) by
        (subst cond; destruct cycle_era; cbn in *; lia).
      rewrite H_cond_pos.
      cbn.
      unfold "+i32".
      rewrite Int32.normalize_identity.
      { lia. }
      { clear - H11.
        unfold "-Z", "/Z", "+Z" in H11.
        revert H11.
        apply Int32.non_negative_impl_t.
      }
    }
    { unfold "-Z", "/Z", "+Z" in ×.
      revert H10.
      apply Int32.non_negative_impl_t.
    }
    { easy. }
    { unfold "-Z", "/Z" in H10.
      clear - H10. revert H10.
      apply Int32.non_negative_impl_t.
    }
    { easy. }
  }
  { destruct H. cbn.
    split; cbn; try easy; unfold Raw_level_repr.diff_value; lia.
  }
  { destruct H0. easy. }
Qed.

The function [level_from_raw] is valid
Lemma level_from_raw_is_valid cycle_eras raw_level
  (output_level : Level_repr.t) :
  List.Forall Level_repr.Cycle_era.Valid.t cycle_eras
  level_belongs_to_cycle_eras.Valid.t cycle_eras raw_level
  Raw_level_repr.Valid.t raw_level
  letP? level := Level_repr.level_from_raw cycle_eras raw_level in
  Level_repr.Valid.t level.
Proof.
  intros H_Forall H_cycle_eras H_raw_level **.
  unfold Level_repr.level_from_raw,
    Level_repr.level_from_raw_aux_exn.
  induction cycle_eras as [|cycle_era cycle_eras IHcycle_eras]
    using rev_ind; [contradiction|].
  rewrite List.rev_eq.
  rewrite rev_unit.
  cbn.
  eapply Error.split_letP. {
    now apply Level_repr.era_of_level_is_valid.
  }
  intros era_of_level [H H']. cbn in ×.
  pose proof Level_repr.level_from_raw_with_era_is_valid era_of_level
     cycle_era.(Level_repr.cycle_era.first_level) raw_level
    output_level as H_from_raw.
  destruct (Level_repr.level_from_raw_with_era _ _ _) eqn:?; cbn in ×.
  { apply H_from_raw; try easy.
    { (* @TODO
         Level_repr.level_from_raw_with_era_invariants.t era_of_level
         cycle_era.(Level_repr.cycle_era.first_level) raw_level
         output_level
       *)

      admit.
    }
    { apply List.Forall_app in H_Forall.
      destruct H_Forall as [_ H_Forall].
      inversion H_Forall as [].
      destruct_by_type (Level_repr.Cycle_era.Valid.t _);
        cbn in ×.
      easy.
    }
  }
  { eapply Error.is_valid_impl_not_internal; [|solve [eauto]].
    apply Level_repr.level_from_raw_with_era_is_valid
      with (output_level := output_level); try easy.
    { (* @TODO Level_repr.level_from_raw_with_era_invariants.t
            era_of_level cycle_era.(Level_repr.cycle_era.first_level)
            raw_level output_level *)

      admit.
    }
    { apply List.Forall_app in H_Forall.
      destruct H_Forall as [_ H_Forall].
      inversion H_Forall as [].
      destruct_by_type (Level_repr.Cycle_era.Valid.t _);
        cbn in ×. easy.
    }
  }
Admitted.

The function [root_level] is valid
The function [last_of_cycle] is valid
The [raw_level] passed to [level_from_raw] is present in the returned level