From ca9405f858159e4e7f4a6a7078d7ea96a12d1270 Mon Sep 17 00:00:00 2001
From: Jacco <4022046+basetunnel@users.noreply.github.com>
Date: Fri, 14 Nov 2025 16:11:40 +0100
Subject: [PATCH 1/2] Add missing empty list in CEK compute rule of constr

---
 doc/plutus-core-spec/untyped-cek-machine.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/plutus-core-spec/untyped-cek-machine.tex b/doc/plutus-core-spec/untyped-cek-machine.tex
index 3f141381205..03c7f4ac9cc 100644
--- a/doc/plutus-core-spec/untyped-cek-machine.tex
+++ b/doc/plutus-core-spec/untyped-cek-machine.tex
@@ -126,7 +126,7 @@ \section{The CEK machine}
  s;\rho & \compute \delay{M}                         &~\mapsto~& s\return \VDelay{M}{\rho}\\
  s;\rho & \compute \force{M}                         &~\mapsto~& \inForceFrame{} \cons s;\rho \compute M \\
  s;\rho & \compute \appU{M}{N}                       &~\mapsto~& \inAppLeftFrame{(N,\rho)} \cons s ;\rho \compute M\\
- s;\rho & \compute \constr{i}{M \cons \repetition{M}} &~\mapsto~& \inConstrFrame{i}{}{(\repetition{M},\rho)} \cons s ;\rho \compute M\\
+  s;\rho & \compute \constr{i}{M \cons \repetition{M}} &~\mapsto~& \inConstrFrame{i}{[]}{(\repetition{M},\rho)} \cons s ;\rho \compute M\\
  s;\rho & \compute \constr{i}{[]} &~\mapsto~&  s \return \VConstr{i}{[]}\\
  s;\rho & \compute \kase{N}{\repetition{M}} &~\mapsto~&  \inCaseFrame{(\repetition{M},\rho)} \cons s ;\rho \compute N\\
 % No nullary builtins (yet)

From 37469c596b7f29892e2847c90d7c073b84202e9c Mon Sep 17 00:00:00 2001
From: Jacco <4022046+basetunnel@users.noreply.github.com>
Date: Fri, 14 Nov 2025 16:12:28 +0100
Subject: [PATCH 2/2] Reverse order of application frames in CEK return rule of
 case

---
 doc/plutus-core-spec/untyped-cek-machine.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/plutus-core-spec/untyped-cek-machine.tex b/doc/plutus-core-spec/untyped-cek-machine.tex
index 03c7f4ac9cc..8cdf84cc84f 100644
--- a/doc/plutus-core-spec/untyped-cek-machine.tex
+++ b/doc/plutus-core-spec/untyped-cek-machine.tex
@@ -155,7 +155,7 @@ \section{The CEK machine}
 \inConstrFrame{i}{\repetition{V}}{([], \rho)} \cons s & \return V   &~\mapsto~&
                          s \return \VConstr{i}{\repetition{V} \cons V} \\
 \inCaseFrame{(M_1 \ldots M_n, \rho)} \cons s & \return \VConstr{i}{V_1 \ldots V_m}   &~\mapsto~&
-                         \inAppLeftFrame{V_m} \cons \cdots \cons \inAppLeftFrame{V_1} \cons s ;\rho \compute M_{i+1} \enskip \text{if $0 \leq i \leq n-1$}
+                         \inAppLeftFrame{V_1} \cons \cdots \cons \inAppLeftFrame{V_m} \cons s ;\rho \compute M_{i+1} \enskip \text{if $0 \leq i \leq n-1$}
 \end{alignat*}
 \end{minipage}
     \caption{CEK machine transitions for Plutus Core}