diff --git a/cabal.project b/cabal.project index 3850315..ba45f11 100644 --- a/cabal.project +++ b/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 diff --git a/examples/Examples.hs b/examples/Examples.hs index ae2f6e5..9a0c095 100644 --- a/examples/Examples.hs +++ b/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 = diff --git a/examples/Examples/Arithmetic.hs b/examples/Examples/Arithmetic.hs index 92f0cb2..a03b28e 100644 --- a/examples/Examples/Arithmetic.hs +++ b/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 diff --git a/examples/Examples/Lens.hs b/examples/Examples/Lens.hs index fa11c1a..410cfbf 100644 --- a/examples/Examples/Lens.hs +++ b/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 diff --git a/examples/Examples/Snarkl.hs b/examples/Examples/Snarkl.hs index a492978..669ae98 100644 --- a/examples/Examples/Snarkl.hs +++ b/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 diff --git a/examples/Examples/SnarklUnitTests.hs b/examples/Examples/SnarklUnitTests.hs index c6a1838..0417e53 100644 --- a/examples/Examples/SnarklUnitTests.hs +++ b/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) --- } +-- } \ No newline at end of file diff --git a/examples/Examples/Stalk.hs b/examples/Examples/Stalk.hs index 171c1c6..01556ed 100644 --- a/examples/Examples/Stalk.hs +++ b/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) diff --git a/src/Stalk.hs b/src/Stalk.hs index 942cf4f..97c0044 100644 --- a/src/Stalk.hs +++ b/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)) => diff --git a/stalk.cabal b/stalk.cabal index 13cbaa3..2a785cd 100644 --- a/stalk.cabal +++ b/stalk.cabal @@ -76,6 +76,8 @@ test-suite examples , snarkl , stalk , vec + , wl-pprint-text + default-language: Haskell2010 ghc-options: