Skip to content

Commit

Permalink
Merge branch 'main' into vlasin-IVC-update1
Browse files Browse the repository at this point in the history
  • Loading branch information
vlasin authored Dec 20, 2024
2 parents 8a6ff61 + bd8fff5 commit b0425ca
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 18 deletions.
24 changes: 8 additions & 16 deletions symbolic-base/src/ZkFold/Symbolic/Data/List.hs
Original file line number Diff line number Diff line change
Expand Up @@ -29,30 +29,22 @@ import ZkFold.Symbolic.Data.Payloaded (Payloaded (Payloaded))
import ZkFold.Symbolic.Data.UInt (UInt)
import ZkFold.Symbolic.MonadCircuit

data ListItem x a = ListItem
{ tailHash :: Layout x a
, headLayout :: Layout x a
, headPayload :: Payload x a
data ListItem l p a = ListItem
{ tailHash :: l a
, headLayout :: l a
, headPayload :: p a
}
deriving (Generic1)
deriving (Functor, Generic1)

deriving instance
(Functor (Layout x), Functor (Payload x)) =>
Functor (ListItem x)

instance
(Representable (Layout x), Representable (Payload x)) =>
Distributive (ListItem x) where
instance (Representable l, Representable p) => Distributive (ListItem l p) where
distribute = distributeRep

instance
(Representable (Layout x), Representable (Payload x)) =>
Representable (ListItem x)
instance (Representable l, Representable p) => Representable (ListItem l p)

data List c x = List
{ lHash :: c (Layout x)
, lSize :: c Par1
, lWitness :: Payloaded (Infinite :.: ListItem x) c
, lWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
}
deriving (Generic)

Expand Down
9 changes: 7 additions & 2 deletions symbolic-base/test/Tests/List.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,25 @@ import ZkFold.Base.Algebra.Basic.Class (one)
import ZkFold.Base.Algebra.Basic.Field (Zp)
import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_Scalar)
import ZkFold.Symbolic.Class (Arithmetic, Symbolic)
import ZkFold.Symbolic.Compiler (compile, eval1)
import ZkFold.Symbolic.Compiler (acOutput, compile, eval1)
import ZkFold.Symbolic.Data.Bool (Bool)
import ZkFold.Symbolic.Data.Eq ((==))
import ZkFold.Symbolic.Data.FieldElement (FieldElement)
import ZkFold.Symbolic.Data.List (emptyList, head, tail, (.:))
import ZkFold.Symbolic.Data.List (List, emptyList, head, tail, (.:))

headTest :: Symbolic c => FieldElement c -> FieldElement c -> Bool c
headTest x y = head (x .: y .: emptyList) == x

tailTest :: Symbolic c => FieldElement c -> FieldElement c -> Bool c
tailTest x y = head (tail (x .: y .: emptyList)) == y

headFun :: Symbolic c => List c (FieldElement c) -> FieldElement c
headFun = head

specList' :: forall a. (Arbitrary a, Arithmetic a, Binary a, Show a) => IO ()
specList' = hspec $ describe "List spec" $ do
let _headChecks = -- compile-time test
acOutput (compile @a headFun)
prop "Head works fine" $ \x y ->
eval1 (compile @a headTest) (U1 :*: U1 :*: U1) (Par1 x :*: Par1 y :*: U1)
Haskell.== one
Expand Down

0 comments on commit b0425ca

Please sign in to comment.