🐆 Tx_rollup_repr.v

Proofs

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_state_repr.

Module Hash.
  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Tx_rollup_repr.Hash.encoding.
    apply Blake2B.Make_is_valid.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

The [compare] function is valid.

  Lemma compare_is_valid :
    Compare.Valid.t (fun _ ⇒ True) id Tx_rollup_repr.Hash.compare.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End Hash.

The [compare] function is valid.

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Tx_rollup_repr.compare.
Proof.
  apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Axiom of_b58_to_b58_eq : ∀ v,
  Tx_rollup_repr.of_b58check (Tx_rollup_repr.to_b58check v) =
  return ? v.

Axiom to_b58_of_b58_eq : ∀ b58,
  match Tx_rollup_repr.of_b58check b58 with
  | Pervasives.Ok v ⇒ Tx_rollup_repr.to_b58check v = b58
  | Pervasives.Error _ ⇒ True
  end.

(* TODO: prove if possible ? *)
Axiom of_b58_opt_to_b58_eq : ∀ v,
  Tx_rollup_repr.of_b58check_opt (Tx_rollup_repr.to_b58check v) =
  return × v.

(* TODO: prove if possible ? *)
Axiom to_b58_opt_of_b58_eq : ∀ b58,
  match Tx_rollup_repr.of_b58check_opt b58 with
  | Some v ⇒ Tx_rollup_repr.to_b58check v = b58
  | None ⇒ True
  end.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Tx_rollup_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros; rewrite of_b58_to_b58_eq; repeat (split; trivial).
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True) Tx_rollup_repr.rpc_arg.
  constructor; intros; simpl.
  - rewrite of_b58_to_b58_eq; reflexivity.
  - destruct (Tx_rollup_repr.of_b58check s) eqn:E; simpl; trivial.
    specialize (to_b58_of_b58_eq s); rewrite E; trivial.
Qed.

Lemma index_path_encoding_is_valid :
  Path_encoding.S.Valid.t
    (Storage_description.INDEX.to_Path Tx_rollup_repr.Index).
Proof.
  constructor;
    unfold Tx_rollup_repr.Index,
           Tx_rollup_repr.Index.module,
           Tx_rollup_repr.Index.to_path,
           Tx_rollup_repr.Index.of_path,
           Binary.to_bytes_exn,
           Tx_rollup_repr.Index.path_length; simpl.
  { intros; destruct (Hex.of_bytes _ _); reflexivity. }
  { intro v; destruct (Hex.of_bytes _ _) eqn:E;
      rewrite <- E, Hex.to_bytes_of_bytes; clear E; simpl.
    specialize
      (Data_encoding.Valid.of_bytes_opt_to_bytes_opt encoding_is_valid v I).
    destruct (Binary.to_bytes_opt _ _ _) eqn:E; [|contradiction].
    intro Epath; rewrite Epath; reflexivity.
  }
  { intro path; destruct path; simpl; trivial; destruct path; simpl; trivial.
    destruct (Hex.to_bytes _) eqn:E; simpl; trivial;
    specialize (Hex.of_bytes_to_bytes (Hex.Hex s)); rewrite E; intro;
      specialize
        (Data_encoding.Valid.to_bytes_opt_of_bytes_opt encoding_is_valid b);
      destruct (Binary.of_bytes_opt _ _) eqn:E1; simpl; trivial.
    hauto lq: on.
  }
  { intros; destruct (Hex.of_bytes None _); reflexivity. }
Qed.

Module Index.

The [compare] function is valid.

  Lemma compare_is_valid :
    Compare.Valid.t (fun _ ⇒ True) id Tx_rollup_repr.Index.compare.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End Index.

Verification of no internal errors below

Import and Abreviations for shortening [oldest] and [newest] names in the proofs.

Import Tx_rollup_state_repr.t.
#[local] Notation oldest :=
Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.oldest.
#[local] Notation newest :=
Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.newest.

[shrink] does not return [Internal_error] as long as the [range] argument is [Internval _]

Lemma shrink_is_valid
  (x : Tx_rollup_state_repr.ConstructorRecords_range.range.Interval_skeleton
         Tx_rollup_level_repr.t Tx_rollup_level_repr.t) :
  letP ? _ := Tx_rollup_state_repr.shrink (Tx_rollup_state_repr.Interval x) in
  True.
Proof.
  intros.
  unfold Tx_rollup_state_repr.shrink.
  now step.
Qed.

[right_cut] does not return [Internal_error]

Lemma right_cut_is_valid
  (range : Tx_rollup_state_repr.range)
  (level : Tx_rollup_level_repr.level) :
  Proofs.Tx_rollup_state_repr.right_cut_valid_range range level →
  letP ? _ := Tx_rollup_state_repr.right_cut range level in True.
Proof.
  intros.
  unfold Tx_rollup_state_repr.right_cut_valid_range in H.
  unfold Tx_rollup_state_repr.right_cut.
  destruct Tx_rollup_level_repr.pred eqn:?; [|easy]; simpl.
  destruct range; [|easy].
  destruct H as [H1 H2].
  apply Zle_imp_le_bool in H1.
  apply Zle_imp_le_bool in H2.
  simpl. unfold Tx_rollup_level_repr.op_lteq; simpl.
  simpl in ×.
  set (cond1 := _ <=? level).
  set (cond2 := level <=? _).
  assert (Hcond1 : cond1 = true)
    by (cbv; cbv in H1; now rewrite H1).
  assert (Hcond2 : cond2 = true)
    by (cbv; cbv in H2; now rewrite H2).
  rewrite Hcond1, Hcond2. simpl.
  now destruct (_ <=? i) eqn:?.
Qed.

[adjust_storage_allocation] does not return [Internal_error]

Lemma adjust_storage_allocation_is_valid
  (state_value : Tx_rollup_state_repr.t) (delta : Z.t) :
  state_value.(Tx_rollup_state_repr.t.occupied_storage) +Z delta > 0 →
  letP ? _ := Tx_rollup_state_repr.adjust_storage_allocation state_value delta in
  True.
Proof.
  intros.
  unfold Tx_rollup_state_repr.adjust_storage_allocation.
  destruct Z.equal; [easy|].
  replace
    (state_value.(Tx_rollup_state_repr.t.occupied_storage) +Z delta <Z Z.zero)
    with false
    by lia.
  now step.
Qed.

[left_extend] does not return [Internal_error]

Lemma left_extend_is_valid range level :
  letP ? _ := Tx_rollup_state_repr.left_extend range level in True.
Proof.
  unfold Tx_rollup_state_repr.left_extend.
  now step.
Qed.

[record_inbox_creation] does not return [Internal_error]

Lemma record_inbox_creation_is_valid
  (t_value : Tx_rollup_state_repr.t)
  (level : Raw_level_repr.raw_level) (delta : Z.t) :
  t_value.(Tx_rollup_state_repr.t.occupied_storage)
    +Z Tx_rollup_inbox_repr.size_value > 0 →
  t_value.(Tx_rollup_state_repr.t.tezos_head_level) = None →
  letP ? _ := Tx_rollup_state_repr.record_inbox_creation t_value level in True.
Proof.
  intros Hzero HNone.
  unfold Tx_rollup_state_repr.record_inbox_creation.
  rewrite HNone. simpl.
  destruct Tx_rollup_state_repr.extend; try easy.
  unfold Tx_rollup_state_repr.adjust_storage_allocation.
  step; [easy|].
  replace (_ +Z _ <? Z.zero) with false by lia.
  now step.
Qed.

[record_commitment_rejection_creation] does not return [Internal_error]

Lemma record_commitment_rejection_is_valid
  (state_value : Tx_rollup_state_repr.t) (level : Tx_rollup_level_repr.t)
  (predecessor_hash : option Tx_rollup_commitment_repr.Hash.t) :
  Tx_rollup_state_repr.Valid.t state_value →
  Tx_rollup_state_repr.right_cut_valid_range
    state_value.(Tx_rollup_state_repr.t.unfinalized_commitments) level →
  Tx_rollup_state_repr.Valid_belongs_to.t state_value level predecessor_hash →
  state_value.(Tx_rollup_state_repr.t.last_removed_commitment_hashes) ≠ None →
  letP ? _ :=
  Tx_rollup_state_repr.record_commitment_rejection
    state_value level predecessor_hash in True.
Proof.
  intros HValid Hright_cut Hbelongs_to Hlast.
  unfold Tx_rollup_state_repr.record_commitment_rejection.
  unfold op_gtgtquestion.
  pose proof left_extend_is_valid as Hleft.
  specialize
    (Hleft state_value.(Tx_rollup_state_repr.t.uncommitted_inboxes) level).
  step; [|assumption].
  unfold Tx_rollup_state_repr.t.with_uncommitted_inboxes; simpl.
  clear Hleft Heqr.
  step; [|
    pose proof right_cut_is_valid as Hright;
    specialize
      (Hright
         state_value.(Tx_rollup_state_repr.t.unfinalized_commitments) level);
    rewrite Heqt in Hright; now apply Hright].
  step; [|easy].
  unfold Tx_rollup_state_repr.Valid_belongs_to.t in Hbelongs_to.
  rewrite Heqo in Hbelongs_to;
    destruct Hbelongs_to as [[Hb Hb'] | [Hb Hb']];
    [step; [now destruct predecessor_hash|easy]|].
  step; [now destruct predecessor_hash|].
  destruct predecessor_hash; [easy|]; simpl.
  destruct HValid; simpl.
  destruct state_value; simpl.
  destruct last_removed_commitment_hashes0; [|easy]; simpl.
  now destruct p.
Qed.

[next_commitment_level] does not return [Internal_error]

Lemma next_commitment_level_is_valid
  (state_value : Tx_rollup_state_repr.t)
  (current_level : Raw_level_repr.raw_level) :
  Tx_rollup_state_repr.Rollup_state_consisitent state_value →
  letP ? _ :=
  Tx_rollup_state_repr.next_commitment_level
    state_value current_level in True.
Proof.
  intros.
  unfold Tx_rollup_state_repr.next_commitment_level.
  destruct H as [Hhead [[Hnewest Holdest] | [Hnewest Holdest]]];
  do 2 step; simpl; try easy.
  step; [easy|].
  step; [|easy].
  unfold error_when.
  now step.
Qed.

[record_inbox_deletion] does not return [Internal_error]

[record_commitment_creation] does not return [Internal_error]

Lemma record_commitment_creation_is_valid
  (state_value : Tx_rollup_state_repr.t)
  (level : Tx_rollup_level_repr.level)
  (hash_value : Tx_rollup_commitment_repr.Hash.t)
  (i : Tx_rollup_state_repr.ConstructorRecords_range.range.Interval_skeleton
         Tx_rollup_level_repr.t Tx_rollup_level_repr.t) :
  Tx_rollup_state_repr.Valid.t state_value →
  state_value.(uncommitted_inboxes) =
    Tx_rollup_state_repr.Interval i →
  level = (oldest i) →
  state_value.(occupied_storage) > Tx_rollup_inbox_repr.size_value →
  0 ≤ Tx_rollup_inbox_repr.size_value →
  letP ? _ :=
     (Tx_rollup_state_repr.record_commitment_creation state_value
         level hash_value ) in True.
Proof.
  intros Hvalid Huinb Hlevel Hocc Hsize_value.
  unfold Tx_rollup_state_repr.record_commitment_creation,
    Tx_rollup_state_repr.range_oldest,
    error_unless,
    Tx_rollup_level_repr.op_eq; simpl.
  rewrite Huinb, Hlevel.
  rewrite <- Hlevel.
  rewrite <- Hlevel at 1.
  rewrite Z.eqb_refl.
  pose proof shrink_is_valid as Hshrink.
  specialize (Hshrink i).
  unfold op_gtgtquestion; simpl.
  step; [|easy].
  unfold Tx_rollup_state_repr.extend.
  step_outer.
  step; [|easy].
  pose proof adjust_storage_allocation_is_valid
    as Hadjust.
  set (state_value' := with_commitment_newest_hash _ _).
  set (level' := Z.neg _).
  specialize (Hadjust state_value' level').
  step; [|
    apply Hadjust; destruct Hvalid;
    subst state_value'; simpl; lia].
  now destruct p.
Qed.

[record_commitment_deletion] does not return [Internal_error]

Lemma record_commitment_deletion_is_valid
  (state_value : Tx_rollup_state_repr.t)
  (level : Tx_rollup_level_repr.t)
  (hash_value : Tx_rollup_commitment_repr.Hash.t)
  (message_hash : Tx_rollup_message_result_hash_repr.t)
  (i : Tx_rollup_state_repr.ConstructorRecords_range.range.Interval_skeleton
         Tx_rollup_level_repr.t Tx_rollup_level_repr.t) :
  state_value.(finalized_commitments) =
    Tx_rollup_state_repr.Interval i →
  level = oldest i →
  letP ? _ :=
    (Tx_rollup_state_repr.record_commitment_deletion
       state_value level hash_value message_hash ) in True.
Proof.
  intros Hfin Hlevel.
  unfold Tx_rollup_state_repr.record_commitment_deletion.
  rewrite Hfin; simpl.
  unfold_match; simpl.
  rewrite Hlevel, Z.eqb_refl; simpl.
  unfold op_gtgtquestion.
  pose proof shrink_is_valid as Hshrink.
  specialize (Hshrink i).
  now step.
Qed.