arm-hyp refine: fix PageTableDuplicates

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

riscv: add kdev_base/kdevBase to handle RISCVVSpaceDeviceWindow and u…

…pdate proofs

- Add HiFive.hs to replace Spike.hs, it's the same except for kdevBase
  addition.
- Originally called KDEV_PPTR in the C Code, to be changed to KDEV_BASE
  across all architectures.
- Add RISCVVSpaceDeviceWindow case for valid_uses_2 definition.

riscv ainvs: cleanup in crunch setup and invariant definitions

riscv ainvs: sorried ArchAcc_AI

co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>

rt: remove trailing whitespaces

rt ainvs: fix more sorries in IpcCancel_AI (12 to go)

rt invariants: more sorrying in IpcCancel_AI

rt abstract/doc: update spec document preamble