Merge pull request #3 from fullstack-development/feature/withdraw-man…

…ual-optimization

Feature/withdraw manual optimization

cabal.project

@@ -44,3 +44,12 @@ constraints:
 
 package nothunks
   flags: +vector
+
+source-repository-package
+  type: git
+  location: https://github.com/well-typed/plutonomy.git
+  tag: 14b9bd46084db1b785b3a99d55f7f10d38165ee8
+  --sha256: wVFNBK6JOTKQX9Ov/SbEmN+ZA79HITQ/axLOmJUJV5o=
+
+package plutonomy
+  flags: +CHaP

src/Ext/Plutarch/Extra/Run.hs

@@ -5,16 +5,18 @@ import Data.ByteString.Short (ShortByteString)
 import Data.Default (Default (..))
 import Data.Text (Text, pack)
 import Plutarch (ClosedTerm, Script, compile)
-import Plutarch.Evaluate (evalScript)
+import Plutarch.Evaluate (evalScript')
 import Plutarch.Prelude
 import Plutarch.Script (Script (..), serialiseScript)
+import Plutonomy (optimizeUPLC)
 import PlutusCore (
   DeBruijn,
   DefaultFun,
   DefaultUni,
  )
 import PlutusCore.Data (Data)
-import PlutusCore.Evaluation.Machine.ExBudget (ExBudget)
+import PlutusCore.Evaluation.Machine.ExBudget (ExBudget (ExBudget))
+import PlutusCore.Evaluation.Machine.ExMemory (ExCPU (..), ExMemory (..))
 import PlutusCore.MkPlc (mkConstant, mkIterApp)
 import PlutusPrelude (over)
 import UntypedPlutusCore (Program, progTerm)
@@ -34,7 +36,9 @@ evalT x = evalWithArgsT x []
 evalWithArgsT :: ClosedTerm a -> [Data] -> Either Text (Script, ExBudget, [Text])
 evalWithArgsT x args = do
   cmp <- compile def x
-  let (escr, budg, trc) = evalScript $ applyArguments cmp args
+  let optimized = Script $ optimizeUPLC (unScript cmp)
+  let budget = ExBudget (ExCPU 10_000_000_000) (ExMemory 14_000_000)
+  let (escr, budg, trc) = evalScript' budget $ applyArguments optimized args
   scr <- first (pack . show) escr
   pure (scr, budg, trc)
 

src/Plutarch/Pairing/Group.hs

@@ -4,6 +4,7 @@ import Ext.Plutarch.Num (ppow)
 import qualified Plutarch.Monadic as P
 import Plutarch.Num (PNum (..))
 import Plutarch.Pairing.BN128 (_q)
+import Plutarch.Pairing.Group.Class as Export
 import Plutarch.Pairing.Group.Fq as Export
 import Plutarch.Pairing.Group.Fq12 as Export
 import Plutarch.Pairing.Group.Fq2 as Export

src/Plutarch/Pairing/Group/Class.hs

@@ -0,0 +1,12 @@
+module Plutarch.Pairing.Group.Class where
+
+import Plutarch.Prelude
+
+class PSemigroup (a :: PType) where
+  pappend :: Term s a -> Term s a -> Term s a
+
+class (PSemigroup a) => PMonoid (a :: PType) where
+  pidentity :: Term s a
+
+class (PMonoid a) => PGroup (a :: PType) where
+  pinv :: Term s a -> Term s a

src/Plutarch/Pairing/Group/Fq.hs

@@ -4,6 +4,11 @@ import Ext.Plutarch.Rational (pgcdExt)
 import qualified Plutarch.Monadic as P
 import Plutarch.Num (PNum (..))
 import Plutarch.Pairing.BN128 (_nqr, _q)
+import Plutarch.Pairing.Group.Class (
+  PGroup (..),
+  PMonoid (..),
+  PSemigroup (..),
+ )
 import Plutarch.Prelude
 import qualified Plutus.Pairing.BN128 as Plutus
 import qualified PlutusTx.Monoid as PlutusTx
@@ -43,29 +48,45 @@ pmkFq :: Integer -> Term s PFq
 pmkFq i = pcon . PFq . pconstant $ i `PlutusTx.modulo` Plutus._q
 
 pfqAdd :: Term s PFq -> Term s PFq -> Term s PFq
-pfqAdd at bt = P.do
-  PFq a <- pmatch at
-  PFq b <- pmatch bt
-  pfq $ pmod # (a + b) # _q
+pfqAdd at bt = pfqAdd' # at # bt
+
+pfqAdd' :: Term s (PFq :--> PFq :--> PFq)
+pfqAdd' = phoistAcyclic $ plam
+  \at bt -> P.do
+    PFq a <- pmatch at
+    PFq b <- pmatch bt
+    pfq $ pmod # (a + b) # _q
 
 pfqSub :: Term s PFq -> Term s PFq -> Term s PFq
-pfqSub at bt = P.do
-  PFq a <- pmatch at
-  PFq b <- pmatch bt
-  pfq $ pmod # (a - b) # _q
+pfqSub at bt = pfqSub' # at # bt
+
+pfqSub' :: Term s (PFq :--> PFq :--> PFq)
+pfqSub' = phoistAcyclic $ plam
+  \at bt -> P.do
+    PFq a <- pmatch at
+    PFq b <- pmatch bt
+    pfq $ pmod # (a - b) # _q
 
 pfqMul :: Term s PFq -> Term s PFq -> Term s PFq
-pfqMul at bt = P.do
-  PFq a <- pmatch at
-  PFq b <- pmatch bt
-  pfq $ pmod # (a * b) # _q
+pfqMul at bt = pfqMul' # at # bt
+
+pfqMul' :: Term s (PFq :--> PFq :--> PFq)
+pfqMul' = phoistAcyclic $ plam
+  \at bt -> P.do
+    PFq a <- pmatch at
+    PFq b <- pmatch bt
+    pfq $ pmod # (a * b) # _q
 
--- | Multiplicative inverse
 pfqInv :: Term s PFq -> Term s PFq
-pfqInv t = P.do
-  PFq a <- pmatch t
-  PPair i _ <- pmatch $ pgcdExt # a # _q
-  pfq $ pmod # i # _q
+pfqInv t = pfqInv' # t
+
+-- | Multiplicative inverse
+pfqInv' :: Term s (PFq :--> PFq)
+pfqInv' = phoistAcyclic $ plam
+  \t -> P.do
+    PFq a <- pmatch t
+    PPair i _ <- pmatch $ pgcdExt # a # _q
+    pfq $ pmod # i # _q
 
 -- | Quadratic non-residue
 pfqNqr :: Term s PFq
@@ -79,3 +100,12 @@ instance PlutusTx.Monoid (Term s PFq) where
 
 instance PlutusTx.Group (Term s PFq) where
   inv = pfqInv
+
+instance PSemigroup PFq where
+  pappend = pfqMul
+
+instance PMonoid PFq where
+  pidentity = 1
+
+instance PGroup PFq where
+  pinv = pfqInv

src/Plutarch/Pairing/Group/Fq12.hs

@@ -4,6 +4,11 @@ import Ext.Plutarch.Num (ppow)
 import Plutarch.DataRepr (PDataFields)
 import qualified Plutarch.Monadic as P
 import Plutarch.Num (PNum (..))
+import Plutarch.Pairing.Group.Class (
+  PGroup (..),
+  PMonoid (..),
+  PSemigroup (..),
+ )
 import Plutarch.Pairing.Group.Fq2 (pFq2, pfq2Conj)
 import Plutarch.Pairing.Group.Fq6 (
   PFq6,
@@ -66,70 +71,98 @@ pmkFq12 i =
     y = pdata 0
 
 pfq12Add :: Term s PFq12 -> Term s PFq12 -> Term s PFq12
-pfq12Add at bt = P.do
-  a <- pletFields @'["x", "y"] at
-  b <- pletFields @'["x", "y"] bt
-  pFq12 (a.x + b.x) (a.y + b.y)
+pfq12Add at bt = pfq12Add' # at # bt
+
+pfq12Add' :: Term s (PFq12 :--> PFq12 :--> PFq12)
+pfq12Add' = phoistAcyclic $ plam
+  \at bt -> P.do
+    a <- pletFields @'["x", "y"] at
+    b <- pletFields @'["x", "y"] bt
+    pFq12 (a.x + b.x) (a.y + b.y)
 
 pfq12Sub :: Term s PFq12 -> Term s PFq12 -> Term s PFq12
-pfq12Sub at bt = P.do
-  a <- pletFields @'["x", "y"] at
-  b <- pletFields @'["x", "y"] bt
-  pFq12 (a.x - b.x) (a.y - b.y)
+pfq12Sub at bt = pfq12Sub' # at # bt
+
+pfq12Sub' :: Term s (PFq12 :--> PFq12 :--> PFq12)
+pfq12Sub' = phoistAcyclic $ plam
+  \at bt -> P.do
+    a <- pletFields @'["x", "y"] at
+    b <- pletFields @'["x", "y"] bt
+    pFq12 (a.x - b.x) (a.y - b.y)
 
 pfq12Mul :: Term s PFq12 -> Term s PFq12 -> Term s PFq12
-pfq12Mul at bt = P.do
-  a <- pletFields @'["x", "y"] at
-  b <- pletFields @'["x", "y"] bt
-  xx <- plet (a.x #* b.x)
-  yy <- plet (a.y #* b.y)
-  pFq12 ((pmulXiFq6 # yy) + xx) ((a.x + a.y) * (b.x + b.y) - xx - yy)
+pfq12Mul at bt = pfq12Mul' # at # bt
+
+pfq12Mul' :: Term s (PFq12 :--> PFq12 :--> PFq12)
+pfq12Mul' = phoistAcyclic $ plam
+  \at bt -> P.do
+    a <- pletFields @'["x", "y"] at
+    b <- pletFields @'["x", "y"] bt
+    xx <- plet (a.x #* b.x)
+    yy <- plet (a.y #* b.y)
+    pFq12 ((pmulXiFq6 # yy) + xx) ((a.x + a.y) * (b.x + b.y) - xx - yy)
 
--- | Multiplicative inverse
 pfq12Inv :: Term s PFq12 -> Term s PFq12
-pfq12Inv at = P.do
-  a <- pletFields @'["x", "y"] at
-  t <- plet $ pfq6Inv (a.x * a.x - (pmulXiFq6 # (a.y * a.y)))
-  pFq12 (a.x * t) $ pnegate # (a.y * t)
+pfq12Inv at = pfq12Inv' # at
+
+-- | Multiplicative inverse
+pfq12Inv' :: Term s (PFq12 :--> PFq12)
+pfq12Inv' = phoistAcyclic $ plam
+  \at -> P.do
+    a <- pletFields @'["x", "y"] at
+    t <- plet $ pfq6Inv (a.x * a.x - (pmulXiFq6 # (a.y * a.y)))
+    pFq12 (a.x * t) $ pnegate # (a.y * t)
 
--- | Conjugation
 pfq12Conj :: Term s PFq12 -> Term s PFq12
-pfq12Conj at = P.do
-  a <- pletFields @'["x", "y"] at
-  pFq12 a.x (pnegate # a.y)
+pfq12Conj at = pfq12Conj' # at
+
+-- | Conjugation
+pfq12Conj' :: Term s (PFq12 :--> PFq12)
+pfq12Conj' = phoistAcyclic $ plam
+  \at -> P.do
+    a <- pletFields @'["x", "y"] at
+    pFq12 a.x (pnegate # a.y)
 
 pfastFrobenius1 :: Term s PFq12 -> Term s PFq12
-pfastFrobenius1 term = P.do
-  arg <- pletFields @'["x", "y"] term
-  a <- pletFields @'["x", "y", "z"] arg.x
-  b <- pletFields @'["x", "y", "z"] arg.y
-  cax <- plet $ pfq2Conj a.x
-  cbx <- plet $ pfq2Conj b.x
-  cay <- plet $ pfq2Conj a.y
-  cby <- plet $ pfq2Conj b.y
-  caz <- plet $ pfq2Conj a.z
-  cbz <- plet $ pfq2Conj b.z
-  x <- plet $ pFq6 cax (cay * gamma2) (caz * gamma4)
-  y <- plet $ pFq6 (cbx * gamma1) (cby * gamma3) (cbz * gamma5)
-  pFq12 x y
+pfastFrobenius1 term = pfastFrobenius1' # term
+
+pfastFrobenius1' :: Term s (PFq12 :--> PFq12)
+pfastFrobenius1' = phoistAcyclic $ plam
+  \term -> P.do
+    arg <- pletFields @'["x", "y"] term
+    a <- pletFields @'["x", "y", "z"] arg.x
+    b <- pletFields @'["x", "y", "z"] arg.y
+    cax <- plet $ pfq2Conj a.x
+    cbx <- plet $ pfq2Conj b.x
+    cay <- plet $ pfq2Conj a.y
+    cby <- plet $ pfq2Conj b.y
+    caz <- plet $ pfq2Conj a.z
+    cbz <- plet $ pfq2Conj b.z
+    x <- plet $ pFq6 cax (cay * gamma2) (caz * gamma4)
+    y <- plet $ pFq6 (cbx * gamma1) (cby * gamma3) (cbz * gamma5)
+    pFq12 x y
   where
     gamma1 = pFq2 8376118865763821496583973867626364092589906065868298776909617916018768340080 16469823323077808223889137241176536799009286646108169935659301613961712198316
     gamma2 = pFq2 21575463638280843010398324269430826099269044274347216827212613867836435027261 10307601595873709700152284273816112264069230130616436755625194854815875713954
     gamma3 = pFq2 2821565182194536844548159561693502659359617185244120367078079554186484126554 3505843767911556378687030309984248845540243509899259641013678093033130930403
     gamma4 = pFq2 2581911344467009335267311115468803099551665605076196740867805258568234346338 19937756971775647987995932169929341994314640652964949448313374472400716661030
     gamma5 = pFq2 685108087231508774477564247770172212460312782337200605669322048753928464687 8447204650696766136447902020341177575205426561248465145919723016860428151883
 
+ppowUnitary :: Term s PFq12 -> Term s PInteger -> Term s PFq12
+ppowUnitary x n = ppowUnitary' # x # n
+
 {- | Unitary exponentiation @^@.
 
  Exponentiation of a unitary element @x@ to an arbitrary integer @n@
  in a specified cyclotomic subgroup.
 -}
-ppowUnitary :: Term s PFq12 -> Term s PInteger -> Term s PFq12
-ppowUnitary x n =
-  pif
-    (n #< 0)
-    (ppow # pfq12Conj x # negate n)
-    (ppow # x # n)
+ppowUnitary' :: Term s (PFq12 :--> PInteger :--> PFq12)
+ppowUnitary' = phoistAcyclic $ plam
+  \x n ->
+    pif
+      (n #< 0)
+      (ppow # pfq12Conj x # negate n)
+      (ppow # x # n)
 
 instance PlutusTx.Semigroup (Term s PFq12) where
   (<>) = pfq12Mul
@@ -139,3 +172,12 @@ instance PlutusTx.Monoid (Term s PFq12) where
 
 instance PlutusTx.Group (Term s PFq12) where
   inv = pfq12Inv
+
+instance PSemigroup PFq12 where
+  pappend = pfq12Mul
+
+instance PMonoid PFq12 where
+  pidentity = 1
+
+instance PGroup PFq12 where
+  pinv = pfq12Inv