🦏 Sc_rollup_arith.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.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Non_empty_string.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Module PS := Sc_rollup_PVM_sig.
Definition reference_initial_state_hash : Sc_rollup_repr.State_hash.t :=
Sc_rollup_repr.State_hash.of_b58check_exn
"scs11cXwQJJ5dkpEQGq3x2MJm3cM73cbEkHJqo5eDSoRpHUPyEQLB4".
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Non_empty_string.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Module PS := Sc_rollup_PVM_sig.
Definition reference_initial_state_hash : Sc_rollup_repr.State_hash.t :=
Sc_rollup_repr.State_hash.of_b58check_exn
"scs11cXwQJJ5dkpEQGq3x2MJm3cM73cbEkHJqo5eDSoRpHUPyEQLB4".
Init function; without side-effects in Coq
Definition init_module : unit :=
let msg := "Invalid claim about outbox" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_arith_invalid_claim_about_outbox" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt msg)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Arith_invalid_claim_about_outbox" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Arith_invalid_claim_about_outbox" unit tt) in
let msg := "Output proof production failed" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_arith_output_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Arith_output_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Arith_output_proof_production_failed" unit tt) in
let msg := "Proof production failed" in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_arith_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Arith_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Arith_proof_production_failed" unit tt).
Module P.
Record signature {Tree_t Tree_tree proof : Set} : Set := {
Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes);
tree := Tree.(Context.TREE.tree);
hash_tree : tree → Sc_rollup_repr.State_hash.t;
proof := proof;
proof_encoding : Data_encoding.t proof;
proof_before : proof → Sc_rollup_repr.State_hash.t;
proof_after : proof → Sc_rollup_repr.State_hash.t;
verify_proof :
∀ {a : Set}, proof → (tree → tree × a) → option (tree × a);
produce_proof :
∀ {a : Set},
Tree.(Context.TREE.t) → tree → (tree → tree × a) → option (proof × a);
}.
End P.
Definition P := @P.signature.
Arguments P {_ _ _}.
Module S.
Record signature {state context proof output_proof status instruction : Set}
: Set := {
state := state;
pp : state → (Format.formatter → unit → unit);
context := context;
hash := Sc_rollup_repr.State_hash.t;
proof := proof;
proof_encoding : Data_encoding.t proof;
proof_start_state : proof → hash;
proof_stop_state : proof → hash;
state_hash : state → hash;
initial_state : state → state;
install_boot_sector : state → string → state;
is_input_state : state → Sc_rollup_PVM_sig.input_request;
set_input : Sc_rollup_PVM_sig.input → state → state;
eval : state → state;
verify_proof :
option Sc_rollup_PVM_sig.input → proof →
M? Sc_rollup_PVM_sig.input_request;
produce_proof :
context → option Sc_rollup_PVM_sig.input → state → M? proof;
verify_origination_proof : proof → string → bool;
produce_origination_proof : context → string → M? proof;
output_proof := output_proof;
output_proof_encoding : Data_encoding.t output_proof;
output_of_output_proof : output_proof → Sc_rollup_PVM_sig.output;
state_of_output_proof : output_proof → hash;
verify_output_proof : output_proof → bool;
produce_output_proof :
context → state → Sc_rollup_PVM_sig.output →
Pervasives.result output_proof Error_monad._error;
(* Internal_for_tests_insert_failure : state -> state; *)
name : string;
parse_boot_sector : string → option string;
pp_boot_sector : Format.formatter → string → unit;
get_tick : state → Sc_rollup_tick_repr.t;
status := status;
get_status : state → status;
get_outbox : Raw_level_repr.t → state → list Sc_rollup_PVM_sig.output;
instruction := instruction;
equal_instruction : instruction → instruction → bool;
pp_instruction : Format.formatter → instruction → unit;
get_parsing_result : state → option bool;
get_code : state → list instruction;
get_stack : state → list int;
get_var : state → string → option int;
get_evaluation_result : state → option bool;
get_is_stuck : state → option string;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _ _ _}.
Module Make.
Class FArgs {Context_Tree_t Context_Tree_tree Context_proof : Set} := {
Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof);
}.
Arguments Build_FArgs {_ _ _}.
Definition Tree `{FArgs} := Context.(P.Tree).
Definition context `{FArgs} : Set := Context.(P.Tree).(Context.TREE.t).
Definition hash `{FArgs} : Set := Sc_rollup_repr.State_hash.t.
Definition proof `{FArgs} : Set := Context.(P.proof).
Definition proof_encoding `{FArgs} : Data_encoding.t proof :=
Context.(P.proof_encoding).
Definition proof_start_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_before) proof_value.
Definition proof_stop_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_after) proof_value.
Definition name `{FArgs} : string := "arith".
Definition parse_boot_sector `{FArgs} {A : Set} (s_value : A) : option A :=
Some s_value.
Definition pp_boot_sector `{FArgs} (fmt : Format.formatter) (s_value : string)
: unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") s_value.
Definition tree `{FArgs} : Set := Context.(P.Tree).(Context.TREE.tree).
Inductive status `{FArgs} : Set :=
| Halted : status
| Waiting_for_input_message : status
| Waiting_for_reveal : status
| Waiting_for_metadata : status
| Parsing : status
| Evaluating : status.
Inductive instruction `{FArgs} : Set :=
| IPush : int → instruction
| IAdd : instruction
| IStore : string → instruction.
Definition equal_instruction `{FArgs} (i1 : instruction) (i2 : instruction)
: bool :=
match (i1, i2) with
| (IPush x_value, IPush y_value) ⇒ x_value =i y_value
| (IAdd, IAdd) ⇒ true
| (IStore x_value, IStore y_value) ⇒
Compare.String.(Compare.S.op_eq) x_value y_value
| (_, _) ⇒ false
end.
Definition pp_instruction `{FArgs}
(fmt : Format.formatter) (function_parameter : instruction) : unit :=
match function_parameter with
| IPush x_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "push("
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))) "push(%d)") x_value
| IAdd ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "add"
CamlinternalFormatBasics.End_of_format) "add")
| IStore x_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "store("
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))) "store(%s)") x_value
end.
Module State.
Definition state `{FArgs} : Set := tree.
Module Monad.
Definition t `{FArgs} (a : Set) : Set := state → state × option a.
Definition _return `{FArgs} {A B : Set} (x_value : A) (state_value : B)
: B × option A := (state_value, (Some x_value)).
Definition bind `{FArgs} {A B C D : Set}
(m_value : A → B × option C) (f_value : C → B → B × option D)
(state_value : A) : B × option D :=
let '(state_value, res) := m_value state_value in
match res with
| None ⇒ (state_value, None)
| Some res ⇒ f_value res state_value
end.
Module Syntax.
Definition op_letstar `{FArgs} {A B C D : Set}
: (A → B × option C) → (C → B → B × option D) → A → B × option D :=
bind.
End Syntax.
Definition run `{FArgs} {A B : Set} (m_value : A → B) (state_value : A)
: B := m_value state_value.
Definition internal_error_key `{FArgs} : list string :=
[ "internal_error" ].
Definition internal_error `{FArgs} {A : Set}
(msg : string) (tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option A :=
let tree_value :=
Tree.(Context.TREE.add) tree_value internal_error_key
(Bytes.of_string msg) in
(tree_value, None).
Definition is_stuck `{FArgs}
(tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option (option string) :=
let v_value := Tree.(Context.TREE.find) tree_value internal_error_key in
(tree_value, (Some (Option.map Bytes.to_string v_value))).
Definition remove `{FArgs}
(key_value : Tree.(Context.TREE.key))
(tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option unit :=
let tree_value := Tree.(Context.TREE.remove) tree_value key_value in
(tree_value, (Some tt)).
Definition decode `{FArgs} {A : Set}
(encoding : Data_encoding.encoding A) (bytes_value : bytes)
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option A :=
match Data_encoding.Binary.of_bytes_opt encoding bytes_value with
| None ⇒ internal_error "Error during decoding" state_value
| Some v_value ⇒ (state_value, (Some v_value))
end.
Definition find_value `{FArgs} {A : Set}
(key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A)
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option (option A) :=
let obytes := Tree.(Context.TREE.find) state_value key_value in
match obytes with
| None ⇒ (state_value, (Some None))
| Some bytes_value ⇒
let '(state_value, value_value) :=
decode encoding bytes_value state_value in
(state_value, (Some value_value))
end.
Definition children `{FArgs} {A : Set}
(key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A)
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option (list (string × A)) :=
let children :=
Tree.(Context.TREE.list_value) state_value None None key_value in
let fix aux {B : Set}
(function_parameter : list (B × Context.(P.Tree).(Context.TREE.tree)))
: Context.(P.Tree).(Context.TREE.tree) × option (list (B × A)) :=
match function_parameter with
| [] ⇒ (state_value, (Some nil))
| cons (key_value, tree_value) children ⇒
let obytes := Tree.(Context.TREE.to_value) tree_value in
match obytes with
| None ⇒ internal_error "Invalid children" state_value
| Some bytes_value ⇒
let '(state_value, v_value) :=
decode encoding bytes_value state_value in
match v_value with
| None ⇒ (state_value, None)
| Some v_value ⇒
let '(state_value, l_value) := aux children in
match l_value with
| None ⇒ (state_value, None)
| Some l_value ⇒
(state_value, (Some (cons (key_value, v_value) l_value)))
end
end
end
end in
aux children.
Definition get_value `{FArgs} {A : Set}
(default : A) (key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A)
: Context.(P.Tree).(Context.TREE.tree) →
Context.(P.Tree).(Context.TREE.tree) × option A :=
Syntax.op_letstar (find_value key_value encoding)
(fun ov ⇒
match ov with
| None ⇒ _return default
| Some x_value ⇒ _return x_value
end).
Definition set_value `{FArgs} {A : Set}
(key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A) (value_value : A)
(tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option unit :=
(fun (function_parameter : option bytes) ⇒
match function_parameter with
| None ⇒ internal_error "Internal_Error during encoding" tree_value
| Some bytes_value ⇒
let tree_value :=
Tree.(Context.TREE.add) tree_value key_value bytes_value in
(tree_value, (Some tt))
end) (Data_encoding.Binary.to_bytes_opt None encoding value_value).
End Monad.
Module P_MakeVar.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
name : string;
initial : t;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
}.
End P_MakeVar.
Definition P_MakeVar := @P_MakeVar.signature.
Arguments P_MakeVar {_ _ _ _ _}.
Module S_MakeVar.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
create : Monad.t unit;
get : Monad.t t;
set : t → Monad.t unit;
pp : Monad.t (Format.formatter → unit → unit);
}.
End S_MakeVar.
Definition S_MakeVar := @S_MakeVar.signature.
Arguments S_MakeVar {_ _ _ _ _}.
Module Make_var.
Class FArgs `{FArgs} {P_t : Set} := {
P : P_MakeVar (t := P_t);
}.
Arguments Build_FArgs {_ _ _ _ _}.
Definition key_value `{FArgs} : list string := [ P.(P_MakeVar.name) ].
Definition create `{FArgs} : Monad.t unit :=
Monad.set_value key_value P.(P_MakeVar.encoding) P.(P_MakeVar.initial).
Definition get `{FArgs} : Monad.t P.(P_MakeVar.t) :=
Monad.Syntax.op_letstar
(Monad.find_value key_value P.(P_MakeVar.encoding))
(fun v_value ⇒
match v_value with
| None ⇒ Monad._return P.(P_MakeVar.initial)
| Some v_value ⇒ Monad._return v_value
end).
Definition set `{FArgs} : P.(P_MakeVar.t) → Monad.t unit :=
Monad.set_value key_value P.(P_MakeVar.encoding).
Definition pp `{FArgs} : Monad.t (Format.formatter → unit → unit) :=
Monad.Syntax.op_letstar get
(fun v_value ⇒
Monad._return
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[%s : %a@]") P.(P_MakeVar.name) P.(P_MakeVar.pp) v_value)).
(* Make_var *)
Definition functor `{FArgs} :=
{|
S_MakeVar.create := create;
S_MakeVar.get := get;
S_MakeVar.set := set;
S_MakeVar.pp := pp
|}.
End Make_var.
Definition Make_var `{FArgs} {P_t : Set} (P : P_MakeVar (t := P_t))
: S_MakeVar (t := P.(P_MakeVar.t)) :=
let '_ := Make_var.Build_FArgs P in
Make_var.functor.
Module P_MakeDict.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
name : string;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
}.
End P_MakeDict.
Definition P_MakeDict := @P_MakeDict.signature.
Arguments P_MakeDict {_ _ _ _ _}.
Module MakeDict_sig.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
get : string → Monad.t (option t);
set : string → t → Monad.t unit;
entries : Monad.t (list (string × t));
mapped_to : string → t → state → bool;
pp : Monad.t (Format.formatter → unit → unit);
}.
End MakeDict_sig.
Definition MakeDict_sig := @MakeDict_sig.signature.
Arguments MakeDict_sig {_ _ _ _ _}.
Module Make_dict.
Class FArgs `{FArgs} {P_t : Set} := {
P : P_MakeDict (t := P_t);
}.
Arguments Build_FArgs {_ _ _ _ _}.
Definition key_value `{FArgs} (k_value : string) : list string :=
[ P.(P_MakeDict.name); k_value ].
Definition get `{FArgs} (k_value : string)
: Monad.t (option P.(P_MakeDict.t)) :=
Monad.find_value (key_value k_value) P.(P_MakeDict.encoding).
Definition set `{FArgs} (k_value : string) (v_value : P.(P_MakeDict.t))
: Monad.t unit :=
Monad.set_value (key_value k_value) P.(P_MakeDict.encoding) v_value.
Definition entries `{FArgs}
: Monad.t (list (string × P.(P_MakeDict.t))) :=
Monad.children [ P.(P_MakeDict.name) ] P.(P_MakeDict.encoding).
Definition mapped_to `{FArgs}
(k_value : string) (v_value : P.(P_MakeDict.t)) (state_value : state)
: bool :=
let '(state', _) := Monad.run (set k_value v_value) state_value in
let t_value :=
Tree.(Context.TREE.find_tree) state_value (key_value k_value) in
let t' := Tree.(Context.TREE.find_tree) state' (key_value k_value) in
Option.equal Tree.(Context.TREE.equal) t_value t'.
Definition pp `{FArgs} : Monad.t (Format.formatter → unit → unit) :=
Monad.Syntax.op_letstar entries
(fun l_value ⇒
let pp_elem
(fmt : Format.formatter)
(function_parameter : string × P.(P_MakeDict.t)) : unit :=
let '(key_value, value_value) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[%s : %a@]") key_value P.(P_MakeDict.pp) value_value in
Monad._return
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_list None pp_elem fmt l_value)).
(* Make_dict *)
Definition functor `{FArgs} :=
{|
MakeDict_sig.get := get;
MakeDict_sig.set := set;
MakeDict_sig.entries := entries;
MakeDict_sig.mapped_to := mapped_to;
MakeDict_sig.pp := pp
|}.
End Make_dict.
Definition Make_dict `{FArgs} {P_t : Set} (P : P_MakeDict (t := P_t))
: MakeDict_sig (t := P.(P_MakeDict.t)) :=
let '_ := Make_dict.Build_FArgs P in
Make_dict.functor.
Module P_deque.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
name : string;
encoding : Data_encoding.t t;
}.
End P_deque.
Definition P_deque := @P_deque.signature.
Arguments P_deque {_ _ _ _ _}.
Module MakeDeque_sig.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
top : Monad.t (option t);
push : t → Monad.t unit;
pop : Monad.t (option t);
inject : t → Monad.t unit;
to_list : Monad.t (list t);
clear : Monad.t unit;
}.
End MakeDeque_sig.
Definition MakeDeque_sig := @MakeDeque_sig.signature.
Arguments MakeDeque_sig {_ _ _ _ _}.
Module Make_deque.
Class FArgs `{FArgs} {P_t : Set} := {
P : P_deque (t := P_t);
}.
Arguments Build_FArgs {_ _ _ _ _}.
Definition head_key `{FArgs} : list string :=
[ P.(P_deque.name); "head" ].
Definition end_key `{FArgs} : list string := [ P.(P_deque.name); "end" ].
Definition get_head `{FArgs} : Monad.t Z.t :=
Monad.get_value Z.zero head_key Data_encoding.z_value.
Definition set_head `{FArgs} : Z.t → Monad.t unit :=
Monad.set_value head_key Data_encoding.z_value.
Definition get_end `{FArgs} : Monad.t Z.t :=
Monad.get_value (Z.of_int 0) end_key Data_encoding.z_value.
Definition set_end `{FArgs} : Z.t → Monad.t unit :=
Monad.set_value end_key Data_encoding.z_value.
Definition idx_key `{FArgs} (idx : Z.t) : list string :=
[ P.(P_deque.name); Z.to_string idx ].
Definition top `{FArgs} : Monad.t (option P.(P_deque.t)) :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
Monad.Syntax.op_letstar
(Monad.find_value (idx_key head_idx) P.(P_deque.encoding))
(fun v_value ⇒
if Z.leq end_idx head_idx then
Monad._return None
else
match v_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Monad.t (option P.(P_deque.t))) false
| Some x_value ⇒ Monad._return (Some x_value)
end))).
Definition push `{FArgs} (x_value : P.(P_deque.t)) : Monad.t unit :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
let head_idx' := Z.pred head_idx in
Monad.Syntax.op_letstar (set_head head_idx')
(fun function_parameter ⇒
let '_ := function_parameter in
Monad.set_value (idx_key head_idx') P.(P_deque.encoding) x_value)).
Definition pop `{FArgs} : Monad.t (option P.(P_deque.t)) :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
if Z.leq end_idx head_idx then
Monad._return None
else
Monad.Syntax.op_letstar
(Monad.find_value (idx_key head_idx) P.(P_deque.encoding))
(fun v_value ⇒
match v_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Monad.t (option P.(P_deque.t))) false
| Some x_value ⇒
Monad.Syntax.op_letstar
(Monad.remove (idx_key head_idx))
(fun function_parameter ⇒
let '_ := function_parameter in
let head_idx := Z.succ head_idx in
Monad.Syntax.op_letstar (set_head head_idx)
(fun function_parameter ⇒
let '_ := function_parameter in
Monad._return (Some x_value)))
end))).
Definition inject `{FArgs} (x_value : P.(P_deque.t)) : Monad.t unit :=
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
let end_idx' := Z.succ end_idx in
Monad.Syntax.op_letstar (set_end end_idx')
(fun function_parameter ⇒
let '_ := function_parameter in
Monad.set_value (idx_key end_idx) P.(P_deque.encoding) x_value)).
#[bypass_check(guard)]
Definition to_list `{FArgs} : Monad.t (list P.(P_deque.t)) :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
let fix aux (l_value : list P.(P_deque.t)) (idx : Z.t)
{struct idx} : Monad.t (list P.(P_deque.t)) :=
if Z.lt idx head_idx then
Monad._return l_value
else
Monad.Syntax.op_letstar
(Monad.find_value (idx_key idx) P.(P_deque.encoding))
(fun v_value ⇒
match v_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Monad.t (list P.(P_deque.t))) false
| Some v_value ⇒
aux (cons v_value l_value) (Z.pred idx)
end) in
aux nil (Z.pred end_idx))).
Definition clear `{FArgs} : Monad.t unit :=
Monad.remove [ P.(P_deque.name) ].
(* Make_deque *)
Definition functor `{FArgs} :=
{|
MakeDeque_sig.top := top;
MakeDeque_sig.push := push;
MakeDeque_sig.pop := pop;
MakeDeque_sig.inject := inject;
MakeDeque_sig.to_list := to_list;
MakeDeque_sig.clear := clear
|}.
End Make_deque.
Definition Make_deque `{FArgs} {P_t : Set} (P : P_deque (t := P_t))
: MakeDeque_sig (t := P.(P_deque.t)) :=
let '_ := Make_deque.Build_FArgs P in
Make_deque.functor.
Definition Current_tick `{FArgs} :=
Make_var
(let t : Set := Sc_rollup_tick_repr.t in
let name := "tick" in
let initial := Sc_rollup_tick_repr.initial in
let pp := Sc_rollup_tick_repr.pp in
let encoding := Sc_rollup_tick_repr.encoding in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Vars `{FArgs} :=
Make_dict
(let t : Set := int in
let name := "vars" in
let encoding := Data_encoding.int31 in
let pp (fmt : Format.formatter) (x_value : int) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%d") x_value in
{|
P_MakeDict.name := name;
P_MakeDict.pp := pp;
P_MakeDict.encoding := encoding
|}).
Definition Stack `{FArgs} :=
Make_deque
(let t : Set := int in
let name := "stack" in
let encoding := Data_encoding.int31 in
{|
P_deque.name := name;
P_deque.encoding := encoding
|}).
Definition Code `{FArgs} :=
Make_deque
(let t : Set := instruction in
let name := "code" in
let encoding :=
Data_encoding.union None
[
Data_encoding.case_value "push" None (Data_encoding.Tag 0)
Data_encoding.int31
(fun (function_parameter : instruction) ⇒
match function_parameter with
| IPush x_value ⇒ Some x_value
| _ ⇒ None
end)
(fun (x_value : int) ⇒ IPush x_value);
Data_encoding.case_value "add" None (Data_encoding.Tag 1)
Data_encoding.unit_value
(fun (function_parameter : instruction) ⇒
match function_parameter with
| IAdd ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
IAdd);
Data_encoding.case_value "store" None (Data_encoding.Tag 2)
Data_encoding.string_value
(fun (function_parameter : instruction) ⇒
match function_parameter with
| IStore x_value ⇒ Some x_value
| _ ⇒ None
end)
(fun (x_value : string) ⇒ IStore x_value)
] in
{|
P_deque.name := name;
P_deque.encoding := encoding
|}).
Definition Boot_sector `{FArgs} :=
Make_var
(let t : Set := string in
let name := "boot_sector" in
let initial := "" in
let encoding := Data_encoding.string_value in
let pp (fmt : Format.formatter) (s_value : string) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") s_value in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Status `{FArgs} :=
Make_var
(let t : Set := status in
let initial := Halted in
let encoding :=
Data_encoding.string_enum
[
("Halted", Halted);
("Waiting_for_input_message", Waiting_for_input_message);
("Waiting_for_reveal", Waiting_for_reveal);
("Waiting_for_metadata", Waiting_for_metadata);
("Parsing", Parsing);
("Evaluating", Evaluating)
] in
let name := "status" in
let string_of_status (function_parameter : status) : string :=
match function_parameter with
| Halted ⇒ "Halted"
| Waiting_for_input_message ⇒ "Waiting for input message"
| Waiting_for_reveal ⇒ "Waiting for reveal"
| Waiting_for_metadata ⇒ "Waiting for metadata"
| Parsing ⇒ "Parsing"
| Evaluating ⇒ "Evaluating"
end in
let pp (fmt : Format.formatter) (status : status) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
(string_of_status status) in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Required_reveal `{FArgs} :=
Make_var
(let t : Set := option PS.reveal in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value PS.reveal_encoding in
let name := "required_reveal" in
let pp (fmt : Format.formatter) (v_value : option PS.reveal) : unit :=
match v_value with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<none>"
CamlinternalFormatBasics.End_of_format) "<none>")
| Some h_value ⇒ PS.pp_reveal fmt h_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Metadata `{FArgs} :=
Make_var
(let t : Set := option Sc_rollup_metadata_repr.t in
let initial {A : Set} : option A :=
None in
let encoding :=
Data_encoding.option_value Sc_rollup_metadata_repr.encoding in
let name := "metadata" in
let pp
(fmt : Format.formatter) (v_value : option Sc_rollup_metadata_repr.t)
: unit :=
match v_value with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<none>"
CamlinternalFormatBasics.End_of_format) "<none>")
| Some v_value ⇒ Sc_rollup_metadata_repr.pp fmt v_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Current_level `{FArgs} :=
Make_var
(let t : Set := Raw_level_repr.t in
let initial := Raw_level_repr.root_value in
let encoding := Raw_level_repr.encoding in
let name := "current_level" in
let pp := Raw_level_repr.pp in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Message_counter `{FArgs} :=
Make_var
(let t : Set := option Z.t in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.n_value in
let name := "message_counter" in
let pp (fmt : Format.formatter) (function_parameter : option Z.t)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "None"
CamlinternalFormatBasics.End_of_format) "None")
| Some c_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Some "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "Some %a")
Z.pp_print c_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
let msg := "Invalid claim about outbox" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_arith_invalid_claim_about_outbox" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt msg)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Arith_invalid_claim_about_outbox" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Arith_invalid_claim_about_outbox" unit tt) in
let msg := "Output proof production failed" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_arith_output_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Arith_output_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Arith_output_proof_production_failed" unit tt) in
let msg := "Proof production failed" in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_arith_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Arith_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Arith_proof_production_failed" unit tt).
Module P.
Record signature {Tree_t Tree_tree proof : Set} : Set := {
Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes);
tree := Tree.(Context.TREE.tree);
hash_tree : tree → Sc_rollup_repr.State_hash.t;
proof := proof;
proof_encoding : Data_encoding.t proof;
proof_before : proof → Sc_rollup_repr.State_hash.t;
proof_after : proof → Sc_rollup_repr.State_hash.t;
verify_proof :
∀ {a : Set}, proof → (tree → tree × a) → option (tree × a);
produce_proof :
∀ {a : Set},
Tree.(Context.TREE.t) → tree → (tree → tree × a) → option (proof × a);
}.
End P.
Definition P := @P.signature.
Arguments P {_ _ _}.
Module S.
Record signature {state context proof output_proof status instruction : Set}
: Set := {
state := state;
pp : state → (Format.formatter → unit → unit);
context := context;
hash := Sc_rollup_repr.State_hash.t;
proof := proof;
proof_encoding : Data_encoding.t proof;
proof_start_state : proof → hash;
proof_stop_state : proof → hash;
state_hash : state → hash;
initial_state : state → state;
install_boot_sector : state → string → state;
is_input_state : state → Sc_rollup_PVM_sig.input_request;
set_input : Sc_rollup_PVM_sig.input → state → state;
eval : state → state;
verify_proof :
option Sc_rollup_PVM_sig.input → proof →
M? Sc_rollup_PVM_sig.input_request;
produce_proof :
context → option Sc_rollup_PVM_sig.input → state → M? proof;
verify_origination_proof : proof → string → bool;
produce_origination_proof : context → string → M? proof;
output_proof := output_proof;
output_proof_encoding : Data_encoding.t output_proof;
output_of_output_proof : output_proof → Sc_rollup_PVM_sig.output;
state_of_output_proof : output_proof → hash;
verify_output_proof : output_proof → bool;
produce_output_proof :
context → state → Sc_rollup_PVM_sig.output →
Pervasives.result output_proof Error_monad._error;
(* Internal_for_tests_insert_failure : state -> state; *)
name : string;
parse_boot_sector : string → option string;
pp_boot_sector : Format.formatter → string → unit;
get_tick : state → Sc_rollup_tick_repr.t;
status := status;
get_status : state → status;
get_outbox : Raw_level_repr.t → state → list Sc_rollup_PVM_sig.output;
instruction := instruction;
equal_instruction : instruction → instruction → bool;
pp_instruction : Format.formatter → instruction → unit;
get_parsing_result : state → option bool;
get_code : state → list instruction;
get_stack : state → list int;
get_var : state → string → option int;
get_evaluation_result : state → option bool;
get_is_stuck : state → option string;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _ _ _}.
Module Make.
Class FArgs {Context_Tree_t Context_Tree_tree Context_proof : Set} := {
Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof);
}.
Arguments Build_FArgs {_ _ _}.
Definition Tree `{FArgs} := Context.(P.Tree).
Definition context `{FArgs} : Set := Context.(P.Tree).(Context.TREE.t).
Definition hash `{FArgs} : Set := Sc_rollup_repr.State_hash.t.
Definition proof `{FArgs} : Set := Context.(P.proof).
Definition proof_encoding `{FArgs} : Data_encoding.t proof :=
Context.(P.proof_encoding).
Definition proof_start_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_before) proof_value.
Definition proof_stop_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_after) proof_value.
Definition name `{FArgs} : string := "arith".
Definition parse_boot_sector `{FArgs} {A : Set} (s_value : A) : option A :=
Some s_value.
Definition pp_boot_sector `{FArgs} (fmt : Format.formatter) (s_value : string)
: unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") s_value.
Definition tree `{FArgs} : Set := Context.(P.Tree).(Context.TREE.tree).
Inductive status `{FArgs} : Set :=
| Halted : status
| Waiting_for_input_message : status
| Waiting_for_reveal : status
| Waiting_for_metadata : status
| Parsing : status
| Evaluating : status.
Inductive instruction `{FArgs} : Set :=
| IPush : int → instruction
| IAdd : instruction
| IStore : string → instruction.
Definition equal_instruction `{FArgs} (i1 : instruction) (i2 : instruction)
: bool :=
match (i1, i2) with
| (IPush x_value, IPush y_value) ⇒ x_value =i y_value
| (IAdd, IAdd) ⇒ true
| (IStore x_value, IStore y_value) ⇒
Compare.String.(Compare.S.op_eq) x_value y_value
| (_, _) ⇒ false
end.
Definition pp_instruction `{FArgs}
(fmt : Format.formatter) (function_parameter : instruction) : unit :=
match function_parameter with
| IPush x_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "push("
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))) "push(%d)") x_value
| IAdd ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "add"
CamlinternalFormatBasics.End_of_format) "add")
| IStore x_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "store("
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))) "store(%s)") x_value
end.
Module State.
Definition state `{FArgs} : Set := tree.
Module Monad.
Definition t `{FArgs} (a : Set) : Set := state → state × option a.
Definition _return `{FArgs} {A B : Set} (x_value : A) (state_value : B)
: B × option A := (state_value, (Some x_value)).
Definition bind `{FArgs} {A B C D : Set}
(m_value : A → B × option C) (f_value : C → B → B × option D)
(state_value : A) : B × option D :=
let '(state_value, res) := m_value state_value in
match res with
| None ⇒ (state_value, None)
| Some res ⇒ f_value res state_value
end.
Module Syntax.
Definition op_letstar `{FArgs} {A B C D : Set}
: (A → B × option C) → (C → B → B × option D) → A → B × option D :=
bind.
End Syntax.
Definition run `{FArgs} {A B : Set} (m_value : A → B) (state_value : A)
: B := m_value state_value.
Definition internal_error_key `{FArgs} : list string :=
[ "internal_error" ].
Definition internal_error `{FArgs} {A : Set}
(msg : string) (tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option A :=
let tree_value :=
Tree.(Context.TREE.add) tree_value internal_error_key
(Bytes.of_string msg) in
(tree_value, None).
Definition is_stuck `{FArgs}
(tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option (option string) :=
let v_value := Tree.(Context.TREE.find) tree_value internal_error_key in
(tree_value, (Some (Option.map Bytes.to_string v_value))).
Definition remove `{FArgs}
(key_value : Tree.(Context.TREE.key))
(tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option unit :=
let tree_value := Tree.(Context.TREE.remove) tree_value key_value in
(tree_value, (Some tt)).
Definition decode `{FArgs} {A : Set}
(encoding : Data_encoding.encoding A) (bytes_value : bytes)
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option A :=
match Data_encoding.Binary.of_bytes_opt encoding bytes_value with
| None ⇒ internal_error "Error during decoding" state_value
| Some v_value ⇒ (state_value, (Some v_value))
end.
Definition find_value `{FArgs} {A : Set}
(key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A)
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option (option A) :=
let obytes := Tree.(Context.TREE.find) state_value key_value in
match obytes with
| None ⇒ (state_value, (Some None))
| Some bytes_value ⇒
let '(state_value, value_value) :=
decode encoding bytes_value state_value in
(state_value, (Some value_value))
end.
Definition children `{FArgs} {A : Set}
(key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A)
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option (list (string × A)) :=
let children :=
Tree.(Context.TREE.list_value) state_value None None key_value in
let fix aux {B : Set}
(function_parameter : list (B × Context.(P.Tree).(Context.TREE.tree)))
: Context.(P.Tree).(Context.TREE.tree) × option (list (B × A)) :=
match function_parameter with
| [] ⇒ (state_value, (Some nil))
| cons (key_value, tree_value) children ⇒
let obytes := Tree.(Context.TREE.to_value) tree_value in
match obytes with
| None ⇒ internal_error "Invalid children" state_value
| Some bytes_value ⇒
let '(state_value, v_value) :=
decode encoding bytes_value state_value in
match v_value with
| None ⇒ (state_value, None)
| Some v_value ⇒
let '(state_value, l_value) := aux children in
match l_value with
| None ⇒ (state_value, None)
| Some l_value ⇒
(state_value, (Some (cons (key_value, v_value) l_value)))
end
end
end
end in
aux children.
Definition get_value `{FArgs} {A : Set}
(default : A) (key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A)
: Context.(P.Tree).(Context.TREE.tree) →
Context.(P.Tree).(Context.TREE.tree) × option A :=
Syntax.op_letstar (find_value key_value encoding)
(fun ov ⇒
match ov with
| None ⇒ _return default
| Some x_value ⇒ _return x_value
end).
Definition set_value `{FArgs} {A : Set}
(key_value : Tree.(Context.TREE.key))
(encoding : Data_encoding.encoding A) (value_value : A)
(tree_value : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) × option unit :=
(fun (function_parameter : option bytes) ⇒
match function_parameter with
| None ⇒ internal_error "Internal_Error during encoding" tree_value
| Some bytes_value ⇒
let tree_value :=
Tree.(Context.TREE.add) tree_value key_value bytes_value in
(tree_value, (Some tt))
end) (Data_encoding.Binary.to_bytes_opt None encoding value_value).
End Monad.
Module P_MakeVar.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
name : string;
initial : t;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
}.
End P_MakeVar.
Definition P_MakeVar := @P_MakeVar.signature.
Arguments P_MakeVar {_ _ _ _ _}.
Module S_MakeVar.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
create : Monad.t unit;
get : Monad.t t;
set : t → Monad.t unit;
pp : Monad.t (Format.formatter → unit → unit);
}.
End S_MakeVar.
Definition S_MakeVar := @S_MakeVar.signature.
Arguments S_MakeVar {_ _ _ _ _}.
Module Make_var.
Class FArgs `{FArgs} {P_t : Set} := {
P : P_MakeVar (t := P_t);
}.
Arguments Build_FArgs {_ _ _ _ _}.
Definition key_value `{FArgs} : list string := [ P.(P_MakeVar.name) ].
Definition create `{FArgs} : Monad.t unit :=
Monad.set_value key_value P.(P_MakeVar.encoding) P.(P_MakeVar.initial).
Definition get `{FArgs} : Monad.t P.(P_MakeVar.t) :=
Monad.Syntax.op_letstar
(Monad.find_value key_value P.(P_MakeVar.encoding))
(fun v_value ⇒
match v_value with
| None ⇒ Monad._return P.(P_MakeVar.initial)
| Some v_value ⇒ Monad._return v_value
end).
Definition set `{FArgs} : P.(P_MakeVar.t) → Monad.t unit :=
Monad.set_value key_value P.(P_MakeVar.encoding).
Definition pp `{FArgs} : Monad.t (Format.formatter → unit → unit) :=
Monad.Syntax.op_letstar get
(fun v_value ⇒
Monad._return
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[%s : %a@]") P.(P_MakeVar.name) P.(P_MakeVar.pp) v_value)).
(* Make_var *)
Definition functor `{FArgs} :=
{|
S_MakeVar.create := create;
S_MakeVar.get := get;
S_MakeVar.set := set;
S_MakeVar.pp := pp
|}.
End Make_var.
Definition Make_var `{FArgs} {P_t : Set} (P : P_MakeVar (t := P_t))
: S_MakeVar (t := P.(P_MakeVar.t)) :=
let '_ := Make_var.Build_FArgs P in
Make_var.functor.
Module P_MakeDict.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
name : string;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
}.
End P_MakeDict.
Definition P_MakeDict := @P_MakeDict.signature.
Arguments P_MakeDict {_ _ _ _ _}.
Module MakeDict_sig.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
get : string → Monad.t (option t);
set : string → t → Monad.t unit;
entries : Monad.t (list (string × t));
mapped_to : string → t → state → bool;
pp : Monad.t (Format.formatter → unit → unit);
}.
End MakeDict_sig.
Definition MakeDict_sig := @MakeDict_sig.signature.
Arguments MakeDict_sig {_ _ _ _ _}.
Module Make_dict.
Class FArgs `{FArgs} {P_t : Set} := {
P : P_MakeDict (t := P_t);
}.
Arguments Build_FArgs {_ _ _ _ _}.
Definition key_value `{FArgs} (k_value : string) : list string :=
[ P.(P_MakeDict.name); k_value ].
Definition get `{FArgs} (k_value : string)
: Monad.t (option P.(P_MakeDict.t)) :=
Monad.find_value (key_value k_value) P.(P_MakeDict.encoding).
Definition set `{FArgs} (k_value : string) (v_value : P.(P_MakeDict.t))
: Monad.t unit :=
Monad.set_value (key_value k_value) P.(P_MakeDict.encoding) v_value.
Definition entries `{FArgs}
: Monad.t (list (string × P.(P_MakeDict.t))) :=
Monad.children [ P.(P_MakeDict.name) ] P.(P_MakeDict.encoding).
Definition mapped_to `{FArgs}
(k_value : string) (v_value : P.(P_MakeDict.t)) (state_value : state)
: bool :=
let '(state', _) := Monad.run (set k_value v_value) state_value in
let t_value :=
Tree.(Context.TREE.find_tree) state_value (key_value k_value) in
let t' := Tree.(Context.TREE.find_tree) state' (key_value k_value) in
Option.equal Tree.(Context.TREE.equal) t_value t'.
Definition pp `{FArgs} : Monad.t (Format.formatter → unit → unit) :=
Monad.Syntax.op_letstar entries
(fun l_value ⇒
let pp_elem
(fmt : Format.formatter)
(function_parameter : string × P.(P_MakeDict.t)) : unit :=
let '(key_value, value_value) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[%s : %a@]") key_value P.(P_MakeDict.pp) value_value in
Monad._return
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_list None pp_elem fmt l_value)).
(* Make_dict *)
Definition functor `{FArgs} :=
{|
MakeDict_sig.get := get;
MakeDict_sig.set := set;
MakeDict_sig.entries := entries;
MakeDict_sig.mapped_to := mapped_to;
MakeDict_sig.pp := pp
|}.
End Make_dict.
Definition Make_dict `{FArgs} {P_t : Set} (P : P_MakeDict (t := P_t))
: MakeDict_sig (t := P.(P_MakeDict.t)) :=
let '_ := Make_dict.Build_FArgs P in
Make_dict.functor.
Module P_deque.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
name : string;
encoding : Data_encoding.t t;
}.
End P_deque.
Definition P_deque := @P_deque.signature.
Arguments P_deque {_ _ _ _ _}.
Module MakeDeque_sig.
Record signature `{FArgs} {t : Set} : Set := {
t := t;
top : Monad.t (option t);
push : t → Monad.t unit;
pop : Monad.t (option t);
inject : t → Monad.t unit;
to_list : Monad.t (list t);
clear : Monad.t unit;
}.
End MakeDeque_sig.
Definition MakeDeque_sig := @MakeDeque_sig.signature.
Arguments MakeDeque_sig {_ _ _ _ _}.
Module Make_deque.
Class FArgs `{FArgs} {P_t : Set} := {
P : P_deque (t := P_t);
}.
Arguments Build_FArgs {_ _ _ _ _}.
Definition head_key `{FArgs} : list string :=
[ P.(P_deque.name); "head" ].
Definition end_key `{FArgs} : list string := [ P.(P_deque.name); "end" ].
Definition get_head `{FArgs} : Monad.t Z.t :=
Monad.get_value Z.zero head_key Data_encoding.z_value.
Definition set_head `{FArgs} : Z.t → Monad.t unit :=
Monad.set_value head_key Data_encoding.z_value.
Definition get_end `{FArgs} : Monad.t Z.t :=
Monad.get_value (Z.of_int 0) end_key Data_encoding.z_value.
Definition set_end `{FArgs} : Z.t → Monad.t unit :=
Monad.set_value end_key Data_encoding.z_value.
Definition idx_key `{FArgs} (idx : Z.t) : list string :=
[ P.(P_deque.name); Z.to_string idx ].
Definition top `{FArgs} : Monad.t (option P.(P_deque.t)) :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
Monad.Syntax.op_letstar
(Monad.find_value (idx_key head_idx) P.(P_deque.encoding))
(fun v_value ⇒
if Z.leq end_idx head_idx then
Monad._return None
else
match v_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Monad.t (option P.(P_deque.t))) false
| Some x_value ⇒ Monad._return (Some x_value)
end))).
Definition push `{FArgs} (x_value : P.(P_deque.t)) : Monad.t unit :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
let head_idx' := Z.pred head_idx in
Monad.Syntax.op_letstar (set_head head_idx')
(fun function_parameter ⇒
let '_ := function_parameter in
Monad.set_value (idx_key head_idx') P.(P_deque.encoding) x_value)).
Definition pop `{FArgs} : Monad.t (option P.(P_deque.t)) :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
if Z.leq end_idx head_idx then
Monad._return None
else
Monad.Syntax.op_letstar
(Monad.find_value (idx_key head_idx) P.(P_deque.encoding))
(fun v_value ⇒
match v_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Monad.t (option P.(P_deque.t))) false
| Some x_value ⇒
Monad.Syntax.op_letstar
(Monad.remove (idx_key head_idx))
(fun function_parameter ⇒
let '_ := function_parameter in
let head_idx := Z.succ head_idx in
Monad.Syntax.op_letstar (set_head head_idx)
(fun function_parameter ⇒
let '_ := function_parameter in
Monad._return (Some x_value)))
end))).
Definition inject `{FArgs} (x_value : P.(P_deque.t)) : Monad.t unit :=
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
let end_idx' := Z.succ end_idx in
Monad.Syntax.op_letstar (set_end end_idx')
(fun function_parameter ⇒
let '_ := function_parameter in
Monad.set_value (idx_key end_idx) P.(P_deque.encoding) x_value)).
#[bypass_check(guard)]
Definition to_list `{FArgs} : Monad.t (list P.(P_deque.t)) :=
Monad.Syntax.op_letstar get_head
(fun head_idx ⇒
Monad.Syntax.op_letstar get_end
(fun end_idx ⇒
let fix aux (l_value : list P.(P_deque.t)) (idx : Z.t)
{struct idx} : Monad.t (list P.(P_deque.t)) :=
if Z.lt idx head_idx then
Monad._return l_value
else
Monad.Syntax.op_letstar
(Monad.find_value (idx_key idx) P.(P_deque.encoding))
(fun v_value ⇒
match v_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Monad.t (list P.(P_deque.t))) false
| Some v_value ⇒
aux (cons v_value l_value) (Z.pred idx)
end) in
aux nil (Z.pred end_idx))).
Definition clear `{FArgs} : Monad.t unit :=
Monad.remove [ P.(P_deque.name) ].
(* Make_deque *)
Definition functor `{FArgs} :=
{|
MakeDeque_sig.top := top;
MakeDeque_sig.push := push;
MakeDeque_sig.pop := pop;
MakeDeque_sig.inject := inject;
MakeDeque_sig.to_list := to_list;
MakeDeque_sig.clear := clear
|}.
End Make_deque.
Definition Make_deque `{FArgs} {P_t : Set} (P : P_deque (t := P_t))
: MakeDeque_sig (t := P.(P_deque.t)) :=
let '_ := Make_deque.Build_FArgs P in
Make_deque.functor.
Definition Current_tick `{FArgs} :=
Make_var
(let t : Set := Sc_rollup_tick_repr.t in
let name := "tick" in
let initial := Sc_rollup_tick_repr.initial in
let pp := Sc_rollup_tick_repr.pp in
let encoding := Sc_rollup_tick_repr.encoding in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Vars `{FArgs} :=
Make_dict
(let t : Set := int in
let name := "vars" in
let encoding := Data_encoding.int31 in
let pp (fmt : Format.formatter) (x_value : int) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%d") x_value in
{|
P_MakeDict.name := name;
P_MakeDict.pp := pp;
P_MakeDict.encoding := encoding
|}).
Definition Stack `{FArgs} :=
Make_deque
(let t : Set := int in
let name := "stack" in
let encoding := Data_encoding.int31 in
{|
P_deque.name := name;
P_deque.encoding := encoding
|}).
Definition Code `{FArgs} :=
Make_deque
(let t : Set := instruction in
let name := "code" in
let encoding :=
Data_encoding.union None
[
Data_encoding.case_value "push" None (Data_encoding.Tag 0)
Data_encoding.int31
(fun (function_parameter : instruction) ⇒
match function_parameter with
| IPush x_value ⇒ Some x_value
| _ ⇒ None
end)
(fun (x_value : int) ⇒ IPush x_value);
Data_encoding.case_value "add" None (Data_encoding.Tag 1)
Data_encoding.unit_value
(fun (function_parameter : instruction) ⇒
match function_parameter with
| IAdd ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
IAdd);
Data_encoding.case_value "store" None (Data_encoding.Tag 2)
Data_encoding.string_value
(fun (function_parameter : instruction) ⇒
match function_parameter with
| IStore x_value ⇒ Some x_value
| _ ⇒ None
end)
(fun (x_value : string) ⇒ IStore x_value)
] in
{|
P_deque.name := name;
P_deque.encoding := encoding
|}).
Definition Boot_sector `{FArgs} :=
Make_var
(let t : Set := string in
let name := "boot_sector" in
let initial := "" in
let encoding := Data_encoding.string_value in
let pp (fmt : Format.formatter) (s_value : string) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") s_value in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Status `{FArgs} :=
Make_var
(let t : Set := status in
let initial := Halted in
let encoding :=
Data_encoding.string_enum
[
("Halted", Halted);
("Waiting_for_input_message", Waiting_for_input_message);
("Waiting_for_reveal", Waiting_for_reveal);
("Waiting_for_metadata", Waiting_for_metadata);
("Parsing", Parsing);
("Evaluating", Evaluating)
] in
let name := "status" in
let string_of_status (function_parameter : status) : string :=
match function_parameter with
| Halted ⇒ "Halted"
| Waiting_for_input_message ⇒ "Waiting for input message"
| Waiting_for_reveal ⇒ "Waiting for reveal"
| Waiting_for_metadata ⇒ "Waiting for metadata"
| Parsing ⇒ "Parsing"
| Evaluating ⇒ "Evaluating"
end in
let pp (fmt : Format.formatter) (status : status) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
(string_of_status status) in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Required_reveal `{FArgs} :=
Make_var
(let t : Set := option PS.reveal in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value PS.reveal_encoding in
let name := "required_reveal" in
let pp (fmt : Format.formatter) (v_value : option PS.reveal) : unit :=
match v_value with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<none>"
CamlinternalFormatBasics.End_of_format) "<none>")
| Some h_value ⇒ PS.pp_reveal fmt h_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Metadata `{FArgs} :=
Make_var
(let t : Set := option Sc_rollup_metadata_repr.t in
let initial {A : Set} : option A :=
None in
let encoding :=
Data_encoding.option_value Sc_rollup_metadata_repr.encoding in
let name := "metadata" in
let pp
(fmt : Format.formatter) (v_value : option Sc_rollup_metadata_repr.t)
: unit :=
match v_value with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<none>"
CamlinternalFormatBasics.End_of_format) "<none>")
| Some v_value ⇒ Sc_rollup_metadata_repr.pp fmt v_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Current_level `{FArgs} :=
Make_var
(let t : Set := Raw_level_repr.t in
let initial := Raw_level_repr.root_value in
let encoding := Raw_level_repr.encoding in
let name := "current_level" in
let pp := Raw_level_repr.pp in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Message_counter `{FArgs} :=
Make_var
(let t : Set := option Z.t in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.n_value in
let name := "message_counter" in
let pp (fmt : Format.formatter) (function_parameter : option Z.t)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "None"
CamlinternalFormatBasics.End_of_format) "None")
| Some c_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Some "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "Some %a")
Z.pp_print c_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Store an internal message counter. This is used to distinguish
an unparsable external message and a internal message, which we both
treat as no-ops.
Definition Internal_message_counter `{FArgs} :=
Make_var
(let t : Set := Z.t in
let initial := Z.zero in
let encoding := Data_encoding.n_value in
let name := "internal_message_counter" in
let pp (fmt : Format.formatter) (c_value : Z.t) : unit :=
Z.pp_print fmt c_value in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition incr_internal_message_counter `{FArgs} : Monad.t unit :=
Monad.Syntax.op_letstar Internal_message_counter.(S_MakeVar.get)
(fun current_counter ⇒
Internal_message_counter.(S_MakeVar.set) (Z.succ current_counter)).
Definition Next_message `{FArgs} :=
Make_var
(let t : Set := option string in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.string_value in
let name := "next_message" in
let pp (fmt : Format.formatter) (function_parameter : option string)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "None"
CamlinternalFormatBasics.End_of_format) "None")
| Some s_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Some "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format)) "Some %s") s_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Inductive parser_state `{FArgs} : Set :=
| ParseInt : parser_state
| ParseVar : parser_state
| SkipLayout : parser_state.
Definition Lexer_state `{FArgs} :=
Make_var
(let t : Set := int × int in
let name := "lexer_buffer" in
let initial := ((-1), (-1)) in
let encoding :=
Data_encoding.tup2 Data_encoding.int31 Data_encoding.int31 in
let pp (fmt : Format.formatter) (function_parameter : int × int)
: unit :=
let '(start, len) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "lexer.(start = "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", len = "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"lexer.(start = %d, len = %d)") start len in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Parser_state `{FArgs} :=
Make_var
(let t : Set := parser_state in
let name := "parser_state" in
let initial := SkipLayout in
let encoding :=
Data_encoding.string_enum
[
("ParseInt", ParseInt);
("ParseVar", ParseVar);
("SkipLayout", SkipLayout)
] in
let pp (fmt : Format.formatter) (function_parameter : parser_state)
: unit :=
match function_parameter with
| ParseInt ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Parsing int"
CamlinternalFormatBasics.End_of_format) "Parsing int")
| ParseVar ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Parsing var"
CamlinternalFormatBasics.End_of_format) "Parsing var")
| SkipLayout ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Skipping layout"
CamlinternalFormatBasics.End_of_format) "Skipping layout")
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Parsing_result `{FArgs} :=
Make_var
(let t : Set := option bool in
let name := "parsing_result" in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.bool_value in
let pp (fmt : Format.formatter) (function_parameter : option bool)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "n/a"
CamlinternalFormatBasics.End_of_format) "n/a")
| Some true ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "parsing succeeds"
CamlinternalFormatBasics.End_of_format) "parsing succeeds")
| Some false ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "parsing fails"
CamlinternalFormatBasics.End_of_format) "parsing fails")
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Evaluation_result `{FArgs} :=
Make_var
(let t : Set := option bool in
let name := "evaluation_result" in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.bool_value in
let pp (fmt : Format.formatter) (function_parameter : option bool)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "n/a"
CamlinternalFormatBasics.End_of_format) "n/a")
| Some true ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "evaluation succeeds"
CamlinternalFormatBasics.End_of_format) "evaluation succeeds")
| Some false ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "evaluation fails"
CamlinternalFormatBasics.End_of_format) "evaluation fails")
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Output_counter `{FArgs} :=
Make_var
(let t : Set := Z.t in
let initial := Z.zero in
let name := "output_counter" in
let encoding := Data_encoding.n_value in
let pp := Z.pp_print in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Output `{FArgs} :=
Make_dict
(let t : Set := Sc_rollup_PVM_sig.output in
let name := "output" in
let encoding := Sc_rollup_PVM_sig.output_encoding in
let pp := Sc_rollup_PVM_sig.pp_output in
{|
P_MakeDict.name := name;
P_MakeDict.pp := pp;
P_MakeDict.encoding := encoding
|}).
Definition pp `{FArgs} : Monad.t (Format.formatter → unit → unit) :=
Monad.Syntax.op_letstar Status.(S_MakeVar.pp)
(fun status_pp ⇒
Monad.Syntax.op_letstar Message_counter.(S_MakeVar.pp)
(fun message_counter_pp ⇒
Monad.Syntax.op_letstar Next_message.(S_MakeVar.pp)
(fun next_message_pp ⇒
Monad.Syntax.op_letstar Parsing_result.(S_MakeVar.pp)
(fun parsing_result_pp ⇒
Monad.Syntax.op_letstar Parser_state.(S_MakeVar.pp)
(fun parser_state_pp ⇒
Monad.Syntax.op_letstar Lexer_state.(S_MakeVar.pp)
(fun lexer_state_pp ⇒
Monad.Syntax.op_letstar
Evaluation_result.(S_MakeVar.pp)
(fun evaluation_result_pp ⇒
Monad.Syntax.op_letstar Vars.(MakeDict_sig.pp)
(fun vars_pp ⇒
Monad.Syntax.op_letstar
Output.(MakeDict_sig.pp)
(fun output_pp ⇒
Monad.Syntax.op_letstar
Stack.(MakeDeque_sig.to_list)
(fun stack_value ⇒
Monad.Syntax.op_letstar
Current_tick.(S_MakeVar.pp)
(fun current_tick_pp ⇒
Monad._return
(fun (fmt :
Format.formatter) ⇒
fun (function_parameter :
unit) ⇒
let '_ :=
function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"<v 0 >"
CamlinternalFormatBasics.End_of_format)
"<v 0 >"))
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"tick : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"vars : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"output :"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"stack : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))))))))))))))))))))))))
"@[<v 0 >@;%a@;%a@;%a@;%a@;%a@;%a@;%a@;tick : %a@;vars : %a@;output :%a@;stack : %a@;@]")
status_pp tt
message_counter_pp tt
next_message_pp tt
parsing_result_pp tt
parser_state_pp tt
lexer_state_pp tt
evaluation_result_pp
tt current_tick_pp tt
vars_pp tt output_pp
tt
(Format.pp_print_list
None
Format.pp_print_int)
stack_value)))))))))))).
End State.
Definition state `{FArgs} : Set := State.state.
Definition initial_state `{FArgs} (empty : State.state) : State.state :=
let m_value :=
State.Monad.Syntax.op_letstar (State.Status.(State.S_MakeVar.set) Halted)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt) in
let '(state_value, _) := State.Monad.run m_value empty in
state_value.
Definition install_boot_sector `{FArgs}
(state_value : State.state) (boot_sector : string) : State.state :=
let m_value :=
State.Monad.Syntax.op_letstar
(State.Boot_sector.(State.S_MakeVar.set) boot_sector)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt) in
let '(state_value, _) := State.Monad.run m_value state_value in
state_value.
Definition state_hash `{FArgs}
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Sc_rollup_repr.State_hash.t :=
let context_hash := Tree.(Context.TREE.hash_value) state_value in
match Sc_rollup_repr.State_hash.context_hash_to_state_hash context_hash with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end.
Definition pp `{FArgs} (state_value : State.state)
: Format.formatter → unit → unit :=
let '(_, pp) := State.Monad.run State.pp state_value in
match pp with
| None ⇒
fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<opaque>"
CamlinternalFormatBasics.End_of_format) "<opaque>")
| Some pp ⇒
let state_hash := state_hash state_value in
fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ": "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))) "@[%a: %a@]")
Sc_rollup_repr.State_hash.pp state_hash pp tt
end.
Definition boot `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.create)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
State.Next_message.(State.S_MakeVar.create)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_metadata)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))).
Definition result_of `{FArgs} {A : Set}
(default : A) (m_value : State.Monad.t A) (state_value : State.state) : A :=
let '(_, v_value) := State.Monad.run m_value state_value in
match v_value with
| None ⇒ default
| Some v_value ⇒ v_value
end.
Definition state_of `{FArgs} {A : Set}
(m_value : State.Monad.t A) (state_value : State.state) : State.state :=
let '(s_value, _) := State.Monad.run m_value state_value in
s_value.
Definition get_tick `{FArgs} : State.state → Sc_rollup_tick_repr.t :=
result_of Sc_rollup_tick_repr.initial
State.Current_tick.(State.S_MakeVar.get).
Definition is_input_state_monadic `{FArgs} : State.Monad.t PS.input_request :=
State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.get)
(fun status ⇒
match status with
| Waiting_for_input_message ⇒
State.Monad.Syntax.op_letstar
State.Current_level.(State.S_MakeVar.get)
(fun level ⇒
State.Monad.Syntax.op_letstar
State.Message_counter.(State.S_MakeVar.get)
(fun counter ⇒
match counter with
| Some n_value ⇒
State.Monad._return
(Sc_rollup_PVM_sig.First_after level n_value)
| None ⇒ State.Monad._return Sc_rollup_PVM_sig.Initial
end))
| Waiting_for_reveal ⇒
State.Monad.Syntax.op_letstar
State.Required_reveal.(State.S_MakeVar.get)
(fun r_value ⇒
match r_value with
| None ⇒
State.Monad.internal_error
"Internal error: Reveal invariant broken"
| Some reveal ⇒
State.Monad._return (Sc_rollup_PVM_sig.Needs_reveal reveal)
end)
| Waiting_for_metadata ⇒
State.Monad._return
(Sc_rollup_PVM_sig.Needs_reveal Sc_rollup_PVM_sig.Reveal_metadata)
| (Halted | Parsing | Evaluating) ⇒
State.Monad._return Sc_rollup_PVM_sig.No_input_required
end).
Definition is_input_state `{FArgs} : State.state → PS.input_request :=
result_of Sc_rollup_PVM_sig.No_input_required is_input_state_monadic.
Definition get_status `{FArgs} : State.state → status :=
result_of Waiting_for_input_message State.Status.(State.S_MakeVar.get).
Definition get_outbox `{FArgs}
(outbox_level : Raw_level_repr.raw_level) (state_value : State.state)
: list PS.output :=
let entries :=
result_of nil State.Output.(State.MakeDict_sig.entries) state_value in
List.filter_map
(fun (function_parameter : string × PS.output) ⇒
let '(_, msg) := function_parameter in
if
Raw_level_repr.op_eq msg.(Sc_rollup_PVM_sig.output.outbox_level)
outbox_level
then
Some msg
else
None) entries.
Definition get_code `{FArgs} : State.state → list instruction :=
result_of nil State.Code.(State.MakeDeque_sig.to_list).
Definition get_parsing_result `{FArgs} : State.state → option bool :=
result_of None State.Parsing_result.(State.S_MakeVar.get).
Definition get_stack `{FArgs} : State.state → list int :=
result_of nil State.Stack.(State.MakeDeque_sig.to_list).
Definition get_var `{FArgs} (state_value : State.state) (k_value : string)
: option int :=
result_of None (State.Vars.(State.MakeDict_sig.get) k_value) state_value.
Definition get_evaluation_result `{FArgs} : State.state → option bool :=
result_of None State.Evaluation_result.(State.S_MakeVar.get).
Definition get_is_stuck `{FArgs} : State.state → option string :=
result_of None State.Monad.is_stuck.
Definition start_parsing `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar (State.Status.(State.S_MakeVar.set) Parsing)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parsing_result.(State.S_MakeVar.set) None)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Lexer_state.(State.S_MakeVar.set) (0, 0))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
State.Code.(State.MakeDeque_sig.clear)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))))).
Definition set_inbox_message_monadic `{FArgs}
(function_parameter : PS.inbox_message) : State.Monad.t unit :=
let '{|
Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload
|} := function_parameter in
State.Monad.Syntax.op_letstar
match Sc_rollup_inbox_message_repr.deserialize payload with
| Pervasives.Error _ ⇒ State.Monad._return None
| Pervasives.Ok (Sc_rollup_inbox_message_repr.External payload) ⇒
State.Monad._return (Some payload)
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
(Sc_rollup_inbox_message_repr.Transfer {|
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.payload :=
payload;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.destination
:= destination
|})) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar State.Metadata.(State.S_MakeVar.get)
(fun function_parameter ⇒
let 'metadata := function_parameter in
match
(metadata,
match metadata with
| Some {| Sc_rollup_metadata_repr.t.address := address |} ⇒
Sc_rollup_repr.Address.op_eq destination address
| _ ⇒ false
end) with
|
(Some {| Sc_rollup_metadata_repr.t.address := address |}, true)
⇒
match Micheline.root_value payload with
| Micheline.Bytes _ payload ⇒
let payload := Bytes.to_string payload in
State.Monad._return (Some payload)
| _ ⇒ State.Monad._return None
end
| (_, _) ⇒ State.Monad._return None
end))
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.Start_of_level) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return None)
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.End_of_level) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return None)
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
(Sc_rollup_inbox_message_repr.Info_per_level _)) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return None)
end
(fun payload ⇒
match payload with
| Some payload ⇒
State.Monad.Syntax.op_letstar State.Boot_sector.(State.S_MakeVar.get)
(fun boot_sector ⇒
let msg := Pervasives.op_caret boot_sector payload in
State.Monad.Syntax.op_letstar
(State.Current_level.(State.S_MakeVar.set) inbox_level)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Message_counter.(State.S_MakeVar.set)
(Some message_counter))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Next_message.(State.S_MakeVar.set) (Some msg))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar start_parsing
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))))
| None ⇒
State.Monad.Syntax.op_letstar
(State.Current_level.(State.S_MakeVar.set) inbox_level)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Message_counter.(State.S_MakeVar.set)
(Some message_counter))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set)
Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))
end).
Definition reveal_monadic `{FArgs} (reveal_data : PS.reveal_data)
: State.Monad.t unit :=
match reveal_data with
| Sc_rollup_PVM_sig.Raw_data data ⇒
State.Monad.Syntax.op_letstar
(State.Next_message.(State.S_MakeVar.set) (Some data))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar start_parsing
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| Sc_rollup_PVM_sig.Metadata metadata ⇒
State.Monad.Syntax.op_letstar
(State.Metadata.(State.S_MakeVar.set) (Some metadata))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| Sc_rollup_PVM_sig.Dal_page None ⇒
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)
| Sc_rollup_PVM_sig.Dal_page (Some data) ⇒
State.Monad.Syntax.op_letstar
(State.Next_message.(State.S_MakeVar.set) (Some (Bytes.to_string data)))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar start_parsing
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
end.
Definition ticked `{FArgs} {A : Set} (m_value : State.Monad.t A)
: State.Monad.t A :=
State.Monad.Syntax.op_letstar State.Current_tick.(State.S_MakeVar.get)
(fun tick ⇒
State.Monad.Syntax.op_letstar
(State.Current_tick.(State.S_MakeVar.set)
(Sc_rollup_tick_repr.next tick))
(fun function_parameter ⇒
let '_ := function_parameter in
m_value)).
Definition set_input_monadic `{FArgs} (input : PS.input)
: State.Monad.t unit :=
match input with
| Sc_rollup_PVM_sig.Inbox_message m_value ⇒
set_inbox_message_monadic m_value
| Sc_rollup_PVM_sig.Reveal s_value ⇒ reveal_monadic s_value
end.
Definition set_input `{FArgs} (input : PS.input)
: State.state → State.state := state_of (ticked (set_input_monadic input)).
Definition next_char `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
(fun function_parameter ⇒
let '(start, len) := function_parameter in
State.Lexer_state.(State.S_MakeVar.set) (start, (len +i 1))).
Definition no_message_to_lex `{FArgs} {A : Set} (function_parameter : unit)
: State.Monad.t A :=
let '_ := function_parameter in
State.Monad.internal_error "lexer: There is no input message to lex".
Definition current_char `{FArgs} : State.Monad.t (option ascii) :=
State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
(fun function_parameter ⇒
let '(start, len) := function_parameter in
State.Monad.Syntax.op_letstar State.Next_message.(State.S_MakeVar.get)
(fun msg ⇒
match msg with
| None ⇒ no_message_to_lex tt
| Some s_value ⇒
if (start +i len) <i (String.length s_value) then
State.Monad._return (Some (String.get s_value (start +i len)))
else
State.Monad._return None
end)).
Definition lexeme `{FArgs} : State.Monad.t string :=
State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
(fun function_parameter ⇒
let '(start, len) := function_parameter in
State.Monad.Syntax.op_letstar State.Next_message.(State.S_MakeVar.get)
(fun msg ⇒
match msg with
| None ⇒ no_message_to_lex tt
| Some s_value ⇒
State.Monad.Syntax.op_letstar
(State.Lexer_state.(State.S_MakeVar.set) ((start +i len), 0))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return (String.sub s_value start len))
end)).
Definition push_int_literal `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar lexeme
(fun s_value ⇒
match Pervasives.int_of_string_opt s_value with
| Some x_value ⇒
State.Code.(State.MakeDeque_sig.inject) (IPush x_value)
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (State.Monad.t unit) false
end).
Definition push_var `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar lexeme
(fun s_value ⇒ State.Code.(State.MakeDeque_sig.inject) (IStore s_value)).
Definition start_evaluating `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Evaluating)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Evaluation_result.(State.S_MakeVar.set) None)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)).
Definition stop_parsing `{FArgs} (outcome : bool) : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Parsing_result.(State.S_MakeVar.set) (Some outcome))
(fun function_parameter ⇒
let '_ := function_parameter in
start_evaluating).
Definition stop_evaluating `{FArgs} (outcome : bool) : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Evaluation_result.(State.S_MakeVar.set) (Some outcome))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Status.(State.S_MakeVar.set) Waiting_for_input_message).
Definition parse `{FArgs} : State.Monad.t unit :=
let produce_add :=
State.Monad.Syntax.op_letstar lexeme
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Code.(State.MakeDeque_sig.inject) IAdd)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))) in
let produce_int :=
State.Monad.Syntax.op_letstar push_int_literal
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)) in
let produce_var :=
State.Monad.Syntax.op_letstar push_var
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)) in
let is_digit (d_value : ascii) : bool :=
(Compare.Char.(Compare.S.op_gteq) d_value "0" % char) &&
(Compare.Char.(Compare.S.op_lteq) d_value "9" % char) in
let is_letter (d_value : ascii) : bool :=
((Compare.Char.(Compare.S.op_gteq) d_value "a" % char) &&
(Compare.Char.(Compare.S.op_lteq) d_value "z" % char)) ||
((Compare.Char.(Compare.S.op_gteq) d_value "A" % char) &&
(Compare.Char.(Compare.S.op_lteq) d_value "Z" % char)) in
let is_identifier_char (d_value : ascii) : bool :=
(is_letter d_value) ||
((is_digit d_value) ||
((Compare.Char.(Compare.S.op_eq) d_value ":" % char) ||
(Compare.Char.(Compare.S.op_eq) d_value "%" % char))) in
State.Monad.Syntax.op_letstar State.Parser_state.(State.S_MakeVar.get)
(fun parser_state ⇒
match parser_state with
| State.ParseInt ⇒
State.Monad.Syntax.op_letstar current_char
(fun char_value ⇒
match
(char_value,
match char_value with
| Some d_value ⇒ is_digit d_value
| _ ⇒ false
end) with
| (Some d_value, true) ⇒ next_char
| (Some "+" % char, _) ⇒
State.Monad.Syntax.op_letstar produce_int
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar produce_add
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (Some (" " % char | "010" % char), _) ⇒
State.Monad.Syntax.op_letstar produce_int
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (None, _) ⇒
State.Monad.Syntax.op_letstar push_int_literal
(fun function_parameter ⇒
let '_ := function_parameter in
stop_parsing true)
| (_, _) ⇒ stop_parsing false
end)
| State.ParseVar ⇒
State.Monad.Syntax.op_letstar current_char
(fun char_value ⇒
match
(char_value,
match char_value with
| Some d_value ⇒ is_identifier_char d_value
| _ ⇒ false
end) with
| (Some d_value, true) ⇒ next_char
| (Some "+" % char, _) ⇒
State.Monad.Syntax.op_letstar produce_var
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar produce_add
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (Some (" " % char | "010" % char), _) ⇒
State.Monad.Syntax.op_letstar produce_var
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (None, _) ⇒
State.Monad.Syntax.op_letstar push_var
(fun function_parameter ⇒
let '_ := function_parameter in
stop_parsing true)
| (_, _) ⇒ stop_parsing false
end)
| State.SkipLayout ⇒
State.Monad.Syntax.op_letstar current_char
(fun char_value ⇒
match
(char_value,
match char_value with
| Some d_value ⇒ is_digit d_value
| _ ⇒ false
end,
match char_value with
| Some d_value ⇒ is_letter d_value
| _ ⇒ false
end) with
| (Some (" " % char | "010" % char), _, _) ⇒ next_char
| (Some "+" % char, _, _) ⇒ produce_add
| (Some d_value, true, _) ⇒
State.Monad.Syntax.op_letstar lexeme
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set)
State.ParseInt)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))
| (Some d_value, _, true) ⇒
State.Monad.Syntax.op_letstar lexeme
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set)
State.ParseVar)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))
| (None, _, _) ⇒ stop_parsing true
| (_, _, _) ⇒ stop_parsing false
end)
end).
Definition output `{FArgs}
(function_parameter : Contract_hash.t × Entrypoint_repr.t)
: int → State.Monad.t unit :=
let '(destination, entrypoint) := function_parameter in
fun (v_value : int) ⇒
State.Monad.Syntax.op_letstar State.Output_counter.(State.S_MakeVar.get)
(fun counter ⇒
State.Monad.Syntax.op_letstar
(State.Output_counter.(State.S_MakeVar.set) (Z.succ counter))
(fun function_parameter ⇒
let '_ := function_parameter in
let unparsed_parameters :=
Micheline.strip_locations (Micheline.Int tt (Z.of_int v_value))
in
let transaction :=
{|
Sc_rollup_outbox_message_repr.transaction.unparsed_parameters
:= unparsed_parameters;
Sc_rollup_outbox_message_repr.transaction.destination :=
destination;
Sc_rollup_outbox_message_repr.transaction.entrypoint :=
entrypoint; |} in
let message :=
Sc_rollup_outbox_message_repr.Atomic_transaction_batch
{|
Sc_rollup_outbox_message_repr.t.Atomic_transaction_batch.transactions
:= [ transaction ]; |} in
State.Monad.Syntax.op_letstar
State.Current_level.(State.S_MakeVar.get)
(fun outbox_level ⇒
let output :=
{| Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
Sc_rollup_PVM_sig.output.message_index := counter;
Sc_rollup_PVM_sig.output.message := message; |} in
State.Output.(State.MakeDict_sig.set) (Z.to_string counter)
output))).
Definition identifies_target_contract `{FArgs} (x_value : string)
: option (Contract_hash.t × Entrypoint_repr.t) :=
match String.split_on_char "%" % char x_value with
| cons destination entrypoint ⇒
match Contract_hash.of_b58check_opt destination with
| None ⇒
if Compare.String.(Compare.S.op_eq) x_value "out" then
return× (Contract_hash.zero, Entrypoint_repr.default)
else
Error_monad.Option_syntax.fail
| Some destination ⇒
let× entrypoint :=
match entrypoint with
| [] ⇒ return× Entrypoint_repr.default
| _ ⇒
let× entrypoint :=
Non_empty_string.of_string (String.concat "" entrypoint) in
let× entrypoint := Entrypoint_repr.of_annot_lax_opt entrypoint in
return× entrypoint
end in
return× (destination, entrypoint)
end
| [] ⇒ Error_monad.Option_syntax.fail
end.
Definition evaluate_preimage_request `{FArgs} (hash_value : string)
: State.Monad.t unit :=
match PS.Reveal_hash.of_b58check_opt hash_value with
| None ⇒ stop_evaluating false
| Some hash_value ⇒
State.Monad.Syntax.op_letstar
(State.Required_reveal.(State.S_MakeVar.set)
(Some (Sc_rollup_PVM_sig.Reveal_raw_data hash_value)))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_reveal)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
end.
Definition evaluate_dal_page_request `{FArgs}
: string → State.Monad.t unit :=
let attestation_lag := 1 in
let page_size := 4096 /i 64 in
let slot_size := (Pervasives.lsl 1 20) /i 64 in
let number_of_slots := 256 /i 64 in
let number_of_pages := slot_size /i page_size in
let mk_slot_index (slot_str : string) : option Dal_slot_repr.Index.t :=
let× index_value := Option.map Int32.to_int (Int32.of_string_opt slot_str)
in
if (index_value <i 0) || (index_value ≥i number_of_slots) then
None
else
Dal_slot_repr.Index.of_int index_value in
let mk_page_index (page_str : string) : option int :=
let× index_value := Option.map Int32.to_int (Int32.of_string_opt page_str)
in
if (index_value <i 0) || (index_value ≥i number_of_pages) then
None
else
Some index_value in
fun (raw_page_id : string) ⇒
let mk_page_id (current_lvl : Raw_level_repr.raw_level)
: option Dal_slot_repr.Page.t :=
match String.split_on_char ":" % char raw_page_id with
| cons lvl (cons slot (cons page [])) ⇒
let× lvl := Int32.of_string_opt lvl in
let× lvl := Bounded.Non_negative_int32.(Bounded.S.of_value) lvl in
let published_level :=
match Raw_level_repr.of_int32_non_negative lvl with
| Pervasives.Ok published_level ⇒ published_level
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Raw_level_repr.raw_level false
end in
let delta := Raw_level_repr.diff_value current_lvl published_level in
if (delta >i32 1) && (delta ≤i32 (2 ×i32 attestation_lag)) then
let× index_value := mk_slot_index slot in
let× page_index := mk_page_index page in
let slot_id :=
{| Dal_slot_repr.Header.id.published_level := published_level;
Dal_slot_repr.Header.id.index := index_value; |} in
Some
{| Dal_slot_repr.Page.t.slot_id := slot_id;
Dal_slot_repr.Page.t.page_index := page_index; |}
else
None
| _ ⇒ None
end in
State.Monad.Syntax.op_letstar State.Current_level.(State.S_MakeVar.get)
(fun current_lvl ⇒
match mk_page_id current_lvl with
| Some page_id ⇒
State.Monad.Syntax.op_letstar
(State.Required_reveal.(State.S_MakeVar.set)
(Some (Sc_rollup_PVM_sig.Request_dal_page page_id)))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_reveal)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| None ⇒ stop_evaluating false
end).
Definition remove_prefix `{FArgs}
(prefix : String.t) (input : string) (input_len : int) : option string :=
let prefix_len := String.length prefix in
if
(input_len >i prefix_len) &&
(String.equal (String.sub input 0 prefix_len) prefix)
then
Some (String.sub input prefix_len (input_len -i prefix_len))
else
None.
Definition evaluate `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Code.(State.MakeDeque_sig.pop)
(fun i_value ⇒
match i_value with
| None ⇒ stop_evaluating true
| Some (IPush x_value) ⇒ State.Stack.(State.MakeDeque_sig.push) x_value
| Some (IStore x_value) ⇒
let len := String.length x_value in
match remove_prefix "hash:" x_value len with
| Some hash_value ⇒ evaluate_preimage_request hash_value
| None ⇒
match remove_prefix "dal:" x_value len with
| Some pid ⇒ evaluate_dal_page_request pid
| None ⇒
State.Monad.Syntax.op_letstar
State.Stack.(State.MakeDeque_sig.top)
(fun v_value ⇒
match v_value with
| None ⇒ stop_evaluating false
| Some v_value ⇒
match identifies_target_contract x_value with
| Some contract_entrypoint ⇒
output contract_entrypoint v_value
| None ⇒
State.Vars.(State.MakeDict_sig.set) x_value v_value
end
end)
end
end
| Some IAdd ⇒
State.Monad.Syntax.op_letstar State.Stack.(State.MakeDeque_sig.pop)
(fun v_value ⇒
match v_value with
| None ⇒ stop_evaluating false
| Some x_value ⇒
State.Monad.Syntax.op_letstar
State.Stack.(State.MakeDeque_sig.pop)
(fun v_value ⇒
match v_value with
| None ⇒ stop_evaluating false
| Some y_value ⇒
State.Stack.(State.MakeDeque_sig.push)
(x_value +i y_value)
end)
end)
end).
Definition reboot `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar State.Stack.(State.MakeDeque_sig.clear)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar State.Code.(State.MakeDeque_sig.clear)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))).
Definition eval_step `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Monad.is_stuck
(fun x_value ⇒
match x_value with
| Some _ ⇒ reboot
| None ⇒
State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.get)
(fun status ⇒
match status with
| Halted ⇒ boot
|
(Waiting_for_input_message | Waiting_for_reveal |
Waiting_for_metadata) ⇒
State.Monad.Syntax.op_letstar
State.Next_message.(State.S_MakeVar.get)
(fun msg ⇒
match msg with
| None ⇒
State.Monad.internal_error
"An input state was not provided an input."
| Some _ ⇒ start_parsing
end)
| Parsing ⇒ parse
| Evaluating ⇒ evaluate
end)
end).
Definition eval `{FArgs} (state_value : State.state) : State.state :=
state_of (ticked eval_step) state_value.
Axiom step_transition : ∀ `{FArgs},
option PS.input → State.state → State.state × PS.input_request.
Definition verify_proof `{FArgs}
(input_given : option PS.input) (proof_value : Context.(P.proof))
: M? PS.input_request :=
let result_value :=
Context.(P.verify_proof) proof_value (step_transition input_given) in
match result_value with
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Arith_proof_verification_failed" unit tt)
| Some (_state, request) ⇒ return? request
end.
Definition produce_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(input_given : option PS.input)
(state_value : Context.(P.Tree).(Context.TREE.tree)) : M? proof :=
let result_value :=
Context.(P.produce_proof) context_value state_value
(step_transition input_given) in
match result_value with
| Some (tree_proof, _requested) ⇒ return? tree_proof
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Arith_proof_production_failed" unit tt)
end.
Definition verify_origination_proof `{FArgs}
(proof_value : proof) (boot_sector : string) : bool :=
let before := Context.(P.proof_before) proof_value in
if
Sc_rollup_repr.State_hash.op_ltgt before reference_initial_state_hash
then
false
else
let result_value :=
Context.(P.verify_proof) proof_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| None ⇒ false
| Some (_, _) ⇒ true
end.
Definition produce_origination_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t)) (boot_sector : string)
: M? proof :=
let state_value := initial_state (Tree.(Context.TREE.empty) context_value)
in
let result_value :=
Context.(P.produce_proof) context_value state_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| Some (proof_value, _) ⇒ return? proof_value
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Arith_proof_production_failed" unit tt)
end.
Module output_proof.
Record record `{FArgs} : Set := Build {
output_proof : Context.(P.proof);
output_proof_state : hash;
output_proof_output : PS.output;
}.
Definition with_output_proof `{FArgs} output_proof (r : record) :=
Build _ _ _ _ output_proof r.(output_proof_state) r.(output_proof_output).
Definition with_output_proof_state `{FArgs} output_proof_state
(r : record) :=
Build _ _ _ _ r.(output_proof) output_proof_state r.(output_proof_output).
Definition with_output_proof_output `{FArgs} output_proof_output
(r : record) :=
Build _ _ _ _ r.(output_proof) r.(output_proof_state) output_proof_output.
End output_proof.
Definition output_proof `{FArgs} := output_proof.record.
Definition output_proof_encoding `{FArgs}
: Data_encoding.encoding output_proof :=
Data_encoding.conv
(fun (function_parameter : output_proof) ⇒
let '{|
output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output
|} := function_parameter in
(output_proof, output_proof_state, output_proof_output))
(fun (function_parameter : Context.(P.proof) × hash × PS.output) ⇒
let '(output_proof, output_proof_state, output_proof_output) :=
function_parameter in
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "output_proof" Context.(P.proof_encoding))
(Data_encoding.req None None "output_proof_state"
Sc_rollup_repr.State_hash.encoding)
(Data_encoding.req None None "output_proof_output" PS.output_encoding)).
Definition output_of_output_proof `{FArgs} (s_value : output_proof)
: PS.output := s_value.(output_proof.output_proof_output).
Definition state_of_output_proof `{FArgs} (s_value : output_proof) : hash :=
s_value.(output_proof.output_proof_state).
Definition output_key `{FArgs} (output : PS.output) : string :=
Z.to_string output.(Sc_rollup_PVM_sig.output.message_index).
Definition has_output `{FArgs} (output : PS.output) (tree_value : State.state)
: State.state × bool :=
let equal :=
State.Output.(State.MakeDict_sig.mapped_to) (output_key output) output
tree_value in
(tree_value, equal).
Definition verify_output_proof `{FArgs} (p_value : output_proof) : bool :=
let transition := has_output p_value.(output_proof.output_proof_output) in
let result_value :=
Context.(P.verify_proof) p_value.(output_proof.output_proof) transition in
match result_value with
| None ⇒ false
| Some _ ⇒ true
end.
Definition produce_output_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(state_value : Context.(P.Tree).(Context.TREE.tree))
(output_proof_output : PS.output)
: Pervasives.result output_proof Error_monad._error :=
let output_proof_state := state_hash state_value in
let result_value :=
Context.(P.produce_proof) context_value state_value
(has_output output_proof_output) in
match result_value with
| Some (output_proof, true) ⇒
return?
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}
| Some (_, false) ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "Arith_invalid_claim_about_outbox" unit tt)
| None ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "Arith_output_proof_production_failed" unit tt)
end.
(* Make *)
Definition functor `{FArgs} :=
{|
S.pp := pp;
S.proof_encoding := proof_encoding;
S.proof_start_state := proof_start_state;
S.proof_stop_state := proof_stop_state;
S.state_hash := state_hash;
S.initial_state := initial_state;
S.install_boot_sector := install_boot_sector;
S.is_input_state := is_input_state;
S.set_input := set_input;
S.eval := eval;
S.verify_proof := verify_proof;
S.produce_proof := produce_proof;
S.verify_origination_proof := verify_origination_proof;
S.produce_origination_proof := produce_origination_proof;
S.output_proof_encoding := output_proof_encoding;
S.output_of_output_proof := output_of_output_proof;
S.state_of_output_proof := state_of_output_proof;
S.verify_output_proof := verify_output_proof;
S.produce_output_proof := produce_output_proof;
S.name := name;
S.parse_boot_sector := parse_boot_sector;
S.pp_boot_sector := pp_boot_sector;
S.get_tick := get_tick;
S.get_status := get_status;
S.get_outbox := get_outbox;
S.equal_instruction := equal_instruction;
S.pp_instruction := pp_instruction;
S.get_parsing_result := get_parsing_result;
S.get_code := get_code;
S.get_stack := get_stack;
S.get_var := get_var;
S.get_evaluation_result := get_evaluation_result;
S.get_is_stuck := get_is_stuck
|}.
End Make.
Definition Make {Context_Tree_t Context_Tree_tree Context_proof : Set}
(Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof))
: S (state := Context.(P.Tree).(Context.TREE.tree))
(context := Context.(P.Tree).(Context.TREE.t)) (proof := Context.(P.proof))
(output_proof := _) (status := _) (instruction := _) :=
let '_ := Make.Build_FArgs Context in
Make.functor.
Definition Protocol_implementation :=
Make
(let Tree :=
let mem := Context.Tree.(Context.TREE.mem) in
let mem_tree := Context.Tree.(Context.TREE.mem_tree) in
let find := Context.Tree.(Context.TREE.find) in
let find_tree := Context.Tree.(Context.TREE.find_tree) in
let list_value := Context.Tree.(Context.TREE.list_value) in
let length := Context.Tree.(Context.TREE.length) in
let add := Context.Tree.(Context.TREE.add) in
let add_tree := Context.Tree.(Context.TREE.add_tree) in
let remove := Context.Tree.(Context.TREE.remove) in
let fold {a : Set} := Context.Tree.(Context.TREE.fold) in
let config_value := Context.Tree.(Context.TREE.config_value) in
let empty := Context.Tree.(Context.TREE.empty) in
let is_empty := Context.Tree.(Context.TREE.is_empty) in
let kind_value := Context.Tree.(Context.TREE.kind_value) in
let to_value := Context.Tree.(Context.TREE.to_value) in
let of_value := Context.Tree.(Context.TREE.of_value) in
let hash_value := Context.Tree.(Context.TREE.hash_value) in
let equal := Context.Tree.(Context.TREE.equal) in
let clear := Context.Tree.(Context.TREE.clear) in
let tree : Set := Context.tree in
let t : Set := Context.t in
let key : Set := list string in
let value : Set := bytes in
{|
Context.TREE.mem := mem;
Context.TREE.mem_tree := mem_tree;
Context.TREE.find := find;
Context.TREE.find_tree := find_tree;
Context.TREE.list_value := list_value;
Context.TREE.length := length;
Context.TREE.add := add;
Context.TREE.add_tree := add_tree;
Context.TREE.remove := remove;
Context.TREE.fold _ := fold;
Context.TREE.config_value := config_value;
Context.TREE.empty := empty;
Context.TREE.is_empty := is_empty;
Context.TREE.kind_value := kind_value;
Context.TREE.to_value := to_value;
Context.TREE.of_value := of_value;
Context.TREE.hash_value := hash_value;
Context.TREE.equal := equal;
Context.TREE.clear := clear
|} in
let tree : Set := Context.tree in
let hash_tree (t_value : Context.tree) : Sc_rollup_repr.State_hash.t :=
match
Sc_rollup_repr.State_hash.context_hash_to_state_hash
(Tree.(Context.TREE.hash_value) t_value) with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof : Set := Context.Proof.t Context.Proof.tree in
let verify_proof {A : Set}
(p_value : Context.Proof.t Context.Proof.tree)
(f_value : Context.tree → Context.tree × A)
: option (Context.tree × A) :=
id Result.to_option (Context.verify_tree_proof p_value f_value) in
let produce_proof {A B C D : Set} (_context : A) (_state : B) (_f : C)
: option D :=
None in
let kinded_hash_to_state_hash (function_parameter : Context.Proof.kinded_hash)
: M? Sc_rollup_repr.State_hash.t :=
match function_parameter with
| (Context.Proof.KValue hash_value | Context.Proof.KNode hash_value) ⇒
Sc_rollup_repr.State_hash.context_hash_to_state_hash hash_value
end in
let proof_before {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.before) with
| Pervasives.Ok prf ⇒ prf
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_after {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.after) with
| Pervasives.Ok prf ⇒ prf
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_encoding :=
Context.Proof_encoding.V2.Tree32.(Context.PROOF_ENCODING.tree_proof_encoding)
in
{|
P.Tree := Tree;
P.hash_tree := hash_tree;
P.proof_encoding := proof_encoding;
P.proof_before := proof_before;
P.proof_after := proof_after;
P.verify_proof _ := verify_proof;
P.produce_proof _ := produce_proof
|}).
Make_var
(let t : Set := Z.t in
let initial := Z.zero in
let encoding := Data_encoding.n_value in
let name := "internal_message_counter" in
let pp (fmt : Format.formatter) (c_value : Z.t) : unit :=
Z.pp_print fmt c_value in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition incr_internal_message_counter `{FArgs} : Monad.t unit :=
Monad.Syntax.op_letstar Internal_message_counter.(S_MakeVar.get)
(fun current_counter ⇒
Internal_message_counter.(S_MakeVar.set) (Z.succ current_counter)).
Definition Next_message `{FArgs} :=
Make_var
(let t : Set := option string in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.string_value in
let name := "next_message" in
let pp (fmt : Format.formatter) (function_parameter : option string)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "None"
CamlinternalFormatBasics.End_of_format) "None")
| Some s_value ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Some "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format)) "Some %s") s_value
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Inductive parser_state `{FArgs} : Set :=
| ParseInt : parser_state
| ParseVar : parser_state
| SkipLayout : parser_state.
Definition Lexer_state `{FArgs} :=
Make_var
(let t : Set := int × int in
let name := "lexer_buffer" in
let initial := ((-1), (-1)) in
let encoding :=
Data_encoding.tup2 Data_encoding.int31 Data_encoding.int31 in
let pp (fmt : Format.formatter) (function_parameter : int × int)
: unit :=
let '(start, len) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "lexer.(start = "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", len = "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"lexer.(start = %d, len = %d)") start len in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Parser_state `{FArgs} :=
Make_var
(let t : Set := parser_state in
let name := "parser_state" in
let initial := SkipLayout in
let encoding :=
Data_encoding.string_enum
[
("ParseInt", ParseInt);
("ParseVar", ParseVar);
("SkipLayout", SkipLayout)
] in
let pp (fmt : Format.formatter) (function_parameter : parser_state)
: unit :=
match function_parameter with
| ParseInt ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Parsing int"
CamlinternalFormatBasics.End_of_format) "Parsing int")
| ParseVar ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Parsing var"
CamlinternalFormatBasics.End_of_format) "Parsing var")
| SkipLayout ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Skipping layout"
CamlinternalFormatBasics.End_of_format) "Skipping layout")
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Parsing_result `{FArgs} :=
Make_var
(let t : Set := option bool in
let name := "parsing_result" in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.bool_value in
let pp (fmt : Format.formatter) (function_parameter : option bool)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "n/a"
CamlinternalFormatBasics.End_of_format) "n/a")
| Some true ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "parsing succeeds"
CamlinternalFormatBasics.End_of_format) "parsing succeeds")
| Some false ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "parsing fails"
CamlinternalFormatBasics.End_of_format) "parsing fails")
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Evaluation_result `{FArgs} :=
Make_var
(let t : Set := option bool in
let name := "evaluation_result" in
let initial {A : Set} : option A :=
None in
let encoding := Data_encoding.option_value Data_encoding.bool_value in
let pp (fmt : Format.formatter) (function_parameter : option bool)
: unit :=
match function_parameter with
| None ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "n/a"
CamlinternalFormatBasics.End_of_format) "n/a")
| Some true ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "evaluation succeeds"
CamlinternalFormatBasics.End_of_format) "evaluation succeeds")
| Some false ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "evaluation fails"
CamlinternalFormatBasics.End_of_format) "evaluation fails")
end in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Output_counter `{FArgs} :=
Make_var
(let t : Set := Z.t in
let initial := Z.zero in
let name := "output_counter" in
let encoding := Data_encoding.n_value in
let pp := Z.pp_print in
{|
P_MakeVar.name := name;
P_MakeVar.initial := initial;
P_MakeVar.pp := pp;
P_MakeVar.encoding := encoding
|}).
Definition Output `{FArgs} :=
Make_dict
(let t : Set := Sc_rollup_PVM_sig.output in
let name := "output" in
let encoding := Sc_rollup_PVM_sig.output_encoding in
let pp := Sc_rollup_PVM_sig.pp_output in
{|
P_MakeDict.name := name;
P_MakeDict.pp := pp;
P_MakeDict.encoding := encoding
|}).
Definition pp `{FArgs} : Monad.t (Format.formatter → unit → unit) :=
Monad.Syntax.op_letstar Status.(S_MakeVar.pp)
(fun status_pp ⇒
Monad.Syntax.op_letstar Message_counter.(S_MakeVar.pp)
(fun message_counter_pp ⇒
Monad.Syntax.op_letstar Next_message.(S_MakeVar.pp)
(fun next_message_pp ⇒
Monad.Syntax.op_letstar Parsing_result.(S_MakeVar.pp)
(fun parsing_result_pp ⇒
Monad.Syntax.op_letstar Parser_state.(S_MakeVar.pp)
(fun parser_state_pp ⇒
Monad.Syntax.op_letstar Lexer_state.(S_MakeVar.pp)
(fun lexer_state_pp ⇒
Monad.Syntax.op_letstar
Evaluation_result.(S_MakeVar.pp)
(fun evaluation_result_pp ⇒
Monad.Syntax.op_letstar Vars.(MakeDict_sig.pp)
(fun vars_pp ⇒
Monad.Syntax.op_letstar
Output.(MakeDict_sig.pp)
(fun output_pp ⇒
Monad.Syntax.op_letstar
Stack.(MakeDeque_sig.to_list)
(fun stack_value ⇒
Monad.Syntax.op_letstar
Current_tick.(S_MakeVar.pp)
(fun current_tick_pp ⇒
Monad._return
(fun (fmt :
Format.formatter) ⇒
fun (function_parameter :
unit) ⇒
let '_ :=
function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"<v 0 >"
CamlinternalFormatBasics.End_of_format)
"<v 0 >"))
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"tick : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"vars : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"output :"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.String_literal
"stack : "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;"
1
0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))))))))))))))))))))))))
"@[<v 0 >@;%a@;%a@;%a@;%a@;%a@;%a@;%a@;tick : %a@;vars : %a@;output :%a@;stack : %a@;@]")
status_pp tt
message_counter_pp tt
next_message_pp tt
parsing_result_pp tt
parser_state_pp tt
lexer_state_pp tt
evaluation_result_pp
tt current_tick_pp tt
vars_pp tt output_pp
tt
(Format.pp_print_list
None
Format.pp_print_int)
stack_value)))))))))))).
End State.
Definition state `{FArgs} : Set := State.state.
Definition initial_state `{FArgs} (empty : State.state) : State.state :=
let m_value :=
State.Monad.Syntax.op_letstar (State.Status.(State.S_MakeVar.set) Halted)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt) in
let '(state_value, _) := State.Monad.run m_value empty in
state_value.
Definition install_boot_sector `{FArgs}
(state_value : State.state) (boot_sector : string) : State.state :=
let m_value :=
State.Monad.Syntax.op_letstar
(State.Boot_sector.(State.S_MakeVar.set) boot_sector)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt) in
let '(state_value, _) := State.Monad.run m_value state_value in
state_value.
Definition state_hash `{FArgs}
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Sc_rollup_repr.State_hash.t :=
let context_hash := Tree.(Context.TREE.hash_value) state_value in
match Sc_rollup_repr.State_hash.context_hash_to_state_hash context_hash with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end.
Definition pp `{FArgs} (state_value : State.state)
: Format.formatter → unit → unit :=
let '(_, pp) := State.Monad.run State.pp state_value in
match pp with
| None ⇒
fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<opaque>"
CamlinternalFormatBasics.End_of_format) "<opaque>")
| Some pp ⇒
let state_hash := state_hash state_value in
fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ": "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))) "@[%a: %a@]")
Sc_rollup_repr.State_hash.pp state_hash pp tt
end.
Definition boot `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.create)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
State.Next_message.(State.S_MakeVar.create)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_metadata)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))).
Definition result_of `{FArgs} {A : Set}
(default : A) (m_value : State.Monad.t A) (state_value : State.state) : A :=
let '(_, v_value) := State.Monad.run m_value state_value in
match v_value with
| None ⇒ default
| Some v_value ⇒ v_value
end.
Definition state_of `{FArgs} {A : Set}
(m_value : State.Monad.t A) (state_value : State.state) : State.state :=
let '(s_value, _) := State.Monad.run m_value state_value in
s_value.
Definition get_tick `{FArgs} : State.state → Sc_rollup_tick_repr.t :=
result_of Sc_rollup_tick_repr.initial
State.Current_tick.(State.S_MakeVar.get).
Definition is_input_state_monadic `{FArgs} : State.Monad.t PS.input_request :=
State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.get)
(fun status ⇒
match status with
| Waiting_for_input_message ⇒
State.Monad.Syntax.op_letstar
State.Current_level.(State.S_MakeVar.get)
(fun level ⇒
State.Monad.Syntax.op_letstar
State.Message_counter.(State.S_MakeVar.get)
(fun counter ⇒
match counter with
| Some n_value ⇒
State.Monad._return
(Sc_rollup_PVM_sig.First_after level n_value)
| None ⇒ State.Monad._return Sc_rollup_PVM_sig.Initial
end))
| Waiting_for_reveal ⇒
State.Monad.Syntax.op_letstar
State.Required_reveal.(State.S_MakeVar.get)
(fun r_value ⇒
match r_value with
| None ⇒
State.Monad.internal_error
"Internal error: Reveal invariant broken"
| Some reveal ⇒
State.Monad._return (Sc_rollup_PVM_sig.Needs_reveal reveal)
end)
| Waiting_for_metadata ⇒
State.Monad._return
(Sc_rollup_PVM_sig.Needs_reveal Sc_rollup_PVM_sig.Reveal_metadata)
| (Halted | Parsing | Evaluating) ⇒
State.Monad._return Sc_rollup_PVM_sig.No_input_required
end).
Definition is_input_state `{FArgs} : State.state → PS.input_request :=
result_of Sc_rollup_PVM_sig.No_input_required is_input_state_monadic.
Definition get_status `{FArgs} : State.state → status :=
result_of Waiting_for_input_message State.Status.(State.S_MakeVar.get).
Definition get_outbox `{FArgs}
(outbox_level : Raw_level_repr.raw_level) (state_value : State.state)
: list PS.output :=
let entries :=
result_of nil State.Output.(State.MakeDict_sig.entries) state_value in
List.filter_map
(fun (function_parameter : string × PS.output) ⇒
let '(_, msg) := function_parameter in
if
Raw_level_repr.op_eq msg.(Sc_rollup_PVM_sig.output.outbox_level)
outbox_level
then
Some msg
else
None) entries.
Definition get_code `{FArgs} : State.state → list instruction :=
result_of nil State.Code.(State.MakeDeque_sig.to_list).
Definition get_parsing_result `{FArgs} : State.state → option bool :=
result_of None State.Parsing_result.(State.S_MakeVar.get).
Definition get_stack `{FArgs} : State.state → list int :=
result_of nil State.Stack.(State.MakeDeque_sig.to_list).
Definition get_var `{FArgs} (state_value : State.state) (k_value : string)
: option int :=
result_of None (State.Vars.(State.MakeDict_sig.get) k_value) state_value.
Definition get_evaluation_result `{FArgs} : State.state → option bool :=
result_of None State.Evaluation_result.(State.S_MakeVar.get).
Definition get_is_stuck `{FArgs} : State.state → option string :=
result_of None State.Monad.is_stuck.
Definition start_parsing `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar (State.Status.(State.S_MakeVar.set) Parsing)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parsing_result.(State.S_MakeVar.set) None)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Lexer_state.(State.S_MakeVar.set) (0, 0))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
State.Code.(State.MakeDeque_sig.clear)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))))).
Definition set_inbox_message_monadic `{FArgs}
(function_parameter : PS.inbox_message) : State.Monad.t unit :=
let '{|
Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload
|} := function_parameter in
State.Monad.Syntax.op_letstar
match Sc_rollup_inbox_message_repr.deserialize payload with
| Pervasives.Error _ ⇒ State.Monad._return None
| Pervasives.Ok (Sc_rollup_inbox_message_repr.External payload) ⇒
State.Monad._return (Some payload)
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
(Sc_rollup_inbox_message_repr.Transfer {|
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.payload :=
payload;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.destination
:= destination
|})) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar State.Metadata.(State.S_MakeVar.get)
(fun function_parameter ⇒
let 'metadata := function_parameter in
match
(metadata,
match metadata with
| Some {| Sc_rollup_metadata_repr.t.address := address |} ⇒
Sc_rollup_repr.Address.op_eq destination address
| _ ⇒ false
end) with
|
(Some {| Sc_rollup_metadata_repr.t.address := address |}, true)
⇒
match Micheline.root_value payload with
| Micheline.Bytes _ payload ⇒
let payload := Bytes.to_string payload in
State.Monad._return (Some payload)
| _ ⇒ State.Monad._return None
end
| (_, _) ⇒ State.Monad._return None
end))
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.Start_of_level) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return None)
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.End_of_level) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return None)
|
Pervasives.Ok
(Sc_rollup_inbox_message_repr.Internal
(Sc_rollup_inbox_message_repr.Info_per_level _)) ⇒
State.Monad.Syntax.op_letstar State.incr_internal_message_counter
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return None)
end
(fun payload ⇒
match payload with
| Some payload ⇒
State.Monad.Syntax.op_letstar State.Boot_sector.(State.S_MakeVar.get)
(fun boot_sector ⇒
let msg := Pervasives.op_caret boot_sector payload in
State.Monad.Syntax.op_letstar
(State.Current_level.(State.S_MakeVar.set) inbox_level)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Message_counter.(State.S_MakeVar.set)
(Some message_counter))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Next_message.(State.S_MakeVar.set) (Some msg))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar start_parsing
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))))
| None ⇒
State.Monad.Syntax.op_letstar
(State.Current_level.(State.S_MakeVar.set) inbox_level)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Message_counter.(State.S_MakeVar.set)
(Some message_counter))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set)
Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))
end).
Definition reveal_monadic `{FArgs} (reveal_data : PS.reveal_data)
: State.Monad.t unit :=
match reveal_data with
| Sc_rollup_PVM_sig.Raw_data data ⇒
State.Monad.Syntax.op_letstar
(State.Next_message.(State.S_MakeVar.set) (Some data))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar start_parsing
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| Sc_rollup_PVM_sig.Metadata metadata ⇒
State.Monad.Syntax.op_letstar
(State.Metadata.(State.S_MakeVar.set) (Some metadata))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| Sc_rollup_PVM_sig.Dal_page None ⇒
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)
| Sc_rollup_PVM_sig.Dal_page (Some data) ⇒
State.Monad.Syntax.op_letstar
(State.Next_message.(State.S_MakeVar.set) (Some (Bytes.to_string data)))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar start_parsing
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
end.
Definition ticked `{FArgs} {A : Set} (m_value : State.Monad.t A)
: State.Monad.t A :=
State.Monad.Syntax.op_letstar State.Current_tick.(State.S_MakeVar.get)
(fun tick ⇒
State.Monad.Syntax.op_letstar
(State.Current_tick.(State.S_MakeVar.set)
(Sc_rollup_tick_repr.next tick))
(fun function_parameter ⇒
let '_ := function_parameter in
m_value)).
Definition set_input_monadic `{FArgs} (input : PS.input)
: State.Monad.t unit :=
match input with
| Sc_rollup_PVM_sig.Inbox_message m_value ⇒
set_inbox_message_monadic m_value
| Sc_rollup_PVM_sig.Reveal s_value ⇒ reveal_monadic s_value
end.
Definition set_input `{FArgs} (input : PS.input)
: State.state → State.state := state_of (ticked (set_input_monadic input)).
Definition next_char `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
(fun function_parameter ⇒
let '(start, len) := function_parameter in
State.Lexer_state.(State.S_MakeVar.set) (start, (len +i 1))).
Definition no_message_to_lex `{FArgs} {A : Set} (function_parameter : unit)
: State.Monad.t A :=
let '_ := function_parameter in
State.Monad.internal_error "lexer: There is no input message to lex".
Definition current_char `{FArgs} : State.Monad.t (option ascii) :=
State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
(fun function_parameter ⇒
let '(start, len) := function_parameter in
State.Monad.Syntax.op_letstar State.Next_message.(State.S_MakeVar.get)
(fun msg ⇒
match msg with
| None ⇒ no_message_to_lex tt
| Some s_value ⇒
if (start +i len) <i (String.length s_value) then
State.Monad._return (Some (String.get s_value (start +i len)))
else
State.Monad._return None
end)).
Definition lexeme `{FArgs} : State.Monad.t string :=
State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
(fun function_parameter ⇒
let '(start, len) := function_parameter in
State.Monad.Syntax.op_letstar State.Next_message.(State.S_MakeVar.get)
(fun msg ⇒
match msg with
| None ⇒ no_message_to_lex tt
| Some s_value ⇒
State.Monad.Syntax.op_letstar
(State.Lexer_state.(State.S_MakeVar.set) ((start +i len), 0))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return (String.sub s_value start len))
end)).
Definition push_int_literal `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar lexeme
(fun s_value ⇒
match Pervasives.int_of_string_opt s_value with
| Some x_value ⇒
State.Code.(State.MakeDeque_sig.inject) (IPush x_value)
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (State.Monad.t unit) false
end).
Definition push_var `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar lexeme
(fun s_value ⇒ State.Code.(State.MakeDeque_sig.inject) (IStore s_value)).
Definition start_evaluating `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Evaluating)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Evaluation_result.(State.S_MakeVar.set) None)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)).
Definition stop_parsing `{FArgs} (outcome : bool) : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Parsing_result.(State.S_MakeVar.set) (Some outcome))
(fun function_parameter ⇒
let '_ := function_parameter in
start_evaluating).
Definition stop_evaluating `{FArgs} (outcome : bool) : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Evaluation_result.(State.S_MakeVar.set) (Some outcome))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Status.(State.S_MakeVar.set) Waiting_for_input_message).
Definition parse `{FArgs} : State.Monad.t unit :=
let produce_add :=
State.Monad.Syntax.op_letstar lexeme
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Code.(State.MakeDeque_sig.inject) IAdd)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))) in
let produce_int :=
State.Monad.Syntax.op_letstar push_int_literal
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)) in
let produce_var :=
State.Monad.Syntax.op_letstar push_var
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)) in
let is_digit (d_value : ascii) : bool :=
(Compare.Char.(Compare.S.op_gteq) d_value "0" % char) &&
(Compare.Char.(Compare.S.op_lteq) d_value "9" % char) in
let is_letter (d_value : ascii) : bool :=
((Compare.Char.(Compare.S.op_gteq) d_value "a" % char) &&
(Compare.Char.(Compare.S.op_lteq) d_value "z" % char)) ||
((Compare.Char.(Compare.S.op_gteq) d_value "A" % char) &&
(Compare.Char.(Compare.S.op_lteq) d_value "Z" % char)) in
let is_identifier_char (d_value : ascii) : bool :=
(is_letter d_value) ||
((is_digit d_value) ||
((Compare.Char.(Compare.S.op_eq) d_value ":" % char) ||
(Compare.Char.(Compare.S.op_eq) d_value "%" % char))) in
State.Monad.Syntax.op_letstar State.Parser_state.(State.S_MakeVar.get)
(fun parser_state ⇒
match parser_state with
| State.ParseInt ⇒
State.Monad.Syntax.op_letstar current_char
(fun char_value ⇒
match
(char_value,
match char_value with
| Some d_value ⇒ is_digit d_value
| _ ⇒ false
end) with
| (Some d_value, true) ⇒ next_char
| (Some "+" % char, _) ⇒
State.Monad.Syntax.op_letstar produce_int
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar produce_add
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (Some (" " % char | "010" % char), _) ⇒
State.Monad.Syntax.op_letstar produce_int
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (None, _) ⇒
State.Monad.Syntax.op_letstar push_int_literal
(fun function_parameter ⇒
let '_ := function_parameter in
stop_parsing true)
| (_, _) ⇒ stop_parsing false
end)
| State.ParseVar ⇒
State.Monad.Syntax.op_letstar current_char
(fun char_value ⇒
match
(char_value,
match char_value with
| Some d_value ⇒ is_identifier_char d_value
| _ ⇒ false
end) with
| (Some d_value, true) ⇒ next_char
| (Some "+" % char, _) ⇒
State.Monad.Syntax.op_letstar produce_var
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar produce_add
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (Some (" " % char | "010" % char), _) ⇒
State.Monad.Syntax.op_letstar produce_var
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| (None, _) ⇒
State.Monad.Syntax.op_letstar push_var
(fun function_parameter ⇒
let '_ := function_parameter in
stop_parsing true)
| (_, _) ⇒ stop_parsing false
end)
| State.SkipLayout ⇒
State.Monad.Syntax.op_letstar current_char
(fun char_value ⇒
match
(char_value,
match char_value with
| Some d_value ⇒ is_digit d_value
| _ ⇒ false
end,
match char_value with
| Some d_value ⇒ is_letter d_value
| _ ⇒ false
end) with
| (Some (" " % char | "010" % char), _, _) ⇒ next_char
| (Some "+" % char, _, _) ⇒ produce_add
| (Some d_value, true, _) ⇒
State.Monad.Syntax.op_letstar lexeme
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set)
State.ParseInt)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))
| (Some d_value, _, true) ⇒
State.Monad.Syntax.op_letstar lexeme
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar next_char
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Parser_state.(State.S_MakeVar.set)
State.ParseVar)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt)))
| (None, _, _) ⇒ stop_parsing true
| (_, _, _) ⇒ stop_parsing false
end)
end).
Definition output `{FArgs}
(function_parameter : Contract_hash.t × Entrypoint_repr.t)
: int → State.Monad.t unit :=
let '(destination, entrypoint) := function_parameter in
fun (v_value : int) ⇒
State.Monad.Syntax.op_letstar State.Output_counter.(State.S_MakeVar.get)
(fun counter ⇒
State.Monad.Syntax.op_letstar
(State.Output_counter.(State.S_MakeVar.set) (Z.succ counter))
(fun function_parameter ⇒
let '_ := function_parameter in
let unparsed_parameters :=
Micheline.strip_locations (Micheline.Int tt (Z.of_int v_value))
in
let transaction :=
{|
Sc_rollup_outbox_message_repr.transaction.unparsed_parameters
:= unparsed_parameters;
Sc_rollup_outbox_message_repr.transaction.destination :=
destination;
Sc_rollup_outbox_message_repr.transaction.entrypoint :=
entrypoint; |} in
let message :=
Sc_rollup_outbox_message_repr.Atomic_transaction_batch
{|
Sc_rollup_outbox_message_repr.t.Atomic_transaction_batch.transactions
:= [ transaction ]; |} in
State.Monad.Syntax.op_letstar
State.Current_level.(State.S_MakeVar.get)
(fun outbox_level ⇒
let output :=
{| Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
Sc_rollup_PVM_sig.output.message_index := counter;
Sc_rollup_PVM_sig.output.message := message; |} in
State.Output.(State.MakeDict_sig.set) (Z.to_string counter)
output))).
Definition identifies_target_contract `{FArgs} (x_value : string)
: option (Contract_hash.t × Entrypoint_repr.t) :=
match String.split_on_char "%" % char x_value with
| cons destination entrypoint ⇒
match Contract_hash.of_b58check_opt destination with
| None ⇒
if Compare.String.(Compare.S.op_eq) x_value "out" then
return× (Contract_hash.zero, Entrypoint_repr.default)
else
Error_monad.Option_syntax.fail
| Some destination ⇒
let× entrypoint :=
match entrypoint with
| [] ⇒ return× Entrypoint_repr.default
| _ ⇒
let× entrypoint :=
Non_empty_string.of_string (String.concat "" entrypoint) in
let× entrypoint := Entrypoint_repr.of_annot_lax_opt entrypoint in
return× entrypoint
end in
return× (destination, entrypoint)
end
| [] ⇒ Error_monad.Option_syntax.fail
end.
Definition evaluate_preimage_request `{FArgs} (hash_value : string)
: State.Monad.t unit :=
match PS.Reveal_hash.of_b58check_opt hash_value with
| None ⇒ stop_evaluating false
| Some hash_value ⇒
State.Monad.Syntax.op_letstar
(State.Required_reveal.(State.S_MakeVar.set)
(Some (Sc_rollup_PVM_sig.Reveal_raw_data hash_value)))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_reveal)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
end.
Definition evaluate_dal_page_request `{FArgs}
: string → State.Monad.t unit :=
let attestation_lag := 1 in
let page_size := 4096 /i 64 in
let slot_size := (Pervasives.lsl 1 20) /i 64 in
let number_of_slots := 256 /i 64 in
let number_of_pages := slot_size /i page_size in
let mk_slot_index (slot_str : string) : option Dal_slot_repr.Index.t :=
let× index_value := Option.map Int32.to_int (Int32.of_string_opt slot_str)
in
if (index_value <i 0) || (index_value ≥i number_of_slots) then
None
else
Dal_slot_repr.Index.of_int index_value in
let mk_page_index (page_str : string) : option int :=
let× index_value := Option.map Int32.to_int (Int32.of_string_opt page_str)
in
if (index_value <i 0) || (index_value ≥i number_of_pages) then
None
else
Some index_value in
fun (raw_page_id : string) ⇒
let mk_page_id (current_lvl : Raw_level_repr.raw_level)
: option Dal_slot_repr.Page.t :=
match String.split_on_char ":" % char raw_page_id with
| cons lvl (cons slot (cons page [])) ⇒
let× lvl := Int32.of_string_opt lvl in
let× lvl := Bounded.Non_negative_int32.(Bounded.S.of_value) lvl in
let published_level :=
match Raw_level_repr.of_int32_non_negative lvl with
| Pervasives.Ok published_level ⇒ published_level
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Raw_level_repr.raw_level false
end in
let delta := Raw_level_repr.diff_value current_lvl published_level in
if (delta >i32 1) && (delta ≤i32 (2 ×i32 attestation_lag)) then
let× index_value := mk_slot_index slot in
let× page_index := mk_page_index page in
let slot_id :=
{| Dal_slot_repr.Header.id.published_level := published_level;
Dal_slot_repr.Header.id.index := index_value; |} in
Some
{| Dal_slot_repr.Page.t.slot_id := slot_id;
Dal_slot_repr.Page.t.page_index := page_index; |}
else
None
| _ ⇒ None
end in
State.Monad.Syntax.op_letstar State.Current_level.(State.S_MakeVar.get)
(fun current_lvl ⇒
match mk_page_id current_lvl with
| Some page_id ⇒
State.Monad.Syntax.op_letstar
(State.Required_reveal.(State.S_MakeVar.set)
(Some (Sc_rollup_PVM_sig.Request_dal_page page_id)))
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_reveal)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))
| None ⇒ stop_evaluating false
end).
Definition remove_prefix `{FArgs}
(prefix : String.t) (input : string) (input_len : int) : option string :=
let prefix_len := String.length prefix in
if
(input_len >i prefix_len) &&
(String.equal (String.sub input 0 prefix_len) prefix)
then
Some (String.sub input prefix_len (input_len -i prefix_len))
else
None.
Definition evaluate `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Code.(State.MakeDeque_sig.pop)
(fun i_value ⇒
match i_value with
| None ⇒ stop_evaluating true
| Some (IPush x_value) ⇒ State.Stack.(State.MakeDeque_sig.push) x_value
| Some (IStore x_value) ⇒
let len := String.length x_value in
match remove_prefix "hash:" x_value len with
| Some hash_value ⇒ evaluate_preimage_request hash_value
| None ⇒
match remove_prefix "dal:" x_value len with
| Some pid ⇒ evaluate_dal_page_request pid
| None ⇒
State.Monad.Syntax.op_letstar
State.Stack.(State.MakeDeque_sig.top)
(fun v_value ⇒
match v_value with
| None ⇒ stop_evaluating false
| Some v_value ⇒
match identifies_target_contract x_value with
| Some contract_entrypoint ⇒
output contract_entrypoint v_value
| None ⇒
State.Vars.(State.MakeDict_sig.set) x_value v_value
end
end)
end
end
| Some IAdd ⇒
State.Monad.Syntax.op_letstar State.Stack.(State.MakeDeque_sig.pop)
(fun v_value ⇒
match v_value with
| None ⇒ stop_evaluating false
| Some x_value ⇒
State.Monad.Syntax.op_letstar
State.Stack.(State.MakeDeque_sig.pop)
(fun v_value ⇒
match v_value with
| None ⇒ stop_evaluating false
| Some y_value ⇒
State.Stack.(State.MakeDeque_sig.push)
(x_value +i y_value)
end)
end)
end).
Definition reboot `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar
(State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar State.Stack.(State.MakeDeque_sig.clear)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad.Syntax.op_letstar State.Code.(State.MakeDeque_sig.clear)
(fun function_parameter ⇒
let '_ := function_parameter in
State.Monad._return tt))).
Definition eval_step `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Monad.is_stuck
(fun x_value ⇒
match x_value with
| Some _ ⇒ reboot
| None ⇒
State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.get)
(fun status ⇒
match status with
| Halted ⇒ boot
|
(Waiting_for_input_message | Waiting_for_reveal |
Waiting_for_metadata) ⇒
State.Monad.Syntax.op_letstar
State.Next_message.(State.S_MakeVar.get)
(fun msg ⇒
match msg with
| None ⇒
State.Monad.internal_error
"An input state was not provided an input."
| Some _ ⇒ start_parsing
end)
| Parsing ⇒ parse
| Evaluating ⇒ evaluate
end)
end).
Definition eval `{FArgs} (state_value : State.state) : State.state :=
state_of (ticked eval_step) state_value.
Axiom step_transition : ∀ `{FArgs},
option PS.input → State.state → State.state × PS.input_request.
Definition verify_proof `{FArgs}
(input_given : option PS.input) (proof_value : Context.(P.proof))
: M? PS.input_request :=
let result_value :=
Context.(P.verify_proof) proof_value (step_transition input_given) in
match result_value with
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Arith_proof_verification_failed" unit tt)
| Some (_state, request) ⇒ return? request
end.
Definition produce_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(input_given : option PS.input)
(state_value : Context.(P.Tree).(Context.TREE.tree)) : M? proof :=
let result_value :=
Context.(P.produce_proof) context_value state_value
(step_transition input_given) in
match result_value with
| Some (tree_proof, _requested) ⇒ return? tree_proof
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Arith_proof_production_failed" unit tt)
end.
Definition verify_origination_proof `{FArgs}
(proof_value : proof) (boot_sector : string) : bool :=
let before := Context.(P.proof_before) proof_value in
if
Sc_rollup_repr.State_hash.op_ltgt before reference_initial_state_hash
then
false
else
let result_value :=
Context.(P.verify_proof) proof_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| None ⇒ false
| Some (_, _) ⇒ true
end.
Definition produce_origination_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t)) (boot_sector : string)
: M? proof :=
let state_value := initial_state (Tree.(Context.TREE.empty) context_value)
in
let result_value :=
Context.(P.produce_proof) context_value state_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| Some (proof_value, _) ⇒ return? proof_value
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Arith_proof_production_failed" unit tt)
end.
Module output_proof.
Record record `{FArgs} : Set := Build {
output_proof : Context.(P.proof);
output_proof_state : hash;
output_proof_output : PS.output;
}.
Definition with_output_proof `{FArgs} output_proof (r : record) :=
Build _ _ _ _ output_proof r.(output_proof_state) r.(output_proof_output).
Definition with_output_proof_state `{FArgs} output_proof_state
(r : record) :=
Build _ _ _ _ r.(output_proof) output_proof_state r.(output_proof_output).
Definition with_output_proof_output `{FArgs} output_proof_output
(r : record) :=
Build _ _ _ _ r.(output_proof) r.(output_proof_state) output_proof_output.
End output_proof.
Definition output_proof `{FArgs} := output_proof.record.
Definition output_proof_encoding `{FArgs}
: Data_encoding.encoding output_proof :=
Data_encoding.conv
(fun (function_parameter : output_proof) ⇒
let '{|
output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output
|} := function_parameter in
(output_proof, output_proof_state, output_proof_output))
(fun (function_parameter : Context.(P.proof) × hash × PS.output) ⇒
let '(output_proof, output_proof_state, output_proof_output) :=
function_parameter in
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "output_proof" Context.(P.proof_encoding))
(Data_encoding.req None None "output_proof_state"
Sc_rollup_repr.State_hash.encoding)
(Data_encoding.req None None "output_proof_output" PS.output_encoding)).
Definition output_of_output_proof `{FArgs} (s_value : output_proof)
: PS.output := s_value.(output_proof.output_proof_output).
Definition state_of_output_proof `{FArgs} (s_value : output_proof) : hash :=
s_value.(output_proof.output_proof_state).
Definition output_key `{FArgs} (output : PS.output) : string :=
Z.to_string output.(Sc_rollup_PVM_sig.output.message_index).
Definition has_output `{FArgs} (output : PS.output) (tree_value : State.state)
: State.state × bool :=
let equal :=
State.Output.(State.MakeDict_sig.mapped_to) (output_key output) output
tree_value in
(tree_value, equal).
Definition verify_output_proof `{FArgs} (p_value : output_proof) : bool :=
let transition := has_output p_value.(output_proof.output_proof_output) in
let result_value :=
Context.(P.verify_proof) p_value.(output_proof.output_proof) transition in
match result_value with
| None ⇒ false
| Some _ ⇒ true
end.
Definition produce_output_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(state_value : Context.(P.Tree).(Context.TREE.tree))
(output_proof_output : PS.output)
: Pervasives.result output_proof Error_monad._error :=
let output_proof_state := state_hash state_value in
let result_value :=
Context.(P.produce_proof) context_value state_value
(has_output output_proof_output) in
match result_value with
| Some (output_proof, true) ⇒
return?
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}
| Some (_, false) ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "Arith_invalid_claim_about_outbox" unit tt)
| None ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "Arith_output_proof_production_failed" unit tt)
end.
(* Make *)
Definition functor `{FArgs} :=
{|
S.pp := pp;
S.proof_encoding := proof_encoding;
S.proof_start_state := proof_start_state;
S.proof_stop_state := proof_stop_state;
S.state_hash := state_hash;
S.initial_state := initial_state;
S.install_boot_sector := install_boot_sector;
S.is_input_state := is_input_state;
S.set_input := set_input;
S.eval := eval;
S.verify_proof := verify_proof;
S.produce_proof := produce_proof;
S.verify_origination_proof := verify_origination_proof;
S.produce_origination_proof := produce_origination_proof;
S.output_proof_encoding := output_proof_encoding;
S.output_of_output_proof := output_of_output_proof;
S.state_of_output_proof := state_of_output_proof;
S.verify_output_proof := verify_output_proof;
S.produce_output_proof := produce_output_proof;
S.name := name;
S.parse_boot_sector := parse_boot_sector;
S.pp_boot_sector := pp_boot_sector;
S.get_tick := get_tick;
S.get_status := get_status;
S.get_outbox := get_outbox;
S.equal_instruction := equal_instruction;
S.pp_instruction := pp_instruction;
S.get_parsing_result := get_parsing_result;
S.get_code := get_code;
S.get_stack := get_stack;
S.get_var := get_var;
S.get_evaluation_result := get_evaluation_result;
S.get_is_stuck := get_is_stuck
|}.
End Make.
Definition Make {Context_Tree_t Context_Tree_tree Context_proof : Set}
(Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof))
: S (state := Context.(P.Tree).(Context.TREE.tree))
(context := Context.(P.Tree).(Context.TREE.t)) (proof := Context.(P.proof))
(output_proof := _) (status := _) (instruction := _) :=
let '_ := Make.Build_FArgs Context in
Make.functor.
Definition Protocol_implementation :=
Make
(let Tree :=
let mem := Context.Tree.(Context.TREE.mem) in
let mem_tree := Context.Tree.(Context.TREE.mem_tree) in
let find := Context.Tree.(Context.TREE.find) in
let find_tree := Context.Tree.(Context.TREE.find_tree) in
let list_value := Context.Tree.(Context.TREE.list_value) in
let length := Context.Tree.(Context.TREE.length) in
let add := Context.Tree.(Context.TREE.add) in
let add_tree := Context.Tree.(Context.TREE.add_tree) in
let remove := Context.Tree.(Context.TREE.remove) in
let fold {a : Set} := Context.Tree.(Context.TREE.fold) in
let config_value := Context.Tree.(Context.TREE.config_value) in
let empty := Context.Tree.(Context.TREE.empty) in
let is_empty := Context.Tree.(Context.TREE.is_empty) in
let kind_value := Context.Tree.(Context.TREE.kind_value) in
let to_value := Context.Tree.(Context.TREE.to_value) in
let of_value := Context.Tree.(Context.TREE.of_value) in
let hash_value := Context.Tree.(Context.TREE.hash_value) in
let equal := Context.Tree.(Context.TREE.equal) in
let clear := Context.Tree.(Context.TREE.clear) in
let tree : Set := Context.tree in
let t : Set := Context.t in
let key : Set := list string in
let value : Set := bytes in
{|
Context.TREE.mem := mem;
Context.TREE.mem_tree := mem_tree;
Context.TREE.find := find;
Context.TREE.find_tree := find_tree;
Context.TREE.list_value := list_value;
Context.TREE.length := length;
Context.TREE.add := add;
Context.TREE.add_tree := add_tree;
Context.TREE.remove := remove;
Context.TREE.fold _ := fold;
Context.TREE.config_value := config_value;
Context.TREE.empty := empty;
Context.TREE.is_empty := is_empty;
Context.TREE.kind_value := kind_value;
Context.TREE.to_value := to_value;
Context.TREE.of_value := of_value;
Context.TREE.hash_value := hash_value;
Context.TREE.equal := equal;
Context.TREE.clear := clear
|} in
let tree : Set := Context.tree in
let hash_tree (t_value : Context.tree) : Sc_rollup_repr.State_hash.t :=
match
Sc_rollup_repr.State_hash.context_hash_to_state_hash
(Tree.(Context.TREE.hash_value) t_value) with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof : Set := Context.Proof.t Context.Proof.tree in
let verify_proof {A : Set}
(p_value : Context.Proof.t Context.Proof.tree)
(f_value : Context.tree → Context.tree × A)
: option (Context.tree × A) :=
id Result.to_option (Context.verify_tree_proof p_value f_value) in
let produce_proof {A B C D : Set} (_context : A) (_state : B) (_f : C)
: option D :=
None in
let kinded_hash_to_state_hash (function_parameter : Context.Proof.kinded_hash)
: M? Sc_rollup_repr.State_hash.t :=
match function_parameter with
| (Context.Proof.KValue hash_value | Context.Proof.KNode hash_value) ⇒
Sc_rollup_repr.State_hash.context_hash_to_state_hash hash_value
end in
let proof_before {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.before) with
| Pervasives.Ok prf ⇒ prf
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_after {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.after) with
| Pervasives.Ok prf ⇒ prf
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_encoding :=
Context.Proof_encoding.V2.Tree32.(Context.PROOF_ENCODING.tree_proof_encoding)
in
{|
P.Tree := Tree;
P.hash_tree := hash_tree;
P.proof_encoding := proof_encoding;
P.proof_before := proof_before;
P.proof_after := proof_after;
P.verify_proof _ := verify_proof;
P.produce_proof _ := produce_proof
|}).