Beta normalize

.github/workflows/nix-ci.yml

@@ -20,11 +20,11 @@ jobs:
         repo: torsion-labs/arkworks-bridge
         tag: v0.2.0
 
-    - uses: cachix/install-nix-action@v22
+    - uses: cachix/install-nix-action@v24
       with:
         nix_path: nixpkgs=channel:nixos-unstable
 
-    - uses: cachix/cachix-action@v12
+    - uses: cachix/cachix-action@v13
       with:
         name: martyall
         authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'

app/Main.hs

@@ -4,10 +4,20 @@ import Control.Monad (unless)
 import qualified Data.ByteString.Lazy as LBS
 import Data.Field.Galois (PrimeField)
 import Data.Typeable (Typeable)
-import Snarkl.Compile (SimplParam (NoSimplify))
 import Snarkl.Errors (ErrMsg (ErrMsg), failWith)
-import Snarkl.Field
+import Snarkl.Field (F_BN128)
+import Snarkl.Language (Comp)
 import Snarkl.Toplevel
+  ( Result (..),
+    SimplParam (..),
+    execute,
+    mkInputsFilePath,
+    mkR1CSFilePath,
+    mkWitnessFilePath,
+    serializeInputsAsJson,
+    serializeR1CSAsJson,
+    serializeWitnessAsJson,
+  )
 import qualified Test.Snarkl.Unit.Programs as Programs
 
 main :: IO ()

benchmarks/Harness.hs

@@ -10,28 +10,25 @@ import qualified Data.ByteString.Lazy as LBS
 import Data.Field.Galois (GaloisField, Prime, PrimeField)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
-import Data.Typeable
-import GHC.IO.Exception
+import Data.Typeable (Typeable)
+import GHC.IO.Exception (ExitCode (..))
 import GHC.TypeLits (KnownNat)
 import Snarkl.Compile (SimplParam)
+import Snarkl.Constraint (ConstraintSystem (..), do_simplify)
 import Snarkl.Errors (ErrMsg (ErrMsg), failWith)
+import Snarkl.Language (Comp)
 import Snarkl.Language.TExpr
   ( TExp (..),
     lastSeq,
   )
 import Snarkl.Toplevel
-  ( Comp,
-    ConstraintSystem (..),
-    Result (..),
-    TExp (..),
+  ( Result (..),
     TExpPkg (..),
     comp_interp,
     compileCompToR1CS,
     compileCompToTexp,
     compileTexpToConstraints,
-    do_simplify,
     execute,
-    lastSeq,
     serializeR1CSAsJson,
     serializeWitnessAsJson,
     wit_of_r1cs,

benchmarks/Main.hs

@@ -14,7 +14,7 @@ import qualified Snarkl.Example.Keccak as Keccak
 import qualified Snarkl.Example.List as List
 import qualified Snarkl.Example.Matrix as Matrix
 import Snarkl.Field (F_BN128, P_BN128)
-import Snarkl.Language (Comp, fromField)
+import Snarkl.Syntax (Comp, fromField)
 
 mk_bgroup :: (Typeable ty) => String -> Comp ty F_BN128 -> [Int] -> F_BN128 -> Benchmark
 mk_bgroup nm mf inputs result =

examples/Snarkl/Example/Basic.hs

@@ -7,10 +7,8 @@ import Data.Typeable (Typeable)
 import GHC.TypeLits (KnownNat)
 import Snarkl.Compile
 import Snarkl.Field (F_BN128)
-import Snarkl.Language.Syntax
-import Snarkl.Language.SyntaxMonad
-import Snarkl.Language.TExpr
-import Snarkl.Toplevel
+import Snarkl.Syntax
+import Snarkl.Toplevel (R1CS, comp_interp)
 import System.Exit (ExitCode)
 import Prelude hiding
   ( fromRational,
@@ -31,7 +29,7 @@ mult_ex ::
   Comp 'TField k
 mult_ex x y = return $ x * y
 
-arr_ex :: (GaloisField k) => TExp 'TField k -> Comp 'TField k
+arr_ex :: TExp 'TField k -> Comp 'TField k
 arr_ex x = do
   a <- arr 2
   forall [0 .. 1] (\i -> set (a, i) x)
@@ -63,13 +61,13 @@ interp2' = comp_interp p2 [256]
 compile1 :: (GaloisField k) => R1CS k
 compile1 = compileCompToR1CS Simplify p1
 
-comp1 :: (GaloisField k, Typeable a) => Comp ('TSum 'TBool a) k
+comp1 :: (Typeable a) => Comp ('TSum 'TBool a) k
 comp1 = inl false
 
 comp2 :: (GaloisField k, Typeable a) => Comp ('TSum a 'TField) k
 comp2 = inr (fromField 0)
 
-test1 :: (GaloisField k) => State (Env k) (TExp 'TBool k)
+test1 :: (GaloisField k) => Comp 'TBool k
 test1 = do
   b <- fresh_input
   z <- if return b then comp1 else comp2

examples/Snarkl/Example/Games.hs

@@ -6,15 +6,13 @@
 
 module Snarkl.Example.Games where
 
-import Data.Field.Galois (GaloisField, Prime)
+import Data.Field.Galois (GaloisField)
+import Data.Kind (Type)
 import Data.Typeable
-import GHC.TypeLits (KnownNat, Nat)
 import Snarkl.Errors
 import Snarkl.Field (F_BN128)
-import Snarkl.Language.Syntax
-import Snarkl.Language.SyntaxMonad
-import Snarkl.Language.TExpr
-import Snarkl.Toplevel
+import Snarkl.Syntax
+import Snarkl.Toplevel (comp_interp)
 import Prelude hiding
   ( fromRational,
     negate,
@@ -38,7 +36,7 @@ data ISO (t :: Ty) (s :: Ty) k = Iso
     from :: TExp s k -> Comp t k
   }
 
-data Game :: Ty -> * -> * where
+data Game :: Ty -> Type -> Type where
   Single ::
     forall (s :: Ty) (t :: Ty) k.
     ( Typeable s,
@@ -108,8 +106,7 @@ sum_game ::
     Zippable t1 k,
     Zippable t2 k,
     Derive t1 k,
-    Derive t2 k,
-    GaloisField k
+    Derive t2 k
   ) =>
   Game t1 k ->
   Game t2 k ->
@@ -133,9 +130,7 @@ t2 :: F_BN128
 t2 = comp_interp basic_test [1, 23, 88] -- 88
 
 (+>) ::
-  ( Typeable t,
-    Typeable s,
-    Zippable t k,
+  ( Typeable s,
     Zippable s k
   ) =>
   Game t k ->
@@ -151,8 +146,7 @@ prodI ::
   ( Typeable a,
     Typeable b,
     Typeable c,
-    Typeable d,
-    GaloisField k
+    Typeable d
   ) =>
   ISO a b k ->
   ISO c d k ->
@@ -174,13 +168,12 @@ prodI (Iso f g) (Iso f' g') =
         pair y1 y2
     )
 
-seqI :: (Typeable b) => ISO a b p -> ISO b c p -> ISO a c p
+seqI :: ISO a b p -> ISO b c p -> ISO a c p
 seqI (Iso f g) (Iso f' g') = Iso (\a -> f a >>= f') (\c -> g' c >>= g)
 
 prodLInputI ::
   ( Typeable a,
-    Typeable b,
-    GaloisField k
+    Typeable b
   ) =>
   ISO ('TProd a b) b k
 prodLInputI =
@@ -200,8 +193,7 @@ prodLSumI ::
     Zippable c k,
     Derive a k,
     Derive b k,
-    Derive c k,
-    GaloisField k
+    Derive c k
   ) =>
   ISO ('TProd ('TSum b c) a) ('TSum ('TProd b a) ('TProd c a)) k
 prodLSumI =
@@ -301,8 +293,7 @@ instance (GaloisField k) => Gameable 'TUnit k where
   mkGame = unit_game
 
 instance
-  ( Typeable a,
-    Typeable b,
+  ( Typeable b,
     Zippable a k,
     Zippable b k,
     Derive a k,
@@ -323,8 +314,7 @@ instance
     Derive a k,
     Derive b k,
     Gameable a k,
-    Gameable b k,
-    GaloisField k
+    Gameable b k
   ) =>
   Gameable ('TSum a b) k
   where

examples/Snarkl/Example/Keccak.hs

@@ -9,10 +9,7 @@ import Data.Bits hiding (xor)
 import Data.Field.Galois (GaloisField, Prime)
 import qualified Data.Map.Strict as Map
 import GHC.TypeLits (KnownNat)
-import Snarkl.Language.Syntax
-import Snarkl.Language.SyntaxMonad
-import Snarkl.Language.TExpr
-import Snarkl.Toplevel
+import Snarkl.Syntax
 import Prelude hiding
   ( fromRational,
     negate,
@@ -35,7 +32,6 @@ ln_width :: Int
 ln_width = 32
 
 round1 ::
-  (GaloisField k) =>
   (Int -> TExp 'TBool k) ->
   -- | 'i'th bit of round constant
   TExp ('TArr ('TArr ('TArr 'TBool))) k ->
@@ -198,7 +194,7 @@ keccak_f1 num_rounds a =
     )
 
 -- num_rounds = 12+2l, where 2^l = ln_width
-keccak1 :: (GaloisField k) => Int -> Comp 'TBool k
+keccak1 :: Int -> Comp 'TBool k
 keccak1 num_rounds =
   do
     a <- input_arr3 5 5 ln_width

examples/Snarkl/Example/Lam.hs

@@ -10,9 +10,7 @@ import Data.Field.Galois (GaloisField, Prime)
 import Data.Typeable
 import GHC.TypeLits (KnownNat)
 import Snarkl.Errors
-import Snarkl.Language.Syntax
-import Snarkl.Language.SyntaxMonad
-import Snarkl.Language.TExpr
+import Snarkl.Syntax
 import Prelude hiding
   ( fromRational,
     negate,
@@ -35,7 +33,7 @@ type TFSubst = 'TFSum ('TFConst 'TField) ('TFProd ('TFConst TTerm) 'TFId)
 
 type TSubst = 'TMu TFSubst
 
-subst_nil :: (GaloisField k) => TExp 'TField k -> State (Env k) (TExp TSubst k)
+subst_nil :: TExp 'TField k -> Comp TSubst k
 subst_nil n =
   do
     n' <- inl n
@@ -68,7 +66,6 @@ type TF = 'TFSum ('TFConst 'TField) ('TFSum 'TFId ('TFProd 'TFId 'TFId))
 type TTerm = 'TMu TF
 
 varN ::
-  (GaloisField k) =>
   TExp 'TField k ->
   Comp TTerm k
 varN e =
@@ -86,7 +83,6 @@ varN' i =
     roll v
 
 lam ::
-  (GaloisField k) =>
   TExp TTerm k ->
   Comp TTerm k
 lam t =
@@ -96,7 +92,6 @@ lam t =
     roll v
 
 app ::
-  (GaloisField k) =>
   TExp TTerm k ->
   TExp TTerm k ->
   Comp TTerm k
@@ -108,9 +103,7 @@ app t1 t2 =
     roll v
 
 case_term ::
-  ( Typeable ty,
-    Zippable ty k,
-    GaloisField k
+  ( Zippable ty k
   ) =>
   TExp TTerm k ->
   (TExp 'TField k -> Comp ty k) ->
@@ -128,7 +121,7 @@ case_term t f_var f_lam f_app =
         e2 <- fst_pair p
         f_app e1 e2
 
-is_lam :: (GaloisField k) => TExp TTerm k -> Comp 'TBool k
+is_lam :: TExp TTerm k -> Comp 'TBool k
 is_lam t =
   case_term
     t
@@ -159,7 +152,7 @@ shift n t = fix go t
               app t1' t2'
         )
 
-compose :: (GaloisField k) => TExp TSubst k -> TExp ('TMu TFSubst) k -> State (Env k) (TExp ('TMu TFSubst) k)
+compose :: (GaloisField k) => TExp TSubst k -> TExp ('TMu TFSubst) k -> Comp ('TMu TFSubst) k
 compose sigma1 sigma2 =
   do
     p <- pair sigma1 sigma2
@@ -192,7 +185,7 @@ compose sigma1 sigma2 =
                     subst_cons t'' s2''
               )
 
-subst_term :: (GaloisField k) => TExp ('TMu TFSubst) k -> TExp TTerm k -> State (Env k) (TExp ('TMu TF) k)
+subst_term :: (GaloisField k) => TExp ('TMu TFSubst) k -> TExp TTerm k -> Comp ('TMu TF) k
 subst_term sigma t =
   do
     p <- pair sigma t