import THE_MODULE_NAME.Sail.Sail import THE_MODULE_NAME.Defs open Sail def print (_ : String) : Unit := () def print_endline (_ : String) : Unit := () def print_bits (_ : String) (_ : BitVec n) : Unit := () def print_string (_ : String) (_ : String) : Unit := () def print_int (_ : String) (_ : Int) : Unit := () def prerr_endline (_: String) : Unit := () def prerr_string (_: String) : Unit := () def putchar {T} (_: T ) : Unit := () def string_of_int (z : Int) := s!"{z}" axiom sys_enable_writable_misa : Unit → Bool axiom sys_enable_rvc : Unit → Bool axiom sys_enable_fdext : Unit → Bool axiom sys_enable_svinval : Unit → Bool axiom sys_enable_zcb : Unit → Bool axiom sys_enable_zfinx : Unit → Bool axiom sys_enable_writable_fiom : Unit → Bool axiom sys_enable_vext : Unit → Bool axiom sys_enable_bext : Unit → Bool axiom sys_enable_zicbom : Unit → Bool axiom sys_enable_zicboz : Unit → Bool axiom sys_enable_sstc : Unit → Bool axiom sys_writable_hpm_counters : Unit → BitVec 32 axiom sys_vext_vl_use_ceil : Unit → Bool axiom sys_vector_elen_exp : Unit → Nat axiom sys_vector_vlen_exp : Unit → Nat axiom sys_pmp_count : Unit → Nat axiom sys_pmp_count_ok : 0 ≤ sys_pmp_count () ∧ sys_pmp_count () ≤ 64 axiom sys_pmp_grain : Unit → Nat axiom sys_pmp_grain_ok : 0 ≤ sys_pmp_grain () ∧ sys_pmp_grain () ≤ 63 section defs variable [Arch] -- Platform definitions axiom plat_ram_base : Unit → Arch.pa axiom plat_ram_size : Unit → Arch.pa axiom elf_tohost : Unit → Int axiom elf_entry : Unit → Int axiom plat_enable_dirty_update : Unit → Bool axiom plat_enable_misaligned_access : Unit → Bool axiom plat_mtval_has_illegal_inst_bits : Unit → Bool axiom plat_rom_base : Unit → Arch.pa axiom plat_rom_size : Unit → Arch.pa axiom plat_htif_tohost : Unit → Arch.pa axiom plat_clint_base : Unit → Arch.pa axiom plat_clint_size : Unit → Arch.pa axiom plat_insns_per_tick : Unit → Int axiom plat_cache_block_size_exp : Unit → Int section Effectful variable {Register : Type} {RegisterType : Register → Type} [DecidableEq Register] [Hashable Register] axiom plat_term_write {α} : α → SailM Unit axiom plat_term_read : Unit → SailM String -- Reservations axiom load_reservation : Arch.pa → SailM Unit axiom match_reservation : Arch.pa → Bool axiom cancel_reservation : Unit → SailM Unit axiom get_16_random_bits : Unit → SailM (BitVec 16) axiom speculate_conditional : Unit → SailM Bool end Effectful -- Floats axiom extern_f16Add : BitVec 3 → BitVec 16 → BitVec 16 → Unit axiom extern_f16Sub : BitVec 3 → BitVec 16 → BitVec 16 → Unit axiom extern_f16Mul : BitVec 3 → BitVec 16 → BitVec 16 → Unit axiom extern_f16Div : BitVec 3 → BitVec 16 → BitVec 16 → Unit axiom extern_f32Add : BitVec 3 → BitVec 32 → BitVec 32 → Unit axiom extern_f32Sub : BitVec 3 → BitVec 32 → BitVec 32 → Unit axiom extern_f32Mul : BitVec 3 → BitVec 32 → BitVec 32 → Unit axiom extern_f32Div : BitVec 3 → BitVec 32 → BitVec 32 → Unit axiom extern_f64Add : BitVec 3 → BitVec 64 → BitVec 64 → Unit axiom extern_f64Sub : BitVec 3 → BitVec 64 → BitVec 64 → Unit axiom extern_f64Mul : BitVec 3 → BitVec 64 → BitVec 64 → Unit axiom extern_f64Div : BitVec 3 → BitVec 64 → BitVec 64 → Unit axiom extern_f16MulAdd : BitVec 3 → BitVec 16 → BitVec 16 → BitVec 16 → Unit axiom extern_f32MulAdd : BitVec 3 → BitVec 32 → BitVec 32 → BitVec 32 → Unit axiom extern_f64MulAdd : BitVec 3 → BitVec 64 → BitVec 64 → BitVec 64 → Unit axiom extern_f16Sqrt : BitVec 3 → BitVec 16 → Unit axiom extern_f32Sqrt : BitVec 3 → BitVec 32 → Unit axiom extern_f64Sqrt : BitVec 3 → BitVec 64 → Unit axiom extern_f16ToI32 : BitVec 3 → BitVec 16 → Unit axiom extern_f16ToUi32 : BitVec 3 → BitVec 16 → Unit axiom extern_i32ToF16 : BitVec 3 → BitVec 32 → Unit axiom extern_ui32ToF16 : BitVec 3 → BitVec 32 → Unit axiom extern_f16ToI64 : BitVec 3 → BitVec 16 → Unit axiom extern_f16ToUi64 : BitVec 3 → BitVec 16 → Unit axiom extern_i64ToF16 : BitVec 3 → BitVec 64 → Unit axiom extern_ui64ToF16 : BitVec 3 → BitVec 64 → Unit axiom extern_f32ToI32 : BitVec 3 → BitVec 32 → Unit axiom extern_f32ToUi32 : BitVec 3 → BitVec 32 → Unit axiom extern_i32ToF32 : BitVec 3 → BitVec 32 → Unit axiom extern_ui32ToF32 : BitVec 3 → BitVec 32 → Unit axiom extern_f32ToI64 : BitVec 3 → BitVec 32 → Unit axiom extern_f32ToUi64 : BitVec 3 → BitVec 32 → Unit axiom extern_i64ToF32 : BitVec 3 → BitVec 64 → Unit axiom extern_ui64ToF32 : BitVec 3 → BitVec 64 → Unit axiom extern_f64ToI32 : BitVec 3 → BitVec 64 → Unit axiom extern_f64ToUi32 : BitVec 3 → BitVec 64 → Unit axiom extern_i32ToF64 : BitVec 3 → BitVec 32 → Unit axiom extern_ui32ToF64 : BitVec 3 → BitVec 32 → Unit axiom extern_f64ToI64 : BitVec 3 → BitVec 64 → Unit axiom extern_f64ToUi64 : BitVec 3 → BitVec 64 → Unit axiom extern_i64ToF64 : BitVec 3 → BitVec 64 → Unit axiom extern_ui64ToF64 : BitVec 3 → BitVec 64 → Unit axiom extern_f16ToF32 : BitVec 3 → BitVec 16 → Unit axiom extern_f16ToF64 : BitVec 3 → BitVec 16 → Unit axiom extern_f32ToF64 : BitVec 3 → BitVec 32 → Unit axiom extern_f32ToF16 : BitVec 3 → BitVec 32 → Unit axiom extern_f64ToF16 : BitVec 3 → BitVec 64 → Unit axiom extern_f64ToF32 : BitVec 3 → BitVec 64 → Unit axiom extern_f16Lt : BitVec 16 → BitVec 16 → Unit axiom extern_f16Lt_quiet : BitVec 16 → BitVec 16 → Unit axiom extern_f16Le : BitVec 16 → BitVec 16 → Unit axiom extern_f16Le_quiet : BitVec 16 → BitVec 16 → Unit axiom extern_f16Eq : BitVec 16 → BitVec 16 → Unit axiom extern_f32Lt : BitVec 32 → BitVec 32 → Unit axiom extern_f32Lt_quiet : BitVec 32 → BitVec 32 → Unit axiom extern_f32Le : BitVec 32 → BitVec 32 → Unit axiom extern_f32Le_quiet : BitVec 32 → BitVec 32 → Unit axiom extern_f32Eq : BitVec 32 → BitVec 32 → Unit axiom extern_f64Lt : BitVec 64 → BitVec 64 → Unit axiom extern_f64Lt_quiet : BitVec 64 → BitVec 64 → Unit axiom extern_f64Le : BitVec 64 → BitVec 64 → Unit axiom extern_f64Le_quiet : BitVec 64 → BitVec 64 → Unit axiom extern_f64Eq : BitVec 64 → BitVec 64 → Unit axiom extern_f16roundToInt : BitVec 3 → BitVec 16 → Bool → Unit axiom extern_f32roundToInt : BitVec 3 → BitVec 32 → Bool → Unit axiom extern_f64roundToInt : BitVec 3 → BitVec 64 → Bool → Unit -- Termination of extensionEnabled instance : SizeOf extension where sizeOf x := match x with | .Ext_Zihpm => 0 | .Ext_B => 0 | .Ext_C => 0 | .Ext_D => 0 | .Ext_F => 0 | .Ext_Zfh => 0 | .Ext_Zca => 1 | _ => 2 macro_rules | `(tactic| decreasing_trivial) => `(tactic| simp [sizeOf])