diff options
| author | Ben Marshall <ben-marshall@users.noreply.github.com> | 2021-10-18 10:16:43 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-18 10:16:43 +0100 |
| commit | 1c7584bb501bb6d4cbc3b95cb22e008220fb537a (patch) | |
| tree | e07939a9a859628d02b77a4063c0321dcaaed4d8 /handwritten_support | |
| parent | 9f71c756484a4aac7c211d5ea266f45b0b3942e7 (diff) | |
| download | sail-riscv-1c7584bb501bb6d4cbc3b95cb22e008220fb537a.zip sail-riscv-1c7584bb501bb6d4cbc3b95cb22e008220fb537a.tar.gz sail-riscv-1c7584bb501bb6d4cbc3b95cb22e008220fb537a.tar.bz2 | |
scalar-crypto: Initial commit of 1.0.0-rc2 spec work. (#99)
Merged scalar-crypto pull request #99 of 1.0.0-rc2 spec work from Ben Marshall. See https://github.com/riscv/sail-riscv/pull/99.
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/0.11/riscv_extras.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem index db93001..2182940 100644 --- a/handwritten_support/0.11/riscv_extras.lem +++ b/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 diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 2431bb3..b0737e5 100644 --- a/handwritten_support/riscv_extras.lem +++ b/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 |