diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 70499927c5..d5b3b47d8b 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.427" +version = "1.0.428" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 8d42964387..92f6caef04 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.427' +VERSION: Final = '1.0.428' diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index b097960374..f15220344b 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -419,6 +419,18 @@ def abi_tuple(values: list[KInner]) -> KApply: def abi_array(elem_type: KInner, length: KInner, elems: list[KInner]) -> KApply: return KApply('abi_type_array', [elem_type, length, KEVM.typed_args(elems)]) + @staticmethod + def abi_dynamic_array(elem_type: KInner) -> KApply: + return KApply('abi_type_dynamic_array', [elem_type]) + + # @staticmethod + # def abi_dynamic_bytes_array(elem_type: KInner) -> KApply: + # return KApply('abi_type_dynamic_bytes_array', [elem_type]) + + @staticmethod + def abi_bytes_array(length: KInner, elems_size: KInner, elems: list[KInner]) -> KApply: + return KApply('abi_type_bytes_array', [length, elems_size, KEVM.typed_args(elems)]) + @staticmethod def empty_typedargs() -> KApply: return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs') diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md index 64377daffe..9995514e74 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md @@ -132,11 +132,16 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of | #bytes ( Bytes ) [klabel(abi_type_bytes), symbol] | #string ( String ) [klabel(abi_type_string), symbol] | #array ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array), symbol] + | #dynArray( TypedArg ) [klabel(abi_type_dynamic_array), symbol] + | #bytesArray ( Int , Int , TypedArgs ) [klabel(abi_type_bytes_array), symbol] | #tuple ( TypedArgs ) [klabel(abi_type_tuple), symbol] // ---------------------------------------------------------------------------------------------- syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)] - // ------------------------------------------------------------ + syntax TypedArgs ::= "concat" "(" TypedArgs "," TypedArgs ")" [function, total] + // ------------------------------------------------------------------------------- + rule concat(.TypedArgs, TA) => TA + rule concat((A, TA:TypedArgs), TB) => concat(TA, (A, TB)) syntax Bytes ::= #abiCallData ( String , TypedArgs ) [function] // --------------------------------------------------------------- @@ -266,13 +271,17 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #typeName( #array(T, _, _)) => #typeName(T) +String "[]" - rule #typeName( #tuple(TARGS)) => "(" +String #generateSignatureArgs(TARGS) +String ")" + rule #typeName( #dynArray( T )) => #typeName(T) +String "[]" + + rule #typeName( #tuple( ARGS )) => "(" +String #generateSignatureArgs(ARGS) +String ")" + + rule #typeName( #bytesArray( _, _, _ )) => "bytes[]" syntax Bytes ::= #encodeArgs ( TypedArgs ) [function] syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [function] // ------------------------------------------------------------------------------ rule #encodeArgs(ARGS) => #encodeArgsAux(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes) - rule #encodeArgs(#tuple(ARGS)) => #encodeArgs(ARGS) + rule #encodeArgsAux(.TypedArgs, _:Int, HEADS, TAILS) => HEADS +Bytes TAILS rule #encodeArgsAux((ARG, ARGS), OFFSET, HEADS, TAILS) @@ -283,6 +292,11 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of => #encodeArgsAux(ARGS, OFFSET +Int #sizeOfDynamicType(ARG), HEADS +Bytes #enc(#uint256(OFFSET)), TAILS +Bytes #enc(ARG)) requires notBool(#isStaticType(ARG)) + syntax Bool ::= #isTuple (TypedArg) [function, total] + // ----------------------------------------------------- + rule #isTuple(#tuple(_)) => true + rule #isTuple(_) => false + syntax Int ::= #lenOfHeads ( TypedArgs ) [function, total] // ---------------------------------------------------------- rule #lenOfHeads(.TypedArgs) => 0 @@ -397,8 +411,14 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #lenOfHead( #string( _ )) => 32 + rule #lenOfHead( #tuple( ARGS )) => #lenOfHeads(ARGS) requires #isStaticType(#tuple(ARGS)) + rule #lenOfHead( #tuple( ARGS )) => 32 requires notBool #isStaticType(#tuple(ARGS)) + rule #lenOfHead(#array(_, _, _)) => 32 + rule #lenOfHead(#dynArray( _ )) => 32 + rule #lenOfHead(#bytesArray( _, _, _ )) => 32 + syntax Bool ::= #isStaticType ( TypedArg ) [function, total] // ------------------------------------------------------------ rule #isStaticType( #address( _ )) => true @@ -510,21 +530,44 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #isStaticType(#array(_, _, _)) => false + rule #isStaticType(#dynArray( _ )) => false + + rule #isStaticType(#tuple( ARGS )) => notBool #hasDynamicType(ARGS) + + rule #isStaticType(#bytesArray( _ , _ , _)) => false + + syntax Bool ::= #hasDynamicType(TypedArgs) [function, total] + // ------------------------------------------------------------ + rule #hasDynamicType(.TypedArgs) => false + rule #hasDynamicType(T, TS ) => #hasDynamicType(TS) requires #isStaticType(T) + rule #hasDynamicType(T, _ ) => true requires notBool #isStaticType(T) + syntax Int ::= #sizeOfDynamicType ( TypedArg ) [function] // --------------------------------------------------------- rule #sizeOfDynamicType(#bytes(BS)) => 32 +Int #ceil32(lengthBytes(BS)) + rule #sizeOfDynamicType(#tuple(ARGS)) => 32 +Int #sizeOfDynamicTypeAux(ARGS) + rule #sizeOfDynamicType(#array(T, N, _)) => 32 *Int (1 +Int N) requires #isStaticType(T) rule #sizeOfDynamicType(#array(T, N, ELEMS)) => 32 *Int (1 +Int N +Int #sizeOfDynamicTypeAux(ELEMS)) requires notBool #isStaticType(T) - syntax Int ::= #sizeOfDynamicTypeAux ( TypedArgs ) [function] - // ------------------------------------------------------------- + // TODO(palina): placeholder rule for dynamic arrays + rule #sizeOfDynamicType(#dynArray(T)) => 32 *Int (1 +Int #sizeOfDynamicType(T)) + requires notBool #isStaticType(T) + + rule #sizeOfDynamicType(#bytesArray(N, L, _)) => 32 +Int N *Int (64 +Int #ceil32(L)) + + syntax Int ::= #sizeOfDynamicTypeAux ( TypedArgs ) [function, total] + // -------------------------------------------------------------------- rule #sizeOfDynamicTypeAux(TARG, TARGS) => #sizeOfDynamicType(TARG) +Int #sizeOfDynamicTypeAux(TARGS) requires notBool #isStaticType(TARG) + rule #sizeOfDynamicTypeAux(TARG, TARGS) => #lenOfHead(TARG) +Int #sizeOfDynamicTypeAux(TARGS) + requires #isStaticType(TARG) + rule #sizeOfDynamicTypeAux(.TypedArgs) => 0 syntax Bytes ::= #enc ( TypedArg ) [function] @@ -632,15 +675,37 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #enc( #bytes32( DATA )) => #bufStrict(32, #getValue(#bytes32( DATA ))) rule #enc( #bool( DATA )) => #bufStrict(32, #getValue( #bool( DATA ))) + rule #enc( #tuple( DATA )) => #encodeArgs(DATA) // dynamic Type rule #enc( #bytes(BS)) => #encBytes(lengthBytes(BS), BS) + // length of `bytes` variable is <= 1 Gb + ensures lengthBytes(BS) <=Int 1073741824 + rule #enc(#array(_, N, DATA)) => #enc(#uint256(N)) +Bytes #encodeArgs(DATA) rule #enc( #string(STR)) => #enc(#bytes(String2Bytes(STR))) + rule #enc(#bytesArray(N, L, DATA)) => #enc(#uint256(N)) +Bytes #encodeArgsBytes(DATA, L) + + // TODO: placeholder rule for dynamic arrays + rule #enc(#dynArray(T)) => #enc(T) syntax Bytes ::= #encBytes ( Int , Bytes ) [function] // ----------------------------------------------------- rule #encBytes(N, BS) => #enc(#uint256(N)) +Bytes BS +Bytes #bufStrict(#ceil32(N) -Int N, 0) + + // Auxilliary bytes encoding functions (for elements of `bytes[]`): + syntax Bytes ::= #encBytes ( Int , TypedArg ) [function] + syntax Bytes ::= #encodeArgsBytes( TypedArgs, Int ) [function] + syntax Bytes ::= #encodeArgsAuxBytes ( TypedArgs , Int , Bytes , Bytes, Int ) [function] + // ----------------------------------------------------- + rule #encBytes(N, #bytes(BS)) => #enc(#uint256(N)) +Bytes BS +Bytes #bufStrict(#ceil32(N) -Int N, 0) + ensures lengthBytes(BS) ==Int N + + rule #encodeArgsBytes(ARGS, N) => #encodeArgsAuxBytes(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes, N) + rule #encodeArgsAuxBytes(.TypedArgs, _:Int, HEADS, TAILS, _) => HEADS +Bytes TAILS + + rule #encodeArgsAuxBytes((ARG, ARGS), OFFSET, HEADS, TAILS, N) + => #encodeArgsAuxBytes(ARGS, OFFSET +Int #sizeOfDynamicType(ARG), HEADS +Bytes #enc(#uint256(OFFSET)), TAILS +Bytes #encBytes(N, ARG), N) ``` ```k diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md index 0018734e51..b1c4f7aade 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md @@ -27,7 +27,7 @@ Claims should always use `#bufStrict` in LHS and `#buf` in RHS. syntax Int ::= #ceil32 ( Int ) [macro] // -------------------------------------- - rule #ceil32(N) => (N up/Int 32) *Int 32 + rule #ceil32(N) => notMaxUInt5 &Int ( N +Int maxUInt5 ) endmodule diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index d94e571521..c646d0a31f 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -748,10 +748,23 @@ These are just used by the other operators for shuffling local execution state a ```k syntax InternalOp ::= "#newAccount" Int | "#newExistingAccount" Int - | "#newFreshAccount" Int // -------------------------------------------- rule #newAccount ACCT => #newExistingAccount ACCT ... ACCT ... - rule #newAccount ACCT => #newFreshAccount ACCT ... [owise] + rule #newAccount ACCT => . ... + + ( .Bag + => + + ACCT + 0 + .Bytes:AccountCode + .Map + .Map + 0 + + ) + ... + [owise, preserves-definedness] rule #newExistingAccount ACCT => #end EVMC_ACCOUNT_ALREADY_EXISTS ... @@ -772,17 +785,6 @@ These are just used by the other operators for shuffling local execution state a ... requires lengthBytes(CODE) ==Int 0 - - rule #newFreshAccount ACCT => . ... - - ( .Bag - => - ACCT - ... - - ) - ... - ``` - `#transferFunds` moves money from one account into another, creating the destination account if it doesn't exist. @@ -811,6 +813,7 @@ These are just used by the other operators for shuffling local execution state a ... requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM + [preserves-definedness] rule #transferFunds ACCTFROM _ACCTTO VALUE => #end EVMC_BALANCE_UNDERFLOW ... diff --git a/package/version b/package/version index e5d8b12201..de5c9be307 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.427 +1.0.428 diff --git a/tests/specs/summarization/summarization-spec.k b/tests/specs/summarization/summarization-spec.k new file mode 100644 index 0000000000..43e16e37c2 --- /dev/null +++ b/tests/specs/summarization/summarization-spec.k @@ -0,0 +1,179 @@ +requires "verification.k" + +module SUMMARIZATION-SPEC + imports VERIFICATION + + claim [program-01]: + + runLemma ( + #range(PROGRAM, PCOUNT, 25) ==K b"`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a" + andBool + #range(PROGRAM, PCOUNT +Int 27, 20) ==K b"\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a" + andBool + #range(PROGRAM, PCOUNT +Int 49, 7) ==K b"\x83\x88\x01\x01R[P" + andBool + #asWord ( #range( PROGRAM, PCOUNT +Int 25, 2 ) ) ==Int #asWord ( #range( PROGRAM, PCOUNT +Int 47, 2 ) ) + ) => + doneLemma ( true ) + + PROGRAM + PCOUNT + requires + PROGRAM ==K b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00AW`\x005`\xe0\x1c\x80c\n\x92T\xe4\x14a\x00FW\x80c\x92\xf8<\x90\x14a\x00PW\x80c\xa1\x02\xc4%\x14a\x00cW[`\x00\x80\xfd[a\x00Na\x00vV[\x00[a\x00Na\x00^6`\x04a\x036V[a\x00\xc1V[a\x00Na\x00q6`\x04a\x036V[a\x012V[`@Qa\x00\x82\x90a\x029V[`@Q\x80\x91\x03\x90`\x00\xf0\x80\x15\x80\x15a\x00\x9eW=`\x00\x80>=`\x00\xfd[P`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90UV[`\x00T`@QcHpIo`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x90cHpIo\x90a\x00\xf9\x90\x88\x90\x88\x90\x88\x90\x88\x90\x88\x90`\x04\x01a\x057V[`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x01\x13W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x01'W=`\x00\x80>=`\x00\xfd[PPPPPPPPPV[`\x00\x80T`@\x80Qc\x84V\xcbY`\xe0\x1b\x81R\x90Q`\x01`\x01`\xa0\x1b\x03\x90\x92\x16\x92c\x84V\xcbY\x92`\x04\x80\x84\x01\x93\x82\x90\x03\x01\x81\x83\x87\x80;\x15\x80\x15a\x01sW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x01\x87W=`\x00\x80>=`\x00\xfd[PPPP\x7f\x88\\\xb6\x92@\xa95\xd62\xd7\x9c1q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-`\x00\x1c`\x01`\x01`\xa0\x1b\x03\x16c\xf4\x84H\x14`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x01\xe9W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x01\xfdW=`\x00\x80>=`\x00\xfd[PP`\x00T`@QcHpIo`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x92PcHpIo\x91Pa\x00\xf9\x90\x88\x90\x88\x90\x88\x90\x88\x90\x88\x90`\x04\x01a\x057V[a\x03E\x80a\x062\x839\x01\x90V[cNH{q`\xe0\x1b`\x00R`A`\x04R`$`\x00\xfd[`@Q`\xc0\x81\x01g\xff\xff\xff\xff\xff\xff\xff\xff\x81\x11\x82\x82\x10\x17\x15a\x02\x7fWa\x02\x7fa\x02FV[`@R\x90V[`@Q`\x1f\x82\x01`\x1f\x19\x16\x81\x01g\xff\xff\xff\xff\xff\xff\xff\xff\x81\x11\x82\x82\x10\x17\x15a\x02\xaeWa\x02\xaea\x02FV[`@R\x91\x90PV[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x02\xcdW`\x00\x80\xfd[\x91\x90PV[`\x00`\x80\x82\x84\x03\x12\x15a\x02\xe4W`\x00\x80\xfd[P\x91\x90PV[`\x00\x80\x83`\x1f\x84\x01\x12a\x02\xfcW`\x00\x80\xfd[P\x815g\xff\xff\xff\xff\xff\xff\xff\xff\x81\x11\x15a\x03\x14W`\x00\x80\xfd[` \x83\x01\x91P\x83` \x82`\x05\x1b\x85\x01\x01\x11\x15a\x03/W`\x00\x80\xfd[\x92P\x92\x90PV[`\x00\x80`\x00\x80`\x00`\xe0\x86\x88\x03\x12\x15a\x03NW`\x00\x80\xfd[\x855g\xff\xff\xff\xff\xff\xff\xff\xff\x80\x82\x11\x15a\x03fW`\x00\x80\xfd[\x90\x87\x01\x90`\xc0\x82\x8a\x03\x12\x15a\x03zW`\x00\x80\xfd[a\x03\x82a\x02\\V[\x825\x81R` a\x03\x93\x81\x85\x01a\x02\xb6V[\x81\x83\x01Ra\x03\xa3`@\x85\x01a\x02\xb6V[`@\x83\x01R``\x84\x015``\x83\x01R`\x80\x84\x015`\x80\x83\x01R`\xa0\x84\x015\x83\x81\x11\x15a\x03\xceW`\x00\x80\xfd[\x80\x85\x01\x94PP\x8a`\x1f\x85\x01\x12a\x03\xe3W`\x00\x80\xfd[\x835\x83\x81\x11\x15a\x03\xf5Wa\x03\xf5a\x02FV[a\x04\x07`\x1f\x82\x01`\x1f\x19\x16\x83\x01a\x02\x85V[\x81\x81R\x8c\x83\x83\x88\x01\x01\x11\x15a\x04\x1bW`\x00\x80\xfd[\x81\x83\x87\x01\x84\x83\x017`\x00\x91\x81\x01\x83\x01\x91\x90\x91R`\xa0\x83\x01R\x90\x97P\x88\x015\x95Pa\x04H\x89`@\x8a\x01a\x02\xd2V[\x94P`\xc0\x88\x015\x91P\x80\x82\x11\x15a\x04^W`\x00\x80\xfd[Pa\x04k\x88\x82\x89\x01a\x02\xeaV[\x96\x99\x95\x98P\x93\x96P\x92\x94\x93\x92PPPV[\x81\x83R\x81\x81` \x85\x017P`\x00\x82\x82\x01` \x90\x81\x01\x91\x90\x91R`\x1f\x90\x91\x01`\x1f\x19\x16\x90\x91\x01\x01\x90V[\x81\x83R`\x00` \x80\x85\x01\x80\x81\x96P\x85`\x05\x1b\x81\x01\x91P\x84`\x00[\x87\x81\x10\x15a\x05*W\x82\x84\x03\x89R\x815`\x1e\x19\x886\x03\x01\x81\x12a\x04\xe0W`\x00\x80\xfd[\x87\x01\x85\x81\x01\x905g\xff\xff\xff\xff\xff\xff\xff\xff\x81\x11\x15a\x04\xfcW`\x00\x80\xfd[\x806\x03\x82\x13\x15a\x05\x0bW`\x00\x80\xfd[a\x05\x16\x86\x82\x84a\x04|V[\x9a\x87\x01\x9a\x95PPP\x90\x84\x01\x90`\x01\x01a\x04\xbfV[P\x91\x97\x96PPPPPPPV[`\xe0\x80\x82R\x86Q\x90\x82\x01R` \x80\x87\x01Q`\x01`\x01`\xa0\x1b\x03\x90\x81\x16a\x01\x00\x84\x01R`@\x88\x01Q\x16a\x01 \x83\x01R``\x87\x01Qa\x01@\x83\x01R`\x80\x87\x01Qa\x01`\x83\x01R`\xa0\x87\x01Q`\xc0a\x01\x80\x84\x01R\x80Qa\x01\xa0\x84\x01\x81\x90R`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a\x01\xc0\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a\x01\xc0\x83\x88\x01\x01R[P\x82\x85\x01\x89\x90R`\x1f\x01`\x1f\x19\x16\x84\x01\x90Pa\x01\xc0a\x06\f`@\x86\x01\x89\x805\x82R` \x81\x015` \x83\x01R`@\x81\x015`@\x83\x01R``\x81\x015``\x83\x01RPPV[\x80\x85\x83\x03\x01`\xc0\x86\x01Ra\x06#\x81\x83\x01\x87\x89a\x04\xa5V[\x9a\x99PPPPPPPPPPV\xfe`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[Pa\x03%\x80a\x00 `\x009`\x00\xf3\xfe`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x006W`\x005`\xe0\x1c\x80cHpIo\x14a\x00;W\x80c\x84V\xcbY\x14a\x00PW[`\x00\x80\xfd[a\x00Na\x00I6`\x04a\x01\xa9V[a\x00bV[\x00[a\x00N`\x00\x80T`\xff\x19\x16`\x01\x17\x90UV[`\x00T`\xff\x16\x15a\x00\xb2W`@QbF\x1b\xcd`\xe5\x1b\x81R` `\x04\x82\x01R`\x16`$\x82\x01Ru\x13\xdc\x1d\x1a[Z\\\xdbT\x1b\xdc\x9d\x18[\x0e\x88\x1c\x18]\\\xd9Y`R\x1b`D\x82\x01R`d\x01`@Q\x80\x91\x03\x90\xfd[PPPPPV[cNH{q`\xe0\x1b`\x00R`A`\x04R`$`\x00\xfd[`@Q`\xc0\x81\x01g\xff\xff\xff\xff\xff\xff\xff\xff\x81\x11\x82\x82\x10\x17\x15a\x00\xf2Wa\x00\xf2a\x00\xb9V[`@R\x90V[`@Q`\x1f\x82\x01`\x1f\x19\x16\x81\x01g\xff\xff\xff\xff\xff\xff\xff\xff\x81\x11\x82\x82\x10\x17\x15a\x01!Wa\x01!a\x00\xb9V[`@R\x91\x90PV[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01@W`\x00\x80\xfd[\x91\x90PV[`\x00`\x80\x82\x84\x03\x12\x15a\x01WW`\x00\x80\xfd[P\x91\x90PV[`\x00\x80\x83`\x1f\x84\x01\x12a\x01oW`\x00\x80\xfd[P\x815g\xff\xff\xff\xff\xff\xff\xff\xff\x81\x11\x15a\x01\x87W`\x00\x80\xfd[` \x83\x01\x91P\x83` \x82`\x05\x1b\x85\x01\x01\x11\x15a\x01\xa2W`\x00\x80\xfd[\x92P\x92\x90PV[`\x00\x80`\x00\x80`\x00`\xe0\x86\x88\x03\x12\x15a\x01\xc1W`\x00\x80\xfd[\x855g\xff\xff\xff\xff\xff\xff\xff\xff\x80\x82\x11\x15a\x01\xd9W`\x00\x80\xfd[\x90\x87\x01\x90`\xc0\x82\x8a\x03\x12\x15a\x01\xedW`\x00\x80\xfd[a\x01\xf5a\x00\xcfV[\x825\x81R` a\x02\x06\x81\x85\x01a\x01)V[\x81\x83\x01Ra\x02\x16`@\x85\x01a\x01)V[`@\x83\x01R``\x84\x015``\x83\x01R`\x80\x84\x015`\x80\x83\x01R`\xa0\x84\x015\x83\x81\x11\x15a\x02AW`\x00\x80\xfd[\x80\x85\x01\x94PP\x8a`\x1f\x85\x01\x12a\x02VW`\x00\x80\xfd[\x835\x83\x81\x11\x15a\x02hWa\x02ha\x00\xb9V[a\x02z`\x1f\x82\x01`\x1f\x19\x16\x83\x01a\x00\xf8V[\x81\x81R\x8c\x83\x83\x88\x01\x01\x11\x15a\x02\x8eW`\x00\x80\xfd[\x81\x83\x87\x01\x84\x83\x017`\x00\x91\x81\x01\x83\x01\x91\x90\x91R`\xa0\x83\x01R\x90\x97P\x88\x015\x95Pa\x02\xbb\x89`@\x8a\x01a\x01EV[\x94P`\xc0\x88\x015\x91P\x80\x82\x11\x15a\x02\xd1W`\x00\x80\xfd[Pa\x02\xde\x88\x82\x89\x01a\x01]V[\x96\x99\x95\x98P\x93\x96P\x92\x94\x93\x92PPPV\xfe\xa2dipfsX\"\x12 \xdc'\xd1\x9b\x8dS\xe0\xa2O\x86k\x19\xa4\x9f\xd1\xa3\x12_\xfb\x0e\x17\xcbDk}\xd6\xc7\x9a\xc5\x9f\xfb\x8bdsolcC\x00\x08\x0f\x003\xa2dipfsX\"\x12 \xb0<\xc1\x9e\xa1U(<)%|.w\xe8\x8c\xa2\x85\xe8y\xc9T\xebI\xf9\x1b\xc2\x91\xd6,\xc58\xeedsolcC\x00\x08\x0f\x003" + andBool + PCOUNT ==Int 1427 + + claim [bytes-indexing-via-range]: + runLemma ( PROGRAM [ PCOUNT ] ==K 96) => doneLemma ( true ) ... + requires #range(PROGRAM, PCOUNT, 25) ==K b"`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a" + andBool #range(PROGRAM, PCOUNT +Int 27, 20) ==K b"\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a" + andBool #range(PROGRAM, PCOUNT +Int 49, 7) ==K b"\x83\x88\x01\x01R[P" + andBool OFFSET:Int ==Int #asWord ( #range( PROGRAM, PCOUNT +Int 25, 2 ) ) + andBool OFFSET:Int ==Int #asWord ( #range( PROGRAM, PCOUNT +Int 47, 2 ) ) + andBool PCOUNT <=Int lengthBytes(PROGRAM) + + claim [bytes-indexing-via-concat]: + runLemma ( PROGRAM [ PCOUNT ] ==Int 96 ) => doneLemma ( true ) ... + requires PROGRAM ==K PROG_PRE +Bytes b"`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a" +Bytes + OFFSET_BYTES +Bytes b"\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a" +Bytes OFFSET_BYTES +Bytes + b"\x83\x88\x01\x01R[P" +Bytes _PROG_POST + andBool lengthBytes(PROG_PRE) ==Int PCOUNT + andBool lengthBytes(OFFSET_BYTES) ==Int 2 + andBool PCOUNT <=Int lengthBytes(PROGRAM) + + claim [bytes-data-provable]: + #execute ... + SHANGHAI + JUMPDESTS + false + _GC + + PROG_PRE +Bytes + b"`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a" +Bytes + OFFSET_BYTES +Bytes + b"\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a" +Bytes + OFFSET_BYTES +Bytes + b"\x83\x88\x01\x01R[P" +Bytes + _PROG_POST + + PCOUNT => PCOUNT +Int 56 + LENGTH : SRC : 32 : DEST : WS => LENGTH : SRC : 32 : 0 : DEST : WS + + LM => LM [ DEST +Int OFFSET := #range ( LM, SRC +Int 32, LENGTH ) +Bytes + #buf ( ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) , 0 ) +Bytes + #buf ( ( ( ( 32 -Int ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) ) ) modInt 32 ), 0 ) ] + + requires 0 <=Int PCOUNT + andBool 0 <=Int LENGTH andBool LENGTH + runLemma ( #range(P, 0, 12) +Bytes #buf(2, 1462) +Bytes #range(P, 14, 11) +Bytes #buf(2, 448) +Bytes + #range(P, 27, 5) +Bytes #buf(2, 1433) +Bytes #range(P, 34, 7) +Bytes #buf(2, 1481) +Bytes + #range(P, 43, 4) +Bytes #buf(2, 448) +Bytes #range(P, 49, 7) ==K P ) => doneLemma ( true ) + + requires P ==K b"`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a\x01\xc0\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a\x01\xc0\x83\x88\x01\x01R[P" + + claim [bytes-data-provable-gen-pcount]: + #execute ... + SHANGHAI + JUMPDESTS + false + _GC + + PROG_PRE +Bytes + #range(OP, 0, 12) +Bytes #buf(2, PCOUNT +Int 35) +Bytes #range(OP, 14, 11) +Bytes OFFSET_BYTES +Bytes + #range(OP, 27, 5) +Bytes #buf(2, PCOUNT +Int 6) +Bytes #range(OP, 34, 7) +Bytes #buf(2, PCOUNT +Int 54) +Bytes + #range(OP, 43, 4) +Bytes OFFSET_BYTES +Bytes #range(OP, 49, 7) +Bytes + _PROG_POST + + PCOUNT => PCOUNT +Int 56 + LENGTH : SRC : 32 : DEST : WS => LENGTH : SRC : 32 : 0 : DEST : WS + + LM => LM [ DEST +Int OFFSET := #range ( LM, SRC +Int 32, LENGTH ) +Bytes + #buf ( ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) , 0 ) +Bytes + #buf ( ( ( ( 32 -Int ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) ) ) modInt 32 ), 0 ) ] + + requires OP ==K b"`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a\x01\xc0\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a\x01\xc0\x83\x88\x01\x01R[P" + andBool 0 <=Int PCOUNT + andBool 0 <=Int LENGTH andBool LENGTH #execute ... + false + SHANGHAI + JUMPDESTS + PROG_PRE +Bytes CP +Bytes _PROG_POST + PCOUNT => PCOUNT +Int 56 + LENGTH : SRC : 32 : DEST : WS => LENGTH : SRC : 32 : 0 : DEST : WS + + LM => LM [ DEST +Int OFFSET := #range ( LM, SRC +Int 32, LENGTH ) +Bytes + #buf ( ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) , 0 ) +Bytes + #buf ( ( ( ( 32 -Int ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) ) ) modInt 32 ), 0 ) ] + + requires OP ==K b"`\x00\x92\x91\x90\x83[\x81\x81\x10\x15a\x05\xb6W\x82\x81\x01\x84\x01Q\x86\x82\x01a\x01\xc0\x01R\x83\x01a\x05\x99V[\x81\x81\x11\x15a\x05\xc9W`\x00a\x01\xc0\x83\x88\x01\x01R[P" + andBool lengthBytes(PROG_PRE) ==Int PCOUNT + andBool lengthBytes(OFFSET_BYTES) ==K 2 + andBool OFFSET ==Int #asWord ( OFFSET_BYTES ) + + andBool CP ==K OP + [ 12 := #buf(2, PCOUNT +Int 35) ] + [ 25 := OFFSET_BYTES ] + [ 32 := #buf(2, PCOUNT +Int 6) ] + [ 41 := #buf(2, PCOUNT +Int 54) ] + [ 47 := OFFSET_BYTES ] + + andBool 0 <=Int PCOUNT + andBool 0 <=Int LENGTH andBool LENGTH doneLemma( T ) + + // Some additional lemmas + // ---------------------- + + syntax Int ::= "maxBytesLength" [alias] + rule maxBytesLength => 9223372036854775808 + + rule B:Bytes [ X:Int ] => #asWord ( #range (B, X, 1) ) + requires X <=Int lengthBytes(B) + [simplification(40)] + + rule B:Bytes [ START:Int := b"" ] => B + requires 0 <=Int START andBool START <=Int lengthBytes(B) + [simplification] + + // Conversion from bytes always yields a non-negative integer + rule 0 <=Int #asWord ( _ ) => true [simplification] + + // Piecemeal non-negativity + rule X <=Int A +Int B => true + requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B + [simplification, concrete(X)] + + // Consecutive quasi-contiguous memory update + rule B [ S1 := B1 ] [ S2 := B2 ] => B [ S1 := #range(B1, 0, S2 -Int S1) +Bytes B2 ] + requires 0 <=Int S1 andBool S1 <=Int S2 andBool S2 <=Int S1 +Int lengthBytes(B1) + [simplification] + + // Parameter equality: byte-array update + rule { B1:Bytes [ S1:Int := B2:Bytes ] #Equals B3:Bytes [ S2:Int := B4:Bytes ] } => #Top + requires B1 ==K B3 andBool S1 ==Int S2 andBool B2 ==K B4 + [simplification] + +endmodule