execute(CJALR)

[fvogels]

function clause execute(CJALR(cd, cs, imm)) = {
  // [...]
  let imm = sail_zero_extend(imm, integer_size);
  let c' = updatePCPerm({c with cap_cursor = c.cap_cursor + imm});
  // [...]
}

imm gets zero-extended, but shouldn't this be sign-extended?
From the corresponding CHERI RISC-V Sail code:

function clause execute(CJALR(imm, cs1, cd)) = {
  let cs1_val = C(cs1);
  let off : xlenbits = sign_extend(imm);    // <--
  let newPC = [cs1_val.address + off with 0 = bitzero]; /* clear bit zero as for RISCV JALR */
  // [...]

Also note that the lsb is set to 0.

[capt-hb]

Yes, it should indeed be sign-extended. These (and maybe other uncovered) bugs are remnants of the "bi-translation" of MinimalCaps (which was initially written directly in microSail). Note that these bugs are only part of the Sail spec of MinimalCaps. The microSail implementation doesn't use bitvectors yet (nor has it any kind of alignment restrictions).