Merge pull request #571 from ConsenSys/570-support-remaining-alt_bn12…

…8-precompiles Implement `alt_bn128` multiplication
Consensys · May 8, 2023 · 1279c7c · 1279c7c
2 parents 6d4cf53 + 9725aa9
commit 1279c7c
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 3 deletions.
diff --git a/src/dafny/core/precompiled.dfy b/src/dafny/core/precompiled.dfy
@@ -279,7 +279,30 @@ module Precompiled {
     const G_BNMUL := 6000
 
     function CallBnMul(data: Array<u8>) : Option<(Array<u8>,nat)> {
-        Some((data, G_BNMUL))
+        // Axiom needed for this all to go through.
+        AltBn128.IsPrimeField();
+        // Point
+        var x0 := BNF(Bytes.ReadUint256(data,0) as nat);
+        var y0 := BNF(Bytes.ReadUint256(data,32) as nat);
+        // Factor
+        var n := Bytes.ReadUint256(data,64);
+        // Sanity check input values are prime fields for BN128
+        if x0 == None || y0 == None
+        then
+            None
+        else
+            var p0 := BNP(x0.Unwrap(),y0.Unwrap());
+            // Sanity check input point is on the BN128 curve
+            if p0 == None
+            then
+                None
+            else
+                var p := AltBn128.PointMul(p0.Unwrap(),n);
+                var p_x := p.0 as u256;
+                var p_y := p.1 as u256;
+                var bytes : Array<u8> := U256.ToBytes(p_x) + U256.ToBytes(p_y);
+                assert |bytes| == 64;
+                Some((bytes,G_BNMUL))
     }
 
     // ========================================================================

diff --git a/src/dafny/crypto/alt_bn128.dfy b/src/dafny/crypto/alt_bn128.dfy
@@ -123,6 +123,18 @@ module EllipticCurve refines FiniteField {
             else
                 INFINITY
     }
+
+    // Multiply a point by a given factor on the curve.
+    function PointMul(p: Point, n: u256) : (r:Point)
+    requires N > 3 && IsPrime(N)
+    decreases n
+    {
+        if n == 0 then INFINITY
+        else
+            var res := PointMul(PointAdd(p,p),n / 2);
+            if n % 2 == 1 then PointAdd(res,p)
+            else res
+    }
 }
 
 // The ellptic curve given by y^2 == x^3 + 3.

diff --git a/src/test/java/dafnyevm/GeneralStateTests.java b/src/test/java/dafnyevm/GeneralStateTests.java
@@ -114,10 +114,10 @@ public class GeneralStateTests {
             "StaticcallToPrecompileFromTransaction_Berlin_0_0_0",
             "precompsEIP2929_Berlin_0_(43|61|151|169|241|295)_0",
             "idPrecomps_Berlin_0_[4-7]_0",
-            "ecmul_.*",
+            //"ecmul_.*",
             "ecpairing.*",
             "pairingTest.*",
-            "pointMulAdd.*",
+            //"pointMulAdd.*",
             // #455
             "MSTORE_Bounds2_Berlin_(0|1)_0_0",
             "modexp_Berlin_[0123]_(2|28|29|30|36|37)_0", // int overflow