Skip to main content

🪜 Level_storage.v

Proofs

See code, Gitlab , OCaml

The [level] is in the context cycle_eras
  Definition t (ctxt : Proto_alpha.Raw_context.t)
    (raw_level : Raw_level_repr.t) :=
    Raw_context.Valid.on
      (fun sim_ctxt
        Level_repr.level_belongs_to_cycle_eras.Valid.t
          sim_ctxt.(Raw_context.config)
            .(Raw_context_aux.config.cycle_eras)
          raw_level)
      ctxt.

Given the context [cycle_eras], if [l] belongs to the [cycle_eras] and [l <= l'], then [l'] belongs to the [cycle_era] too.
  Lemma le_impl_t ctxt l l' :
    l l'
    t ctxt l
    t ctxt l'.
  Proof.
    intros H_le H_ctxt. cbn in ×.
    Raw_context.Valid.destruct_rewrite H_ctxt.
    unfold Raw_context.Valid.on.
     sim_ctxt. intros.
    split_conj; [easy..|].
    induction sim_ctxt.(Raw_context.config)
      .(Raw_context_aux.config.cycle_eras)
      as [|cycle_era cycle_eras IHcycle_eras].
    { contradiction. }
    { cbn in ×.
      destruct H_sim_ctxt_domain.
      { left.
        clear - H_le H.
        destruct cycle_era; cbn in ×.
        apply Z.le_ge.
        apply Z.ge_le in H.
        lia.
      }
      { right.
        now apply IHcycle_eras.
      }
    }
  Qed.
End Valid.

The function [from_raw] is valid.
Lemma from_raw_is_valid ctxt level :
  Valid.t ctxt level
  Raw_level_repr.Valid.t level
  letP? level := Level_storage.from_raw ctxt level in
  Level_repr.Valid.t level.
Proof.
  intros H_ctxt H_level.
  unfold Level_storage.from_raw.
  pose proof (Level_repr.level_from_raw_is_valid
    (Raw_context.cycle_eras ctxt) level)
    as H_from_raw.
  destruct (Level_repr.level_from_raw _ _);
    Raw_context.Valid.destruct_rewrite H_ctxt.
  { cbn in ×. apply H_from_raw.
     { hauto l: on. }
     { now destruct H_sim_ctxt, config, cycle_eras. }
     { easy. }
     { easy. }
  }
  { cbn in ×. apply H_from_raw.
     { hauto l: on. }
     { now destruct H_sim_ctxt, config, cycle_eras. }
     { easy. }
     { easy. }
  }
Qed.

The raw level [from_raw] passed as argument to [from_raw] is inside the returned level
Lemma from_raw_eq ctxt raw_level :
  Valid.t ctxt raw_level
  Raw_level_repr.Valid.t raw_level
  letP? level := Level_storage.from_raw ctxt raw_level in
  level.(Level_repr.t.level) = raw_level.
Proof.
  intros H_ctxt H_raw_level.
  unfold Level_storage.from_raw.
  apply Level_repr.level_from_raw_eq; [|easy].
  unfold Valid.t in ×.
  Raw_context.Valid.destruct_rewrite H_ctxt.
  now destruct H_sim_ctxt, config.
Qed.

[from_raw_with_offset] returns a valid level
[root_value] level is valid
Lemma root_value_is_valid : {ctxt} l,
  Int32.Valid.t Cycle_repr.root_value
  Raw_level_repr.Valid.t l.(Level_repr.cycle_era.first_level)
  last_opt (Raw_context.cycle_eras ctxt) = Some l
  letP? lsrv := Level_storage.root_value ctxt in
  Level_repr.Valid.t lsrv.
Proof.
  intros.
  unfold Level_storage.root_value.
  unfold Level_repr.root_level.
  unfold "letP? ' _ := _ in _".
  unfold "let? ' _ := _ in _".
  now rewrite H1.
Qed.

The function [succ] is valid.
Lemma succ_is_valid ctxt level :
  Valid.t ctxt level.(Level_repr.t.level)
  Level_repr.Valid.t level
  Raw_level_repr.Valid.t (level.(Level_repr.t.level) +Z 1)
  letP? level := Level_storage.succ ctxt level in
  Level_repr.Valid.t level.
Proof.
  intros H_ctxt H_level H_raw_level.
  unfold Level_storage.succ.
  apply Level_storage.from_raw_is_valid.
  { set (s := Raw_level_repr.succ _).
    assert (H_lt : level.(Level_repr.t.level) < s).
    { subst s.
      unfold Raw_level_repr.succ, Int32.succ. lia.
    }
    pose (level' := level.(Level_repr.t.level)).
    pose proof Valid.le_impl_t ctxt level' s as H_ctxt'.
    apply H_ctxt'.
    { lia. }
    { easy. }
  }
  { apply Raw_level_repr.succ_is_valid.
    apply H_level.
  }
Qed.

[succ] is equivalent to [Z.succ]
Lemma succ_eq (ctxt : Proto_alpha.Raw_context.t)
  (level : Level_repr.t) :
  Valid.t ctxt level.(Level_repr.t.level)
  Raw_level_repr.Valid.t (level.(Level_repr.t.level) +Z 1)
  Level_repr.Valid.t level
  letP? l' := Level_storage.succ ctxt level in
  let raw_level1 := level.(Level_repr.t.level) in
  let raw_level2 := l'.(Level_repr.t.level) in
  raw_level2 = Z.succ raw_level1.
Proof.
  intros H_ctxt H_int H_level.
  unfold Level_storage.succ,
    Raw_level_repr.succ,
    Int32.succ,
    "+i32" in ×.
  rewrite Int32.normalize_identity; [|lia].
  pose proof Level_storage.from_raw_eq ctxt
    (level.(Level_repr.t.level) +Z 1)
    as H_from_raw.
  fold Z.add.
  destruct (Level_storage.from_raw _ _) eqn:?;
    apply H_from_raw; try easy;
    apply (Valid.le_impl_t ctxt level.(Level_repr.t.level)
      (level.(Level_repr.t.level) +Z 1) ltac:(lia) ltac:(assumption)).
Qed.

The function [pred] is valid.
Lemma pred_is_valid ctxt level :
  Valid.t ctxt (level.(Level_repr.t.level) -Z 1)
  Level_repr.Valid.t level
  letP? level := Level_storage.pred ctxt level in
  Option.Forall Level_repr.Valid.t level.
Proof.
  intros ? H_level. unfold Level_storage.pred.
  destruct H_level.
  pose proof @Raw_level_repr.pred_is_valid level.(Level_repr.t.level)
    ltac:(assumption) as H_pred.
  destruct (Raw_level_repr.pred _) as [pred_level|]; [|easy].
  Tactics.destruct_conjs.
  subst pred_level.
  eapply Error.split_letP with (P := Level_repr.Valid.t); [|intros]. {
    now apply from_raw_is_valid.
  }
  easy.
Qed.

[preq] is equivalent to [Z.pred] on positives
Lemma pred_eq
  (ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t) :
  Int32.Valid.t (level.(Level_repr.t.level) - 1)
  Valid.t ctxt (level.(Level_repr.t.level) - 1)
  Level_repr.Valid.t level
  letP? lsc := Level_storage.pred ctxt level in
  match lsc with
  | Some l
      let raw_level1 := level.(Level_repr.t.level) in
      let raw_level2 := l.(Level_repr.t.level) in
      raw_level2 = Int32.pred raw_level1
  | NoneTrue
  end.
Proof.
  intros ? H_ctxt H_level.
  unfold Level_storage.pred.
  unfold Raw_level_repr.pred.
  destruct (Raw_level_repr.op_eq _ _) eqn:?; [easy|].
  assert (H_pos : Raw_level_repr.Valid.t
    (level.(Level_repr.t.level) - 1)).
  { destruct level, H_level; cbn in ×.
    lia.
  }
  unfold Int32.pred, "-i32".
  rewrite Int32.normalize_identity by assumption.
  pose proof Level_storage.from_raw_eq ctxt
    (level.(Level_repr.t.level) - 1) H_ctxt H_pos
    as H_from_raw.
  now destruct (Level_storage.from_raw _ _).
Qed.

[current] level is valid
Lemma current_is_valid ctxt :
  Raw_context.Valid.t ctxt
  Level_repr.Valid.t (Level_storage.current ctxt).
Proof.
  intros H.
  Raw_context.Valid.destruct_rewrite H.
  dtauto.
Qed.

The function [add] is valid.
Lemma add_is_valid ctxt level n :
  Valid.t ctxt level.(Level_repr.t.level)
  Level_repr.Valid.t level
  Pervasives.Int.Valid.positive n
  letP? level := Level_storage.add ctxt level n in
  Level_repr.Valid.t level.
Proof.
  intros H_ctxt H_level H_n.
  unfold Level_storage.add.
  destruct H_level.
  pose proof Raw_level_repr.add_eq level.(Level_repr.t.level) n
    as H_add.
  repeat specialize (H_add ltac:(assumption || lia)).
  pose proof Raw_level_repr.add_is_valid level.(Level_repr.t.level) n
    as H_add'.
  repeat specialize (H_add' ltac:(assumption || lia)).
  step; cbn in *; [|easy]. subst i.
  apply from_raw_is_valid; [|easy].
  apply (Valid.le_impl_t ctxt level.(Level_repr.t.level)
      (level.(Level_repr.t.level) +Z n)); [lia|easy].
Qed.

[add] is equivalent to [+Z]
Lemma add_eq (ctxt : Proto_alpha.Raw_context.t) (l : Level_repr.t)
  (i : Int32.t) :
  Valid.t ctxt l.(Level_repr.t.level)
  Int32.Valid.positive i
  Level_repr.Valid.t l
  Raw_level_repr.Valid.t (l.(Level_repr.t.level) +Z i)
  letP? l' := Level_storage.add ctxt l i in
  let raw_level1 := l.(Level_repr.t.level) in
  let raw_level2 := l'.(Level_repr.t.level) in
  raw_level2 = raw_level1 +Z i.
Proof.
  intros H_ctxt Hint Hlevel Hint_level.
  unfold Level_storage.add.
  eapply Error.split_letP. {
    apply Raw_level_repr.add_eq.
    { apply Hlevel. }
    { lia. }
  }
  intros raw_level H_raw_level. cbn in ×.
  subst raw_level.
  pose proof (Level_storage.from_raw_eq ctxt
    (l.(Level_repr.t.level) +Z i)) as H_from_raw.
  pose proof (Level_storage.from_raw_is_valid ctxt
    (l.(Level_repr.t.level) +Z i)) as H_from_raw'.
  destruct (Level_storage.from_raw _ _).
  { apply H_from_raw; [|assumption].
    apply (Valid.le_impl_t ctxt l.(Level_repr.t.level)
     (l.(Level_repr.t.level) +Z i) ltac:(lia) ltac:(assumption)).
  }
  { cbn in ×. apply H_from_raw'; try easy.
    apply (Valid.le_impl_t ctxt l.(Level_repr.t.level)
      (l.(Level_repr.t.level) +Z i) ltac:(lia) ltac:(assumption)).
  }
Qed.

The function [sub] is valid.
Lemma sub_is_valid ctxt level n :
  Pervasives.Int.Valid.t n
  Raw_level_repr.Valid.t (level.(Level_repr.t.level))
  Raw_level_repr.Valid.t (level.(Level_repr.t.level) -Z n)
  Valid.t ctxt (level.(Level_repr.t.level) -Z n)
  letP? level := Level_storage.sub ctxt level n in
  Option.Forall Level_repr.Valid.t level.
Proof.
  intros H_n H_level H_level' H_ctxt.
  unfold Level_storage.sub.
  eapply Error.split_letP. {
    apply Raw_level_repr.sub_eq; [|easy].
    apply H_level.
  }
  intros opti32 H_opt; cbn in ×.
  step; [|easy].
  injection H_opt as H_i. subst i.
  eapply Error.split_letP. {
    apply Level_repr.root_level_is_valid.
    Raw_context.Valid.destruct_rewrite H_ctxt.
    cbn in ×.
    now destruct H_sim_ctxt, config.
  }
  intros level'' H_level''.
  step; [|easy].
  eapply Error.split_letP. {
    now apply from_raw_is_valid.
  } easy.
Qed.

[sub] is equivalent to [-Z]
Lemma sub_eq (ctxt : Proto_alpha.Raw_context.t)
  (l : Level_repr.t) (i : Int32.t) :
  Pervasives.Int.Valid.t i
  Valid.t ctxt (l.(Level_repr.t.level) -Z i)
  Int32.Valid.t (l.(Level_repr.t.level) -Z i)
  Level_repr.Valid.t l
  letP? res := Level_storage.sub ctxt l i in
  match res with
  | Some l'
      let raw_level1 := l.(Level_repr.t.level) in
      let raw_level2 := l'.(Level_repr.t.level) in
      raw_level2 = raw_level1 -Z i
  | NoneTrue
  end.
Proof.
  intros H_int H_ctxt H_int32 H_level.
  unfold Level_storage.sub.
  destruct H_level.
  pose proof (Raw_level_repr.sub_eq l.(Level_repr.t.level) i
    level ltac:(assumption)) as H_sub.
  pose proof (Raw_level_repr.sub_is_valid l.(Level_repr.t.level) i
    level ltac:(assumption)) as H_sub'.
  destruct (Raw_level_repr.sub _ _) as [opt|]; cbn in *; [|easy].
  subst opt. cbn in ×.
  eapply Error.split_letP. {
    apply Level_repr.root_level_is_valid.
    Raw_context.Valid.destruct_rewrite H_ctxt.
    cbn in ×.
    now destruct H_sim_ctxt, config.
  } intros level' H_level'.
  step; [|easy].
  eapply Error.split_letP. {
    now apply from_raw_eq.
  }
  easy.
Qed.

[previous] level is valid
Lemma previous_is_valid ctxt :
  Valid.t ctxt
     ((Level_storage.current ctxt).(Level_repr.t.level) -Z 1)
  (letP? pred :=
    Level_storage.pred ctxt (Level_storage.current ctxt) in
  pred None)
  letP? lsp := Level_storage.previous ctxt in
  Level_repr.Valid.t lsp.
Proof.
  intros H_ctxt H_pred.
  unfold Level_storage.previous.
  eapply Error.split_letP. {
    assert (H_ctxt' : Raw_context.Valid.t ctxt).
    { unfold Valid.t in H_ctxt.
      now apply Raw_context.on_impl_t in H_ctxt.
    }
    let current := constr:(Level_storage.current ctxt) in
    pose proof pred_is_valid ctxt current
      H_ctxt (current_is_valid ctxt H_ctxt')
      as H_pred'.
    destruct (Level_storage.pred _ _); [|easy].
    cbn in ×.
    instantiate (1 := fun x
      x None Option.Forall Level_repr.Valid.t x).
    easy.
  }
  intros opt_level H_opt_level; cbn in ×. destruct H_opt_level as
    [H_opt_neq H_opt_valid].
  step; cbn; [|contradiction].
  easy.
Qed.

[pred] do not return none on positive input
Lemma pred_not_none ctxt x :
  Valid.t ctxt (x.(Level_repr.t.level) -i32 1)
  Int32.Valid.positive x.(Level_repr.t.level)
  letP? x' := Level_storage.pred ctxt x in
  x' None.
Proof.
  intros.
  unfold Level_storage.pred, Raw_level_repr.pred.
  destruct x; cbn in ×.
  replace (_ =? 0) with false by lia.
  unfold Int32.pred in ×.
  pose proof (from_raw_is_valid ctxt (Int32.pred level)
    ltac:(assumption)) as H_from_raw.
  destruct (Level_storage.from_raw _ _); [
    |apply H_from_raw; lia].
  cbn.
  discriminate.
Qed.

[previous] is equal to [pred (current ctxt)]
Lemma pred_current_eq_previous (ctxt : Proto_alpha.Raw_context.t) :
  letP?relaxed res :=
    Level_storage.pred ctxt (Level_storage.current ctxt) in
  letP?relaxed res' := Level_storage.previous ctxt in
  match res with
  | Some prevprev = res'
  | NoneTrue
  end.
Proof.
  intros; unfold Level_storage.previous.
  do 2 (step; cbn; [|try easy]).
  reflexivity.
Qed.

The function [first_level_in_cycle] is valid.
The function [last_level_in_cycle] is valid.
Lemma last_level_in_cycle_is_valid ctxt cycle :
  Raw_context.Valid.t ctxt
  Cycle_repr.Valid.t (cycle +Z 1)
  letP? first_level_in_next_cycle :=
    Level_storage.first_level_in_cycle ctxt (cycle +Z 1) in
  Raw_level_repr.Valid.t
    (first_level_in_next_cycle.(Level_repr.t.level) - 1)
  Valid.t ctxt (first_level_in_next_cycle.(Level_repr.t.level) - 1)
  letP? last_level_in_cycle :=
    Level_storage.last_level_in_cycle ctxt cycle in
  Level_repr.Valid.t last_level_in_cycle.
Proof.
  intros.
  unfold Level_storage.last_level_in_cycle in ×.
  unfold Cycle_repr.succ, Int32.succ, "+i32". fold Z.add in ×.
  rewrite Int32.normalize_identity by lia.
  pose proof (first_level_in_cycle_is_valid ctxt (cycle +Z 1)
    ltac:(assumption) ltac:(assumption)) as H_first.
  destruct (Level_storage.first_level_in_cycle ctxt (cycle +Z 1))
    as [first_level_in_next_cycle|]; cbn in *; [|easy].
  intros H_raw_level H_ctxt.
  pose proof (pred_not_none ctxt first_level_in_next_cycle)
    as H_pred_not_none.
  unfold "-i32" in ×. rewrite Int32.normalize_identity in × by lia.
  specialize (H_pred_not_none H_ctxt ltac:(destruct H_first; cbn in *;
    lia)).
  pose proof (pred_eq ctxt first_level_in_next_cycle ltac:(lia)
    H_ctxt H_first) as H_pred.
  pose proof (pred_is_valid ctxt first_level_in_next_cycle ltac:(lia)
    H_first) as H_pred_valid.
  destruct (Level_storage.pred _ _) as [opt_pred|]; cbn in *; [|easy].
  destruct opt_pred as [last_level_in_cycle|]; [|easy]. cbn.
  easy.
Qed.

The function [levels_in_cycle] is valid.
Lemma levels_in_cycle_is_valid ctxt cycle :
  Raw_context.Valid.t ctxt
  Cycle_repr.Valid.t cycle
  letP? levels := Level_storage.levels_in_cycle ctxt cycle in
  List.Forall Level_repr.Valid.t levels.
Proof.
  intros.
  unfold Level_storage.levels_in_cycle.
  eapply Error.split_letP. {
    now apply first_level_in_cycle_is_valid.
  }
  intros first_level_in_cycle' H_first.
  cbn.
  (* @TODO : This involves a loop function that recurses
     over the levels, the levels are ints so Coq cannot
     check that it ends
   *)

Admitted.

The function [levels_in_current_cycle] is valid.
Lemma levels_in_current_cycle_is_valid ctxt offset :
  Raw_context.Valid.t ctxt
  Option.Forall (fun offset : int32
     let current :=
       (Level_storage.current ctxt).(Level_repr.t.level) in
     Cycle_repr.Valid.t (current +Z offset))
     offset
  letP? levels :=
    Level_storage.levels_in_current_cycle ctxt offset tt in
  List.Forall Level_repr.Valid.t levels.
Proof.
  intros H_ctxt **.
  unfold Level_storage.levels_in_current_cycle.
  unfold Cycle_repr.to_int32.
  destruct offset as [offset|].
  { cbn in ×. step; cbn.
    { constructor. }
    { apply levels_in_cycle_is_valid; [easy|].
      unfold Cycle_repr.of_int32_exn.
      step; [|lia].
      pose proof current_is_valid as H_current.
      repeat specialize (H_current ltac:(assumption)).
      destruct (Level_storage.current ctxt); cbn.
      destruct H_current; cbn in ×.
      lia.
    }
  }
  { cbn in ×. step; cbn; [constructor|].
    apply levels_in_cycle_is_valid; [easy|].
    unfold Cycle_repr.of_int32_exn.
    step; lia.
  }
Qed.

The function [levels_with_commitments_in_cycle] is valid.
This involves a loop function that recurses over the levels. Coq can't check that it finishes
Admitted.

The function [last_allowed_fork_level] is valid.
Lemma last_allowed_fork_level_is_valid ctxt :
  Raw_context.Valid.t ctxt
  letP? level :=
    Level_storage.last_allowed_fork_level ctxt in
  Raw_level_repr.Valid.t level.
Proof.
  intros H.
  unfold Level_storage.last_allowed_fork_level.
  Raw_context.Valid.destruct_rewrite H.
  eapply Error.split_letP.
  { apply Cycle_repr.sub_is_valid.
    unfold Constants_storage.preserved_cycles; cbn.
    destruct H_sim_ctxt, config, constants.
    lia.
  }
  { intros [cycle|] ?; simpl in *;
      [|apply Raw_level_repr.root_value_is_valid].
    eapply Error.split_letP; [
      now apply first_level_in_cycle_is_valid |
      sauto l: on
    ].
  }
Qed.

The function [last_of_a_cycle] is valid.
Given a context with at last one era, with a level on it, [dawn_of_a_new_cycle] is when the next [cycle_position] is equal to the [cycle_era.blocks_per_cycle] for that era
Lemma dawn_of_a_new_cycle_eq (ctxt : Proto_alpha.Raw_context.t)
  (era : Level_repr.cycle_era) :
  Raw_context.Has_one_era.t ctxt era
  Level_repr.Level_in_era.t (Level_storage.current ctxt) era
  Int32.succ
    (Level_storage.current ctxt).(Level_repr.t.cycle_position) =?
    era.(Level_repr.cycle_era.blocks_per_cycle) = true
  letP? res := Level_storage.dawn_of_a_new_cycle ctxt in
  match res with
  | Some ll = (Level_storage.current ctxt).(Level_repr.t.cycle)
  | NoneTrue
  end.
Proof.
  intros.
  unfold Level_storage.dawn_of_a_new_cycle.
  unfold Level_storage.last_of_a_cycle.
  unfold Level_repr.last_of_cycle. simpl.
  unfold Level_repr.era_of_level.
  rewrite H.
  unfold Raw_level_repr.op_gteq. simpl.
  unfold Level_repr.Level_in_era.t in H0.
  rewrite <- Reflect.Z_geb_ge in H0; unfold is_true in H0.
  remember (_ >=? _) as cond. rewrite H0.
  hauto lq: on.
Qed.