Documentation Improvements in ZK-EVM Specs

specs/bytecode-proof.md

@@ -17,7 +17,7 @@ The column `tag` (advice) makes the circuit behave as a state machine, selecting
 | `index`               | The position of the byte in the bytecode, starting from 0           |
 | `value`               | A bytecode byte if it's a `Byte` row. Length if it's a `Header` row.|
 | `is_code`             | `1` if the byte is code, `0` if the byte is PUSH data               |
-| `push_data_left`      | The number of left bytes data needs to be PUSHed                    |
+| `push_data_left`      | The number of bytes remaining to be pushed as data                  |
 | `value_rlc`           | The accumulator containing the current and previous bytes RLC       |
 | `length`              | The bytecode length, that could be 0 for empty bytecodes and padding|
 | `push_data_size`      | The number of bytes needs to be pushed if `is_code` is true         |

specs/copy-proof.md

@@ -1,6 +1,6 @@
 # Copy Proof
 
-The copy proof checks the values in the copy table and applies the lookup arguments to the corresponding tables to check if the value read from and write to data source is correct.
+The copy proof checks the values in the copy table and applies the lookup arguments to the corresponding tables to check if the value read from and written to the data source is correct.
 It also checks the padding behavior that the value read from an out-of-boundary address is 0.
 
 ## Circuit Layout

specs/evm-proof.md

@@ -17,7 +17,7 @@ We define the following Python custom types for type hinting and readability:
 
 ## Random Accessible Data
 
-In EVM, the interpreter has ability to do any random access to data like account balance, account storage, or stack and memory in current scope, but it's hard EVM circuit to keep tracking these data to ensure their consistency from time to time. So EVM proof has the state proof to provide a valid list of random read-write access records indexed by the `GlobalCounter` as a lookup table to do random access at any moment.
+In EVM, the interpreter has ability to do any random access to data like account balance, account storage, or stack and memory in current scope, but it's hard for the EVM circuit to keep tracking these data to ensure their consistency from time to time. So EVM proof has the state proof to provide a valid list of random read-write access records indexed by the `GlobalCounter` as a lookup table to do random access at any moment.
 
 We call the list of random read-write access records `BusMapping` because it acts like the bus in computer which transfers data between components. Similarly, read-only data are loaded as a lookup table into circuit for random access.
 

specs/opcode/5AGAS.md

@@ -2,7 +2,7 @@
 
 ## Procedure
 
-The `GAS` opcode gets the amount of available gas, including the correspoding reduction for the cost of the instruction itself.
+The `GAS` opcode gets the amount of available gas, including the corresponding reduction for the cost of the instruction itself.
 
 ## EVM behaviour