open import Pervasives
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_prompt
open import ArmV8_types

val rMem_NORMAL         : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_STREAM         : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_ORDERED        : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_ATOMICL        : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e

let rMem_NORMAL addr size         = read_mem Read_plain () addr size
let rMem_STREAM addr size         = read_mem Read_stream () addr size
let rMem_ORDERED addr size        = read_mem Read_acquire () addr size
let rMem_ATOMIC addr size         = read_mem Read_exclusive () addr size
let rMem_ATOMIC_ORDERED addr size = read_mem Read_exclusive_acquire () addr size

val wMem_Addr_NORMAL         : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
val wMem_Addr_ORDERED        : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
val wMem_Addr_ATOMIC         : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
val wMem_Addr_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e

let wMem_Addr_NORMAL addr size         = write_mem_ea Write_plain () addr size
let wMem_Addr_ORDERED addr size        = write_mem_ea Write_release () addr size
let wMem_Addr_ATOMIC addr size         = write_mem_ea Write_exclusive () addr size
let wMem_Addr_ATOMIC_ORDERED addr size = write_mem_ea Write_exclusive_release () addr size


val wMem_Val_NORMAL : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv unit 'e
val wMem_Val_ORDERED : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv unit 'e
val wMem_Val_ATOMIC : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv bool 'e
val wMem_Val_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv bool 'e

let wMem_Val_NORMAL addr size v = write_mem Write_plain () addr size v >>= fun _ -> return ()
let wMem_Val_ORDERED addr size v = write_mem Write_release () addr size v >>= fun _ -> return ()
(* in ARM the status returned is inversed *)
let wMem_Val_ATOMIC addr size v = write_mem Write_exclusive () addr size v >>= fun b -> return (not b)
let wMem_Val_ATOMIC_ORDERED addr size v = write_mem Write_exclusive_release () addr size v >>= fun b -> return (not b)

let speculate_exclusive_success () = excl_result ()

val DataMemoryBarrier_NonShReads    : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_NonShWrites   : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_NonShAll      : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_InnerShReads  : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_InnerShAll    : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_OuterShReads  : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_OuterShAll    : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_FullShReads   : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_FullShWrites  : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_FullShAll     : forall 'rv 'e. unit -> monad 'rv unit 'e
let DataMemoryBarrier_NonShReads ()    = barrier (Barrier_DMB (A64_NonShare,   A64_barrier_LD))
let DataMemoryBarrier_NonShWrites ()   = barrier (Barrier_DMB (A64_NonShare,   A64_barrier_ST))
let DataMemoryBarrier_NonShAll ()      = barrier (Barrier_DMB (A64_NonShare,   A64_barrier_all))
let DataMemoryBarrier_InnerShReads ()  = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_LD))
let DataMemoryBarrier_InnerShWrites () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_ST))
let DataMemoryBarrier_InnerShAll ()    = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_all))
let DataMemoryBarrier_OuterShReads ()  = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_LD))
let DataMemoryBarrier_OuterShWrites () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_ST))
let DataMemoryBarrier_OuterShAll ()    = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_all))
let DataMemoryBarrier_FullShReads ()   = barrier (Barrier_DMB (A64_FullShare,  A64_barrier_LD))
let DataMemoryBarrier_FullShWrites ()  = barrier (Barrier_DMB (A64_FullShare,  A64_barrier_ST))
let DataMemoryBarrier_FullShAll ()     = barrier (Barrier_DMB (A64_FullShare,  A64_barrier_all))

val DataSynchronizationBarrier_NonShReads    : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_NonShWrites   : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_NonShAll      : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_InnerShReads  : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_InnerShAll    : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_OuterShReads  : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_OuterShAll    : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_FullShReads   : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_FullShWrites  : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_FullShAll     : forall 'rv 'e. unit -> monad 'rv unit 'e
let DataSynchronizationBarrier_NonShReads ()    = barrier (Barrier_DSB (A64_NonShare,   A64_barrier_LD))
let DataSynchronizationBarrier_NonShWrites ()   = barrier (Barrier_DSB (A64_NonShare,   A64_barrier_ST))
let DataSynchronizationBarrier_NonShAll ()      = barrier (Barrier_DSB (A64_NonShare,   A64_barrier_all))
let DataSynchronizationBarrier_InnerShReads ()  = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_LD))
let DataSynchronizationBarrier_InnerShWrites () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_ST))
let DataSynchronizationBarrier_InnerShAll ()    = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_all))
let DataSynchronizationBarrier_OuterShReads ()  = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_LD))
let DataSynchronizationBarrier_OuterShWrites () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_ST))
let DataSynchronizationBarrier_OuterShAll ()    = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_all))
let DataSynchronizationBarrier_FullShReads ()   = barrier (Barrier_DSB (A64_FullShare,  A64_barrier_LD))
let DataSynchronizationBarrier_FullShWrites ()  = barrier (Barrier_DSB (A64_FullShare,  A64_barrier_ST))
let DataSynchronizationBarrier_FullShAll ()     = barrier (Barrier_DSB (A64_FullShare,  A64_barrier_all))

val InstructionSynchronizationBarrier  : forall 'rv 'e. unit -> monad 'rv unit 'e
let InstructionSynchronizationBarrier () = barrier (Barrier_ISB ())

val TMCommitEffect : forall 'rv 'e. unit -> monad 'rv unit 'e
let TMCommitEffect () = barrier (Barrier_TM_COMMIT ())

val SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type
let SCTLR_EL1_type_to_SCTLR_type <| SCTLR_EL1_type_SCTLR_EL1_type_chunk_0 = x |> = <| SCTLR_type_SCTLR_type_chunk_0 = x |>