From 9683a7d8c07d169677479f28263fde026079056d Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 27 Jan 2026 14:33:31 +0100
Subject: [PATCH 1/2] spec: update `ECALL` signature

---
 spec/decode.typ   | 9 +++------
 spec/src/cpu.toml | 4 +---
 2 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/spec/decode.typ b/spec/decode.typ
index d8332e033..218cb84a3 100644
--- a/spec/decode.typ
+++ b/spec/decode.typ
@@ -146,7 +146,7 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is
   ([`SH       rs1, rs2, imm`], [`STORE`], [], [], [`mem_2B`], []),
   ([`SB       rs1, rs2, imm`], [`STORE`], [], [], [], []),
   // ECALL/EBREAK
-  ([`ECALL`], [`ECALL`], [], [], [$#`rs1` := #`x17`$, $#`rs2` := #`x10`$, $#`rd` := #`x10`$], [#ref_note(<note-ecall>)]),
+  ([`ECALL`], [`ECALL`], [], [], [$#`rs1` := #`x17`$], [#ref_note(<note-ecall>)]),
   ([`EBREAK`], [`EBREAK`], [], [], [], []),
   // FENCE
   ([`FENCE`], [`ADD`], [], [], [], [#ref_note(<note-fence>)]),
@@ -203,11 +203,8 @@ We note the following about the above decoding table:
     referenceable_note(
       "note-ecall",
       [`ECALL`:
-      "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]]
-      As such,
-      - syscall number in A7 (= register `x17`)
-      - first syscall argument in A0 (= register `x10`)
-      - syscall output in A0 (= register `x10`)]
+      "On RISC-V a system call has its own instruction: `ECALL`. [...] A7 [= register `x17`] contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]]
+      ]
     )
   ),
   enum.item(
diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml
index 49a78ee15..480b92613 100644
--- a/spec/src/cpu.toml
+++ b/spec/src/cpu.toml
@@ -705,12 +705,10 @@ desc = "We treat `EBREAK` as an unprovable trap"
 poly = ["not", "EBREAK"]
 ref = "cpu:c:ebreak_traps"
 
-# TODO: no types available, so no casting yet
 [[constraints.sys]]
 kind = "interaction"
 tag = "ECALL"
-input = ["rv1", "pc", "timestamp", "rv2"]
-output = "rvd"
+input = ["timestamp", "rv1"]
 multiplicity = "ECALL"
 
 

From 708447ff28a04a19dd16d57a23765e5e91de4855 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 27 Jan 2026 14:49:11 +0100
Subject: [PATCH 2/2] spec: CPU/ECALL: cast rv1 to DWordWL

---
 spec/src/cpu.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml
index 480b92613..d8609e935 100644
--- a/spec/src/cpu.toml
+++ b/spec/src/cpu.toml
@@ -708,7 +708,7 @@ ref = "cpu:c:ebreak_traps"
 [[constraints.sys]]
 kind = "interaction"
 tag = "ECALL"
-input = ["timestamp", "rv1"]
+input = ["timestamp", ["cast", "rv1", "DWordWL"]]
 multiplicity = "ECALL"