Creating separate module for bn128-operations

src/kontrol/kdist/bn128.md

@@ -0,0 +1,25 @@
+
+BN128 curve operations. These functions are part of the operations introduced in EIP-197, aimed at representing operations performed by precompiled contracts that operate on the elliptic curve alt_bn128.
+
+```k
+
+module BN128-OPERATIONS
+    imports EVM
+
+    syntax Bool ::= isValidPointSymbolic(G1Point) [function, total, no-evaluators, smtlib(isValidG1Point)]
+    rule isValidPoint(G) => isValidPointSymbolic(G) [priority(30)]
+
+    syntax G1Point ::= BN128MulOp(G1Point, Int) [function, total, smtlib(BN128Mul)]
+    rule BN128Mul(G, I) => BN128MulOp(G:G1Point, I:Int) [priority(30)]
+    rule BN128MulOp((PA:Int, PB:Int):G1Point, I:Int) => (PA *Int I , PB *Int I):G1Point
+
+
+    syntax G1Point ::= BN128AddOp(G1Point, G1Point) [function, total, smtlib(BN128Add)]
+    rule BN128Add(PA, PB) => BN128AddOp(PA, PB) [priority(30)]
+    rule BN128AddOp((PAA:Int, PAB:Int):G1Point, (PBA:Int, PBB:Int):G1Point) => (PAA +Int PBA , PAB +Int PBB):G1Point
+
+```
+
+```k
+endmodule
+```

src/kontrol/kdist/cheatcodes.md

@@ -1820,24 +1820,6 @@ Selector for Solidity built-in Error
 ```k
     rule ( selector ( "Error(string)" ) => 147028384 )
 ```
-
-BN128 functions
-
-```k
-    syntax Bool ::= isValidPointSymbolic(G1Point) [function, total, no-evaluators, smtlib(isValidG1Point)]
-    rule isValidPoint(G) => isValidPointSymbolic(G) [priority(30)]
-
-    syntax G1Point ::= BN128MulOp(G1Point, Int) [function, total, smtlib(BN128Mul)]
-    rule BN128Mul(G, I) => BN128MulOp(G:G1Point, I:Int) [priority(30)]
-    rule BN128MulOp((PA:Int, PB:Int):G1Point, I:Int) => (PA *Int I , PB *Int I):G1Point
-
-
-    syntax G1Point ::= BN128AddOp(G1Point, G1Point) [function, total, smtlib(BN128Add)]
-    rule BN128Add(PA, PB) => BN128AddOp(PA, PB) [priority(30)]
-    rule BN128AddOp((PAA:Int, PAB:Int):G1Point, (PBA:Int, PBB:Int):G1Point) => (PAA +Int PBA , PAB +Int PBB):G1Point
-
-```
-
 ```k
 endmodule
 ```

src/kontrol/kdist/foundry.md

@@ -16,6 +16,7 @@ requires "edsl.md"
 requires "trace.md"
 requires "assert.md"
 requires "lemmas/lemmas.k"
+requires "bn128.md"
 
 module FOUNDRY
     imports FOUNDRY-SUCCESS
@@ -26,6 +27,7 @@ module FOUNDRY
     imports KONTROL-ASSERTIONS
     imports EDSL
     imports LEMMAS
+    imports BN128-OPERATIONS
 
     configuration
       <foundry>