🐆 Tx_rollup_commitment_storage.v
Translated 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_value ⇒ return? (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_value ⇒ x_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 count ⇒ count +i delta
| None ⇒ delta
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
| None ⇒ return? (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 res ⇒ return? (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 commitment ⇒ return? (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 commitment ⇒ return? (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;
|}).
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_value ⇒ return? (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_value ⇒ x_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 count ⇒ count +i delta
| None ⇒ delta
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
| None ⇒ return? (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 res ⇒ return? (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 commitment ⇒ return? (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 commitment ⇒ return? (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)
| None ⇒ return? (ctxt, None)
end in
let? state_value :=
Tx_rollup_state_repr.record_commitment_rejection state_value level pred_hash
in
return? (ctxt, state_value).
(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)
| None ⇒ return? (ctxt, None)
end in
let? state_value :=
Tx_rollup_state_repr.record_commitment_rejection state_value level pred_hash
in
return? (ctxt, state_value).