From 12d244065f508107ba4b9f3879253811855181d7 Mon Sep 17 00:00:00 2001 From: Emiel Sebastiaan <14069142+emielsebastiaan@users.noreply.github.com> Date: Fri, 22 Nov 2024 08:33:29 +0100 Subject: [PATCH 1/6] Allow 8 octets input signed extension function (64bit) Allow up to 8 input octets for the signed extension function as a consequence of the change to a 64bit architecture. Direct evidence of this requirement in instructions 140 & 141. --- text/pvm.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/pvm.tex b/text/pvm.tex index eb838e5..890486c 100644 --- a/text/pvm.tex +++ b/text/pvm.tex @@ -175,7 +175,7 @@ \subsection{Single-Step State Transition} Immediate arguments are encoded in little-endian format with the most-significant bit being the sign bit. They may be compactly encoded by eliding more significant octets. Elided octets are assumed to be zero if the \textsc{msb} of the value is zero, and 255 otherwise. This allows for compact representation of both positive and negative encoded values. We thus define the signed extension function operating on an input of $n$ octets as $\sext_n$: \begin{align}\label{eq:signedextension} - \sext_{n \in \{0, 1, 2, 3, 4\}}\colon\left\{\begin{aligned} + \sext_{n \in \{0, 1, 2, 3, 4, 5, 6, 7, 8\}}\colon\left\{\begin{aligned} \N_{2^{8n}} &\to \N_R\\ x &\mapsto x + \ffrac{x}{2^{8n-1}}(2^{64}-2^{8n}) \end{aligned}\right. From b8eb72fc8e6064ed23a9990ecd30bd439b370c94 Mon Sep 17 00:00:00 2001 From: Emiel Sebastiaan <14069142+emielsebastiaan@users.noreply.github.com> Date: Fri, 22 Nov 2024 14:19:10 +0100 Subject: [PATCH 2/6] GP-0.5.0-eq:A.17 (32bit -> 64bit) Allow `L_Y` to be up to (value) 8 and thus allow the `signed extension`-function up to 8 bytes of input to determine `V_Y`. --- text/pvm.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/pvm.tex b/text/pvm.tex index 890486c..e56da71 100644 --- a/text/pvm.tex +++ b/text/pvm.tex @@ -264,7 +264,7 @@ \subsubsection{Instructions with Arguments of Two Immediates} \begin{aligned} \using l_X &= \min(4, \instructions_{\imath+1} \bmod 8) \,,\quad& \immed_X &\equiv \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \\ - \using l_Y &= \min(4, \max(0, \ell - l_X - 1)) \,,\quad& + \using l_Y &= \min(8, \max(0, \ell - l_X - 1)) \,,\quad& \immed_Y &\equiv \sext_{l_Y}(\de_{l_Y}(\instructions_{\imath+2+l_X\dots+l_Y})) \end{aligned} \end{equation} From 8083e851104fdc6ef4d637a2b4768720a1eef6c6 Mon Sep 17 00:00:00 2001 From: Emiel Sebastiaan <14069142+emielsebastiaan@users.noreply.github.com> Date: Fri, 22 Nov 2024 14:27:23 +0100 Subject: [PATCH 3/6] GP-0.5.0-eq:A.20 (32bit -> 64bit) In GP-0.5.0-eq:A.20: Allow `L_Y` to be up to (value) 8 and thus allow the `signed extension`-function up to 8 bytes of input to determine `V_Y`. And add mod2^32 to instruction 72. --- text/pvm.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/pvm.tex b/text/pvm.tex index e56da71..4cd2681 100644 --- a/text/pvm.tex +++ b/text/pvm.tex @@ -341,7 +341,7 @@ \subsubsection{Instructions with Arguments of One Register \& Two Immediates} \reg'_A \equiv \reg'_{r_A} \\ \using l_X &= \min(4, \ffrac{\instructions_{\imath+1}}{16} \bmod 8) \,,\quad& \immed_X &= \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \\ - \using l_Y &= \min(4, \max(0, \ell - l_X - 1)) \,,\quad& + \using l_Y &= \min(8, \max(0, \ell - l_X - 1)) \,,\quad& \immed_Y &= \sext_{l_Y}(\de_{l_Y}(\instructions_{\imath+2+l_X\dots+l_Y})) \end{aligned} \end{equation} @@ -354,7 +354,7 @@ \subsubsection{Instructions with Arguments of One Register \& Two Immediates} \endhead 70&\token{store\_imm\_ind\_u8}&0&$\memwr_{\reg_A + \immed_X} = \immed_Y \bmod 2^8$\\ \mrule 71&\token{store\_imm\_ind\_u16}&0&$\memwr_{\reg_A + \immed_X \dots+ 2} = \se_2(\immed_Y \bmod 2^{16})$\\ \mrule - 72&\token{store\_imm\_ind\_u32}&0&$\memwr_{\reg_A + \immed_X \dots+ 4} = \se_4(\immed_Y)$\\ \mrule + 72&\token{store\_imm\_ind\_u32}&0&$\memwr_{\reg_A + \immed_X \dots+ 4} = \se_4(\immed_Y \bmod 2^{32})$\\ \mrule 73&\token{store\_imm\_ind\_u64}&0&$\memwr_{\reg_A + \immed_X \dots+ 8} = \se_8(\immed_Y)$\\ \bottomrule \end{longtable} From eeb0019e1247530e18581f5286fab00ce352911a Mon Sep 17 00:00:00 2001 From: Emiel Sebastiaan <14069142+emielsebastiaan@users.noreply.github.com> Date: Fri, 22 Nov 2024 14:32:10 +0100 Subject: [PATCH 4/6] GP-0.5.0-eq:A.21 (32bit -> 64bit) In GP-0.5.0-eq:A.21: Allow `L_X` to be up to (value) 8 and thus allow the `signed extension`-function up to 8 bytes of input to determine `V_X`. --- text/pvm.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/pvm.tex b/text/pvm.tex index 4cd2681..50fe295 100644 --- a/text/pvm.tex +++ b/text/pvm.tex @@ -365,7 +365,7 @@ \subsubsection{Instructions with Arguments of One Register, One Immediate and On \using r_A &= \min(12, \instructions_{\imath+1} \bmod 16) \,,\quad& \reg_A &\equiv \reg_{r_A} \,,\quad \reg'_A \equiv \reg'_{r_A} \\ - \using l_X &= \min(4, \ffrac{\instructions_{\imath+1}}{16} \bmod 8) \,,\quad& + \using l_X &= \min(8, \ffrac{\instructions_{\imath+1}}{16} \bmod 8) \,,\quad& \immed_X &= \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \\ \using l_Y &= \min(4, \max(0, \ell - l_X - 1)) \,,\quad& \immed_Y &= \imath + \signfunc{l_Y}(\de_{l_Y}(\instructions_{\imath+2+l_X\dots+l_Y})) From d6f3937539da2d315e6804861ab85e35dfbb05cb Mon Sep 17 00:00:00 2001 From: Emiel Sebastiaan <14069142+emielsebastiaan@users.noreply.github.com> Date: Fri, 22 Nov 2024 14:45:31 +0100 Subject: [PATCH 5/6] GP-0.5.0-eq:A.23 (32bit -> 64bit) In GP-0.5.0-eq:A.23: Allow `L_X` to be up to (value) 8 and thus allow the `signed extension`-function up to 8 bytes of input to determine `V_X`. Required for instructions: 126, 127, 132, 133, 137, 138, 139, 140, 141, 142, 144, 145, 146, 147. --- text/pvm.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/pvm.tex b/text/pvm.tex index 50fe295..9911522 100644 --- a/text/pvm.tex +++ b/text/pvm.tex @@ -431,7 +431,7 @@ \subsubsection{Instructions with Arguments of Two Registers \& One Immediate} \using r_B &= \min(12, \ffrac{\instructions_{\imath+1}}{16}) \,,\quad& \reg_B &\equiv \reg_{r_B} \,,\quad \reg'_B \equiv \reg'_{r_B} \\ - \using l_X &= \min(4, \max(0, \ell - 1)) \,,\quad& + \using l_X &= \min(8, \max(0, \ell - 1)) \,,\quad& \immed_X &\equiv \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \end{aligned} \end{equation} From ce60bb405a3e379bb44b6079f8c45b551ad373ec Mon Sep 17 00:00:00 2001 From: Emiel Sebastiaan <14069142+emielsebastiaan@users.noreply.github.com> Date: Mon, 25 Nov 2024 13:46:56 +0100 Subject: [PATCH 6/6] Corrections pvm.tex Corrections --- text/pvm.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/text/pvm.tex b/text/pvm.tex index 9911522..c84bc35 100644 --- a/text/pvm.tex +++ b/text/pvm.tex @@ -175,7 +175,7 @@ \subsection{Single-Step State Transition} Immediate arguments are encoded in little-endian format with the most-significant bit being the sign bit. They may be compactly encoded by eliding more significant octets. Elided octets are assumed to be zero if the \textsc{msb} of the value is zero, and 255 otherwise. This allows for compact representation of both positive and negative encoded values. We thus define the signed extension function operating on an input of $n$ octets as $\sext_n$: \begin{align}\label{eq:signedextension} - \sext_{n \in \{0, 1, 2, 3, 4, 5, 6, 7, 8\}}\colon\left\{\begin{aligned} + \sext_{n \in \{0, 1, 2, 3, 4, 8\}}\colon\left\{\begin{aligned} \N_{2^{8n}} &\to \N_R\\ x &\mapsto x + \ffrac{x}{2^{8n-1}}(2^{64}-2^{8n}) \end{aligned}\right. @@ -264,7 +264,7 @@ \subsubsection{Instructions with Arguments of Two Immediates} \begin{aligned} \using l_X &= \min(4, \instructions_{\imath+1} \bmod 8) \,,\quad& \immed_X &\equiv \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \\ - \using l_Y &= \min(8, \max(0, \ell - l_X - 1)) \,,\quad& + \using l_Y &= \min(4, \max(0, \ell - l_X - 1)) \,,\quad& \immed_Y &\equiv \sext_{l_Y}(\de_{l_Y}(\instructions_{\imath+2+l_X\dots+l_Y})) \end{aligned} \end{equation} @@ -341,7 +341,7 @@ \subsubsection{Instructions with Arguments of One Register \& Two Immediates} \reg'_A \equiv \reg'_{r_A} \\ \using l_X &= \min(4, \ffrac{\instructions_{\imath+1}}{16} \bmod 8) \,,\quad& \immed_X &= \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \\ - \using l_Y &= \min(8, \max(0, \ell - l_X - 1)) \,,\quad& + \using l_Y &= \min(4, \max(0, \ell - l_X - 1)) \,,\quad& \immed_Y &= \sext_{l_Y}(\de_{l_Y}(\instructions_{\imath+2+l_X\dots+l_Y})) \end{aligned} \end{equation} @@ -365,7 +365,7 @@ \subsubsection{Instructions with Arguments of One Register, One Immediate and On \using r_A &= \min(12, \instructions_{\imath+1} \bmod 16) \,,\quad& \reg_A &\equiv \reg_{r_A} \,,\quad \reg'_A \equiv \reg'_{r_A} \\ - \using l_X &= \min(8, \ffrac{\instructions_{\imath+1}}{16} \bmod 8) \,,\quad& + \using l_X &= \min(4, \ffrac{\instructions_{\imath+1}}{16} \bmod 8) \,,\quad& \immed_X &= \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \\ \using l_Y &= \min(4, \max(0, \ell - l_X - 1)) \,,\quad& \immed_Y &= \imath + \signfunc{l_Y}(\de_{l_Y}(\instructions_{\imath+2+l_X\dots+l_Y})) @@ -431,7 +431,7 @@ \subsubsection{Instructions with Arguments of Two Registers \& One Immediate} \using r_B &= \min(12, \ffrac{\instructions_{\imath+1}}{16}) \,,\quad& \reg_B &\equiv \reg_{r_B} \,,\quad \reg'_B \equiv \reg'_{r_B} \\ - \using l_X &= \min(8, \max(0, \ell - 1)) \,,\quad& + \using l_X &= \min(4, \max(0, \ell - 1)) \,,\quad& \immed_X &\equiv \sext_{l_X}(\de_{l_X}(\instructions_{\imath+2\dots+l_X})) \end{aligned} \end{equation}