Add support for Zfh extension (#129)

4 files changed, 665 insertions, 0 deletions

diff --git a/prover_snapshots/hol4/RV32/riscvScript.sml b/prover_snapshots/hol4/RV32/riscvScript.sml
index e8a4065..a537181 100644
--- a/prover_snapshots/hol4/RV32/riscvScript.sml
+++ b/prover_snapshots/hol4/RV32/riscvScript.sml
@@ -10325,6 +10325,50 @@ val _ = Define `
     (sail2_state_monad$write_regS float_fflags_ref ((zero_extend flags (( 64 : int):ii)  :  64 words$word))))`;
 
 
+(*val riscv_f16Add : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Add:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_add rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Sub : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Sub:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_sub rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Mul : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Mul:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_mul rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Div : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Div:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_div rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32Add : mword ty3 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10409,6 +10453,17 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16MulAdd : mword ty3 -> mword ty16 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16MulAdd:(3)words$word ->(16)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2 v3=
+    (let (_ : unit) = (softfloat_f16_muladd rm v1 v2 v3) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32MulAdd : mword ty3 -> mword ty32 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10430,6 +10485,17 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16Sqrt : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Sqrt:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_sqrt rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32Sqrt : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10451,6 +10517,92 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16ToI32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)*)
+
+val _ = Define `
+ ((riscv_f16ToI32:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_i32 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
+
+
+(*val riscv_f16ToUi32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)*)
+
+val _ = Define `
+ ((riscv_f16ToUi32:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_ui32 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
+
+
+(*val riscv_i32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_i32ToF16:(3)words$word ->(32)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_i32_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_ui32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_ui32ToF16:(3)words$word ->(32)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_ui32_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16ToI64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)*)
+
+val _ = Define `
+ ((riscv_f16ToI64:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(64)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_i64 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
+
+
+(*val riscv_f16ToUi64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)*)
+
+val _ = Define `
+ ((riscv_f16ToUi64:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(64)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_ui64 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
+
+
+(*val riscv_i64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_i64ToF16:(3)words$word ->(64)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_i64_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_ui64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_ui64ToF16:(3)words$word ->(64)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_ui64_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32ToI32 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10619,6 +10771,27 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16ToF32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)*)
+
+val _ = Define `
+ ((riscv_f16ToF32:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_f32 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
+
+
+(*val riscv_f16ToF64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)*)
+
+val _ = Define `
+ ((riscv_f16ToF64:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(64)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_f64 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
+
+
 (*val riscv_f32ToF64 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty64)*)
 
 val _ = Define `
@@ -10629,6 +10802,28 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f32ToF16:(3)words$word ->(32)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f32_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f64ToF16:(3)words$word ->(64)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f64_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f64ToF32 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10640,6 +10835,39 @@ val _ = Define `
            (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
 
 
+(*val riscv_f16Lt : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Lt:(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) v1 v2=
+    (let (_ : unit) = (softfloat_f16_lt v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Le : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Le:(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) v1 v2=
+    (let (_ : unit) = (softfloat_f16_le v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Eq : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Eq:(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) v1 v2=
+    (let (_ : unit) = (softfloat_f16_eq v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32Lt : mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
diff --git a/prover_snapshots/hol4/RV32/riscv_extras_fdextScript.sml b/prover_snapshots/hol4/RV32/riscv_extras_fdextScript.sml
index ab68323..55e47ec 100644
--- a/prover_snapshots/hol4/RV32/riscv_extras_fdextScript.sml
+++ b/prover_snapshots/hol4/RV32/riscv_extras_fdextScript.sml
@@ -20,6 +20,25 @@ val _ = type_abbrev((*  'a *) "bitvector0" , ``:  'a words$word``);
 
 (* stub functions emulating the C softfloat interface *)
 
+(*val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_add:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
+
+(*val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_sub:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
+
+(*val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_mul:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
+
+(*val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_div:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
 (*val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_add:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
@@ -61,6 +80,11 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_muladd:'rm words$word -> 's words$word -> 's words$word -> 's words$word -> unit) _ _ _ _=  () )`;
+
+
 (*val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_muladd:'rm words$word -> 's words$word -> 's words$word -> 's words$word -> unit) _ _ _ _=  () )`;
@@ -72,6 +96,11 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_sqrt:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
 (*val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_sqrt:'rm words$word -> 's words$word -> unit) _ _=  () )`;
@@ -83,6 +112,47 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_i32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_ui32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_i32_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_ui32_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_i64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_ui64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_i64_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_ui64_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+
 (*val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_to_i32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
@@ -165,17 +235,52 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_f32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_f64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
 (*val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_to_f64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
 
 
+(*val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f32_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f64_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
 (*val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f64_to_f32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
 
 
 
+(*val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_lt:'s words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_le:'s words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_eq:'s words$word -> 's words$word -> unit) _ _=  () )`;
+
+
 (*val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_lt:'s words$word -> 's words$word -> unit) _ _=  () )`;
diff --git a/prover_snapshots/hol4/RV64/riscvScript.sml b/prover_snapshots/hol4/RV64/riscvScript.sml
index 1910c35..7796250 100644
--- a/prover_snapshots/hol4/RV64/riscvScript.sml
+++ b/prover_snapshots/hol4/RV64/riscvScript.sml
@@ -10339,6 +10339,50 @@ val _ = Define `
     (sail2_state_monad$write_regS float_fflags_ref ((zero_extend flags (( 64 : int):ii)  :  64 words$word))))`;
 
 
+(*val riscv_f16Add : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Add:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_add rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Sub : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Sub:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_sub rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Mul : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Mul:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_mul rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Div : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Div:(3)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2=
+    (let (_ : unit) = (softfloat_f16_div rm v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32Add : mword ty3 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10423,6 +10467,17 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16MulAdd : mword ty3 -> mword ty16 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16MulAdd:(3)words$word ->(16)words$word ->(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v1 v2 v3=
+    (let (_ : unit) = (softfloat_f16_muladd rm v1 v2 v3) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32MulAdd : mword ty3 -> mword ty32 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10444,6 +10499,17 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16Sqrt : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Sqrt:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_sqrt rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32Sqrt : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10465,6 +10531,92 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16ToI32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)*)
+
+val _ = Define `
+ ((riscv_f16ToI32:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_i32 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
+
+
+(*val riscv_f16ToUi32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)*)
+
+val _ = Define `
+ ((riscv_f16ToUi32:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_ui32 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
+
+
+(*val riscv_i32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_i32ToF16:(3)words$word ->(32)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_i32_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_ui32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_ui32ToF16:(3)words$word ->(32)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_ui32_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16ToI64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)*)
+
+val _ = Define `
+ ((riscv_f16ToI64:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(64)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_i64 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
+
+
+(*val riscv_f16ToUi64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)*)
+
+val _ = Define `
+ ((riscv_f16ToUi64:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(64)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_ui64 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
+
+
+(*val riscv_i64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_i64ToF15:(3)words$word ->(64)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_i64_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_ui64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_ui64ToF16:(3)words$word ->(64)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_ui64_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32ToI32 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10633,6 +10785,27 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f16ToF32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)*)
+
+val _ = Define `
+ ((riscv_f16ToF32:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(32)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_f32 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
+
+
+(*val riscv_f16ToF64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)*)
+
+val _ = Define `
+ ((riscv_f16ToF64:(3)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(64)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f16_to_f64 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
+
+
 (*val riscv_f32ToF64 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty64)*)
 
 val _ = Define `
@@ -10643,6 +10816,28 @@ val _ = Define `
    sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word), w__1)))))`;
 
 
+(*val riscv_f32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f32ToF16:(3)words$word ->(32)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f32_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f64ToF16:(3)words$word ->(64)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) rm v=
+    (let (_ : unit) = (softfloat_f64_to_f16 rm v) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f64ToF32 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
@@ -10654,6 +10849,39 @@ val _ = Define `
            (subrange_vec_dec w__1 (( 31 : int):ii) (( 0 : int):ii)  :  32 words$word))))))`;
 
 
+(*val riscv_f16Lt : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Lt:(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) v1 v2=
+    (let (_ : unit) = (softfloat_f16_lt v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Le : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Le:(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) v1 v2=
+    (let (_ : unit) = (softfloat_f16_le v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
+(*val riscv_f16Eq : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)*)
+
+val _ = Define `
+ ((riscv_f16Eq:(16)words$word ->(16)words$word ->(regstate)sail2_state_monad$sequential_state ->((((5)words$word#(16)words$word),(exception))sail2_state_monad$result#(regstate)sail2_state_monad$sequential_state)set) v1 v2=
+    (let (_ : unit) = (softfloat_f16_eq v1 v2) in sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_fflags_ref  : ( 64 words$word) M) (\ (w__0 :  64 words$word) .  sail2_state_monad$bindS
+   (sail2_state_monad$read_regS float_result_ref  : ( 64 words$word) M) (\ (w__1 :  64 words$word) . 
+   sail2_state_monad$returnS ((subrange_vec_dec w__0 (( 4 : int):ii) (( 0 : int):ii)  :  5 words$word),
+           (subrange_vec_dec w__1 (( 15 : int):ii) (( 0 : int):ii)  :  16 words$word))))))`;
+
+
 (*val riscv_f32Lt : mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)*)
 
 val _ = Define `
diff --git a/prover_snapshots/hol4/RV64/riscv_extras_fdextScript.sml b/prover_snapshots/hol4/RV64/riscv_extras_fdextScript.sml
index ab68323..e1d399a 100644
--- a/prover_snapshots/hol4/RV64/riscv_extras_fdextScript.sml
+++ b/prover_snapshots/hol4/RV64/riscv_extras_fdextScript.sml
@@ -20,6 +20,25 @@ val _ = type_abbrev((*  'a *) "bitvector0" , ``:  'a words$word``);
 
 (* stub functions emulating the C softfloat interface *)
 
+(*val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_add:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
+
+(*val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_sub:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
+
+(*val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_mul:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
+
+(*val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_div:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
+
 (*val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_add:'rm words$word -> 's words$word -> 's words$word -> unit) _ _ _=  () )`;
@@ -61,6 +80,11 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_muladd:'rm words$word -> 's words$word -> 's words$word -> 's words$word -> unit) _ _ _ _=  () )`;
+
+
 (*val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_muladd:'rm words$word -> 's words$word -> 's words$word -> 's words$word -> unit) _ _ _ _=  () )`;
@@ -72,6 +96,11 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_sqrt:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
 (*val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_sqrt:'rm words$word -> 's words$word -> unit) _ _=  () )`;
@@ -83,6 +112,47 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_i32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_ui32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_i32_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_ui32_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_i64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_ui64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_i64_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_ui64_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+
 (*val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_to_i32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
@@ -165,16 +235,50 @@ val _ = Define `
 
 
 
+(*val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_f32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_to_f64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
 (*val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f32_to_f64:'rm words$word -> 's words$word -> unit) _ _=  () )`;
 
 
+(*val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f32_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f64_to_f16:'rm words$word -> 's words$word -> unit) _ _=  () )`;
+
+
 (*val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit*)
 val _ = Define `
  ((softfloat_f64_to_f32:'rm words$word -> 's words$word -> unit) _ _=  () )`;
 
 
+(*val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_lt:'s words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_le:'s words$word -> 's words$word -> unit) _ _=  () )`;
+
+
+(*val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
+val _ = Define `
+ ((softfloat_f16_eq:'s words$word -> 's words$word -> unit) _ _=  () )`;
+
 
 (*val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit*)
 val _ = Define `