diff --git a/bench/BenchDiv.hs b/bench/BenchDiv.hs
new file mode 100644
index 000000000..1d9eb3112
--- /dev/null
+++ b/bench/BenchDiv.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE AllowAmbiguousTypes          #-}
+{-# LANGUAGE DeriveAnyClass               #-}
+{-# LANGUAGE NoGeneralisedNewtypeDeriving #-}
+{-# LANGUAGE ScopedTypeVariables          #-}
+{-# LANGUAGE TypeApplications             #-}
+{-# LANGUAGE TypeOperators                #-}
+{-# OPTIONS_GHC -freduction-depth=0 #-}
+
+module Main where
+
+import           Control.DeepSeq                             (force)
+import           Control.Exception                           (evaluate)
+import qualified Data.Map                                    as M
+import           Data.Time.Clock                             (getCurrentTime)
+import           Prelude                                     hiding (divMod, not, sum, (&&), (*), (+), (-), (/), (^),
+                                                              (||))
+import           System.Random                               (randomIO)
+import           Test.Tasty.Bench
+
+import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Algebra.Basic.Field
+import           ZkFold.Base.Algebra.Basic.Number
+import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381
+import           ZkFold.Base.Data.Vector
+import           ZkFold.Symbolic.Compiler
+import           ZkFold.Symbolic.Data.Combinators
+import           ZkFold.Symbolic.Data.UInt
+
+evalUInt :: forall a n . UInt n ArithmeticCircuit a -> Vector (NumberOfRegisters a n) a
+evalUInt (UInt xs) = eval xs M.empty
+
+-- | Generate random addition circuit of given size
+--
+divisionCircuit
+    :: forall n p r
+    .  KnownNat n
+    => PrimeField (Zp p)
+    => r ~ NumberOfRegisters (Zp p) n
+    => KnownNat r
+    => KnownNat (r - 1)
+    => KnownNat (r + r)
+    => 1 + (r - 1) ~ r
+    => 1 <= r
+    => IO (UInt n ArithmeticCircuit (Zp p), UInt n ArithmeticCircuit (Zp p))
+divisionCircuit = do
+    x <- randomIO
+    y <- randomIO
+    let acX = fromConstant (x :: Integer) :: UInt n ArithmeticCircuit (Zp p)
+        acY = fromConstant (y :: Integer) :: UInt n ArithmeticCircuit (Zp p)
+
+        acZ = acX `divMod` acY
+
+    evaluate . force $ acZ
+
+benchOps
+    :: forall n p r
+    .  KnownNat n
+    => PrimeField (Zp p)
+    => r ~ NumberOfRegisters (Zp p) n
+    => KnownNat r
+    => KnownNat (r - 1)
+    => KnownNat (r + r)
+    => 1 + (r - 1) ~ r
+    => 1 <= r
+    => Benchmark
+benchOps = env (divisionCircuit @n @p) $ \ ~ac ->
+    bench ("Dividing UInts of size " <> show (value @n)) $ nf (\(a, b) -> (evalUInt a, evalUInt b)) ac
+
+main :: IO ()
+main = do
+  getCurrentTime >>= print
+  (UInt ac32q, UInt ac32r)  <- divisionCircuit @32 @BLS12_381_Scalar
+  getCurrentTime >>= print
+  (UInt ac64q,  UInt ac64r)  <- divisionCircuit @64 @BLS12_381_Scalar
+  getCurrentTime >>= print
+  (UInt ac128q, UInt ac128r) <- divisionCircuit @128 @BLS12_381_Scalar
+  getCurrentTime >>= print
+
+  putStrLn "Sizes"
+
+  print $ (acSizeM ac32q, acSizeM ac32r)
+  getCurrentTime >>= print
+  print $ (acSizeM ac64q, acSizeM ac64r)
+  getCurrentTime >>= print
+  print $ (acSizeM ac128q, acSizeM ac128r)
+  getCurrentTime >>= print
+
+  putStrLn "Evaluation"
+
+  print $ (exec ac32q, exec ac32r)
+  getCurrentTime >>= print
+  print $ (exec ac64q, exec ac64r)
+  getCurrentTime >>= print
+  print $ (exec ac128q, exec ac128r)
+  getCurrentTime >>= print
+
+  defaultMain
+      [ benchOps @32 @BLS12_381_Scalar
+      , benchOps @64 @BLS12_381_Scalar
+      , benchOps @128 @BLS12_381_Scalar
+      ]
+
diff --git a/src/ZkFold/Base/Algebra/Basic/Class.hs b/src/ZkFold/Base/Algebra/Basic/Class.hs
index 60758e757..87a105106 100644
--- a/src/ZkFold/Base/Algebra/Basic/Class.hs
+++ b/src/ZkFold/Base/Algebra/Basic/Class.hs
@@ -7,9 +7,9 @@
 module ZkFold.Base.Algebra.Basic.Class where
 
 import           Data.Bool                        (bool)
+import           Data.Foldable                    (foldl')
 import           Data.Kind                        (Type)
 import           GHC.Natural                      (naturalFromInteger)
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (Num (..), div, divMod, length, mod, negate, product,
                                                    replicate, sum, (/), (^))
 import qualified Prelude                          as Haskell
@@ -99,6 +99,7 @@ class (MultiplicativeSemigroup a, Exponent a Natural) => MultiplicativeMonoid a
     -- [Right identity] @x * one == x@
     one :: a
 
+{-# INLINE natPow #-}
 natPow :: MultiplicativeMonoid a => a -> Natural -> a
 -- | A default implementation for natural exponentiation. Uses only @('*')@ and
 -- @'one'@ so doesn't loop via an @'Exponent' Natural a@ instance.
@@ -109,10 +110,10 @@ natPow a n = product $ zipWith f (binaryExpansion n) (iterate (\x -> x * x) a)
     f _ _ = error "^: This should never happen."
 
 product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
-product = foldl (*) one
+product = foldl' (*) one
 
 multiExp :: (MultiplicativeMonoid a, Exponent a b, Foldable t) => a -> t b -> a
-multiExp a = foldl (\x y -> x * (a ^ y)) one
+multiExp a = foldl' (\x y -> x * (a ^ y)) one
 
 {- | A class for monoid actions where multiplicative notation is the most
 natural (including multiplication by constant itself).
diff --git a/src/ZkFold/Base/Algebra/Basic/Field.hs b/src/ZkFold/Base/Algebra/Basic/Field.hs
index c97ee0d75..786dd6fad 100644
--- a/src/ZkFold/Base/Algebra/Basic/Field.hs
+++ b/src/ZkFold/Base/Algebra/Basic/Field.hs
@@ -22,7 +22,6 @@ import           Data.Bool                                  (bool)
 import qualified Data.Vector                                as V
 import           GHC.Generics                               (Generic)
 import           GHC.TypeLits                               (Symbol)
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Fractional (..), Num (..), div, length, (^))
 import qualified Prelude                                    as Haskell
 import           System.Random                              (Random (..), RandomGen, mkStdGen, uniformR)
@@ -38,12 +37,15 @@ import           ZkFold.Base.Data.ByteString
 newtype Zp (p :: Natural) = Zp Integer
     deriving (Generic, NFData)
 
+{-# INLINE fromZp #-}
 fromZp :: Zp p -> Natural
 fromZp (Zp a) = fromIntegral a
 
+{-# INLINE residue #-}
 residue :: forall p . KnownNat p => Integer -> Integer
 residue = (`Haskell.mod` fromIntegral (value @p))
 
+{-# INLINE toZp #-}
 toZp :: forall p . KnownNat p => Integer -> Zp p
 toZp = Zp . residue @p
 
diff --git a/src/ZkFold/Base/Algebra/Basic/Number.hs b/src/ZkFold/Base/Algebra/Basic/Number.hs
index 0a0bd2066..6a3dbee54 100644
--- a/src/ZkFold/Base/Algebra/Basic/Number.hs
+++ b/src/ZkFold/Base/Algebra/Basic/Number.hs
@@ -4,7 +4,22 @@
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module ZkFold.Base.Algebra.Basic.Number (KnownNat, Prime, KnownPrime, IsPrime, Log2, Mod, Div, value, type (<=), type (*), type (+), type (-), type (^)) where
+module ZkFold.Base.Algebra.Basic.Number
+    ( Natural
+    , KnownNat
+    , Prime
+    , KnownPrime
+    , IsPrime
+    , Log2
+    , Mod
+    , Div
+    , value
+    , type (<=)
+    , type (*)
+    , type (+)
+    , type (-)
+    , type (^)
+    ) where
 
 import           Data.Kind      (Constraint)
 import           Data.Type.Bool (If, type (&&))
diff --git a/src/ZkFold/Base/Algebra/Basic/Permutations.hs b/src/ZkFold/Base/Algebra/Basic/Permutations.hs
index c8faf1b7c..e6f312f43 100644
--- a/src/ZkFold/Base/Algebra/Basic/Permutations.hs
+++ b/src/ZkFold/Base/Algebra/Basic/Permutations.hs
@@ -14,7 +14,6 @@ module ZkFold.Base.Algebra.Basic.Permutations (
 import           Data.Map                         (Map, elems, empty, singleton, union)
 import           Data.Maybe                       (fromJust)
 import qualified Data.Vector                      as V
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (Num (..), drop, length, mod, (!!))
 import qualified Prelude                          as P
 import           Test.QuickCheck                  (Arbitrary (..))
diff --git a/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs b/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
index bd7d9d931..f79e7aa10 100644
--- a/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
+++ b/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
@@ -11,7 +11,6 @@ import           Data.Bits
 import           Data.Foldable
 import           Data.List                                  (unfoldr)
 import           Data.Word
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Num (..), (/), (^))
 import qualified Prelude                                    as Haskell
 
diff --git a/src/ZkFold/Base/Algebra/Polynomials/Multivariate/Polynomial.hs b/src/ZkFold/Base/Algebra/Polynomials/Multivariate/Polynomial.hs
index d45befc35..505cc41dc 100644
--- a/src/ZkFold/Base/Algebra/Polynomials/Multivariate/Polynomial.hs
+++ b/src/ZkFold/Base/Algebra/Polynomials/Multivariate/Polynomial.hs
@@ -38,9 +38,14 @@ newtype Poly c i j = P [(c, Mono i j)]
 polynomial :: Polynomial c i j => [(c, Mono i j)] -> Poly c i j
 polynomial = foldr (\(c, m) x -> if c == zero then x else P [(c, m)] + x) zero
 
-evalPolynomial :: forall c i j b .
-    Algebra c b =>
-    ((i -> b) -> Mono i j -> b) -> (i -> b) -> Poly c i j -> b
+evalPolynomial
+    :: forall c i j b
+     . AdditiveMonoid b
+    => Scale c b
+    => ((i -> b) -> Mono i j -> b)
+    -> (i -> b)
+    -> Poly c i j
+    -> b
 evalPolynomial e f (P p) = foldr (\(c, m) x -> x + scale c (e f m)) zero p
 
 variables :: forall c .
diff --git a/src/ZkFold/Base/Algebra/Polynomials/Univariate.hs b/src/ZkFold/Base/Algebra/Polynomials/Univariate.hs
index 5a778cfdc..ea8558571 100644
--- a/src/ZkFold/Base/Algebra/Polynomials/Univariate.hs
+++ b/src/ZkFold/Base/Algebra/Polynomials/Univariate.hs
@@ -40,7 +40,6 @@ module ZkFold.Base.Algebra.Polynomials.Univariate
 import           Control.DeepSeq                  (NFData (..))
 import qualified Data.Vector                      as V
 import           GHC.Generics                     (Generic)
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (Num (..), drop, length, product, replicate, sum, take, (/),
                                                    (^))
 import qualified Prelude                          as P
diff --git a/src/ZkFold/Base/Data/Vector.hs b/src/ZkFold/Base/Data/Vector.hs
index 87492e2df..52f08a674 100644
--- a/src/ZkFold/Base/Data/Vector.hs
+++ b/src/ZkFold/Base/Data/Vector.hs
@@ -14,7 +14,6 @@ import           Data.List.Split                  (chunksOf)
 import           Data.These                       (These (..))
 import           Data.Zip                         (Semialign (..), Zip (..))
 import           GHC.Generics                     (Generic)
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (drop, head, length, mod, replicate, sum, tail, take, zip,
                                                    zipWith, (*))
 import qualified Prelude                          as P
@@ -41,6 +40,9 @@ toVector as
 unsafeToVector :: forall size a . [a] -> Vector size a
 unsafeToVector = Vector
 
+generate :: forall size a . KnownNat size => (Natural -> a) -> Vector size a
+generate f = Vector $ f <$> [0 .. value @size -! 1]
+
 unfold :: forall size a b. KnownNat size => (b -> (a, b)) -> b -> Vector size a
 unfold f = Vector . ZP.take (value @size) . List.unfoldr (Just . f)
 
diff --git a/src/ZkFold/Base/Protocol/ARK/Plonk.hs b/src/ZkFold/Base/Protocol/ARK/Plonk.hs
index a63b75056..987c42300 100644
--- a/src/ZkFold/Base/Protocol/ARK/Plonk.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Plonk.hs
@@ -15,7 +15,6 @@ import           Data.Maybe                                 (fromJust)
 import qualified Data.Vector                                as V
 import           GHC.Generics                               (Par1)
 import           GHC.IsList                                 (IsList (..))
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Num (..), div, drop, length, replicate, sum, take,
                                                              (!!), (/), (^))
 import qualified Prelude                                    as P hiding (length)
diff --git a/src/ZkFold/Base/Protocol/ARK/Plonk/Internal.hs b/src/ZkFold/Base/Protocol/ARK/Plonk/Internal.hs
index e62a464d2..a38283b76 100644
--- a/src/ZkFold/Base/Protocol/ARK/Plonk/Internal.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Plonk/Internal.hs
@@ -8,7 +8,6 @@ import           Data.Bool                                  (bool)
 import qualified Data.Map                                   as Map
 import qualified Data.Vector                                as V
 import           GHC.IsList                                 (IsList (..))
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Num (..), drop, length, sum, take, (!!), (/), (^))
 import           System.Random                              (RandomGen, mkStdGen, uniformR)
 import           Test.QuickCheck                            (Arbitrary (..), Gen, shuffle)
diff --git a/src/ZkFold/Base/Protocol/ARK/Plonk/Relation.hs b/src/ZkFold/Base/Protocol/ARK/Plonk/Relation.hs
index 5db16eb4b..f478f0d5d 100644
--- a/src/ZkFold/Base/Protocol/ARK/Plonk/Relation.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Plonk/Relation.hs
@@ -6,7 +6,6 @@ module ZkFold.Base.Protocol.ARK.Plonk.Relation where
 import           Data.Map                                     (Map, elems, (!))
 import           GHC.Generics                                 (Par1)
 import           GHC.IsList                                   (IsList (..))
-import           Numeric.Natural                              (Natural)
 import           Prelude                                      hiding (Num (..), drop, length, replicate, sum, take,
                                                                (!!), (/), (^))
 
@@ -37,7 +36,6 @@ toPlonkRelation :: forall n l a .
     => KnownNat l
     => Arithmetic a
     => Scale a a
-    => FromConstant a a
     => Vector l Natural
     -> ArithmeticCircuit a Par1
     -> Maybe (PlonkRelation n l a)
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar.hs b/src/ZkFold/Base/Protocol/ARK/Protostar.hs
index b20435fc1..b55138b77 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar.hs
@@ -1 +1,71 @@
+{-# LANGUAGE DeriveAnyClass #-}
+
 module ZkFold.Base.Protocol.ARK.Protostar where
+
+
+import           Control.DeepSeq                                     (NFData)
+import           Data.Map.Strict                                     (Map)
+import qualified Data.Map.Strict                                     as M
+import           GHC.Generics                                        (Generic)
+import           Prelude                                             (($), (==))
+import qualified Prelude                                             as P
+
+import           ZkFold.Base.Algebra.Basic.Number
+import qualified ZkFold.Base.Data.Vector                             as V
+import           ZkFold.Base.Data.Vector                             (Vector)
+import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+
+{--
+
+1. Compress verification checks (Section 3.5; )
+2. Commit (Section 3.2; ZkFold.Base.Protocol.ARK.Protostar.CommitOpen)
+3. Fiat-Shamir transform (Section 3.3; ZkFold.Base.Protocol.ARK.Protostar.FiatShamir)
+   A technique for taking an interactive proof of knowledge and creating a digital signature based on it.
+   This way, some fact (for example, knowledge of a certain secret number) can be publicly proven without revealing underlying information.
+4. Accumulation scheme (Section 3.4; ZkFold.Base.Protocol.ARK.Protostar.AccumulatorScheme)
+5. Obtain the IVC scheme (Theorem 1 from “Proof-Carrying Data Without Succinct Arguments”; )
+
+--}
+--
+--
+-- To complete the protocol:
+-- 1. Finish AccumulatorScheme -- and Lookup
+-- 2. Implement IVC scheme
+-- 3. Put it all together
+-- 4. Input and output == AC
+
+
+-- | A data for recurcive computations.
+-- @circuit@ is an Arithmetic circuit with @n@ inputs and @n@ outputs applied to itself (i.e. outputs are fed as inputs at the next iteration) @iterations@ times.
+--
+data RecursiveCircuit n a
+    = RecursiveCircuit
+        { iterations :: Natural
+        , circuit    :: ArithmeticCircuit a (Vector n)
+        } deriving (Generic, NFData)
+
+instance Arithmetic a => SpecialSoundProtocol a (RecursiveCircuit n a) where
+    type Witness a (RecursiveCircuit n a) = Map Natural a
+    type Input a (RecursiveCircuit n a) = Vector n a
+    type ProverMessage a (RecursiveCircuit n a) = Vector n a
+    type VerifierMessage a (RecursiveCircuit n a) = Vector n a
+    type Degree (RecursiveCircuit n a) = 2
+
+    -- One round for Plonk
+    rounds = P.const 1
+
+    outputLength (RecursiveCircuit _ c) = P.fromIntegral $ M.size $ constraintSystem c
+
+    -- The transcript will be empty at this point, it is a one-round protocol
+    --
+    prover rc _ i _ = eval (circuit rc) (M.fromList $ P.zip [1..] (V.fromVector i))
+
+    -- We can use the polynomial system from the circuit, no need to build it from scratch
+    --
+    algebraicMap rc _ _ _ = M.elems $ constraintSystem (circuit rc)
+
+    -- The transcript is only one prover message since this is a one-round protocol
+    --
+    verifier rc i pm _ = eval (circuit rc) (M.fromList $ P.zip [1..] (V.fromVector i)) == P.head pm
+
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/Accumulator.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/Accumulator.hs
index acd71de12..ad9419f4f 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/Accumulator.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/Accumulator.hs
@@ -1,32 +1,44 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell     #-}
 
 module ZkFold.Base.Protocol.ARK.Protostar.Accumulator where
 
-import           Prelude                         hiding (length)
-
-import           ZkFold.Base.Algebra.Basic.Class
+import           Control.Lens.Combinators (makeLenses)
+import           Prelude                  hiding (length)
 
+-- Page 19, Accumulator instance
 data AccumulatorInstance f c = AccumulatorInstance {
-      accPublicInput :: f
-    , accCommits     :: [c]
-    , accChallenges  :: [f]
-    , accError       :: c
-    , accMu          :: f
+      _pi :: f     -- pi ∈  M^{l_in} in the paper
+    , _c  :: [c]   -- [C_i] ∈  C^k in the paper
+    , _r  :: [f]   -- [r_i] ∈  F^{k-1} in the paper
+    , _e  :: c     -- E ∈  C in the paper
+    , _mu :: f     -- μ ∈  F in the paper
 }
 
-newtype AccumulatorWitness m = AccumulatorWitness { accMessages :: [m] }
+makeLenses ''AccumulatorInstance
 
-data Accumulator f c m = Accumulator (AccumulatorInstance f c) (AccumulatorWitness m)
+-- Page 19, Accumulator
+-- @acc.x@ (accumulator instance) from the paper corresponds to _x
+-- @acc.w@ (accumulator witness) from the paper corresponds to _w
+data Accumulator f c m
+    = Accumulator
+        { _x :: AccumulatorInstance f c
+        , _w :: [m]
+        }
 
-data NARKInstance f c = NARKInstance {
-      narkPublicInput :: f
-    , narkCommits     :: [c]
-}
+makeLenses ''Accumulator
 
-newtype NARKWitness m = NARKWitness { narkMessages :: [m] }
+-- Page 18, section 3.4, The accumulation predicate
+--
+data NARKProof c m
+    = NARKProof
+        { narkCommits :: [c] -- Commits [C_i] ∈  C^k
+        , narkWitness :: [m] -- prover messages in the special-sound protocol [m_i]
+        }
 
-data NARKPair pi f c m = NARKPair (NARKInstance f c) (NARKWitness m)
+data InstanceProofPair pi c m = InstanceProofPair pi (NARKProof c m)
 
+{--
 toAccumulatorInstance :: (FiniteField f, AdditiveGroup c) => (f -> c -> f) -> NARKInstance f c -> AccumulatorInstance f c
 toAccumulatorInstance oracle (NARKInstance i cs) =
       let r0 = oracle i zero
@@ -40,3 +52,4 @@ toAccumulatorWitness (NARKWitness ms) = AccumulatorWitness ms
 
 toAccumulator :: (FiniteField f, AdditiveGroup c) => (f -> c -> f) -> NARKPair pi f c m -> Accumulator f c m
 toAccumulator oracle (NARKPair i w) = Accumulator (toAccumulatorInstance oracle i) (toAccumulatorWitness w)
+--}
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/AccumulatorScheme.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/AccumulatorScheme.hs
index 2811fecd7..6f0c868b7 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/AccumulatorScheme.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/AccumulatorScheme.hs
@@ -1,33 +1,191 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE AllowAmbiguousTypes  #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.ARK.Protostar.AccumulatorScheme where
 
-import           Prelude                                         hiding (length)
+import           Control.Lens                                    ((^.))
+import qualified Data.Vector                                     as DV
+import           Prelude                                         (fmap, otherwise, type (~), ($), (&&), (.), (<$>),
+                                                                  (<=), (==))
+import qualified Prelude                                         as P
 
+import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Algebra.Basic.Number
+import qualified ZkFold.Base.Algebra.Polynomials.Multivariate    as PM
+import qualified ZkFold.Base.Algebra.Polynomials.Univariate      as PU
+import qualified ZkFold.Base.Data.Vector                         as V
 import           ZkFold.Base.Protocol.ARK.Protostar.Accumulator
 import           ZkFold.Base.Protocol.ARK.Protostar.CommitOpen   (CommitOpen (..))
 import           ZkFold.Base.Protocol.ARK.Protostar.FiatShamir   (FiatShamir (..))
-import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (Input, ProverMessage)
+import           ZkFold.Base.Protocol.ARK.Protostar.Oracle       (RandomOracle (..))
+import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (Input, LMap, ProverMessage, SpecialSoundProtocol (..))
+import           ZkFold.Prelude                                  ((!!))
 
+
+-- | Accumulator scheme for V_NARK as described in Chapter 3.4 of the Protostar paper
+--
 class AccumulatorScheme f c m a where
-  commit   :: a -> m -> c
+  commit   :: a -> [m] -> c
 
-  prover   :: a -> Accumulator f c m -> Accumulator f c m -> (Accumulator f c m, [f])
+  prover   :: a                        -- input commitment key
+           -> Accumulator f c m        -- accumulator
+           -> InstanceProofPair f c m  -- instance-proof pair (pi, π)
+           -> (Accumulator f c m, [c]) -- updated accumulator and accumulation proof
 
-  verifier :: a
-           -> AccumulatorInstance f c
-           -> AccumulatorInstance f c
-           -> (AccumulatorInstance f c, [f])
-           -> Bool
+  verifier :: f                        -- Public input
+           -> [c]                      -- NARK proof π.x
+           -> AccumulatorInstance f c  -- accumulator instance acc.x
+           -> AccumulatorInstance f c  -- updated accumulator instance acc'.x
+           -> [c]                      -- accumulation proof E_j
+           -> P.Bool
 
-  decider  :: a -> Accumulator f c m -> Bool
+  decider  :: a                   -- Commitment key ck
+           -> Accumulator f c m   -- accumulator
+           -> P.Bool
 
-instance (Input f a ~ f, ProverMessage f a ~ m) => AccumulatorScheme f c m (FiatShamir f (CommitOpen f c a)) where
+instance
+    ( Input f a ~ f
+    , ProverMessage f a ~ m
+    , f ~ m -- TODO: Seems off but I really have no idea how to compile the code without it
+    , P.Eq c
+    , AdditiveGroup c
+    , Ring m
+    , Scale m c
+    , Input m (FiatShamir m (CommitOpen m c a)) ~ m
+    , ProverMessage Natural (FiatShamir m (CommitOpen m c a)) ~ m
+    , VerifierMessage Natural (FiatShamir m (CommitOpen m c a)) ~ m
+    , KnownNat (Degree (FiatShamir f (CommitOpen f c a)))
+    , SpecialSoundProtocol f (FiatShamir f (CommitOpen f c a))
+    , RandomOracle (f, c) f                                  -- Random oracle ρ_NARK
+    , RandomOracle (AccumulatorInstance f c, f, [c], [c]) f  -- Random oracle ρ_acc
+    ) => AccumulatorScheme f c m (FiatShamir f (CommitOpen f c a)) where
   commit (FiatShamir (CommitOpen cm _) _) = cm
 
-  prover   = undefined
+  prover sps@(FiatShamir (CommitOpen cm _) _) acc (InstanceProofPair pubi (NARKProof pi_x pi_w)) =
+      (Accumulator (AccumulatorInstance pi'' ci'' ri'' eCapital' mu') mi'', eCapital_j)
+      where
+          -- Fig. 3, step 1
+          r_i :: [f]
+          r_i = P.tail $ P.scanl (P.curry oracle) pubi (zero : pi_x)
+
+          -- Fig. 3, step 2
+          f_sps = degreeDecomposition @(Degree (FiatShamir f (CommitOpen f c a))) $ algebraicMap @f sps pubi (acc^.x^.r) (acc^.w)
+
+          -- X + mu as a univariate polynomial
+          xMu :: PU.Poly f
+          xMu = PU.toPoly $ DV.fromList [acc^.x^.mu, one]
+
+          d :: Natural
+          d = outputLength @f sps
+
+          k :: Natural
+          k = rounds @f sps
+
+          ixToPoly :: Natural -> PU.Poly f
+          ixToPoly n
+            | n == 0    = PU.toPoly $ DV.fromList [acc^.x^.pi, pubi]                                   -- X * pi + pi'
+            | n <= k    = PU.toPoly $ DV.fromList [(acc^.w) !! (n -! 1), pi_w !! (n -! 1)]             -- X * mi + mi'
+            | otherwise = PU.toPoly $ DV.fromList [(acc^.x^.r) !! (n -! k -! 1), r_i !! (n -! k -! 1)] -- X * ri + ri'
+
+          -- The @lxd@ matrix of coefficients as a vector of @l@ univariate degree-@d@ polynomials
+          --
+          e_uni :: [PU.Poly f]
+          e_uni = P.foldl (P.liftA2 (+)) (P.pure zero) $ V.mapWithIx (\j p -> ((xMu ^ (d -! j)) *) <$> p) $ fmap (PM.evalPolynomial PM.evalMonomial ixToPoly) <$> f_sps
+
+          e_all = (DV.toList . PU.fromPoly) <$> e_uni
+
+          e_j :: [[f]]
+          e_j = P.tail e_all
+
+          -- Fig. 3, step 3
+          eCapital_j = cm <$> e_j
+
+          -- Fig. 3, step 4
+          alpha :: f
+          alpha = oracle (acc^.x, pubi, pi_x, eCapital_j)
+
+          -- Fig. 3, steps 5, 6
+          mu'  = alpha            + acc^.x^.mu
+          pi'' = scale alpha pubi + acc^.x^.pi
+          ri'' = P.zipWith (\rl r' -> scale alpha rl + r') r_i  $ acc^.x^.r
+          ci'' = P.zipWith (\cl c' -> scale alpha cl + c') pi_x $ acc^.x^.c
+          mi'' = P.zipWith (\ml m' -> scale alpha ml + m') pi_w $ acc^.w
+
+          -- Fig. 3, step 7
+          eCapital' = acc^.x^.e + sum (P.zipWith (\e' p -> scale (alpha ^ p) e') eCapital_j [1::Natural ..])
+
+
+  verifier pubi c_i acc acc' pf = P.and [muEq, piEq, riEq, ciEq, eEq]
+      where
+          -- Fig. 4, step 1
+          r_i :: [f]
+          r_i = P.tail $ P.scanl (P.curry oracle) pubi (zero : c_i)
+
+          -- Fig. 4, step 2
+          alpha :: f
+          alpha = oracle (acc, pubi, c_i, pf)
+
+          -- Fig. 4, step 3
+          mu'  = alpha            + acc^.mu
+          pi'' = scale alpha pubi + acc^.pi
+          ri'' = P.zipWith (\rl r' -> scale alpha rl + r') r_i $ acc^.r
+          ci'' = P.zipWith (\cl c' -> scale alpha cl + c') c_i $ acc^.c
+
+          -- Fig 4, step 4
+          muEq = acc'^.mu == mu'
+          piEq = acc'^.pi == pi''
+          riEq = acc'^.r  == ri''
+          ciEq = acc'^.c  == ci''
+
+          -- Fig 4, step 5
+          eEq = acc'^.e == acc^.e + sum (P.zipWith scale ((\p -> alpha^p) <$> [1 :: Natural ..]) pf)
+
+  decider sps@(FiatShamir (CommitOpen cm _) _) acc = commitsEq && eEq
+      where
+          d :: Natural
+          d = outputLength @f sps
+
+          k :: Natural
+          k = rounds @f sps
+
+
+          -- Fig. 5, step 1
+          commitsEq = P.and $ P.zipWith (\cl m -> cm [m] == cl) (acc^.x^.c) (acc^.w)
+
+          -- Fig. 5, step 2
+          f_sps = mulDeg (acc^.x^.mu) d <$> algebraicMap @f sps (acc^.x^.pi) (acc^.x^.r) (acc^.w)
+
+          ixToVal :: Natural -> f
+          ixToVal n
+            | n == 0    = acc^.x^.pi                   -- pi
+            | n <= k    = (acc^.w) !! (n -! 1)         -- mi
+            | otherwise = (acc^.x^.r) !! (n -! k -! 1) -- ri
+
+          err = PM.evalPolynomial PM.evalMonomial ixToVal <$> f_sps
+
+          -- Fig. 5, step 3
+          eEq = acc^.x^.e == cm err
+
+mulDeg
+    :: MultiplicativeSemigroup f
+    => Exponent f Natural
+    => f
+    -> Natural
+    -> PM.Poly f Natural Natural
+    -> PM.Poly f Natural Natural
+mulDeg f d (PM.P monomials) = PM.P $ (\(coeff, m) -> (f ^ (d -! deg m) * coeff, m)) <$> monomials
+
+-- | Decomposes an algebraic map into homogenous degree-j maps for j from 0 to @n@
+--
+degreeDecomposition :: forall n f . KnownNat n => LMap f -> V.Vector n (LMap f)
+degreeDecomposition lmap = V.generate degree_j
+    where
+        degree_j :: Natural -> LMap f
+        degree_j j = P.fmap (leaveDeg j) lmap
 
-  verifier = undefined
+        leaveDeg :: Natural -> PM.Poly f Natural Natural -> PM.Poly f Natural Natural
+        leaveDeg j (PM.P monomials) = PM.P $ P.filter (\(_, m) -> deg m == j) monomials
 
-  decider  = undefined
+deg :: PM.Mono Natural Natural -> Natural
+deg (PM.M m) = sum m
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/CommitOpen.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/CommitOpen.hs
index a3f367caa..7f97ebf56 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/CommitOpen.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/CommitOpen.hs
@@ -1,15 +1,17 @@
 {-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.ARK.Protostar.CommitOpen where
 
 import           Prelude                                         hiding (length)
 
+import           ZkFold.Base.Algebra.Basic.Class                 (Bits)
 import           ZkFold.Base.Data.ByteString
 import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript)
 import           ZkFold.Prelude                                  (length)
 
-data CommitOpen f c a = CommitOpen (ProverMessage f a -> c) a
+data CommitOpen f c a = CommitOpen ([ProverMessage f a] -> c) a
 
 data CommitOpenProverMessage t c a = Commit c | Open [ProverMessage t a]
 instance (Binary c, Binary (ProverMessage t a)) => Binary (CommitOpenProverMessage t c a) where
@@ -21,36 +23,41 @@ instance (Binary c, Binary (ProverMessage t a)) => Binary (CommitOpenProverMessa
             else if flag == 1 then Open <$> get
             else fail ("Binary (CommitOpenProverMessage t c a): unexpected flag " <> show flag)
 
-instance (SpecialSoundProtocol f a, Eq c) => SpecialSoundProtocol f (CommitOpen f c a) where
+instance (SpecialSoundProtocol f a, Eq c, Bits a ~ [a]) => SpecialSoundProtocol f (CommitOpen f c a) where
       type Witness f (CommitOpen f c a)         = (Witness f a, [ProverMessage f a])
       type Input f (CommitOpen f c a)           = Input f a
       type ProverMessage t (CommitOpen f c a)   = CommitOpenProverMessage t c a
       type VerifierMessage t (CommitOpen f c a) = VerifierMessage t a
 
-      type Dimension (CommitOpen f c a)         = Dimension a
       type Degree (CommitOpen f c a)            = Degree a
 
+      outputLength (CommitOpen _ a) = outputLength @f a
+
       rounds a = rounds @f a + 1
 
       prover (CommitOpen cm a) (w, ms) i ts
             | length ts /= length ms  = error "Invalid transcript length"
-            | length ts < rounds @f a = Commit $ cm $ prover @f a w i $ zip ms $ map snd ts
+            | length ts < rounds @f a = Commit $ cm [prover @f a w i $ zip ms $ map snd ts]
             | otherwise               = Open ms
 
       -- TODO: Implement this
-      verifier' = undefined
+      -- make in an AC and use only it
+      -- decider is also AC
+      algebraicMap = undefined
 
-      verifier (CommitOpen cm a) i ((Open ms, _) : ts) = map cm ms == map f ts && verifier @f a i (zip ms $ map snd ts)
-            where f (Commit c, _) = c
-                  f _             = error "Invalid message"
-      verifier _ _ _ = error "Invalid transcript"
+      verifier (CommitOpen cm a) i ((Open ms):mss) (_:ts) = map (cm . pure) ms == map f mss && verifier @f a i ms ts
+            where f (Commit c) = c
+                  f _          = error "Invalid message"
+      verifier _ _ _ _ = error "Invalid transcript"
 
 commits :: SpecialSoundTranscript t (CommitOpen f c a) -> [c]
 commits = map f
       where f (Commit c, _) = c
             f _             = error "Invalid message"
 
-opening :: forall f a c . (SpecialSoundProtocol f a, Eq c)
+-- TODO: looks like Fiat-Shamir transform itself
+-- Why is it called opening?
+opening :: forall f a c . (SpecialSoundProtocol f a, Eq c, Bits a ~ [a])
         => CommitOpen f c a
         -> Witness f a
         -> Input f a
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/FiatShamir.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/FiatShamir.hs
index ef87797bc..f4621636f 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/FiatShamir.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/FiatShamir.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.ARK.Protostar.FiatShamir where
@@ -6,6 +7,7 @@ module ZkFold.Base.Protocol.ARK.Protostar.FiatShamir where
 import           Data.ByteString                                 (ByteString)
 import           Prelude                                         hiding (length)
 
+import           ZkFold.Base.Algebra.Basic.Class                 (Bits)
 import           ZkFold.Base.Data.ByteString                     (Binary (..))
 import           ZkFold.Base.Protocol.ARK.Protostar.CommitOpen
 import qualified ZkFold.Base.Protocol.ARK.Protostar.SpecialSound as SpS
@@ -15,7 +17,7 @@ import           ZkFold.Base.Protocol.NonInteractiveProof        (NonInteractive
 
 data FiatShamir f a = FiatShamir a (SpS.Input f a)
 
-fsChallenge :: forall f a c . (Binary (SpS.Input f a), Binary (VerifierMessage f a))
+fsChallenge :: forall f a c . (Binary (SpS.Input f a), Binary (VerifierMessage f a), Binary c, Binary (ProverMessage f a))
       => FiatShamir f (CommitOpen f c a)
       -> SpecialSoundTranscript f (CommitOpen f c a) -> ProverMessage f (CommitOpen f c a) -> VerifierMessage f a
 fsChallenge (FiatShamir _ ip) []           c =
@@ -24,14 +26,17 @@ fsChallenge (FiatShamir _ ip) []           c =
 fsChallenge _                 ((_, r) : _) c = fst $ challenge @ByteString $ toTranscript r <> toTranscript c
 
 instance (SpS.SpecialSoundProtocol f a, Eq c, Binary (SpS.Input f a), Binary (VerifierMessage f a),
-            Binary c, Binary (VerifierMessage f a)) => NonInteractiveProof (FiatShamir f (CommitOpen f c a)) where
+            Binary c, Binary (ProverMessage f a), Bits a ~ [a]) => NonInteractiveProof (FiatShamir f (CommitOpen f c a)) where
       type Transcript (FiatShamir f (CommitOpen f c a)) = ByteString
-      type Setup (FiatShamir f (CommitOpen f c a))      = FiatShamir f (CommitOpen f c a)
+      type SetupProve (FiatShamir f (CommitOpen f c a))      = FiatShamir f (CommitOpen f c a)
+      type SetupVerify (FiatShamir f (CommitOpen f c a))      = FiatShamir f (CommitOpen f c a)
       type Witness (FiatShamir f (CommitOpen f c a))    = SpS.Witness f a
       type Input (FiatShamir f (CommitOpen f c a))      = (SpS.Input f a, [c])
       type Proof (FiatShamir f (CommitOpen f c a))      = [ProverMessage f a]
 
-      setup x = x
+      setupProve x = x
+
+      setupVerify x = x
 
       prove fs@(FiatShamir a ip) w =
             let (ms, ts) = opening a w ip (fsChallenge fs)
@@ -40,4 +45,5 @@ instance (SpS.SpecialSoundProtocol f a, Eq c, Binary (SpS.Input f a), Binary (Ve
       verify fs@(FiatShamir a _) (ip, cs) ms =
             let ts' = foldl (\acc c -> acc ++ [(c, fsChallenge fs acc c)]) [] $ map Commit cs
                 ts  = ts' ++ [(Open ms, fsChallenge fs ts' $ Open ms)]
-            in verifier a ip ts
+                (ri, ci) = unzip ts
+            in verifier a ip ri ci
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/Gate.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/Gate.hs
index 78b08114e..40293771c 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/Gate.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/Gate.hs
@@ -6,12 +6,14 @@ import           Prelude                                         hiding (Num (..
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field                 (Zp)
-import           ZkFold.Base.Algebra.Basic.Number                (KnownNat)
+import           ZkFold.Base.Algebra.Basic.Number                (KnownNat, value)
 import           ZkFold.Base.Algebra.Polynomials.Multivariate    (Poly, evalMonomial, evalPolynomial, subs, var)
 import           ZkFold.Base.Data.Matrix                         (Matrix (..), outer, sum1, transpose)
+import qualified ZkFold.Base.Data.Vector                         as V
 import           ZkFold.Base.Data.Vector                         (Vector)
 import           ZkFold.Base.Protocol.ARK.Protostar.Internal     (PolynomialProtostar (..))
-import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript)
+import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (LMap, SpecialSoundProtocol (..),
+                                                                  SpecialSoundTranscript)
 import           ZkFold.Symbolic.Compiler.Arithmetizable         (Arithmetic)
 
 data ProtostarGate (m :: Natural) (n :: Natural) (c :: Natural) (d :: Natural)
@@ -25,9 +27,10 @@ instance (Arithmetic f, KnownNat m, KnownNat n) => SpecialSoundProtocol f (Proto
     -- ^ same as Witness
     type VerifierMessage t (ProtostarGate m n c d) = ()
 
-    type Dimension (ProtostarGate m n c d)        = n
     type Degree (ProtostarGate m n c d)           = d
 
+    outputLength _ = value @n
+
     rounds :: ProtostarGate m n c d -> Natural
     rounds _ = 1
 
@@ -38,23 +41,25 @@ instance (Arithmetic f, KnownNat m, KnownNat n) => SpecialSoundProtocol f (Proto
           -> ProverMessage f (ProtostarGate m n c d)
     prover _ w _ _ = w
 
-    verifier' :: ProtostarGate m n c d
-              -> Input f (ProtostarGate m n c d)
-              -> SpecialSoundTranscript Natural (ProtostarGate m n c d)
-              -> Vector (Dimension (ProtostarGate m n c d)) (Poly f Natural Natural)
-    verifier' _ (s, g) [(w, _)] =
+    algebraicMap :: ProtostarGate m n c d
+                 -> Input f (ProtostarGate m n c d)
+                 -> [ProverMessage Natural (ProtostarGate m n c d)]
+                 -> [VerifierMessage Natural (ProtostarGate m n c d)]
+                 -> LMap f
+    algebraicMap _ (s, g) [w] _ =
       let w' = fmap ((var .) . subs) w :: Vector n (Zp c -> Poly f Natural Natural)
           z  = transpose $ outer (evalPolynomial evalMonomial) w' $ fmap (\(PolynomialProtostar p) -> p) g
-      in sum1 $ zipWith scale s z
-    verifier' _ _ _ = error "Invalid transcript"
+      in V.fromVector $ sum1 $ zipWith scale s z
+    algebraicMap _ _ _ _ = error "Invalid transcript"
 
     verifier :: ProtostarGate m n c d
              -> Input f (ProtostarGate m n c d)
-             -> SpecialSoundTranscript f (ProtostarGate m n c d)
+             -> [ProverMessage f (ProtostarGate m n c d)]
+             -> [VerifierMessage f (ProtostarGate m n c d)]
              -> Bool
-    verifier _ (s, g) [(w, _)] =
+    verifier _ (s, g) [w] _ =
       let w' = fmap subs w :: Vector n (Zp c -> f)
           z  = transpose $ outer (evalPolynomial evalMonomial) w' $ fmap (\(PolynomialProtostar p) -> p) g
       in all (== zero) $ sum1 $ zipWith (*) s z
-    verifier _ _ _ = error "Invalid transcript"
+    verifier _ _ _ _ = error "Invalid transcript"
 
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/Lookup.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/Lookup.hs
index e25d3bbac..c72349d42 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/Lookup.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/Lookup.hs
@@ -6,24 +6,23 @@ module ZkFold.Base.Protocol.ARK.Protostar.Lookup where
 import           Data.Map                                        (fromList, mapWithKey)
 import           Data.These                                      (These (..))
 import           Data.Zip
-import           Numeric.Natural                                 (Natural)
 import           Prelude                                         hiding (Num (..), repeat, sum, zip, zipWith, (!!), (/),
                                                                   (^))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field                 (Zp)
 import           ZkFold.Base.Algebra.Basic.Number
-import           ZkFold.Base.Algebra.Polynomials.Multivariate    (Poly)
 import           ZkFold.Base.Data.Sparse.Vector                  (SVector (..))
 import           ZkFold.Base.Data.Vector                         (Vector)
-import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript)
+import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (LMap, SpecialSoundProtocol (..),
+                                                                  SpecialSoundTranscript)
 import           ZkFold.Symbolic.Compiler                        (Arithmetic)
 
 data ProtostarLookup (l :: Natural) (sizeT :: Natural)
 
 data ProtostarLookupParams f sizeT = ProtostarLookupParams (Zp sizeT -> f) (f -> [Zp sizeT])
 
-instance (Arithmetic f, KnownNat sizeT) => SpecialSoundProtocol f (ProtostarLookup l sizeT) where
+instance (Arithmetic f, KnownNat l, KnownNat sizeT) => SpecialSoundProtocol f (ProtostarLookup l sizeT) where
     type Witness f (ProtostarLookup l sizeT)         = Vector l f
     -- ^ w in the paper
     type Input f (ProtostarLookup l sizeT)           = ProtostarLookupParams f sizeT
@@ -32,9 +31,10 @@ instance (Arithmetic f, KnownNat sizeT) => SpecialSoundProtocol f (ProtostarLook
     -- ^ (w, m) or (h, g) in the paper
     type VerifierMessage t (ProtostarLookup l sizeT) = t
 
-    type Dimension (ProtostarLookup l sizeT)         = l + sizeT + 1
     type Degree (ProtostarLookup l sizeT)            = 2
 
+    outputLength _ = value @l + (value @sizeT) + 1
+
     rounds :: ProtostarLookup l sizeT -> Natural
     rounds _ = 2
 
@@ -53,17 +53,19 @@ instance (Arithmetic f, KnownNat sizeT) => SpecialSoundProtocol f (ProtostarLook
     prover _ _ _ _ = error "Invalid transcript"
 
     -- TODO: implement this
-    verifier' :: ProtostarLookup l sizeT
-              -> Input f (ProtostarLookup l sizeT)
-              -> SpecialSoundTranscript Natural (ProtostarLookup l sizeT)
-              -> Vector (Dimension (ProtostarLookup l sizeT)) (Poly f Natural Natural)
-    verifier' = undefined
+    algebraicMap :: ProtostarLookup l sizeT
+                 -> Input f (ProtostarLookup l sizeT)
+                 -> [ProverMessage Natural (ProtostarLookup l sizeT)]
+                 -> [VerifierMessage Natural (ProtostarLookup l sizeT)]
+                 -> LMap f
+    algebraicMap = undefined
 
     verifier :: ProtostarLookup l sizeT
              -> Input f (ProtostarLookup l sizeT)
-             -> SpecialSoundTranscript f (ProtostarLookup l sizeT)
+             -> [ProverMessage f (ProtostarLookup l sizeT)]
+             -> [VerifierMessage f (ProtostarLookup l sizeT)]
              -> Bool
-    verifier _ (ProtostarLookupParams t _) [((w, m), r), ((h, g), _)] =
+    verifier _ (ProtostarLookupParams t _) [(w, m), (h, g)] [r, _] =
         let c1 = sum h == sum g
             c2 = all (== one) $ zipWith (*) h (fmap (+r) w)
             g' = SVector $ mapWithKey (\i g_i -> g_i * (t i + r)) $ fromSVector m
@@ -73,5 +75,5 @@ instance (Arithmetic f, KnownNat sizeT) => SpecialSoundProtocol f (ProtostarLook
                 These x y -> x == y
             c3 = all (== one) $ alignWith f g' m
         in c1 && c2 && c3
-    verifier _ _ _ = error "Invalid transcript"
+    verifier _ _ _ _ = error "Invalid transcript"
 
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/Oracle.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/Oracle.hs
new file mode 100644
index 000000000..e612bb499
--- /dev/null
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/Oracle.hs
@@ -0,0 +1,6 @@
+module ZkFold.Base.Protocol.ARK.Protostar.Oracle where
+
+class RandomOracle a b where
+    oracle :: a -> b
+
+
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/Permutation.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/Permutation.hs
index 619e930d0..a07dd64d9 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/Permutation.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/Permutation.hs
@@ -1,19 +1,20 @@
 module ZkFold.Base.Protocol.ARK.Protostar.Permutation where
 
 import           Data.Zip                                        (Zip (..))
-import           Numeric.Natural                                 (Natural)
 import           Prelude                                         hiding (Num (..), zipWith, (!!), (^))
 
 import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Algebra.Basic.Permutations          (Permutation, applyPermutation)
-import           ZkFold.Base.Algebra.Polynomials.Multivariate    (Poly, var)
-import           ZkFold.Base.Data.Vector                         (Vector)
-import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript)
+import           ZkFold.Base.Algebra.Polynomials.Multivariate    (var)
+import           ZkFold.Base.Data.Vector                         as V
+import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (LMap, SpecialSoundProtocol (..),
+                                                                  SpecialSoundTranscript)
 import           ZkFold.Symbolic.Compiler                        (Arithmetic)
 
 data ProtostarPermutation (n :: Natural)
 
-instance Arithmetic f => SpecialSoundProtocol f (ProtostarPermutation n) where
+instance (Arithmetic f, KnownNat n) => SpecialSoundProtocol f (ProtostarPermutation n) where
     type Witness f (ProtostarPermutation n)         = Vector n f
     -- ^ w in the paper
     type Input f (ProtostarPermutation n)           = Permutation n
@@ -22,9 +23,10 @@ instance Arithmetic f => SpecialSoundProtocol f (ProtostarPermutation n) where
     -- ^ same as Witness
     type VerifierMessage t (ProtostarPermutation n) = ()
 
-    type Dimension (ProtostarPermutation n)         = n
     type Degree (ProtostarPermutation n)            = 1
 
+    outputLength _ = value @n
+
     rounds :: ProtostarPermutation n -> Natural
     rounds _ = 1
 
@@ -35,18 +37,20 @@ instance Arithmetic f => SpecialSoundProtocol f (ProtostarPermutation n) where
            -> ProverMessage f (ProtostarPermutation n)
     prover _ w _ _ = w
 
-    verifier' :: ProtostarPermutation n
-              -> Input f (ProtostarPermutation n)
-              -> SpecialSoundTranscript Natural (ProtostarPermutation n)
-              -> Vector (Dimension (ProtostarPermutation n)) (Poly f Natural Natural)
-    verifier' _ sigma [(w, _)] = zipWith (-) (applyPermutation sigma wX) wX
+    algebraicMap :: ProtostarPermutation n
+                 -> Input f (ProtostarPermutation n)
+                 -> [ProverMessage Natural (ProtostarPermutation n)]
+                 -> [VerifierMessage Natural (ProtostarPermutation n)]
+                 -> LMap f
+    algebraicMap _ sigma [w] _ = V.fromVector $ zipWith (-) (applyPermutation sigma wX) wX
       where wX = fmap var w
-    verifier' _ _ _ = error "Invalid transcript"
+    algebraicMap _ _ _ _ = error "Invalid transcript"
 
 
     verifier :: ProtostarPermutation n
              -> Input f (ProtostarPermutation n)
-             -> SpecialSoundTranscript f (ProtostarPermutation n)
+             -> [ProverMessage f (ProtostarPermutation n)]
+             -> [VerifierMessage f (ProtostarPermutation n)]
              -> Bool
-    verifier _ sigma [(w, _)] = applyPermutation sigma w == w
-    verifier _ _     _        = error "Invalid transcript"
+    verifier _ sigma [w] _ = applyPermutation sigma w == w
+    verifier _ _     _   _ = error "Invalid transcript"
diff --git a/src/ZkFold/Base/Protocol/ARK/Protostar/SpecialSound.hs b/src/ZkFold/Base/Protocol/ARK/Protostar/SpecialSound.hs
index 11e1f560b..a75488e60 100644
--- a/src/ZkFold/Base/Protocol/ARK/Protostar/SpecialSound.hs
+++ b/src/ZkFold/Base/Protocol/ARK/Protostar/SpecialSound.hs
@@ -6,29 +6,52 @@ import           Numeric.Natural                              (Natural)
 import           Prelude                                      hiding (length)
 
 import           ZkFold.Base.Algebra.Polynomials.Multivariate (Poly)
-import           ZkFold.Base.Data.Vector                      (Vector)
 import           ZkFold.Symbolic.Compiler.Arithmetizable      (Arithmetic)
 
 type SpecialSoundTranscript t a = [(ProverMessage t a, VerifierMessage t a)]
 
+type LMap f = [Poly f Natural Natural]
+
+{-- | Section 3.1
+
+The protocol Πsps has 3 essential parameters k, d, l ∈ N, meaning that Πsps is a (2k − 1)-
+move protocol with verifier degree d and output length l (i.e. the verifier checks l degree
+d algebraic equations). In each round i (1 ≤ i ≤ k), the prover Psps(pi, w, [mj , rj], j=1 to i-1)
+generates the next message mi on input the public input pi, the witness w, and the current
+transcript [mj , rj], j=1 to i-1, and sends mi to the verifier; the verifier replies with a random
+challenge ri ∈ F. After the final message mk, the verifier computes the algebraic map Vsps
+and checks that the output is a zero vector of length l.
+
+--}
 class Arithmetic f => SpecialSoundProtocol f a where
       type Witness f a
       type Input f a
       type ProverMessage t a
       type VerifierMessage t a
 
-      type Dimension a :: Natural
-      -- ^ l in the paper
       type Degree a :: Natural
-      -- ^ d in the paper
+      -- ^ d in the paper, the verifier degree
+
+      outputLength :: a -> Natural
+      -- ^ l in the paper, the number of algebraic equations checked by the verifier
 
       rounds :: a -> Natural
       -- ^ k in the paper
 
       prover :: a -> Witness f a -> Input f a -> SpecialSoundTranscript f a -> ProverMessage f a
 
-      verifier' :: a -> Input f a -> SpecialSoundTranscript Natural a
-            -> Vector (Dimension a) (Poly f Natural Natural)
-
-      verifier :: a -> Input f a -> SpecialSoundTranscript f a -> Bool
+      algebraicMap
+          :: a
+          -> Input f a
+          -> [ProverMessage Natural a]
+          -> [VerifierMessage Natural a]
+          -> LMap f
+      -- ^ the algebraic map V_sps computed by the verifier.
+      -- The j-th element of the vector is a homogeneous degree-j algebraic map that outputs a vector of @Dimension a@ field elements.
+      -- Variables have natural indices from @0@ to @2k@:
+      -- Variable @0@ is public input
+      -- Variables @1@ to @k@ are prover messages from the transcript
+      -- Variables @k+1@ to @2k@ are random challenges from the verifier
+
+      verifier :: a -> Input f a -> [ProverMessage f a] -> [VerifierMessage f a] -> Bool
 
diff --git a/src/ZkFold/Base/Protocol/Commitment/KZG.hs b/src/ZkFold/Base/Protocol/Commitment/KZG.hs
index 129a44ae7..9429183f2 100644
--- a/src/ZkFold/Base/Protocol/Commitment/KZG.hs
+++ b/src/ZkFold/Base/Protocol/Commitment/KZG.hs
@@ -11,7 +11,6 @@ import           Data.Kind                                  (Type)
 import           Data.Map.Strict                            (Map, fromList, insert, keys, toList, (!))
 import qualified Data.Vector                                as V
 import           Data.Vector.Binary                         ()
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Num (..), length, sum, (/), (^))
 import           Test.QuickCheck                            (Arbitrary (..), chooseInt)
 
diff --git a/src/ZkFold/Symbolic/Algorithms/Hash/Blake2b.hs b/src/ZkFold/Symbolic/Algorithms/Hash/Blake2b.hs
index a58be0bf4..e4b2ee9e3 100644
--- a/src/ZkFold/Symbolic/Algorithms/Hash/Blake2b.hs
+++ b/src/ZkFold/Symbolic/Algorithms/Hash/Blake2b.hs
@@ -10,7 +10,6 @@ import           Data.Ratio                                        ((%))
 import           Data.Vector                                       ((!), (//))
 import qualified Data.Vector                                       as V
 import           GHC.IsList                                        (IsList (..))
-import           GHC.Natural                                       (Natural)
 import qualified GHC.Num                                           as GHC
 import           Prelude                                           hiding (Num (..), concat, divMod, length, mod,
                                                                     replicate, splitAt, truncate, (!!), (&&), (^))
diff --git a/src/ZkFold/Symbolic/Algorithms/Hash/SHA2.hs b/src/ZkFold/Symbolic/Algorithms/Hash/SHA2.hs
index 6d9d84b4e..84040b812 100644
--- a/src/ZkFold/Symbolic/Algorithms/Hash/SHA2.hs
+++ b/src/ZkFold/Symbolic/Algorithms/Hash/SHA2.hs
@@ -16,7 +16,7 @@ import           Data.Type.Bool                                 (If)
 import qualified Data.Vector                                    as V
 import qualified Data.Vector.Mutable                            as VM
 import           GHC.TypeLits                                   (Symbol)
-import           GHC.TypeNats                                   (Natural, natVal, type (<=?))
+import           GHC.TypeNats                                   (natVal, type (<=?))
 import           Prelude                                        (Int, id, pure, zip, ($!), ($), (.), (>>=))
 import qualified Prelude                                        as P
 
diff --git a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs
index 436a04a8d..e864e4659 100644
--- a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs
+++ b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs
@@ -121,8 +121,8 @@ acPrint ac@(ArithmeticCircuit r o) = do
 ---------------------------------- Testing -------------------------------------
 
 checkClosedCircuit
-    :: Arithmetic a
-    => FromConstant a a
+    :: forall a n
+     . Arithmetic a
     => Scale a a
     => Show a
     => ArithmeticCircuit a n
@@ -135,7 +135,6 @@ checkClosedCircuit c@(ArithmeticCircuit r _) = withMaxSuccess 1 $ conjoin [ test
 checkCircuit
     :: Arbitrary a
     => Arithmetic a
-    => FromConstant a a
     => Scale a a
     => Show a
     => ArithmeticCircuit a n
diff --git a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Combinators.hs b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Combinators.hs
index fe77de775..bbc46b366 100644
--- a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Combinators.hs
+++ b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Combinators.hs
@@ -29,7 +29,6 @@ import           Data.Traversable                                          (for)
 import qualified Data.Zip                                                  as Z
 import           GHC.Generics                                              (Par1)
 import           GHC.IsList                                                (IsList (..))
-import           Numeric.Natural                                           (Natural)
 import           Prelude                                                   hiding (Bool, Eq (..), length, negate,
                                                                             splitAt, (!!), (*), (+), (-), (^))
 
diff --git a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs
index 150a332bd..ba0aab2f2 100644
--- a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs
+++ b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs
@@ -16,7 +16,6 @@ import           Data.Traversable                                          (Trav
 import qualified Data.Zip                                                  as Z
 import           GHC.Generics                                              (Par1 (..))
 import           GHC.Num                                                   (integerToNatural)
-import           Numeric.Natural                                           (Natural)
 import           Prelude                                                   (Integer, Show, const, id, mempty, pure,
                                                                             return, show, type (~), ($), (++), (.),
                                                                             (<$>), (>>=))
diff --git a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs
index c34621172..459073a18 100644
--- a/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs
+++ b/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs
@@ -31,9 +31,9 @@ module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal (
 import           Control.DeepSeq                              (NFData, force)
 import           Control.Monad.State                          (MonadState (..), State, gets, modify)
 import           Data.Map.Strict                              hiding (drop, foldl, foldr, map, null, splitAt, take)
+import qualified Data.Map.Strict                              as M
 import qualified Data.Set                                     as S
 import           GHC.Generics                                 (Generic, Par1 (..))
-import           Numeric.Natural                              (Natural)
 import           Optics
 import           Prelude                                      hiding (Num (..), drop, length, product, splitAt, sum,
                                                                take, (!!), (^))
@@ -42,6 +42,7 @@ import           System.Random                                (StdGen, mkStdGen,
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field              (Zp, fromZp, toZp)
+import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381  (BLS12_381_Scalar)
 import           ZkFold.Base.Algebra.Polynomials.Multivariate (Mono, Poly, evalMonomial, evalPolynomial, mapCoeffs, var)
 import           ZkFold.Base.Control.HApplicative
@@ -114,14 +115,14 @@ instance Eq a => Semigroup (Circuit a) where
     c1 <> c2 =
         Circuit
            {
-               acSystem   = {-# SCC system_union #-}    acSystem c1 `union` acSystem c2
-            ,  acRange    = {-# SCC range_union #-}     acRange c1 `union` acRange c2
+               acSystem   = acSystem c1 `union` acSystem c2
+            ,  acRange    = acRange c1 `union` acRange c2
                -- NOTE: is it possible that we get a wrong argument order when doing `apply` because of this concatenation?
                -- We need a way to ensure the correct order no matter how `(<>)` is used.
-           ,   acInput    = {-# SCC input_union #-}     nubConcat (acInput c1) (acInput c2)
-           ,   acWitness  = {-# SCC witness_union #-}   acWitness c1 `union` acWitness c2
-           ,   acVarOrder = {-# SCC var_order_union #-} acVarOrder c1 `union` acVarOrder c2
-           ,   acRNG      = {-# SCC rng_union #-}       mkStdGen $ fst (uniform (acRNG c1)) Haskell.* fst (uniform (acRNG c2))
+           ,   acInput    = nubConcat (acInput c1) (acInput c2)
+           ,   acWitness  = acWitness c1 `union` acWitness c2
+           ,   acVarOrder = acVarOrder c1 `union` acVarOrder c2
+           ,   acRNG      = mkStdGen $ fst (uniform (acRNG c1)) Haskell.* fst (uniform (acRNG c2))
            }
 
 nubConcat :: Ord a => [a] -> [a] -> [a]
@@ -169,7 +170,7 @@ newVariableWithSource srcs con = toVar srcs . con . fst <$> do
 addVariable :: Natural -> State (Circuit a) Natural
 addVariable x = do
     zoom #acVarOrder . modify
-        $ \vo -> insert (length vo, x) x vo
+        $ \vo -> insert (Haskell.fromIntegral $ M.size vo, x) x vo
     pure x
 
 ---------------------------------- Low-level functions --------------------------------
diff --git a/src/ZkFold/Symbolic/Compiler/Arithmetizable.hs b/src/ZkFold/Symbolic/Compiler/Arithmetizable.hs
index 26e2c759b..c0d2a14b0 100644
--- a/src/ZkFold/Symbolic/Compiler/Arithmetizable.hs
+++ b/src/ZkFold/Symbolic/Compiler/Arithmetizable.hs
@@ -14,7 +14,6 @@ module ZkFold.Symbolic.Compiler.Arithmetizable (
     ) where
 
 import           Data.Typeable                                       (Typeable)
-import           Numeric.Natural                                     (Natural)
 import           Prelude                                             hiding (Bool, Num (..), drop, length, product,
                                                                       splitAt, sum, take, (!!), (^))
 
diff --git a/src/ZkFold/Symbolic/Data/ByteString.hs b/src/ZkFold/Symbolic/Data/ByteString.hs
index b5ee2e844..a97f4261e 100644
--- a/src/ZkFold/Symbolic/Data/ByteString.hs
+++ b/src/ZkFold/Symbolic/Data/ByteString.hs
@@ -30,7 +30,7 @@ import           Data.String                                               (IsSt
 import           Data.Traversable                                          (for)
 import           GHC.Generics                                              (Generic, Par1 (..))
 import           GHC.Natural                                               (naturalFromInteger)
-import           GHC.TypeNats                                              (Natural, natVal)
+import           GHC.TypeNats                                              (natVal)
 import           Prelude                                                   (Integer, drop, fmap, otherwise, pure, take,
                                                                             type (~), ($), (.), (<$>), (<), (<>), (==),
                                                                             (>=))
diff --git a/src/ZkFold/Symbolic/Data/Ed25519.hs b/src/ZkFold/Symbolic/Data/Ed25519.hs
index cee23fb79..fe40a24ed 100644
--- a/src/ZkFold/Symbolic/Data/Ed25519.hs
+++ b/src/ZkFold/Symbolic/Data/Ed25519.hs
@@ -8,7 +8,6 @@
 module ZkFold.Symbolic.Data.Ed25519  where
 
 import           Data.Void                                 (Void)
-import           GHC.TypeNats                              (Natural)
 import           Prelude                                   (type (~), ($), (.))
 import qualified Prelude                                   as P
 
diff --git a/src/ZkFold/Symbolic/Data/FieldElement.hs b/src/ZkFold/Symbolic/Data/FieldElement.hs
index 09a2c0dc0..30120c9a7 100644
--- a/src/ZkFold/Symbolic/Data/FieldElement.hs
+++ b/src/ZkFold/Symbolic/Data/FieldElement.hs
@@ -6,7 +6,6 @@
 module ZkFold.Symbolic.Data.FieldElement where
 
 import           GHC.Generics                                        (Par1 (..))
-import           Numeric.Natural                                     (Natural)
 import           Prelude                                             hiding (Bool, Eq, Num (..), Ord, drop, length,
                                                                       product, splitAt, sum, take, (!!), (^))
 import qualified Prelude                                             as Haskell
diff --git a/src/ZkFold/Symbolic/Data/UInt.hs b/src/ZkFold/Symbolic/Data/UInt.hs
index 5a56b0925..0f688ce4a 100644
--- a/src/ZkFold/Symbolic/Data/UInt.hs
+++ b/src/ZkFold/Symbolic/Data/UInt.hs
@@ -27,7 +27,6 @@ import           Data.Tuple                                                (swap
 import qualified Data.Zip                                                  as Z
 import           GHC.Generics                                              (Generic, Par1 (..))
 import           GHC.Natural                                               (naturalFromInteger)
-import           GHC.TypeNats                                              (Natural)
 import           Prelude                                                   (Integer, error, flip, otherwise, return,
                                                                             type (~), ($), (++), (.), (<>), (>>=))
 import qualified Prelude                                                   as Haskell
@@ -268,6 +267,7 @@ instance
     , KnownNat (r + r)
     , KnownRegisterSize rs
     , r ~ NumberOfRegisters (BaseField b) n rs
+    , NFData (b (Vector r))
     , Ord (Bool b) (UInt n rs b)
     , AdditiveGroup (UInt n rs b)
     , Semiring (UInt n rs b)
@@ -296,7 +296,7 @@ instance
                 -> Natural
                 -> (UInt n rs b, UInt n rs b)
             longDivisionStep (q', r') i =
-                let rs = addBit (r' + r') (value @n -! i -! 1)
+                let rs = force $ addBit (r' + r') (value @n -! i -! 1)
                  in bool @(Bool b) (q', rs) (q' + fromConstant ((2 :: Natural) ^ i), rs - d) (rs >= d)
 
 instance (Arithmetic a, KnownNat n, KnownRegisterSize r, KnownNat (NumberOfRegisters a n r)) => Ord (Bool (ArithmeticCircuit a)) (UInt n r (ArithmeticCircuit a)) where
diff --git a/tests/Main.hs b/tests/Main.hs
index b2921a838..c8d14dfdc 100644
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -1,6 +1,8 @@
 module Main where
 
+import           Control.Monad             (when)
 import           Prelude                   hiding (Bool, Fractional (..), Num (..), drop, length, replicate, take, (==))
+import           System.Environment        (lookupEnv)
 import           Tests.ArithmeticCircuit   (specArithmeticCircuit)
 import           Tests.Arithmetization     (specArithmetization)
 import           Tests.Binary              (specBinary)
@@ -13,7 +15,7 @@ import           Tests.Group               (specAdditiveGroup)
 import           Tests.NonInteractiveProof (specNonInteractiveProof)
 import           Tests.Pairing             (specPairing)
 import           Tests.Permutations        (specPermutations)
-import           Tests.SHA2                (specSHA2Natural)
+import           Tests.SHA2                (specSHA2, specSHA2Natural)
 import           Tests.UInt                (specUInt)
 import           Tests.Univariate          (specUnivariate)
 
@@ -34,10 +36,6 @@ main = do
     specUInt
     specFFA
     specByteString
-    --TODO: implement a proper blake2b test
-    specBlake2b
-    --TODO: optimise eval and uncomment this test
-    -- specSHA2
 
     -- Arithmetic circuit
     specArithmeticCircuit
@@ -50,5 +48,12 @@ main = do
 
     -- Cryptography
     specSHA2Natural
+    -- These tests are slow. Only run them locally by setting the environment variable FULL_SHA2
+    fullTests <- lookupEnv "FULL_SHA2"
+    when (not . null $ fullTests) specSHA2
+
+    --TODO: implement a proper blake2b test
+    specBlake2b
+
 
     putStrLn "\nAll tests passed!"
diff --git a/tests/Tests/ArithmeticCircuit.hs b/tests/Tests/ArithmeticCircuit.hs
index 7289595a8..592352e71 100644
--- a/tests/Tests/ArithmeticCircuit.hs
+++ b/tests/Tests/ArithmeticCircuit.hs
@@ -22,19 +22,19 @@ import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.DiscreteField
 import           ZkFold.Symbolic.Data.Eq
 
-correctHom0 :: forall a . (Arithmetic a, FromConstant a a, Scale a a, Show a) => (forall b . Field b => b) -> Property
+correctHom0 :: forall a . (Arithmetic a, Scale a a, Show a) => (forall b . Field b => b) -> Property
 correctHom0 f = let r = f in withMaxSuccess 1 $ checkClosedCircuit r .&&. exec1 r === f @a
 
-correctHom1 :: forall a . (Arithmetic a, FromConstant a a, Scale a a, Show a) => (forall b . Field b => b -> b) -> a -> Property
+correctHom1 :: forall a . (Arithmetic a, Scale a a, Show a) => (forall b . Field b => b -> b) -> a -> Property
 correctHom1 f x = let r = f (embed x) in checkClosedCircuit r .&&. exec1 r === f x
 
-correctHom2 :: forall a . (Arithmetic a, FromConstant a a, Scale a a, Show a) => (forall b . Field b => b -> b -> b) -> a -> a -> Property
+correctHom2 :: forall a . (Arithmetic a, Scale a a, Show a) => (forall b . Field b => b -> b -> b) -> a -> a -> Property
 correctHom2 f x y = let r = f (embed x) (embed y) in checkClosedCircuit r .&&. exec1 r === f x y
 
 it :: Testable prop => String -> prop -> Spec
 it desc prop = Test.Hspec.it desc (property prop)
 
-specArithmeticCircuit' :: forall a . (Arbitrary a, Arithmetic a, FromConstant a a, Scale a a, Show a) => IO ()
+specArithmeticCircuit' :: forall a . (Arbitrary a, Arithmetic a, Scale a a, Show a) => IO ()
 specArithmeticCircuit' = hspec $ do
     describe "ArithmeticCircuit specification" $ do
         it "embeds constants" $ correctHom1 @a id
diff --git a/tests/Tests/ByteString.hs b/tests/Tests/ByteString.hs
index 8961d5038..aa49e0619 100644
--- a/tests/Tests/ByteString.hs
+++ b/tests/Tests/ByteString.hs
@@ -9,7 +9,6 @@ import           Control.Monad                               (return)
 import           Data.Function                               (($))
 import           Data.Functor                                ((<$>))
 import           Data.List                                   ((++))
-import           Numeric.Natural                             (Natural)
 import           Prelude                                     (show, type (~), (<>))
 import qualified Prelude                                     as Haskell
 import           System.IO                                   (IO)
diff --git a/tests/Tests/SHA2.hs b/tests/Tests/SHA2.hs
index b0cf22fbd..6e12c2d62 100644
--- a/tests/Tests/SHA2.hs
+++ b/tests/Tests/SHA2.hs
@@ -11,7 +11,6 @@ import           Data.List                                   (isPrefixOf, isSuff
 import           Data.List.Split                             (splitOn)
 import           Data.Proxy                                  (Proxy (..))
 import           GHC.TypeLits                                (KnownSymbol, Symbol, symbolVal)
-import           Numeric.Natural                             (Natural)
 import           Prelude                                     (String, fmap, otherwise, pure, read, (<>), (==))
 import qualified Prelude                                     as Haskell
 import           System.Directory                            (listDirectory)
@@ -19,7 +18,7 @@ import           System.Environment                          (lookupEnv)
 import           System.FilePath.Posix
 import           System.IO                                   (IO)
 import           Test.Hspec                                  (Spec, describe, hspec, shouldBe)
-import           Test.QuickCheck                             (Gen, (===))
+import           Test.QuickCheck                             (Gen, withMaxSuccess, (===))
 import           Tests.ArithmeticCircuit                     (it)
 import           Text.Regex.TDFA
 
@@ -146,7 +145,7 @@ specSHA2bs
 specSHA2bs = do
     let n = value @n
         m = 2 ^ n -! 1
-    it ("calculates " <> symbolVal (Proxy @algorithm) <> " of a " <> Haskell.show n <> "-bit bytestring") $ do
+    it ("calculates " <> symbolVal (Proxy @algorithm) <> " of a " <> Haskell.show n <> "-bit bytestring") $ withMaxSuccess 2 $ do
         x <- toss m
         let hashAC = sha2 @algorithm @(ArithmeticCircuit (Zp BLS12_381_Scalar)) @n $ fromConstant x
             ByteString (Interpreter hashZP) = sha2Natural @algorithm @(Interpreter (Zp BLS12_381_Scalar)) n x
@@ -160,24 +159,14 @@ specSHA2'
     .  KnownSymbol algorithm
     => SHA2N algorithm (Interpreter (Zp BLS12_381_Scalar))
     => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 1
-    => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 2
-    => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 3
-    => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 4
-    => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 10
     => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 63
     => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 64
-    => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 900
     => SHA2 algorithm (ArithmeticCircuit (Zp BLS12_381_Scalar)) 1900
     => IO ()
 specSHA2' = hspec $ do
     specSHA2bs @1    @algorithm
-    specSHA2bs @2    @algorithm
-    specSHA2bs @3    @algorithm
-    specSHA2bs @4    @algorithm
-    specSHA2bs @10   @algorithm
     specSHA2bs @63   @algorithm
     specSHA2bs @64   @algorithm
-    specSHA2bs @900  @algorithm
     specSHA2bs @1900 @algorithm
 
 specSHA2 :: IO ()
diff --git a/tests/Tests/UInt.hs b/tests/Tests/UInt.hs
index c0ef1d042..4e4b3f16d 100644
--- a/tests/Tests/UInt.hs
+++ b/tests/Tests/UInt.hs
@@ -7,12 +7,11 @@
 module Tests.UInt (specUInt) where
 
 import           Control.Applicative                         ((<*>))
-import           Control.Monad                               (return)
+import           Control.Monad                               (return, when)
 import           Data.Function                               (($))
 import           Data.Functor                                ((<$>))
 import           Data.List                                   ((++))
 import           GHC.Generics                                (Par1 (Par1))
-import           Numeric.Natural                             (Natural)
 import           Prelude                                     (show, type (~))
 import qualified Prelude                                     as P
 import           System.IO                                   (IO)
@@ -98,15 +97,13 @@ specUInt' = hspec $ do
         it "subtracts correctly" $ isHom @n @p @rs (-) (-) <$> toss m <*> toss m
         it "multiplies correctly" $ isHom @n @p @rs (*) (*) <$> toss m <*> toss m
 
-        -- TODO: Optimise exec and uncomment this test
-        {--
-        it "performs divMod correctly" $ do
-            n <- toss m
+        -- TODO: reduce the number of constraints in divMod or wait for lookup arguments
+        when (n <= 128) $ it "performs divMod correctly" $ withMaxSuccess 10 $ do
+            num <- toss m
             d <- toss m
-            let (acQ, acR) = (fromConstant n :: UInt n ArithmeticCircuit (Zp p)) `divMod` (fromConstant d)
-            let (zpQ, zpR) = (fromConstant n :: UInt n Vector (Zp p)) `divMod` (fromConstant d)
+            let (acQ, acR) = (fromConstant num :: UInt n rs (ArithmeticCircuit (Zp p))) `divMod` (fromConstant d)
+            let (zpQ, zpR) = (fromConstant num :: UInt n rs (Interpreter (Zp p))) `divMod` (fromConstant d)
             return $ (execAcUint acQ, execAcUint acR) === (execZpUint zpQ, execZpUint zpR)
-        --}
 
         it "calculates gcd correctly" $ withMaxSuccess 10 $ do
             x <- toss m
diff --git a/tests/Tests/Univariate/PolyVec.hs b/tests/Tests/Univariate/PolyVec.hs
index 3a6ca53c5..10233b58e 100644
--- a/tests/Tests/Univariate/PolyVec.hs
+++ b/tests/Tests/Univariate/PolyVec.hs
@@ -12,7 +12,6 @@ import           Data.Data                                   (Typeable, typeOf)
 import           Data.List                                   ((\\))
 import qualified Data.Vector                                 as V
 import qualified Data.Vector.Algorithms.Intro                as VA
-import           Numeric.Natural                             (Natural)
 import           Prelude                                     hiding (Fractional (..), Num (..), drop, length, take,
                                                               (!!), (^))
 import           Prelude                                     (abs)
diff --git a/zkfold-base.cabal b/zkfold-base.cabal
index 9750469f6..c14596d49 100644
--- a/zkfold-base.cabal
+++ b/zkfold-base.cabal
@@ -113,10 +113,13 @@ library
       ZkFold.Base.Protocol.ARK.Plonk.Relation
       ZkFold.Base.Protocol.ARK.Protostar
       ZkFold.Base.Protocol.ARK.Protostar.Accumulator
+      ZkFold.Base.Protocol.ARK.Protostar.AccumulatorScheme
       ZkFold.Base.Protocol.ARK.Protostar.CommitOpen
+      ZkFold.Base.Protocol.ARK.Protostar.FiatShamir
       ZkFold.Base.Protocol.ARK.Protostar.Internal
       ZkFold.Base.Protocol.ARK.Protostar.Gate
       ZkFold.Base.Protocol.ARK.Protostar.Lookup
+      ZkFold.Base.Protocol.ARK.Protostar.Oracle
       ZkFold.Base.Protocol.ARK.Protostar.Permutation
       ZkFold.Base.Protocol.ARK.Protostar.SpecialSound
       ZkFold.Base.Protocol.Commitment.KZG
@@ -200,6 +203,7 @@ library
       containers                            < 0.7,
       cryptohash-sha256                    < 0.12,
       deepseq                          <= 1.5.0.0,
+      lens                                       ,
       mtl                                   < 2.4,
       optics                                < 0.5,
       parallel                          < 3.2.3.0,
@@ -221,7 +225,9 @@ library
 test-suite zkfold-base-test
     import: options
     type: exitcode-stdio-1.0
-    ghc-options: -rtsopts
+    ghc-options: 
+        -rtsopts
+        "-with-rtsopts=-A128M -AL256m -qb0 -qn4 -N" 
     main-is: Main.hs
     other-modules:
       Tests.ArithmeticCircuit
@@ -326,3 +332,22 @@ benchmark arithmetic-circuit
       time,
       vector,
       zkfold-base 
+
+benchmark division 
+    import:           options
+    main-is:          BenchDiv.hs
+    hs-source-dirs:   bench
+    type:             exitcode-stdio-1.0
+    ghc-options:      
+      -rtsopts
+      -O3
+    build-depends: 
+      base, 
+      array,
+      containers,
+      deepseq,
+      random,
+      tasty-bench,
+      time,
+      vector,
+      zkfold-base