package Ġorg . move . ide . ins pe ctions Ċ Ċ import Ġorg . move . utils . tests . annotation . Ins pe ctions TestCase Ċ Ċ class ĠM v Type Check Inspection Test : ĠIns pe ctions TestCase ( Mv Type Check Inspection :: class ) Ġ{ ĊĠĠĠ Ġfun Ġ` test Ġincorrect Ġtype Ġaddress Ġpassed Ġwhere Ġ& signer Ġis Ġexpected `() Ġ= Ġcheck Errors (""" ĊĠĠĠĠĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġsend ( account : Ġ& signer ) Ġ{} ĊĠĠĠĠĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġmain ( addr : Ġaddress ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġsend (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' account ': Ġtype Ġ' address ' Ġis Ġnot Ġcompatible Ġwith Ġ'& signer '"> addr </ error >) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĠĠĠĠĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġincorrect Ġtype Ġu 8 Ġpassed Ġwhere Ġ& signer Ġis Ġexpected `() Ġ= Ġcheck Errors (""" ĊĠĠĠĠĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġsend ( account : Ġ& signer ) Ġ{} ĊĠĠĠĠĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġmain ( addr : Ġu 8 ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġsend (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' account ': Ġtype Ġ' u 8 ' Ġis Ġnot Ġcompatible Ġwith Ġ'& signer '"> addr </ error >) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĠĠĠĠĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġerrors Ġif Ġsame Ġtype `() Ġ= Ġcheck Errors (""" ĊĠĠĠĠĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġsend ( account : Ġ& signer ) Ġ{} ĊĠĠĠĠĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġmain ( acc : Ġ& signer ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġsend ( acc ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĠĠĠĠĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġmutable Ġreference Ġcompatible Ġwith Ġimmutable Ġreference `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠOption < Element > Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġvec : Ġvector < Element > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġis _ none < Element >( t : Ġ& Option < Element >): Ġbool Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġtrue ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġmain ( opt : Ġ& mut ĠOption < Element >) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis _ none ( opt ); ĊĠĠĠĠĠĠĠ Ġ} ĠĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġdifferent Ġgeneric Ġtypes `() Ġ= Ġcheck Errors ( ĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠOption < Element > Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġis _ none < Elem >( t : ĠOption < u 6 4 >): Ġbool Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġtrue ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġopt Ġ= ĠOption < u 8 > Ġ{}; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis _ none (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' t ': Ġtype Ġ' Option < u 8 >' Ġis Ġnot Ġcompatible Ġwith Ġ' Option < u 6 4 >' "> opt </ error >) ĊĠĠĠĠĠĠĠ Ġ} ĠĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġdifferent Ġgeneric Ġtypes Ġfor Ġreferences `() Ġ= Ġcheck Errors ( ĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠOption < Element > Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġis _ none < Elem >( t : Ġ& Option < u 6 4 >): Ġbool Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġtrue ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġopt Ġ= Ġ& Option < u 8 > Ġ{}; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis _ none (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' t ': Ġtype Ġ'& Option < u 8 >' Ġis Ġnot Ġcompatible Ġwith Ġ'& Option < u 6 4 >' "> opt </ error >) ĊĠĠĠĠĠĠĠ Ġ} ĠĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġimmutable Ġreference Ġis Ġnot Ġcompatible Ġwith Ġmutable Ġreference `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠOption < Element > Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġvec : Ġvector < Element > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġis _ none < Element >( t : Ġ& mut ĠOption < Element >): Ġbool Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġtrue ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġmain < Element >( opt : Ġ& Option < Element >) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis _ none (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' t ': Ġtype Ġ'& Option < Element >' Ġis Ġnot Ġcompatible Ġwith Ġ'& mut ĠOption < Element >' "> opt </ error >); ĊĠĠĠĠĠĠĠ Ġ} ĠĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġincorrect Ġtype Ġof Ġargument Ġwith Ġstruct Ġliteral `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġuse _ a ( a : ĠA ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġuse _ a (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' a ': Ġtype Ġ' B ' Ġis Ġnot Ġcompatible Ġwith Ġ' A '"> B Ġ{} </ error >) ĠĠĠĠĠĠĠĠĠĠĠĠ ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġincorrect Ġtype Ġof Ġargument Ġwith Ġcall Ġexpression `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġuse _ a ( a : ĠA ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġget _ b (): ĠB Ġ{ ĠB Ġ{} Ġ} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġuse _ a (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' a ': Ġtype Ġ' B ' Ġis Ġnot Ġcompatible Ġwith Ġ' A '"> get _ b ()</ error >) ĠĠĠĠĠĠĠĠĠĠĠĠ ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġincorrect Ġtype Ġof Ġargument Ġwith Ġcall Ġexpression Ġfrom Ġdifferent Ġmodule `() Ġ= Ġcheck Errors (""" Ċ address Ġ 0 x 1 Ġ{ ĊĠĠĠ Ġmodule ĠOther Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġ{} ĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġget _ b (): ĠB Ġ{ ĠB Ġ{} Ġ} ĊĠĠĠ Ġ} ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġuse Ġ 0 x 1 :: Other :: get _ b ; ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġuse _ a ( a : ĠA ) Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġuse _ a (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' a ': Ġtype Ġ' 0 x 1 :: Other :: B ' Ġis Ġnot Ġcompatible Ġwith Ġ' A '"> get _ b ()</ error >) ĠĠĠĠĠĠĠĠĠĠĠĠ ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} Ċ } ĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġbyte array Ġis Ġvector Ġof Ġu 8 `() Ġ= Ġcheck Errors (""" ĊĠĠĠĠĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġsend ( a : Ġvector < u 8 >) Ġ{} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġa Ġ= Ġb " dead beef "; ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġsend ( a ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĠĠĠĠĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġerror Ġfor Ġcompatible Ġgeneric Ġwith Ġexplicit Ġparameter `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠDi em < Coin Type > Ġhas Ġstore Ġ{ Ġval : Ġu 6 4 Ġ} ĊĠĠĠĠĠĠĠ Ġstruct ĠBalance < Token > Ġhas Ġkey Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġcoin : ĠDi em < Token > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġvalue < Coin Type : Ġstore >( coin : Ġ& Di em < Coin Type >) Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġmain < Token : Ġstore >() Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġbalance : ĠBalance < Token >; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġcoin Ġ= Ġ& balance . coin ; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġvalue < Token >( coin ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġerror Ġfor Ġcompatible Ġgeneric Ġwith Ġinferred Ġparameter `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠDi em < Coin Type > Ġhas Ġstore Ġ{ Ġval : Ġu 6 4 Ġ} ĊĠĠĠĠĠĠĠ Ġstruct ĠBalance < Token > Ġhas Ġkey Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġcoin : ĠDi em < Token > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġvalue < Coin Type : Ġstore >( coin : Ġ& Di em < Coin Type >) Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġmain < Token : Ġstore >() Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġbalance : ĠBalance < Token >; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġcoin Ġ= Ġ& balance . coin ; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġvalue ( coin ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġreturn Ġtype Ġbut Ġreturns Ġu 8 `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġcall () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" Invalid Ġreturn Ġtype : Ġexpected Ġ' ()', Ġfound Ġ' integer '"> return Ġ 1 </ error >; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġreturn Ġtype Ġbut Ġreturns Ġu 8 Ġwith Ġexpression `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġcall () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" Invalid Ġreturn Ġtype : Ġexpected Ġ' ()', Ġfound Ġ' integer '"> 1 </ error > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġif Ġstatement Ġreturns Ġ() `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif Ġ( true ) Ġ{ 1 } Ġelse Ġ{ 2 }; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġblock Ġexpr Ġreturns Ġ() `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ{ 1 }; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġerror Ġon Ġcode Ġblock Ġif Ġempty Ġblock Ġand Ġreturn Ġtype `() Ġ= Ġcheck Errors ( ĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġcall (): Ġu 8 Ġ{< error Ġdescr =" Invalid Ġreturn Ġtype : Ġexpected Ġ' u 8 ', Ġfound Ġ' () '"> }</ error > ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġvector Ġpush Ġback `() Ġ= Ġcheck Errors ( ĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġnative Ġpublic Ġfun Ġpush _ back < Element >( v : Ġ& mut Ġvector < Element >, Ġe : ĠElement ); ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġfun Ġm < E : Ġdrop >( v : Ġ& mut Ġvector < E >, Ġx : ĠE ): Ġu 8 Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" Invalid Ġreturn Ġtype : Ġexpected Ġ' u 8 ', Ġfound Ġ' () '"> push _ back ( v , Ġx )</ error > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġif Ġcondition Ġshould Ġbe Ġboolean `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif Ġ(< error Ġdescr =" In compatible Ġtype Ġ' integer ', Ġexpected Ġ' bool '"> 1 </ error >) Ġ 1 ; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġincompatible Ġtypes Ġfrom Ġbranches `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif Ġ( true ) Ġ{ 1 } Ġelse Ġ{< error Ġdescr =" In compatible Ġtype Ġ' bool ', Ġexpected Ġ' integer '"> true </ error > }; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġtype Ġerror Ġwith Ġexplicit Ġgeneric Ġas Ġmove _ to `() Ġ= Ġcheck Errors ( ĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠOption < Element > Ġhas Ġcopy , Ġdrop , Ġstore Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġelement : ĠElement ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġsome < Element >( e : ĠElement ): ĠOption < Element > Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠOption Ġ{ Ġelement : Ġe Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġstruct ĠVault < Vault Content : Ġstore > Ġhas Ġkey Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġcontent : ĠOption < Vault Content > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġnew < Content : Ġstore >( owner : Ġ& signer , Ġ Ġcontent : ĠContent ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġmove _ to < Vault < Content >>( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġowner , ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠVault Ġ{ Ġcontent : Ġsome ( content ) Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġtype Ġcheck Ġincompatible Ġconstraints `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠC Ġ{} ĊĠĠĠĠĠĠĠ Ġstruct ĠD Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġnew < Content >( a : ĠContent , Ġb : ĠContent ): ĠContent Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġnew ( C Ġ{}, Ġ< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' b ': Ġtype Ġ' D ' Ġis Ġnot Ġcompatible Ġwith Ġ' C '"> D Ġ{} </ error >) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġerror Ġif Ġresolved Ġtype Ġrequires Ġa Ġreference `() Ġ= Ġcheck Errors ( ĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġindex _ of < Element >( v : Ġ& vector < Element >, Ġe : Ġ& Element ): Ġ( bool , Ġu 6 4 ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ( false , Ġ 0 ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġids : Ġvector < u 6 4 >; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġindex _ of (& ids , Ġ< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' e ': Ġtype Ġ' u 6 4 ' Ġis Ġnot Ġcompatible Ġwith Ġ'& u 6 4 '"> 1 u 6 4 </ error >); ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġreturn Ġgeneric Ġtuple Ġfrom Ġnested Ġcallable `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠM int Capability < phantom ĠCoin Type > Ġhas Ġkey , Ġstore Ġ{} ĊĠĠĠĠĠĠĠ Ġstruct ĠB urn Capability < phantom ĠCoin Type > Ġhas Ġkey , Ġstore Ġ{} ĊĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġregister _ native _ currency < FC oin Type > (): Ġ( Mint Capability < FC oin Type >, ĠB urn Capability < FC oin Type >) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġregister _ currency < FC oin Type >() ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġregister _ currency < FC oin Type > (): Ġ( Mint Capability < FC oin Type >, ĠB urn Capability < FC oin Type >) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn Ġ( Mint Capability < FC oin Type >{ }, ĠB urn Capability < FC oin Type >{ }) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġemit Ġevent Ġrequires Ġmutable Ġreference Ġerror `() Ġ= Ġcheck Errors ( ĊĠĠĠĠĠĠĠ Ġ""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠEvent Handle < phantom ĠT : Ġdrop Ġ+ Ġstore > Ġhas Ġstore Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġcounter : Ġu 6 4 , ĊĠĠĠĠĠĠĠĠĠĠĠ Ġguid : Ġvector < u 8 >, ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġstruct ĠAccount Ġhas Ġkey Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġhandle : ĠEvent Handle < Event > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġstruct ĠEvent Ġhas Ġstore , Ġdrop Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġemit _ event < T : Ġdrop Ġ+ Ġstore >( handler _ ref : Ġ& mut ĠEvent Handle < T >, Ġmsg : ĠT ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġm < Type : Ġstore Ġ+ Ġdrop >() Ġacquire s ĠAccount Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġemit _ event (< error Ġdescr =" Invalid Ġargument Ġfor Ġparameter Ġ' handler _ ref ': Ġtype Ġ' Event Handle < Event >' Ġis Ġnot Ġcompatible Ġwith Ġ'& mut ĠEvent Handle < Event >' "> borrow _ global _ mut < Account >( @ 0 x 1 ). handle </ error >, ĠEvent Ġ{}); ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ""" ĊĠĠĠ Ġ) ĊĊĠĠĠ Ġfun Ġ` test Ġfields Ġof Ġstruct Ġshould Ġhave Ġabilities Ġof Ġstruct `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġhas Ġcopy Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" The Ġtype Ġ' A ' Ġdoes Ġnot Ġhave Ġthe Ġability Ġ' copy ' Ġrequired Ġby Ġthe Ġdeclared Ġability Ġ' copy ' Ġof Ġthe Ġstruct Ġ' B '"> a : ĠA </ error > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġkey Ġstruct Ġrequires Ġstore Ġfields `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġhas Ġkey Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" The Ġtype Ġ' A ' Ġdoes Ġnot Ġhave Ġthe Ġability Ġ' store ' Ġrequired Ġby Ġthe Ġdeclared Ġability Ġ' key ' Ġof Ġthe Ġstruct Ġ' B '"> a : ĠA </ error > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġstore Ġstruct Ġrequires Ġstore Ġfields `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġhas Ġstore Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" The Ġtype Ġ' A ' Ġdoes Ġnot Ġhave Ġthe Ġability Ġ' store ' Ġrequired Ġby Ġthe Ġdeclared Ġability Ġ' store ' Ġof Ġthe Ġstruct Ġ' B '"> a : ĠA </ error > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġcopy Ġstruct Ġrequires Ġcopy Ġfields `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġhas Ġcopy Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" The Ġtype Ġ' A ' Ġdoes Ġnot Ġhave Ġthe Ġability Ġ' copy ' Ġrequired Ġby Ġthe Ġdeclared Ġability Ġ' copy ' Ġof Ġthe Ġstruct Ġ' B '"> a : ĠA </ error > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġdrop Ġstruct Ġrequires Ġdrop Ġfields `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠA Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġstruct ĠB Ġhas Ġdrop Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ< error Ġdescr =" The Ġtype Ġ' A ' Ġdoes Ġnot Ġhave Ġthe Ġability Ġ' drop ' Ġrequired Ġby Ġthe Ġdeclared Ġability Ġ' drop ' Ġof Ġthe Ġstruct Ġ' B '"> a : ĠA </ error > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġfunction Ġinvocation Ġwith Ġexplicitly Ġprovided Ġgeneric Ġtype `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule ĠEvent Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠMessage Ġhas Ġdrop Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġemit _ event < T : Ġstore Ġ+ Ġdrop >() Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġemit _ event << error Ġdescr =" The Ġtype Ġ' Message ' Ġdoes Ġnot Ġhave Ġrequired Ġability Ġ' store '"> Message </ error >>() ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġstruct Ġconstructor Ġwith Ġexplicitly Ġprovided Ġgeneric Ġtype `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule ĠEvent Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠMessage Ġhas Ġdrop Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġstruct ĠEvent < Message : Ġstore Ġ+ Ġdrop > Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠEvent << error Ġdescr =" The Ġtype Ġ' Message ' Ġdoes Ġnot Ġhave Ġrequired Ġability Ġ' store '"> Message </ error >> Ġ{}; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġtype Ġparam `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: Event Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠMessage Ġhas Ġdrop Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġemit _ event < T : Ġstore Ġ+ Ġdrop >() Ġ{} ĊĠĠĠĠĠĠĠĠĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġmain < M : Ġdrop >() Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġemit _ event << error Ġdescr =" The Ġtype Ġ' M ' Ġdoes Ġnot Ġhave Ġrequired Ġability Ġ' store '"> M </ error >>() ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĊĠĠĠ Ġfun Ġ` test Ġno Ġrequired Ġability Ġ' key ' Ġfor Ġmove _ to Ġargument `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠRes Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġmain ( s : Ġ& signer , Ġr : ĠRes ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġmove _ to ( s , Ġ< error Ġdescr =" The Ġtype Ġ' Res ' Ġdoes Ġnot Ġhave Ġrequired Ġability Ġ' key '"> r </ error >) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġerror Ġin Ġmove _ to Ġwith Ġresource `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠRes Ġhas Ġkey Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġmain ( s : Ġ& signer , Ġr : ĠRes ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġmove _ to < Res >( s , Ġr ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġrequired Ġability Ġfor Ġstruct Ġfor Ġtype Ġparam `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠRes Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġsave < T : Ġkey >( r : ĠT ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġmain ( r : ĠRes ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġsave (< error Ġdescr =" The Ġtype Ġ' Res ' Ġdoes Ġnot Ġhave Ġrequired Ġability Ġ' key '"> r </ error >) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġerror Ġin Ġtype Ġparam Ġif Ġstructure Ġhas Ġrequired Ġabilities `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠRes Ġhas Ġkey Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġsave < T : Ġkey >( r : ĠT ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġmain ( r : ĠRes ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġsave ( r ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġerror Ġin Ġspecs `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġbalance < Token : Ġstore >() Ġ{} ĊĠĠĠĠĠĠĠ Ġspec Ġschema ĠPay From Ens ures < Token > Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġensures Ġbalance < Token >(); ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġpass Ġprimitive Ġtype Ġto Ġgeneric Ġwith Ġrequired Ġabilities `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġbalance < Token : Ġkey >( k : ĠToken ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġbalance (< error Ġdescr =" The Ġtype Ġ' address ' Ġdoes Ġnot Ġhave Ġrequired Ġability Ġ' key ' ">@ 0 x 1 </ error >); ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġpass Ġgeneric Ġwith Ġabilities Ġwhen Ġprimitive Ġtype Ġis Ġexpected `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġcount ( val : Ġu 8 ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġbalance < Token : Ġkey >( k : ĠToken ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġcount (< error Ġdescr =" The Ġtype Ġ' Token ' Ġdoes Ġnot Ġhave Ġrequired Ġability Ġ' drop '"> k </ error >); ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġinvalid Ġtype Ġfor Ġfield Ġin Ġstruct Ġliteral `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠDe al Ġ{ Ġval : Ġu 8 Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠDe al Ġ{ Ġval : Ġ< error Ġdescr =" Invalid Ġargument Ġfor Ġfield Ġ' val ': Ġtype Ġ' bool ' Ġis Ġnot Ġcompatible Ġwith Ġ' u 8 '"> false </ error > Ġ}; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġvalid Ġtype Ġfor Ġfield `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠDe al Ġ{ Ġval : Ġu 8 Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġmain () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠDe al Ġ{ Ġval : Ġ 1 0 Ġ}; ĊĠĠĠĠĠĠĠĠĠĠĠ ĠDe al Ġ{ Ġval : Ġ 1 0 u 8 Ġ}; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġneed Ġfor Ġexplicit Ġtype Ġparameter Ġif Ġinf err able Ġfrom Ġcontext `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠOption < Element > Ġhas Ġcopy , Ġdrop , Ġstore Ġ{} ĊĠĠĠĠĠĠĠ Ġpublic Ġfun Ġnone < Element > (): ĠOption < Element > Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠOption Ġ{} ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġstruct ĠS Ġ{ Ġfield : ĠOption < address > Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġm (): ĠS Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠS Ġ{ Ġfield : Ġnone () Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĊĠĠĠ Ġ} ĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġno Ġneed Ġfor Ġvector Ġempty () Ġgeneric `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġ/// ĠCreate Ġan Ġempty Ġvector . ĊĠĠĠĠĠĠĠ Ġnative Ġpublic Ġfun Ġempty < Element > (): Ġvector < Element >; ĊĠĠĠĠĠĠĠ Ġstruct ĠCap State < phantom ĠFeature > Ġhas Ġkey Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġdeleg ates : Ġvector < address > ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠCap State Ġ{ Ġdeleg ates : Ġempty () Ġ}; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġtype Ġerror Ġin Ġstruct Ġliteral Ġfield Ġsh orthand `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠS Ġ{ Ġa : Ġu 8 Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġa Ġ= Ġtrue ; ĊĠĠĠĠĠĠĠĠĠĠĠ ĠS Ġ{ Ġ< error Ġdescr =" Invalid Ġargument Ġfor Ġfield Ġ' a ': Ġtype Ġ' bool ' Ġis Ġnot Ġcompatible Ġwith Ġ' u 8 '"> a </ error > Ġ}; ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġdo Ġnot Ġcrash Ġtype Ġchecking Ġinvalid Ġnumber Ġof Ġtype Ġparams Ġor Ġcall Ġparams `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠS < R : Ġkey > Ġ{ Ġval : ĠR Ġ} ĊĠĠĠĠĠĠĠ Ġfun Ġcall ( a : Ġu 8 ) Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġm () Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlet Ġs Ġ= ĠS < u 8 , Ġu 8 >{ }; ĊĠĠĠĠĠĠĠĠĠĠĠ Ġcall ( 1 , Ġ 2 , Ġ 3 ); ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġexplicit Ġunit Ġreturn `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġfun Ġm (): Ġ() Ġ{} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") ĊĊĠĠĠ Ġfun Ġ` test Ġif Ġelse Ġwith Ġreferences Ġno Ġerror Ġif Ġco erce able `() Ġ= Ġcheck Errors (""" ĊĠĠĠ Ġmodule Ġ 0 x 1 :: M Ġ{ ĊĠĠĠĠĠĠĠ Ġstruct ĠS Ġ{} ĊĠĠĠĠĠĠĠ Ġfun Ġm ( s : Ġ& S , Ġs _ mut : Ġ& mut ĠS ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ( if Ġ( cond ) Ġs _ mut Ġelse Ġs ); ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĠĠĠĠĊĠĠĠ Ġ"" ") Ċ } Ċ