🦏 Sc_rollup_game_repr.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.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_dissection_chunk_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Module Proof_start_state_hash_mismatch.
Record record : Set := Build {
start_state_hash : option Sc_rollup_repr.State_hash.t;
start_proof : Sc_rollup_repr.State_hash.t;
}.
Definition with_start_state_hash start_state_hash (r : record) :=
Build start_state_hash r.(start_proof).
Definition with_start_proof start_proof (r : record) :=
Build r.(start_state_hash) start_proof.
End Proof_start_state_hash_mismatch.
Definition Proof_start_state_hash_mismatch :=
Proof_start_state_hash_mismatch.record.
Module Proof_stop_state_hash_failed_to_refute.
Record record : Set := Build {
stop_state_hash : option Sc_rollup_repr.State_hash.t;
stop_proof : option Sc_rollup_repr.State_hash.t;
}.
Definition with_stop_state_hash stop_state_hash (r : record) :=
Build stop_state_hash r.(stop_proof).
Definition with_stop_proof stop_proof (r : record) :=
Build r.(stop_state_hash) stop_proof.
End Proof_stop_state_hash_failed_to_refute.
Definition Proof_stop_state_hash_failed_to_refute :=
Proof_stop_state_hash_failed_to_refute.record.
Module Proof_stop_state_hash_failed_to_validate.
Record record : Set := Build {
stop_state_hash : option Sc_rollup_repr.State_hash.t;
stop_proof : option Sc_rollup_repr.State_hash.t;
}.
Definition with_stop_state_hash stop_state_hash (r : record) :=
Build stop_state_hash r.(stop_proof).
Definition with_stop_proof stop_proof (r : record) :=
Build r.(stop_state_hash) stop_proof.
End Proof_stop_state_hash_failed_to_validate.
Definition Proof_stop_state_hash_failed_to_validate :=
Proof_stop_state_hash_failed_to_validate.record.
Definition pp_hash_opt
(fmt : Format.formatter)
(function_parameter : option Sc_rollup_repr.State_hash.t) : unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "None"
CamlinternalFormatBasics.End_of_format) "None")
| Some x_value ⇒ Sc_rollup_repr.State_hash.pp fmt x_value
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_dissection_chunk_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Module Proof_start_state_hash_mismatch.
Record record : Set := Build {
start_state_hash : option Sc_rollup_repr.State_hash.t;
start_proof : Sc_rollup_repr.State_hash.t;
}.
Definition with_start_state_hash start_state_hash (r : record) :=
Build start_state_hash r.(start_proof).
Definition with_start_proof start_proof (r : record) :=
Build r.(start_state_hash) start_proof.
End Proof_start_state_hash_mismatch.
Definition Proof_start_state_hash_mismatch :=
Proof_start_state_hash_mismatch.record.
Module Proof_stop_state_hash_failed_to_refute.
Record record : Set := Build {
stop_state_hash : option Sc_rollup_repr.State_hash.t;
stop_proof : option Sc_rollup_repr.State_hash.t;
}.
Definition with_stop_state_hash stop_state_hash (r : record) :=
Build stop_state_hash r.(stop_proof).
Definition with_stop_proof stop_proof (r : record) :=
Build r.(stop_state_hash) stop_proof.
End Proof_stop_state_hash_failed_to_refute.
Definition Proof_stop_state_hash_failed_to_refute :=
Proof_stop_state_hash_failed_to_refute.record.
Module Proof_stop_state_hash_failed_to_validate.
Record record : Set := Build {
stop_state_hash : option Sc_rollup_repr.State_hash.t;
stop_proof : option Sc_rollup_repr.State_hash.t;
}.
Definition with_stop_state_hash stop_state_hash (r : record) :=
Build stop_state_hash r.(stop_proof).
Definition with_stop_proof stop_proof (r : record) :=
Build r.(stop_state_hash) stop_proof.
End Proof_stop_state_hash_failed_to_validate.
Definition Proof_stop_state_hash_failed_to_validate :=
Proof_stop_state_hash_failed_to_validate.record.
Definition pp_hash_opt
(fmt : Format.formatter)
(function_parameter : option Sc_rollup_repr.State_hash.t) : unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "None"
CamlinternalFormatBasics.End_of_format) "None")
| Some x_value ⇒ Sc_rollup_repr.State_hash.pp fmt x_value
end.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
let description := "Dissection choice not found" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Dissection_choice_not_found" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (choice : Sc_rollup_tick_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"No section starting with tick "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " found"
CamlinternalFormatBasics.End_of_format)))
"No section starting with tick %a found") Sc_rollup_tick_repr.pp
choice))
(Data_encoding.obj1
(Data_encoding.req None None "choice" Sc_rollup_tick_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Dissection_choice_not_found" then
let tick := cast Sc_rollup_tick_repr.t payload in
Some tick
else None
end)
(fun (tick : Sc_rollup_tick_repr.t) ⇒
Build_extensible "Dissection_choice_not_found" Sc_rollup_tick_repr.t
tick) in
let description := "The distance for a proof should be equal to 1" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Dissection_unexpected_section_size" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (n_value : Z.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Distance should be equal to 1 in a proof, but got "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"Distance should be equal to 1 in a proof, but got %a")
Z.pp_print n_value))
(Data_encoding.obj1
(Data_encoding.req None None "n" Data_encoding.n_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_unexpected_section_size" then
let n_value := cast Z.t payload in
Some n_value
else None
end)
(fun (n_value : Z.t) ⇒
Build_extensible "Proof_unexpected_section_size" Z.t n_value) in
let description := "The start state hash of the proof is invalid" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Proof_start_state_hash_mismatch" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
option Sc_rollup_repr.State_hash.t × Sc_rollup_repr.State_hash.t) ⇒
let '(start_state_hash, start_proof) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "start("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
") should be equal to start_proof("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"start(%a) should be equal to start_proof(%a)") pp_hash_opt
start_state_hash Sc_rollup_repr.State_hash.pp start_proof))
(Data_encoding.obj2
(Data_encoding.req None None "start_state_hash"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
(Data_encoding.req None None "start_proof"
Sc_rollup_repr.State_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_start_state_hash_mismatch" then
let '{|
Proof_start_state_hash_mismatch.start_state_hash := start_state_hash;
Proof_start_state_hash_mismatch.start_proof := start_proof
|} := cast Proof_start_state_hash_mismatch payload in
Some (start_state_hash, start_proof)
else None
end)
(fun (function_parameter :
option Sc_rollup_repr.State_hash.t × Sc_rollup_repr.State_hash.t) ⇒
let '(start_state_hash, start_proof) := function_parameter in
Build_extensible "Proof_start_state_hash_mismatch"
Proof_start_state_hash_mismatch
{|
Proof_start_state_hash_mismatch.start_state_hash :=
start_state_hash;
Proof_start_state_hash_mismatch.start_proof := start_proof; |}) in
let description := "Failed to refute the stop state hash with the proof" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Proof_stop_state_hash_failed_to_refute" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
option Sc_rollup_repr.State_hash.t ×
option Sc_rollup_repr.State_hash.t) ⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Trying to refute "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", the stop_proof must not be equal to "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"Trying to refute %a, the stop_proof must not be equal to %a")
pp_hash_opt stop_state_hash pp_hash_opt stop_proof))
(Data_encoding.obj2
(Data_encoding.req None None "stop_state_hash"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
(Data_encoding.req None None "stop_proof"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_stop_state_hash_failed_to_refute" then
let '{|
Proof_stop_state_hash_failed_to_refute.stop_state_hash := stop_state_hash;
Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof
|} := cast Proof_stop_state_hash_failed_to_refute payload in
Some (stop_state_hash, stop_proof)
else None
end)
(fun (function_parameter :
option Sc_rollup_repr.State_hash.t × option Sc_rollup_repr.State_hash.t)
⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Build_extensible "Proof_stop_state_hash_failed_to_refute"
Proof_stop_state_hash_failed_to_refute
{|
Proof_stop_state_hash_failed_to_refute.stop_state_hash :=
stop_state_hash;
Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof; |})
in
let description := "Failed to validate the stop state hash with the proof" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Proof_stop_state_hash_failed_to_validate" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
option Sc_rollup_repr.State_hash.t ×
option Sc_rollup_repr.State_hash.t) ⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Trying to validate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", the stop_proof must not be equal to "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"Trying to validate %a, the stop_proof must not be equal to %a")
pp_hash_opt stop_state_hash pp_hash_opt stop_proof))
(Data_encoding.obj2
(Data_encoding.req None None "stop_state_hash"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
(Data_encoding.req None None "stop_proof"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_stop_state_hash_failed_to_validate" then
let '{|
Proof_stop_state_hash_failed_to_validate.stop_state_hash := stop_state_hash;
Proof_stop_state_hash_failed_to_validate.stop_proof :=
stop_proof
|} := cast Proof_stop_state_hash_failed_to_validate payload in
Some (stop_state_hash, stop_proof)
else None
end)
(fun (function_parameter :
option Sc_rollup_repr.State_hash.t × option Sc_rollup_repr.State_hash.t)
⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Build_extensible "Proof_stop_state_hash_failed_to_validate"
Proof_stop_state_hash_failed_to_validate
{|
Proof_stop_state_hash_failed_to_validate.stop_state_hash :=
stop_state_hash;
Proof_stop_state_hash_failed_to_validate.stop_proof := stop_proof;
|}) in
let description := "Tried to play a dissecting when the final move started" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Dissecting_during_final_move" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Dissecting_during_final_move" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Dissecting_during_final_move" unit tt) in
tt.
Inductive player : Set :=
| Alice : player
| Bob : player.
Module V1.
Definition dissection_chunk : Set := Sc_rollup_dissection_chunk_repr.t.
let description := "Dissection choice not found" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Dissection_choice_not_found" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (choice : Sc_rollup_tick_repr.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"No section starting with tick "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " found"
CamlinternalFormatBasics.End_of_format)))
"No section starting with tick %a found") Sc_rollup_tick_repr.pp
choice))
(Data_encoding.obj1
(Data_encoding.req None None "choice" Sc_rollup_tick_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Dissection_choice_not_found" then
let tick := cast Sc_rollup_tick_repr.t payload in
Some tick
else None
end)
(fun (tick : Sc_rollup_tick_repr.t) ⇒
Build_extensible "Dissection_choice_not_found" Sc_rollup_tick_repr.t
tick) in
let description := "The distance for a proof should be equal to 1" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Dissection_unexpected_section_size" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (n_value : Z.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Distance should be equal to 1 in a proof, but got "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"Distance should be equal to 1 in a proof, but got %a")
Z.pp_print n_value))
(Data_encoding.obj1
(Data_encoding.req None None "n" Data_encoding.n_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_unexpected_section_size" then
let n_value := cast Z.t payload in
Some n_value
else None
end)
(fun (n_value : Z.t) ⇒
Build_extensible "Proof_unexpected_section_size" Z.t n_value) in
let description := "The start state hash of the proof is invalid" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Proof_start_state_hash_mismatch" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
option Sc_rollup_repr.State_hash.t × Sc_rollup_repr.State_hash.t) ⇒
let '(start_state_hash, start_proof) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "start("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
") should be equal to start_proof("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"start(%a) should be equal to start_proof(%a)") pp_hash_opt
start_state_hash Sc_rollup_repr.State_hash.pp start_proof))
(Data_encoding.obj2
(Data_encoding.req None None "start_state_hash"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
(Data_encoding.req None None "start_proof"
Sc_rollup_repr.State_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_start_state_hash_mismatch" then
let '{|
Proof_start_state_hash_mismatch.start_state_hash := start_state_hash;
Proof_start_state_hash_mismatch.start_proof := start_proof
|} := cast Proof_start_state_hash_mismatch payload in
Some (start_state_hash, start_proof)
else None
end)
(fun (function_parameter :
option Sc_rollup_repr.State_hash.t × Sc_rollup_repr.State_hash.t) ⇒
let '(start_state_hash, start_proof) := function_parameter in
Build_extensible "Proof_start_state_hash_mismatch"
Proof_start_state_hash_mismatch
{|
Proof_start_state_hash_mismatch.start_state_hash :=
start_state_hash;
Proof_start_state_hash_mismatch.start_proof := start_proof; |}) in
let description := "Failed to refute the stop state hash with the proof" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Proof_stop_state_hash_failed_to_refute" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
option Sc_rollup_repr.State_hash.t ×
option Sc_rollup_repr.State_hash.t) ⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Trying to refute "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", the stop_proof must not be equal to "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"Trying to refute %a, the stop_proof must not be equal to %a")
pp_hash_opt stop_state_hash pp_hash_opt stop_proof))
(Data_encoding.obj2
(Data_encoding.req None None "stop_state_hash"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
(Data_encoding.req None None "stop_proof"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_stop_state_hash_failed_to_refute" then
let '{|
Proof_stop_state_hash_failed_to_refute.stop_state_hash := stop_state_hash;
Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof
|} := cast Proof_stop_state_hash_failed_to_refute payload in
Some (stop_state_hash, stop_proof)
else None
end)
(fun (function_parameter :
option Sc_rollup_repr.State_hash.t × option Sc_rollup_repr.State_hash.t)
⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Build_extensible "Proof_stop_state_hash_failed_to_refute"
Proof_stop_state_hash_failed_to_refute
{|
Proof_stop_state_hash_failed_to_refute.stop_state_hash :=
stop_state_hash;
Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof; |})
in
let description := "Failed to validate the stop state hash with the proof" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Proof_stop_state_hash_failed_to_validate" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
option Sc_rollup_repr.State_hash.t ×
option Sc_rollup_repr.State_hash.t) ⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Trying to validate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", the stop_proof must not be equal to "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"Trying to validate %a, the stop_proof must not be equal to %a")
pp_hash_opt stop_state_hash pp_hash_opt stop_proof))
(Data_encoding.obj2
(Data_encoding.req None None "stop_state_hash"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
(Data_encoding.req None None "stop_proof"
(Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proof_stop_state_hash_failed_to_validate" then
let '{|
Proof_stop_state_hash_failed_to_validate.stop_state_hash := stop_state_hash;
Proof_stop_state_hash_failed_to_validate.stop_proof :=
stop_proof
|} := cast Proof_stop_state_hash_failed_to_validate payload in
Some (stop_state_hash, stop_proof)
else None
end)
(fun (function_parameter :
option Sc_rollup_repr.State_hash.t × option Sc_rollup_repr.State_hash.t)
⇒
let '(stop_state_hash, stop_proof) := function_parameter in
Build_extensible "Proof_stop_state_hash_failed_to_validate"
Proof_stop_state_hash_failed_to_validate
{|
Proof_stop_state_hash_failed_to_validate.stop_state_hash :=
stop_state_hash;
Proof_stop_state_hash_failed_to_validate.stop_proof := stop_proof;
|}) in
let description := "Tried to play a dissecting when the final move started" in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Dissecting_during_final_move" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Dissecting_during_final_move" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Dissecting_during_final_move" unit tt) in
tt.
Inductive player : Set :=
| Alice : player
| Bob : player.
Module V1.
Definition dissection_chunk : Set := Sc_rollup_dissection_chunk_repr.t.
Records for the constructor parameters
Module ConstructorRecords_game_state.
Module game_state.
Module Dissecting.
Record record {dissection default_number_of_sections : Set} : Set := Build {
dissection : dissection;
default_number_of_sections : default_number_of_sections;
}.
Arguments record : clear implicits.
Definition with_dissection {t_dissection t_default_number_of_sections}
dissection (r : record t_dissection t_default_number_of_sections) :=
Build t_dissection t_default_number_of_sections dissection
r.(default_number_of_sections).
Definition with_default_number_of_sections
{t_dissection t_default_number_of_sections} default_number_of_sections
(r : record t_dissection t_default_number_of_sections) :=
Build t_dissection t_default_number_of_sections r.(dissection)
default_number_of_sections.
End Dissecting.
Definition Dissecting_skeleton := Dissecting.record.
Module Final_move.
Record record {agreed_start_chunk refuted_stop_chunk : Set} : Set := Build {
agreed_start_chunk : agreed_start_chunk;
refuted_stop_chunk : refuted_stop_chunk;
}.
Arguments record : clear implicits.
Definition with_agreed_start_chunk
{t_agreed_start_chunk t_refuted_stop_chunk} agreed_start_chunk
(r : record t_agreed_start_chunk t_refuted_stop_chunk) :=
Build t_agreed_start_chunk t_refuted_stop_chunk agreed_start_chunk
r.(refuted_stop_chunk).
Definition with_refuted_stop_chunk
{t_agreed_start_chunk t_refuted_stop_chunk} refuted_stop_chunk
(r : record t_agreed_start_chunk t_refuted_stop_chunk) :=
Build t_agreed_start_chunk t_refuted_stop_chunk r.(agreed_start_chunk)
refuted_stop_chunk.
End Final_move.
Definition Final_move_skeleton := Final_move.record.
End game_state.
End ConstructorRecords_game_state.
Import ConstructorRecords_game_state.
Reserved Notation "'game_state.Dissecting".
Reserved Notation "'game_state.Final_move".
Inductive game_state : Set :=
| Dissecting : 'game_state.Dissecting → game_state
| Final_move : 'game_state.Final_move → game_state
where "'game_state.Dissecting" :=
(game_state.Dissecting_skeleton (list dissection_chunk) int)
and "'game_state.Final_move" :=
(game_state.Final_move_skeleton dissection_chunk dissection_chunk).
Module game_state.
Include ConstructorRecords_game_state.game_state.
Definition Dissecting := 'game_state.Dissecting.
Definition Final_move := 'game_state.Final_move.
End game_state.
Module t.
Record record : Set := Build {
turn : player;
inbox_snapshot : Sc_rollup_inbox_repr.history_proof;
dal_snapshot : Dal_slot_repr.History.t;
start_level : Raw_level_repr.t;
inbox_level : Raw_level_repr.t;
pvm_name : string;
game_state : game_state;
}.
Definition with_turn turn (r : record) :=
Build turn r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_inbox_snapshot inbox_snapshot (r : record) :=
Build r.(turn) inbox_snapshot r.(dal_snapshot) r.(start_level)
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_dal_snapshot dal_snapshot (r : record) :=
Build r.(turn) r.(inbox_snapshot) dal_snapshot r.(start_level)
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_start_level start_level (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) start_level
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_inbox_level inbox_level (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
inbox_level r.(pvm_name) r.(game_state).
Definition with_pvm_name pvm_name (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
r.(inbox_level) pvm_name r.(game_state).
Definition with_game_state game_state (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
r.(inbox_level) r.(pvm_name) game_state.
End t.
Definition t := t.record.
Definition player_encoding : Data_encoding.encoding player :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Alice" None (Data_encoding.Tag 0)
(Data_encoding.constant "alice")
(fun (function_parameter : player) ⇒
match function_parameter with
| Alice ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alice);
Data_encoding.case_value "Bob" None (Data_encoding.Tag 1)
(Data_encoding.constant "bob")
(fun (function_parameter : player) ⇒
match function_parameter with
| Bob ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Bob)
].
Definition player_equal (p1 : player) (p2 : player) : bool :=
match (p1, p2) with
| (Alice, Alice) ⇒ true
| (Bob, Bob) ⇒ true
| (_, _) ⇒ false
end.
Definition game_state_equal (gs1 : game_state) (gs2 : game_state) : bool :=
match (gs1, gs2) with
|
(Dissecting {|
game_state.Dissecting.dissection := dissection1;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections1
|},
Dissecting {|
game_state.Dissecting.dissection := dissection2;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections2
|}) ⇒
(Compare.Int.equal default_number_of_sections1 default_number_of_sections2)
&&
(List.equal Sc_rollup_dissection_chunk_repr.equal dissection1 dissection2)
| (Dissecting _, _) ⇒ false
|
(Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk1;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk1
|},
Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk2;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk2
|}) ⇒
(Sc_rollup_dissection_chunk_repr.equal agreed_start_chunk1
agreed_start_chunk2) &&
(Sc_rollup_dissection_chunk_repr.equal refuted_stop_chunk1
refuted_stop_chunk2)
| (Final_move _, _) ⇒ false
end.
Definition equal (function_parameter : t) : t → bool :=
let '{|
t.turn := turn;
t.inbox_snapshot := inbox_snapshot;
t.dal_snapshot := dal_snapshot;
t.start_level := start_level;
t.inbox_level := inbox_level;
t.pvm_name := pvm_name;
t.game_state := game_state
|} := function_parameter in
fun (g2 : t) ⇒
(player_equal turn g2.(t.turn)) &&
((Sc_rollup_inbox_repr.equal_history_proof inbox_snapshot
g2.(t.inbox_snapshot)) &&
((Dal_slot_repr.History.equal dal_snapshot g2.(t.dal_snapshot)) &&
((Raw_level_repr.equal start_level g2.(t.start_level)) &&
((Raw_level_repr.equal inbox_level g2.(t.inbox_level)) &&
((String.equal pvm_name g2.(t.pvm_name)) &&
(game_state_equal game_state g2.(t.game_state))))))).
Definition string_of_player (function_parameter : player) : string :=
match function_parameter with
| Alice ⇒ "alice"
| Bob ⇒ "bob"
end.
Definition pp_player (ppf : Format.formatter) (player_value : player)
: unit := Format.pp_print_string ppf (string_of_player player_value).
Definition opponent (function_parameter : player) : player :=
match function_parameter with
| Alice ⇒ Bob
| Bob ⇒ Alice
end.
Definition dissection_encoding
: Data_encoding.encoding (list Sc_rollup_dissection_chunk_repr.t) :=
Data_encoding.list_value None Sc_rollup_dissection_chunk_repr.encoding.
Definition game_state_encoding : Data_encoding.encoding game_state :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Dissecting" None (Data_encoding.Tag 0)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "Dissecting"))
(Data_encoding.req None None "dissection"
dissection_encoding)
(Data_encoding.req None None "default_number_of_sections"
Data_encoding.uint8))
(fun (function_parameter : game_state) ⇒
match function_parameter with
|
Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections
:=
default_number_of_sections
|} ⇒
Some (tt, dissection, default_number_of_sections)
| _ ⇒ None
end)
(fun (function_parameter :
unit × list Sc_rollup_dissection_chunk_repr.t × int) ⇒
let '(_, dissection, default_number_of_sections) :=
function_parameter in
Dissecting
{| game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections
:= default_number_of_sections; |});
Data_encoding.case_value "Final_move" None (Data_encoding.Tag 1)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "Final_move"))
(Data_encoding.req None None "agreed_start_chunk"
Sc_rollup_dissection_chunk_repr.encoding)
(Data_encoding.req None None "refuted_stop_chunk"
Sc_rollup_dissection_chunk_repr.encoding))
(fun (function_parameter : game_state) ⇒
match function_parameter with
|
Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk
:=
refuted_stop_chunk
|} ⇒
Some (tt, agreed_start_chunk, refuted_stop_chunk)
| _ ⇒ None
end)
(fun (function_parameter :
unit × Sc_rollup_dissection_chunk_repr.t ×
Sc_rollup_dissection_chunk_repr.t) ⇒
let '(_, agreed_start_chunk, refuted_stop_chunk) :=
function_parameter in
Final_move
{|
game_state.Final_move.agreed_start_chunk :=
agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk :=
refuted_stop_chunk; |})
].
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.turn := turn;
t.inbox_snapshot := inbox_snapshot;
t.dal_snapshot := dal_snapshot;
t.start_level := start_level;
t.inbox_level := inbox_level;
t.pvm_name := pvm_name;
t.game_state := game_state
|} := function_parameter in
(turn, inbox_snapshot, dal_snapshot, start_level, inbox_level, pvm_name,
game_state))
(fun (function_parameter :
player × Sc_rollup_inbox_repr.history_proof × Dal_slot_repr.History.t ×
Raw_level_repr.t × Raw_level_repr.t × string × game_state) ⇒
let
'(turn, inbox_snapshot, dal_snapshot, start_level, inbox_level,
pvm_name, game_state) := function_parameter in
{| t.turn := turn; t.inbox_snapshot := inbox_snapshot;
t.dal_snapshot := dal_snapshot; t.start_level := start_level;
t.inbox_level := inbox_level; t.pvm_name := pvm_name;
t.game_state := game_state; |}) None
(Data_encoding.obj7 (Data_encoding.req None None "turn" player_encoding)
(Data_encoding.req None None "inbox_snapshot"
Sc_rollup_inbox_repr.history_proof_encoding)
(Data_encoding.req None None "dal_snapshot"
Dal_slot_repr.History.encoding)
(Data_encoding.req None None "start_level" Raw_level_repr.encoding)
(Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "pvm_name" Data_encoding.string_value)
(Data_encoding.req None None "game_state" game_state_encoding)).
Definition pp_dissection
(ppf : Format.formatter) (d_value : list Sc_rollup_dissection_chunk_repr.t)
: unit :=
Format.pp_print_list
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf (";" ++ String.String "010" "")))
Sc_rollup_dissection_chunk_repr.pp ppf d_value.
Definition pp_game_state (ppf : Format.formatter) (game_state : game_state)
: unit :=
match game_state with
|
Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections
|} ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Dissecting "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " using "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " number of sections"
CamlinternalFormatBasics.End_of_format)))))
"Dissecting %a using %d number of sections") pp_dissection dissection
default_number_of_sections
|
Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk
|} ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Final move to refute "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " from "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", opponent failed to refute"
CamlinternalFormatBasics.End_of_format)))))
"Final move to refute %a from %a, opponent failed to refute")
Sc_rollup_dissection_chunk_repr.pp agreed_start_chunk
Sc_rollup_dissection_chunk_repr.pp refuted_stop_chunk
end.
Definition pp (ppf : Format.formatter) (game : t) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " playing; inbox snapshot = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; start level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; inbox level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; pvm_name = "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
"; game_state = "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))))))))
"%a playing; inbox snapshot = %a; start level = %a; inbox level = %a; pvm_name = %s; game_state = %a")
pp_player game.(t.turn) Sc_rollup_inbox_repr.pp_history_proof
game.(t.inbox_snapshot) Raw_level_repr.pp game.(t.start_level)
Raw_level_repr.pp game.(t.inbox_level) game.(t.pvm_name) pp_game_state
game.(t.game_state).
End V1.
Inductive versioned : Set :=
| V1 : V1.t → versioned.
Definition versioned_encoding : Data_encoding.encoding versioned :=
Data_encoding.union None
[
Data_encoding.case_value "V1" None (Data_encoding.Tag 0) V1.encoding
(fun (function_parameter : versioned) ⇒
let 'V1 game := function_parameter in
Some game) (fun (game : V1.t) ⇒ V1 game)
].
Include V1.
Definition of_versioned (function_parameter : versioned) : V1.t :=
let 'V1 game := function_parameter in
game.
Definition to_versioned (game : V1.t) : versioned := V1 game.
Module Index.
Module t.
Record record : Set := Build {
alice : Signature.public_key_hash;
bob : Signature.public_key_hash;
}.
Definition with_alice alice (r : record) :=
Build alice r.(bob).
Definition with_bob bob (r : record) :=
Build r.(alice) bob.
End t.
Definition t := t.record.
Definition make
(a_value : Signature.public_key_hash) (b_value : Signature.public_key_hash)
: t :=
let '(alice, bob) :=
if
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) a_value
b_value) >i 0
then
(b_value, a_value)
else
(a_value, b_value) in
{| t.alice := alice; t.bob := bob; |}.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
(alice, bob))
(fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash) ⇒
let '(alice, bob) := function_parameter in
make alice bob) None
(Data_encoding.obj2
(Data_encoding.req None None "alice"
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "bob"
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))).
Definition compare (function_parameter : t) : t → int :=
let '{| t.alice := a_value; t.bob := b_value |} := function_parameter in
fun (function_parameter : t) ⇒
let '{| t.alice := c_value; t.bob := d_value |} := function_parameter in
match
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) a_value
c_value with
| 0 ⇒
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) b_value
d_value
| x_value ⇒ x_value
end.
Definition to_path (function_parameter : t) : list string → list string :=
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
fun (p_value : list string) ⇒
cons
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) alice)
(cons
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) bob)
p_value).
Definition both_of_b58check_opt (function_parameter : string × string)
: option t :=
let '(a_value, b_value) := function_parameter in
let op_letstar {A B : Set} : option A → (A → option B) → option B :=
Option.bind in
op_letstar
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt)
a_value)
(fun a_staker ⇒
op_letstar
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt)
b_value) (fun b_staker ⇒ Some (make a_staker b_staker))).
Definition of_path {A : Set} (function_parameter : list string)
: Pervasives.result (option t) A :=
match function_parameter with
| cons a_value (cons b_value []) ⇒
return? (both_of_b58check_opt (a_value, b_value))
| _ ⇒ return? None
end.
Definition path_length {A : Set} : Pervasives.result int A := return? 2.
Definition rpc_arg : RPC_arg.arg t :=
let descr_value :=
"A pair of stakers that index a smart contract rollup refutation game." in
let construct (function_parameter : t) : string :=
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal "-" % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))) "%s-%s")
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) alice)
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) bob) in
let destruct (s_value : string) : Pervasives.result t string :=
match String.split_on_char "-" % char s_value with
| cons a_value (cons b_value []) ⇒
match both_of_b58check_opt (a_value, b_value) with
| Some stakers ⇒ return? stakers
| None ⇒
Result.error_value
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid game index notation "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid game index notation %s") s_value)
end
| _ ⇒
Result.error_value
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid game index notation "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid game index notation %s") s_value)
end in
RPC_arg.make (Some descr_value) "game_index" destruct construct tt.
Definition staker (function_parameter : t)
: player → Signature.public_key_hash :=
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
fun (function_parameter : player) ⇒
match function_parameter with
| Alice ⇒ alice
| Bob ⇒ bob
end.
End Index.
Definition make_chunk
(state_hash : option Sc_rollup_repr.State_hash.t)
(tick : Sc_rollup_tick_repr.t) : dissection_chunk :=
{| Sc_rollup_dissection_chunk_repr.t.state_hash := state_hash;
Sc_rollup_dissection_chunk_repr.t.tick := tick; |}.
Definition initial
(inbox_value : Sc_rollup_inbox_repr.history_proof)
(dal_snapshot : Dal_slot_repr.History.t) (start_level : Raw_level_repr.t)
(pvm_name : string) (parent : Sc_rollup_commitment_repr.t)
(child : Sc_rollup_commitment_repr.t) (refuter : Signature.public_key_hash)
(defender : Signature.public_key_hash) (default_number_of_sections : int)
: t :=
let '{| Index.t.alice := alice |} := Index.make refuter defender in
let alice_to_play :=
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) alice refuter in
let tick :=
Sc_rollup_tick_repr.of_number_of_ticks
child.(Sc_rollup_commitment_repr.V1.t.number_of_ticks) in
let game_state :=
V1.Dissecting
{|
game_state.Dissecting.dissection :=
[
make_chunk
(Some
parent.(Sc_rollup_commitment_repr.V1.t.compressed_state))
Sc_rollup_tick_repr.initial;
make_chunk
(Some
child.(Sc_rollup_commitment_repr.V1.t.compressed_state))
tick;
make_chunk None (Sc_rollup_tick_repr.next tick)
];
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections; |} in
{|
V1.t.turn :=
if alice_to_play then
Alice
else
Bob; V1.t.inbox_snapshot := inbox_value;
V1.t.dal_snapshot := dal_snapshot; V1.t.start_level := start_level;
V1.t.inbox_level := child.(Sc_rollup_commitment_repr.V1.t.inbox_level);
V1.t.pvm_name := pvm_name; V1.t.game_state := game_state; |}.
Inductive step : Set :=
| Dissection : list dissection_chunk → step
| Proof : Sc_rollup_proof_repr.t → step.
Definition step_encoding : Data_encoding.encoding step :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Dissection" None (Data_encoding.Tag 0)
dissection_encoding
(fun (function_parameter : step) ⇒
match function_parameter with
| Dissection d_value ⇒ Some d_value
| _ ⇒ None
end) (fun (d_value : list dissection_chunk) ⇒ Dissection d_value);
Data_encoding.case_value "Proof" None (Data_encoding.Tag 1)
Sc_rollup_proof_repr.encoding
(fun (function_parameter : step) ⇒
match function_parameter with
| Proof p_value ⇒ Some p_value
| _ ⇒ None
end) (fun (p_value : Sc_rollup_proof_repr.t) ⇒ Proof p_value)
].
Definition pp_step (ppf : Format.formatter) (step : step) : unit :=
match step with
| Dissection states ⇒
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Dissection:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
CamlinternalFormatBasics.End_of_format)) "Dissection:@ ") in
Format.pp_print_list
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf
(";" ++ String.String "010" (String.String "010" ""))))
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : dissection_chunk) ⇒
let '{|
Sc_rollup_dissection_chunk_repr.t.state_hash := state_hash;
Sc_rollup_dissection_chunk_repr.t.tick := tick
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Tick: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "State: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "010" % char
CamlinternalFormatBasics.End_of_format)))))))
("Tick: %a,@ State: %a" ++ String.String "010" ""))
Sc_rollup_tick_repr.pp tick
(Format.pp_print_option None Sc_rollup_repr.State_hash.pp)
state_hash) ppf states
| Proof proof_value ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "proof: "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"proof: %a") Sc_rollup_proof_repr.pp proof_value
end.
Module refutation.
Record record : Set := Build {
choice : Sc_rollup_tick_repr.t;
step : step;
}.
Definition with_choice choice (r : record) :=
Build choice r.(step).
Definition with_step step (r : record) :=
Build r.(choice) step.
End refutation.
Definition refutation := refutation.record.
Definition pp_refutation
(ppf : Format.formatter) (function_parameter : refutation) : unit :=
let '{| refutation.choice := choice; refutation.step := step |} :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Tick: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "Step: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))) "Tick: %a@ Step: %a")
Sc_rollup_tick_repr.pp choice pp_step step.
Definition refutation_encoding : Data_encoding.encoding refutation :=
Data_encoding.conv
(fun (function_parameter : refutation) ⇒
let '{| refutation.choice := choice; refutation.step := step |} :=
function_parameter in
(choice, step))
(fun (function_parameter : Sc_rollup_tick_repr.t × step) ⇒
let '(choice, step) := function_parameter in
{| refutation.choice := choice; refutation.step := step; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "choice" Sc_rollup_tick_repr.encoding)
(Data_encoding.req None None "step" step_encoding)).
Inductive reason : Set :=
| Conflict_resolved : reason
| Timeout : reason.
Definition pp_reason (ppf : Format.formatter) (reason_value : reason) : unit :=
match reason_value with
| Conflict_resolved ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "conflict resolved"
CamlinternalFormatBasics.End_of_format) "conflict resolved")
| Timeout ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "timeout"
CamlinternalFormatBasics.End_of_format) "timeout")
end.
Definition reason_encoding : Data_encoding.encoding reason :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Conflict_resolved" None (Data_encoding.Tag 0)
(Data_encoding.constant "conflict_resolved")
(fun (function_parameter : reason) ⇒
match function_parameter with
| Conflict_resolved ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Conflict_resolved);
Data_encoding.case_value "Timeout" None (Data_encoding.Tag 1)
(Data_encoding.constant "timeout")
(fun (function_parameter : reason) ⇒
match function_parameter with
| Timeout ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Timeout)
].
Module game_state.
Module Dissecting.
Record record {dissection default_number_of_sections : Set} : Set := Build {
dissection : dissection;
default_number_of_sections : default_number_of_sections;
}.
Arguments record : clear implicits.
Definition with_dissection {t_dissection t_default_number_of_sections}
dissection (r : record t_dissection t_default_number_of_sections) :=
Build t_dissection t_default_number_of_sections dissection
r.(default_number_of_sections).
Definition with_default_number_of_sections
{t_dissection t_default_number_of_sections} default_number_of_sections
(r : record t_dissection t_default_number_of_sections) :=
Build t_dissection t_default_number_of_sections r.(dissection)
default_number_of_sections.
End Dissecting.
Definition Dissecting_skeleton := Dissecting.record.
Module Final_move.
Record record {agreed_start_chunk refuted_stop_chunk : Set} : Set := Build {
agreed_start_chunk : agreed_start_chunk;
refuted_stop_chunk : refuted_stop_chunk;
}.
Arguments record : clear implicits.
Definition with_agreed_start_chunk
{t_agreed_start_chunk t_refuted_stop_chunk} agreed_start_chunk
(r : record t_agreed_start_chunk t_refuted_stop_chunk) :=
Build t_agreed_start_chunk t_refuted_stop_chunk agreed_start_chunk
r.(refuted_stop_chunk).
Definition with_refuted_stop_chunk
{t_agreed_start_chunk t_refuted_stop_chunk} refuted_stop_chunk
(r : record t_agreed_start_chunk t_refuted_stop_chunk) :=
Build t_agreed_start_chunk t_refuted_stop_chunk r.(agreed_start_chunk)
refuted_stop_chunk.
End Final_move.
Definition Final_move_skeleton := Final_move.record.
End game_state.
End ConstructorRecords_game_state.
Import ConstructorRecords_game_state.
Reserved Notation "'game_state.Dissecting".
Reserved Notation "'game_state.Final_move".
Inductive game_state : Set :=
| Dissecting : 'game_state.Dissecting → game_state
| Final_move : 'game_state.Final_move → game_state
where "'game_state.Dissecting" :=
(game_state.Dissecting_skeleton (list dissection_chunk) int)
and "'game_state.Final_move" :=
(game_state.Final_move_skeleton dissection_chunk dissection_chunk).
Module game_state.
Include ConstructorRecords_game_state.game_state.
Definition Dissecting := 'game_state.Dissecting.
Definition Final_move := 'game_state.Final_move.
End game_state.
Module t.
Record record : Set := Build {
turn : player;
inbox_snapshot : Sc_rollup_inbox_repr.history_proof;
dal_snapshot : Dal_slot_repr.History.t;
start_level : Raw_level_repr.t;
inbox_level : Raw_level_repr.t;
pvm_name : string;
game_state : game_state;
}.
Definition with_turn turn (r : record) :=
Build turn r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_inbox_snapshot inbox_snapshot (r : record) :=
Build r.(turn) inbox_snapshot r.(dal_snapshot) r.(start_level)
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_dal_snapshot dal_snapshot (r : record) :=
Build r.(turn) r.(inbox_snapshot) dal_snapshot r.(start_level)
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_start_level start_level (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) start_level
r.(inbox_level) r.(pvm_name) r.(game_state).
Definition with_inbox_level inbox_level (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
inbox_level r.(pvm_name) r.(game_state).
Definition with_pvm_name pvm_name (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
r.(inbox_level) pvm_name r.(game_state).
Definition with_game_state game_state (r : record) :=
Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
r.(inbox_level) r.(pvm_name) game_state.
End t.
Definition t := t.record.
Definition player_encoding : Data_encoding.encoding player :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Alice" None (Data_encoding.Tag 0)
(Data_encoding.constant "alice")
(fun (function_parameter : player) ⇒
match function_parameter with
| Alice ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alice);
Data_encoding.case_value "Bob" None (Data_encoding.Tag 1)
(Data_encoding.constant "bob")
(fun (function_parameter : player) ⇒
match function_parameter with
| Bob ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Bob)
].
Definition player_equal (p1 : player) (p2 : player) : bool :=
match (p1, p2) with
| (Alice, Alice) ⇒ true
| (Bob, Bob) ⇒ true
| (_, _) ⇒ false
end.
Definition game_state_equal (gs1 : game_state) (gs2 : game_state) : bool :=
match (gs1, gs2) with
|
(Dissecting {|
game_state.Dissecting.dissection := dissection1;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections1
|},
Dissecting {|
game_state.Dissecting.dissection := dissection2;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections2
|}) ⇒
(Compare.Int.equal default_number_of_sections1 default_number_of_sections2)
&&
(List.equal Sc_rollup_dissection_chunk_repr.equal dissection1 dissection2)
| (Dissecting _, _) ⇒ false
|
(Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk1;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk1
|},
Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk2;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk2
|}) ⇒
(Sc_rollup_dissection_chunk_repr.equal agreed_start_chunk1
agreed_start_chunk2) &&
(Sc_rollup_dissection_chunk_repr.equal refuted_stop_chunk1
refuted_stop_chunk2)
| (Final_move _, _) ⇒ false
end.
Definition equal (function_parameter : t) : t → bool :=
let '{|
t.turn := turn;
t.inbox_snapshot := inbox_snapshot;
t.dal_snapshot := dal_snapshot;
t.start_level := start_level;
t.inbox_level := inbox_level;
t.pvm_name := pvm_name;
t.game_state := game_state
|} := function_parameter in
fun (g2 : t) ⇒
(player_equal turn g2.(t.turn)) &&
((Sc_rollup_inbox_repr.equal_history_proof inbox_snapshot
g2.(t.inbox_snapshot)) &&
((Dal_slot_repr.History.equal dal_snapshot g2.(t.dal_snapshot)) &&
((Raw_level_repr.equal start_level g2.(t.start_level)) &&
((Raw_level_repr.equal inbox_level g2.(t.inbox_level)) &&
((String.equal pvm_name g2.(t.pvm_name)) &&
(game_state_equal game_state g2.(t.game_state))))))).
Definition string_of_player (function_parameter : player) : string :=
match function_parameter with
| Alice ⇒ "alice"
| Bob ⇒ "bob"
end.
Definition pp_player (ppf : Format.formatter) (player_value : player)
: unit := Format.pp_print_string ppf (string_of_player player_value).
Definition opponent (function_parameter : player) : player :=
match function_parameter with
| Alice ⇒ Bob
| Bob ⇒ Alice
end.
Definition dissection_encoding
: Data_encoding.encoding (list Sc_rollup_dissection_chunk_repr.t) :=
Data_encoding.list_value None Sc_rollup_dissection_chunk_repr.encoding.
Definition game_state_encoding : Data_encoding.encoding game_state :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Dissecting" None (Data_encoding.Tag 0)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "Dissecting"))
(Data_encoding.req None None "dissection"
dissection_encoding)
(Data_encoding.req None None "default_number_of_sections"
Data_encoding.uint8))
(fun (function_parameter : game_state) ⇒
match function_parameter with
|
Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections
:=
default_number_of_sections
|} ⇒
Some (tt, dissection, default_number_of_sections)
| _ ⇒ None
end)
(fun (function_parameter :
unit × list Sc_rollup_dissection_chunk_repr.t × int) ⇒
let '(_, dissection, default_number_of_sections) :=
function_parameter in
Dissecting
{| game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections
:= default_number_of_sections; |});
Data_encoding.case_value "Final_move" None (Data_encoding.Tag 1)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "Final_move"))
(Data_encoding.req None None "agreed_start_chunk"
Sc_rollup_dissection_chunk_repr.encoding)
(Data_encoding.req None None "refuted_stop_chunk"
Sc_rollup_dissection_chunk_repr.encoding))
(fun (function_parameter : game_state) ⇒
match function_parameter with
|
Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk
:=
refuted_stop_chunk
|} ⇒
Some (tt, agreed_start_chunk, refuted_stop_chunk)
| _ ⇒ None
end)
(fun (function_parameter :
unit × Sc_rollup_dissection_chunk_repr.t ×
Sc_rollup_dissection_chunk_repr.t) ⇒
let '(_, agreed_start_chunk, refuted_stop_chunk) :=
function_parameter in
Final_move
{|
game_state.Final_move.agreed_start_chunk :=
agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk :=
refuted_stop_chunk; |})
].
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.turn := turn;
t.inbox_snapshot := inbox_snapshot;
t.dal_snapshot := dal_snapshot;
t.start_level := start_level;
t.inbox_level := inbox_level;
t.pvm_name := pvm_name;
t.game_state := game_state
|} := function_parameter in
(turn, inbox_snapshot, dal_snapshot, start_level, inbox_level, pvm_name,
game_state))
(fun (function_parameter :
player × Sc_rollup_inbox_repr.history_proof × Dal_slot_repr.History.t ×
Raw_level_repr.t × Raw_level_repr.t × string × game_state) ⇒
let
'(turn, inbox_snapshot, dal_snapshot, start_level, inbox_level,
pvm_name, game_state) := function_parameter in
{| t.turn := turn; t.inbox_snapshot := inbox_snapshot;
t.dal_snapshot := dal_snapshot; t.start_level := start_level;
t.inbox_level := inbox_level; t.pvm_name := pvm_name;
t.game_state := game_state; |}) None
(Data_encoding.obj7 (Data_encoding.req None None "turn" player_encoding)
(Data_encoding.req None None "inbox_snapshot"
Sc_rollup_inbox_repr.history_proof_encoding)
(Data_encoding.req None None "dal_snapshot"
Dal_slot_repr.History.encoding)
(Data_encoding.req None None "start_level" Raw_level_repr.encoding)
(Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "pvm_name" Data_encoding.string_value)
(Data_encoding.req None None "game_state" game_state_encoding)).
Definition pp_dissection
(ppf : Format.formatter) (d_value : list Sc_rollup_dissection_chunk_repr.t)
: unit :=
Format.pp_print_list
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf (";" ++ String.String "010" "")))
Sc_rollup_dissection_chunk_repr.pp ppf d_value.
Definition pp_game_state (ppf : Format.formatter) (game_state : game_state)
: unit :=
match game_state with
|
Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections
|} ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Dissecting "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " using "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " number of sections"
CamlinternalFormatBasics.End_of_format)))))
"Dissecting %a using %d number of sections") pp_dissection dissection
default_number_of_sections
|
Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk
|} ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Final move to refute "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " from "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", opponent failed to refute"
CamlinternalFormatBasics.End_of_format)))))
"Final move to refute %a from %a, opponent failed to refute")
Sc_rollup_dissection_chunk_repr.pp agreed_start_chunk
Sc_rollup_dissection_chunk_repr.pp refuted_stop_chunk
end.
Definition pp (ppf : Format.formatter) (game : t) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " playing; inbox snapshot = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; start level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; inbox level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; pvm_name = "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
"; game_state = "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))))))))
"%a playing; inbox snapshot = %a; start level = %a; inbox level = %a; pvm_name = %s; game_state = %a")
pp_player game.(t.turn) Sc_rollup_inbox_repr.pp_history_proof
game.(t.inbox_snapshot) Raw_level_repr.pp game.(t.start_level)
Raw_level_repr.pp game.(t.inbox_level) game.(t.pvm_name) pp_game_state
game.(t.game_state).
End V1.
Inductive versioned : Set :=
| V1 : V1.t → versioned.
Definition versioned_encoding : Data_encoding.encoding versioned :=
Data_encoding.union None
[
Data_encoding.case_value "V1" None (Data_encoding.Tag 0) V1.encoding
(fun (function_parameter : versioned) ⇒
let 'V1 game := function_parameter in
Some game) (fun (game : V1.t) ⇒ V1 game)
].
Include V1.
Definition of_versioned (function_parameter : versioned) : V1.t :=
let 'V1 game := function_parameter in
game.
Definition to_versioned (game : V1.t) : versioned := V1 game.
Module Index.
Module t.
Record record : Set := Build {
alice : Signature.public_key_hash;
bob : Signature.public_key_hash;
}.
Definition with_alice alice (r : record) :=
Build alice r.(bob).
Definition with_bob bob (r : record) :=
Build r.(alice) bob.
End t.
Definition t := t.record.
Definition make
(a_value : Signature.public_key_hash) (b_value : Signature.public_key_hash)
: t :=
let '(alice, bob) :=
if
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) a_value
b_value) >i 0
then
(b_value, a_value)
else
(a_value, b_value) in
{| t.alice := alice; t.bob := bob; |}.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
(alice, bob))
(fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash) ⇒
let '(alice, bob) := function_parameter in
make alice bob) None
(Data_encoding.obj2
(Data_encoding.req None None "alice"
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "bob"
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))).
Definition compare (function_parameter : t) : t → int :=
let '{| t.alice := a_value; t.bob := b_value |} := function_parameter in
fun (function_parameter : t) ⇒
let '{| t.alice := c_value; t.bob := d_value |} := function_parameter in
match
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) a_value
c_value with
| 0 ⇒
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) b_value
d_value
| x_value ⇒ x_value
end.
Definition to_path (function_parameter : t) : list string → list string :=
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
fun (p_value : list string) ⇒
cons
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) alice)
(cons
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) bob)
p_value).
Definition both_of_b58check_opt (function_parameter : string × string)
: option t :=
let '(a_value, b_value) := function_parameter in
let op_letstar {A B : Set} : option A → (A → option B) → option B :=
Option.bind in
op_letstar
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt)
a_value)
(fun a_staker ⇒
op_letstar
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt)
b_value) (fun b_staker ⇒ Some (make a_staker b_staker))).
Definition of_path {A : Set} (function_parameter : list string)
: Pervasives.result (option t) A :=
match function_parameter with
| cons a_value (cons b_value []) ⇒
return? (both_of_b58check_opt (a_value, b_value))
| _ ⇒ return? None
end.
Definition path_length {A : Set} : Pervasives.result int A := return? 2.
Definition rpc_arg : RPC_arg.arg t :=
let descr_value :=
"A pair of stakers that index a smart contract rollup refutation game." in
let construct (function_parameter : t) : string :=
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal "-" % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))) "%s-%s")
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) alice)
(Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) bob) in
let destruct (s_value : string) : Pervasives.result t string :=
match String.split_on_char "-" % char s_value with
| cons a_value (cons b_value []) ⇒
match both_of_b58check_opt (a_value, b_value) with
| Some stakers ⇒ return? stakers
| None ⇒
Result.error_value
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid game index notation "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid game index notation %s") s_value)
end
| _ ⇒
Result.error_value
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid game index notation "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid game index notation %s") s_value)
end in
RPC_arg.make (Some descr_value) "game_index" destruct construct tt.
Definition staker (function_parameter : t)
: player → Signature.public_key_hash :=
let '{| t.alice := alice; t.bob := bob |} := function_parameter in
fun (function_parameter : player) ⇒
match function_parameter with
| Alice ⇒ alice
| Bob ⇒ bob
end.
End Index.
Definition make_chunk
(state_hash : option Sc_rollup_repr.State_hash.t)
(tick : Sc_rollup_tick_repr.t) : dissection_chunk :=
{| Sc_rollup_dissection_chunk_repr.t.state_hash := state_hash;
Sc_rollup_dissection_chunk_repr.t.tick := tick; |}.
Definition initial
(inbox_value : Sc_rollup_inbox_repr.history_proof)
(dal_snapshot : Dal_slot_repr.History.t) (start_level : Raw_level_repr.t)
(pvm_name : string) (parent : Sc_rollup_commitment_repr.t)
(child : Sc_rollup_commitment_repr.t) (refuter : Signature.public_key_hash)
(defender : Signature.public_key_hash) (default_number_of_sections : int)
: t :=
let '{| Index.t.alice := alice |} := Index.make refuter defender in
let alice_to_play :=
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) alice refuter in
let tick :=
Sc_rollup_tick_repr.of_number_of_ticks
child.(Sc_rollup_commitment_repr.V1.t.number_of_ticks) in
let game_state :=
V1.Dissecting
{|
game_state.Dissecting.dissection :=
[
make_chunk
(Some
parent.(Sc_rollup_commitment_repr.V1.t.compressed_state))
Sc_rollup_tick_repr.initial;
make_chunk
(Some
child.(Sc_rollup_commitment_repr.V1.t.compressed_state))
tick;
make_chunk None (Sc_rollup_tick_repr.next tick)
];
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections; |} in
{|
V1.t.turn :=
if alice_to_play then
Alice
else
Bob; V1.t.inbox_snapshot := inbox_value;
V1.t.dal_snapshot := dal_snapshot; V1.t.start_level := start_level;
V1.t.inbox_level := child.(Sc_rollup_commitment_repr.V1.t.inbox_level);
V1.t.pvm_name := pvm_name; V1.t.game_state := game_state; |}.
Inductive step : Set :=
| Dissection : list dissection_chunk → step
| Proof : Sc_rollup_proof_repr.t → step.
Definition step_encoding : Data_encoding.encoding step :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Dissection" None (Data_encoding.Tag 0)
dissection_encoding
(fun (function_parameter : step) ⇒
match function_parameter with
| Dissection d_value ⇒ Some d_value
| _ ⇒ None
end) (fun (d_value : list dissection_chunk) ⇒ Dissection d_value);
Data_encoding.case_value "Proof" None (Data_encoding.Tag 1)
Sc_rollup_proof_repr.encoding
(fun (function_parameter : step) ⇒
match function_parameter with
| Proof p_value ⇒ Some p_value
| _ ⇒ None
end) (fun (p_value : Sc_rollup_proof_repr.t) ⇒ Proof p_value)
].
Definition pp_step (ppf : Format.formatter) (step : step) : unit :=
match step with
| Dissection states ⇒
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Dissection:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
CamlinternalFormatBasics.End_of_format)) "Dissection:@ ") in
Format.pp_print_list
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf
(";" ++ String.String "010" (String.String "010" ""))))
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : dissection_chunk) ⇒
let '{|
Sc_rollup_dissection_chunk_repr.t.state_hash := state_hash;
Sc_rollup_dissection_chunk_repr.t.tick := tick
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Tick: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "State: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "010" % char
CamlinternalFormatBasics.End_of_format)))))))
("Tick: %a,@ State: %a" ++ String.String "010" ""))
Sc_rollup_tick_repr.pp tick
(Format.pp_print_option None Sc_rollup_repr.State_hash.pp)
state_hash) ppf states
| Proof proof_value ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "proof: "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"proof: %a") Sc_rollup_proof_repr.pp proof_value
end.
Module refutation.
Record record : Set := Build {
choice : Sc_rollup_tick_repr.t;
step : step;
}.
Definition with_choice choice (r : record) :=
Build choice r.(step).
Definition with_step step (r : record) :=
Build r.(choice) step.
End refutation.
Definition refutation := refutation.record.
Definition pp_refutation
(ppf : Format.formatter) (function_parameter : refutation) : unit :=
let '{| refutation.choice := choice; refutation.step := step |} :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Tick: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "Step: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))) "Tick: %a@ Step: %a")
Sc_rollup_tick_repr.pp choice pp_step step.
Definition refutation_encoding : Data_encoding.encoding refutation :=
Data_encoding.conv
(fun (function_parameter : refutation) ⇒
let '{| refutation.choice := choice; refutation.step := step |} :=
function_parameter in
(choice, step))
(fun (function_parameter : Sc_rollup_tick_repr.t × step) ⇒
let '(choice, step) := function_parameter in
{| refutation.choice := choice; refutation.step := step; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "choice" Sc_rollup_tick_repr.encoding)
(Data_encoding.req None None "step" step_encoding)).
Inductive reason : Set :=
| Conflict_resolved : reason
| Timeout : reason.
Definition pp_reason (ppf : Format.formatter) (reason_value : reason) : unit :=
match reason_value with
| Conflict_resolved ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "conflict resolved"
CamlinternalFormatBasics.End_of_format) "conflict resolved")
| Timeout ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "timeout"
CamlinternalFormatBasics.End_of_format) "timeout")
end.
Definition reason_encoding : Data_encoding.encoding reason :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Conflict_resolved" None (Data_encoding.Tag 0)
(Data_encoding.constant "conflict_resolved")
(fun (function_parameter : reason) ⇒
match function_parameter with
| Conflict_resolved ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Conflict_resolved);
Data_encoding.case_value "Timeout" None (Data_encoding.Tag 1)
(Data_encoding.constant "timeout")
(fun (function_parameter : reason) ⇒
match function_parameter with
| Timeout ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Timeout)
].
Records for the constructor parameters
Module ConstructorRecords_game_result.
Module game_result.
Module Loser.
Record record {reason loser : Set} : Set := Build {
reason : reason;
loser : loser;
}.
Arguments record : clear implicits.
Definition with_reason {t_reason t_loser} reason
(r : record t_reason t_loser) :=
Build t_reason t_loser reason r.(loser).
Definition with_loser {t_reason t_loser} loser
(r : record t_reason t_loser) :=
Build t_reason t_loser r.(reason) loser.
End Loser.
Definition Loser_skeleton := Loser.record.
End game_result.
End ConstructorRecords_game_result.
Import ConstructorRecords_game_result.
Reserved Notation "'game_result.Loser".
Inductive game_result : Set :=
| Loser : 'game_result.Loser → game_result
| Draw : game_result
where "'game_result.Loser" :=
(game_result.Loser_skeleton reason Signature.public_key_hash).
Module game_result.
Include ConstructorRecords_game_result.game_result.
Definition Loser := 'game_result.Loser.
End game_result.
Definition pp_game_result (ppf : Format.formatter) (r_value : game_result)
: unit :=
match r_value with
|
Loser {|
game_result.Loser.reason := reason_value;
game_result.Loser.loser := loser
|} ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " lost because: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "%a lost because: %a")
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) loser pp_reason
reason_value
| Draw ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Draw"
CamlinternalFormatBasics.End_of_format) "Draw")
end.
Definition game_result_encoding : Data_encoding.encoding game_result :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Loser" None (Data_encoding.Tag 0)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "loser"))
(Data_encoding.req None None "reason" reason_encoding)
(Data_encoding.req None None "player"
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : game_result) ⇒
match function_parameter with
|
Loser {|
game_result.Loser.reason := reason_value;
game_result.Loser.loser := loser
|} ⇒ Some (tt, reason_value, loser)
| _ ⇒ None
end)
(fun (function_parameter : unit × reason × Signature.public_key_hash)
⇒
let '(_, reason_value, loser) := function_parameter in
Loser
{| game_result.Loser.reason := reason_value;
game_result.Loser.loser := loser; |});
Data_encoding.case_value "Draw" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "kind"
(Data_encoding.constant "draw")))
(fun (function_parameter : game_result) ⇒
match function_parameter with
| Draw ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Draw)
].
Inductive status : Set :=
| Ongoing : status
| Ended : game_result → status.
Definition pp_status (ppf : Format.formatter) (status : status) : unit :=
match status with
| Ongoing ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Game ongoing"
CamlinternalFormatBasics.End_of_format) "Game ongoing")
| Ended game_result ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Game ended: "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"Game ended: %a") pp_game_result game_result
end.
Definition status_encoding : Data_encoding.encoding status :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Ongoing" None (Data_encoding.Tag 0)
(Data_encoding.constant "ongoing")
(fun (function_parameter : status) ⇒
match function_parameter with
| Ongoing ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Ongoing);
Data_encoding.case_value "Ended" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "result" game_result_encoding))
(fun (function_parameter : status) ⇒
match function_parameter with
| Ended r_value ⇒ Some r_value
| _ ⇒ None
end) (fun (r_value : game_result) ⇒ Ended r_value)
].
#[bypass_check(guard)]
Definition find_choice
(dissection : list dissection_chunk) (tick : Sc_rollup_tick_repr.t)
: M? (dissection_chunk × dissection_chunk) :=
let fix traverse (states : list dissection_chunk) {struct states}
: M? (dissection_chunk × dissection_chunk) :=
match states with
|
cons
({|
Sc_rollup_dissection_chunk_repr.t.state_hash := _;
Sc_rollup_dissection_chunk_repr.t.tick := state_tick
|} as curr) (cons next others) ⇒
if Sc_rollup_tick_repr.op_eq tick state_tick then
return? (curr, next)
else
traverse (cons next others)
| _ ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Dissection_choice_not_found" Sc_rollup_tick_repr.t
tick)
end in
traverse dissection.
Module game_result.
Module Loser.
Record record {reason loser : Set} : Set := Build {
reason : reason;
loser : loser;
}.
Arguments record : clear implicits.
Definition with_reason {t_reason t_loser} reason
(r : record t_reason t_loser) :=
Build t_reason t_loser reason r.(loser).
Definition with_loser {t_reason t_loser} loser
(r : record t_reason t_loser) :=
Build t_reason t_loser r.(reason) loser.
End Loser.
Definition Loser_skeleton := Loser.record.
End game_result.
End ConstructorRecords_game_result.
Import ConstructorRecords_game_result.
Reserved Notation "'game_result.Loser".
Inductive game_result : Set :=
| Loser : 'game_result.Loser → game_result
| Draw : game_result
where "'game_result.Loser" :=
(game_result.Loser_skeleton reason Signature.public_key_hash).
Module game_result.
Include ConstructorRecords_game_result.game_result.
Definition Loser := 'game_result.Loser.
End game_result.
Definition pp_game_result (ppf : Format.formatter) (r_value : game_result)
: unit :=
match r_value with
|
Loser {|
game_result.Loser.reason := reason_value;
game_result.Loser.loser := loser
|} ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " lost because: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "%a lost because: %a")
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) loser pp_reason
reason_value
| Draw ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Draw"
CamlinternalFormatBasics.End_of_format) "Draw")
end.
Definition game_result_encoding : Data_encoding.encoding game_result :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Loser" None (Data_encoding.Tag 0)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "loser"))
(Data_encoding.req None None "reason" reason_encoding)
(Data_encoding.req None None "player"
Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : game_result) ⇒
match function_parameter with
|
Loser {|
game_result.Loser.reason := reason_value;
game_result.Loser.loser := loser
|} ⇒ Some (tt, reason_value, loser)
| _ ⇒ None
end)
(fun (function_parameter : unit × reason × Signature.public_key_hash)
⇒
let '(_, reason_value, loser) := function_parameter in
Loser
{| game_result.Loser.reason := reason_value;
game_result.Loser.loser := loser; |});
Data_encoding.case_value "Draw" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "kind"
(Data_encoding.constant "draw")))
(fun (function_parameter : game_result) ⇒
match function_parameter with
| Draw ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Draw)
].
Inductive status : Set :=
| Ongoing : status
| Ended : game_result → status.
Definition pp_status (ppf : Format.formatter) (status : status) : unit :=
match status with
| Ongoing ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Game ongoing"
CamlinternalFormatBasics.End_of_format) "Game ongoing")
| Ended game_result ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Game ended: "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"Game ended: %a") pp_game_result game_result
end.
Definition status_encoding : Data_encoding.encoding status :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Ongoing" None (Data_encoding.Tag 0)
(Data_encoding.constant "ongoing")
(fun (function_parameter : status) ⇒
match function_parameter with
| Ongoing ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Ongoing);
Data_encoding.case_value "Ended" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "result" game_result_encoding))
(fun (function_parameter : status) ⇒
match function_parameter with
| Ended r_value ⇒ Some r_value
| _ ⇒ None
end) (fun (r_value : game_result) ⇒ Ended r_value)
].
#[bypass_check(guard)]
Definition find_choice
(dissection : list dissection_chunk) (tick : Sc_rollup_tick_repr.t)
: M? (dissection_chunk × dissection_chunk) :=
let fix traverse (states : list dissection_chunk) {struct states}
: M? (dissection_chunk × dissection_chunk) :=
match states with
|
cons
({|
Sc_rollup_dissection_chunk_repr.t.state_hash := _;
Sc_rollup_dissection_chunk_repr.t.tick := state_tick
|} as curr) (cons next others) ⇒
if Sc_rollup_tick_repr.op_eq tick state_tick then
return? (curr, next)
else
traverse (cons next others)
| _ ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Dissection_choice_not_found" Sc_rollup_tick_repr.t
tick)
end in
traverse dissection.
Check that the chosen interval is a single tick.
Definition check_proof_distance_is_one
(start_tick : Sc_rollup_tick_repr.t) (stop_tick : Sc_rollup_tick_repr.t)
: M? unit :=
let dist := Sc_rollup_tick_repr.distance start_tick stop_tick in
Error_monad.error_unless (Z.equal dist Z.one)
(Build_extensible "Proof_unexpected_section_size" Z.t dist).
(start_tick : Sc_rollup_tick_repr.t) (stop_tick : Sc_rollup_tick_repr.t)
: M? unit :=
let dist := Sc_rollup_tick_repr.distance start_tick stop_tick in
Error_monad.error_unless (Z.equal dist Z.one)
(Build_extensible "Proof_unexpected_section_size" Z.t dist).
Check the proof begins with the correct state.
Definition check_proof_start_state
(start_state : option Sc_rollup_repr.State_hash.t)
(proof_value : Sc_rollup_proof_repr.t) : M? unit :=
let start_proof := Sc_rollup_proof_repr.start proof_value in
Error_monad.error_unless
(Option.equal Sc_rollup_repr.State_hash.equal start_state (Some start_proof))
(Build_extensible "Proof_start_state_hash_mismatch"
Proof_start_state_hash_mismatch
{| Proof_start_state_hash_mismatch.start_state_hash := start_state;
Proof_start_state_hash_mismatch.start_proof := start_proof; |}).
(start_state : option Sc_rollup_repr.State_hash.t)
(proof_value : Sc_rollup_proof_repr.t) : M? unit :=
let start_proof := Sc_rollup_proof_repr.start proof_value in
Error_monad.error_unless
(Option.equal Sc_rollup_repr.State_hash.equal start_state (Some start_proof))
(Build_extensible "Proof_start_state_hash_mismatch"
Proof_start_state_hash_mismatch
{| Proof_start_state_hash_mismatch.start_state_hash := start_state;
Proof_start_state_hash_mismatch.start_proof := start_proof; |}).
Check the proof stops with a different state than refuted one.
Definition check_proof_stop_state {A : Set}
(stop_state : option Sc_rollup_repr.State_hash.t) (input_given : option A)
(input_request : Sc_rollup_PVM_sig.input_request)
(proof_value : Sc_rollup_proof_repr.t) (validate : bool) : M? unit :=
let stop_proof :=
match (input_given, input_request) with
|
((None, Sc_rollup_PVM_sig.No_input_required) |
(Some _, Sc_rollup_PVM_sig.Initial) |
(Some _, Sc_rollup_PVM_sig.First_after _ _) |
(Some _, Sc_rollup_PVM_sig.Needs_reveal _)) ⇒
Some (Sc_rollup_proof_repr.stop proof_value)
|
((Some _, Sc_rollup_PVM_sig.No_input_required) |
(None, Sc_rollup_PVM_sig.Initial) |
(None, Sc_rollup_PVM_sig.First_after _ _) |
(None, Sc_rollup_PVM_sig.Needs_reveal _)) ⇒ None
end in
Error_monad.error_unless
(let b_value :=
Option.equal Sc_rollup_repr.State_hash.equal stop_state stop_proof in
if validate then
b_value
else
Pervasives.not b_value)
(if validate then
Build_extensible "Proof_stop_state_hash_failed_to_validate"
Proof_stop_state_hash_failed_to_validate
{|
Proof_stop_state_hash_failed_to_validate.stop_state_hash :=
stop_state;
Proof_stop_state_hash_failed_to_validate.stop_proof := stop_proof; |}
else
Build_extensible "Proof_stop_state_hash_failed_to_refute"
Proof_stop_state_hash_failed_to_refute
{| Proof_stop_state_hash_failed_to_refute.stop_state_hash := stop_state;
Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof; |}).
(stop_state : option Sc_rollup_repr.State_hash.t) (input_given : option A)
(input_request : Sc_rollup_PVM_sig.input_request)
(proof_value : Sc_rollup_proof_repr.t) (validate : bool) : M? unit :=
let stop_proof :=
match (input_given, input_request) with
|
((None, Sc_rollup_PVM_sig.No_input_required) |
(Some _, Sc_rollup_PVM_sig.Initial) |
(Some _, Sc_rollup_PVM_sig.First_after _ _) |
(Some _, Sc_rollup_PVM_sig.Needs_reveal _)) ⇒
Some (Sc_rollup_proof_repr.stop proof_value)
|
((Some _, Sc_rollup_PVM_sig.No_input_required) |
(None, Sc_rollup_PVM_sig.Initial) |
(None, Sc_rollup_PVM_sig.First_after _ _) |
(None, Sc_rollup_PVM_sig.Needs_reveal _)) ⇒ None
end in
Error_monad.error_unless
(let b_value :=
Option.equal Sc_rollup_repr.State_hash.equal stop_state stop_proof in
if validate then
b_value
else
Pervasives.not b_value)
(if validate then
Build_extensible "Proof_stop_state_hash_failed_to_validate"
Proof_stop_state_hash_failed_to_validate
{|
Proof_stop_state_hash_failed_to_validate.stop_state_hash :=
stop_state;
Proof_stop_state_hash_failed_to_validate.stop_proof := stop_proof; |}
else
Build_extensible "Proof_stop_state_hash_failed_to_refute"
Proof_stop_state_hash_failed_to_refute
{| Proof_stop_state_hash_failed_to_refute.stop_state_hash := stop_state;
Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof; |}).
Check the proof validates the stop state.
Definition check_proof_validate_stop_state {A : Set}
(stop_state : option Sc_rollup_repr.State_hash.t) (input : option A)
(input_request : Sc_rollup_PVM_sig.input_request)
(proof_value : Sc_rollup_proof_repr.t) : M? unit :=
check_proof_stop_state stop_state input input_request proof_value true.
(stop_state : option Sc_rollup_repr.State_hash.t) (input : option A)
(input_request : Sc_rollup_PVM_sig.input_request)
(proof_value : Sc_rollup_proof_repr.t) : M? unit :=
check_proof_stop_state stop_state input input_request proof_value true.
Check the proof refutes the stop state.
Definition check_proof_refute_stop_state {A : Set}
(stop_state : option Sc_rollup_repr.State_hash.t) (input : option A)
(input_request : Sc_rollup_PVM_sig.input_request)
(proof_value : Sc_rollup_proof_repr.t) : M? unit :=
check_proof_stop_state stop_state input input_request proof_value false.
(stop_state : option Sc_rollup_repr.State_hash.t) (input : option A)
(input_request : Sc_rollup_PVM_sig.input_request)
(proof_value : Sc_rollup_proof_repr.t) : M? unit :=
check_proof_stop_state stop_state input input_request proof_value false.
Returns the validity of the first final move on top of a dissection.
Definition validity_final_move
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(first_move : bool) (metadata : Sc_rollup_metadata_repr.t)
(proof_value : Sc_rollup_proof_repr.t) (game : t)
(start_chunk : dissection_chunk) (stop_chunk : dissection_chunk) : bool :=
let res :=
let '{|
V1.t.inbox_snapshot := inbox_snapshot;
V1.t.dal_snapshot := dal_snapshot;
V1.t.inbox_level := inbox_level;
V1.t.pvm_name := pvm_name
|} := game in
let valid :=
Sc_rollup_proof_repr.valid metadata inbox_snapshot inbox_level
dal_snapshot dal_parameters dal_attestation_lag pvm_name proof_value in
let? '_ :=
if first_move then
check_proof_distance_is_one
start_chunk.(Sc_rollup_dissection_chunk_repr.t.tick)
stop_chunk.(Sc_rollup_dissection_chunk_repr.t.tick)
else
return? tt in
let? '_ :=
check_proof_start_state
start_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) proof_value
in
match valid with
| Pervasives.Ok (input, input_request) ⇒
let? '_ :=
if first_move then
check_proof_refute_stop_state
stop_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) input
input_request proof_value
else
check_proof_validate_stop_state
stop_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) input
input_request proof_value in
Error_monad.Lwt_result_syntax.return_true
| _ ⇒ Error_monad.Lwt_result_syntax.return_false
end in
Result.value_value res false.
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(first_move : bool) (metadata : Sc_rollup_metadata_repr.t)
(proof_value : Sc_rollup_proof_repr.t) (game : t)
(start_chunk : dissection_chunk) (stop_chunk : dissection_chunk) : bool :=
let res :=
let '{|
V1.t.inbox_snapshot := inbox_snapshot;
V1.t.dal_snapshot := dal_snapshot;
V1.t.inbox_level := inbox_level;
V1.t.pvm_name := pvm_name
|} := game in
let valid :=
Sc_rollup_proof_repr.valid metadata inbox_snapshot inbox_level
dal_snapshot dal_parameters dal_attestation_lag pvm_name proof_value in
let? '_ :=
if first_move then
check_proof_distance_is_one
start_chunk.(Sc_rollup_dissection_chunk_repr.t.tick)
stop_chunk.(Sc_rollup_dissection_chunk_repr.t.tick)
else
return? tt in
let? '_ :=
check_proof_start_state
start_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) proof_value
in
match valid with
| Pervasives.Ok (input, input_request) ⇒
let? '_ :=
if first_move then
check_proof_refute_stop_state
stop_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) input
input_request proof_value
else
check_proof_validate_stop_state
stop_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) input
input_request proof_value in
Error_monad.Lwt_result_syntax.return_true
| _ ⇒ Error_monad.Lwt_result_syntax.return_false
end in
Result.value_value res false.
Returns the validity of the first final move on top of a dissection.
It is valid if and only:
The distance of the refuted dissection is [1].
The proof start on the agreed start state.
The proof stop on the state different than the refuted one.
The proof is correctly verified.
Definition validity_first_final_move
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(metadata : Sc_rollup_metadata_repr.t) (proof_value : Sc_rollup_proof_repr.t)
(game : t) (start_chunk : dissection_chunk) (stop_chunk : dissection_chunk)
: bool :=
validity_final_move dal_parameters dal_attestation_lag true metadata
proof_value game start_chunk stop_chunk.
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(metadata : Sc_rollup_metadata_repr.t) (proof_value : Sc_rollup_proof_repr.t)
(game : t) (start_chunk : dissection_chunk) (stop_chunk : dissection_chunk)
: bool :=
validity_final_move dal_parameters dal_attestation_lag true metadata
proof_value game start_chunk stop_chunk.
Returns the validity of the second final move.
It is valid if and only:
The proof start on the agreed start state.
The proof stop on the state validates the refuted one.
The proof is correctly verified.
Definition validity_second_final_move
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(metadata : Sc_rollup_metadata_repr.t) (agreed_start_chunk : dissection_chunk)
(refuted_stop_chunk : dissection_chunk) (game : t)
(proof_value : Sc_rollup_proof_repr.t) : bool :=
validity_final_move dal_parameters dal_attestation_lag false metadata
proof_value game agreed_start_chunk refuted_stop_chunk.
Definition loser_of_results (alice_result : bool) (bob_result : bool)
: option player :=
match (alice_result, bob_result) with
| (true, true) ⇒ None
| (false, false) ⇒ None
| (false, true) ⇒ Some Alice
| (true, false) ⇒ Some Bob
end.
Definition play
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(stakers : Index.t) (metadata : Sc_rollup_metadata_repr.t) (game : t)
(refutation : refutation) : M? (Either.t game_result t) :=
let mk_loser {A : Set} (loser : player) : Either.t game_result A :=
let loser := Index.staker stakers loser in
Either.Left
(Loser
{| game_result.Loser.reason := Conflict_resolved;
game_result.Loser.loser := loser; |}) in
match (refutation.(refutation.step), game.(V1.t.game_state)) with
|
(Dissection states,
V1.Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections
|}) ⇒
let? '(start_chunk, stop_chunk) :=
find_choice dissection refutation.(refutation.choice) in
let? '_ :=
Sc_rollup_dissection_chunk_repr.default_check default_number_of_sections
start_chunk stop_chunk states in
let new_game_state :=
V1.Dissecting
{| game_state.Dissecting.dissection := states;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections; |} in
return?
(Either.Right
{| V1.t.turn := opponent game.(V1.t.turn);
V1.t.inbox_snapshot := game.(V1.t.inbox_snapshot);
V1.t.dal_snapshot := game.(V1.t.dal_snapshot);
V1.t.start_level := game.(V1.t.start_level);
V1.t.inbox_level := game.(V1.t.inbox_level);
V1.t.pvm_name := game.(V1.t.pvm_name);
V1.t.game_state := new_game_state; |})
| (Dissection _, V1.Final_move _) ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Dissecting_during_final_move" unit tt)
|
(Proof proof_value,
V1.Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections := _
|}) ⇒
let? '(start_chunk, stop_chunk) :=
find_choice dissection refutation.(refutation.choice) in
let player_result :=
validity_first_final_move dal_parameters dal_attestation_lag metadata
proof_value game start_chunk stop_chunk in
if player_result then
return? (mk_loser (opponent game.(V1.t.turn)))
else
let new_game_state :=
let agreed_start_chunk := start_chunk in
let refuted_stop_chunk := stop_chunk in
V1.Final_move
{| game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk; |}
in
return?
(Either.Right
{| V1.t.turn := opponent game.(V1.t.turn);
V1.t.inbox_snapshot := game.(V1.t.inbox_snapshot);
V1.t.dal_snapshot := game.(V1.t.dal_snapshot);
V1.t.start_level := game.(V1.t.start_level);
V1.t.inbox_level := game.(V1.t.inbox_level);
V1.t.pvm_name := game.(V1.t.pvm_name);
V1.t.game_state := new_game_state; |})
|
(Proof proof_value,
V1.Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk
|}) ⇒
let player_result :=
validity_second_final_move dal_parameters dal_attestation_lag metadata
agreed_start_chunk refuted_stop_chunk game proof_value in
if player_result then
return? (mk_loser (opponent game.(V1.t.turn)))
else
return? (Either.Left Draw)
end.
Module timeout.
Record record : Set := Build {
alice : int;
bob : int;
last_turn_level : Raw_level_repr.t;
}.
Definition with_alice alice (r : record) :=
Build alice r.(bob) r.(last_turn_level).
Definition with_bob bob (r : record) :=
Build r.(alice) bob r.(last_turn_level).
Definition with_last_turn_level last_turn_level (r : record) :=
Build r.(alice) r.(bob) last_turn_level.
End timeout.
Definition timeout := timeout.record.
Definition timeout_encoding : Data_encoding.encoding timeout :=
Data_encoding.conv
(fun (function_parameter : timeout) ⇒
let '{|
timeout.alice := alice;
timeout.bob := bob;
timeout.last_turn_level := last_turn_level
|} := function_parameter in
(alice, bob, last_turn_level))
(fun (function_parameter : int × int × Raw_level_repr.t) ⇒
let '(alice, bob, last_turn_level) := function_parameter in
{| timeout.alice := alice; timeout.bob := bob;
timeout.last_turn_level := last_turn_level; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "alice" Data_encoding.int31)
(Data_encoding.req None None "bob" Data_encoding.int31)
(Data_encoding.req None None "last_turn_level" Raw_level_repr.encoding)).
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(metadata : Sc_rollup_metadata_repr.t) (agreed_start_chunk : dissection_chunk)
(refuted_stop_chunk : dissection_chunk) (game : t)
(proof_value : Sc_rollup_proof_repr.t) : bool :=
validity_final_move dal_parameters dal_attestation_lag false metadata
proof_value game agreed_start_chunk refuted_stop_chunk.
Definition loser_of_results (alice_result : bool) (bob_result : bool)
: option player :=
match (alice_result, bob_result) with
| (true, true) ⇒ None
| (false, false) ⇒ None
| (false, true) ⇒ Some Alice
| (true, false) ⇒ Some Bob
end.
Definition play
(dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
(stakers : Index.t) (metadata : Sc_rollup_metadata_repr.t) (game : t)
(refutation : refutation) : M? (Either.t game_result t) :=
let mk_loser {A : Set} (loser : player) : Either.t game_result A :=
let loser := Index.staker stakers loser in
Either.Left
(Loser
{| game_result.Loser.reason := Conflict_resolved;
game_result.Loser.loser := loser; |}) in
match (refutation.(refutation.step), game.(V1.t.game_state)) with
|
(Dissection states,
V1.Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections
|}) ⇒
let? '(start_chunk, stop_chunk) :=
find_choice dissection refutation.(refutation.choice) in
let? '_ :=
Sc_rollup_dissection_chunk_repr.default_check default_number_of_sections
start_chunk stop_chunk states in
let new_game_state :=
V1.Dissecting
{| game_state.Dissecting.dissection := states;
game_state.Dissecting.default_number_of_sections :=
default_number_of_sections; |} in
return?
(Either.Right
{| V1.t.turn := opponent game.(V1.t.turn);
V1.t.inbox_snapshot := game.(V1.t.inbox_snapshot);
V1.t.dal_snapshot := game.(V1.t.dal_snapshot);
V1.t.start_level := game.(V1.t.start_level);
V1.t.inbox_level := game.(V1.t.inbox_level);
V1.t.pvm_name := game.(V1.t.pvm_name);
V1.t.game_state := new_game_state; |})
| (Dissection _, V1.Final_move _) ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Dissecting_during_final_move" unit tt)
|
(Proof proof_value,
V1.Dissecting {|
game_state.Dissecting.dissection := dissection;
game_state.Dissecting.default_number_of_sections := _
|}) ⇒
let? '(start_chunk, stop_chunk) :=
find_choice dissection refutation.(refutation.choice) in
let player_result :=
validity_first_final_move dal_parameters dal_attestation_lag metadata
proof_value game start_chunk stop_chunk in
if player_result then
return? (mk_loser (opponent game.(V1.t.turn)))
else
let new_game_state :=
let agreed_start_chunk := start_chunk in
let refuted_stop_chunk := stop_chunk in
V1.Final_move
{| game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk; |}
in
return?
(Either.Right
{| V1.t.turn := opponent game.(V1.t.turn);
V1.t.inbox_snapshot := game.(V1.t.inbox_snapshot);
V1.t.dal_snapshot := game.(V1.t.dal_snapshot);
V1.t.start_level := game.(V1.t.start_level);
V1.t.inbox_level := game.(V1.t.inbox_level);
V1.t.pvm_name := game.(V1.t.pvm_name);
V1.t.game_state := new_game_state; |})
|
(Proof proof_value,
V1.Final_move {|
game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk
|}) ⇒
let player_result :=
validity_second_final_move dal_parameters dal_attestation_lag metadata
agreed_start_chunk refuted_stop_chunk game proof_value in
if player_result then
return? (mk_loser (opponent game.(V1.t.turn)))
else
return? (Either.Left Draw)
end.
Module timeout.
Record record : Set := Build {
alice : int;
bob : int;
last_turn_level : Raw_level_repr.t;
}.
Definition with_alice alice (r : record) :=
Build alice r.(bob) r.(last_turn_level).
Definition with_bob bob (r : record) :=
Build r.(alice) bob r.(last_turn_level).
Definition with_last_turn_level last_turn_level (r : record) :=
Build r.(alice) r.(bob) last_turn_level.
End timeout.
Definition timeout := timeout.record.
Definition timeout_encoding : Data_encoding.encoding timeout :=
Data_encoding.conv
(fun (function_parameter : timeout) ⇒
let '{|
timeout.alice := alice;
timeout.bob := bob;
timeout.last_turn_level := last_turn_level
|} := function_parameter in
(alice, bob, last_turn_level))
(fun (function_parameter : int × int × Raw_level_repr.t) ⇒
let '(alice, bob, last_turn_level) := function_parameter in
{| timeout.alice := alice; timeout.bob := bob;
timeout.last_turn_level := last_turn_level; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "alice" Data_encoding.int31)
(Data_encoding.req None None "bob" Data_encoding.int31)
(Data_encoding.req None None "last_turn_level" Raw_level_repr.encoding)).