Skip to main content

🪜 Level_storage.v

Proofs

See code, Gitlab , OCaml

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

[previous] level is valid
Lemma previous_is_valid : {ctxt},
    match Level_storage.pred ctxt (Level_storage.current ctxt) with
    | Some lLevel_repr.Valid.t l
    | NoneFalse
    end
    Level_repr.Valid.t (Level_storage.previous ctxt).
Proof.
  intros ctxt.
  unfold Level_storage.previous.
  destruct (Level_storage.pred _ _); easy.
Qed.

[root_value] level is valid
Lemma root_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
    Level_repr.Valid.t (Level_storage.root_value ctxt).
Proof.
  intros.
  unfold Level_storage.root_value.
  unfold Level_repr.root_level.
  constructor; simpl; try lia.
  now rewrite H1.
Qed.

[from_raw_with_offset] returns a valid level
[preq] is equivalent to [Z.pred] on positives
Lemma pred_eq
  (ctxt : Raw_context.t) (level : Level_repr.t) :
  Level_repr.Valid.t level
  match Level_storage.pred ctxt level with
  | Some l
      let raw_level1 := level.(Level_repr.t.level) in
      let raw_level2 := l.(Level_repr.t.level) in
      raw_level2 = Z.pred raw_level1
  | NoneTrue
  end.
Proof.
  intros.
  unfold Level_storage.pred.
  unfold Raw_level_repr.pred.
  destruct (Raw_level_repr.op_eq _ _) eqn:?; [easy|].
  unfold Level_storage.from_raw. simpl. unfold pred.
  unfold Int32.pred. unfold "-i32".
  rewrite Int32.normalize_identity; [|destruct H; lia].
  easy.
Qed.

[succ] is equivalent to [Z.succ]
Lemma succ_eq (ctxt : Raw_context.t) (level : Level_repr.t) :
  Int32.Valid.t (level.(Level_repr.t.level) +Z 1)
  Level_repr.Valid.t level
  let 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.
  unfold Level_storage.succ,
    Raw_level_repr.succ,
    Int32.succ,
    "+i32" in ×.
  simpl in ×.
  subst raw_level2.
  rewrite Int32.normalize_identity; easy.
Qed.

[add] is equivalent to [+Z]
Lemma add_eq (ctxt : Raw_context.t) (l : Level_repr.t)
  (i : Int32.t) :
  Int32.Valid.t i
  Level_repr.Valid.t l
  Int32.Valid.t (l.(Level_repr.t.level) +Z i)
  let 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 Hint Hlevel Hint_level.
  autounfold with tezos_z in ×.
  unfold Level_storage.add,
    Raw_level_repr.add,
    "+i32".
  repeat rewrite Int32.normalize_identity; lia.
Qed.

[sub] is equivalent to [-Z]
Lemma sub_eq (ctxt : Raw_context.t)
  (l : Level_repr.t) (i : Int32.t) :
  Int32.Valid.non_negative i
  Int32.Valid.t (l.(Level_repr.t.level) -Z i)
  Level_repr.Valid.t l
  match Level_storage.sub ctxt l i 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 Hint Hint2 Hlevel.
  autounfold with tezos_z in ×.
  unfold Level_storage.sub,
    Raw_level_repr.sub,
    "-i32".
  repeat rewrite Int32.normalize_identity; try lia.
  simpl.
  repeat match goal with
  | |- context [match ?e with __ end] ⇒ destruct e eqn:?
  end; [|easy].
  hauto lq: on rew: off.
Qed.

[previous] is equal to [pred (current ctxt)]
Lemma pred_current_eq_previous (ctxt : Raw_context.t) :
  match Level_storage.pred ctxt (Level_storage.current ctxt) with
  | Some prevprev = Level_storage.previous ctxt
  | NoneTrue
  end.
Proof.
  intros.
  unfold Level_storage.previous.
  destruct (Level_storage.pred _ _) eqn:?; trivial.
Qed.

[pred] and [succ] are inverse
Lemma pred_succ_inverse (ctxt : Raw_context.t)
  (l0 l1 : Level_repr.t) (era : Level_repr.cycle_era) :
  Level_repr.Valid.level_from_raw_with_era_invariants.t l0 era
  Level_repr.Valid.t l0
  Raw_context.Has_one_era.t ctxt era
  Level_repr.Level_in_era.t l0 era
  Level_storage.pred ctxt l0 = Some l1
  Level_storage.succ ctxt l1 = l0.
Proof.
  intros Hinvariants_l0 Hvalid_l0 H_has_era H_level_in_era.
  unfold Level_storage.pred, Level_storage.succ.
  unfold Raw_level_repr.pred, Raw_level_repr.succ.
  unfold Raw_level_repr.op_eq. simpl.
  destruct (_ =? 0) eqn:?; [easy|].
  intros Hpred. injection Hpred as Hpred.
  rewrite <- Hpred. simpl.
  destruct Hvalid_l0 as [level _ _ _].
  unfold Raw_level_repr.Valid.t in level.
  assert (Int32_succ_pred_id :
     x, Int32.Valid.t x
         Int32.succ (Int32.pred x) = x) by lia.
  rewrite Int32_succ_pred_id; [|lia].
  unfold Level_storage.from_raw.
  unfold Level_repr.level_from_raw.
  unfold Level_repr.level_from_raw_aux_exn.
  rewrite H_has_era. simpl.
  unfold Level_repr.Level_in_era.t in H_level_in_era.
  unfold Raw_level_repr.op_gteq; simpl;
  rewrite <- Reflect.Z_geb_ge in H_level_in_era;
    unfold is_true in H_level_in_era.
  remember (_ >=? _) as cond.
  rewrite H_level_in_era.
  now apply Level_repr.level_from_raw_with_era_id.
Qed.

Given a context with two cycles, [last_level_in_cycle] is equal to the predecessor of the first level of the next cycle
First level in a cycle is equal to the sucessor of the last level in the previous cycle
Lemma first_level_in_cycle_eq ctxt cycle
  (era : Level_repr.cycle_era) :
  Int32.Valid.non_negative cycle
  Level_repr.Valid.t (Level_storage.first_level_in_cycle ctxt cycle)
  Level_storage.pred ctxt
     (Level_storage.first_level_in_cycle ctxt cycle) None
  Level_repr.Valid.level_from_raw_with_era_invariants.t (Level_storage.first_level_in_cycle
     ctxt cycle) era
  Raw_context.Has_one_era.t ctxt era
  Level_repr.Level_in_era.t (Level_storage.first_level_in_cycle ctxt cycle) era
  match Cycle_repr.pred cycle with
  | Some previous_cycle
      Level_repr.Valid.t (Level_storage.last_level_in_cycle
                            ctxt previous_cycle)
      Level_storage.succ
        ctxt
        (Level_storage.last_level_in_cycle ctxt previous_cycle) =
        Level_storage.first_level_in_cycle ctxt cycle
  | NoneTrue
  end.
Proof.
  intros.
  destruct (Cycle_repr.pred _) as [previous_cycle|] eqn:?; [|easy].
  unfold Level_storage.last_level_in_cycle.
  assert (Hcycle : Cycle_repr.succ previous_cycle = cycle).
  { unfold Cycle_repr.succ. unfold Cycle_repr.pred in Heqo.
    assert (cycle_dec : cycle = 0 cycle > 0) by lia.
    destruct cycle_dec; [scongruence|].
    destruct cycle; [discriminate Heqo| |hfcrush].
    injection Heqo as Heqo. rewrite <- Heqo.
    unfold Int32.succ, Int32.pred.
    assert (plus_1_plus_one_id : x,
      Int32.Valid.t x
      x -i32 1 +i32 1 = x) by lia.
    rewrite plus_1_plus_one_id; easy. }
  rewrite Hcycle.
  destruct (Level_storage.pred _) eqn:?; [|easy].
  intros Hvalid.
  apply pred_succ_inverse with (era := era) in Heqo0; easy.
Qed.

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 : 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
  match Level_storage.dawn_of_a_new_cycle ctxt 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.
  now rewrite H1.
Qed.