diff --git a/flake.nix b/flake.nix index a2c55c35f4..b04bcefcb6 100644 --- a/flake.nix +++ b/flake.nix @@ -66,7 +66,7 @@ "result*" "*.nix" "kevm-pyk/" - # do not include submodule directories that might be initilized empty or non-existent + # do not include submodule directories that might be initialized empty or non-existent "/deps/" "/tests/ethereum-tests" "/web/k-web-theme" @@ -137,7 +137,7 @@ projectDir = prev.lib.cleanSource ( prev.nix-gitignore.gitignoreSourcePure [ ./.gitignore - # do not include submodule directories that might be initilized empty or non-existent + # do not include submodule directories that might be initialized empty or non-existent "/src/kevm_pyk/kproj/plugin" ] ./kevm-pyk/. ); @@ -276,7 +276,7 @@ "result*" "*.nix" "kevm-pyk/" - # do not include submodule directories that might be initilized empty or non-existent + # do not include submodule directories that might be initialized empty or non-existent "/deps/" "/tests/ethereum-tests" "/web/k-web-theme" diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py index 345fb4fbf2..7b9af7a55c 100644 --- a/kevm-pyk/src/kevm_pyk/summarizer.py +++ b/kevm-pyk/src/kevm_pyk/summarizer.py @@ -583,7 +583,7 @@ class KEVMSummarizer: """ A class for summarizing the instructions of the KEVM. - 1. `build_spec` builds the proof to symbolically execute one abitrary opcode. + 1. `build_spec` builds the proof to symbolically execute one arbitrary opcode. 2. `explore` runs the proof to get the KCFG. 3. `summarize` minimizes the KCFG to get the summarized rules for opcodes. """ @@ -599,7 +599,7 @@ def __init__(self, proof_dir: Path, save_directory: Path) -> None: self.save_directory = save_directory def build_stack_underflow_spec(self) -> APRProof | None: - """Build the specification to symbolically execute abitrary instruction with stack underflow.""" + """Build the specification to symbolically execute arbitrary instruction with stack underflow.""" ... def show_proof( diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 2ee628b92e..61e8d1de3b 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -159,7 +159,7 @@ def target_dir(kompiled_targets_dir: Path | None, tmp_path_factory: TempPathFact @pytest.fixture(scope='module') def kompiled_target_for(target_dir: Path) -> Callable[[Path], Path]: """ - Generate a function that returns a path to the kompiled defintion for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec. + Generate a function that returns a path to the kompiled definition for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec. """ def kompile(spec_file: Path) -> Path: @@ -263,7 +263,7 @@ def test_kompile_targets( """ This test function is intended to be used to pre-kompile all definitions, so that the actual proof tests do not need to do the actual compilation, - which is disturbing performance measurment. + which is disturbing performance measurement. To achieve the desired caching, this test should be run like this: pytest src/tests/integration/test_prove.py::test_kompile_targets --kompiled-targets-dir ./prekompiled diff --git a/media/201710-presentation-devcon3.md b/media/201710-presentation-devcon3.md index d4353c2ea9..c17360eb50 100644 --- a/media/201710-presentation-devcon3.md +++ b/media/201710-presentation-devcon3.md @@ -444,7 +444,7 @@ head: andBool G >=Int 52 *Int I +Int 21 ``` -Verifing ABI compliant contracts +Verifying ABI compliant contracts -------------------------------- . . . diff --git a/tests/specs/examples/ERC721.sol b/tests/specs/examples/ERC721.sol index d3ec55f9d1..54bcdae798 100644 --- a/tests/specs/examples/ERC721.sol +++ b/tests/specs/examples/ERC721.sol @@ -635,7 +635,7 @@ contract ERC721 is Context, ERC165, IERC721, IERC721Metadata { /** * @dev Base URI for computing {tokenURI}. If set, the resulting URI for each * token will be the concatenation of the `baseURI` and the `tokenId`. Empty - * by default, can be overriden in child contracts. + * by default, can be overridden in child contracts. */ function _baseURI() internal view virtual returns (string memory) { return ""; diff --git a/tests/specs/examples/README.md b/tests/specs/examples/README.md index aafc5986b5..c9d0eb572e 100644 --- a/tests/specs/examples/README.md +++ b/tests/specs/examples/README.md @@ -45,8 +45,8 @@ For `kevm prove`, you can use `kevm show-kcfg ...` or `kevm view-kcfg ...` to ge This is the same file that is used for `kevm prove …`. - `--save-directory` must be passed as where the KCFGs have been saved (by a previous call to `kevm prove --save-directory save_directory ...`) - `--claim claim_label` lets you select an individual claim out of the `spec_file`. -If the flag is ommited, it’s assumed that only one claim is present. -If the flag is ommited and more than one claim is present in the `spec_file` then an error will be raised. +If the flag is omitted, it’s assumed that only one claim is present. +If the flag is omitted and more than one claim is present in the `spec_file` then an error will be raised. - `--spec-module spec_module` is also an inherited option. The interactive KCFG (`view-kcfg`) puts your terminal in *application mode*.