Fix the steppable machine, add the 'fixLoop' test

Author: effectfully

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

@@ -63,6 +63,7 @@ data MachineError fun
     | NonConstrScrutinized
     | MissingCaseBranch Word64
     | NonLambdaFixedMachineError
+    | FixLoopMachineError
     deriving stock (Show, Eq, Functor, Generic)
     deriving anyclass (NFData)
 
@@ -136,3 +137,5 @@ instance (HasPrettyDefaults config ~ 'True, Pretty fun) =>
         "Case expression missing the branch required by the scrutinee tag:" <+> pretty i
     prettyBy _      NonLambdaFixedMachineError =
         "Attempted to take the fixed-point of a non-lambda term"
+    prettyBy _      FixLoopMachineError =
+        "Fix entered infinite recursion"

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

@@ -511,6 +511,7 @@ dischargeCekValEnv valEnv = go 0
                -- var is in the env, discharge its value
                (\case
                    VBlackHole recName recLamCnt ->
+                       -- TODO: is this right?
                        Var () (NamedDeBruijn recName . coerce $ lamCnt - recLamCnt)
                    val -> dischargeCekValue val)
                -- index relative to (as seen from the point of view of) the environment
@@ -541,7 +542,8 @@ dischargeCekValue = \case
         stack2list = go []
         go acc EmptyStack           = acc
         go acc (ConsStack arg rest) = go (arg : acc) rest
-    VBlackHole _ _ -> error "can't happen"
+    -- TODO: is this right?
+    VBlackHole recName _ -> Var () (NamedDeBruijn recName 0)
 
 instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
     prettyBy cfg = prettyBy cfg . dischargeCekValue
@@ -772,6 +774,7 @@ enterComputeCek = computeCek
                 let env' = Env.contUpdateZero (\_ -> bodyV') env (Env.length env - recIx)
                     bodyV' = VLamAbs nameArg bodyLam env'
                 returnCek ctx bodyV'
+            VBlackHole{} -> throwingDischarged _MachineError FixLoopMachineError bodyV
             _ -> throwingDischarged _MachineError NonLambdaFixedMachineError bodyV
 
     -- | Evaluate a 'HeadSpine' by pushing the arguments (if any) onto the stack and proceeding with

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

@@ -59,6 +59,7 @@ import Control.Monad
 import Control.Monad.Primitive
 import Data.Proxy
 import Data.RandomAccessList.Class qualified as Env
+import Data.RandomAccessList.SkewBinary qualified as Env
 import Data.Semigroup (stimes)
 import Data.Text (Text)
 import Data.Vector qualified as V
@@ -101,7 +102,7 @@ data Context uni fun ann
     | FrameForce ann !(Context uni fun ann)                                               -- ^ @(force _)@
     | FrameConstr ann !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
     | FrameCases ann !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
-    | FrameFix ann !(Context uni fun ann)
+    | FrameFix ann !Word64 !(Context uni fun ann)
     | NoFrame
 
 deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
@@ -165,9 +166,10 @@ computeCek !ctx !env (Constr ann i es) = do
 computeCek !ctx !env (Case ann scrut cs) = do
     stepAndMaybeSpend BCase
     pure $ Computing (FrameCases ann env cs ctx) env scrut
-computeCek !ctx !env (Fix ann _ bodyOuter) = do
+computeCek !ctx !env (Fix ann rec body) = do
     stepAndMaybeSpend BFix
-    pure $ Computing (FrameFix ann ctx) env bodyOuter
+    let !len' = Env.length env + 1
+    pure $ Computing (FrameFix ann len' ctx) (Env.cons (VBlackHole (ndbnString rec) len') env) body
 -- s ; ρ ▻ error A  ↦  <> A
 computeCek !_ !_ (Error _) =
     throwing_ _EvaluationFailure
@@ -216,13 +218,13 @@ returnCek (FrameCases ann env cs ctx) e = case e of
               in computeCek ctx' env t
         Nothing -> throwingDischarged _MachineError (MissingCaseBranch i) e
     _ -> throwingDischarged _MachineError NonConstrScrutinized e
-returnCek (FrameFix _ ctx) bodyOuter =
-    case bodyOuter of
-        VLamAbs nameArg bodyInner env ->
-            let env' = Env.cons bodyOuter' env
-                bodyOuter' = VLamAbs nameArg bodyInner env'
-            in pure $ Returning ctx bodyOuter'
-        _ -> throwingDischarged _MachineError NonLambdaFixedMachineError bodyOuter
+returnCek (FrameFix _ recIx ctx) bodyV =
+    case bodyV of
+        VLamAbs nameArg bodyLam env -> do
+            let env' = Env.contUpdateZero (\_ -> bodyV') env (Env.length env - recIx)
+                bodyV' = VLamAbs nameArg bodyLam env'
+            pure $ Returning ctx bodyV'
+        _ -> throwingDischarged _MachineError NonLambdaFixedMachineError bodyV
 
 -- | @force@ a term and proceed.
 -- If v is a delay then compute the body of v;
@@ -394,7 +396,7 @@ contextAnn = \case
     FrameForce ann _            -> pure ann
     FrameConstr ann _ _ _ _ _   -> pure ann
     FrameCases ann _ _ _        -> pure ann
-    FrameFix ann _              -> pure ann
+    FrameFix ann _ _            -> pure ann
     NoFrame                     -> empty
 
 lenContext :: Context uni fun ann -> Word
@@ -408,7 +410,7 @@ lenContext = go 0
               FrameForce _ k            -> go (n+1) k
               FrameConstr _ _ _ _ _ k   -> go (n+1) k
               FrameCases _ _ _ k        -> go (n+1) k
-              FrameFix _ k              -> go (n+1) k
+              FrameFix _ _ k            -> go (n+1) k
               NoFrame                   -> 0
 
 

plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Definition.hs

@@ -33,6 +33,7 @@ import PlutusCore.Compiler.Erase (eraseTerm)
 import PlutusCore.Data
 import PlutusCore.Default
 import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
+import PlutusCore.Evaluation.Machine.Exception
 import PlutusCore.Evaluation.Machine.MachineParameters
 import PlutusCore.Examples.Builtins
 import PlutusCore.Examples.Data.Data
@@ -524,6 +525,20 @@ test_fixId =
                     ]
         typecheckAndEvalToOutOfEx fixId
 
+test_fixLoop :: TestTree
+test_fixLoop =
+    testCase "a 'fix' loop finishes" $ do
+        let fixLoop :: Term TyName Name DefaultUni DefaultFun ()
+            fixLoop = runQuote $ do
+                rec <- freshName "rec"
+                pure $ Fix () rec (TyFun () integer integer) $ Var () rec
+            evalRestricting params = fst . runCekNoEmit params restrictingLarge
+        case typecheckAnd def evalRestricting defaultBuiltinCostModelForTesting fixLoop of
+                Right (Left (ErrorWithCause (StructuralEvaluationError FixLoopMachineError) _)) ->
+                    pure ()
+                err ->
+                    assertFailure $ "Expected a 'FixLoopMachineError' but got: " ++ displayPlc err
+
 -- | If the first char is an opening paren and the last chat is a closing paren, then remove them.
 -- This is useful for rendering a term-as-a-test-name in CLI, since currently we wrap readably
 -- pretty-printed terms in parens (which is to be fixed).
@@ -1212,6 +1227,7 @@ test_definition =
 #endif
         , test_SerialiseDataImpossible
         , test_fixId
+        , test_fixLoop
         , runTestNestedHere
             [ test_Integer
             , test_String

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/Fib/1.uplc.golden

@@ -8,9 +8,10 @@
 | BStep BBuiltin causes ({cpu: 32000 | mem: 200})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp LessThanEqualsInteger causes ({cpu: 43837 | mem: 1})
 | BBuiltinApp IfThenElse causes ({cpu: 76049 | mem: 1})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 583986
-| mem: 3002})
+| budget: ({cpu: 599986
+| mem: 3102})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/Fib/2.uplc.golden

@@ -8,11 +8,12 @@
 | BStep BBuiltin causes ({cpu: 144000 | mem: 900})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp AddInteger causes ({cpu: 101208 | mem: 2})
 | BBuiltinApp SubtractInteger causes ({cpu: 202416 | mem: 4})
 | BBuiltinApp LessThanEqualsInteger causes ({cpu: 131511 | mem: 3})
 | BBuiltinApp IfThenElse causes ({cpu: 228147 | mem: 3})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 2215382
-| mem: 9812})
+| budget: ({cpu: 2231382
+| mem: 9912})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/Fib/3.uplc.golden

@@ -8,11 +8,12 @@
 | BStep BBuiltin causes ({cpu: 256000 | mem: 1600})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp AddInteger causes ({cpu: 202416 | mem: 4})
 | BBuiltinApp SubtractInteger causes ({cpu: 404832 | mem: 8})
 | BBuiltinApp LessThanEqualsInteger causes ({cpu: 219185 | mem: 5})
 | BBuiltinApp IfThenElse causes ({cpu: 380245 | mem: 5})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 3846778
-| mem: 16622})
+| budget: ({cpu: 3862778
+| mem: 16722})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IdNat/0.uplc.golden

@@ -51,7 +51,8 @@
 | BStep BBuiltin causes ({cpu: 0 | mem: 0})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 5168100
-| mem: 32400})
+| budget: ({cpu: 5184100
+| mem: 32500})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IdNat/3.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 48000 | mem: 300})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp Id causes ({cpu: 0 | mem: 0})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 5312100
-| mem: 33300})
+| budget: ({cpu: 5328100
+| mem: 33400})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IdNat/6.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 96000 | mem: 600})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp Id causes ({cpu: 0 | mem: 0})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 5456100
-| mem: 34200})
+| budget: ({cpu: 5472100
+| mem: 34300})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IdNat/9.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 144000 | mem: 900})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp Id causes ({cpu: 0 | mem: 0})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 5600100
-| mem: 35100})
+| budget: ({cpu: 5616100
+| mem: 35200})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IfThenElse/0.uplc.golden

@@ -51,7 +51,8 @@
 | BStep BBuiltin causes ({cpu: 0 | mem: 0})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 5168100
-| mem: 32400})
+| budget: ({cpu: 5184100
+| mem: 32500})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IfThenElse/1.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 16000 | mem: 100})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 32000 | mem: 200})
 | BBuiltinApp IfThenElse causes ({cpu: 76049 | mem: 1})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 5740149
-| mem: 35501})
+| budget: ({cpu: 5772149
+| mem: 35701})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IfThenElse/2.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 32000 | mem: 200})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 32000 | mem: 200})
 | BBuiltinApp IfThenElse causes ({cpu: 152098 | mem: 2})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 5976198
-| mem: 36502})
+| budget: ({cpu: 6008198
+| mem: 36702})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IfThenElse/3.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 48000 | mem: 300})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 32000 | mem: 200})
 | BBuiltinApp IfThenElse causes ({cpu: 228147 | mem: 3})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 6212247
-| mem: 37503})
+| budget: ({cpu: 6244247
+| mem: 37703})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IfThenElse/4.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 64000 | mem: 400})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 32000 | mem: 200})
 | BBuiltinApp IfThenElse causes ({cpu: 304196 | mem: 4})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 6448296
-| mem: 38504})
+| budget: ({cpu: 6480296
+| mem: 38704})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Budget/IfThenElse/5.uplc.golden

@@ -51,8 +51,9 @@
 | BStep BBuiltin causes ({cpu: 80000 | mem: 500})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 32000 | mem: 200})
 | BBuiltinApp IfThenElse causes ({cpu: 380245 | mem: 5})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 6684345
-| mem: 39505})
+| budget: ({cpu: 6716345
+| mem: 39705})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/NumberOfStepCounters.golden

@@ -1 +1 @@
-9
+10

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Tallying/Fib/1.uplc.golden

@@ -8,9 +8,10 @@
 | BStep BBuiltin causes ({cpu: 32000 | mem: 200})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp LessThanEqualsInteger causes ({cpu: 43837 | mem: 1})
 | BBuiltinApp IfThenElse causes ({cpu: 76049 | mem: 1})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 583986
-| mem: 3002})
+| budget: ({cpu: 599986
+| mem: 3102})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Tallying/Fib/2.uplc.golden

@@ -8,11 +8,12 @@
 | BStep BBuiltin causes ({cpu: 144000 | mem: 900})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp AddInteger causes ({cpu: 101208 | mem: 2})
 | BBuiltinApp SubtractInteger causes ({cpu: 202416 | mem: 4})
 | BBuiltinApp LessThanEqualsInteger causes ({cpu: 131511 | mem: 3})
 | BBuiltinApp IfThenElse causes ({cpu: 228147 | mem: 3})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 2215382
-| mem: 9812})
+| budget: ({cpu: 2231382
+| mem: 9912})
 }) )

plutus-core/untyped-plutus-core/test/Evaluation/Machines/Tallying/Fib/3.uplc.golden

@@ -8,11 +8,12 @@
 | BStep BBuiltin causes ({cpu: 256000 | mem: 1600})
 | BStep BConstr causes ({cpu: 0 | mem: 0})
 | BStep BCase causes ({cpu: 0 | mem: 0})
+| BStep BFix causes ({cpu: 16000 | mem: 100})
 | BBuiltinApp AddInteger causes ({cpu: 202416 | mem: 4})
 | BBuiltinApp SubtractInteger causes ({cpu: 404832 | mem: 8})
 | BBuiltinApp LessThanEqualsInteger causes ({cpu: 219185 | mem: 5})
 | BBuiltinApp IfThenElse causes ({cpu: 380245 | mem: 5})
 | BStartup causes ({cpu: 100 | mem: 100})})
-| budget: ({cpu: 3846778
-| mem: 16622})
+| budget: ({cpu: 3862778
+| mem: 16722})
 }) )