Skip to main content

🐆 Tx_rollup_l2_verifier.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.V7.
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_valuek_value x_value
      | Pervasives.Error e_valueh_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.
[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.