Clean up Halo2

sellout

Sep 28, 2022, 5:33 PM

SF4ZFNFOVLPGZN4AZPLZNDTE3WHP6CTZEAGNW5A46PCOFAWCNOYQC

Dependencies

• [2] OLNSSFZI Rearrange the halo2 code, and some cleanup
• [3] B27NZRDF Initial commit, with start of some Halo2 junk.

Change contents

• edit in halo2/halo2.cabal at line 22
  [2.680]

  [2.680]
  + -- These are required by @-Weverything@.

  + default-extensions: DerivingStrategies

  + , ImportQualifiedPost

  + , NoImplicitPrelude
• replacement in halo2/PLONKish.hs at line 1
  [3.870]→[3.871:1021](∅→∅),[3.1021]→[3.1021:1050](∅→∅),[3.1050]→[3.1050:1070](∅→∅),[3.1070]→[2.1372:1399](∅→∅),[2.1399]→[3.1070:1090](∅→∅),[3.1070]→[3.1070:1090](∅→∅),[3.1090]→[2.1400:1414](∅→∅),[2.1414]→[3.1090:1121](∅→∅),[3.1090]→[3.1090:1121](∅→∅)
  − {-# language

  − ConstraintKinds,

  − DataKinds,

  − DeriveDataTypeable,

  − DeriveGeneric,

  − DeriveTraversable,

  − GADTs,

  − ImportQualifiedPost,

  − LambdaCase,

  − NoImplicitPrelude,

  − RankNTypes,

  − Safe,

  − StandaloneDeriving

  − #-}
  [3.870]

  [3.1121]
  + {-# LANGUAGE ConstraintKinds #-}

  + {-# LANGUAGE DataKinds #-}

  + {-# LANGUAGE DeriveDataTypeable #-}

  + {-# LANGUAGE DeriveGeneric #-}

  + {-# LANGUAGE DeriveTraversable #-}

  + {-# LANGUAGE GADTs #-}

  + {-# LANGUAGE LambdaCase #-}

  + {-# LANGUAGE RankNTypes #-}

  + {-# LANGUAGE Safe #-}

  + {-# LANGUAGE StandaloneDeriving #-}
• replacement in halo2/PLONKish.hs at line 30
  [2.1478]→[2.1478:1517](∅→∅)
  − import Control.Category (Category(..))
  [2.1478]

  [3.1507]
  + import Control.Category (Category (..))
• replacement in halo2/PLONKish.hs at line 58
  [3.2232]→[3.2232:2310](∅→∅)
  − deriving (Data, Eq, Generic, Ord, Foldable, Functor, Generic1, Traversable)
  [3.2232]

  [3.2310]
  + deriving stock (Data, Eq, Generic, Ord, Foldable, Functor, Generic1, Traversable)
• edit in halo2/PLONKish.hs at line 67
  [3.2583]→[3.2583:2660](∅→∅)
  − -- deriving (Data, Generic, Ord, Foldable, Functor, Generic1, Traversable)
• replacement in halo2/PLONKish.hs at line 68
  [3.2661]→[3.2661:2751](∅→∅)
  − deriving instance Eq a => Eq (BoundedList n a)

  − deriving instance Foldable (BoundedList n)
  [3.2661]

  [3.2751]
  + deriving stock instance Eq a => Eq (BoundedList n a)

  +

  + deriving stock instance Foldable (BoundedList n)
• replacement in halo2/PLONKish.hs at line 75
  [3.2916]→[3.2916:2934](∅→∅)
  − weaken = go where
  [3.2916]

  [3.2934]
  + weaken = go

  + where
• replacement in halo2/PLONKish.hs at line 82
  [3.3132]→[3.3132:3230](∅→∅),[3.3230]→[3.3230:3252](∅→∅)
  − newtype OrderedBoundedList n a =

  − OrderedBoundedList { unorderedBoundedList :: BoundedList n a }

  − deriving (Foldable)
  [3.3132]

  [3.3252]
  + newtype OrderedBoundedList n a = OrderedBoundedList

  + { unorderedBoundedList :: BoundedList n a

  + }

  + deriving stock (Foldable)
• replacement in halo2/PLONKish.hs at line 113
  [3.4229]→[3.4229:4546](∅→∅)
  − data MultivariatePolynomial f maximumDegree c vars

  − -- |

  − --

  − -- __NB__: We could keep @vars@ universal here, but we'd then have to wrap

  − -- it in another @data@ declaration in order to use it in other

  − -- structures. We shuld re-evaluate this later.

  − = MultivariatePolynomial
  [3.4229]

  [3.4546]
  + data MultivariatePolynomial f maximumDegree c vars = MultivariatePolynomial
• replacement in halo2/PLONKish.hs at line 121
  [3.4859]→[3.4859:5020](∅→∅)
  − evaluateMultivariatePolynomial

  − :: (Field f, Nat.SNatI r)

  − => MultivariatePolynomial f maximumDegree c vars

  − -> Circuit f c r maximumDegree

  − -> Fin r

  − -> f
  [3.4859]

  [3.5020]
  + evaluateMultivariatePolynomial ::

  + (Field f, Nat.SNatI r) =>

  + MultivariatePolynomial f maximumDegree c vars ->

  + Circuit f c r maximumDegree ->

  + Fin r ->

  + f
• replacement in halo2/PLONKish.hs at line 140
  [3.5296]→[3.5296:5424](∅→∅)
  − data MultivarPoly f maximumConstraintDegree c =

  − forall v. MultivarPoly (MultivariatePolynomial f maximumConstraintDegree c v)
  [3.5296]

  [3.5424]
  + data MultivarPoly f maximumConstraintDegree c

  + = forall v. MultivarPoly (MultivariatePolynomial f maximumConstraintDegree c v)
• replacement in halo2/PLONKish.hs at line 172
  [3.6694]→[3.6694:6813](∅→∅)
  − circuit

  − :: Configuration f c maximumConstraintDegree

  − -> Vec c (Vec r f)

  − -> Circuit f c r maximumConstraintDegree
  [3.6694]

  [3.6813]
  + circuit ::

  + Configuration f c maximumConstraintDegree ->

  + Vec c (Vec r f) ->

  + Circuit f c r maximumConstraintDegree
• replacement in halo2/PLONKish.hs at line 180
  [3.6935]→[3.6935:6944](∅→∅)
  − -- |
  [3.6935]

  [3.6944]
  + | -- |
• replacement in halo2/PLONKish.hs at line 183
  [3.7018]→[3.7018:7068](∅→∅),[3.7068]→[3.7068:7089](∅→∅)
  − | TautologicalEqualityConstraint (Fin c, Fin r)

  − deriving (Eq, Ord)
  [3.7018]

  [3.7089]
  + TautologicalEqualityConstraint (Fin c, Fin r)

  + deriving stock (Eq, Ord)
• replacement in halo2/PLONKish.hs at line 209
  [3.7999]→[3.7999:8159](∅→∅)
  − addEqualityConstraint

  − :: (Fin c, Fin r)

  − -> (Fin c, Fin r)

  − -> Circuit f c r mcd

  − -> Either (NonEmpty (EqualityConstraintFailure c r)) (Circuit f c r mcd)
  [3.7999]

  [3.8159]
  + addEqualityConstraint ::

  + (Fin c, Fin r) ->

  + (Fin c, Fin r) ->

  + Circuit f c r mcd ->

  + Either (NonEmpty (EqualityConstraintFailure c r)) (Circuit f c r mcd)
• replacement in halo2/PLONKish.hs at line 216
  [2.1905]→[2.1905:1928](∅→∅),[2.1928]→[3.8225:8334](∅→∅),[3.8225]→[3.8225:8334](∅→∅)
  − ( pure $ circuit {

  − equalityConstraints' =

  − Set.insert (orderedPair a b) (equalityConstraints' circuit)

  − }
  [2.1905]

  [3.8334]
  + ( pure $

  + circuit

  + { equalityConstraints' =

  + Set.insert (orderedPair a b) (equalityConstraints' circuit)

  + }
• replacement in halo2/PLONKish.hs at line 224
  [3.8355]→[3.8355:8417](∅→∅)
  − $ validateEqualityConstraint (configuration circuit) a b
  [3.8355]

  [3.8417]
  + $ validateEqualityConstraint (configuration circuit) a b
• replacement in halo2/PLONKish.hs at line 226
  [3.8418]→[3.8418:8445](∅→∅),[3.8445]→[3.8445:8472](∅→∅),[3.8472]→[3.8472:8549](∅→∅)
  − validateEqualityConstraint

  − :: Configuration f c mcd

  − -> (Fin c, Fin r)

  − -> (Fin c, Fin r)

  − -> [EqualityConstraintFailure c r]
  [3.8418]

  [3.8549]
  + validateEqualityConstraint ::

  + forall f c mcd r.

  + Configuration f c mcd ->

  + (Fin c, Fin r) ->

  + (Fin c, Fin r) ->

  + [EqualityConstraintFailure c r]
• replacement in halo2/PLONKish.hs at line 235
  [3.8644]→[3.8644:8724](∅→∅)
  − catMaybes [reifyEqualityCheck config a, reifyEqualityCheck config b]
  [3.8644]

  [3.8724]
  + catMaybes [reifyEqualityCheck config a, reifyEqualityCheck config b]
• edit in halo2/PLONKish.hs at line 240
  [3.8839]

  [3.8839]
  + reifyEqualityCheck ::

  + Configuration f c mcd ->

  + (Fin c, b) ->

  + Maybe (EqualityConstraintFailure c r)