For curve25519-dalek, overflow doesn't happen in field AddAssign for a collaborative prover

Cargo.toml

@@ -10,3 +10,11 @@ resolver = "2"
 [profile.dev]
 opt-level = 2
 
+[patch.crates-io.crypto-bigint]
+git = "https://github.com/risc0/RustCrypto-crypto-bigint"
+tag = "v0.5.2-risc0"
+
+[patch.crates-io.sha2]
+git = "https://github.com/risc0/RustCrypto-hashes"
+tag = "sha2-v0.10.6-risc0"
+

curve25519-dalek/Cargo.toml

@@ -32,8 +32,6 @@ features = ["serde", "rand_core", "digest", "legacy_compatibility"]
 [dev-dependencies]
 sha2 = { version = "0.10", default-features = false }
 bincode = "1"
-criterion = { version = "0.5", features = ["html_reports"] }
-hex = "0.4.2"
 rand = "0.8"
 rand_core = { version = "0.6", default-features = false, features = ["getrandom"] }
 
@@ -49,18 +47,26 @@ required-features = ["alloc", "rand_core"]
 [dependencies]
 cfg-if = "1"
 group = { version = "0.13", default-features = false, optional = true }
+hex = "0.4.2"
 rand_core = { version = "0.6.4", default-features = false, optional = true }
 digest = { version = "0.10", default-features = false, optional = true }
 subtle = { version = "2.3.0", default-features = false }
 serde = { version = "1.0", default-features = false, optional = true, features = ["derive"] }
 zeroize = { version = "1", default-features = false, optional = true }
 
+[target.'cfg(target_os = "zkvm")'.dependencies]
+# Use crypto-bigint v0.5.2, which is overridden with a patch for RISC Zero acceleration.
+crypto-bigint = { version = "=0.5.2", default-features = false, features = ["zeroize"] }
+
 [target.'cfg(target_arch = "x86_64")'.dependencies]
 cpufeatures = "0.2.6"
 
 [target.'cfg(curve25519_dalek_backend = "fiat")'.dependencies]
 fiat-crypto = { version = "0.2.1", default-features = false }
 
+[target.'cfg(not(target_os = "zkvm"))'.dev-dependencies]
+criterion = { version = "0.5.1", features = ["html_reports"] }
+
 [features]
 default = ["alloc", "precomputed-tables", "zeroize"]
 alloc = ["zeroize?/alloc"]

curve25519-dalek/build.rs

@@ -103,7 +103,9 @@ mod deterministic {
         let platform = match platforms::Platform::find(&target_triplet) {
             Some(p) => p,
             None => {
-                determine_curve25519_dalek_bits_warning(ERR_MSG_NO_PLATFORM);
+                if target_triplet != "riscv32im-risc0-zkvm-elf" {
+                    determine_curve25519_dalek_bits_warning(ERR_MSG_NO_PLATFORM);
+                }
                 return DalekBits::Dalek32;
             }
         };

curve25519-dalek/src/backend/serial/curve_models/mod.rs

@@ -383,13 +383,25 @@ impl ProjectivePoint {
         let XX = self.X.square();
         let YY = self.Y.square();
         let ZZ2 = self.Z.square2();
-        let X_plus_Y = &self.X + &self.Y;
-        let X_plus_Y_sq = X_plus_Y.square();
         let YY_plus_XX = &YY + &XX;
         let YY_minus_XX = &YY - &XX;
 
+        cfg_if::cfg_if! {
+            if #[cfg(all(target_os = "zkvm", target_arch = "riscv32"))] {
+                // According to https://en.wikipedia.org/wiki/Edwards_curve#Doubling,
+                // (x + y)^2 - x^2 - y^2 is used as an optimization for computing 2xy.
+                // However, multiplication is faster inside the zkvm so we compute
+                // 2xy directly instead.
+                let new_x = &(&FieldElement::TWO * &self.X) * &self.Y;
+            } else {
+                let X_plus_Y = &self.X + &self.Y;
+                let X_plus_Y_sq = X_plus_Y.square();
+                let new_x = &X_plus_Y_sq - &YY_plus_XX;
+            }
+        }
+
         CompletedPoint {
-            X: &X_plus_Y_sq - &YY_plus_XX,
+            X: new_x,
             Y: YY_plus_XX,
             Z: YY_minus_XX,
             T: &ZZ2 - &YY_minus_XX,
@@ -418,7 +430,14 @@ impl<'a, 'b> Add<&'b ProjectiveNielsPoint> for &'a EdwardsPoint {
         let MM = &Y_minus_X * &other.Y_minus_X;
         let TT2d = &self.T * &other.T2d;
         let ZZ = &self.Z * &other.Z;
-        let ZZ2 = &ZZ + &ZZ;
+
+        cfg_if::cfg_if! {
+            if #[cfg(all(target_os = "zkvm", target_arch = "riscv32"))] {
+                let ZZ2 = &FieldElement::TWO * &ZZ;
+            } else {
+                let ZZ2 = &ZZ + &ZZ;
+            }
+        }
 
         CompletedPoint {
             X: &PP - &MM,
@@ -440,7 +459,14 @@ impl<'a, 'b> Sub<&'b ProjectiveNielsPoint> for &'a EdwardsPoint {
         let MP = &Y_minus_X * &other.Y_plus_X;
         let TT2d = &self.T * &other.T2d;
         let ZZ = &self.Z * &other.Z;
-        let ZZ2 = &ZZ + &ZZ;
+
+        cfg_if::cfg_if! {
+            if #[cfg(all(target_os = "zkvm", target_arch = "riscv32"))] {
+                let ZZ2 = &FieldElement::TWO * &ZZ;
+            } else {
+                let ZZ2 = &ZZ + &ZZ;
+            }
+        }
 
         CompletedPoint {
             X: &PM - &MP,
@@ -461,7 +487,14 @@ impl<'a, 'b> Add<&'b AffineNielsPoint> for &'a EdwardsPoint {
         let PP = &Y_plus_X * &other.y_plus_x;
         let MM = &Y_minus_X * &other.y_minus_x;
         let Txy2d = &self.T * &other.xy2d;
-        let Z2 = &self.Z + &self.Z;
+
+        cfg_if::cfg_if! {
+            if #[cfg(all(target_os = "zkvm", target_arch = "riscv32"))] {
+                let Z2 = &FieldElement::TWO * &self.Z;
+            } else {
+                let Z2 = &self.Z + &self.Z;
+            }
+        }
 
         CompletedPoint {
             X: &PP - &MM,
@@ -482,7 +515,14 @@ impl<'a, 'b> Sub<&'b AffineNielsPoint> for &'a EdwardsPoint {
         let PM = &Y_plus_X * &other.y_minus_x;
         let MP = &Y_minus_X * &other.y_plus_x;
         let Txy2d = &self.T * &other.xy2d;
-        let Z2 = &self.Z + &self.Z;
+
+        cfg_if::cfg_if! {
+            if #[cfg(all(target_os = "zkvm", target_arch = "riscv32"))] {
+                let Z2 = &FieldElement::TWO * &self.Z;
+            } else {
+                let Z2 = &self.Z + &self.Z;
+            }
+        }
 
         CompletedPoint {
             X: &PM - &MP,

curve25519-dalek/src/backend/serial/mod.rs

@@ -31,6 +31,10 @@ cfg_if! {
         #[doc(hidden)]
         pub mod fiat_u64;
 
+    } else if #[cfg(all(target_os = "zkvm", target_arch = "riscv32"))] {
+
+        pub mod risc0;
+
     } else {
 
         #[cfg(curve25519_dalek_bits = "32")]