Implement sqrt

evm/src/cpu/kernel/asm/secp256k1/lift_x.asm

@@ -60,759 +60,13 @@
     ADDMOD
 %endmacro
 
-// Returns a square root of x if one exists, otherwise an undefined value.
+// Non-deterministically provide the square root modulo N.
-// Computed as x^(q+1)/4, with q the Secp base field order.
-// To replace with more efficient method using non-determinism later.
 %macro sqrt_secp_base
     // stack: x
-    DUP1
+    PROVER_INPUT(ff::secp256k1_base::sqrt)
-    %squaremodn_secp_base
+    // stack: √x, x
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    %squaremodn_secp_base
-    %squaremodn_secp_base
-    %squaremodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    DUP2
-    %mulmodn_secp_base
-    %squaremodn_secp_base
-    %squaremodn_secp_base
     SWAP1
-    // stack: x, x^-1
+    // stack: x, √x
     POP
-    // stack: x^-1
+    // stack: √x
 %endmacro

evm/src/cpu/kernel/prover_input.rs

@@ -103,7 +103,7 @@ impl Field {
     fn op(&self, op: FieldOp, x: U256) -> U256 {
         match op {
             FieldOp::Inverse => self.inverse(x),
-            FieldOp::Sqrt => todo!(),
+            FieldOp::Sqrt => self.sqrt(x),
         }
     }
 
@@ -112,6 +112,17 @@ impl Field {
         assert!(x < n);
         modexp(x, n - 2, n)
     }
+
+    fn sqrt(&self, x: U256) -> U256 {
+        let n = self.order();
+        assert!(x < n);
+        let (q, r) = (n + 1).div_mod(4.into());
+        assert!(
+            r.is_zero(),
+            "Only naive sqrt implementation for now. If needed implement Tonelli-Shanks."
+        );
+        modexp(x, q, n)
+    }
 }
 
 fn modexp(x: U256, e: U256, n: U256) -> U256 {