Skip to main content

🐆 Tx_rollup_commitment_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_hash_builder.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.

Inductive hash_or_result : Set :=
| Hash : Tx_rollup_message_result_hash_repr.t hash_or_result
| Result : Tx_rollup_message_result_repr.t hash_or_result.

Definition check_message_result
  (ctxt : Raw_context.t)
  (function_parameter :
    Tx_rollup_commitment_repr.template Tx_rollup_commitment_repr.Compact.excerpt)
  : hash_or_result Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
  int M? Raw_context.t :=
  let '{| Tx_rollup_commitment_repr.template.messages := messages |} :=
    function_parameter in
  fun (result_value : hash_or_result) ⇒
    fun (path : Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)) ⇒
      fun (index_value : int) ⇒
        let? '(ctxt, computed) :=
          match result_value with
          | Hash hash_valuereturn? (ctxt, hash_value)
          | Result result_value
            Tx_rollup_hash_builder.message_result ctxt result_value
          end in
        let? ctxt := Tx_rollup_gas.consume_check_path_commitment_cost ctxt in
        let cond :=
          match
            Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.check_path) path
              index_value computed
              messages.(Tx_rollup_commitment_repr.Compact.excerpt.root) with
          | Pervasives.Ok x_valuex_value
          | Pervasives.Error _false
          end in
        let? '_ :=
          Error_monad.error_unless cond
            (Build_extensible "Wrong_rejection_hash"
              Tx_rollup_errors_repr.Wrong_rejection_hash
              {|
                Tx_rollup_errors_repr.Wrong_rejection_hash.provided := computed;
                Tx_rollup_errors_repr.Wrong_rejection_hash.expected :=
                  Tx_rollup_errors_repr.Valid_path
                    messages.(Tx_rollup_commitment_repr.Compact.excerpt.root)
                    index_value; |}) in
        return? ctxt.

Inductive direction : Set :=
| Incr : direction
| Decr : direction.

Definition adjust_commitments_count
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (pkh : Signature.public_key_hash) (dir : direction) : M? Raw_context.t :=
  let delta :=
    match dir with
    | Incr ⇒ 1
    | Decr ⇒ (-1)
    end in
  let? '(ctxt, commitment) :=
    Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) pkh in
  let count :=
    match commitment with
    | Some countcount +i delta
    | Nonedelta
    end in
  let? '_ :=
    Error_monad.fail_when (count <i 0)
      (Build_extensible "Commitment_bond_negative" int count) in
  let? '(ctxt, _, _) :=
    Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      (ctxt, tx_rollup) pkh count in
  return? ctxt.

Definition remove_bond
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (contract : Signature.public_key_hash) : M? Raw_context.t :=
  let? '(ctxt, bond) :=
    Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) contract in
  match bond with
  | None
    Error_monad.tzfail
      (Build_extensible "Bond_does_not_exist" Signature.public_key_hash contract)
  | Some 0 ⇒
    let? '(ctxt, _, _) :=
      Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
        (ctxt, tx_rollup) contract in
    return? ctxt
  | Some _
    Error_monad.tzfail
      (Build_extensible "Bond_in_use" Signature.public_key_hash contract)
  end.

Definition slash_bond
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (contract : Signature.public_key_hash) : M? (Raw_context.t × bool) :=
  let? '(ctxt, bond_counter) :=
    Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) contract in
  match bond_counter with
  | Nonereturn? (ctxt, false)
  | Some c_value
    let? '(ctxt, _, _) :=
      Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
        (ctxt, tx_rollup) contract in
    return? (ctxt, (0 <i c_value))
  end.

Definition find
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t) (level : Tx_rollup_level_repr.t)
  : M?
    (Raw_context.t ×
      option
        Tx_rollup_commitment_repr.Submitted_commitment.(Storage_sigs.VALUE.t)) :=
  if Tx_rollup_state_repr.has_valid_commitment_at state_value level then
    let? '(ctxt, commitment) :=
      Storage.Tx_rollup.Commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
        (ctxt, tx_rollup) level in
    match commitment with
    | None
      let? ctxt := Tx_rollup_state_storage.assert_exist ctxt tx_rollup in
      return? (ctxt, None)
    | Some resreturn? (ctxt, (Some res))
    end
  else
    return? (ctxt, None).

Definition get
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t) (level : Tx_rollup_level_repr.t)
  : M?
    (Raw_context.t ×
      Tx_rollup_commitment_repr.Submitted_commitment.(Storage_sigs.VALUE.t)) :=
  let? '(ctxt, commitment) := find ctxt tx_rollup state_value level in
  match commitment with
  | None
    Error_monad.tzfail
      (Build_extensible "Commitment_does_not_exist" Tx_rollup_level_repr.t level)
  | Some commitmentreturn? (ctxt, commitment)
  end.

Definition get_finalized
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t) (level : Tx_rollup_level_repr.t)
  : M?
    (Raw_context.t ×
      Tx_rollup_commitment_repr.Submitted_commitment.(Storage_sigs.VALUE.t)) :=
  let window := Tx_rollup_state_repr.finalized_commitments_range state_value in
  let? '_ :=
    match window with
    | Some (first, last)
      Error_monad.error_unless
        ((Tx_rollup_level_repr.op_lteq first level) &&
        (Tx_rollup_level_repr.op_lteq level last))
        (Build_extensible "No_finalized_commitment_for_level"
          Tx_rollup_errors_repr.No_finalized_commitment_for_level
          {|
            Tx_rollup_errors_repr.No_finalized_commitment_for_level.level :=
              level;
            Tx_rollup_errors_repr.No_finalized_commitment_for_level.window :=
              window; |})
    | None
      Error_monad.error_value
        (Build_extensible "No_finalized_commitment_for_level"
          Tx_rollup_errors_repr.No_finalized_commitment_for_level
          {|
            Tx_rollup_errors_repr.No_finalized_commitment_for_level.level :=
              level;
            Tx_rollup_errors_repr.No_finalized_commitment_for_level.window :=
              window; |})
    end in
  let? '(ctxt, commitment) :=
    Storage.Tx_rollup.Commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) level in
  match commitment with
  | None
    Error_monad.tzfail
      (Build_extensible "Commitment_does_not_exist" Tx_rollup_level_repr.t level)
  | Some commitmentreturn? (ctxt, commitment)
  end.

Definition check_commitment_level {A : Set}
  (current_level : Raw_level_repr.t) (state_value : Tx_rollup_state_repr.t)
  (commitment : Tx_rollup_commitment_repr.template A) : M? unit :=
  let? expected_level :=
    Tx_rollup_state_repr.next_commitment_level state_value current_level in
  let? '_ :=
    Error_monad.error_when
      (Tx_rollup_level_repr.op_lt
        commitment.(Tx_rollup_commitment_repr.template.level) expected_level)
      (Build_extensible "Level_already_has_commitment" Tx_rollup_level_repr.t
        commitment.(Tx_rollup_commitment_repr.template.level)) in
  Error_monad.error_when
    (Tx_rollup_level_repr.op_lt expected_level
      commitment.(Tx_rollup_commitment_repr.template.level))
    (Build_extensible "Commitment_too_early"
      Tx_rollup_errors_repr.Commitment_too_early
      {|
        Tx_rollup_errors_repr.Commitment_too_early.provided :=
          commitment.(Tx_rollup_commitment_repr.template.level);
        Tx_rollup_errors_repr.Commitment_too_early.expected := expected_level;
        |}).

[check_commitment_predecessor ctxt tx_rollup state commitment] will raise an error if the [predecessor] field of [commitment] is not consistent with the context, assuming its [level] field is correct.
Definition check_commitment_predecessor {A B : Set}
  (ctxt : A) (state_value : Tx_rollup_state_repr.t)
  (commitment : Tx_rollup_commitment_repr.template B) : M? A :=
  match
    ((commitment.(Tx_rollup_commitment_repr.template.predecessor),
      (Tx_rollup_state_repr.next_commitment_predecessor state_value)),
      match
        (commitment.(Tx_rollup_commitment_repr.template.predecessor),
          (Tx_rollup_state_repr.next_commitment_predecessor state_value)) with
      | (Some pred_hash, Some expected_hash)
        Tx_rollup_commitment_repr.Hash.op_eq pred_hash expected_hash
      | _false
      end) with
  | ((Some pred_hash, Some expected_hash), true)return? ctxt
  | ((None, None), _)return? ctxt
  | ((provided, expected), _)
    Error_monad.tzfail
      (Build_extensible "Wrong_predecessor_hash"
        Tx_rollup_errors_repr.Wrong_predecessor_hash
        {| Tx_rollup_errors_repr.Wrong_predecessor_hash.provided := provided;
          Tx_rollup_errors_repr.Wrong_predecessor_hash.expected := expected; |})
  end.

Definition check_commitment_batches_and_merkle_root {A B C : Set}
  (ctxt : A) (state_value : B) (inbox_value : Tx_rollup_inbox_repr.t)
  (commitment : Tx_rollup_commitment_repr.template (list C)) : M? (A × B) :=
  let '{|
    Tx_rollup_inbox_repr.t.inbox_length := inbox_length;
      Tx_rollup_inbox_repr.t.merkle_root := merkle_root
      |} := inbox_value in
  let? '_ :=
    Error_monad.fail_unless
      (Compare.List_length_with.op_eq
        commitment.(Tx_rollup_commitment_repr.template.messages) inbox_length)
      (Build_extensible "Wrong_batch_count" unit tt) in
  let? '_ :=
    Error_monad.fail_unless
      (Tx_rollup_inbox_repr.Merkle.op_eq
        commitment.(Tx_rollup_commitment_repr.template.inbox_merkle_root)
        merkle_root) (Build_extensible "Wrong_inbox_hash" unit tt) in
  return? (ctxt, state_value).

Definition add_commitment
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t) (pkh : Signature.public_key_hash)
  (commitment :
    Tx_rollup_commitment_repr.template
      (list Tx_rollup_message_result_hash_repr.t))
  : M?
    (Raw_context.t × Tx_rollup_state_repr.t × option Signature.public_key_hash) :=
  let commitment_limit := Constants_storage.tx_rollup_max_commitments_count ctxt
    in
  let? '_ :=
    Error_monad.fail_when
      ((Tx_rollup_state_repr.commitments_count state_value) i commitment_limit)
      (Build_extensible "Too_many_commitments" unit tt) in
  let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
  let? '_ := check_commitment_level current_level state_value commitment in
  let? ctxt := check_commitment_predecessor ctxt state_value commitment in
  let? '(ctxt, inbox_value) :=
    Tx_rollup_inbox_storage.get ctxt
      commitment.(Tx_rollup_commitment_repr.template.level) tx_rollup in
  let? '(ctxt, state_value) :=
    check_commitment_batches_and_merkle_root ctxt state_value inbox_value
      commitment in
  let? '(ctxt, invalid_commitment) :=
    Storage.Tx_rollup.Commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) commitment.(Tx_rollup_commitment_repr.template.level) in
  let? to_slash :=
    Option.map_e
      (fun (x_value :
        Tx_rollup_commitment_repr.Submitted_commitment.(Storage_sigs.VALUE.t))
        ⇒
        let to_slash :=
          x_value.(Tx_rollup_commitment_repr.Submitted_commitment.t.committer)
          in
        let? '_ :=
          Error_monad.error_when
            (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_eq) pkh
              to_slash) (Build_extensible "Invalid_committer" unit tt) in
        return? to_slash) invalid_commitment in
  let? ctxt :=
    Tx_rollup_gas.consume_compact_commitment_cost ctxt
      inbox_value.(Tx_rollup_inbox_repr.t.inbox_length) in
  let commitment := Tx_rollup_commitment_repr.Full.compact commitment in
  let? '(ctxt, commitment_hash) :=
    Tx_rollup_hash_builder.compact_commitment ctxt commitment in
  let submitted :=
    {|
      Tx_rollup_commitment_repr.Submitted_commitment.t.commitment := commitment;
      Tx_rollup_commitment_repr.Submitted_commitment.t.commitment_hash :=
        commitment_hash;
      Tx_rollup_commitment_repr.Submitted_commitment.t.committer := pkh;
      Tx_rollup_commitment_repr.Submitted_commitment.t.submitted_at :=
        current_level;
      Tx_rollup_commitment_repr.Submitted_commitment.t.finalized_at := None; |}
    in
  let? '(ctxt, _commitment_size_alloc, _) :=
    Storage.Tx_rollup.Commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      (ctxt, tx_rollup) commitment.(Tx_rollup_commitment_repr.template.level)
      submitted in
  let? state_value :=
    Tx_rollup_state_repr.record_commitment_creation state_value
      commitment.(Tx_rollup_commitment_repr.template.level) commitment_hash in
  let? ctxt := adjust_commitments_count ctxt tx_rollup pkh Incr in
  return? (ctxt, state_value, to_slash).

Definition pending_bonded_commitments
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (pkh : Signature.public_key_hash) : M? (Raw_context.t × int) :=
  let? '(ctxt, pending) :=
    Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) pkh in
  return? (ctxt, (Option.value_value pending 0)).

Definition has_bond
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (pkh : Signature.public_key_hash) : M? (Raw_context.t × bool) :=
  let? '(ctxt, pending) :=
    Storage.Tx_rollup.Commitment_bond.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) pkh in
  return? (ctxt, (Option.is_some pending)).

Definition finalize_commitment
  (ctxt : Raw_context.t) (rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t)
  : M? (Raw_context.t × Tx_rollup_state_repr.t × Tx_rollup_level_repr.t) :=
  match Tx_rollup_state_repr.next_commitment_to_finalize state_value with
  | Some oldest_inbox_level
    let? '(ctxt, commitment) := get ctxt rollup state_value oldest_inbox_level
      in
    let finality_period := Constants_storage.tx_rollup_finality_period ctxt in
    let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level)
      in
    let? res :=
      Raw_level_repr.add
        commitment.(Tx_rollup_commitment_repr.Submitted_commitment.t.submitted_at)
        finality_period in
    let? '_ :=
      Error_monad.fail_when (Raw_level_repr.op_lt current_level res)
        (Build_extensible "No_commitment_to_finalize" unit tt) in
    let? ctxt := Tx_rollup_inbox_storage.remove ctxt oldest_inbox_level rollup
      in
    let? '(ctxt, _commitment_size_alloc) :=
      Storage.Tx_rollup.Commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
        (ctxt, rollup) oldest_inbox_level
        (Tx_rollup_commitment_repr.Submitted_commitment.t.with_finalized_at
          (Some current_level) commitment) in
    let? state_value :=
      Tx_rollup_state_repr.record_inbox_deletion state_value oldest_inbox_level
      in
    return? (ctxt, state_value, oldest_inbox_level)
  | None
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "No_commitment_to_finalize" unit tt)
  end.

Definition remove_commitment
  (ctxt : Raw_context.t) (rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t)
  : M? (Raw_context.t × Tx_rollup_state_repr.t × Tx_rollup_level_repr.t) :=
  match Tx_rollup_state_repr.next_commitment_to_remove state_value with
  | Some tail
    let? '(ctxt, commitment) := get ctxt rollup state_value tail in
    let? '_ :=
      match
        commitment.(Tx_rollup_commitment_repr.Submitted_commitment.t.finalized_at)
        with
      | Some finalized_at
        let withdraw_period := Constants_storage.tx_rollup_withdraw_period ctxt
          in
        let current_level :=
          (Raw_context.current_level ctxt).(Level_repr.t.level) in
        let? res := Raw_level_repr.add finalized_at withdraw_period in
        Error_monad.fail_when (Raw_level_repr.op_lt current_level res)
          (Build_extensible "Remove_commitment_too_early" unit tt)
      | None
        Error_monad.Lwt_result_syntax.tzfail
          (Build_extensible "Internal_error" string "Missing finalized_at field")
      end in
    let? ctxt :=
      adjust_commitments_count ctxt rollup
        commitment.(Tx_rollup_commitment_repr.Submitted_commitment.t.committer)
        Decr in
    let? '(ctxt, _freed_size, _existed) :=
      Storage.Tx_rollup.Commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
        (ctxt, rollup) tail in
    let? ctxt := Tx_rollup_reveal_storage.remove ctxt rollup tail in
    let msg_hash :=
      commitment.(Tx_rollup_commitment_repr.Submitted_commitment.t.commitment).(Tx_rollup_commitment_repr.template.messages).(Tx_rollup_commitment_repr.Compact.excerpt.last_result_message_hash)
      in
    let? state_value :=
      Tx_rollup_state_repr.record_commitment_deletion state_value tail
        commitment.(Tx_rollup_commitment_repr.Submitted_commitment.t.commitment_hash)
        msg_hash in
    return? (ctxt, state_value, tail)
  | None
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "No_commitment_to_remove" unit tt)
  end.

Definition check_agreed_and_disputed_results
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t)
  (submitted_commitment :
    Tx_rollup_commitment_repr.Submitted_commitment.(Storage_sigs.VALUE.t))
  (agreed_result : Tx_rollup_message_result_repr.t)
  (agreed_result_path : Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path))
  (disputed_result : Tx_rollup_message_result_hash_repr.t)
  (disputed_position : int)
  (disputed_result_path : Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path))
  : M? Raw_context.t :=
  let commitment :=
    submitted_commitment.(Tx_rollup_commitment_repr.Submitted_commitment.t.commitment)
    in
  let? '_ :=
    Tx_rollup_state_repr.check_level_can_be_rejected state_value
      commitment.(Tx_rollup_commitment_repr.template.level) in
  let? ctxt :=
    check_message_result ctxt commitment (Hash disputed_result)
      disputed_result_path disputed_position in
  if disputed_position =i 0 then
    let? '(ctxt, agreed) :=
      Tx_rollup_hash_builder.message_result ctxt agreed_result in
    match
      Tx_rollup_level_repr.pred
        commitment.(Tx_rollup_commitment_repr.template.level) with
    | None
      let expected := Tx_rollup_message_result_hash_repr.init_value in
      let? '_ :=
        Error_monad.fail_unless
          (Tx_rollup_message_result_hash_repr.op_eq agreed expected)
          (Build_extensible "Wrong_rejection_hash"
            Tx_rollup_errors_repr.Wrong_rejection_hash
            {| Tx_rollup_errors_repr.Wrong_rejection_hash.provided := agreed;
              Tx_rollup_errors_repr.Wrong_rejection_hash.expected :=
                Tx_rollup_errors_repr.Hash expected; |}) in
      return? ctxt
    | Some pred_level
      let? '(ctxt, candidate) :=
        Storage.Tx_rollup.Commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
          (ctxt, tx_rollup) pred_level in
      match candidate with
      | Some commitment
        let expected :=
          commitment.(Tx_rollup_commitment_repr.Submitted_commitment.t.commitment).(Tx_rollup_commitment_repr.template.messages).(Tx_rollup_commitment_repr.Compact.excerpt.last_result_message_hash)
          in
        let? '_ :=
          Error_monad.fail_unless
            (Tx_rollup_message_result_hash_repr.op_eq agreed expected)
            (Build_extensible "Wrong_rejection_hash"
              Tx_rollup_errors_repr.Wrong_rejection_hash
              {| Tx_rollup_errors_repr.Wrong_rejection_hash.provided := agreed;
                Tx_rollup_errors_repr.Wrong_rejection_hash.expected :=
                  Tx_rollup_errors_repr.Hash expected; |}) in
        return? ctxt
      | None
        match Tx_rollup_state_repr.last_removed_commitment_hashes state_value
          with
        | Some (last_hash, _)
          let? '_ :=
            Error_monad.fail_unless
              (Tx_rollup_message_result_hash_repr.op_eq agreed last_hash)
              (Build_extensible "Wrong_rejection_hash"
                Tx_rollup_errors_repr.Wrong_rejection_hash
                {|
                  Tx_rollup_errors_repr.Wrong_rejection_hash.provided := agreed;
                  Tx_rollup_errors_repr.Wrong_rejection_hash.expected :=
                    Tx_rollup_errors_repr.Hash last_hash; |}) in
          return? ctxt
        | None
          Error_monad.tzfail
            (Build_extensible "Internal_error" string
              "Missing commitment predecessor")
        end
      end
    end
  else
    let? ctxt :=
      check_message_result ctxt commitment (Result agreed_result)
        agreed_result_path (disputed_position -i 1) in
    return? ctxt.

Definition reject_commitment
  (ctxt : Raw_context.t) (rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t) (level : Tx_rollup_level_repr.t)
  : M? (Raw_context.t × Tx_rollup_state_repr.t) :=
  let? '_ := Tx_rollup_state_repr.check_level_can_be_rejected state_value level
    in
  let? '(ctxt, pred_hash) :=
    match Tx_rollup_level_repr.pred level with
    | Some pred_level
      let? '(ctxt, pred_commitment) := find ctxt rollup state_value pred_level
        in
      let pred_hash :=
        Option.map
          (fun (x_value :
            Tx_rollup_commitment_repr.Submitted_commitment.(Storage_sigs.VALUE.t))
            ⇒
            x_value.(Tx_rollup_commitment_repr.Submitted_commitment.t.commitment_hash))
          pred_commitment in
      return? (ctxt, pred_hash)
    | Nonereturn? (ctxt, None)
    end in
  let? state_value :=
    Tx_rollup_state_repr.record_commitment_rejection state_value level pred_hash
    in
  return? (ctxt, state_value).