wip

Author: SeungheonOh

plutus-core/plutus-core.cabal

@@ -240,6 +240,7 @@ library
     PlutusCore.Builtin.KnownKind
     PlutusCore.Builtin.KnownType
     PlutusCore.Builtin.KnownTypeAst
+    PlutusCore.Builtin.Let
     PlutusCore.Builtin.Meaning
     PlutusCore.Builtin.Polymorphism
     PlutusCore.Builtin.Result

plutus-core/plutus-core/src/PlutusCore/Builtin.hs

@@ -9,6 +9,7 @@ import PlutusCore.Builtin.HasConstant as Export
 import PlutusCore.Builtin.KnownKind as Export
 import PlutusCore.Builtin.KnownType as Export
 import PlutusCore.Builtin.KnownTypeAst as Export
+import PlutusCore.Builtin.Let as Export
 import PlutusCore.Builtin.Meaning as Export
 import PlutusCore.Builtin.Polymorphism as Export
 import PlutusCore.Builtin.Result as Export

plutus-core/plutus-core/src/PlutusCore/Builtin/Let.hs

@@ -0,0 +1,45 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TypeOperators     #-}
+
+module PlutusCore.Builtin.Let where
+
+import PlutusCore.Builtin.KnownType (Spine)
+import PlutusCore.Core.Type (Type, UniOf)
+import PlutusCore.Name.Unique (TyName)
+
+import Control.DeepSeq (NFData (..), rwhnf)
+import Data.Default.Class (Default (..))
+import Data.Text (Text)
+import Data.Vector (Vector)
+import NoThunks.Class
+import Text.PrettyBy (display)
+import Universe
+
+
+class LetBuiltin uni where
+    -- | Given a constant with its type tag and a vector of branches, choose the appropriate branch
+    -- or fail if the constant doesn't correspond to any of the branches (or casing on constants of
+    -- this type isn't supported at all).
+    letBuiltin
+        :: Some (ValueOf uni)
+        -> Either Text [Some (ValueOf uni)]
+
+data LeterBuiltin uni = LeterBuiltin
+    { unLeterBuiltin :: !(Some (ValueOf uni) -> Either Text [Some (ValueOf uni)])
+    }
+
+instance NFData (LeterBuiltin uni) where
+    rnf = rwhnf
+
+deriving via OnlyCheckWhnfNamed "PlutusCore.Builtin.Case.LeterBuiltin" (LeterBuiltin uni)
+    instance NoThunks (LeterBuiltin uni)
+
+instance LetBuiltin uni => Default (LeterBuiltin uni) where
+    def = LeterBuiltin letBuiltin
+
+unavailableLeterBuiltin :: Int -> LeterBuiltin uni
+unavailableLeterBuiltin ver =
+    LeterBuiltin $ \_ -> Left $
+        "'let' TODO " <> display ver

plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs

@@ -50,7 +50,7 @@ import PlutusCore.Core.Type (Type (..))
 import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
 import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
 import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
-import PlutusCore.Data (Data)
+import PlutusCore.Data (Data (Constr))
 import PlutusCore.Evaluation.Machine.ExMemoryUsage (IntegerCostedLiterally (..),
                                                     NumBytesCostedAsNumWords (..))
 import PlutusCore.Pretty.Extra (juxtRenderContext)
@@ -651,11 +651,28 @@ instance CaseBuiltin DefaultUni where
               case x of
                 (l, r) -> Right $ headSpine (branches Vector.! 0) [someValueOf tyL l, someValueOf tyR r]
             | otherwise -> Left $ outOfBoundsErr someVal branches
+        DefaultUniData ->
+          case x of
+            Constr ix ds
+              | 0 <= ix && ix < toInteger len ->
+                Right $
+                  headSpine
+                    (branches Vector.! (fromIntegral ix))
+                    (someValueOf DefaultUniData <$> ds)
+              | otherwise -> Left $ outOfBoundsErr someVal branches
+            _ -> Left "Only 'Constr' constructor can be cased"
         _ -> Left $ display uni <> " isn't supported in 'case'"
       where
         !len = Vector.length branches
     {-# INLINE caseBuiltin #-}
 
+instance LetBuiltin DefaultUni where
+  letBuiltin _someVal@(Some (ValueOf uni x)) =
+    case uni of
+      DefaultUniList ty      -> Right $ someValueOf ty <$> x
+      DefaultUniPair tyL tyR -> Right [someValueOf tyL $ fst x, someValueOf tyR $ snd x]
+      _                      -> Left $ display uni <> "no"
+
 {- Note [Stable encoding of tags]
 'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the
 universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni'

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs

@@ -149,19 +149,19 @@ faster than the used in production. Also see Note [noinline for saving on
 ticks]. -}
 defaultCekParametersA :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersA =
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantA cekCostModelVariantA
 
 -- See Note [No inlining for MachineParameters]
 defaultCekParametersB :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersB =
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantB cekCostModelVariantB
 
 -- See Note [No inlining for MachineParameters]
 defaultCekParametersC :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersC =
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantC cekCostModelVariantC
 
 {- Note [noinline for saving on ticks]
@@ -360,6 +360,6 @@ unitCostBuiltinCostModel = BuiltinCostModelBase
 unitCekParameters :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 unitCekParameters =
     -- See Note [noinline for saving on ticks].
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters def $
             CostModel unitCekMachineCosts unitCostBuiltinCostModel

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs

@@ -55,6 +55,7 @@ The @val@ type will be 'CekValue' when we're using this with the CEK machine.
 data MachineParameters machineCosts fun val =
     MachineParameters {
       machineCaserBuiltin      :: CaserBuiltin (UniOf val)
+    , machineLeterBuiltin      :: LeterBuiltin (UniOf val)
     , machineVariantParameters :: MachineVariantParameters machineCosts fun val
     }
     deriving stock Generic
@@ -67,8 +68,8 @@ instance (NoThunks machinecosts, Bounded fun, Enum fun) => NoThunks (MachineVari
       allNoThunks [ noThunks ctx costs, noThunks ctx runtime ]
 
 instance (NoThunks machinecosts, Bounded fun, Enum fun) => NoThunks (MachineParameters machinecosts fun val) where
-  wNoThunks ctx (MachineParameters caser varPars) =
-      allNoThunks [ noThunks ctx caser, noThunks ctx varPars ]
+  wNoThunks ctx (MachineParameters caser leter varPars) =
+      allNoThunks [ noThunks ctx caser, noThunks ctx leter, noThunks ctx varPars ]
 
 {- Note [The CostingPart constraint in mkMachineVariantParameters]
 Discharging the @CostingPart uni fun ~ builtincosts@ constraint in 'mkMachineParameters' causes GHC

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs

@@ -459,6 +459,7 @@ they don't actually take the context as an argument even at the source level.
 -- | Implicit parameter for the builtin runtime.
 type GivenCekRuntime uni fun ann = (?cekRuntime :: BuiltinsRuntime fun (CekValue uni fun ann))
 type GivenCekCaserBuiltin uni = (?cekCaserBuiltin :: CaserBuiltin uni)
+type GivenCekLeterBuiltin uni = (?cekLeterBuiltin :: LeterBuiltin uni)
 -- | Implicit parameter for the log emitter reference.
 type GivenCekEmitter uni fun s = (?cekEmitter :: CekEmitter uni fun s)
 -- | Implicit parameter for budget spender.
@@ -471,6 +472,7 @@ type GivenCekCosts = (?cekCosts :: CekMachineCosts)
 type GivenCekReqs uni fun ann s =
     ( GivenCekRuntime uni fun ann
     , GivenCekCaserBuiltin uni
+    , GivenCekLeterBuiltin uni
     , GivenCekEmitter uni fun s
     , GivenCekSpender uni fun s
     , GivenCekSlippage
@@ -713,8 +715,8 @@ data Context uni fun ann
     -- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
     | FrameCases !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
     -- ^ @(case _ C0 .. Cn)@
-    | FrameAwaitLetBinds !(CekValEnv uni fun ann) !(NTerm uni fun ann) ![NTerm uni fun ann] ![CekValue uni fun ann] !(Context uni fun ann)
-    | FrameAwaitLet ![CekValue uni fun ann] !(Context uni fun ann)
+    | FrameAwaitLetBinds !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 !(NTerm uni fun ann) ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
+    | FrameAwaitLet {-# UNPACK #-} !Word64 !(ArgStack uni fun ann) !(Context uni fun ann)
     | NoFrame
 
 deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
@@ -754,7 +756,7 @@ runCekM
     -> (forall s. GivenCekReqs uni fun ann s => CekM uni fun s (DischargeResult uni fun))
     -> CekReport cost NamedDeBruijn uni fun
 runCekM
-        (MachineParameters caser (MachineVariantParameters costs runtime))
+        (MachineParameters caser leter (MachineVariantParameters costs runtime))
         (ExBudgetMode getExBudgetInfo)
         (EmitterMode getEmitterMode)
         a = runST $ do
@@ -763,6 +765,7 @@ runCekM
     ctr <- newCounter (Proxy @CounterSize)
     let ?cekRuntime = runtime
         ?cekCaserBuiltin = caser
+        ?cekLeterBuiltin = leter
         ?cekEmitter = _cekEmitterInfoEmit
         ?cekBudgetSpender = _exBudgetModeSpender
         ?cekCosts = costs
@@ -851,7 +854,7 @@ enterComputeCek = computeCek
         --stepAndMaybeSpend BApply
         -- computeCek (FrameAwaitLetBinds env t bs ctx) env t
         case bs of
-          (t : rest) -> computeCek (FrameAwaitLetBinds env body rest [] ctx) env t
+          (t : rest) -> computeCek (FrameAwaitLetBinds env 0 body rest NilStack ctx) env t
           []         -> computeCek ctx env body
 
     {- | The returning phase of the CEK machine.
@@ -892,11 +895,16 @@ enterComputeCek = computeCek
         SpineLast arg      -> applyEvaluate ctx fun (VCon arg)
         SpineCons arg rest -> applyEvaluate (FrameAwaitFunConN rest ctx) fun (VCon arg)
     -- s , [_ V1 .. Vn] ◅ lam x (M,ρ)  ↦  s , [_ V2 .. Vn]; ρ [ x  ↦  V1 ] ▻ M
-    returnCek (FrameAwaitLet args ctx) l =
-      case l of
-        VLet names body env
-          | length names == length args -> computeCek ctx (foldr Env.cons env args) body
-        _               -> error "no"
+    returnCek (FrameAwaitLet cnt args ctx) l =
+      let
+        -- this can probably be done in FrameAwaitLetBinds for better performance.
+        go acc NilStack         = acc
+        go acc (ConsStack x xs) = Env.cons x (go acc xs)
+      in case l of
+           VLet names body env
+             | length names == fromIntegral cnt -> computeCek ctx (go env args) body
+             | otherwise -> error $ show (length names) <> " " <> show cnt
+           _               -> error "no"
 
     returnCek (FrameAwaitFunValueN args ctx) fun =
         case args of
@@ -930,16 +938,20 @@ enterComputeCek = computeCek
         VCon val -> case unCaserBuiltin ?cekCaserBuiltin val cs of
             Left err          -> throwErrorDischarged (OperationalError $ CekCaseBuiltinError err) e
             Right (HeadOnly fX) -> computeCek ctx env fX
-            Right (HeadSpine f xs) -> computeCek (FrameAwaitFunConN xs ctx) env f
+            Right (HeadSpine f xs) ->
+              let
+                -- we reverse and reverse again, this is bad, just POC
+                go acc (SpineLast x)      = (ConsStack (VCon x) acc, 1)
+                go acc (SpineCons x rest) = (+1) <$> go (ConsStack (VCon x) acc) rest
+
+                (xs', cnt) = go NilStack xs
+              in computeCek (FrameAwaitLet cnt xs' ctx) env f
         _ -> throwErrorDischarged (StructuralError NonConstrScrutinizedMachineError) e
-    -- returnCek (FrameAwaitLetTerm env bs ctx) e =
-    --   case bs of
-    --     (next : todo) -> computeCek (FrameAwaitLetBinds env e todo [] ctx) env next
-        -- [] -> returnCek ctx e -- no bindings
-    returnCek (FrameAwaitLetBinds env l todo done ctx) e =
+    returnCek (FrameAwaitLetBinds env cnt l todo done ctx) e =
       case todo of
-        (next : todo') -> computeCek (FrameAwaitLetBinds env l todo' (e : done) ctx) env next
-        []             -> computeCek (FrameAwaitLet (e : done) ctx) env l
+        (next : todo') ->
+          computeCek (FrameAwaitLetBinds env (cnt + 1) l todo' (ConsStack e done) ctx) env next
+        []             -> computeCek (FrameAwaitLet (cnt + 1) (ConsStack e done) ctx) env l
 
     -- | @force@ a term and proceed.
     -- If v is a delay then compute the body of v;
@@ -996,6 +1008,15 @@ enterComputeCek = computeCek
                 evalBuiltinApp ctx fun term' $ f arg
             _ ->
                 throwErrorWithCause (StructuralError UnexpectedBuiltinTermArgumentMachineError) term'
+    applyEvaluate !ctx (VLet names body env) (VCon v) =
+      case unLeterBuiltin ?cekLeterBuiltin v of
+        Right binds
+          | length binds == length names ->
+            computeCek ctx (foldl (flip (Env.cons . VCon)) env binds) body
+          | otherwise -> error "aa"
+        Left e -> error $ show e
+
+      -- computeCek (FrameAwaitLet cnt xs' ctx) env body
     applyEvaluate !_ val _ =
         throwErrorDischarged (StructuralError NonFunctionalApplicationMachineError) val
 

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs

@@ -347,7 +347,7 @@ mkCekTrans
     -> Slippage
     -> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
 mkCekTrans
-        (MachineParameters caser (MachineVariantParameters costs runtime))
+        (MachineParameters caser leter (MachineVariantParameters costs runtime))
         (ExBudgetMode getExBudgetInfo)
         (EmitterMode getEmitterMode)
         slippage = do
@@ -356,6 +356,7 @@ mkCekTrans
     ctr <- newCounter (Proxy @CounterSize)
     let ?cekRuntime = runtime
         ?cekCaserBuiltin = caser
+        ?cekLeterBuiltin = leter
         ?cekEmitter = _cekEmitterInfoEmit
         ?cekBudgetSpender = _exBudgetModeSpender
         ?cekCosts = costs