Merge pull request #3 from l-adic/update-snarkl

update snarkl to lates

cabal.project

@@ -28,7 +28,7 @@ source-repository-package
 source-repository-package
  type: git
  location: https://github.com/l-adic/snarkl.git
- tag: 5d539a7827f570ee6e9dbf9a30e898acccd6c0cb
+ tag: c2561b898d93fd444ca57aaf8b2ad8b203f19489
  --sha256: jHy2OKlvSgBAkvtadvDVB0t3Hr2wTgXTFKW5T2t/yi0=
 
 source-repository-package

examples/Examples.hs

@@ -15,10 +15,10 @@ import qualified Snarkl.Toplevel as Snarkl
 
 -- | Little helper to get our expressions into a form that Hedgehog can compare.
 comparable :: (Typeable ty, GaloisField k) => Snarkl.Comp ty k -> String
-comparable = show . Snarkl.compileCompToR1CS Snarkl.Simplify
+comparable = show . Snarkl.compileCompToR1CS [Snarkl.Simplify]
 
 interpretable :: (Typeable ty, GaloisField k) => Snarkl.Comp ty k -> [k] -> k
-interpretable = Snarkl.comp_interp
+interpretable comp is = Snarkl.comp_interp comp is mempty
 
 prop_simple_bool :: Hedgehog.Property
 prop_simple_bool =

examples/Examples/Arithmetic.hs

@@ -7,8 +7,8 @@ module Examples.Arithmetic (simpleBool, simpleArith) where
 import qualified Categorifier.Categorify as Categorify
 import Categorifier.Vec.Client ()
 import Snarkl.Field (F_BN128)
-import Snarkl.Language (Ty (..), pair, (>>=))
-import qualified Snarkl.Language.SyntaxMonad as Snarkl
+import Snarkl.Language.Prelude (Ty (..), pair, (>>=))
+import qualified Snarkl.Language.Prelude as Snarkl
 import Stalk (Stalk (runStalk))
 import Prelude (Bool (..), fromInteger, (*), (+), (-), (==))
 
@@ -33,7 +33,7 @@ simpleArith =
       compiledProg :: Stalk F_BN128 F_BN128 F_BN128
       compiledProg = Categorify.expression prog
    in do
-        z <- Snarkl.fresh_input
+        z <- Snarkl.fresh_public_input
         runStalk compiledProg z
 
 {-
@@ -57,7 +57,7 @@ simpleBool =
       compiledProg :: Stalk F_BN128 (F_BN128, F_BN128) F_BN128
       compiledProg = Categorify.expression prog
    in do
-        x <- Snarkl.fresh_input
-        y <- Snarkl.fresh_input
+        x <- Snarkl.fresh_public_input
+        y <- Snarkl.fresh_public_input
         p <- pair x y
         runStalk compiledProg p

examples/Examples/Lens.hs

@@ -11,8 +11,8 @@ import qualified Categorifier.Categorify as Categorify
 import Categorifier.Client
 import Control.Lens
 import Snarkl.Field (F_BN128)
-import Snarkl.Language (Ty (TField), pair, (>>=))
-import qualified Snarkl.Language.SyntaxMonad as Snarkl
+import Snarkl.Language.Prelude (Ty (TField), pair, (>>=))
+import qualified Snarkl.Language.Prelude as Snarkl
 import Stalk
 import Prelude (fromInteger)
 
@@ -43,8 +43,8 @@ simpleLens =
       compiledProg :: Stalk F_BN128 (F_BN128, F_BN128) F_BN128
       compiledProg = Categorify.expression prog
    in do
-        x <- Snarkl.fresh_input
-        y <- Snarkl.fresh_input
+        x <- Snarkl.fresh_public_input
+        y <- Snarkl.fresh_public_input
         p <- pair x y
         runStalk compiledProg p
 

examples/Examples/Snarkl.hs

@@ -12,7 +12,7 @@ module Examples.Snarkl
 where
 
 import Snarkl.Field (F_BN128)
-import Snarkl.Language (Comp, TExp, Ty (..), arr, forall, fromField, get, return, set, (+), (>>), (>>=))
+import Snarkl.Language.Prelude (Comp, TExp, Ty (..), arr, forall, fromField, get, return, set, (+), (>>), (>>=))
 import Prelude (fromInteger, ($))
 
 arr_ex :: TExp 'TField F_BN128 -> Comp 'TField F_BN128

examples/Examples/SnarklUnitTests.hs

@@ -8,8 +8,8 @@ module Examples.SnarklUnitTests where
 import qualified Categorifier.Categorify as Categorify
 import Categorifier.Vec.Client ()
 import Snarkl.Field (F_BN128)
-import Snarkl.Language (Ty (TField), pair, (>>=))
-import qualified Snarkl.Language.SyntaxMonad as Snarkl
+import Snarkl.Language.Prelude (Ty (TField), pair, (>>=))
+import qualified Snarkl.Language.Prelude as Snarkl
 import Stalk
 import Prelude (Bool (..), fromInteger, (&&), (*), (+), (-))
 
@@ -30,9 +30,9 @@ prog1 =
       compiledProg :: Stalk F_BN128 (Bool, (F_BN128, Bool)) F_BN128
       compiledProg = Categorify.expression prog
    in do
-        x <- Snarkl.fresh_input
-        y <- Snarkl.fresh_input
-        z <- Snarkl.fresh_input
+        x <- Snarkl.fresh_public_input
+        y <- Snarkl.fresh_public_input
+        z <- Snarkl.fresh_public_input
         yz <- pair y z
         p <- pair x yz
         runStalk compiledProg p
@@ -68,8 +68,8 @@ bool_prog9 =
       compiledProg :: Stalk F_BN128 (Bool, Bool) Bool
       compiledProg = Categorify.expression prog
    in do
-        x <- Snarkl.fresh_input
-        y <- Snarkl.fresh_input
+        x <- Snarkl.fresh_public_input
+        y <- Snarkl.fresh_public_input
         p <- pair x y
         runStalk compiledProg p
 
@@ -87,4 +87,4 @@ bool_prog9 =
 --   = do { e1 <- fresh_input
 --        ; e2 <- fresh_input
 --        ; return (e1 && e2)
---        }
+--        }

examples/Examples/Stalk.hs

@@ -22,9 +22,9 @@ import Data.Either (fromLeft)
 import Data.Field.Galois (GaloisField)
 import Data.Vec.Lazy (Vec (..))
 import Snarkl.Field (F_BN128)
-import qualified Snarkl.Language as Snarkl
+import qualified Snarkl.Language.Prelude as Snarkl
 import Stalk
-import "snarkl" Snarkl.Language (fromField, (>>=))
+import "snarkl" Snarkl.Language.Prelude (Comp, fromField, (>>=))
 import Prelude (Bool (..), Either (..), fromInteger, sum, ($), (*), (+), (.))
 
 -- * Basic
@@ -44,9 +44,9 @@ arr_ex x =
 p1 :: Snarkl.Comp 'Snarkl.TField F_BN128
 p1 = runStalk (Categorify.expression arr_ex) (fromField @F_BN128 1)
 
-p2 :: Snarkl.State (Snarkl.Env F_BN128) (Snarkl.TExp 'Snarkl.TField F_BN128)
+p2 :: Snarkl.Comp 'Snarkl.TField F_BN128
 p2 =
-  Snarkl.fresh_input
+  Snarkl.fresh_public_input
     >>= runStalk (Categorify.expression $ \(x :: F_BN128) -> x + x)
 
 comp1 :: Either Bool F_BN128
@@ -56,8 +56,8 @@ comp2 :: Either Bool F_BN128
 comp2 = Right 0
 
 -- | __TODO__: Needs @`ConCat.Category.ClosedCat` `Stalk`@
-test1 :: Snarkl.State (Snarkl.Env F_BN128) (Snarkl.TExp 'Snarkl.TBool F_BN128)
+test1 :: Comp 'Snarkl.TBool F_BN128
 test1 =
-  Snarkl.fresh_input
+  Snarkl.fresh_public_input
     >>= runStalk
       (Categorify.expression $ fromLeft False . bool comp2 comp1)

src/Stalk.hs

@@ -26,8 +26,8 @@ import Categorifier.Category
   )
 import qualified Categorifier.Category as Categorifier
 import Categorifier.Vec.Client ()
-import qualified ConCat.Category as ConCat
 import qualified ConCat.Additive
+import qualified ConCat.Category as ConCat
 import Data.Bool (bool)
 import qualified Data.Constraint as Constraint
 import Data.Field.Galois (GaloisField)
@@ -37,11 +37,11 @@ import Data.Type.Nat (Nat (..))
 import qualified Data.Type.Nat as Nat
 import Data.Typeable (Typeable)
 import Data.Vec.Lazy (Vec (..))
+import GHC.Natural (Natural)
 import Snarkl.Field (F_BN128)
-import Snarkl.Language (return, (>>), (>>=))
-import qualified Snarkl.Language as Snarkl
+import Snarkl.Language.Prelude (return, (>>), (>>=))
+import qualified Snarkl.Language.Prelude as Snarkl
 import Prelude (Bool, Either, error, fromInteger, ($), (+), (.))
-import GHC.Natural (Natural)
 
 -- | Mapping from Haskell types to Snarkl types.
 data Stalk k a b = Stalk
@@ -205,8 +205,8 @@ instance (ConCat.Additive.Additive k, Nat.SNatI n, GaloisField k, SnarklTy k ~ '
       (\n' e -> Snarkl.get (a, n') >>= (return . (Snarkl.+ e)))
       (Snarkl.fromField 0)
 
-instance GaloisField k => ConCat.Additive.Additive k where
-  zero  = 0
+instance (GaloisField k) => ConCat.Additive.Additive k where
+  zero = 0
   (^+^) = (+)
 
 instance
@@ -247,7 +247,7 @@ cat ::
   (Typeable (SnarklTy b)) =>
   Snarkl.TExp (SnarklTy (a -> b)) k ->
   Stalk k a b
-cat f = Stalk $ \x -> return $ Snarkl.TEApp f x
+cat f = Stalk $ \x -> Snarkl.apply f x
 
 lowerCat ::
   (Typeable (SnarklTy a)) =>

stalk.cabal

@@ -76,6 +76,8 @@ test-suite examples
     , snarkl
     , stalk
     , vec
+    , wl-pprint-text
+
 
   default-language: Haskell2010
   ghc-options: