🦏 Sc_rollup_PVM_sig.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_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Module inbox_message.
Record record : Set := Build {
inbox_level : Raw_level_repr.t;
message_counter : Z.t;
payload : Sc_rollup_inbox_message_repr.serialized;
}.
Definition with_inbox_level inbox_level (r : record) :=
Build inbox_level r.(message_counter) r.(payload).
Definition with_message_counter message_counter (r : record) :=
Build r.(inbox_level) message_counter r.(payload).
Definition with_payload payload (r : record) :=
Build r.(inbox_level) r.(message_counter) payload.
End inbox_message.
Definition inbox_message := inbox_message.record.
Inductive reveal_data : Set :=
| Raw_data : string → reveal_data
| Metadata : Sc_rollup_metadata_repr.t → reveal_data
| Dal_page : option Dal_slot_repr.Page.content → reveal_data.
Inductive input : Set :=
| Inbox_message : inbox_message → input
| Reveal : reveal_data → input.
Definition pp_inbox_message
(fmt : Format.formatter) (function_parameter : inbox_message) : unit :=
let '{|
inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "message index: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))
"@[<v 2>level: %a@,message index: %a@]") Raw_level_repr.pp inbox_level
Z.pp_print message_counter.
Definition pp_reveal_data
(fmt : Format.formatter) (function_parameter : reveal_data) : unit :=
match function_parameter with
| Raw_data _ ⇒ Format.pp_print_string fmt "raw data"
| Metadata metadata ⇒ Sc_rollup_metadata_repr.pp fmt metadata
| Dal_page content_opt ⇒
Format.pp_print_option
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt "<No_dal_data>"))
(fun (fmt : Format.formatter) ⇒
fun (_a : Dal_slot_repr.Page.content) ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<Some_dal_data>"
CamlinternalFormatBasics.End_of_format) "<Some_dal_data>")) fmt
content_opt
end.
Definition pp_input (fmt : Format.formatter) (function_parameter : input)
: unit :=
match function_parameter with
| Inbox_message msg ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "inbox message:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[<v 2>inbox message:@,%a@]") pp_inbox_message msg
| Reveal reveal ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "reveal: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))) "@[<v 2>reveal: %a@]")
pp_reveal_data reveal
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Module inbox_message.
Record record : Set := Build {
inbox_level : Raw_level_repr.t;
message_counter : Z.t;
payload : Sc_rollup_inbox_message_repr.serialized;
}.
Definition with_inbox_level inbox_level (r : record) :=
Build inbox_level r.(message_counter) r.(payload).
Definition with_message_counter message_counter (r : record) :=
Build r.(inbox_level) message_counter r.(payload).
Definition with_payload payload (r : record) :=
Build r.(inbox_level) r.(message_counter) payload.
End inbox_message.
Definition inbox_message := inbox_message.record.
Inductive reveal_data : Set :=
| Raw_data : string → reveal_data
| Metadata : Sc_rollup_metadata_repr.t → reveal_data
| Dal_page : option Dal_slot_repr.Page.content → reveal_data.
Inductive input : Set :=
| Inbox_message : inbox_message → input
| Reveal : reveal_data → input.
Definition pp_inbox_message
(fmt : Format.formatter) (function_parameter : inbox_message) : unit :=
let '{|
inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "message index: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))
"@[<v 2>level: %a@,message index: %a@]") Raw_level_repr.pp inbox_level
Z.pp_print message_counter.
Definition pp_reveal_data
(fmt : Format.formatter) (function_parameter : reveal_data) : unit :=
match function_parameter with
| Raw_data _ ⇒ Format.pp_print_string fmt "raw data"
| Metadata metadata ⇒ Sc_rollup_metadata_repr.pp fmt metadata
| Dal_page content_opt ⇒
Format.pp_print_option
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt "<No_dal_data>"))
(fun (fmt : Format.formatter) ⇒
fun (_a : Dal_slot_repr.Page.content) ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<Some_dal_data>"
CamlinternalFormatBasics.End_of_format) "<Some_dal_data>")) fmt
content_opt
end.
Definition pp_input (fmt : Format.formatter) (function_parameter : input)
: unit :=
match function_parameter with
| Inbox_message msg ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "inbox message:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[<v 2>inbox message:@,%a@]") pp_inbox_message msg
| Reveal reveal ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "reveal: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))) "@[<v 2>reveal: %a@]")
pp_reveal_data reveal
end.
[inbox_message_encoding] encoding value for {!inbox_message}.
Definition inbox_message_encoding : Data_encoding.encoding inbox_message :=
Data_encoding.conv
(fun (function_parameter : inbox_message) ⇒
let '{|
inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter;
inbox_message.payload := payload
|} := function_parameter in
(inbox_level, message_counter, payload))
(fun (function_parameter : Raw_level_repr.t × Z.t × string) ⇒
let '(inbox_level, message_counter, payload) := function_parameter in
let payload := Sc_rollup_inbox_message_repr.unsafe_of_string payload in
{| inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter;
inbox_message.payload := payload; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "message_counter" Data_encoding.n_value)
(Data_encoding.req None None "payload"
(Data_encoding.string' None Data_encoding.Hex))).
Definition reveal_data_encoding : Data_encoding.encoding reveal_data :=
let case_raw_data : Data_encoding.case reveal_data :=
Data_encoding.case_value "raw data" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_data_kind"
(Data_encoding.constant "raw_data"))
(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_data) ⇒
match function_parameter with
| Raw_data m_value ⇒ Some (tt, m_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × string) ⇒
let '(_, m_value) := function_parameter in
Raw_data m_value)
in let case_metadata : Data_encoding.case reveal_data :=
Data_encoding.case_value "metadata" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_data_kind"
(Data_encoding.constant "metadata"))
(Data_encoding.req None None "metadata" Sc_rollup_metadata_repr.encoding))
(fun (function_parameter : reveal_data) ⇒
match function_parameter with
| Metadata md ⇒ Some (tt, md)
| _ ⇒ None
end)
(fun (function_parameter : unit × Sc_rollup_metadata_repr.t) ⇒
let '(_, md) := function_parameter in
Metadata md) in
let case_dal_page :=
Data_encoding.case_value "dal page" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_data_kind"
(Data_encoding.constant "dal_page"))
(Data_encoding.req None None "dal_page_content"
(Data_encoding.option_value Data_encoding.bytes_value)))
(fun (function_parameter : reveal_data) ⇒
match function_parameter with
| Dal_page p_value ⇒ Some (tt, p_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × option Bytes.t) ⇒
let '(_, p_value) := function_parameter in
Dal_page p_value) in
Data_encoding.union None [ case_raw_data; case_metadata; case_dal_page ].
Definition input_encoding : Data_encoding.encoding input :=
let case_inbox_message : Data_encoding.case input :=
Data_encoding.case_value "inbox msg" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "input_kind"
(Data_encoding.constant "inbox_message"))
(Data_encoding.req None None "inbox_message" inbox_message_encoding))
(fun (function_parameter : input) ⇒
match function_parameter with
| Inbox_message m_value ⇒ Some (tt, m_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × inbox_message) ⇒
let '(_, m_value) := function_parameter in
Inbox_message m_value)
in let case_reveal_revelation : Data_encoding.case input :=
Data_encoding.case_value "reveal" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "input_kind"
(Data_encoding.constant "reveal_revelation"))
(Data_encoding.req None None "reveal_data" reveal_data_encoding))
(fun (function_parameter : input) ⇒
match function_parameter with
| Reveal d_value ⇒ Some (tt, d_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × reveal_data) ⇒
let '(_, d_value) := function_parameter in
Reveal d_value) in
Data_encoding.union None [ case_inbox_message; case_reveal_revelation ].
Data_encoding.conv
(fun (function_parameter : inbox_message) ⇒
let '{|
inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter;
inbox_message.payload := payload
|} := function_parameter in
(inbox_level, message_counter, payload))
(fun (function_parameter : Raw_level_repr.t × Z.t × string) ⇒
let '(inbox_level, message_counter, payload) := function_parameter in
let payload := Sc_rollup_inbox_message_repr.unsafe_of_string payload in
{| inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter;
inbox_message.payload := payload; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "message_counter" Data_encoding.n_value)
(Data_encoding.req None None "payload"
(Data_encoding.string' None Data_encoding.Hex))).
Definition reveal_data_encoding : Data_encoding.encoding reveal_data :=
let case_raw_data : Data_encoding.case reveal_data :=
Data_encoding.case_value "raw data" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_data_kind"
(Data_encoding.constant "raw_data"))
(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_data) ⇒
match function_parameter with
| Raw_data m_value ⇒ Some (tt, m_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × string) ⇒
let '(_, m_value) := function_parameter in
Raw_data m_value)
in let case_metadata : Data_encoding.case reveal_data :=
Data_encoding.case_value "metadata" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_data_kind"
(Data_encoding.constant "metadata"))
(Data_encoding.req None None "metadata" Sc_rollup_metadata_repr.encoding))
(fun (function_parameter : reveal_data) ⇒
match function_parameter with
| Metadata md ⇒ Some (tt, md)
| _ ⇒ None
end)
(fun (function_parameter : unit × Sc_rollup_metadata_repr.t) ⇒
let '(_, md) := function_parameter in
Metadata md) in
let case_dal_page :=
Data_encoding.case_value "dal page" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_data_kind"
(Data_encoding.constant "dal_page"))
(Data_encoding.req None None "dal_page_content"
(Data_encoding.option_value Data_encoding.bytes_value)))
(fun (function_parameter : reveal_data) ⇒
match function_parameter with
| Dal_page p_value ⇒ Some (tt, p_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × option Bytes.t) ⇒
let '(_, p_value) := function_parameter in
Dal_page p_value) in
Data_encoding.union None [ case_raw_data; case_metadata; case_dal_page ].
Definition input_encoding : Data_encoding.encoding input :=
let case_inbox_message : Data_encoding.case input :=
Data_encoding.case_value "inbox msg" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "input_kind"
(Data_encoding.constant "inbox_message"))
(Data_encoding.req None None "inbox_message" inbox_message_encoding))
(fun (function_parameter : input) ⇒
match function_parameter with
| Inbox_message m_value ⇒ Some (tt, m_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × inbox_message) ⇒
let '(_, m_value) := function_parameter in
Inbox_message m_value)
in let case_reveal_revelation : Data_encoding.case input :=
Data_encoding.case_value "reveal" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "input_kind"
(Data_encoding.constant "reveal_revelation"))
(Data_encoding.req None None "reveal_data" reveal_data_encoding))
(fun (function_parameter : input) ⇒
match function_parameter with
| Reveal d_value ⇒ Some (tt, d_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × reveal_data) ⇒
let '(_, d_value) := function_parameter in
Reveal d_value) in
Data_encoding.union None [ case_inbox_message; case_reveal_revelation ].
[input_equal i1 i2] return whether [i1] and [i2] are equal.
Definition inbox_message_equal
(a_value : inbox_message) (b_value : inbox_message) : bool :=
let '{|
inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter;
inbox_message.payload := payload
|} := a_value in
(Raw_level_repr.equal inbox_level b_value.(inbox_message.inbox_level)) &&
((Z.equal message_counter b_value.(inbox_message.message_counter)) &&
(String.equal payload b_value.(inbox_message.payload))).
Definition reveal_data_equal (a_value : reveal_data) (b_value : reveal_data)
: bool :=
match (a_value, b_value) with
| (Raw_data a_value, Raw_data b_value) ⇒ String.equal a_value b_value
| (Raw_data _, _) ⇒ false
| (Metadata a_value, Metadata b_value) ⇒
Sc_rollup_metadata_repr.equal a_value b_value
| (Metadata _, _) ⇒ false
| (Dal_page a_value, Dal_page b_value) ⇒
Option.equal Bytes.equal a_value b_value
| (Dal_page _, _) ⇒ false
end.
Definition input_equal (a_value : input) (b_value : input) : bool :=
match (a_value, b_value) with
| (Inbox_message a_value, Inbox_message b_value) ⇒
inbox_message_equal a_value b_value
| (Inbox_message _, _) ⇒ false
| (Reveal a_value, Reveal b_value) ⇒ reveal_data_equal a_value b_value
| (Reveal _, _) ⇒ false
end.
Definition Input_hash :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Sc_rollup_input_hash" in
let title := "A smart contract rollup input hash" in
let b58check_prefix := String.String "001" ("v}" ++ String.String "135" "")
in
let size_value := Some 20 in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Module Reveal_hash.
Definition V0 :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Sc_rollup_reveal_data_hash" in
let title := "A smart contract rollup reveal hash" in
let b58check_prefix :=
String.String "017"
(String.String "144"
("y" ++ String.String "209" (String.String "203" ""))) in
let size_value := Some 31 in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
(a_value : inbox_message) (b_value : inbox_message) : bool :=
let '{|
inbox_message.inbox_level := inbox_level;
inbox_message.message_counter := message_counter;
inbox_message.payload := payload
|} := a_value in
(Raw_level_repr.equal inbox_level b_value.(inbox_message.inbox_level)) &&
((Z.equal message_counter b_value.(inbox_message.message_counter)) &&
(String.equal payload b_value.(inbox_message.payload))).
Definition reveal_data_equal (a_value : reveal_data) (b_value : reveal_data)
: bool :=
match (a_value, b_value) with
| (Raw_data a_value, Raw_data b_value) ⇒ String.equal a_value b_value
| (Raw_data _, _) ⇒ false
| (Metadata a_value, Metadata b_value) ⇒
Sc_rollup_metadata_repr.equal a_value b_value
| (Metadata _, _) ⇒ false
| (Dal_page a_value, Dal_page b_value) ⇒
Option.equal Bytes.equal a_value b_value
| (Dal_page _, _) ⇒ false
end.
Definition input_equal (a_value : input) (b_value : input) : bool :=
match (a_value, b_value) with
| (Inbox_message a_value, Inbox_message b_value) ⇒
inbox_message_equal a_value b_value
| (Inbox_message _, _) ⇒ false
| (Reveal a_value, Reveal b_value) ⇒ reveal_data_equal a_value b_value
| (Reveal _, _) ⇒ false
end.
Definition Input_hash :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Sc_rollup_input_hash" in
let title := "A smart contract rollup input hash" in
let b58check_prefix := String.String "001" ("v}" ++ String.String "135" "")
in
let size_value := Some 20 in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Module Reveal_hash.
Definition V0 :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Sc_rollup_reveal_data_hash" in
let title := "A smart contract rollup reveal hash" in
let b58check_prefix :=
String.String "017"
(String.String "144"
("y" ++ String.String "209" (String.String "203" ""))) in
let size_value := Some 31 in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Init function; without side-effects in Coq
Definition init_module : unit :=
Base58.check_encoded_prefix V0.(S.HASH.b58check_encoding) "scrrh1" 54.
Base58.check_encoded_prefix V0.(S.HASH.b58check_encoding) "scrrh1" 54.
Inclusion of the module [V0]
Definition t := V0.(S.HASH.t).
Definition name := V0.(S.HASH.name).
Definition title := V0.(S.HASH.title).
Definition pp := V0.(S.HASH.pp).
Definition pp_short := V0.(S.HASH.pp_short).
Definition op_eq := V0.(S.HASH.op_eq).
Definition op_ltgt := V0.(S.HASH.op_ltgt).
Definition op_lt := V0.(S.HASH.op_lt).
Definition op_lteq := V0.(S.HASH.op_lteq).
Definition op_gteq := V0.(S.HASH.op_gteq).
Definition op_gt := V0.(S.HASH.op_gt).
Definition compare := V0.(S.HASH.compare).
Definition equal := V0.(S.HASH.equal).
Definition max := V0.(S.HASH.max).
Definition min := V0.(S.HASH.min).
Definition hash_bytes := V0.(S.HASH.hash_bytes).
Definition hash_string := V0.(S.HASH.hash_string).
Definition zero := V0.(S.HASH.zero).
Definition size_value := V0.(S.HASH.size_value).
Definition to_bytes := V0.(S.HASH.to_bytes).
Definition of_bytes_opt := V0.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := V0.(S.HASH.of_bytes_exn).
Definition to_b58check := V0.(S.HASH.to_b58check).
Definition to_short_b58check := V0.(S.HASH.to_short_b58check).
Definition of_b58check_exn := V0.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := V0.(S.HASH.of_b58check_opt).
Definition b58check_encoding := V0.(S.HASH.b58check_encoding).
Definition rpc_arg := V0.(S.HASH.rpc_arg).
Definition encoding : Data_encoding.encoding V0.(S.HASH.t) :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Reveal_data_hash_v0" None
(Data_encoding.Tag 0) V0.(S.HASH.encoding)
(fun (s_value : V0.(S.HASH.t)) ⇒ Some s_value)
(fun (s_value : V0.(S.HASH.t)) ⇒ s_value)
].
End Reveal_hash.
Inductive reveal : Set :=
| Reveal_raw_data : Reveal_hash.t → reveal
| Reveal_metadata : reveal
| Request_dal_page : Dal_slot_repr.Page.t → reveal.
Definition reveal_encoding : Data_encoding.encoding reveal :=
let case_raw_data : Data_encoding.case reveal :=
Data_encoding.case_value "Reveal_raw_data" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_kind"
(Data_encoding.constant "reveal_raw_data"))
(Data_encoding.req None None "input_hash" Reveal_hash.encoding))
(fun (function_parameter : reveal) ⇒
match function_parameter with
| Reveal_raw_data s_value ⇒ Some (tt, s_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × Reveal_hash.t) ⇒
let '(_, s_value) := function_parameter in
Reveal_raw_data s_value)
in let case_metadata : Data_encoding.case reveal :=
Data_encoding.case_value "Reveal_metadata" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "reveal_kind"
(Data_encoding.constant "reveal_metadata")))
(fun (function_parameter : reveal) ⇒
match function_parameter with
| Reveal_metadata ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Reveal_metadata) in
let case_dal_page :=
Data_encoding.case_value "Request_dal_page" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_kind"
(Data_encoding.constant "request_dal_page"))
(Data_encoding.req None None "page_id" Dal_slot_repr.Page.encoding))
(fun (function_parameter : reveal) ⇒
match function_parameter with
| Request_dal_page s_value ⇒ Some (tt, s_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × Dal_slot_repr.Page.t) ⇒
let '(_, s_value) := function_parameter in
Request_dal_page s_value) in
Data_encoding.union None [ case_raw_data; case_metadata; case_dal_page ].
Definition name := V0.(S.HASH.name).
Definition title := V0.(S.HASH.title).
Definition pp := V0.(S.HASH.pp).
Definition pp_short := V0.(S.HASH.pp_short).
Definition op_eq := V0.(S.HASH.op_eq).
Definition op_ltgt := V0.(S.HASH.op_ltgt).
Definition op_lt := V0.(S.HASH.op_lt).
Definition op_lteq := V0.(S.HASH.op_lteq).
Definition op_gteq := V0.(S.HASH.op_gteq).
Definition op_gt := V0.(S.HASH.op_gt).
Definition compare := V0.(S.HASH.compare).
Definition equal := V0.(S.HASH.equal).
Definition max := V0.(S.HASH.max).
Definition min := V0.(S.HASH.min).
Definition hash_bytes := V0.(S.HASH.hash_bytes).
Definition hash_string := V0.(S.HASH.hash_string).
Definition zero := V0.(S.HASH.zero).
Definition size_value := V0.(S.HASH.size_value).
Definition to_bytes := V0.(S.HASH.to_bytes).
Definition of_bytes_opt := V0.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := V0.(S.HASH.of_bytes_exn).
Definition to_b58check := V0.(S.HASH.to_b58check).
Definition to_short_b58check := V0.(S.HASH.to_short_b58check).
Definition of_b58check_exn := V0.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := V0.(S.HASH.of_b58check_opt).
Definition b58check_encoding := V0.(S.HASH.b58check_encoding).
Definition rpc_arg := V0.(S.HASH.rpc_arg).
Definition encoding : Data_encoding.encoding V0.(S.HASH.t) :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Reveal_data_hash_v0" None
(Data_encoding.Tag 0) V0.(S.HASH.encoding)
(fun (s_value : V0.(S.HASH.t)) ⇒ Some s_value)
(fun (s_value : V0.(S.HASH.t)) ⇒ s_value)
].
End Reveal_hash.
Inductive reveal : Set :=
| Reveal_raw_data : Reveal_hash.t → reveal
| Reveal_metadata : reveal
| Request_dal_page : Dal_slot_repr.Page.t → reveal.
Definition reveal_encoding : Data_encoding.encoding reveal :=
let case_raw_data : Data_encoding.case reveal :=
Data_encoding.case_value "Reveal_raw_data" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_kind"
(Data_encoding.constant "reveal_raw_data"))
(Data_encoding.req None None "input_hash" Reveal_hash.encoding))
(fun (function_parameter : reveal) ⇒
match function_parameter with
| Reveal_raw_data s_value ⇒ Some (tt, s_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × Reveal_hash.t) ⇒
let '(_, s_value) := function_parameter in
Reveal_raw_data s_value)
in let case_metadata : Data_encoding.case reveal :=
Data_encoding.case_value "Reveal_metadata" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "reveal_kind"
(Data_encoding.constant "reveal_metadata")))
(fun (function_parameter : reveal) ⇒
match function_parameter with
| Reveal_metadata ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Reveal_metadata) in
let case_dal_page :=
Data_encoding.case_value "Request_dal_page" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.req None None "reveal_kind"
(Data_encoding.constant "request_dal_page"))
(Data_encoding.req None None "page_id" Dal_slot_repr.Page.encoding))
(fun (function_parameter : reveal) ⇒
match function_parameter with
| Request_dal_page s_value ⇒ Some (tt, s_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × Dal_slot_repr.Page.t) ⇒
let '(_, s_value) := function_parameter in
Request_dal_page s_value) in
Data_encoding.union None [ case_raw_data; case_metadata; case_dal_page ].
The PVM's current input expectations:
[No_input_required] if the machine is busy and has no need for new input.
- [Initial] if the machine has never received an input so expects the very
first item in the inbox.
- [First_after (level, counter)] expects whatever comes next after that
position in the inbox.
- [Needs_metadata] if the machine needs the metadata to continue
its execution.
Inductive input_request : Set :=
| No_input_required : input_request
| Initial : input_request
| First_after : Raw_level_repr.t → Z.t → input_request
| Needs_reveal : reveal → input_request.
| No_input_required : input_request
| Initial : input_request
| First_after : Raw_level_repr.t → Z.t → input_request
| Needs_reveal : reveal → input_request.
[input_request_encoding] encoding value for {!input_request}.
Definition input_request_encoding : Data_encoding.encoding input_request :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "No_input_required" None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "no_input_required")))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| No_input_required ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
No_input_required);
Data_encoding.case_value "Initial" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "initial")))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| Initial ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Initial);
Data_encoding.case_value "First_after" None (Data_encoding.Tag 2)
(Data_encoding.obj3
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "first_after"))
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "counter" Data_encoding.n_value))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| First_after level counter ⇒ Some (tt, level, counter)
| _ ⇒ None
end)
(fun (function_parameter : unit × Raw_level_repr.raw_level × Z.t) ⇒
let '(_, level, counter) := function_parameter in
First_after level counter);
Data_encoding.case_value "Needs_reveal" None (Data_encoding.Tag 3)
(Data_encoding.obj2
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "needs_reveal"))
(Data_encoding.req None None "reveal" reveal_encoding))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| Needs_reveal p_value ⇒ Some (tt, p_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × reveal) ⇒
let '(_, p_value) := function_parameter in
Needs_reveal p_value)
].
Definition pp_reveal (fmt : Format.formatter) (function_parameter : reveal)
: unit :=
match function_parameter with
| Reveal_raw_data hash_value ⇒ Reveal_hash.pp fmt hash_value
| Reveal_metadata ⇒ Format.pp_print_string fmt "Reveal metadata"
| Request_dal_page id ⇒ Dal_slot_repr.Page.pp fmt id
end.
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "No_input_required" None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "no_input_required")))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| No_input_required ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
No_input_required);
Data_encoding.case_value "Initial" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "initial")))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| Initial ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Initial);
Data_encoding.case_value "First_after" None (Data_encoding.Tag 2)
(Data_encoding.obj3
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "first_after"))
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "counter" Data_encoding.n_value))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| First_after level counter ⇒ Some (tt, level, counter)
| _ ⇒ None
end)
(fun (function_parameter : unit × Raw_level_repr.raw_level × Z.t) ⇒
let '(_, level, counter) := function_parameter in
First_after level counter);
Data_encoding.case_value "Needs_reveal" None (Data_encoding.Tag 3)
(Data_encoding.obj2
(Data_encoding.req None None "input_request_kind"
(Data_encoding.constant "needs_reveal"))
(Data_encoding.req None None "reveal" reveal_encoding))
(fun (function_parameter : input_request) ⇒
match function_parameter with
| Needs_reveal p_value ⇒ Some (tt, p_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × reveal) ⇒
let '(_, p_value) := function_parameter in
Needs_reveal p_value)
].
Definition pp_reveal (fmt : Format.formatter) (function_parameter : reveal)
: unit :=
match function_parameter with
| Reveal_raw_data hash_value ⇒ Reveal_hash.pp fmt hash_value
| Reveal_metadata ⇒ Format.pp_print_string fmt "Reveal metadata"
| Request_dal_page id ⇒ Dal_slot_repr.Page.pp fmt id
end.
[pp_input_request fmt i] pretty prints the given input [i] to the formatter
[fmt].
Definition pp_input_request (fmt : Format.formatter) (request : input_request)
: unit :=
match request with
| No_input_required ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "No_input_required"
CamlinternalFormatBasics.End_of_format) "No_input_required")
| Initial ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Initial"
CamlinternalFormatBasics.End_of_format) "Initial")
| First_after l_value n_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "First_after (level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", counter = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"First_after (level = %a, counter = %a)") Raw_level_repr.pp l_value
Z.pp_print n_value
| Needs_reveal reveal ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Needs reveal of "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"Needs reveal of %a") pp_reveal reveal
end.
Definition reveal_equal (p1 : reveal) (p2 : reveal) : bool :=
match (p1, p2) with
| (Reveal_raw_data h1, Reveal_raw_data h2) ⇒ Reveal_hash.equal h1 h2
| (Reveal_metadata, Reveal_metadata) ⇒ true
| (Request_dal_page a_value, Request_dal_page b_value) ⇒
Dal_slot_repr.Page.equal a_value b_value
| ((Reveal_raw_data _ | Reveal_metadata | Request_dal_page _), _) ⇒ false
end.
: unit :=
match request with
| No_input_required ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "No_input_required"
CamlinternalFormatBasics.End_of_format) "No_input_required")
| Initial ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Initial"
CamlinternalFormatBasics.End_of_format) "Initial")
| First_after l_value n_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "First_after (level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", counter = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"First_after (level = %a, counter = %a)") Raw_level_repr.pp l_value
Z.pp_print n_value
| Needs_reveal reveal ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Needs reveal of "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"Needs reveal of %a") pp_reveal reveal
end.
Definition reveal_equal (p1 : reveal) (p2 : reveal) : bool :=
match (p1, p2) with
| (Reveal_raw_data h1, Reveal_raw_data h2) ⇒ Reveal_hash.equal h1 h2
| (Reveal_metadata, Reveal_metadata) ⇒ true
| (Request_dal_page a_value, Request_dal_page b_value) ⇒
Dal_slot_repr.Page.equal a_value b_value
| ((Reveal_raw_data _ | Reveal_metadata | Request_dal_page _), _) ⇒ false
end.
[input_request_equal i1 i2] return whether [i1] and [i2] are equal.
Definition input_request_equal
(a_value : input_request) (b_value : input_request) : bool :=
match (a_value, b_value) with
| (No_input_required, No_input_required) ⇒ true
| (No_input_required, _) ⇒ false
| (Initial, Initial) ⇒ true
| (Initial, _) ⇒ false
| (First_after l_value n_value, First_after m_value o_value) ⇒
(Raw_level_repr.equal l_value m_value) && (Z.equal n_value o_value)
| (First_after _ _, _) ⇒ false
| (Needs_reveal p1, Needs_reveal p2) ⇒ reveal_equal p1 p2
| (Needs_reveal _, _) ⇒ false
end.
(a_value : input_request) (b_value : input_request) : bool :=
match (a_value, b_value) with
| (No_input_required, No_input_required) ⇒ true
| (No_input_required, _) ⇒ false
| (Initial, Initial) ⇒ true
| (Initial, _) ⇒ false
| (First_after l_value n_value, First_after m_value o_value) ⇒
(Raw_level_repr.equal l_value m_value) && (Z.equal n_value o_value)
| (First_after _ _, _) ⇒ false
| (Needs_reveal p1, Needs_reveal p2) ⇒ reveal_equal p1 p2
| (Needs_reveal _, _) ⇒ false
end.
Type that describes output values.
Module output.
Record record : Set := Build {
outbox_level : Raw_level_repr.t;
message_index : Z.t;
message : Sc_rollup_outbox_message_repr.t;
}.
Definition with_outbox_level outbox_level (r : record) :=
Build outbox_level r.(message_index) r.(message).
Definition with_message_index message_index (r : record) :=
Build r.(outbox_level) message_index r.(message).
Definition with_message message (r : record) :=
Build r.(outbox_level) r.(message_index) message.
End output.
Definition output := output.record.
Record record : Set := Build {
outbox_level : Raw_level_repr.t;
message_index : Z.t;
message : Sc_rollup_outbox_message_repr.t;
}.
Definition with_outbox_level outbox_level (r : record) :=
Build outbox_level r.(message_index) r.(message).
Definition with_message_index message_index (r : record) :=
Build r.(outbox_level) message_index r.(message).
Definition with_message message (r : record) :=
Build r.(outbox_level) r.(message_index) message.
End output.
Definition output := output.record.
[output_encoding] encoding value for {!output}.
Definition output_encoding : Data_encoding.encoding output :=
Data_encoding.conv
(fun (function_parameter : output) ⇒
let '{|
output.outbox_level := outbox_level;
output.message_index := message_index;
output.message := message
|} := function_parameter in
(outbox_level, message_index, message))
(fun (function_parameter :
Raw_level_repr.t × Z.t × Sc_rollup_outbox_message_repr.t) ⇒
let '(outbox_level, message_index, message) := function_parameter in
{| output.outbox_level := outbox_level;
output.message_index := message_index; output.message := message; |})
None
(Data_encoding.obj3
(Data_encoding.req None None "outbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "message_index" Data_encoding.n_value)
(Data_encoding.req None None "message"
Sc_rollup_outbox_message_repr.encoding)).
Data_encoding.conv
(fun (function_parameter : output) ⇒
let '{|
output.outbox_level := outbox_level;
output.message_index := message_index;
output.message := message
|} := function_parameter in
(outbox_level, message_index, message))
(fun (function_parameter :
Raw_level_repr.t × Z.t × Sc_rollup_outbox_message_repr.t) ⇒
let '(outbox_level, message_index, message) := function_parameter in
{| output.outbox_level := outbox_level;
output.message_index := message_index; output.message := message; |})
None
(Data_encoding.obj3
(Data_encoding.req None None "outbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "message_index" Data_encoding.n_value)
(Data_encoding.req None None "message"
Sc_rollup_outbox_message_repr.encoding)).
[pp_output fmt o] pretty prints the given output [o] to the formatter
[fmt].
Definition pp_output (fmt : Format.formatter) (function_parameter : output)
: unit :=
let '{|
output.outbox_level := outbox_level;
output.message_index := message_index;
output.message := message
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))))
"@[%a@;%a@;%a@;@]") Raw_level_repr.pp outbox_level Z.pp_print
message_index Sc_rollup_outbox_message_repr.pp message.
Module S.
Record signature {state context proof output_proof : Set} : Set := {
: unit :=
let '{|
output.outbox_level := outbox_level;
output.message_index := message_index;
output.message := message
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))))
"@[%a@;%a@;%a@;@]") Raw_level_repr.pp outbox_level Z.pp_print
message_index Sc_rollup_outbox_message_repr.pp message.
Module S.
Record signature {state context proof output_proof : Set} : Set := {
The state of the PVM denotes a state of the rollup.
The life cycle of the PVM is as follows. It starts its execution
from an {!initial_state}. The initial state is specialized at
origination with a [boot_sector], using the
{!install_boot_sector} function. The resulting state is call the
“genesis” of the rollup.
Afterwards, we classify states into two categories: "internal\n states" do not require any external information to be executed
while "input states" are waiting for some information from the
inbox to be executable.
A [context] represents the executable environment needed by the state to
exist. Typically, the rollup node storage can be part of this context to
allow the PVM state to be persistent.
A [hash] characterizes the contents of a state.
During interactive refutation games, a player may need to provide a proof
that a given execution step is valid. The PVM implementation is
responsible for ensuring that this proof type has the correct semantics.
A proof [p] has four parameters:
- [start_hash := proof_start_state p]
[stop_hash := proof_stop_state p]
[input_requested := proof_input_requested p]
[input_given := proof_input_given p]
The following predicate must hold of a valid proof:
[exists start_state, stop_state.
(state_hash start_state == start_hash)
AND (Option.map state_hash stop_state == stop_hash)
AND (is_input_state start_state == input_requested)
AND (match (input_given, input_requested) with
| (None, No_input_required) -> eval start_state == stop_state
| (None, Initial) -> stop_state == None
| (None, First_after (l, n)) -> stop_state == None
| (Some input, No_input_required) -> true
| (Some input, Initial) ->
set_input input_given start_state == stop_state
| (Some input, First_after (l, n)) ->
set_input input_given start_state == stop_state)]
In natural language---the two hash parameters [start_hash] and [stop_hash]
must have actual [state] values (or possibly [None] in the case of
[stop_hash]) of which they are the hashes. The [input_requested] parameter
must be the correct request from the [start_hash], given according to
[is_input_state]. Finally there are four possibilities of [input_requested]
and [input_given].
- if no input is required, or given, the proof is a simple [eval]
step ;
if input was required but not given, the [stop_hash] must be
[None] (the machine is blocked) ;
if no input was required but some was given, this makes no sense
and it doesn't matter if the proof is valid or invalid (this
case will be ruled out by the inbox proof anyway) ;
finally, if input was required and given, the proof is a
[set_input] step.
[proof]s are embedded in L1 refutation game operations using
[proof_encoding]. Given that the size of L1 operations are limited, it is
of *critical* importance to make sure that no execution step of the PVM
can generate proofs that do not fit in L1 operations when encoded. If such
a proof existed, the rollup could get stuck.
[proof_start_state proof] returns the initial state hash of the [proof]
execution step.
[proof_stop_state proof] returns the final state hash of the [proof]
execution step.
[state_hash state] returns a compressed representation of [state].
[initial_state ~empty] is the initial state of the PVM, before its
specialization with a given [boot_sector]. The initial state is built on
the [empty] state which must be provided.
[install_boot_sector state boot_sector] specializes the initial
[state] of a PVM using a dedicated [boot_sector], submitted at
the origination of the rollup.
[is_input_state state] returns the input expectations of the
[state]---does it need input, and if so, how far through the inbox
has it read so far?
[set_input input state] sets [input] in [state] as the next
input to be processed. This must answer the [input_request]
from [is_input_state state].
[eval s0] returns a state [s1] resulting from the
execution of an atomic step of the rollup at state [s0].
[verify_proof input p] checks the proof [p] with input [input] and returns
the [input_request] before the evaluation of the proof. See the doc-string
for the [proof] type.
[verify_proof input p] fails when the proof is invalid in regards to the
given input.
[produce_proof ctxt input_given state] should return a [proof] for
the PVM step starting from [state], if possible. This may fail for
a few reasons:
the [input_given] doesn't match the expectations of [state] ;
the [context] for this instance of the PVM doesn't have access
to enough of the [state] to build the proof.
[verify_origination_proof proof boot_sector] verifies a proof
supposedly generated by [produce_origination_proof].
[produce_origination_proof context boot_sector] produces a proof
[p] covering the specialization of a PVM, from the
[initial_state] up to the genesis state wherein the
[boot_sector] has been installed.
The following type is inhabited by the proofs that a given [output]
is part of the outbox of a given [state].
[output_proof_encoding] encoding value for [output_proof]s.
[output_of_output_proof proof] returns the [output] that is referred to in
[proof]'s statement.
[state_of_output_proof proof] returns the [state] hash that is referred to
in [proof]'s statement.
[verify_output_proof output_proof] returns [true] iff [proof] is a valid
witness that its [output] is part of its [state]'s outbox.
[produce_output_proof ctxt state output] returns a proof that witnesses
the fact that [output] is part of [state]'s outbox.
produce_output_proof :
context → state → output →
Pervasives.result output_proof Error_monad._error;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _}.
context → state → output →
Pervasives.result output_proof Error_monad._error;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _}.