mirror of
https://github.com/logos-storage/circom-goldilocks.git
synced 2026-01-02 13:03:10 +00:00
implement quadratic field extension (unfortunately, for some reasons, the test framework doesn't work for the more interesting extension field operations...??)
This commit is contained in:
parent
d52cb86c7d
commit
f19f908d0a
@ -18,11 +18,11 @@ pragma circom 2.2.0;
|
|||||||
|
|
||||||
//------------------------------------------------------------------------------
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
function SolinasExpoBig() { return 64; }
|
// function SolinasExpoBig() { return 64; }
|
||||||
function SolinasExpoSmall() { return 32; }
|
// function SolinasExpoSmall() { return 32; }
|
||||||
|
|
||||||
// function SolinasExpoBig() { return 8; }
|
function SolinasExpoBig() { return 8; }
|
||||||
// function SolinasExpoSmall() { return 4; }
|
function SolinasExpoSmall() { return 4; }
|
||||||
|
|
||||||
function FieldPrime() {
|
function FieldPrime() {
|
||||||
return (2**SolinasExpoBig() - 2**SolinasExpoSmall() + 1);
|
return (2**SolinasExpoBig() - 2**SolinasExpoSmall() + 1);
|
||||||
|
|||||||
@ -191,7 +191,6 @@ template Mul() {
|
|||||||
C <== ReduceModP( SolinasExpoBig() )( A.val * B.val );
|
C <== ReduceModP( SolinasExpoBig() )( A.val * B.val );
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
//
|
//
|
||||||
// multiplication of 3 Goldilocks field elements
|
// multiplication of 3 Goldilocks field elements
|
||||||
// as this still fits into 192 < 254 bits, we can do it a bit more efficiently
|
// as this still fits into 192 < 254 bits, we can do it a bit more efficiently
|
||||||
@ -209,6 +208,16 @@ template Mul3() {
|
|||||||
D <== ReduceModP( 2 * SolinasExpoBig() )( AB * C.val );
|
D <== ReduceModP( 2 * SolinasExpoBig() )( AB * C.val );
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//--------------------------------------
|
||||||
|
|
||||||
|
// Squaring (this is more interesting in the extension field case)
|
||||||
|
//
|
||||||
|
template Sqr() {
|
||||||
|
input Goldilocks() A;
|
||||||
|
output Goldilocks() C;
|
||||||
|
C <== Mul()( A , A );
|
||||||
|
}
|
||||||
|
|
||||||
//------------------------------------------------------------------------------
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
//
|
//
|
||||||
|
|||||||
140
circuit/goldilocks_ext.circom
Normal file
140
circuit/goldilocks_ext.circom
Normal file
@ -0,0 +1,140 @@
|
|||||||
|
|
||||||
|
//
|
||||||
|
// the quadratic field extension `F[X] / (X^2 - 7)` over Goldilocks
|
||||||
|
//
|
||||||
|
// note: `X^2 - 7` is also irreducible over the field of size `2^8 - 2^4 + 1`
|
||||||
|
// so can use it for testing too.
|
||||||
|
//
|
||||||
|
|
||||||
|
pragma circom 2.2.0;
|
||||||
|
|
||||||
|
include "goldilocks.circom";
|
||||||
|
// include "misc.circom";
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
//
|
||||||
|
// the type of quadratic field extension elements.
|
||||||
|
//
|
||||||
|
|
||||||
|
bus GoldilocksExt() {
|
||||||
|
Goldilocks() real;
|
||||||
|
Goldilocks() imag;
|
||||||
|
}
|
||||||
|
|
||||||
|
template GoldilocksToExt() {
|
||||||
|
input Goldilocks() inp;
|
||||||
|
output GoldilocksExt() out;
|
||||||
|
out.real <== inp;
|
||||||
|
out.imag.val <== 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
template NegExt() {
|
||||||
|
input GoldilocksExt() A;
|
||||||
|
output GoldilocksExt() C;
|
||||||
|
|
||||||
|
C.real <== Neg()( A.real );
|
||||||
|
C.imag <== Neg()( A.imag );
|
||||||
|
}
|
||||||
|
|
||||||
|
template AddExt() {
|
||||||
|
input GoldilocksExt() A,B;
|
||||||
|
output GoldilocksExt() C;
|
||||||
|
|
||||||
|
C.real <== Add()( A.real , B.real );
|
||||||
|
C.imag <== Add()( A.imag , B.imag );
|
||||||
|
}
|
||||||
|
|
||||||
|
template SubExt() {
|
||||||
|
input GoldilocksExt() A,B;
|
||||||
|
output GoldilocksExt() C;
|
||||||
|
|
||||||
|
C.real <== Sub()( A.real , B.real );
|
||||||
|
C.imag <== Sub()( A.imag , B.imag );
|
||||||
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
template SevenTimesProduct() {
|
||||||
|
input Goldilocks() inp1,inp2;
|
||||||
|
output Goldilocks() out;
|
||||||
|
out <== ReduceModP( 3 + SolinasExpoBig() )( 7 * inp1.val * inp2.val );
|
||||||
|
}
|
||||||
|
|
||||||
|
template SevenTimesSquare() {
|
||||||
|
input Goldilocks() inp;
|
||||||
|
output Goldilocks() out;
|
||||||
|
out <== ReduceModP( 3 + SolinasExpoBig() )( 7 * inp.val * inp.val );
|
||||||
|
}
|
||||||
|
|
||||||
|
//--------------------------------------
|
||||||
|
|
||||||
|
template MulExt() {
|
||||||
|
input GoldilocksExt() A,B;
|
||||||
|
output GoldilocksExt() C;
|
||||||
|
|
||||||
|
Goldilocks() RR, IR, RI, IIx7;
|
||||||
|
RR <== Mul()( A.real , B.real );
|
||||||
|
IR <== Mul()( A.imag , B.real );
|
||||||
|
RI <== Mul()( A.real , B.imag );
|
||||||
|
IIx7 <== SevenTimesProduct()( A.imag , B.imag );
|
||||||
|
|
||||||
|
C.real <== Add()( RR , IIx7 );
|
||||||
|
C.imag <== Add()( IR , RI );
|
||||||
|
}
|
||||||
|
|
||||||
|
template SqrExt() {
|
||||||
|
input GoldilocksExt() A;
|
||||||
|
output GoldilocksExt() C;
|
||||||
|
|
||||||
|
Goldilocks() RR, IR, IIx7;
|
||||||
|
RR <== Sqr()( A.real );
|
||||||
|
IR <== Mul()( A.imag , A.real );
|
||||||
|
IIx7 <== SevenTimesSquare()( A.imag );
|
||||||
|
|
||||||
|
C.real <== Add()( RR , IIx7 );
|
||||||
|
C.imag <== Add()( IR , IR );
|
||||||
|
|
||||||
|
// log("\nsqrExt");
|
||||||
|
// log( "A = (", A.real.val, " , ", A.imag.val, ")" );
|
||||||
|
// log( "C = (", C.real.val, " , ", C.imag.val, ")" );
|
||||||
|
// log( "RR = ", RR.val );
|
||||||
|
// log( "IR = ", IR.val );
|
||||||
|
// log( "IRx7 = ", IIx7.val );
|
||||||
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
template InvExt() {
|
||||||
|
input GoldilocksExt() A;
|
||||||
|
output GoldilocksExt() C;
|
||||||
|
|
||||||
|
Goldilocks() seven, RR, IIx7;
|
||||||
|
seven.val <== 7;
|
||||||
|
RR <== Sqr()( A.real );
|
||||||
|
IIx7 <== SevenTimesSquare()( A.imag );
|
||||||
|
|
||||||
|
Goldilocks() denom <== Sub()( RR , IIx7 );
|
||||||
|
Goldilocks() mult <== Inv()( denom );
|
||||||
|
Goldilocks() minusImag <== Neg()( A.imag );
|
||||||
|
|
||||||
|
C.real <== Mul()( A.real , mult );
|
||||||
|
C.imag <== Mul()( minusImag , mult );
|
||||||
|
}
|
||||||
|
|
||||||
|
template DivExt() {
|
||||||
|
input GoldilocksExt() A,B;
|
||||||
|
output GoldilocksExt() C;
|
||||||
|
|
||||||
|
GoldilocksExt() invB <== InvExt()( B );
|
||||||
|
C <== MulExt()( A , invB );
|
||||||
|
|
||||||
|
log("\ndivExt");
|
||||||
|
log( "A = (", A.real.val, " , ", A.imag.val, ")" );
|
||||||
|
log( "B = (", B.real.val, " , ", B.imag.val, ")" );
|
||||||
|
log( "C = (", C.real.val, " , ", C.imag.val, ")" );
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
@ -2,13 +2,15 @@
|
|||||||
|
|
||||||
ORIG=`pwd`
|
ORIG=`pwd`
|
||||||
MAIN="testmain"
|
MAIN="testmain"
|
||||||
INPUT="dummy.json"
|
INPUT="input.json"
|
||||||
|
|
||||||
cd build
|
cd build
|
||||||
|
|
||||||
circom ../${MAIN}.circom --r1cs --wasm
|
circom ../${MAIN}.circom --r1cs --wasm
|
||||||
|
|
||||||
echo '{ "dummy": 666 }' >${INPUT}
|
#echo '{ "dummy": 666 }' >${INPUT}
|
||||||
|
#echo '{ "A": [66,111] }' >${INPUT}
|
||||||
|
echo '{ "A": [57,137] , "B": [66,111] }' >${INPUT}
|
||||||
|
|
||||||
cd ${MAIN}_js
|
cd ${MAIN}_js
|
||||||
|
|
||||||
|
|||||||
@ -65,6 +65,17 @@ template SubWrapper() {
|
|||||||
|
|
||||||
//------------------------------------------------------------------------------
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
template SqrWrapper() {
|
||||||
|
signal input A;
|
||||||
|
signal output C;
|
||||||
|
|
||||||
|
Goldilocks() A1; A1.val <== A;
|
||||||
|
Goldilocks() C1;
|
||||||
|
|
||||||
|
C1 <== Sqr()( A1 );
|
||||||
|
C1.val ==> C;
|
||||||
|
}
|
||||||
|
|
||||||
template MulWrapper() {
|
template MulWrapper() {
|
||||||
signal input A,B;
|
signal input A,B;
|
||||||
signal output C;
|
signal output C;
|
||||||
@ -77,6 +88,8 @@ template MulWrapper() {
|
|||||||
C1.val ==> C;
|
C1.val ==> C;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
template InvWrapper() {
|
template InvWrapper() {
|
||||||
signal input A;
|
signal input A;
|
||||||
signal output C;
|
signal output C;
|
||||||
|
|||||||
104
circuit/test_wrapper_ext.circom
Normal file
104
circuit/test_wrapper_ext.circom
Normal file
@ -0,0 +1,104 @@
|
|||||||
|
|
||||||
|
// wrappers around the Goldilocks templates, so that input and output are classic
|
||||||
|
// signals, not Bus-es. The testing framework does not handle Bus inputs/outputs yet
|
||||||
|
|
||||||
|
pragma circom 2.2.0;
|
||||||
|
|
||||||
|
include "goldilocks.circom";
|
||||||
|
include "goldilocks_ext.circom";
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
template NegExtWrapper() {
|
||||||
|
signal input A[2];
|
||||||
|
signal output C[2];
|
||||||
|
|
||||||
|
GoldilocksExt() A1; A1.real.val <== A[0]; A1.imag.val <== A[1];
|
||||||
|
|
||||||
|
GoldilocksExt() C1 <== NegExt()( A1 );
|
||||||
|
|
||||||
|
C1.real.val ==> C[0];
|
||||||
|
C1.imag.val ==> C[1];
|
||||||
|
}
|
||||||
|
|
||||||
|
template AddExtWrapper() {
|
||||||
|
signal input A[2],B[2];
|
||||||
|
signal output C[2];
|
||||||
|
|
||||||
|
GoldilocksExt() A1; A1.real.val <== A[0]; A1.imag.val <== A[1];
|
||||||
|
GoldilocksExt() B1; B1.real.val <== B[0]; B1.imag.val <== B[1];
|
||||||
|
|
||||||
|
GoldilocksExt() C1 <== AddExt()( A1 , B1 );
|
||||||
|
|
||||||
|
C1.real.val ==> C[0];
|
||||||
|
C1.imag.val ==> C[1];
|
||||||
|
}
|
||||||
|
|
||||||
|
template SubExtWrapper() {
|
||||||
|
signal input A[2],B[2];
|
||||||
|
signal output C[2];
|
||||||
|
|
||||||
|
GoldilocksExt() A1; A1.real.val <== A[0]; A1.imag.val <== A[1];
|
||||||
|
GoldilocksExt() B1; B1.real.val <== B[0]; B1.imag.val <== B[1];
|
||||||
|
|
||||||
|
GoldilocksExt() C1 <== SubExt()( A1 , B1 );
|
||||||
|
|
||||||
|
C1.real.val ==> C[0];
|
||||||
|
C1.imag.val ==> C[1];
|
||||||
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
template SqrExtWrapper() {
|
||||||
|
signal input A[2];
|
||||||
|
signal output C[2];
|
||||||
|
|
||||||
|
GoldilocksExt() A1; A1.real.val <== A[0]; A1.imag.val <== A[1];
|
||||||
|
|
||||||
|
GoldilocksExt() C1 <== SqrExt()( A1 );
|
||||||
|
|
||||||
|
C1.real.val ==> C[0];
|
||||||
|
C1.imag.val ==> C[1];
|
||||||
|
}
|
||||||
|
|
||||||
|
template MulExtWrapper() {
|
||||||
|
signal input A[2],B[2];
|
||||||
|
signal output C[2];
|
||||||
|
|
||||||
|
GoldilocksExt() A1; A1.real.val <== A[0]; A1.imag.val <== A[1];
|
||||||
|
GoldilocksExt() B1; B1.real.val <== B[0]; B1.imag.val <== B[1];
|
||||||
|
|
||||||
|
GoldilocksExt() C1 <== MulExt()( A1 , B1 );
|
||||||
|
|
||||||
|
C1.real.val ==> C[0];
|
||||||
|
C1.imag.val ==> C[1];
|
||||||
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
template InvExtWrapper() {
|
||||||
|
signal input A[2];
|
||||||
|
signal output C[2];
|
||||||
|
|
||||||
|
GoldilocksExt() A1; A1.real.val <== A[0]; A1.imag.val <== A[1];
|
||||||
|
|
||||||
|
GoldilocksExt() C1 <== InvExt()( A1 );
|
||||||
|
|
||||||
|
C1.real.val ==> C[0];
|
||||||
|
C1.imag.val ==> C[1];
|
||||||
|
}
|
||||||
|
|
||||||
|
template DivExtWrapper() {
|
||||||
|
signal input A[2],B[2];
|
||||||
|
signal output C[2];
|
||||||
|
|
||||||
|
GoldilocksExt() A1; A1.real.val <== A[0]; A1.imag.val <== A[1];
|
||||||
|
GoldilocksExt() B1; B1.real.val <== B[0]; B1.imag.val <== B[1];
|
||||||
|
|
||||||
|
GoldilocksExt() C1 <== DivExt()( A1 , B1 );
|
||||||
|
|
||||||
|
C1.real.val ==> C[0];
|
||||||
|
C1.imag.val ==> C[1];
|
||||||
|
}
|
||||||
|
|
||||||
|
//------------------------------------------------------------------------------
|
||||||
@ -2,9 +2,15 @@
|
|||||||
pragma circom 2.2.0;
|
pragma circom 2.2.0;
|
||||||
|
|
||||||
include "test_wrapper.circom";
|
include "test_wrapper.circom";
|
||||||
|
include "test_wrapper_ext.circom";
|
||||||
|
|
||||||
include "poseidon.circom";
|
include "poseidon.circom";
|
||||||
|
|
||||||
// component main { public [A,B] } = AddWrapper();
|
// component main { public [A,B] } = AddWrapper();
|
||||||
// component main { public [A] } = InvWrapper();
|
// component main { public [A] } = InvWrapper();
|
||||||
|
|
||||||
component main { public [dummy] } = CheckPermutationKAT();
|
// component main { public [dummy] } = CheckPermutationKAT();
|
||||||
|
|
||||||
|
// component main { public [A,B] } = MulExtWrapper();
|
||||||
|
// component main { public [A] } = SqrExtWrapper();
|
||||||
|
component main { public [A,B] } = DivExtWrapper();
|
||||||
|
|||||||
@ -8,7 +8,8 @@ module Main where
|
|||||||
|
|
||||||
import R1CS
|
import R1CS
|
||||||
|
|
||||||
import TestGoldilocks
|
import qualified TestGoldilocks as Gld
|
||||||
|
import qualified TestGoldilocksExt as Ext
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
@ -21,18 +22,39 @@ testGoldilocks' fld verbosity = runWithField fld $ \pxy -> do
|
|||||||
let runSpec what = testSemantics pxy what verbosity
|
let runSpec what = testSemantics pxy what verbosity
|
||||||
let runSpecMany what = testSemanticsMany pxy what verbosity
|
let runSpecMany what = testSemanticsMany pxy what verbosity
|
||||||
|
|
||||||
runSpec specIsZero
|
runSpec Gld.specIsZero
|
||||||
runSpec specToGoldi
|
runSpec Gld.specToGoldi
|
||||||
runSpec $ specUnary Neg semantics_neg
|
runSpec $ Gld.specUnary Gld.Neg Gld.semantics_neg
|
||||||
runSpec $ specBinary Add semantics_add
|
runSpec $ Gld.specBinary Gld.Add Gld.semantics_add
|
||||||
runSpec $ specBinary Sub semantics_sub
|
runSpec $ Gld.specBinary Gld.Sub Gld.semantics_sub
|
||||||
runSpec $ specUnary Inv semantics_inv
|
runSpec $ Gld.specUnary Gld.Sqr Gld.semantics_sqr
|
||||||
|
runSpec $ Gld.specUnary Gld.Inv Gld.semantics_inv
|
||||||
|
|
||||||
-- these are very slow so we don't do exhaustive testing
|
-- these are very slow so we don't do exhaustive testing
|
||||||
runSpec $ specBinarySmall Mul semantics_mul
|
runSpec $ Gld.specBinarySmall Gld.Mul Gld.semantics_mul
|
||||||
runSpec $ specBinarySmall Div semantics_div
|
runSpec $ Gld.specBinarySmall Gld.Div Gld.semantics_div
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
testGoldilocksExt :: IO ()
|
||||||
|
testGoldilocksExt = testGoldilocksExt' Field24 Silent
|
||||||
|
|
||||||
|
testGoldilocksExt' :: FieldChoice -> Verbosity -> IO ()
|
||||||
|
testGoldilocksExt' fld verbosity = runWithField fld $ \pxy -> do
|
||||||
|
|
||||||
|
let runSpec what = testSemantics pxy what verbosity
|
||||||
|
let runSpecMany what = testSemanticsMany pxy what verbosity
|
||||||
|
|
||||||
|
runSpec $ Ext.specUnary Ext.Neg Ext.semantics_neg
|
||||||
|
runSpec $ Ext.specBinary Ext.Add Ext.semantics_add
|
||||||
|
runSpec $ Ext.specBinary Ext.Sub Ext.semantics_sub
|
||||||
|
-- runSpec $ Ext.specUnary Ext.Sqr Ext.semantics_sqr
|
||||||
|
-- runSpec $ Ext.specBinary Ext.Mul Ext.semantics_mul
|
||||||
|
-- runSpec $ Ext.specUnary Ext.Inv Ext.semantics_inv
|
||||||
|
-- runSpec $ Ext.specBinary Ext.Div Ext.semantics_div
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
main = do
|
main = do
|
||||||
testGoldilocks
|
testGoldilocks
|
||||||
|
testGoldilocksExt
|
||||||
|
|||||||
@ -1,13 +1,17 @@
|
|||||||
|
|
||||||
|
{-# LANGUAGE BlockArguments #-}
|
||||||
module Semantics where
|
module Semantics where
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
import Prelude hiding (div)
|
import Prelude hiding (div)
|
||||||
|
import Control.Monad
|
||||||
|
import System.Random
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
type F = Int
|
type F = Int
|
||||||
|
type FExt = (F,F)
|
||||||
|
|
||||||
fieldPrime :: Int
|
fieldPrime :: Int
|
||||||
fieldPrime = 2^8 - 2^4 + 1
|
fieldPrime = 2^8 - 2^4 + 1
|
||||||
@ -54,3 +58,123 @@ div :: F -> F -> F
|
|||||||
div x y = mul x (inv y)
|
div x y = mul x (inv y)
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
negExt :: FExt -> FExt
|
||||||
|
negExt (r,i) = (neg r, neg i)
|
||||||
|
|
||||||
|
addExt :: FExt -> FExt -> FExt
|
||||||
|
addExt (r1,i1) (r2,i2) = (add r1 r2, add i1 i2)
|
||||||
|
|
||||||
|
subExt :: FExt -> FExt -> FExt
|
||||||
|
subExt (r1,i1) (r2,i2) = (sub r1 r2, sub i1 i2)
|
||||||
|
|
||||||
|
mulExt :: FExt -> FExt -> FExt
|
||||||
|
mulExt (r1,i1) (r2,i2) = (r3,i3) where
|
||||||
|
r3 = (mul r1 r2) `add` (mul3 7 i1 i2)
|
||||||
|
i3 = (mul r1 i2) `add` (mul i1 r2)
|
||||||
|
|
||||||
|
sqrExt :: FExt -> FExt
|
||||||
|
sqrExt x = mulExt x x
|
||||||
|
|
||||||
|
powExt :: FExt -> Int -> FExt
|
||||||
|
powExt x0 expo
|
||||||
|
| expo < 0 = error "pow: negative exponent"
|
||||||
|
| expo == 0 = (1,0)
|
||||||
|
| otherwise = go (1,0) x0 expo
|
||||||
|
where
|
||||||
|
go acc s 0 = acc
|
||||||
|
go acc s e = case divMod e 2 of
|
||||||
|
(e', 0) -> go acc (sqrExt s) e'
|
||||||
|
(e' ,1) -> go (mulExt acc s) (sqrExt s) e'
|
||||||
|
|
||||||
|
invExt :: FExt -> FExt
|
||||||
|
invExt (r,i) = (r `mul` z , neg i `mul` z) where
|
||||||
|
denom = (sqr r) `sub` (mul3 7 i i)
|
||||||
|
z = inv denom
|
||||||
|
|
||||||
|
divExt :: FExt -> FExt -> FExt
|
||||||
|
divExt x y = mulExt x (invExt y)
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- some quick & dirty testing
|
||||||
|
|
||||||
|
data Prop a
|
||||||
|
= Prop1 String (a -> Bool)
|
||||||
|
| Prop2 String (a -> a -> Bool)
|
||||||
|
| Prop3 String (a -> a -> a -> Bool)
|
||||||
|
|
||||||
|
propName :: Prop a -> String
|
||||||
|
propName prop = case prop of
|
||||||
|
Prop1 name _ -> name
|
||||||
|
Prop2 name _ -> name
|
||||||
|
Prop3 name _ -> name
|
||||||
|
|
||||||
|
some_properties :: [Prop F]
|
||||||
|
some_properties =
|
||||||
|
[ Prop2 "add-sub" \x y -> add (sub x y) y == x
|
||||||
|
, Prop2 "add-neg" \x y -> sub x y == add x (neg y)
|
||||||
|
, Prop1 "inv-mul" \x -> x == 0 || inv x `mul` x == 1
|
||||||
|
, Prop1 "inv-pow" \x -> inv x == pow x (fieldPrime - 2)
|
||||||
|
, Prop2 "mul-div" \x y -> y == 0 || mul (div x y) y == x
|
||||||
|
, Prop3 "mul-add" \x y z -> mul (add x y) z == mul x z `add` mul y z
|
||||||
|
, Prop1 "mul-pow" \x -> mul (mul x x) x == pow x 3
|
||||||
|
]
|
||||||
|
|
||||||
|
some_ext_properties :: [Prop FExt]
|
||||||
|
some_ext_properties =
|
||||||
|
[ Prop2 "add-sub" \x y -> addExt (subExt x y) y == x
|
||||||
|
, Prop2 "add-neg" \x y -> subExt x y == addExt x (negExt y)
|
||||||
|
, Prop1 "inv-mul" \x -> x == (0,0) || invExt x `mulExt` x == (1,0)
|
||||||
|
, Prop1 "inv-pow" \x -> invExt x == powExt x (fieldPrime^2 - 2)
|
||||||
|
, Prop2 "mul-div" \x y -> y == (0,0) || mulExt (divExt x y) y == x
|
||||||
|
, Prop3 "mul-add" \x y z -> mulExt (addExt x y) z == mulExt x z `addExt` mulExt y z
|
||||||
|
, Prop1 "mul-pow" \x -> mulExt (mulExt x x) x == powExt x 3
|
||||||
|
]
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
runTests :: IO ()
|
||||||
|
runTests = do
|
||||||
|
let n = 1000
|
||||||
|
runTestsBase n
|
||||||
|
runTestsExt n
|
||||||
|
|
||||||
|
runTestsBase :: Int -> IO ()
|
||||||
|
runTestsBase n = do
|
||||||
|
putStrLn $ "\nbase field properties"
|
||||||
|
forM_ some_properties $ \prop -> do
|
||||||
|
oks <- replicateM n (runPropF prop)
|
||||||
|
let good = length (filter id oks)
|
||||||
|
let bad = if good < n then " - FAILED!" else " - OK."
|
||||||
|
putStrLn $ " - " ++ propName prop ++ ": " ++ show good ++ " / " ++ show n ++ " passed. " ++ bad
|
||||||
|
|
||||||
|
runTestsExt :: Int -> IO ()
|
||||||
|
runTestsExt n = do
|
||||||
|
putStrLn $ "\nextension field properties"
|
||||||
|
forM_ some_ext_properties $ \prop -> do
|
||||||
|
oks <- replicateM n (runPropFExt prop)
|
||||||
|
let good = length (filter id oks)
|
||||||
|
let bad = if good < n then " - FAILED!" else " - OK."
|
||||||
|
putStrLn $ " - " ++ propName prop ++ ": " ++ show good ++ " / " ++ show n ++ " passed. " ++ bad
|
||||||
|
|
||||||
|
----------------------------------------
|
||||||
|
|
||||||
|
rndF :: IO F
|
||||||
|
rndF = randomRIO (0,fieldPrime-1)
|
||||||
|
|
||||||
|
rndFExt :: IO FExt
|
||||||
|
rndFExt = (,) <$> rndF <*> rndF
|
||||||
|
|
||||||
|
runPropF :: Prop F -> IO Bool
|
||||||
|
runPropF prop = case prop of
|
||||||
|
Prop1 _ f1 -> f1 <$> rndF
|
||||||
|
Prop2 _ f2 -> f2 <$> rndF <*> rndF
|
||||||
|
Prop3 _ f3 -> f3 <$> rndF <*> rndF <*> rndF
|
||||||
|
|
||||||
|
runPropFExt :: Prop FExt -> IO Bool
|
||||||
|
runPropFExt prop = case prop of
|
||||||
|
Prop1 _ f1 -> f1 <$> rndFExt
|
||||||
|
Prop2 _ f2 -> f2 <$> rndFExt <*> rndFExt
|
||||||
|
Prop3 _ f3 -> f3 <$> rndFExt <*> rndFExt <*> rndFExt
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|||||||
@ -18,6 +18,7 @@ data Op
|
|||||||
= Neg
|
= Neg
|
||||||
| Add
|
| Add
|
||||||
| Sub
|
| Sub
|
||||||
|
| Sqr
|
||||||
| Mul
|
| Mul
|
||||||
| Inv
|
| Inv
|
||||||
| Div
|
| Div
|
||||||
@ -34,6 +35,7 @@ mainComponent op =
|
|||||||
Neg -> unary "Neg"
|
Neg -> unary "Neg"
|
||||||
Add -> binary "Add"
|
Add -> binary "Add"
|
||||||
Sub -> binary "Sub"
|
Sub -> binary "Sub"
|
||||||
|
Sqr -> unary "Sqr"
|
||||||
Mul -> binary "Mul"
|
Mul -> binary "Mul"
|
||||||
Inv -> unary "Inv"
|
Inv -> unary "Inv"
|
||||||
Div -> binary "Div"
|
Div -> binary "Div"
|
||||||
@ -81,6 +83,9 @@ semantics_add (x,y) = Expecting $ Semantics.add x y
|
|||||||
semantics_sub :: (F,F) -> Expected F
|
semantics_sub :: (F,F) -> Expected F
|
||||||
semantics_sub (x,y) = Expecting $ Semantics.sub x y
|
semantics_sub (x,y) = Expecting $ Semantics.sub x y
|
||||||
|
|
||||||
|
semantics_sqr :: F -> Expected F
|
||||||
|
semantics_sqr x = Expecting $ Semantics.sqr x
|
||||||
|
|
||||||
semantics_mul :: (F,F) -> Expected F
|
semantics_mul :: (F,F) -> Expected F
|
||||||
semantics_mul (x,y) = Expecting $ Semantics.mul x y
|
semantics_mul (x,y) = Expecting $ Semantics.mul x y
|
||||||
|
|
||||||
|
|||||||
118
tests/TestGoldilocksExt.hs
Normal file
118
tests/TestGoldilocksExt.hs
Normal file
@ -0,0 +1,118 @@
|
|||||||
|
|
||||||
|
|
||||||
|
module TestGoldilocksExt where
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
import Control.Monad
|
||||||
|
import System.IO.Unsafe
|
||||||
|
|
||||||
|
import Semantics
|
||||||
|
import Common
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- global parameters
|
||||||
|
|
||||||
|
circomFile :: FilePath
|
||||||
|
circomFile = circuitSourceDir </> "test_wrapper_ext.circom"
|
||||||
|
|
||||||
|
data Op
|
||||||
|
= Neg
|
||||||
|
| Add
|
||||||
|
| Sub
|
||||||
|
| Sqr
|
||||||
|
| Mul
|
||||||
|
| Inv
|
||||||
|
| Div
|
||||||
|
deriving (Eq,Show,Bounded,Enum)
|
||||||
|
|
||||||
|
enumerateOps :: [Op]
|
||||||
|
enumerateOps = enumFromTo minBound maxBound
|
||||||
|
|
||||||
|
----------------------------------------
|
||||||
|
|
||||||
|
mainComponent :: Op -> MainComponent
|
||||||
|
mainComponent op =
|
||||||
|
case op of
|
||||||
|
Neg -> unary "NegExt"
|
||||||
|
Add -> binary "AddExt"
|
||||||
|
Sub -> binary "SubExt"
|
||||||
|
Sqr -> unary "SqrExt"
|
||||||
|
Mul -> binary "MulExt"
|
||||||
|
Inv -> unary "InvExt"
|
||||||
|
Div -> binary "DivExt"
|
||||||
|
where
|
||||||
|
|
||||||
|
unary name = MainComponent
|
||||||
|
{ _templateName = name ++ "Wrapper"
|
||||||
|
, _templateParams = []
|
||||||
|
, _publicInputs = ["A"]
|
||||||
|
}
|
||||||
|
|
||||||
|
binary name = MainComponent
|
||||||
|
{ _templateName = name ++ "Wrapper"
|
||||||
|
, _templateParams = []
|
||||||
|
, _publicInputs = ["A","B"]
|
||||||
|
}
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- test cases and expected semantics
|
||||||
|
|
||||||
|
type TestCase1 = (Int,Int)
|
||||||
|
type TestCase2 = ((Int,Int),(Int,Int))
|
||||||
|
|
||||||
|
type Output = (Int,Int)
|
||||||
|
|
||||||
|
nNestCases = 10
|
||||||
|
|
||||||
|
randomTestCasesUnary :: [TestCase1]
|
||||||
|
randomTestCasesUnary = unsafePerformIO $ replicateM nNestCases rndFExt
|
||||||
|
|
||||||
|
randomTestCasesBinary :: [TestCase2]
|
||||||
|
randomTestCasesBinary = unsafePerformIO $ replicateM nNestCases $ do { x <- rndFExt ; y <- rndFExt ; return (x,y) }
|
||||||
|
|
||||||
|
----------------------------------------
|
||||||
|
|
||||||
|
semantics_neg :: FExt -> Expected FExt
|
||||||
|
semantics_neg x = Expecting $ Semantics.negExt x
|
||||||
|
|
||||||
|
semantics_add :: (FExt,FExt) -> Expected FExt
|
||||||
|
semantics_add (x,y) = Expecting $ Semantics.addExt x y
|
||||||
|
|
||||||
|
semantics_sub :: (FExt,FExt) -> Expected FExt
|
||||||
|
semantics_sub (x,y) = Expecting $ Semantics.subExt x y
|
||||||
|
|
||||||
|
semantics_sqr :: FExt -> Expected FExt
|
||||||
|
semantics_sqr x = Expecting $ Semantics.sqrExt x
|
||||||
|
|
||||||
|
semantics_mul :: (FExt,FExt) -> Expected FExt
|
||||||
|
semantics_mul (x,y) = Expecting $ Semantics.mulExt x y
|
||||||
|
|
||||||
|
semantics_inv :: FExt -> Expected FExt
|
||||||
|
semantics_inv x = Expecting $ Semantics.invExt x
|
||||||
|
|
||||||
|
semantics_div :: (FExt,FExt) -> Expected FExt
|
||||||
|
semantics_div (x,y) = Expecting $ Semantics.divExt x y
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- inputs and outputs
|
||||||
|
|
||||||
|
inputsA :: TestCase1 -> Inputs Name Integer
|
||||||
|
inputsA a = Inputs $ toMapping "A" a
|
||||||
|
|
||||||
|
inputsAB :: TestCase2 -> Inputs Name Integer
|
||||||
|
inputsAB (a,b) = Inputs $ toMapping "A" a
|
||||||
|
<> toMapping "B" b
|
||||||
|
|
||||||
|
outputsC :: Output -> Outputs Name Integer
|
||||||
|
outputsC y = Outputs $ toMapping "C" y
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
specUnary :: Op -> (FExt -> Expected FExt) -> TestSpec TestCase1 Output
|
||||||
|
specUnary op semantics = TestSpec circomFile (mainComponent op) inputsA outputsC semantics randomTestCasesUnary
|
||||||
|
|
||||||
|
specBinary :: Op -> ((FExt,FExt) -> Expected FExt) -> TestSpec TestCase2 Output
|
||||||
|
specBinary op semantics = TestSpec circomFile (mainComponent op) inputsAB outputsC semantics randomTestCasesBinary
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
Loading…
x
Reference in New Issue
Block a user