Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file sc_rollup_wasm.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721(*****************************************************************************)(* *)(* Open Source License *)(* Copyright (c) 2021 Nomadic Labs <contact@nomadic-labs.com> *)(* Copyright (c) 2022 Trili Tech, <contact@trili.tech> *)(* *)(* Permission is hereby granted, free of charge, to any person obtaining a *)(* copy of this software and associated documentation files (the "Software"),*)(* to deal in the Software without restriction, including without limitation *)(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)(* and/or sell copies of the Software, and to permit persons to whom the *)(* Software is furnished to do so, subject to the following conditions: *)(* *)(* The above copyright notice and this permission notice shall be included *)(* in all copies or substantial portions of the Software. *)(* *)(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*)(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*)(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)(* DEALINGS IN THE SOFTWARE. *)(* *)(*****************************************************************************)typeerror+=WASM_proof_verification_failedtypeerror+=WASM_proof_production_failedtypeerror+=WASM_output_proof_production_failedtypeerror+=WASM_invalid_claim_about_outboxtypeerror+=WASM_invalid_dissection_distributionlet()=letopenData_encodinginletmsg="Invalid claim about outbox"inregister_error_kind`Permanent~id:"smart_rollup_wasm_invalid_claim_about_outbox"~title:msg~pp:(funfmt()->Format.pp_print_stringfmtmsg)~description:msgunit(functionWASM_invalid_claim_about_outbox->Some()|_->None)(fun()->WASM_invalid_claim_about_outbox);letmsg="Output proof production failed"inregister_error_kind`Permanent~id:"smart_rollup_wasm_output_proof_production_failed"~title:msg~pp:(funfmt()->Format.fprintffmt"%s"msg)~description:msgunit(functionWASM_output_proof_production_failed->Some()|_->None)(fun()->WASM_output_proof_production_failed);letmsg="Proof production failed"inregister_error_kind`Permanent~id:"smart_rollup_wasm_proof_production_failed"~title:msg~pp:(funfmt()->Format.fprintffmt"%s"msg)~description:msgunit(functionWASM_proof_production_failed->Some()|_->None)(fun()->WASM_proof_production_failed);letmsg="Invalid dissection distribution: not all ticks are a multiplier of the \
maximum number of ticks of a snapshot"inregister_error_kind`Permanent~id:"smart_rollup_wasm_invalid_dissection_distribution"~title:msg~pp:(funfmt()->Format.fprintffmt"%s"msg)~description:msgunit(functionWASM_invalid_dissection_distribution->Some()|_->None)(fun()->WASM_invalid_dissection_distribution)moduleV2_0_0=structletticks_per_snapshot=Z.of_int6411_000_000_000Lletoutbox_validity_period=Int32.of_int80_640letoutbox_message_limit=Z.of_int100letwell_known_reveal_preimage=""letwell_known_reveal_hash=Sc_rollup_reveal_hash.hash_string~scheme:Blake2B[well_known_reveal_preimage](*
This is the state hash of reference that both the prover of the
node and the verifier of the protocol {!Protocol_implementation}
have to agree on (if they do, it means they are using the same
tree structure).
We have to hard-code this value because the Wasm PVM uses Irmin as
its Merkle proof verification backend, and the economic protocol
cannot create an empty Irmin context. Such a context is required to
create an empty tree, itself required to create the initial state of
the Wasm PVM.
Utlimately, the value of this constant is decided by the prover of
reference (the only need is for it to be compatible with
{!Protocol_implementation}.)
Its value is the result of the following snippet
{|
let*! state = Prover.initial_state context in
Prover.state_hash state
|}
*)letreference_initial_state_hash=Sc_rollup_repr.State_hash.of_b58check_exn"srs11XQCynQfGtuUr4c47rAoazGeTfC33R5FmimBKbnMrWwntHURX1"openSc_rollup_reprmodulePS=Sc_rollup_PVM_sigmoduletypeTreeS=Context.TREEwithtypekey=stringlistandtypevalue=bytesmoduletypeMake_wasm=moduletypeofWasm_2_0_0.MakemoduletypeP=sigmoduleTree:TreeStypetree=Tree.treetypeproofvalproof_encoding:proofData_encoding.tvalproof_before:proof->State_hash.tvalproof_after:proof->State_hash.tvalverify_proof:proof->(tree->(tree*'a)Lwt.t)->(tree*'a)optionLwt.tvalproduce_proof:Tree.t->tree->(tree->(tree*'a)Lwt.t)->(proof*'a)optionLwt.tendmoduletypeS=sigincludeSc_rollup_PVM_sig.Svalparse_boot_sector:string->stringoptionvalpp_boot_sector:Format.formatter->string->unit(** [get_tick state] gets the total tick counter for the given PVM state. *)valget_tick:state->Sc_rollup_tick_repr.tLwt.t(** PVM status *)typestatus=|Computing|Waiting_for_input_message|Waiting_for_revealofSc_rollup_PVM_sig.reveal(** [get_status state] gives you the current execution status for the PVM. *)valget_status:state->statusLwt.tvalget_outbox:Raw_level_repr.t->state->Sc_rollup_PVM_sig.outputlistLwt.tend(* [Make (Make_backend) (Context)] creates a PVM.
The Make_backend is a functor that creates the backend of the PVM.
The Conext provides the tree and the proof types.
*)moduleMake(Make_backend:Make_wasm)(Context:P):Swithtypecontext=Context.Tree.tandtypestate=Context.treeandtypeproof=Context.proof=structmoduleTree=Context.Treetypecontext=Context.Tree.ttypehash=State_hash.ttypeproof=Context.proofletproof_encoding=Context.proof_encodingletproof_start_stateproof=Context.proof_beforeproofletproof_stop_stateproof=Context.proof_afterproofletparse_boot_sectors=Hex.to_string@@`Hexsletpp_boot_sectorfmts=Format.fprintffmt"%s"stypetree=Tree.treetypestatus=|Computing|Waiting_for_input_message|Waiting_for_revealofSc_rollup_PVM_sig.revealmoduleState=structtypestate=treemoduleMonad:sigtype'atvalrun:'at->state->(state*'a)Lwt.tvalreturn:'a->'atmoduleSyntax:sigval(let*):'at->('a->'bt)->'btendvalget:treetvalset:tree->unittvallift:'aLwt.t->'atend=structtype'at=state->(state*'a)Lwt.tletreturnxstate=Lwt.return(state,x)letbindmfstate=letopenLwt_syntaxinlet*state,res=mstateinfresstatemoduleSyntax=structlet(let*)=bindendletrunmstate=mstateletgets=Lwt.return(s,s)letsets_=Lwt.return(s,())letliftms=Lwt.map(funr->(s,r))mendendtypestate=State.statemoduleWASM_machine=Make_backend(Tree)openStateletpp_state=Lwt.return@@funfmt()->Format.pp_print_stringfmt"<wasm-state>"openMonadletinitial_state~empty=WASM_machine.initial_stateemptyletinstall_boot_sectorstateboot_sector=WASM_machine.install_boot_sector~ticks_per_snapshot~outbox_validity_period~outbox_message_limitboot_sectorstateletstate_hashstate=letcontext_hash=Tree.hashstateinLwt.return@@State_hash.context_hash_to_state_hashcontext_hashletresult_ofmstate=letopenLwt_syntaxinlet*_,v=runmstateinreturnvletstate_ofmstate=letopenLwt_syntaxinlet*s,_=runmstateinreturnsletget_tick:Sc_rollup_tick_repr.tMonad.t=letopenMonad.Syntaxinlet*s=getinlet*info=lift(WASM_machine.get_infos)inreturn@@Sc_rollup_tick_repr.of_zinfo.current_tickletget_tick:state->Sc_rollup_tick_repr.tLwt.t=result_ofget_tickletget_status:statusMonad.t=letopenMonad.SyntaxinletopenSc_rollup_PVM_siginlet*s=getinlet*info=lift(WASM_machine.get_infos)inreturn@@matchinfo.input_requestwith|No_input_required->Computing|Input_required->Waiting_for_input_message|Reveal_required(Wasm_2_0_0.Reveal_raw_datahash)->(matchData_encoding.Binary.of_string_optSc_rollup_reveal_hash.encodinghashwith|Somehash->Waiting_for_reveal(Reveal_raw_datahash)|None->(* In case of an invalid hash, the rollup is
blocked. Any commitment will be invalid. *)Waiting_for_reveal(Reveal_raw_datawell_known_reveal_hash))|Reveal_requiredWasm_2_0_0.Reveal_metadata->Waiting_for_revealReveal_metadataletget_last_message_read:_Monad.t=letopenMonad.Syntaxinlet*s=getinlet*info=lift(WASM_machine.get_infos)inreturn@@matchinfo.last_input_readwith|Some{inbox_level;message_counter}->letinbox_level=Raw_level_repr.of_int32_non_negativeinbox_levelinSome(inbox_level,message_counter)|_->Noneletis_input_state=letopenMonad.Syntaxinlet*status=get_statusinmatchstatuswith|Waiting_for_input_message->(let*last_read=get_last_message_readinmatchlast_readwith|Some(level,n)->return(PS.First_after(level,n))|None->returnPS.Initial)|Computing->returnPS.No_input_required|Waiting_for_revealreveal->return(PS.Needs_revealreveal)letis_input_state=result_ofis_input_stateletget_status:state->statusLwt.t=result_ofget_statusletget_outboxoutbox_levelstate=letoutbox_level_int32=Raw_level_repr.to_int32_non_negativeoutbox_levelinletopenLwt_syntaxinletrecauxoutboxmessage_index=letoutput=Wasm_2_0_0.{outbox_level=outbox_level_int32;message_index}inlet*res=WASM_machine.get_outputoutputstateinmatchreswith|None->return(List.revoutbox)|Somemsg->(letserialized=Sc_rollup_outbox_message_repr.unsafe_of_stringmsginmatchSc_rollup_outbox_message_repr.deserializeserializedwith|Error_->(* The [write_output] host function does not guarantee that the contents
of the returned output is a valid encoding of an outbox message.
We choose to ignore such messages. An alternative choice would be to
craft an output with a payload witnessing the illformedness of the
output produced by the kernel. *)(aux[@ocaml.tailcall])outbox(Z.succmessage_index)|Okmessage->letoutput=PS.{outbox_level;message_index;message}in(aux[@ocaml.tailcall])(output::outbox)(Z.succmessage_index))inaux[]Z.zeroletset_input_stateinput=letopenMonad.Syntaxinmatchinputwith|PS.Inbox_messageinput->letopenPSinlet{inbox_level;message_counter;payload}=inputinlet*s=getinlet*s=lift(WASM_machine.set_input_step{inbox_level=Raw_level_repr.to_int32_non_negativeinbox_level;message_counter;}(payload:>string)s)insets|PS.Reveal(PS.Raw_datadata)->let*s=getinlet*s=lift(WASM_machine.reveal_step(Bytes.of_stringdata)s)insets|PS.Reveal(PS.Metadatametadata)->letmetadata_bytes=Data_encoding.Binary.to_bytes_exnSc_rollup_metadata_repr.encodingmetadatainlet*s=getinlet*s=lift(WASM_machine.reveal_stepmetadata_bytess)insets|PS.Reveal(PS.Dal_page_content_opt)->(* FIXME/DAL: https://gitlab.com/tezos/tezos/-/issues/3927.
Handle DAL pages in wasm PVM. *)assertfalseletset_inputinput=state_of@@set_input_stateinputleteval_step=letopenMonad.Syntaxinlet*s=getinlet*s=lift(WASM_machine.compute_steps)insetsletevalstate=state_ofeval_stepstateletstep_transitioninput_givenstate=letopenLwt_syntaxinlet*request=is_input_statestateinlet*state=matchrequestwith|PS.No_input_required->evalstate|_->(matchinput_givenwith|Someinput->set_inputinputstate|None->returnstate)inreturn(state,request)letverify_proofinput_givenproof=letopenLwt_result_syntaxinlet*!result=Context.verify_proofproof(step_transitioninput_given)inmatchresultwith|None->tzfailWASM_proof_verification_failed|Some(_state,request)->returnrequestletproduce_proofcontextinput_givenstate=letopenLwt_result_syntaxinlet*!result=Context.produce_proofcontextstate(step_transitioninput_given)inmatchresultwith|Some(tree_proof,_requested)->returntree_proof|None->tzfailWASM_proof_production_failedletverify_origination_proofproofboot_sector=letopenLwt_syntaxinletbefore=Context.proof_beforeproofinifState_hash.(before<>reference_initial_state_hash)thenreturnfalseelselet*result=Context.verify_proofproof(funstate->let*state=install_boot_sectorstateboot_sectorinreturn(state,()))inmatchresultwithNone->returnfalse|Some(_,())->returntrueletproduce_origination_proofcontextboot_sector=letopenLwt_result_syntaxinlet*!state=initial_state~empty:(Tree.emptycontext)inlet*!result=Context.produce_proofcontextstate(funstate->letopenLwt_syntaxinlet*state=install_boot_sectorstateboot_sectorinreturn(state,()))inmatchresultwith|Some(tree_proof,())->returntree_proof|None->tzfailWASM_proof_production_failedtypeoutput_proof={output_proof:Context.proof;output_proof_state:hash;output_proof_output:PS.output;}letoutput_proof_encoding=letopenData_encodinginconv(fun{output_proof;output_proof_state;output_proof_output}->(output_proof,output_proof_state,output_proof_output))(fun(output_proof,output_proof_state,output_proof_output)->{output_proof;output_proof_state;output_proof_output})(obj3(req"output_proof"Context.proof_encoding)(req"output_proof_state"State_hash.encoding)(req"output_proof_output"PS.output_encoding))letoutput_of_output_proofs=s.output_proof_outputletstate_of_output_proofs=s.output_proof_statelethas_output:PS.output->boolMonad.t=function|{outbox_level;message_index;message}->(letopenMonad.Syntaxinlet*s=getinlet*result=lift(WASM_machine.get_output{outbox_level=Raw_level_repr.to_int32_non_negativeoutbox_level;message_index;}s)inletmessage_encoded=Data_encoding.Binary.to_string_exnSc_rollup_outbox_message_repr.encodingmessageinreturn@@matchresultwith|Someresult->Compare.String.(result=message_encoded)|None->false)letverify_output_proofp=letopenLwt_syntaxinlettransition=run@@has_outputp.output_proof_outputinlet*result=Context.verify_proofp.output_prooftransitioninmatchresultwithNone->returnfalse|Some_->returntrueletproduce_output_proofcontextstateoutput_proof_output=letopenLwt_result_syntaxinlet*!output_proof_state=state_hashstateinlet*!result=Context.produce_proofcontextstate@@run@@has_outputoutput_proof_outputinmatchresultwith|Some(output_proof,true)->return{output_proof;output_proof_state;output_proof_output}|Some(_,false)->failWASM_invalid_claim_about_outbox|None->failWASM_output_proof_production_failedletcheck_sections_number~default_number_of_sections~number_of_sections~dist=letopenSc_rollup_dissection_chunk_reprinletis_stop_chunk_aligned=Compare.Z.(Z.remdistticks_per_snapshot=Z.zero)inletmax_number_of_sections=Z.(divdistticks_per_snapshot)inletexpected=Compare.Z.min(Z.of_intdefault_number_of_sections)(ifis_stop_chunk_alignedthenmax_number_of_sectionselseZ.succmax_number_of_sections)inletgiven=Z.of_intnumber_of_sectionsinerror_unlessCompare.Z.(given=expected)(Dissection_number_of_sections_mismatch{given;expected})letcheck_dissection~default_number_of_sections~start_chunk~stop_chunkdissection=letopenResult_syntaxinletopenSc_rollup_dissection_chunk_reprinletdist=Sc_rollup_tick_repr.distancestart_chunk.tickstop_chunk.tickin(*
We fall back to the default dissection check when the
[kernel_run] culprit has been found and is being dissected.
This condition will also be met if the PVM is stuck (because
it is unlikely that [ticks_per_snapshot] messages can be
posted in a commitment period), which is OKay because the Fast
Execution cannot be leveraged in that case, which means the
ad-hoc dissection predicate would not provide any speed up.
*)ifCompare.Z.(dist<=ticks_per_snapshot)thendefault_check~section_maximum_size:Z.(divdist(Z.of_int2))~check_sections_number:default_check_sections_number~default_number_of_sections~start_chunk~stop_chunkdissectionelse(*
There are enough ticks to consider that at least one call
to [kernel_run] is involved.
We now need to consider two cases: either [stop_chunk] is a
multiple of [ticks_per_snapshot] (the PVM is not stuck), or
it is not (the PVM has been stuck during the processing
of one of the ticks of the dissection).
For the latter case, we want to validate a dissection if
1. Every complete [kernel_run] invocations are dissected
as normal in the n-1 first chunks, and
2. The final section contains all the ticks of the
interrupted [kernel_run].
*)letis_stop_chunk_aligned=Compare.Z.(Z.remdistticks_per_snapshot=Z.zero)in(*
We keep the same dissection predicate as the default
dissection that a given section cannot be more than half of
the “full distance”, but we only consider the complete
calls to [kernel_run] in the “full distance”. The remainder
ticks will be put in the very last section.
*)letconsidered_dist=ifis_stop_chunk_alignedthendistelseletlast_valid_stop_tick=Sc_rollup_tick_repr.of_zZ.(mul(div(Sc_rollup_tick_repr.to_zstop_chunk.tick)ticks_per_snapshot)ticks_per_snapshot)inSc_rollup_tick_repr.(distancestart_chunk.ticklast_valid_stop_tick)in(*
There is one last corner case to consider: if the stuck
state happens in the second [kernel_run] of the period.
In this case, the considered distance is equal to the
snapshot size, and divided this value by two means the
maximum size of a section becomes 0.
So we keep that a section length is at least
[ticks_per_snapshot].
*)letsection_maximum_size=Z.maxticks_per_snapshot(Z.divconsidered_dist(Z.of_int2))inlet*()=default_check~section_maximum_size~check_sections_number~default_number_of_sections~start_chunk~stop_chunkdissectioninerror_unless(List.for_all(funchunk->letopenSc_rollup_tick_reprinZ.(equal(rem(to_zchunk.tick)ticks_per_snapshot)zero||Sc_rollup_tick_repr.equalstart_chunk.tickchunk.tick||Sc_rollup_tick_repr.equalstop_chunk.tickchunk.tick))dissection)WASM_invalid_dissection_distributionletget_current_levelstate=letopenLwt_syntaxinlet+res=result_ofget_last_message_readstateinOption.mapfstresmoduleInternal_for_tests=structletinsert_failurestate=letaddn=Tree.addstate["failures";string_of_intn]Bytes.emptyinletopenLwt_syntaxinlet*n=Tree.lengthstate["failures"]inaddnendendmoduleProtocol_implementation=Make(Wasm_2_0_0.Make)(structmoduleTree=structincludeContext.Treetypetree=Context.treetypet=Context.ttypekey=stringlisttypevalue=bytesendtypetree=Context.treetypeproof=Context.Proof.treeContext.Proof.tletverify_proofpf=letopenLwt_option_syntaxinlet*?()=Result.to_option(Context_binary_proof.check_is_binaryp)inLwt.mapResult.to_option(Context.verify_tree_proofpf)letproduce_proof_context_state_f=(* Can't produce proof without full context*)Lwt.returnNoneletkinded_hash_to_state_hash=function|`Valuehash|`Nodehash->State_hash.context_hash_to_state_hashhashletproof_beforeproof=kinded_hash_to_state_hashproof.Context.Proof.beforeletproof_afterproof=kinded_hash_to_state_hashproof.Context.Proof.afterletproof_encoding=Context.Proof_encoding.V2.Tree2.tree_proof_encodingend)end