Merge pull request #351 from zkFold/hov-const-optim

Optimize Arithmetic Circuits
zkFold · Nov 18, 2024 · 245785c · 245785c
2 parents 6da2598 + e39db59
commit 245785c
Show file tree

Hide file tree

Showing 20 changed files with 137 additions and 51 deletions.
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/Basic/Class.hs b/symbolic-base/src/ZkFold/Base/Algebra/Basic/Class.hs
@@ -690,3 +690,77 @@ instance FromConstant b a => FromConstant b (p -> a) where
 instance Semiring a => Semiring (p -> a)
 
 instance Ring a => Ring (p -> a)
+
+---------------------------------------------------------------------------------
+
+instance Finite a => Finite (Maybe a) where
+    type Order (Maybe a) = Order a
+
+instance FromConstant Integer a => FromConstant Integer (Maybe a) where
+    fromConstant = Just . fromConstant
+
+instance FromConstant Natural a => FromConstant Natural (Maybe a) where
+    fromConstant = Just . fromConstant
+
+instance AdditiveSemigroup a => AdditiveSemigroup (Maybe a) where
+    (+) :: Maybe a -> Maybe a -> Maybe a
+    (+) = liftA2 (+)
+
+instance MultiplicativeSemigroup a => MultiplicativeSemigroup (Maybe a) where
+    (*) :: Maybe a -> Maybe a -> Maybe a
+    (*) = liftA2 (*)
+
+instance Scale Natural a => Scale Natural (Maybe a) where
+    scale = fmap . scale
+
+instance Scale Integer a => Scale Integer (Maybe a) where
+    scale = fmap . scale
+
+instance AdditiveMonoid a => AdditiveMonoid (Maybe a) where
+    zero :: Maybe a
+    zero = Just zero
+
+instance Exponent a Natural => Exponent (Maybe a) Natural where
+    (^) :: Maybe a -> Natural -> Maybe a
+    (^) m n = liftA2 (^) m (Just n)
+
+instance Exponent a Integer => Exponent (Maybe a) Integer where
+    (^) :: Maybe a -> Integer -> Maybe a
+    (^) m n = liftA2 (^) m (Just n)
+
+instance MultiplicativeMonoid a => MultiplicativeMonoid (Maybe a) where
+    one :: Maybe a
+    one = Just one
+
+instance Semiring a => Semiring (Maybe a)
+
+instance AdditiveGroup a => AdditiveGroup (Maybe a) where
+    negate :: Maybe a -> Maybe a
+    negate = fmap negate
+
+instance Ring a => Ring (Maybe a)
+
+instance Field a => Field (Maybe a) where
+    finv :: Maybe a -> Maybe a
+    finv = fmap finv
+
+    rootOfUnity :: Natural -> Maybe (Maybe a)
+    rootOfUnity = Just . rootOfUnity @a
+
+instance ToConstant a => ToConstant (Maybe a) where
+    type Const (Maybe a) = Maybe (Const a)
+    toConstant :: Maybe a -> Maybe (Const a)
+    toConstant = fmap toConstant
+
+instance Scale a a => Scale a (Maybe a) where
+    scale s = fmap (scale s)
+
+instance FromConstant a (Maybe a) where
+    fromConstant = Just
+
+instance FromConstant Natural a => FromConstant (Maybe Natural) (Maybe a) where
+    fromConstant = fmap fromConstant
+
+instance SemiEuclidean Natural => SemiEuclidean (Maybe Natural) where
+    divMod (Just a) (Just b) = let (d, m) = divMod a b in (Just d, Just m)
+    divMod _ _               = (Nothing, Nothing)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs
@@ -85,7 +85,9 @@ toPlonkConstraint p =
             return $ PlonkConstraint qm ql qr qo qc va vb vc
         getCoefs _ = Nothing
 
-    in head $ mapMaybe getCoefs perms
+    in case mapMaybe getCoefs perms of
+        [] -> toPlonkConstraint zero
+        _  -> head $ mapMaybe getCoefs perms
 
 fromPlonkConstraint :: (Ord a, Field a, KnownNat i) => PlonkConstraint i a -> Poly a (Var a (Vector i)) Natural
 fromPlonkConstraint (PlonkConstraint qm ql qr qo qc a b c) =

diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs
@@ -199,24 +199,33 @@ instance
   ( Arithmetic a, Binary a, Representable i, Binary (Rep i), Ord (Rep i)
   , o ~ U1) => MonadCircuit (Var a i) a (WitnessF a (SysVar i)) (State (ArithmeticCircuit a i o)) where
 
-    unconstrained wf = do
-      let v = toVar @a wf
-      -- TODO: forbid reassignment of variables
-      zoom #acWitness $ modify (insert v wf)
-      return $ SysVar (NewVar v)
+    unconstrained wf = case runWitnessF wf $ const Nothing of
+      Just cV -> return (ConstVar cV)
+      Nothing -> do
+        let v = toVar @a wf
+        -- TODO: forbid reassignment of variables
+        zoom #acWitness $ modify (insert v wf)
+        return $ SysVar (NewVar v)
 
     constraint p =
-      let
-        evalConstVar = \case
-          SysVar sysV -> var sysV
-          ConstVar cV -> fromConstant cV
-      in
-        zoom #acSystem . modify $ insert (toVar (p at)) (p evalConstVar)
+      let evalConstVar = \case
+            SysVar sysV -> var sysV
+            ConstVar cV -> fromConstant cV
+          evalMaybe = \case
+            SysVar _ -> Nothing
+            ConstVar cV -> Just cV
+      in case p evalMaybe of
+        Just c -> if c ==zero
+                    then return ()
+                    else error "The constraint is non-zero"
+        Nothing -> zoom #acSystem . modify $ insert (toVar (p at)) (p evalConstVar)
 
     rangeConstraint (SysVar v) upperBound =
       zoom #acRange . modify $ insertWith S.union upperBound (S.singleton v)
-    -- FIXME range-constrain other variable types
-    rangeConstraint _ _ = error "Cannot range-constrain this variable"
+    rangeConstraint (ConstVar c) upperBound =
+      if c <= upperBound
+        then return ()
+        else error "The constant does not belong to the interval"
 
 -- | Generates new variable index given a witness for it.
 --

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs
@@ -70,7 +70,7 @@ fromBits hiBits loBits bits = do
     highNew <- horner . Haskell.reverse $  bitsHighNew
     pure $ highNew : lowsNew
 
-data RegisterSize = Auto | Fixed Natural
+data RegisterSize = Auto | Fixed Natural deriving (Haskell.Eq)
 
 class KnownRegisterSize (r :: RegisterSize) where
   regSize :: RegisterSize

diff --git a/symbolic-base/test/Tests/UInt.hs b/symbolic-base/test/Tests/UInt.hs
@@ -33,8 +33,9 @@ import           ZkFold.Symbolic.Class                       (Arithmetic)
 import           ZkFold.Symbolic.Compiler                    (ArithmeticCircuit, exec)
 import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.ByteString
-import           ZkFold.Symbolic.Data.Combinators            (Ceil, GetRegisterSize, Iso (..), KnownRegisterSize,
-                                                              NumberOfRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Combinators            (Ceil, GetRegisterSize, Iso (..),
+                                                              KnownRegisterSize (regSize), NumberOfRegisters,
+                                                              RegisterSize (..))
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Ord
 import           ZkFold.Symbolic.Data.UInt
@@ -113,8 +114,8 @@ specUInt' = hspec $ do
         it "negates correctly" $ do
             x <- toss m
             return $ execAcUint @(Zp p) @n @rs (negate (fromConstant x)) === execZpUint @_ @n @rs (negate (fromConstant x))
-        it "subtracts correctly" $ isHom @n @p @rs (-) (-) (overflowSub @n) <$> toss m <*> toss m
-        it "multiplies correctly" $ isHom @n @p @rs (*) (*) (*) <$> toss m <*> toss m
+        when (regSize @rs == Auto) $ it "subtracts correctly" $ isHom @n @p @rs (-) (-) (overflowSub @n) <$> toss m <*> toss m
+        when (regSize @rs == Auto) $ it "multiplies correctly" $ isHom @n @p @rs (*) (*) (*) <$> toss m <*> toss m
         it "iso uint correctly" $ do
             x <- toss m
             let bx = fromConstant x :: ByteString n (ArithmeticCircuit (Zp p) U1)
@@ -126,7 +127,7 @@ specUInt' = hspec $ do
                 bx = fromConstant x :: ByteString n (ArithmeticCircuit (Zp p) U1)
             return $ evalBS (from ux :: ByteString n (ArithmeticCircuit (Zp p) U1)) === evalBS bx
 
-        when (n <= 128) $ it "performs divMod correctly" $ withMaxSuccess 10 $ do
+        when (n <= 128 && regSize @rs == Auto) $ it "performs divMod correctly" $ withMaxSuccess 10 $ do
             num <- toss m
             d <- toss m
             let (acQ, acR) = (fromConstant num :: UInt n rs (ArithmeticCircuit (Zp p) U1)) `divMod` fromConstant d

diff --git a/symbolic-examples/stats/ByteString.Add.512 b/symbolic-examples/stats/ByteString.Add.512
@@ -1,4 +1,4 @@
 ByteString.Add.512
-Number of constraints: 5639
-Number of variables: 6150
+Number of constraints: 5638
+Number of variables: 6149
 Number of range lookups: 522
diff --git a/symbolic-examples/stats/ByteString.Extend.1.512 b/symbolic-examples/stats/ByteString.Extend.1.512
@@ -1,4 +1,4 @@
 ByteString.Extend.1.512
-Number of constraints: 6
-Number of variables: 5
+Number of constraints: 5
+Number of variables: 4
 Number of range lookups: 0
diff --git a/symbolic-examples/stats/Constant.5 b/symbolic-examples/stats/Constant.5
@@ -1,4 +1,4 @@
 Constant.5
-Number of constraints: 1
+Number of constraints: 0
 Number of variables: 0
 Number of range lookups: 0
diff --git a/symbolic-examples/stats/Eq b/symbolic-examples/stats/Eq
@@ -1,4 +1,4 @@
 Eq
-Number of constraints: 7
-Number of variables: 6
+Number of constraints: 4
+Number of variables: 4
 Number of range lookups: 0
diff --git a/symbolic-examples/stats/Eq.Constant.5 b/symbolic-examples/stats/Eq.Constant.5
@@ -1,4 +1,4 @@
 Eq.Constant.5
-Number of constraints: 6
-Number of variables: 5
+Number of constraints: 4
+Number of variables: 4
 Number of range lookups: 0
diff --git a/symbolic-examples/stats/FFA.Add.097 b/symbolic-examples/stats/FFA.Add.097
@@ -1,4 +1,4 @@
 FFA.Add.097
-Number of constraints: 18873
-Number of variables: 23899
+Number of constraints: 18859
+Number of variables: 23886
 Number of range lookups: 11916
diff --git a/symbolic-examples/stats/FFA.Add.337 b/symbolic-examples/stats/FFA.Add.337
@@ -1,4 +1,4 @@
 FFA.Add.337
-Number of constraints: 18873
-Number of variables: 23899
+Number of constraints: 18859
+Number of variables: 23886
 Number of range lookups: 11916
diff --git a/symbolic-examples/stats/FFA.Mul.097 b/symbolic-examples/stats/FFA.Mul.097
@@ -1,4 +1,4 @@
 FFA.Mul.097
-Number of constraints: 18901
-Number of variables: 23941
+Number of constraints: 18887
+Number of variables: 23928
 Number of range lookups: 11944
diff --git a/symbolic-examples/stats/FFA.Mul.337 b/symbolic-examples/stats/FFA.Mul.337
@@ -1,4 +1,4 @@
 FFA.Mul.337
-Number of constraints: 18901
-Number of variables: 23941
+Number of constraints: 18887
+Number of variables: 23928
 Number of range lookups: 11944
diff --git a/symbolic-examples/stats/Fibonacci.100 b/symbolic-examples/stats/Fibonacci.100
@@ -1,4 +1,4 @@
 Fibonacci.100
-Number of constraints: 796
-Number of variables: 795
+Number of constraints: 696
+Number of variables: 696
 Number of range lookups: 0
diff --git a/symbolic-examples/stats/LEQ b/symbolic-examples/stats/LEQ
@@ -1,4 +1,4 @@
 LEQ
-Number of constraints: 3065
-Number of variables: 4082
+Number of constraints: 3060
+Number of variables: 4078
 Number of range lookups: 2040
diff --git a/symbolic-examples/stats/MiMCHash b/symbolic-examples/stats/MiMCHash
@@ -1,4 +1,4 @@
 MiMCHash
-Number of constraints: 1763
-Number of variables: 1762
+Number of constraints: 1760
+Number of variables: 1760
 Number of range lookups: 0
diff --git a/symbolic-examples/stats/SHA256.32 b/symbolic-examples/stats/SHA256.32
@@ -1,4 +1,4 @@
 SHA256.32
-Number of constraints: 53761
-Number of variables: 64018
-Number of range lookups: 11156
+Number of constraints: 50680
+Number of variables: 60797
+Number of range lookups: 10996
diff --git a/symbolic-examples/stats/UInt.DivMod.32.Auto b/symbolic-examples/stats/UInt.DivMod.32.Auto
@@ -1,4 +1,4 @@
 UInt.DivMod.32.Auto
-Number of constraints: 1430
-Number of variables: 1780
-Number of range lookups: 770
+Number of constraints: 1422
+Number of variables: 1770
+Number of range lookups: 766
diff --git a/symbolic-examples/stats/UInt.StrictAdd.256.Auto b/symbolic-examples/stats/UInt.StrictAdd.256.Auto
@@ -1,4 +1,4 @@
 UInt.StrictAdd.256.Auto
-Number of constraints: 547
-Number of variables: 1055
+Number of constraints: 546
+Number of variables: 1054
 Number of range lookups: 518