🦏 Sc_rollup_proof_repr.v

Translated OCaml

File generated by coq-of-ocaml

Init function; without side-effects in Coq

Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Sc_rollup_proof_check" "Invalid proof"
      "An invalid proof has been submitted"
      (Some
        (fun (fmt : Format.formatter) ⇒
          fun (msg : string) ⇒
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Invalid proof: "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.End_of_format)) "Invalid proof: %s")
              msg))
      (Data_encoding.obj1
        (Data_encoding.req None None "reason" Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Sc_rollup_proof_check" then
            let msg := cast string payload in
            Some msg
          else None
        end)
      (fun (msg : string) ⇒ Build_extensible "Sc_rollup_proof_check" string msg)
    in
  Error_monad.register_error_kind Error_monad.Permanent
    "Sc_rollup_invalid_serialized_inbox_proof" "Invalid serialized inbox proof"
    "The serialized inbox proof can not be de-serialized"
    (Some
      (fun (fmt : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Invalid serialized inbox proof"
                CamlinternalFormatBasics.End_of_format)
              "Invalid serialized inbox proof"))) Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Sc_rollup_invalid_serialized_inbox_proof" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Sc_rollup_invalid_serialized_inbox_proof" unit tt).

Records for the constructor parameters

Module ConstructorRecords_reveal_proof.
  Module reveal_proof.
    Module Dal_page_proof.
      Record record {page_id proof : Set} : Set := Build {
        page_id : page_id;
        proof : proof;
      }.
      Arguments record : clear implicits.
      Definition with_page_id {t_page_id t_proof} page_id
        (r : record t_page_id t_proof) :=
        Build t_page_id t_proof page_id r.(proof).
      Definition with_proof {t_page_id t_proof} proof
        (r : record t_page_id t_proof) :=
        Build t_page_id t_proof r.(page_id) proof.
    End Dal_page_proof.
    Definition Dal_page_proof_skeleton := Dal_page_proof.record.
  End reveal_proof.
End ConstructorRecords_reveal_proof.
Import ConstructorRecords_reveal_proof.

Reserved Notation "'reveal_proof.Dal_page_proof".

Inductive reveal_proof : Set :=
| Raw_data_proof : string → reveal_proof
| Metadata_proof : reveal_proof
| Dal_page_proof : 'reveal_proof.Dal_page_proof → reveal_proof

where "'reveal_proof.Dal_page_proof" :=
  (reveal_proof.Dal_page_proof_skeleton Dal_slot_repr.Page.t
    Dal_slot_repr.History.proof).

Module reveal_proof.
  Include ConstructorRecords_reveal_proof.reveal_proof.
  Definition Dal_page_proof := 'reveal_proof.Dal_page_proof.
End reveal_proof.

Definition reveal_proof_encoding : Data_encoding.encoding reveal_proof :=
  let case_raw_data : Data_encoding.case reveal_proof :=
    Data_encoding.case_value "raw data proof" None (Data_encoding.Tag 0)
      (Data_encoding.obj2
        (Data_encoding.req None None "reveal_proof_kind"
          (Data_encoding.constant "raw_data_proof"))
        (Data_encoding.req None None "raw_data"
          (Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
            (Data_encoding.string' None Data_encoding.Hex))))
      (fun (function_parameter : reveal_proof) ⇒
        match function_parameter with
        | Raw_data_proof s_value ⇒ Some (tt, s_value)
        | _ ⇒ None
        end)
      (fun (function_parameter : unit × string) ⇒
        let '(_, s_value) := function_parameter in
        Raw_data_proof s_value)
  in let case_metadata_proof : Data_encoding.case reveal_proof :=
    Data_encoding.case_value "metadata proof" None (Data_encoding.Tag 1)
      (Data_encoding.obj1
        (Data_encoding.req None None "reveal_proof_kind"
          (Data_encoding.constant "metadata_proof")))
      (fun (function_parameter : reveal_proof) ⇒
        match function_parameter with
        | Metadata_proof ⇒ Some tt
        | _ ⇒ None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Metadata_proof) in
  let case_dal_page :=
    Data_encoding.case_value "dal page proof" None (Data_encoding.Tag 2)
      (Data_encoding.obj3
        (Data_encoding.req None None "reveal_proof_kind"
          (Data_encoding.constant "dal_page_proof"))
        (Data_encoding.req None None "dal_page_id" Dal_slot_repr.Page.encoding)
        (Data_encoding.req None None "dal_proof"
          Dal_slot_repr.History.proof_encoding))
      (fun (function_parameter : reveal_proof) ⇒
        match function_parameter with
        |
          Dal_page_proof {|
            reveal_proof.Dal_page_proof.page_id := page_id;
              reveal_proof.Dal_page_proof.proof := proof_value
              |} ⇒ Some (tt, page_id, proof_value)
        | _ ⇒ None
        end)
      (fun (function_parameter :
        unit × Dal_slot_repr.Page.t × Dal_slot_repr.History.proof) ⇒
        let '(_, page_id, proof_value) := function_parameter in
        Dal_page_proof
          {| reveal_proof.Dal_page_proof.page_id := page_id;
            reveal_proof.Dal_page_proof.proof := proof_value; |}) in
  Data_encoding.union None [ case_raw_data; case_metadata_proof; case_dal_page ].

Records for the constructor parameters

Module ConstructorRecords_input_proof.
  Module input_proof.
    Module Inbox_proof.
      Record record {level message_counter proof : Set} : Set := Build {
        level : level;
        message_counter : message_counter;
        proof : proof;
      }.
      Arguments record : clear implicits.
      Definition with_level {t_level t_message_counter t_proof} level
        (r : record t_level t_message_counter t_proof) :=
        Build t_level t_message_counter t_proof level r.(message_counter)
          r.(proof).
      Definition with_message_counter {t_level t_message_counter t_proof}
        message_counter (r : record t_level t_message_counter t_proof) :=
        Build t_level t_message_counter t_proof r.(level) message_counter
          r.(proof).
      Definition with_proof {t_level t_message_counter t_proof} proof
        (r : record t_level t_message_counter t_proof) :=
        Build t_level t_message_counter t_proof r.(level) r.(message_counter)
          proof.
    End Inbox_proof.
    Definition Inbox_proof_skeleton := Inbox_proof.record.
  End input_proof.
End ConstructorRecords_input_proof.
Import ConstructorRecords_input_proof.

Reserved Notation "'input_proof.Inbox_proof".

Inductive input_proof : Set :=
| Inbox_proof : 'input_proof.Inbox_proof → input_proof
| Reveal_proof : reveal_proof → input_proof
| First_inbox_message : input_proof

where "'input_proof.Inbox_proof" :=
  (input_proof.Inbox_proof_skeleton Raw_level_repr.t Z.t
    Sc_rollup_inbox_repr.serialized_proof).

Module input_proof.
  Include ConstructorRecords_input_proof.input_proof.
  Definition Inbox_proof := 'input_proof.Inbox_proof.
End input_proof.

Definition input_proof_encoding : Data_encoding.encoding input_proof :=
  let proof_kind (kind_value : string) : Data_encoding.field unit :=
    Data_encoding.req None None "input_proof_kind"
      (Data_encoding.constant kind_value) in
  let case_inbox_proof :=
    Data_encoding.case_value "inbox proof" None (Data_encoding.Tag 0)
      (Data_encoding.obj4 (proof_kind "inbox_proof")
        (Data_encoding.req None None "level" Raw_level_repr.encoding)
        (Data_encoding.req None None "message_counter" Data_encoding.n_value)
        (Data_encoding.req None None "serialized_proof"
          Sc_rollup_inbox_repr.serialized_proof_encoding))
      (fun (function_parameter : input_proof) ⇒
        match function_parameter with
        |
          Inbox_proof {|
            input_proof.Inbox_proof.level := level;
              input_proof.Inbox_proof.message_counter := message_counter;
              input_proof.Inbox_proof.proof := proof_value
              |} ⇒ Some (tt, level, message_counter, proof_value)
        | _ ⇒ None
        end)
      (fun (function_parameter :
        unit × Raw_level_repr.raw_level × Z.t ×
          Sc_rollup_inbox_repr.serialized_proof) ⇒
        let '(_, level, message_counter, proof_value) := function_parameter in
        Inbox_proof
          {| input_proof.Inbox_proof.level := level;
            input_proof.Inbox_proof.message_counter := message_counter;
            input_proof.Inbox_proof.proof := proof_value; |}) in
  let case_reveal_proof :=
    Data_encoding.case_value "reveal proof" None (Data_encoding.Tag 1)
      (Data_encoding.obj2 (proof_kind "reveal_proof")
        (Data_encoding.req None None "reveal_proof" reveal_proof_encoding))
      (fun (function_parameter : input_proof) ⇒
        match function_parameter with
        | Reveal_proof s_value ⇒ Some (tt, s_value)
        | _ ⇒ None
        end)
      (fun (function_parameter : unit × reveal_proof) ⇒
        let '(_, s_value) := function_parameter in
        Reveal_proof s_value) in
  let first_input :=
    Data_encoding.case_value "first input" None (Data_encoding.Tag 2)
      (Data_encoding.obj1 (proof_kind "first_input"))
      (fun (function_parameter : input_proof) ⇒
        match function_parameter with
        | First_inbox_message ⇒ Some tt
        | _ ⇒ None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        First_inbox_message) in
  Data_encoding.union None [ case_inbox_proof; case_reveal_proof; first_input ].

Module t.
  Record record : Set := Build {
    pvm_step : Sc_rollups.wrapped_proof;
    input_proof : option input_proof;
  }.
  Definition with_pvm_step pvm_step (r : record) :=
    Build pvm_step r.(input_proof).
  Definition with_input_proof input_proof (r : record) :=
    Build r.(pvm_step) input_proof.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{| t.pvm_step := pvm_step; t.input_proof := input_proof |} :=
        function_parameter in
      (pvm_step, input_proof))
    (fun (function_parameter : Sc_rollups.wrapped_proof × option input_proof) ⇒
      let '(pvm_step, input_proof) := function_parameter in
      {| t.pvm_step := pvm_step; t.input_proof := input_proof; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "pvm_step" Sc_rollups.wrapped_proof_encoding)
      (Data_encoding.opt None None "input_proof" input_proof_encoding)).

Definition pp {A : Set} (ppf : Format.formatter) (function_parameter : A)
  : unit :=
  let '_ := function_parameter in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal "Refutation game proof"
        CamlinternalFormatBasics.End_of_format) "Refutation game proof").

Definition start (proof_value : t) : Sc_rollup_repr.State_hash.t :=
  let P := Sc_rollups.wrapped_proof_module proof_value.(t.pvm_step) in
  let 'existS _ _ P := P in
  P.(Sc_rollups.PVM_with_proof.proof_start_state)
    P.(Sc_rollups.PVM_with_proof.proof_val).

Definition stop (proof_value : t) : Sc_rollup_repr.State_hash.t :=
  let P := Sc_rollups.wrapped_proof_module proof_value.(t.pvm_step) in
  let 'existS _ _ P := P in
  P.(Sc_rollups.PVM_with_proof.proof_stop_state)
    P.(Sc_rollups.PVM_with_proof.proof_val).

Definition cut_at_level
  (origination_level : Raw_level_repr.raw_level)
  (commit_level : Raw_level_repr.raw_level) (input : Sc_rollup_PVM_sig.input)
  : option Sc_rollup_PVM_sig.input :=
  match input with
  |
    Sc_rollup_PVM_sig.Inbox_message {|
      Sc_rollup_PVM_sig.inbox_message.inbox_level := input_level |} ⇒
    if
      (Raw_level_repr.op_lteq input_level origination_level ) ||
      (Raw_level_repr.op_lteq commit_level input_level)
    then
      None
    else
      Some input
  | Sc_rollup_PVM_sig.Reveal _data ⇒ Some input
  end.

Definition proof_error {A : Set} (reason_value : string) : M ? A :=
  Error_monad.Lwt_result_syntax.tzfail
    (Build_extensible "Sc_rollup_proof_check" string reason_value).

Definition check (p_value : bool) (reason_value : string) : M ? unit :=
  if p_value then
    return ? tt
  else
    proof_error reason_value.

Definition check_inbox_proof
  (snapshot_value : Sc_rollup_inbox_repr.history_proof)
  (serialized_inbox_proof : Sc_rollup_inbox_repr.serialized_proof)
  (function_parameter : Raw_level_repr.t × Z.t)
  : M ? (option Sc_rollup_PVM_sig.inbox_message ) :=
  let '(level, counter) := function_parameter in
  match Sc_rollup_inbox_repr.of_serialized_proof serialized_inbox_proof with
  | None ⇒
    Error_monad.error_value
      (Build_extensible "Sc_rollup_invalid_serialized_inbox_proof" unit tt)
  | Some inbox_proof ⇒
    Sc_rollup_inbox_repr.verify_proof (level, counter) snapshot_value
      inbox_proof
  end.

Module Dal_proofs.

Given a page, identified by its ID, we accept to produce or verify a proof for it if, and only if, the page's level [page_published_level] is in the following boundaries: page_published_level > origination_level: this means that the slot of the page was published after the rollup origination ; page_published_level + dal_attestation_lag < commit_level: this means that the slot of the page has been confirmed before the [commit_level]. According to the definition in {!Sc_rollup_commitment_repr}, [commit_level] (aka inbox_level in that module) is the level (excluded) up to which the PVM consumed all messages and DAL/DAC inputs before producing the related commitment.