Documentation

EvmYul.EVM.Semantics

source
def EvmYul.EVM.argOnNBytesOfInstr :
Operation OperationType.EVM → ℕ
Equations
Instances For
    source
    def EvmYul.EVM.N (pc : UInt256) (instr : Operation OperationType.EVM) :
    UInt256
    Equations
    Instances For
      source
      def EvmYul.EVM.decode (arr : ByteArray) (pc : UInt256) :
      Option (Operation OperationType.EVM × Option (UInt256 × ℕ))

      Returns the instruction from arr at pc assuming it is valid.

      The Push instruction also returns the argument as an EVM word along with the width of the instruction.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def EvmYul.EVM.fetchInstr (I : ExecutionEnv) (pc : UInt256) :
        Except ExecutionException (Operation OperationType.EVM × Option (UInt256 × ℕ))
        Equations
        Instances For
          source
          partial def EvmYul.EVM.D_J_aux (c : ByteArray) (i : UInt256) (result : Array UInt256) :
          Array UInt256
          source
          def EvmYul.EVM.D_J (c : ByteArray) (i : UInt256) :
          Array UInt256
          Equations
          Instances For
            source
            def EvmYul.EVM.byteAt (μ₀ μ₁ : UInt256) :
            UInt256
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def EvmYul.EVM.dup (n : ℕ) :
              Transformer
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def EvmYul.EVM.swap (n : ℕ) :
                Transformer
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def EvmYul.EVM.instMonadLiftOptionExceptExecutionException :
                  MonadLift Option (Except ExecutionException)
                  Equations
                  Instances For
                    source
                    def EvmYul.EVM.call (fuel gasCost : ℕ) (blobVersionedHashes : List ByteArray) (gas source recipient t value value' inOffset inSize outOffset outSize : UInt256) (permission : Bool) (evmState : State) :
                    Except ExecutionException (UInt256 × State)
                    Equations
                    Instances For
                      source
                      def EvmYul.EVM.step (fuel gasCost : ℕ) (instr : Option (Operation OperationType.EVM × Option (UInt256 × ℕ)) := none) :
                      Transformer
                      Equations
                      Instances For
                        source
                        def EvmYul.EVM.X (fuel : ℕ) (validJumps : Array UInt256) (evmState : State) :
                        Except ExecutionException (ExecutionResult State)

                        Iterative progression of step

                        Equations
                        Instances For
                          source
                          def EvmYul.EVM.X.belongs (o : Option UInt256) (l : Array UInt256) :
                          Bool
                          Equations
                          Instances For
                            source
                            def EvmYul.EVM.X.notIn (o : Option UInt256) (l : Array UInt256) :
                            Bool
                            Equations
                            Instances For
                              source
                              def EvmYul.EVM.Ξ (fuel : ℕ) (createdAccounts : Batteries.RBSet AccountAddress compare) (genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (σ σ₀ : AccountMap) (g : UInt256) (A : Substate) (I : ExecutionEnv) :
                              Except ExecutionException (ExecutionResult (Batteries.RBSet AccountAddress compare × AccountMap × UInt256 × Substate))

                              The code execution function

                              Equations
                              Instances For
                                source
                                def EvmYul.EVM.Lambda (fuel : ℕ) (blobVersionedHashes : List ByteArray) (createdAccounts : Batteries.RBSet AccountAddress compare) (genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (σ σ₀ : AccountMap) (A : Substate) (s o : AccountAddress) (g p v : UInt256) (i : ByteArray) (e : UInt256) (ζ : Option ByteArray) (H : BlockHeader) (w : Bool) :
                                Except ExecutionException (AccountAddress × Batteries.RBSet AccountAddress compare × AccountMap × UInt256 × Substate × Bool × ByteArray)
                                Equations
                                Instances For
                                  source
                                  def EvmYul.EVM.Lambda.L_A (s : AccountAddress) (n : UInt256) (ζ : Option ByteArray) (i : ByteArray) :
                                  Option ByteArray
                                  Equations
                                  Instances For
                                    source
                                    def EvmYul.EVM.Θ (fuel : ℕ) (blobVersionedHashes : List ByteArray) (createdAccounts : Batteries.RBSet AccountAddress compare) (genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (σ σ₀ : AccountMap) (A : Substate) (s o r : AccountAddress) (c : ToExecute) (g p v v' : UInt256) (d : ByteArray) (e : ℕ) (H : BlockHeader) (w : Bool) :
                                    Except ExecutionException (Batteries.RBSet AccountAddress compare × AccountMap × UInt256 × Substate × Bool × ByteArray)

                                    Message cal σ - evm state A - accrued substate s - sender o - transaction originator r - recipient c - the account whose code is to be called, usually the same as r g - available gas p - effective gas price v - value v' - value in the execution context d - input data of the call e - depth of the message-call / contract-creation stack w - permissions to make modifications to the stack

                                    NB - This is implemented using the 'boolean' fragment with ==, <=, ||, etc. The 'prop' version will come next once we have the comutable one.

                                    Equations
                                    Instances For
                                      source
                                      def EvmYul.EVM.Υ (fuel : ℕ) (σ : AccountMap) (H_f : ℕ) (H genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (T : Transaction) (S_T : AccountAddress) :
                                      Except Exception (AccountMap × Substate × Bool × UInt256)
                                      Instances For