Add begin_tx and end_tx specs (#512)

* specs/begin_tx.md: create file

* specs/end_tx.md : create file

* being_tx: Update procedure and lookups

* end_tx: Update procedure and lookups

* being_tx: Adding consummed gas

* end_tx: Adding refund gas

* Second pass on begin_tx

* Second pass on end_tx

* fixup begin_tx: adding back tx lookups, txid and gas fee constraints

* begin/end_tx: update rw accesses

specs/virtual_state/begin_tx.md

@@ -0,0 +1,96 @@
+# BEGIN_TX 
+
+## Procedure
+
+The `begin_tx` gadget performs preliminary checks on a transaction and its caller's account as well as further checks depending on the transaction type. 
+
+More particularly, for all transactions, we make sure that the account nonce is incremented by 1 if the tx is valid, and that the caller address is not null. We also verify that a transaction is set as invalid if and only if there is either not enough gas, the tx's nonce is not the same as caller's account previous nonce or the balance is insufficient.
+
+Depending whether the transaction is a CREATE, calls a precompile or calls an account with or without code, the checks as well as the number of lookups vary.
+
+## Constraints
+/!\ Call to precompiles are not handled yet
+
+1. The transaction id is set to 1 if this is the first step.
+2. Calculate the transaction gas fee (gas price * gas + tx value = cost sum )
+3. The transaction is successful (lookup to CallContextFieldTag::IsSuccess with reversion_info.is_persistent)
+4. The transaction is valid
+    1. The gas is sufficient (tx.gas > tx.intrinsic_gas)
+    2. The balance is sufficient (gas limit > gas used, handled when transferring gas)
+    3. The nonce is valid (caller's previous nonce = tx.nonce)
+5. The access list of the transaction is initialised with the addresses of the caller, callee, coinbase and precompiles
+6. The caller's address is not null
+7. The caller's nonce is incremented (caller.nonce = tx.nonce + 1)
+8. The callee's codehash is correct
+9. Transfer the gas (reversible)
+10. If the transaction is a CREATE
+    1. Create the contract
+    2. The callee's address is correctly initialised from the caller's nonce
+    3. The callee's nonce is correctly initialised (reversible)
+    4. The contract's caller address is correctly initialised
+    5. The contract's caller nonce is correctly initialised
+    6. Transition to new context (reversible_write_counter = transfer.reversible + 1, rw_counter = 23 + transfer.rw + #precompiles)
+11. Else (call to account)
+    1. The callee's address is not null
+    2. If the account called has no code (empty code hash or account does not exist (i.e. code_hash = 0))
+        1. The transaction is persistant
+        2. The next execution state is endTx
+        3. Transition to new context (rw_counter = 9 + transfer.rw + #precompiles)
+    3. Else (call to account with code)
+        1. Transition to new context (reversible_write_counter = transfer.reversible, rw_counter = 22 + transfer.rw + #precompiles)
+12. (TODO. Call to precompile)
+
+Consummed gas: tx_calldata_gas_cost + tx_accesslist_gas + !is_create * GAS_COST_TX  + is_create * (GAS_COST_CREATION_TX + len_words * GAS_COST_INITCODE_WORD)
+
+### Lookups
+
+#### RW accesses
+In all cases, we bump read-write-counter by 9 + #transfer:
+- BeginTxHelper
+    - CallContext TxId
+- CallContext RwCounterEndOfReversion (done through reversion_info)
+- CallContext IsPersistent (done through reversion_info)
+- CallContext IsSuccess
+- StateWrite adding caller's address to Tx access list
+- StateWrite adding callee's address to Tx access list
+- StateWrite adding coinbase address to Tx access list
+- StateWrite adding precompile addresses to Tx access list    #precompile
+- AccountWrite caller's Nonce
+- AccountRead calee's CodeHash
+- TransferWithGasFee (reversible)
+    - AccountWrite caller's Balance 
+    - AccountWrite callee's Balance
+
+If tx is CREATE, we also bump read-write-counter by 1:
+- AccountWrite callee's Nonce (reversible)
+
+If tx is not a contract call with no code, we also bump read-write-counter by 13:
+- CallContext Depth
+- CallContext CallerAddress
+- CallContext CalleeAddress
+- CallContext CallDataOffset
+- CallContext CallDataLength
+- CallContext Value
+- CallContext IsStatic
+- CallContext LastCalleeId
+- CallContext LastCalleeReturnDataOffset
+- CallContext LastCalleeReturnDataLength
+- CallContext IsRoot
+- CallContext IsCreate
+- CallContext CodeHash
+
+#### Other Lookups
+- TxData
+    - TxContext Nonce
+    - TxContext Gas
+    - TxContext IsCreate
+    - TxContext CallDataLength
+    - TxContext CallDataGasCost
+    - TxContext GasPrice
+    - TxContext Value
+    - TxContext Caller Address
+    - TxContext Callee Address
+- BlockContext Coinbase
+- KeccakTable create.input_rlc
+
+## Exceptions

specs/virtual_state/end_tx.md

@@ -0,0 +1,52 @@
+# END_TX 
+
+## Procedure
+
+The `end_tx` gadget handles refund and coinbase tip as well as cumulative gas within a block. 
+
+
+## Constraints
+
+1. Calculate effective refund (c.f. below list)
+2. Add [(effective_refund + gas_left) * gas_price] back to caller's balance
+3. Check effective tip = tx gas price - base fee
+4. Add gas_used * effective_tip to coinbase's balance (and create coinbase account if needs be)
+5. End transaction
+    1. Check that the current cumulative gas used is null if this is the 1st transaction else corresponds to previous transaction's
+    2. Increase cumulative gas used by the gas used
+    3. If the next execution state is BeginTx
+        1. The next transaction's id is correctly incremented
+        2. Transition to new context (rw_counter =  9 + transfer.rw - is_first_tx)
+    4. Elif the next execution step is EndBlock
+        1. Transition to new context (rw_counter =  9 + transfer.rw - is_first_tx, and same call id)
+
+Gas refund: it is capped to  gas_used // MAX_REFUND_QUOTIENT_OF_GAS_USED (c.f. EIP 3529)
+
+### Lookups
+
+#### RW accesses
+In all cases, we bump read-write-counter by 9 + transfer.rw - is_first_tx:
+- CallContext TxId
+- CallContext IsPersistent
+- RWLookup Read TxRefund
+- AccountRead coinbase's codehash
+- UpdateBalance
+    - AccountWrite caller's balance
+- TransferTo
+    - AccountWrite coinbase's balance
+- EndTx
+    - RWLookup Write TxReceipt.PostStateOrStatus
+    - RWLookup Write TxReceipt.LogLength
+    - RWLookup Write current transaction's TxReceipt.CumulativeGasUsed
+    - If not first tx, RWLookup Read previous transaction's TxReceipt.CumulativeGasUsed
+    - If next execution state is BeginTx, CallContext TxId (does not increase rw counter)
+
+
+#### Other Lookups
+- TxContext Gas
+- TxContext GasPrice
+- TxContext CallerAddress
+- BlockContext BaseFee
+- BlockContext Coinbase
+
+## Exceptions