network, evm: add EVM_EC_ERROR exceptional status code for crypto function errors

Author: Everett Hildenbrandt

evm.md

@@ -1801,7 +1801,7 @@ Precompiled Contracts
 
     syntax InternalOp ::= #ecadd(G1Point, G1Point)
  // ----------------------------------------------
-    rule <k> #ecadd(P1, P2) => #exception EVM_INTERNAL_ERROR ... </k>
+    rule <k> #ecadd(P1, P2) => #exception EVM_EC_ERROR ... </k>
       requires notBool isValidPoint(P1) orBool notBool isValidPoint(P2)
     rule <k> #ecadd(P1, P2) => #end ... </k> <output> _ => #point(BN128Add(P1, P2)) </output>
       requires isValidPoint(P1) andBool isValidPoint(P2)
@@ -1813,7 +1813,7 @@ Precompiled Contracts
 
     syntax InternalOp ::= #ecmul(G1Point, Int)
  // ------------------------------------------
-    rule <k> #ecmul(P, S) => #exception EVM_INTERNAL_ERROR ... </k>
+    rule <k> #ecmul(P, S) => #exception EVM_EC_ERROR ... </k>
       requires notBool isValidPoint(P)
     rule <k> #ecmul(P, S) => #end ... </k> <output> _ => #point(BN128Mul(P, S)) </output>
       requires isValidPoint(P)
@@ -1827,7 +1827,7 @@ Precompiled Contracts
     rule <k> ECPAIRING => #ecpairing(.List, .List, 0, DATA, #sizeWordStack(DATA)) ... </k>
          <callData> DATA </callData>
       requires #sizeWordStack(DATA) modInt 192 ==Int 0
-    rule <k> ECPAIRING => #exception EVM_INTERNAL_ERROR ... </k>
+    rule <k> ECPAIRING => #exception EVM_EC_ERROR ... </k>
          <callData> DATA </callData>
       requires #sizeWordStack(DATA) modInt 192 =/=Int 0
 
@@ -1842,7 +1842,7 @@ Precompiled Contracts
  // -----------------------------------
     rule <k> (#checkPoint => .) ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) ... </k>
       requires isValidPoint(AK) andBool isValidPoint(BK)
-    rule <k> #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #exception EVM_INTERNAL_ERROR ... </k>
+    rule <k> #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #exception EVM_EC_ERROR ... </k>
       requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK)
 ```
 

network.md

@@ -26,6 +26,7 @@ The following codes all indicate that the VM ended execution with an exception,
     This can happen when accessing local memory with `CODECOPY*` or `CALLDATACOPY`, or when accessing return data with `RETURNDATACOPY`.
 -   `EVM_STATIC_MODE_ERROR` indicates that a `STATICCALL` tried to change state.
     **TODO:** Avoid `_ERROR` suffix that suggests fatal error.
+-   `EVM_EC_ERROR` indicates an error with the eliptic curve cryptographic builtins.
 
 ```k
     syntax ExceptionalStatusCode ::= "EVM_FAILURE"
@@ -37,6 +38,7 @@ The following codes all indicate that the VM ended execution with an exception,
                                    | "EVM_STACK_UNDERFLOW"
                                    | "EVM_INVALID_MEMORY_ACCESS"
                                    | "EVM_STATIC_MODE_ERROR"
+                                   | "EVM_EC_ERROR"
 ```
 
 ### Ending Codes