Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file sc_rollup_arith.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862(*****************************************************************************)(* *)(* Open Source License *)(* Copyright (c) 2021 Nomadic Labs <contact@nomadic-labs.com> *)(* *)(* 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. *)(* *)(*****************************************************************************)openAlpha_contextopenSc_rollupmoduletypeP=sigmoduleTree:Context.TREEwithtypekey=stringlistandtypevalue=bytestypetree=Tree.treetypeproofvalproof_encoding:proofData_encoding.tvalproof_start_state:proof->State_hash.tvalproof_stop_state:proof->State_hash.tvalverify_proof:proof->(tree->(tree*'a)Lwt.t)->(tree*'a,[`Proof_mismatchofstring|`Stream_too_longofstring|`Stream_too_shortofstring])resultLwt.tendmoduletypeS=sigincludeSc_rollup_PVM_sem.Svalname:stringvalparse_boot_sector:string->stringoptionvalpp_boot_sector:Format.formatter->string->unitvalpp:state->(Format.formatter->unit->unit)Lwt.tvalget_tick:state->Sc_rollup.Tick.tLwt.ttypestatus=Halted|WaitingForInputMessage|Parsing|Evaluatingvalget_status:state->statusLwt.ttypeinstruction=IPush:int->instruction|IAdd:instructionvalequal_instruction:instruction->instruction->boolvalpp_instruction:Format.formatter->instruction->unitvalget_parsing_result:state->booloptionLwt.tvalget_code:state->instructionlistLwt.tvalget_stack:state->intlistLwt.tvalget_evaluation_result:state->booloptionLwt.tvalget_is_stuck:state->stringoptionLwt.tendmoduleMake(Context:P):Swithtypecontext=Context.Tree.tandtypestate=Context.tree=structmoduleTree=Context.Treetypecontext=Context.Tree.ttypehash=State_hash.ttypeproof=Context.proofletproof_encoding=Context.proof_encodingletproof_start_state=Context.proof_start_stateletproof_stop_state=Context.proof_stop_stateletname="arith"letparse_boot_sectors=Somesletpp_boot_sectorfmts=Format.fprintffmt"%s"stypetree=Tree.treetypestatus=Halted|WaitingForInputMessage|Parsing|Evaluatingtypeinstruction=IPush:int->instruction|IAdd:instructionletequal_instructioni1i2=match(i1,i2)with|(IPushx,IPushy)->Compare.Int.(x=y)|(IAdd,IAdd)->true|(_,_)->falseletpp_instructionfmt=function|IPushx->Format.fprintffmt"push(%d)"x|IAdd->Format.fprintffmt"add"(*
The machine state is represented using a Merkle tree.
Here is the data model of this state represented in the tree:
- tick : Tick.t
The current tick counter of the machine.
- status : status
The current status of the machine.
- stack : int deque
The stack of integers.
- next_message : string option
The current input message to be processed.
- code : instruction deque
The instructions parsed from the input message.
- lexer_state : int * int
The internal state of the lexer.
- parsing_state : parsing_state
The internal state of the parser.
- parsing_result : bool option
The outcome of parsing.
- evaluation_result : bool option
The outcome of evaluation.
*)moduleState=structtypestate=treemoduleMonad:sigtype'atvalrun:'at->state->(state*'aoption)Lwt.tvalis_stuck:stringoptiontvalinternal_error:string->'atvalreturn:'a->'atmoduleSyntax:sigval(let*):'at->('a->'bt)->'btendvalremove:Tree.key->unittvalfind_value:Tree.key->'aData_encoding.t->'aoptiontvalget_value:default:'a->Tree.key->'aData_encoding.t->'atvalset_value:Tree.key->'aData_encoding.t->'a->unittend=structtype'at=state->(state*'aoption)Lwt.tletreturnxstate=Lwt.return(state,Somex)letbindmfstate=letopenLwt_syntaxinlet*(state,res)=mstateinmatchreswithNone->return(state,None)|Someres->fresstatemoduleSyntax=structlet(let*)=bindendletrunmstate=mstateletinternal_error_key=["internal_error"]letinternal_errormsgtree=letopenLwt_syntaxinlet*tree=Tree.addtreeinternal_error_key(Bytes.of_stringmsg)inreturn(tree,None)letis_stucktree=letopenLwt_syntaxinlet*v=Tree.findtreeinternal_error_keyinreturn(tree,Some(Option.mapBytes.to_stringv))letremovekeytree=letopenLwt_syntaxinlet*tree=Tree.removetreekeyinreturn(tree,Some())letfind_valuekeyencodingstate=letopenLwt_syntaxinlet*obytes=Tree.findstatekeyinmatchobyteswith|None->return(state,SomeNone)|Somebytes->(matchData_encoding.Binary.of_bytes_optencodingbyteswith|None->internal_error"Internal_Error during decoding"state|Somev->return(state,Some(Somev)))letget_value~defaultkeyencoding=letopenSyntaxinlet*ov=find_valuekeyencodinginmatchovwithNone->returndefault|Somex->returnxletset_valuekeyencodingvaluetree=letopenLwt_syntaxinData_encoding.Binary.to_bytes_optencodingvalue|>function|None->internal_error"Internal_Error during encoding"tree|Somebytes->let*tree=Tree.addtreekeybytesinreturn(tree,Some())endopenMonadopenMonad.SyntaxmoduleMakeVar(P:sigtypetvalname:stringvalinitial:tvalpp:Format.formatter->t->unitvalencoding:tData_encoding.tend)=structletkey=[P.name]letcreate=set_valuekeyP.encodingP.initialletget=let*v=find_valuekeyP.encodinginmatchvwith|None->(* This case should not happen if [create] is properly called. *)returnP.initial|Somev->returnvletset=set_valuekeyP.encodingletpp=letopenMonad.Syntaxinlet*v=getinreturn@@funfmt()->Format.fprintffmt"@[%s : %a@]"P.nameP.ppvendmoduleMakeDeque(P:sigtypetvalname:stringvalencoding:tData_encoding.tend)=struct(*
A stateful deque.
[[head; end[] is the index range for the elements of the deque.
The length of the deque is therefore [end - head].
*)lethead_key=[P.name;"head"]letend_key=[P.name;"end"]letget_head=get_value~default:Z.zerohead_keyData_encoding.zletset_head=set_valuehead_keyData_encoding.zletget_end=get_value~default:(Z.of_int0)end_keyData_encoding.zletset_end=set_valueend_keyData_encoding.zletidx_keyidx=[P.name;Z.to_stringidx]letpushx=letopenMonad.Syntaxinlet*head_idx=get_headinlethead_idx'=Z.predhead_idxinlet*()=set_headhead_idx'inset_value(idx_keyhead_idx')P.encodingxletpop=letopenMonad.Syntaxinlet*head_idx=get_headinlet*end_idx=get_endinifZ.(leqend_idxhead_idx)thenreturnNoneelselet*v=find_value(idx_keyhead_idx)P.encodinginmatchvwith|None->(* By invariants of the Deque. *)assertfalse|Somex->let*()=remove(idx_keyhead_idx)inlethead_idx=Z.succhead_idxinlet*()=set_headhead_idxinreturn(Somex)letinjectx=letopenMonad.Syntaxinlet*end_idx=get_endinletend_idx'=Z.succend_idxinlet*()=set_endend_idx'inset_value(idx_keyend_idx)P.encodingxletto_list=letopenMonad.Syntaxinlet*head_idx=get_headinlet*end_idx=get_endinletrecauxlidx=ifZ.(ltidxhead_idx)thenreturnlelselet*v=find_value(idx_keyidx)P.encodinginmatchvwith|None->(* By invariants of deque *)assertfalse|Somev->aux(v::l)(Z.predidx)inaux[](Z.predend_idx)letclear=remove[P.name]endmoduleCurrentTick=MakeVar(structincludeTickletname="tick"end)moduleStack=MakeDeque(structtypet=intletname="stack"letencoding=Data_encoding.int31end)moduleCode=MakeDeque(structtypet=instructionletname="code"letencoding=Data_encoding.(union[case~title:"push"(Tag0)Data_encoding.int31(functionIPushx->Somex|_->None)(funx->IPushx);case~title:"add"(Tag1)Data_encoding.unit(functionIAdd->Some()|_->None)(fun()->IAdd);])end)moduleBoot_sector=MakeVar(structtypet=stringletname="boot_sector"letinitial=""letencoding=Data_encoding.stringletppfmts=Format.fprintffmt"%s"send)moduleStatus=MakeVar(structtypet=statusletinitial=Haltedletencoding=Data_encoding.string_enum[("Halted",Halted);("WaitingForInput",WaitingForInputMessage);("Parsing",Parsing);("Evaluating",Evaluating);]letname="status"letstring_of_status=function|Halted->"Halted"|WaitingForInputMessage->"WaitingForInputMessage"|Parsing->"Parsing"|Evaluating->"Evaluating"letppfmtstatus=Format.fprintffmt"%s"(string_of_statusstatus)end)moduleCurrentLevel=MakeVar(structtypet=Raw_level.tletinitial=Raw_level.rootletencoding=Raw_level.encodingletname="current_level"letpp=Raw_level.ppend)moduleMessageCounter=MakeVar(structtypet=Z.tletinitial=Z.(predzero)letencoding=Data_encoding.nletname="message_counter"letpp=Z.pp_printend)moduleNextMessage=MakeVar(structtypet=stringoptionletinitial=Noneletencoding=Data_encoding.(optionstring)letname="next_message"letppfmt=function|None->Format.fprintffmt"None"|Somes->Format.fprintffmt"Some %s"send)typeparser_state=ParseInt|SkipLayoutmoduleLexerState=MakeVar(structtypet=int*intletname="lexer_buffer"letinitial=(-1,-1)letencoding=Data_encoding.(tup2int31int31)letppfmt(start,len)=Format.fprintffmt"lexer.(start = %d, len = %d)"startlenend)moduleParserState=MakeVar(structtypet=parser_stateletname="parser_state"letinitial=SkipLayoutletencoding=Data_encoding.string_enum[("ParseInt",ParseInt);("SkipLayout",SkipLayout)]letppfmt=function|ParseInt->Format.fprintffmt"Parsing int"|SkipLayout->Format.fprintffmt"Skipping layout"end)moduleParsingResult=MakeVar(structtypet=booloptionletname="parsing_result"letinitial=Noneletencoding=Data_encoding.(optionbool)letppfmt=function|None->Format.fprintffmt"n/a"|Sometrue->Format.fprintffmt"parsing succeeds"|Somefalse->Format.fprintffmt"parsing fails"end)moduleEvaluationResult=MakeVar(structtypet=booloptionletname="evaluation_result"letinitial=Noneletencoding=Data_encoding.(optionbool)letppfmt=function|None->Format.fprintffmt"n/a"|Sometrue->Format.fprintffmt"evaluation succeeds"|Somefalse->Format.fprintffmt"evaluation fails"end)letpp=letopenMonad.Syntaxinlet*status_pp=Status.ppinlet*message_counter_pp=MessageCounter.ppinlet*next_message_pp=NextMessage.ppinlet*parsing_result_pp=ParsingResult.ppinlet*parser_state_pp=ParserState.ppinlet*lexer_state_pp=LexerState.ppinlet*evaluation_result_pp=EvaluationResult.ppinreturn@@funfmt()->Format.fprintffmt"@[<v 0 >@;%a@;%a@;%a@;%a@;%a@;%a@;%a@]"status_pp()message_counter_pp()next_message_pp()parsing_result_pp()parser_state_pp()lexer_state_pp()evaluation_result_pp()endopenStatetypestate=State.stateletppstate=letopenLwt_syntaxinlet*(_,pp)=Monad.runppstateinmatchppwith|None->return@@funfmt_->Format.fprintffmt"<opaque>"|Somepp->returnppopenMonadletinitial_statectxtboot_sector=letstate=Tree.emptyctxtinletm=letopenMonad.Syntaxinlet*()=Boot_sector.setboot_sectorinlet*()=Status.setHaltedinreturn()inletopenLwt_syntaxinlet*(state,_)=runmstateinreturnstateletstate_hashstate=letm=letopenMonad.Syntaxinlet*status=Status.getinmatchstatuswith|Halted->returnState_hash.zero|_->Context_hash.to_bytes@@Tree.hashstate|>funh->return@@State_hash.hash_bytes[h]inletopenLwt_syntaxinlet*state=Monad.runmstateinmatchstatewith|(_,Somehash)->returnhash|_->(* Hash computation always succeeds. *)assertfalseletboot=letopenMonad.Syntaxinlet*()=Status.createinlet*()=NextMessage.createinlet*()=Status.setWaitingForInputMessageinreturn()letresult_of~defaultmstate=letopenLwt_syntaxinlet*(_,v)=runmstateinmatchvwithNone->returndefault|Somev->returnvletstate_ofmstate=letopenLwt_syntaxinlet*(s,_)=runmstateinreturnsletget_tick=result_of~default:Tick.initialCurrentTick.getletis_input_state_monadic=letopenMonad.Syntaxinlet*status=Status.getinmatchstatuswith|WaitingForInputMessage->let*level=CurrentLevel.getinlet*counter=MessageCounter.getinreturn(Some(level,counter))|_->returnNoneletis_input_state=result_of~default:None@@is_input_state_monadicletget_status=result_of~default:WaitingForInputMessage@@Status.getletget_code=result_of~default:[]@@Code.to_listletget_parsing_result=result_of~default:None@@ParsingResult.getletget_stack=result_of~default:[]@@Stack.to_listletget_evaluation_result=result_of~default:None@@EvaluationResult.getletget_is_stuck=result_of~default:None@@is_stuckletset_input_monadicinput=letopenSc_rollup_PVM_seminlet{inbox_level;message_counter;payload}=inputinletopenMonad.Syntaxinlet*boot_sector=Boot_sector.getinletmsg=boot_sector^payloadinlet*last_level=CurrentLevel.getinlet*last_counter=MessageCounter.getinletupdate=let*()=CurrentLevel.setinbox_levelinlet*()=MessageCounter.setmessage_counterinlet*()=NextMessage.set(Somemsg)inreturn()inletdoes_not_follow=internal_error"The input message does not follow the previous one."inifRaw_level.(equallast_levelinbox_level)thenifZ.(equalmessage_counter(succlast_counter))thenupdateelsedoes_not_followelseifRaw_level.(last_level<inbox_level)thenifZ.(equalmessage_counterZ.zero)thenupdateelsedoes_not_followelsedoes_not_followletset_inputinput=state_of@@set_input_monadicinputletnext_char=letopenMonad.SyntaxinLexerState.(let*(start,len)=getinset(start,len+1))letno_message_to_lex()=internal_error"lexer: There is no input message to lex"letcurrent_char=letopenMonad.Syntaxinlet*(start,len)=LexerState.getinlet*msg=NextMessage.getinmatchmsgwith|None->no_message_to_lex()|Somes->ifCompare.Int.(start+len<String.lengths)thenreturn(Somes.[start+len])elsereturnNoneletlexeme=letopenMonad.Syntaxinlet*(start,len)=LexerState.getinlet*msg=NextMessage.getinmatchmsgwith|None->no_message_to_lex()|Somes->let*()=LexerState.set(start+len,0)inreturn(String.subsstartlen)letpush_int_literal=letopenMonad.Syntaxinlet*s=lexemeinmatchint_of_string_optswith|Somex->Code.inject(IPushx)|None->(* By validity of int parsing. *)assertfalseletstart_parsing:unitt=letopenMonad.Syntaxinlet*()=Status.setParsinginlet*()=ParsingResult.setNoneinlet*()=ParserState.setSkipLayoutinlet*()=LexerState.set(0,0)inlet*()=Status.setParsinginlet*()=Code.clearinreturn()letstart_evaluating:unitt=letopenMonad.Syntaxinlet*()=EvaluationResult.setNoneinlet*()=Stack.clearinlet*()=Status.setEvaluatinginreturn()letstop_parsingoutcome=letopenMonad.Syntaxinlet*()=ParsingResult.set(Someoutcome)instart_evaluatingletstop_evaluatingoutcome=letopenMonad.Syntaxinlet*()=EvaluationResult.set(Someoutcome)inStatus.setWaitingForInputMessageletparse:unitt=letopenMonad.Syntaxinletproduce_add=let*_=lexemeinlet*()=next_charinlet*()=Code.injectIAddinreturn()inletproduce_int=let*()=push_int_literalinlet*()=ParserState.setSkipLayoutinreturn()inletis_digitd=Compare.Char.(d>='0'&&d<='9')inlet*parser_state=ParserState.getinmatchparser_statewith|ParseInt->(let*char=current_charinmatchcharwith|Somedwhenis_digitd->next_char|Some'+'->let*()=produce_intinlet*()=produce_addinreturn()|Some' '->let*()=produce_intinlet*()=next_charinreturn()|None->let*()=push_int_literalinstop_parsingtrue|_->stop_parsingfalse)|SkipLayout->(let*char=current_charinmatchcharwith|Some' '->next_char|Some'+'->produce_add|Somedwhenis_digitd->let*_=lexemeinlet*()=next_charinlet*()=ParserState.setParseIntinreturn()|None->stop_parsingtrue|_->stop_parsingfalse)letevaluate=letopenMonad.Syntaxinlet*i=Code.popinmatchiwith|None->stop_evaluatingtrue|Some(IPushx)->Stack.pushx|SomeIAdd->(let*v=Stack.popinmatchvwith|None->stop_evaluatingfalse|Somex->(let*v=Stack.popinmatchvwith|None->stop_evaluatingfalse|Somey->Stack.push(x+y)))letreboot=letopenMonad.Syntaxinlet*()=Status.setWaitingForInputMessageinlet*()=Stack.clearinlet*()=Code.clearinreturn()leteval_step=letopenMonad.Syntaxinlet*x=is_stuckinmatchxwith|Some_->reboot|None->(let*status=Status.getinmatchstatuswith|Halted->boot|WaitingForInputMessage->(let*msg=NextMessage.getinmatchmsgwith|None->internal_error"An input state was not provided an input message."|Some_->start_parsing)|Parsing->parse|Evaluating->evaluate)lettickedm=letopenMonad.Syntaxinlet*tick=CurrentTick.getinlet*()=CurrentTick.set(Tick.nexttick)inmletevalstate=state_of(tickedeval_step)stateletverify_proof~inputproof=letopenLwt_syntaxinlettransitionstate=let*state=matchinputwith|None->evalstate|Someinput->state_of(ticked(set_input_monadicinput))stateinreturn(state,())inlet*x=Context.verify_proofprooftransitioninmatchxwithOk_->return_true|Error_->return_falseendmoduleProtocolImplementation=Make(structmoduleTree=structincludeContext.Treetypetree=Context.treetypet=Context.ttypekey=stringlisttypevalue=bytesendtypetree=Context.treetypeproof=Context.Proof.treeContext.Proof.tletverify_proof=Context.verify_tree_proofletkinded_hash_to_state_hash=function|`Valuehash|`Nodehash->State_hash.hash_bytes[Context_hash.to_byteshash]letproof_start_stateproof=kinded_hash_to_state_hashproof.Context.Proof.beforeletproof_stop_stateproof=kinded_hash_to_state_hashproof.Context.Proof.afterletproof_encoding=Context.Proof_encoding.V2.Tree32.tree_proof_encodingend)