🐆 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.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).

[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).