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_Reads            : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_Writes           : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataMemoryBarrier_All              : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_Reads   : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_Writes  : forall 'rv 'e. unit -> monad 'rv unit 'e
val DataSynchronizationBarrier_All     : forall 'rv 'e. unit -> monad 'rv unit 'e
val InstructionSynchronizationBarrier  : forall 'rv 'e. unit -> monad 'rv unit 'e

let DataMemoryBarrier_Reads ()           = barrier Barrier_DMB_LD
let DataMemoryBarrier_Writes ()          = barrier Barrier_DMB_ST
let DataMemoryBarrier_All ()             = barrier Barrier_DMB
let DataSynchronizationBarrier_Reads ()  = barrier Barrier_DSB_LD
let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST
let DataSynchronizationBarrier_All ()    = barrier Barrier_DSB
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 |>