spec: update ECALL signature

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(

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", ["cast", "rv1", "DWordWL"]]
 multiplicity = "ECALL"