pub unsafe extern "C" fn Hacl_Bignum64_sub( len: u32, a: *mut u64, b: *mut u64, res: *mut u64, ) -> u64