Merge pull request #2 from l-adic/sized-vector

use sized-vector instead of vec package

Author: martyall

Diff for: arithmetic-circuits.cabal

@@ -45,14 +45,14 @@ common deps
     , base            >=4.10  && <5
     , containers      >=0.6.0
     , filepath        >=1.4.2
+    , finite-typelits >=0.1.0
     , galois-field    >=2.0.0
-    , fin
     , process
     , propagators
     , protolude       >=0.2
     , semirings       >=0.7
     , text            >=1.2.3
-    , vec
+    , vector-sized
     , wl-pprint-text  >=1.2.0
 
 library
@@ -128,6 +128,7 @@ test-suite circuit-tests
       arithmetic-circuits
     , array
     , distributive 
+    , fin
     , integer-logarithms
     , quickcheck-instances  >=0.3
     , QuickCheck
@@ -137,6 +138,7 @@ test-suite circuit-tests
     , tasty-hunit           >=0.10
     , tasty-hspec
     , tasty-quickcheck      >=0.10
+    , vec
 
   build-tool-depends: tasty-discover:tasty-discover >=4.2
 

Diff for: src/Circuit/Expr.hs

@@ -27,20 +27,18 @@ module Circuit.Expr
     evalExpr,
     rawWire,
     exprToArithCircuit,
-    type Nat.FromGHC,
   )
 where
 
 import Circuit.Affine
 import Circuit.Arithmetic
 import Data.Field.Galois (GaloisField, PrimeField (fromP))
-import Data.Fin (Fin)
+import Data.Finite (Finite)
 import Data.Map qualified as Map
 import Data.Semiring (Ring (..), Semiring (..))
 import Data.Set qualified as Set
-import Data.Type.Nat qualified as Nat
-import Data.Vec.Lazy (Vec, universe)
-import Data.Vec.Lazy qualified as Vec
+import Data.Vector.Sized (Vector)
+import Data.Vector.Sized qualified as V
 import Protolude hiding (Semiring)
 import Text.PrettyPrint.Leijen.Text hiding ((<$>))
 
@@ -92,7 +90,7 @@ rawWire :: Var i f ty -> i
 rawWire (VarField i) = i
 rawWire (VarBool i) = i
 
-type family NBits a :: Nat.Nat
+type family NBits a :: Nat
 
 -- | Expression data type of (arithmetic) expressions over a field @f@
 -- with variable names/indices coming from @i@.
@@ -103,9 +101,9 @@ data Expr i f t ty where
   EBinOp :: BinOp f ty -> Expr i f Identity ty -> Expr i f Identity ty -> Expr i f Identity ty
   EIf :: Expr i f Identity Bool -> Expr i f Identity ty -> Expr i f Identity ty -> Expr i f Identity ty
   EEq :: Expr i f Identity f -> Expr i f Identity f -> Expr i f Identity Bool
-  ESplit :: (Nat.SNatI (NBits f)) => Expr i f Identity f -> Expr i f (Vec (NBits f)) Bool
-  EJoin :: (Num f, Nat.SNatI n) => Expr i f (Vec n) Bool -> Expr i f Identity f
-  EAtIndex :: (Nat.SNatI n) => Expr i f (Vec n) ty -> Fin n -> Expr i f Identity ty
+  ESplit :: (KnownNat (NBits f)) => Expr i f Identity f -> Expr i f (Vector (NBits f)) Bool
+  EJoin :: (Num f, KnownNat n) => Expr i f (Vector n) Bool -> Expr i f Identity f
+  EAtIndex :: (KnownNat n) => Expr i f (Vector n) ty -> Finite n -> Expr i f Identity ty
 
 deriving instance (Show f) => Show (BinOp f a)
 
@@ -235,15 +233,15 @@ evalExpr' expr = case expr of
     pure $ Identity $ lhs' == rhs'
   ESplit i -> do
     x <- runIdentity <$> evalExpr' i
-    pure $ Vec.tabulate $ \ix -> testBit (fromP x) (fromIntegral ix)
+    pure $ V.generate $ \ix -> testBit (fromP x) (fromIntegral ix)
   EJoin i -> do
     bits <- evalExpr' i
     pure $
       Identity $
-        Vec.ifoldMap (\ix b -> if b then fromInteger (2 ^ fromIntegral @_ @Integer ix) else 0) bits
+        V.ifoldl (\acc ix b -> acc + if b then fromInteger (2 ^ fromIntegral @_ @Integer ix) else 0) 0 bits
   EAtIndex v i -> do
     _v <- evalExpr' v
-    pure $ Identity $ _v Vec.! i
+    pure $ Identity $ _v `V.index` i
 
 --   pure $ Vec.fromList $ map (testBit i) [0 .. Nat.toInt (Vec.length i) - 1]
 
@@ -442,7 +440,7 @@ compile expr = case expr of
   ESplit input -> do
     i <- compile input >>= addWire . runIdentity
     outputs <- traverse (\_ -> mkBoolVar =<< imm) $ universe @(NBits f)
-    emit $ Split i (Vec.toList outputs)
+    emit $ Split i (V.toList outputs)
     traverse (fmap runIdentity . compile . EVar . VarBool) outputs
     where
       mkBoolVar w = do
@@ -455,7 +453,7 @@ compile expr = case expr of
     pure . Identity . Right $ unsplit ws
   EAtIndex v ix -> do
     v' <- compile v
-    pure . Identity $ v' Vec.! ix
+    pure . Identity $ v' `V.index` ix
 
 exprToArithCircuit ::
   (Num f, Foldable t) =>
@@ -486,3 +484,6 @@ instance (GaloisField f) => Num (Expr Wire f Identity f) where
   abs = identity
   signum = const 1
   fromInteger = EVal . ValField . fromInteger
+
+universe :: (KnownNat n) => Vector n (Finite n)
+universe = V.enumFromN 0

Diff for: src/Circuit/Lang.hs

@@ -34,16 +34,15 @@ import Circuit.Affine (AffineCircuit (..))
 import Circuit.Arithmetic (Gate (..), InputType (Private, Public), Wire (..))
 import Circuit.Expr
 import Data.Field.Galois (GaloisField)
-import Data.Fin (Fin)
-import Data.Type.Nat qualified as Nat
-import Data.Vec.Lazy (Vec)
+import Data.Finite (Finite)
+import Data.Vector.Sized (Vector)
 import Protolude
 
 --------------------------------------------------------------------------------
 
 type Signal f a = Expr Wire f Identity a
 
-type Bundle f n a = Expr Wire f (Vec n) a
+type Bundle f n a = Expr Wire f (Vector n) a
 
 -- | Convert constant to expression
 cField :: f -> Signal f f
@@ -89,12 +88,12 @@ cond :: Signal f Bool -> Signal f ty -> Signal f ty -> Signal f ty
 cond = EIf
 
 splitBits ::
-  (Nat.SNatI (NBits f)) =>
+  (KnownNat (NBits f)) =>
   Signal f f ->
   Bundle f (NBits f) Bool
 splitBits = ESplit
 
-joinBits :: (Num f, Nat.SNatI n) => Bundle f n Bool -> Signal f f
+joinBits :: (Num f, KnownNat n) => Bundle f n Bool -> Signal f f
 joinBits = EJoin
 
 deref :: Var Wire f ty -> Signal f ty
@@ -119,7 +118,7 @@ retBool label = compileWithWire (boolInput Public label)
 retField :: (Num f) => Text -> Signal f f -> ExprM f Wire
 retField label = compileWithWire (fieldInput Public label)
 
-atIndex :: (Nat.SNatI n) => Bundle f n ty -> Fin n -> Signal f ty
+atIndex :: (KnownNat n) => Bundle f n ty -> Finite n -> Signal f ty
 atIndex = EAtIndex
 
 --------------------------------------------------------------------------------

Diff for: test/Test/Circuit/Lang.hs

@@ -1,20 +1,19 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# OPTIONS_GHC -freduction-depth=0 #-}
 
 module Test.Circuit.Lang where
 
 import Circuit
 import Data.Field.Galois (Prime, PrimeField (fromP))
-import Data.Fin (Fin)
+import Data.Finite (Finite)
 import Data.Map qualified as Map
 import Data.Maybe (fromJust)
 import Protolude hiding (Show, show)
 import Test.QuickCheck (Property, (==>))
 
 type Fr = Prime 21888242871839275222246405745257275088548364400416034343698204186575808495617
 
-type instance NBits (Prime p) = FromGHC 256
+type instance NBits (Prime p) = 256
 
 bitSplitJoin :: ExprM Fr Wire
 bitSplitJoin = do
@@ -59,7 +58,7 @@ prop_factorizationContra x y z =
         w = solve bsVars bsCircuit inputs
      in lookupVar bsVars "out" w == Just 0
 
-bitIndex :: Fin (NBits Fr) -> ExprM Fr Wire
+bitIndex :: Finite (NBits Fr) -> ExprM Fr Wire
 bitIndex i = do
   x <- deref <$> fieldInput Public "x"
   let bits = splitBits x