Add support for Zfh extension (#129)

8 files changed, 1429 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 `
diff --git a/prover_snapshots/isabelle/RV32/Riscv.thy b/prover_snapshots/isabelle/RV32/Riscv.thy
index 75b4089..2108651 100644
--- a/prover_snapshots/isabelle/RV32/Riscv.thy
+++ b/prover_snapshots/isabelle/RV32/Riscv.thy
@@ -10514,6 +10514,62 @@ definition update_softfloat_fflags  :: \<open>(5)Word.word \<Rightarrow>((regist
   for  flags  :: "(5)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16Add : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Add  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Add rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_add rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Sub : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Sub  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Sub rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_sub rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Mul : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Mul  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Mul rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_mul rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Div : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Div  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Div rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_div rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32Add : mword ty3 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32Add  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10622,6 +10678,21 @@ definition riscv_f64Div  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rig
   and  v2  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16MulAdd : mword ty3 -> mword ty16 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16MulAdd  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16MulAdd rm v1 v2 v3 = (
+   (let (_ :: unit) = (softfloat_f16_muladd rm v1 v2 v3) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word " 
+  and  v3  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32MulAdd : mword ty3 -> mword ty32 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32MulAdd  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10651,6 +10722,19 @@ definition riscv_f64MulAdd  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<
   and  v3  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16Sqrt : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Sqrt  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Sqrt rm v = (
+   (let (_ :: unit) = (softfloat_f16_sqrt rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32Sqrt : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32Sqrt  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10676,6 +10760,108 @@ definition riscv_f64Sqrt  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Ri
   and  v  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16ToI32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)\<close>\<close>
+
+definition riscv_f16ToI32  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToI32 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_i32 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 31 :: int)::ii) (( 0 :: int)::ii)  ::  32 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToUi32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)\<close>\<close>
+
+definition riscv_f16ToUi32  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToUi32 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_ui32 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 31 :: int)::ii) (( 0 :: int)::ii)  ::  32 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_i32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_i32ToF16  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_i32ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_i32_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(32)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_ui32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_ui32ToF16  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_ui32ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_ui32_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(32)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToI64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)\<close>\<close>
+
+definition riscv_f16ToI64  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToI64 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_i64 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word), w__1)))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToUi64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)\<close>\<close>
+
+definition riscv_f16ToUi64  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToUi64 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_ui64 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word), w__1)))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_i64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_i64ToF16  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_i64ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_i64_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(64)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_ui64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_ui64ToF16  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_ui64ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_ui64_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(64)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32ToI32 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32ToI32  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10876,6 +11062,31 @@ definition riscv_ui64ToF64  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<
   and  v  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16ToF32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)\<close>\<close>
+
+definition riscv_f16ToF32  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToF32 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_f32 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 31 :: int)::ii) (( 0 :: int)::ii)  ::  32 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToF64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)\<close>\<close>
+
+definition riscv_f16ToF64  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToF64 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_f64 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word), w__1)))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32ToF64 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty64)\<close>\<close>
 
 definition riscv_f32ToF64  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
@@ -10888,6 +11099,32 @@ definition riscv_f32ToF64  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<R
   and  v  :: "(32)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f32ToF16  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f32ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_f32_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(32)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f64ToF16  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f64ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_f64_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(64)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f64ToF32 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f64ToF32  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10901,6 +11138,45 @@ definition riscv_f64ToF32  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<R
   and  v  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16Lt : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Lt  :: \<open>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Lt v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_lt v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Le : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Le  :: \<open>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Le v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_le v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Eq : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Eq  :: \<open>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Eq v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_eq v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32Lt : mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32Lt  :: \<open>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
diff --git a/prover_snapshots/isabelle/RV32/Riscv_extras_fdext.thy b/prover_snapshots/isabelle/RV32/Riscv_extras_fdext.thy
index 19fa034..a6e1817 100644
--- a/prover_snapshots/isabelle/RV32/Riscv_extras_fdext.thy
+++ b/prover_snapshots/isabelle/RV32/Riscv_extras_fdext.thy
@@ -26,6 +26,26 @@ type_synonym 'a bitvector0 =" ( 'a::len)Word.word "
 
 \<comment> \<open>\<open> stub functions emulating the C softfloat interface \<close>\<close>
 
+\<comment> \<open>\<open>val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_add  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_add _ _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_sub  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_sub _ _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_mul  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_mul _ _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_div  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_div _ _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_add  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_add _ _ _ = ( ()  )\<close>
@@ -67,6 +87,11 @@ definition softfloat_f64_div  :: \<open>('rm::len)Word.word \<Rightarrow>('s::le
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_muladd  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_muladd _ _ _ _ = ( ()  )\<close>
+ 
+
 \<comment> \<open>\<open>val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_muladd  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_muladd _ _ _ _ = ( ()  )\<close>
@@ -78,6 +103,11 @@ definition softfloat_f64_muladd  :: \<open>('rm::len)Word.word \<Rightarrow>('s:
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_sqrt  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_sqrt _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_sqrt  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_sqrt _ _ = ( ()  )\<close>
@@ -89,6 +119,47 @@ definition softfloat_f64_sqrt  :: \<open>('rm::len)Word.word \<Rightarrow>('s::l
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_i32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_i32 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_ui32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_ui32 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_i32_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_i32_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_ui32_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_ui32_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_i64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_i64 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_ui64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_ui64 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_i64_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_i64_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_ui64_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_ui64_to_f16 _ _ = ( ()  )\<close>
+
+
+
 \<comment> \<open>\<open>val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_to_i32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_to_i32 _ _ = ( ()  )\<close>
@@ -171,17 +242,52 @@ definition softfloat_ui64_to_f64  :: \<open>('rm::len)Word.word \<Rightarrow>('s
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_f32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_f32 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_f64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_f64 _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_to_f64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_to_f64 _ _ = ( ()  )\<close>
 
 
+\<comment> \<open>\<open>val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f32_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f32_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f64_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f64_to_f16 _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f64_to_f32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f64_to_f32 _ _ = ( ()  )\<close>
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_lt  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_lt _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_le  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_le _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_eq  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_eq _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_lt  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_lt _ _ = ( ()  )\<close>
diff --git a/prover_snapshots/isabelle/RV64/Riscv.thy b/prover_snapshots/isabelle/RV64/Riscv.thy
index e449315..a6964d2 100644
--- a/prover_snapshots/isabelle/RV64/Riscv.thy
+++ b/prover_snapshots/isabelle/RV64/Riscv.thy
@@ -10528,6 +10528,62 @@ definition update_softfloat_fflags  :: \<open>(5)Word.word \<Rightarrow>((regist
   for  flags  :: "(5)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16Add : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Add  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Add rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_add rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Sub : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Sub  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Sub rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_sub rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Mul : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Mul  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Mul rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_mul rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Div : mword ty3 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Div  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Div rm v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_div rm v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32Add : mword ty3 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32Add  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10636,6 +10692,21 @@ definition riscv_f64Div  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rig
   and  v2  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16MulAdd : mword ty3 -> mword ty16 -> mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16MulAdd  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16MulAdd rm v1 v2 v3 = (
+   (let (_ :: unit) = (softfloat_f16_muladd rm v1 v2 v3) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word " 
+  and  v3  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32MulAdd : mword ty3 -> mword ty32 -> mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32MulAdd  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10665,6 +10736,19 @@ definition riscv_f64MulAdd  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<
   and  v3  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16Sqrt : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Sqrt  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Sqrt rm v = (
+   (let (_ :: unit) = (softfloat_f16_sqrt rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32Sqrt : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32Sqrt  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10690,6 +10774,108 @@ definition riscv_f64Sqrt  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Ri
   and  v  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16ToI32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)\<close>\<close>
+
+definition riscv_f16ToI32  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToI32 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_i32 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 31 :: int)::ii) (( 0 :: int)::ii)  ::  32 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToUi32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)\<close>\<close>
+
+definition riscv_f16ToUi32  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToUi32 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_ui32 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 31 :: int)::ii) (( 0 :: int)::ii)  ::  32 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_i32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_i32ToF16  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_i32ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_i32_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(32)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_ui32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_ui32ToF16  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_ui32ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_ui32_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(32)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToI64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)\<close>\<close>
+
+definition riscv_f16ToI64  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToI64 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_i64 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word), w__1)))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToUi64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)\<close>\<close>
+
+definition riscv_f16ToUi64  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToUi64 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_ui64 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word), w__1)))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_i64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_i64ToF16  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_i64ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_i64_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(64)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_ui64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_ui64ToF16  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_ui64ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_ui64_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(64)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32ToI32 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32ToI32  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10890,6 +11076,31 @@ definition riscv_ui64ToF64  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<
   and  v  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16ToF32 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty32)\<close>\<close>
+
+definition riscv_f16ToF32  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToF32 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_f32 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 31 :: int)::ii) (( 0 :: int)::ii)  ::  32 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16ToF64 : mword ty3 -> mword ty16 -> M (mword ty5 * mword ty64)\<close>\<close>
+
+definition riscv_f16ToF64  :: \<open>(3)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16ToF64 rm v = (
+   (let (_ :: unit) = (softfloat_f16_to_f64 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word), w__1)))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32ToF64 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty64)\<close>\<close>
 
 definition riscv_f32ToF64  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(64)Word.word),(exception))monad \<close>  where 
@@ -10902,6 +11113,32 @@ definition riscv_f32ToF64  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<R
   and  v  :: "(32)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f32ToF16 : mword ty3 -> mword ty32 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f32ToF16  :: \<open>(3)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f32ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_f32_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(32)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f64ToF16 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f64ToF16  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f64ToF16 rm v = (
+   (let (_ :: unit) = (softfloat_f64_to_f16 rm v) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  rm  :: "(3)Word.word " 
+  and  v  :: "(64)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f64ToF32 : mword ty3 -> mword ty64 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f64ToF32  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
@@ -10915,6 +11152,45 @@ definition riscv_f64ToF32  :: \<open>(3)Word.word \<Rightarrow>(64)Word.word \<R
   and  v  :: "(64)Word.word "
 
 
+\<comment> \<open>\<open>val riscv_f16Lt : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Lt  :: \<open>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Lt v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_lt v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Le : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Le  :: \<open>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Le v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_le v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
+\<comment> \<open>\<open>val riscv_f16Eq : mword ty16 -> mword ty16 -> M (mword ty5 * mword ty16)\<close>\<close>
+
+definition riscv_f16Eq  :: \<open>(16)Word.word \<Rightarrow>(16)Word.word \<Rightarrow>((register_value),((5)Word.word*(16)Word.word),(exception))monad \<close>  where 
+     \<open> riscv_f16Eq v1 v2 = (
+   (let (_ :: unit) = (softfloat_f16_eq v1 v2) in
+   (read_reg float_fflags_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__0 ::  64 Word.word) . 
+   (read_reg float_result_ref  :: ( 64 Word.word) M) \<bind> ((\<lambda> (w__1 ::  64 Word.word) . 
+   return ((subrange_vec_dec w__0 (( 4 :: int)::ii) (( 0 :: int)::ii)  ::  5 Word.word),
+           (subrange_vec_dec w__1 (( 15 :: int)::ii) (( 0 :: int)::ii)  ::  16 Word.word))))))))\<close> 
+  for  v1  :: "(16)Word.word " 
+  and  v2  :: "(16)Word.word "
+
+
 \<comment> \<open>\<open>val riscv_f32Lt : mword ty32 -> mword ty32 -> M (mword ty5 * mword ty32)\<close>\<close>
 
 definition riscv_f32Lt  :: \<open>(32)Word.word \<Rightarrow>(32)Word.word \<Rightarrow>((register_value),((5)Word.word*(32)Word.word),(exception))monad \<close>  where 
diff --git a/prover_snapshots/isabelle/RV64/Riscv_extras_fdext.thy b/prover_snapshots/isabelle/RV64/Riscv_extras_fdext.thy
index 19fa034..cc26980 100644
--- a/prover_snapshots/isabelle/RV64/Riscv_extras_fdext.thy
+++ b/prover_snapshots/isabelle/RV64/Riscv_extras_fdext.thy
@@ -26,6 +26,26 @@ type_synonym 'a bitvector0 =" ( 'a::len)Word.word "
 
 \<comment> \<open>\<open> stub functions emulating the C softfloat interface \<close>\<close>
 
+\<comment> \<open>\<open>val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_add  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_add _ _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_sub  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_sub _ _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_mul  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_mul _ _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_div  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_div _ _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_add  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_add _ _ _ = ( ()  )\<close>
@@ -67,6 +87,11 @@ definition softfloat_f64_div  :: \<open>('rm::len)Word.word \<Rightarrow>('s::le
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_muladd  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_muladd _ _ _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_muladd  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_muladd _ _ _ _ = ( ()  )\<close>
@@ -78,6 +103,11 @@ definition softfloat_f64_muladd  :: \<open>('rm::len)Word.word \<Rightarrow>('s:
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_sqrt  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_sqrt _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_sqrt  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_sqrt _ _ = ( ()  )\<close>
@@ -89,6 +119,47 @@ definition softfloat_f64_sqrt  :: \<open>('rm::len)Word.word \<Rightarrow>('s::l
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_i32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_i32 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_ui32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_ui32 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_i32_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_i32_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_ui32_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_ui32_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_i64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_i64 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_ui64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_ui64 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_i64_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_i64_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_ui64_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_ui64_to_f16 _ _ = ( ()  )\<close>
+
+
+
 \<comment> \<open>\<open>val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_to_i32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_to_i32 _ _ = ( ()  )\<close>
@@ -171,17 +242,52 @@ definition softfloat_ui64_to_f64  :: \<open>('rm::len)Word.word \<Rightarrow>('s
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_f32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_f32 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_to_f64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_to_f64 _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_to_f64  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_to_f64 _ _ = ( ()  )\<close>
 
 
+\<comment> \<open>\<open>val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f32_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f32_to_f16 _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f64_to_f16  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f64_to_f16 _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f64_to_f32  :: \<open>('rm::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f64_to_f32 _ _ = ( ()  )\<close>
 
 
 
+\<comment> \<open>\<open>val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_lt  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_lt _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_le  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_le _ _ = ( ()  )\<close>
+
+
+\<comment> \<open>\<open>val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
+definition softfloat_f16_eq  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
+     \<open> softfloat_f16_eq _ _ = ( ()  )\<close>
+
+
 \<comment> \<open>\<open>val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit\<close>\<close>
 definition softfloat_f32_lt  :: \<open>('s::len)Word.word \<Rightarrow>('s::len)Word.word \<Rightarrow> unit \<close>  where 
      \<open> softfloat_f32_lt _ _ = ( ()  )\<close>