scalar-crypto: Initial commit of 1.0.0-rc2 spec work.

Makefile

@@ -22,8 +22,11 @@ endif
 SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail
 SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_hints.sail
 SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail
+SAIL_DEFAULT_INST += riscv_insts_zkn.sail
+SAIL_DEFAULT_INST += riscv_insts_zks.sail
 ifeq ($(ARCH),RV64)
 SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_cdext.sail
+else
 endif
 
 SAIL_SEQ_INST  = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
@@ -63,7 +66,8 @@ SAIL_ARCH_SRCS = $(PRELUDE)
 SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail
 SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail
 SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS)
-SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS)
+SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail
+SAIL_ARCH_SRCS += riscv_types_kext.sail    # Shared/common code for the cryptography extension.
 
 SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
 RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail

c_emulator/riscv_platform.c

@@ -45,6 +45,10 @@ mach_bits plat_rom_base(unit u)
 mach_bits plat_rom_size(unit u)
 { return rv_rom_size; }
 
+// Provides entropy for the scalar cryptography extension.
+mach_bits plat_get_16_random_bits()
+{ return rv_16_random_bits(); }
+
 mach_bits plat_clint_base(unit u)
 { return rv_clint_base; }
 

c_emulator/riscv_platform.h

@@ -18,6 +18,9 @@ bool within_phys_mem(mach_bits, sail_int);
 mach_bits plat_rom_base(unit);
 mach_bits plat_rom_size(unit);
 
+// Provides entropy for the scalar cryptography extension.
+mach_bits plat_get_16_random_bits();
+
 mach_bits plat_clint_base(unit);
 mach_bits plat_clint_size(unit);
 

c_emulator/riscv_platform_impl.c

@@ -19,6 +19,20 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
 uint64_t rv_rom_base = UINT64_C(0x1000);
 uint64_t rv_rom_size = UINT64_C(0x100);
 
+// Provides entropy for the scalar cryptography extension.
+uint64_t rv_16_random_bits(void) {
+  // This function can be changed to support deterministic sequences of
+  // pseudo-random bytes. This is useful for testing.
+  const char *name = "/dev/urandom";
+  FILE *f = fopen(name, "rb");
+  uint16_t val;
+  if (fread(&val, 2, 1, f) != 1) {
+    fprintf(stderr, "Unable to read 2 bytes from %s\n", name);
+  }
+  fclose(f);
+  return (uint64_t)val;
+}
+
 uint64_t rv_clint_base = UINT64_C(0x2000000);
 uint64_t rv_clint_size = UINT64_C(0xc0000);
 

c_emulator/riscv_platform_impl.h

@@ -22,6 +22,9 @@ extern uint64_t rv_ram_size;
 extern uint64_t rv_rom_base;
 extern uint64_t rv_rom_size;
 
+// Provides entropy for the scalar cryptography extension.
+extern uint64_t rv_16_random_bits(void);
+
 extern uint64_t rv_clint_base;
 extern uint64_t rv_clint_size;
 

handwritten_support/0.11/riscv_extras.lem

@@ -143,6 +143,10 @@ val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_term_read () = wordFromInteger 0
 declare ocaml target_rep function plat_term_read = `Platform.term_read`
 
+val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_get_16_random_bits () = wordFromInteger 0
+declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits`
+
 val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_right v m = shiftr v (uint m)
 val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a

handwritten_support/riscv_extras.lem

@@ -211,6 +211,10 @@ val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_term_read () = wordFromInteger 0
 declare ocaml target_rep function plat_term_read = `Platform.term_read`
 
+val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_get_16_random_bits () = wordFromInteger 0
+declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits`
+
 val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_right v m = shiftr v (uint m)
 val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a

model/prelude.sail

@@ -248,6 +248,28 @@ function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
     let v64 : bits(64) = EXTS(v) in
     (v64 >> shift)[31..0]
 
+infix 7 >>>
+infix 7 <<<
+
+val rotate_bits_right : forall 'n 'm, 'm >= 0. (bits('n), bits('m)) -> bits('n)
+function rotate_bits_right (v, n) =
+    (v >> n) | (v << (to_bits(length(n), length(v)) - n))
+
+val rotate_bits_left : forall 'n 'm, 'm >= 0. (bits('n), bits('m)) -> bits('n)
+function rotate_bits_left (v, n) =
+    (v << n) | (v >> (to_bits(length(n), length(v)) - n))
+
+val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
+function rotater (v, n) =
+    (v >> n) | (v << (length(v) - n))
+
+val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
+function rotatel (v, n) =
+    (v << n) | (v >> (length(v) - n))
+
+overload operator >>> = {rotate_bits_right, rotater}
+overload operator <<< = {rotate_bits_left, rotatel}
+
 /* helpers for mappings */
 
 val spc : unit <-> string

model/riscv_csr_map.sail

@@ -86,6 +86,8 @@ mapping clause csr_name_map = 0x044  <-> "uip"
 mapping clause csr_name_map = 0x001  <-> "fflags"
 mapping clause csr_name_map = 0x002  <-> "frm"
 mapping clause csr_name_map = 0x003  <-> "fcsr"
+/* user entropy source */
+mapping clause csr_name_map = 0x015  <-> "seed"
 /* counter/timers */
 mapping clause csr_name_map = 0xC00  <-> "cycle"
 mapping clause csr_name_map = 0xC01  <-> "time"
@@ -185,4 +187,4 @@ scattered function ext_read_CSR
 
 /* returns new value (after legalisation) if the CSR is defined */
 val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg}
-scattered function ext_write_CSR
+scattered function ext_write_CSR

model/riscv_insts_zicsr.sail

@@ -158,6 +158,9 @@ function readCSR csr : csreg -> xlenbits = {
     (0xC81, 32) => mtime[63 .. 32],
     (0xC82, 32) => minstret[63 .. 32],
 
+    /* user mode: Zkr */
+    (0x015,  _) => read_seed_csr(),
+
     _           => /* check extensions */
                    match ext_read_CSR(csr) {
                      Some(res) => res,
@@ -235,6 +238,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x144,  _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) },
     (0x180,  _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) },
 
+    /* user mode: seed (entropy source). writes are ignored */
+    (0x015,  _) => write_seed_csr(),
+
     _           => ext_write_CSR(csr, value)
   };
   match res {