From 87cab0f744bb36550f0f91c84bac1d2382bee51e Mon Sep 17 00:00:00 2001
From: John Guibas <jtguibas@gmail.com>
Date: Wed, 20 Nov 2024 16:46:07 -0800
Subject: [PATCH] chore: rv32im deviations (#1807)

---
 book/SUMMARY.md                         |  2 +-
 book/developers/rv32im-deviations.md    | 27 +++++++++++++++++++++++++
 book/developers/rv32im-specification.md |  8 --------
 3 files changed, 28 insertions(+), 9 deletions(-)
 create mode 100644 book/developers/rv32im-deviations.md
 delete mode 100644 book/developers/rv32im-specification.md

diff --git a/book/SUMMARY.md b/book/SUMMARY.md
index 55ec23f628..4bde9eef98 100644
--- a/book/SUMMARY.md
+++ b/book/SUMMARY.md
@@ -72,6 +72,6 @@
 
 - [Usage in CI](./developers/usage-in-ci.md)
 
-- [RV32IM Specification](./developers/rv32im-specification.md)
+- [RV32IM Deviations](./developers/rv32im-deviations.md)
 
 - [Building Circuit Artifacts](./developers/building-circuit-artifacts.md)
diff --git a/book/developers/rv32im-deviations.md b/book/developers/rv32im-deviations.md
new file mode 100644
index 0000000000..e28f294450
--- /dev/null
+++ b/book/developers/rv32im-deviations.md
@@ -0,0 +1,27 @@
+# RV32IM Deviations
+
+**SP1 does not conform exactly to the official RISC-V RV32IM specification.** Instead, it includes 
+several minor modifications tailored to make it more suitable for use in proving systems. These 
+deviations are outlined below:
+
+- Addresses `0x0` to `0x20` are reserved for registers. Writing to these addresses will modify
+  register state and cause divergent behavior from the RISC-V specification.
+- Memory access is only valid for addresses `0x20, 0x78000000`. Writing to any other addresses
+  will result in undefined behavior. The heap allocator is also constrained to these addresses.
+- Memory access must be "aligned". The alignment is automatically enforced by all programs compiled
+  through the official SP1 RISC-V toolchain.
+    - LW/SW memory access must be word aligned. 
+    - LH/LHU/SH memory access must be half-word aligned.
+    - LW/SW memory access must be word aligned.
+    - LH/LHU/SH memory access must be half-word aligned.
+- The ECALL instruction is used for system calls and precompiles. Only valid syscall IDs should be called, and only using the specific convention of loading the ID into register T0 and arguments into registers A0 and A1. If the arguments are addresses, they must be word-aligned. Failure to follow this convention can result in undefined behavior. Correct usages can be found in the `sp1_zkvm` and `sp1_lib` crates.
+
+## Security Considerations
+
+While the deviations from the RISC-V specification could theoretically be exploited to cause 
+divergent execution, such scenarios require a deliberately malicious program. The SP1 security 
+model assumes that programs are honestly compiled, as malicious bytecode could otherwise exploit 
+program execution and I/O.
+
+These security concerns regarding divergent execution have been reviewed and discussed with external
+security researchers, including rkm0959, Zellic, samczsun, and others.
\ No newline at end of file
diff --git a/book/developers/rv32im-specification.md b/book/developers/rv32im-specification.md
deleted file mode 100644
index 84e8aa7584..0000000000
--- a/book/developers/rv32im-specification.md
+++ /dev/null
@@ -1,8 +0,0 @@
-# RV32IM Specification
-
-SP1 implements the RISC-V RV32IM instruction set with some implementation details that make it more suitable for proving.
-
-- LW/SW memory access must be word aligned.
-- LH/LHU/SH memory access must be half-word aligned.
-- Memory access is only valid for addresses `0x20, 0x78000000`. Accessing addresses outside of this range will result in undefined behavior. The global heap allocator in `sp1_zkvm` will panic if memory exceeds this range.
-- The ECALL instruction is used for system calls and precompiles. Only valid syscall IDs should be called, and only using the specific convention of loading the ID into register T0 and arguments into registers A0 and A1. If the arguments are addresses, they must be word-aligned. Failure to follow this convention can result in undefined behavior. Correct usages can be found in the `sp1_zkvm` and `sp1_lib` crates.