🐆 Tx_rollup_l2_verifier.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_apply.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_proof.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_storage_sig.
Definition verify_proof_model (message_size : int) (proof_size : int)
: Saturation_repr.t :=
let proof_size_coeff := Saturation_repr.safe_int 124 in
let message_size_coeff := Saturation_repr.safe_int 8416 in
let op_star := Saturation_repr.mul in
let op_plus := Saturation_repr.add in
op_plus (op_star proof_size_coeff (Saturation_repr.safe_int proof_size))
(op_star message_size_coeff (Saturation_repr.safe_int message_size)).
Definition consume_verify_proof_cost
(ctxt : Alpha_context.context) (message_size : int) (proof_size : int)
: M? Alpha_context.context :=
let max_proof_size :=
Alpha_context.Constants.tx_rollup_rejection_max_proof_size ctxt in
Alpha_context.Gas.consume ctxt
(verify_proof_model message_size (Compare.Int.max proof_size max_proof_size)).
Module Verifier_storage.
Definition t : Set := Context.tree.
Definition m (a : Set) : Set := Pervasives.result a Error_monad._error.
Module Syntax.
Definition op_letstar {a b : Set} : m a → (a → m b) → m b :=
Error_monad.op_gtgteqquestion.
Definition op_letplus {a b : Set} : m a → (a → b) → m b :=
Error_monad.op_gtpipeeqquestion.
Definition _return {a : Set} : a → m a := Error_monad._return.
Definition fail {a : Set} (e_value : Error_monad._error) : m a :=
Pervasives.Error e_value.
Definition catch {a B : Set}
(m_value : m a) (k_value : a → B) (h_value : Error_monad._error → B)
: B :=
let function_parameter := m_value in
match function_parameter with
| Pervasives.Ok x_value ⇒ k_value x_value
| Pervasives.Error e_value ⇒ h_value e_value
end.
Definition list_fold_left_m {a b : Set}
: (a → b → m a) → a → list b → m a := List.fold_left_es.
(* Syntax *)
Definition module :=
{|
Tx_rollup_l2_storage_sig.SYNTAX.op_letstar _ _ := op_letstar;
Tx_rollup_l2_storage_sig.SYNTAX.op_letplus _ _ := op_letplus;
Tx_rollup_l2_storage_sig.SYNTAX._return _ := _return;
Tx_rollup_l2_storage_sig.SYNTAX.fail _ := fail;
Tx_rollup_l2_storage_sig.SYNTAX.catch _ _ := catch;
Tx_rollup_l2_storage_sig.SYNTAX.list_fold_left_m _ _ := list_fold_left_m
|}.
End Syntax.
Definition Syntax := Syntax.module.
Definition path (k_value : bytes) : list string :=
[ Bytes.to_string k_value ].
Definition get {A : Set} (store : Context.tree) (key_value : bytes)
: Pervasives.result (option Context.value) A :=
Error_monad.op_gtgteq
(Context.Tree.(Context.TREE.find) store (path key_value))
Error_monad._return.
Definition set {A : Set}
(store : Context.tree) (key_value : bytes) (value_value : Context.value)
: Pervasives.result Context.tree A :=
Error_monad.op_gtgteq
(Context.Tree.(Context.TREE.add) store (path key_value) value_value)
Error_monad._return.
Definition remove {A : Set} (store : Context.tree) (key_value : bytes)
: Pervasives.result Context.tree A :=
Error_monad.op_gtgteq
(Context.Tree.(Context.TREE.remove) store (path key_value))
Error_monad._return.
(* Verifier_storage *)
Definition module :=
{|
Tx_rollup_l2_storage_sig.STORAGE.Syntax := Syntax;
Tx_rollup_l2_storage_sig.STORAGE.get := get;
Tx_rollup_l2_storage_sig.STORAGE.set := set;
Tx_rollup_l2_storage_sig.STORAGE.remove := remove
|}.
End Verifier_storage.
Definition Verifier_storage
: Tx_rollup_l2_storage_sig.STORAGE (t := Context.tree)
(m := fun (a : Set) ⇒ Pervasives.result a Error_monad._error) :=
Verifier_storage.module.
Definition Verifier_context := Tx_rollup_l2_context.Make Verifier_storage.
Definition Verifier_apply := Tx_rollup_l2_apply.Make Verifier_context.
Definition hash_message_result
(ctxt : Alpha_context.context) (after : Context_hash.t)
(withdraw : Alpha_context.Tx_rollup_withdraw_list_hash.t)
: M? (Alpha_context.context × Alpha_context.Tx_rollup_message_result_hash.t) :=
Alpha_context.Tx_rollup_hash.message_result ctxt
{| Alpha_context.Tx_rollup_message_result.t.context_hash := after;
Alpha_context.Tx_rollup_message_result.t.withdraw_list_hash := withdraw;
|}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_apply.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_proof.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_storage_sig.
Definition verify_proof_model (message_size : int) (proof_size : int)
: Saturation_repr.t :=
let proof_size_coeff := Saturation_repr.safe_int 124 in
let message_size_coeff := Saturation_repr.safe_int 8416 in
let op_star := Saturation_repr.mul in
let op_plus := Saturation_repr.add in
op_plus (op_star proof_size_coeff (Saturation_repr.safe_int proof_size))
(op_star message_size_coeff (Saturation_repr.safe_int message_size)).
Definition consume_verify_proof_cost
(ctxt : Alpha_context.context) (message_size : int) (proof_size : int)
: M? Alpha_context.context :=
let max_proof_size :=
Alpha_context.Constants.tx_rollup_rejection_max_proof_size ctxt in
Alpha_context.Gas.consume ctxt
(verify_proof_model message_size (Compare.Int.max proof_size max_proof_size)).
Module Verifier_storage.
Definition t : Set := Context.tree.
Definition m (a : Set) : Set := Pervasives.result a Error_monad._error.
Module Syntax.
Definition op_letstar {a b : Set} : m a → (a → m b) → m b :=
Error_monad.op_gtgteqquestion.
Definition op_letplus {a b : Set} : m a → (a → b) → m b :=
Error_monad.op_gtpipeeqquestion.
Definition _return {a : Set} : a → m a := Error_monad._return.
Definition fail {a : Set} (e_value : Error_monad._error) : m a :=
Pervasives.Error e_value.
Definition catch {a B : Set}
(m_value : m a) (k_value : a → B) (h_value : Error_monad._error → B)
: B :=
let function_parameter := m_value in
match function_parameter with
| Pervasives.Ok x_value ⇒ k_value x_value
| Pervasives.Error e_value ⇒ h_value e_value
end.
Definition list_fold_left_m {a b : Set}
: (a → b → m a) → a → list b → m a := List.fold_left_es.
(* Syntax *)
Definition module :=
{|
Tx_rollup_l2_storage_sig.SYNTAX.op_letstar _ _ := op_letstar;
Tx_rollup_l2_storage_sig.SYNTAX.op_letplus _ _ := op_letplus;
Tx_rollup_l2_storage_sig.SYNTAX._return _ := _return;
Tx_rollup_l2_storage_sig.SYNTAX.fail _ := fail;
Tx_rollup_l2_storage_sig.SYNTAX.catch _ _ := catch;
Tx_rollup_l2_storage_sig.SYNTAX.list_fold_left_m _ _ := list_fold_left_m
|}.
End Syntax.
Definition Syntax := Syntax.module.
Definition path (k_value : bytes) : list string :=
[ Bytes.to_string k_value ].
Definition get {A : Set} (store : Context.tree) (key_value : bytes)
: Pervasives.result (option Context.value) A :=
Error_monad.op_gtgteq
(Context.Tree.(Context.TREE.find) store (path key_value))
Error_monad._return.
Definition set {A : Set}
(store : Context.tree) (key_value : bytes) (value_value : Context.value)
: Pervasives.result Context.tree A :=
Error_monad.op_gtgteq
(Context.Tree.(Context.TREE.add) store (path key_value) value_value)
Error_monad._return.
Definition remove {A : Set} (store : Context.tree) (key_value : bytes)
: Pervasives.result Context.tree A :=
Error_monad.op_gtgteq
(Context.Tree.(Context.TREE.remove) store (path key_value))
Error_monad._return.
(* Verifier_storage *)
Definition module :=
{|
Tx_rollup_l2_storage_sig.STORAGE.Syntax := Syntax;
Tx_rollup_l2_storage_sig.STORAGE.get := get;
Tx_rollup_l2_storage_sig.STORAGE.set := set;
Tx_rollup_l2_storage_sig.STORAGE.remove := remove
|}.
End Verifier_storage.
Definition Verifier_storage
: Tx_rollup_l2_storage_sig.STORAGE (t := Context.tree)
(m := fun (a : Set) ⇒ Pervasives.result a Error_monad._error) :=
Verifier_storage.module.
Definition Verifier_context := Tx_rollup_l2_context.Make Verifier_storage.
Definition Verifier_apply := Tx_rollup_l2_apply.Make Verifier_context.
Definition hash_message_result
(ctxt : Alpha_context.context) (after : Context_hash.t)
(withdraw : Alpha_context.Tx_rollup_withdraw_list_hash.t)
: M? (Alpha_context.context × Alpha_context.Tx_rollup_message_result_hash.t) :=
Alpha_context.Tx_rollup_hash.message_result ctxt
{| Alpha_context.Tx_rollup_message_result.t.context_hash := after;
Alpha_context.Tx_rollup_message_result.t.withdraw_list_hash := withdraw;
|}.
[after_hash_when_proof_failed before] produces the
{!Alpha_context.Tx_rollup_message_result_hash} expected if a proof failed.
That is, the after hash is the same as [before] and it produced zero
withdrawals.
Definition after_hash_when_proof_failed
(ctxt : Alpha_context.context) (before : Context_hash.t)
: M? (Alpha_context.context × Alpha_context.Tx_rollup_message_result_hash.t) :=
hash_message_result ctxt before
Alpha_context.Tx_rollup_withdraw_list_hash.empty.
Definition verify_l2_proof
(proof_value : Context.Proof.t Context.Proof.stream)
(parameters : Tx_rollup_l2_apply.parameters)
(message : Alpha_context.Tx_rollup_message.t)
: Pervasives.result (Context.tree × list Alpha_context.Tx_rollup_withdraw.t)
Variant.t :=
Context.verify_stream_proof proof_value
(fun (tree_value : Context.tree) ⇒
let function_parameter :=
Verifier_apply.(Tx_rollup_l2_apply.S.apply_message) tree_value
parameters message in
match function_parameter with
| Pervasives.Ok (tree_value, (_, withdrawals)) ⇒
(tree_value, withdrawals)
| Pervasives.Error _ ⇒ (tree_value, nil)
end).
(ctxt : Alpha_context.context) (before : Context_hash.t)
: M? (Alpha_context.context × Alpha_context.Tx_rollup_message_result_hash.t) :=
hash_message_result ctxt before
Alpha_context.Tx_rollup_withdraw_list_hash.empty.
Definition verify_l2_proof
(proof_value : Context.Proof.t Context.Proof.stream)
(parameters : Tx_rollup_l2_apply.parameters)
(message : Alpha_context.Tx_rollup_message.t)
: Pervasives.result (Context.tree × list Alpha_context.Tx_rollup_withdraw.t)
Variant.t :=
Context.verify_stream_proof proof_value
(fun (tree_value : Context.tree) ⇒
let function_parameter :=
Verifier_apply.(Tx_rollup_l2_apply.S.apply_message) tree_value
parameters message in
match function_parameter with
| Pervasives.Ok (tree_value, (_, withdrawals)) ⇒
(tree_value, withdrawals)
| Pervasives.Error _ ⇒ (tree_value, nil)
end).
[compute_proof_after_hash ~max_proof_size agreed proof message] computes the
after hash expected while verifying [proof] on [message] starting from
[agreed].
Note that if the proof is incorrect this function fails and the commit
can not be rejected.
Axiom compute_proof_after_hash :
int → int → Alpha_context.context → Tx_rollup_l2_apply.parameters →
Context_hash.t → Tx_rollup_l2_proof.t → Alpha_context.Tx_rollup_message.t →
M? (Alpha_context.context × Alpha_context.Tx_rollup_message_result_hash.t).
Definition verify_proof
(ctxt : Alpha_context.context) (parameters : Tx_rollup_l2_apply.parameters)
(message : Alpha_context.Tx_rollup_message.t)
(proof_value : Tx_rollup_l2_proof.t) (proof_length : int)
(agreed : Alpha_context.Tx_rollup_message_result.t)
(rejected : Alpha_context.Tx_rollup_message_result_hash.t)
(max_proof_size : int) : M? Alpha_context.context :=
let? '(ctxt, computed_result) :=
compute_proof_after_hash proof_length max_proof_size ctxt parameters
agreed.(Alpha_context.Tx_rollup_message_result.t.context_hash) proof_value
message in
if
Alpha_context.Tx_rollup_message_result_hash.op_ltgt computed_result rejected
then
return? ctxt
else
Error_monad.tzfail
(Build_extensible "Proof_produced_rejected_state" unit tt).
int → int → Alpha_context.context → Tx_rollup_l2_apply.parameters →
Context_hash.t → Tx_rollup_l2_proof.t → Alpha_context.Tx_rollup_message.t →
M? (Alpha_context.context × Alpha_context.Tx_rollup_message_result_hash.t).
Definition verify_proof
(ctxt : Alpha_context.context) (parameters : Tx_rollup_l2_apply.parameters)
(message : Alpha_context.Tx_rollup_message.t)
(proof_value : Tx_rollup_l2_proof.t) (proof_length : int)
(agreed : Alpha_context.Tx_rollup_message_result.t)
(rejected : Alpha_context.Tx_rollup_message_result_hash.t)
(max_proof_size : int) : M? Alpha_context.context :=
let? '(ctxt, computed_result) :=
compute_proof_after_hash proof_length max_proof_size ctxt parameters
agreed.(Alpha_context.Tx_rollup_message_result.t.context_hash) proof_value
message in
if
Alpha_context.Tx_rollup_message_result_hash.op_ltgt computed_result rejected
then
return? ctxt
else
Error_monad.tzfail
(Build_extensible "Proof_produced_rejected_state" unit tt).