Merge pull request #2 from l-adic/stalk

Stalk

.github/workflows/ci.yml

@@ -14,5 +14,5 @@ jobs:
       with:
         name: martyall
         authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-    - run: nix build
+    - run: nix develop --command cabal update
     - run: nix develop --command cabal run tests

CHANGELOG.md

@@ -1,4 +1,4 @@
-# Revision history for straw
+# Revision history for stalk
 
 ## 0.1.0.0 -- YYYY-mm-dd
 

README.md

@@ -1,4 +1,4 @@
-# Straw
+# Stalk
 
 Compiling Haskell to cryptographic circuits.
 

cabal.project

@@ -1,9 +1,8 @@
 source-repository-package
   type: git
   location: https://github.com/con-kitty/categorifier.git
-  -- master branch as of 12/3/23
-  tag: 2eb124f2fbb3ced9ddf60872f571011da4e26dbf
-  --sha256: QLF8PQq6vPwhqXoDs4Txu4Fu3Z9R/rQ6fHWAdIpV/1c=
+  tag: 39ddecc07f41114b14dfc68c35ea1042698f8b77
+  --sha256: yRkxydkQ+3dVnEelPzEoGgc6WcIe0ktYxLVhLEj7K8o=
   subdir: 
    category
    client
@@ -15,13 +14,11 @@ source-repository-package
    integrations/vec/integration
    plugin
 
-
 source-repository-package
   type: git
   location: https://github.com/con-kitty/concat.git
-  -- ghc9 branch as of 12/3/23
-  tag: 99ee4981c096180abe99c24b12ff79e85d1817df
-  --sha256: LTKVbU2NQqA41hHUkSfgnBWzaiox3J/XT0ZqH1BqBNo=
+  tag: cb398e15d142ca198ccd9f952cdc4e74104c9c12
+  --sha256: BCu7IdKNhxq0Jf9iEW9LaV4qC3Ir1gxP91b0EBom4CQ=
   subdir:
     classes
     satisfy
@@ -30,10 +27,15 @@ source-repository-package
 
 source-repository-package
  type: git
- location: https://github.com/martyall/snarkl.git
- -- lambdas branch
- tag: 78eedc4b6777f10489cc54b77bba137ca3e7b40b
- --sha256: XvlFyP5MUABiMV/EW8jzG49FfcxZxfeKVD/ZvNLEw5E=
+ location: https://github.com/l-adic/snarkl.git
+ tag: 5d539a7827f570ee6e9dbf9a30e898acccd6c0cb
+ --sha256: jHy2OKlvSgBAkvtadvDVB0t3Hr2wTgXTFKW5T2t/yi0=
+
+source-repository-package
+  type: git
+  location: https://github.com/sdiehl/galois-field.git
+  tag: 3b13705fe26ea1dc03e1a6d7dac4089085c5362d
+  --sha256: +vkeD6mjdRk4epuvfIxf284A1vgPHxqSb3jLxBHuk60=
 
 constraints:
     PyF >=0.9.0 && <0.10
@@ -67,4 +69,6 @@ constraints:
 tests: True
 
 packages:
-  ./straw.cabal
+  ./stalk.cabal
+--  ../galois-fields/galois-field.cabal
+--  ../modular-arithmetic/modular-arithmetic.cabal

dev-profile

@@ -0,0 +1 @@
+dev-profile-1-link

dev-profile-1-link

@@ -0,0 +1 @@
+/nix/store/9qygy4mfpfna3khl01s1hcmvi2wz8ljw-nix-shell-env

examples/Examples.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE PackageImports #-}
 {-# LANGUAGE TemplateHaskell #-}
 
+import Data.Field.Galois (GaloisField)
 import Data.Typeable (Typeable)
 import qualified Examples.Arithmetic as Arithmetic
 import qualified Examples.Lens as Lens
@@ -13,10 +14,10 @@ import qualified Snarkl.Compile as Snarkl
 import qualified Snarkl.Toplevel as Snarkl
 
 -- | Little helper to get our expressions into a form that Hedgehog can compare.
-comparable :: (Typeable ty) => Snarkl.Comp ty -> String
-comparable = show . Snarkl.r1cs_of_comp Snarkl.Simplify
+comparable :: (Typeable ty, GaloisField k) => Snarkl.Comp ty k -> String
+comparable = show . Snarkl.compileCompToR1CS Snarkl.Simplify
 
-interpretable :: (Typeable ty) => Snarkl.Comp ty -> [Rational] -> Rational
+interpretable :: (Typeable ty, GaloisField k) => Snarkl.Comp ty k -> [k] -> k
 interpretable = Snarkl.comp_interp
 
 prop_simple_bool :: Hedgehog.Property
@@ -39,10 +40,10 @@ prop_simple_lens =
   Hedgehog.property $
     interpretable Lens.simpleLens [1, 2] === 42
 
-prop_complicated_lens :: Hedgehog.Property
-prop_complicated_lens =
-  Hedgehog.property $
-    interpretable Lens.simpleLens [1, 2, 32] === 42
+-- prop_complicated_lens :: Hedgehog.Property
+-- prop_complicated_lens =
+--  Hedgehog.property $
+--    interpretable Lens.simpleLens [1, 2, 32] === 42
 
 main :: IO ()
 main = do

examples/Examples/Arithmetic.hs

@@ -6,10 +6,11 @@ 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 Straw (Straw (runStraw))
-import Prelude (Bool (..), Rational, fromInteger, (&&), (*), (+), (-), (==))
+import Stalk (Stalk (runStalk))
+import Prelude (Bool (..), fromInteger, (*), (+), (-), (==))
 
 -- we need the because we enabled rebindable syntax
 ifThenElse :: Bool -> a -> a -> a
@@ -22,18 +23,18 @@ let x = 4^2;
 let y = 2 * x * z - 1 ;
 x + y
 -}
-simpleArith :: Snarkl.Comp 'TField
+simpleArith :: Snarkl.Comp 'TField F_BN128
 simpleArith =
-  let prog :: Rational -> Rational
+  let prog :: F_BN128 -> F_BN128
       prog z =
         let x = 4 * 4
             y = 2 * x * z - 1
          in x + 1
-      compiledProg :: Straw Rational Rational
+      compiledProg :: Stalk F_BN128 F_BN128 F_BN128
       compiledProg = Categorify.expression prog
    in do
         z <- Snarkl.fresh_input
-        runStraw compiledProg z
+        runStalk compiledProg z
 
 {-
 pub x: F;
@@ -45,18 +46,18 @@ if (f == 0 && g == 0)
   else 0
 -}
 
-simpleBool :: Snarkl.Comp 'TField
+simpleBool :: Snarkl.Comp 'TField F_BN128
 simpleBool =
-  let prog :: (Rational, Rational) -> Rational
+  let prog :: (F_BN128, F_BN128) -> F_BN128
       prog (x, y) =
-        let f = x * x + 2 * x + 1 - y
+        let -- f = x * x + 2 * x + 1 - y
             g = x + 7 - y
-         in if f == 0 && g == 0 then 42 else 0
+         in if g == 0 then 42 else 0
 
-      compiledProg :: Straw (Rational, Rational) Rational
+      compiledProg :: Stalk F_BN128 (F_BN128, F_BN128) F_BN128
       compiledProg = Categorify.expression prog
    in do
         x <- Snarkl.fresh_input
         y <- Snarkl.fresh_input
         p <- pair x y
-        runStraw compiledProg p
+        runStalk compiledProg p

examples/Examples/Lens.hs

@@ -10,61 +10,61 @@ module Examples.Lens where
 import qualified Categorifier.Categorify as Categorify
 import Categorifier.Client
 import Control.Lens
-import Data.Vec.Lazy (Vec (..))
+import Snarkl.Field (F_BN128)
 import Snarkl.Language (Ty (TField), pair, (>>=))
 import qualified Snarkl.Language.SyntaxMonad as Snarkl
-import Straw
-import Prelude (Rational, foldl, fromInteger)
+import Stalk
+import Prelude (fromInteger)
 
-data Point = Point {_x :: Rational, _y :: Rational}
+data Point = Point {_x :: F_BN128, _y :: F_BN128}
 
 type instance SnarklTy Point = SnarklTy (Rep Point)
 
 $(deriveHasRep ''Point)
 $(makeLenses ''Point)
 
-data Atom = Atom {_elem :: Rational, _point :: Point, _foo :: Rational}
+data Atom = Atom {_elem :: F_BN128, _point :: Point, _foo :: F_BN128}
 
 type instance SnarklTy Atom = SnarklTy (Rep Atom)
 
 $(deriveHasRep ''Atom)
 $(makeLenses ''Atom)
 
-simpleLens :: Snarkl.Comp 'TField
+simpleLens :: Snarkl.Comp 'TField F_BN128
 simpleLens =
-  let prog :: (Rational, Rational) -> Rational
+  let prog :: (F_BN128, F_BN128) -> F_BN128
       prog (x, y) =
         let p = Point x y
             atom = Atom 32 p 1
-            f :: Atom -> Rational -> Atom
+            f :: Atom -> F_BN128 -> Atom
             f a n = a & elem +~ n
          in f atom 10 ^. elem
 
-      compiledProg :: Straw (Rational, Rational) Rational
+      compiledProg :: Stalk F_BN128 (F_BN128, F_BN128) F_BN128
       compiledProg = Categorify.expression prog
    in do
         x <- Snarkl.fresh_input
         y <- Snarkl.fresh_input
         p <- pair x y
-        runStraw compiledProg p
+        runStalk compiledProg p
 
-complicatedLens :: Snarkl.Comp 'TField
-complicatedLens =
-  let prog :: (Rational, (Rational, Rational)) -> Rational
-      prog (x, (y, z)) =
-        let p = Point x y
-            atom :: Atom
-            atom = Atom z p 1
-            f :: Atom -> Rational -> Atom
-            f a n = a & elem +~ n
-            ls = 1 ::: 2 ::: 3 ::: VNil
-         in foldl f atom ls ^. elem
-      compiledProg :: Straw (Rational, (Rational, Rational)) Rational
-      compiledProg = Categorify.expression prog
-   in do
-        x <- Snarkl.fresh_input
-        y <- Snarkl.fresh_input
-        z <- Snarkl.fresh_input
-        yz <- pair y z
-        p <- pair x yz
-        runStraw compiledProg p
+-- complicatedLens :: Snarkl.Comp 'TField F_BN128
+-- complicatedLens =
+--  let prog :: (F_BN128, (F_BN128, F_BN128)) -> F_BN128
+--      prog (x, (y, z)) =
+--        let p = Point x y
+--            atom :: Atom
+--            atom = Atom z p 1
+--            f :: Atom -> F_BN128 -> Atom
+--            f a n = a & elem +~ n
+--            ls = 1 ::: 2 ::: 3 ::: VNil
+--         in foldl f atom ls ^. elem
+--      compiledProg :: Stalk F_BN128 (F_BN128, (F_BN128, F_BN128)) F_BN128
+--      compiledProg = Categorify.expression prog
+--   in do
+--        x <- Snarkl.fresh_input
+--        y <- Snarkl.fresh_input
+--        z <- Snarkl.fresh_input
+--        yz <- pair y z
+--        p <- pair x yz
+--        runStalk compiledProg p

examples/Examples/Snarkl.hs

@@ -11,15 +11,16 @@ module Examples.Snarkl
   )
 where
 
-import Snarkl.Language (Comp, TExp, Ty (..), arr, forall, fromRational, get, return, set, (+), (>>), (>>=))
-import Prelude (Rational, fromInteger, ($))
+import Snarkl.Field (F_BN128)
+import Snarkl.Language (Comp, TExp, Ty (..), arr, forall, fromField, get, return, set, (+), (>>), (>>=))
+import Prelude (fromInteger, ($))
 
-arr_ex :: TExp 'TField Rational -> Comp 'TField
+arr_ex :: TExp 'TField F_BN128 -> Comp 'TField F_BN128
 arr_ex x = do
   a <- arr 2
   forall [0 .. 1] (\i -> set (a, i) x)
   y <- get (a, 0)
   z <- get (a, 1)
   return $ y + z
 
-p1 = arr_ex 1.0
+p1 = arr_ex (fromField 1)

examples/Examples/SnarklUnitTests.hs

@@ -7,34 +7,35 @@ 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 Straw
-import Prelude (Bool (..), Rational, fromInteger, (&&), (*), (+), (-))
+import Stalk
+import Prelude (Bool (..), fromInteger, (&&), (*), (+), (-))
 
 -- we need the because we enabled rebindable syntax
 ifThenElse :: Bool -> a -> a -> a
 ifThenElse True t _ = t
 ifThenElse False _ f = f
 
-prog1 :: Snarkl.Comp 'TField
+prog1 :: Snarkl.Comp 'TField F_BN128
 prog1 =
-  let prog :: (Bool, (Rational, Bool)) -> Rational
+  let prog :: (Bool, (F_BN128, Bool)) -> F_BN128
       prog (x, (y, z)) =
         let u = y + 2
             v = if z then y else y + 1
             w = if x then y else y + 2
          in u * u - (w * u * u * y * y * v)
 
-      compiledProg :: Straw (Bool, (Rational, Bool)) Rational
+      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
         yz <- pair y z
         p <- pair x yz
-        runStraw compiledProg p
+        runStalk compiledProg p
 
 -- -- | 1. A standalone "program" in the expression language
 -- prog1
@@ -64,13 +65,13 @@ bool_prog9 =
   let prog :: (Bool, Bool) -> Bool
       prog (x, y) = x && y
 
-      compiledProg :: Straw (Bool, Bool) Bool
+      compiledProg :: Stalk F_BN128 (Bool, Bool) Bool
       compiledProg = Categorify.expression prog
    in do
         x <- Snarkl.fresh_input
         y <- Snarkl.fresh_input
         p <- pair x y
-        runStraw compiledProg p
+        runStalk compiledProg p
 
 -- {-# INLINE catExpr #-}
 -- catExpr expr =
@@ -79,7 +80,7 @@ bool_prog9 =
 --         x <- Snarkl.fresh_input
 --         y <- Snarkl.fresh_input
 --         p <- pair x y
---         runStraw compiledExpr p
+--         runStalk compiledExpr p
 
 -- -- | 9. 'and' test
 -- bool_prog9