From b2720c8939044bdbc3c9773fd05cf8a0c2c5ab4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Sat, 7 Sep 2024 13:01:23 +0200 Subject: [PATCH] Typos and minor lemma clean-up (#2611) * cleanup * lemmas --- .../src/kevm_pyk/kproj/evm-semantics/evm-types.md | 12 ++++++------ kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 10 +++++----- .../kevm_pyk/kproj/evm-semantics/serialization.md | 6 +++--- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 222a511ab0..9c1efd77d1 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -38,8 +38,8 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to EVM's rule word2Bool( W ) => true requires W =/=Int 0 ``` -- `sgn` gives the twos-complement interperetation of the sign of a word. -- `abs` gives the twos-complement interperetation of the magnitude of a word. +- `sgn` gives the twos-complement interpretation of the sign of a word. +- `abs` gives the twos-complement interpretation of the magnitude of a word. ```k syntax Int ::= sgn ( Int ) [symbol(sgn), function, total] @@ -114,7 +114,7 @@ The helper `powmod` is a totalization of the operator `_^%Int__` (which comes wi rule [powmod.zero]: powmod( _, _, W2) => 0 requires W2 ==Int 0 [concrete] ``` -`/sWord` and `%sWord` give the signed interperetations of `/Word` and `%Word`. +`/sWord` and `%sWord` give the signed interpretations of `/Word` and `%Word`. ```k syntax Int ::= Int "/sWord" Int [function] @@ -144,7 +144,7 @@ The `Word` comparisons similarly lift K operators to EVM ones: rule W0 ==Word W1 => bool2Word(W0 ==Int W1) ``` -- `s #exec [ SO:StackOp ] => #gas [ SO , SO WS ] ~> SO WS ... WS ``` -The `CallOp` opcodes all interperet their second argument as an address. +The `CallOp` opcodes all interpret their second argument as an address. ```k syntax InternalOp ::= CallSixOp Int Int Int Int Int Int @@ -2344,13 +2344,13 @@ EVM Program Representations EVM programs are represented algebraically in K, but programs can load and manipulate program data directly. The opcodes `CODECOPY` and `EXTCODECOPY` rely on the assembled form of the programs being present. -The opcode `CREATE` relies on being able to interperet EVM data as a program. +The opcode `CREATE` relies on being able to interpret EVM data as a program. This is a program representation dependence, which we might want to avoid. Perhaps the only program representation dependence we should have is the hash of the program; doing so achieves: -- Program representation independence (different analysis tools on the language don't have to ensure they have a common representation of programs, just a common interperetation of the data-files holding programs). -- Programming language independence (we wouldn't even have to commit to a particular language or interperetation of the data-file). +- Program representation independence (different analysis tools on the language don't have to ensure they have a common representation of programs, just a common interpretation of the data-files holding programs). +- Programming language independence (we wouldn't even have to commit to a particular language or interpretation of the data-file). - Only depending on the hash allows us to know that we have *exactly* the correct data-file (program), and nothing more. Disassembler @@ -2358,7 +2358,7 @@ Disassembler After interpreting the strings representing programs as a `WordStack`, it should be changed into an `OpCodes` for use by the EVM semantics. -- `#dasmOpCode` interperets a `Int` as an `OpCode`. +- `#dasmOpCode` interprets a `Int` as an `OpCode`. ```k syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [symbol(#dasmOpCode), function, memo, total] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index 24fe46ea72..13a582cb6c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -149,7 +149,7 @@ Here we provide some standard parser/unparser functions for that format. Parsing ------- -These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s. +These parsers can interpret hex-encoded strings as `Int`s, `Bytes`s, and `Map`s. - `#parseHexWord` interprets a string as a single hex-encoded `Word`. - `#parseHexBytes` interprets a string as a hex-encoded stack of bytes. @@ -207,7 +207,7 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s Unparsing --------- -- `#padByte` ensures that the `String` interperetation of a `Int` is wide enough. +- `#padByte` ensures that the `String` interpretation of a `Int` is wide enough. ```k syntax String ::= #padByte ( String ) [symbol(#padByte), function] @@ -396,7 +396,7 @@ Decoding -------- - `#rlpDecode` RLP decodes a single `Bytes` into a `JSON`. -- `#rlpDecodeList` RLP decodes a single `Bytes` into a `JSONs`, interpereting the input as the RLP encoding of a list. +- `#rlpDecodeList` RLP decodes a single `Bytes` into a `JSONs`, interpreting the input as the RLP encoding of a list. ```k syntax JSON ::= #rlpDecode ( Bytes ) [symbol(#rlpDecode ), function]