diff options
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 |