RISC-V specification in Lean

riscv.lean

/-

This set of extensions is guided by the RISC-V profiles draft spec. We deviate by
ignoring `N` as it was never ratified and include `Zihintntl` because it should
really be included. Additionally Zmmul is just a nice touch. Insert additional
divergence here.

https://github.com/riscv/riscv-profiles/blob/main/profiles.adoc

-/
inductive Extensions
/- FIXME: profile spec doesn't include these in its glossary. -/
| Zihintntl | Zmmul

/- The following unprivileged ISA extensions are defined in Volume I of the
https://github.com/riscv/riscv-isa-manual[RISC-V Instruction Set Manual]. -/

/- M Extension for Integer Multiplication and Division -/
| M
/- A Extension for Atomic Memory Operations -/
| A
/- F Extension for Single-Precision Floating-Point
 - D Extension for Double-Precision Floating-Point
 - Q Extension for Quad-Precision Floating-Point -/
| F | D | Q
/- C Extension for Compressed Instructions -/
| C
/- Zifencei Instruction-Fetch Synchronization Extension -/
| Zifencei
/- Zicsr Extension for Control and Status Register Access -/
| Zicsr
/- Zicntr Extension for Basic Performance Counters
 - Zihpm Extension for Hardware Performance Counters -/
| Zicntr | Zihpm
/- Zihintpause Pause Hint Extension -/
| Zihintpause
/- Zfh Extension for Half-Precision Floating-Point
 - Zfhmin Minimal Extension for Half-Precision Floating-Point
 -/
| Zfh | Zfhmin
/- Zfinx Extension for Single-Precision Floating-Point in x-registers
 - Zdinx Extension for Double-Precision Floating-Point in x-registers
 - Zhinx Extension for Half-Precision Floating-Point in x-registers
 - Zhinxmin Minimal Extension for Half-Precision Floating-Point in x-registers
 -/
| Zfinx | Zdinx | Zhinx | Zhinxmin

/-
The following privileged ISA extensions are defined in Volume II of the
https://github.com/riscv/riscv-isa-manual[RISC-V Instruction Set Manual]. -/

/- Sv32 Page-based Virtual Memory Extension, 32-bit
 - Sv39 Page-based Virtual Memory Extension, 39-bit
 - Sv48 Page-based Virtual Memory Extension, 48-bit
 - Sv57 Page-based Virtual Memory Extension, 57-bit -/
| Sv32 | Sv39 | Sv48 | Sv57
/- Svpbmt, Page-Based Memory Types
 - Svnapot, NAPOT Translation Contiguity
 - Svinval, Fine-Grained Address-Translation Cache Invalidation -/
| Svpbmt | Svnapot | Svinval
/- Hypervisor Extension -/
| H
/- Sm1p11, Machine Architecture v1.11
 - Sm1p12, Machine Architecture v1.12 -/
| Sm1p11 | Sm1p12
/- Ss1p11, Supervisor Architecture v1.11
 - Ss1p12, Supervisor Architecture v1.12 -/
| Ss1p11 | Ss1p12

/- The following extensions have not yet been incorporated into the RISC-V
Instruction Set Manual.

https://github.com/riscv/riscv-bitmanip[Bitmanipulation Extension]
https://github.com/riscv/riscv-crypto[Scalar Cryptography Extension]
https://github.com/riscv/riscv-v-spec[Vector Extension]
https://github.com/riscv/riscv-CMOs[Cache Management Operations]
https://github.com/riscv/riscv-time-compare[Supervisor-mode Timer Interrupts]
https://github.com/riscv/riscv-count-overflow[Count Overflow and Mode-Based Filtering]
https://github.com/riscv/riscv-state-enable[State-enable]

-/

/- Zba Address Computation Extension
 - Zbb Bit Manipulation Extension
 - Zbc Carryless Multiplication Extension
 - Zbs Single-Bit Manipulation Extension -/
| Zba | Zbb | Zbc | Zbs
/- Zbkb Extension for Bit Manipulation for Cryptography
 - Zbkc Extension for Carryless Multiplication for Cryptography
 - Zbkx Crossbar Permutation Extension -/
| Zbkb | Zbkc | Zbkx
/- Zk Standard Scalar Cryptography Extension -/
| Zk
/- Zkn NIST Cryptography Extension
 - Zknd AES Decryption Extension
 - Zkne AES Encryption Extension
 - Zknh SHA2 Hashing Extension -/
| Zkn | Zknd | Zkne | Zknh
/- Zkr Entropy Source Extension -/
| Zkr
/- Zks ShangMi Cryptography Extension
 - Zksed SM4 Block Cypher Extension
 - Zksh SM3 Hashing Extension -/
| Zks | Zksed | Zksh
/- Zkt Extension for Data-Independent Execution Latency -/
| Zkt
/- V Extension for Vector Computation -/
| V
/- Zve32x Extension for Embedded Vector Computation (32-bit integer)
 - Zve32f Extension for Embedded Vector Computation (32-bit integer, 32-bit FP)
 - Zve32d Extension for Embedded Vector Computation (32-bit integer, 64-bit FP)
 - Zve64x Extension for Embedded Vector Computation (64-bit integer)
 - Zve64f Extension for Embedded Vector Computation (64-bit integer, 32-bit FP)
 - Zve64d Extension for Embedded Vector Computation (64-bit integer, 64-bit FP) -/
| Zve32x | Zve32f | Zve32d | Zve64x | Zve64f | Zve64d
/- Zicbom Extension for Cache-Block Management
 - Zicbop Extension for Cache-Block Prefetching
 - Zicboz Extension for Cache-Block Zeroin -/
| Zicbom | Zicbop | Zicboz
/- Sstc Extension for Supervisor-mode Timer Interrupts
 - Sscofpmf Extension for Count Overflow and Mode-Based Filtering
 - Smstateen Extension for State-enable -/
| Sstc | Sscofpmf | Smstateen
deriving BEq

structure Profile where
    xlen : Nat
    (mandatory optional uoptional incompatible : Array Extensions := #[])

section Profiles
open Extensions

def RVI20U32 : Profile where
    xlen := 32
    /- +misaligned loads and stores -/
    optional := #[M, A, F, D, C, Zifencei]
    uoptional := #[Zicsr, Q]

def RVI20U64 := { RVI20U32 with xlen := 64 }

def RVA20U64 : Profile where
    xlen := 64
    /- +misaligned loads and stores -/
    mandatory := #[M, A, F, D, C]
    uoptional := #[Zifencei, Q]

def RVA20S64 : Profile where
    xlen := 64
    mandatory := RVA20U64.mandatory.append #[Zifencei, Ss1p11, Sv39]
    optional := #[Sv48]
    uoptional := #[Q]

def RVA22U64 : Profile where
    xlen := 64
    mandatory := RVA20U64.mandatory.append #[Zicntr, Zihpm, Zihintpause, Zba,
        Zbb, Zbs, Zicbom, Zicbop, Zicboz, Zfhmin, Zkt]
    optional := #[Zfh, V, Zkn, Zks]
    uoptional := RVA20U64.uoptional.append #[Zbc, Zbkb, Zbkc, Zbkx, Zknd,
        Zkne, Zknh, Zksed, Zksh, Zve32f, Zve32x, Zve64d, Zve64f, Zve64x, Zkr]
    incompatible := #[Zfinx, Zdinx, Zhinx, Zhinxmin]

def RVA22S64 : Profile where
    xlen := 64
    mandatory := RVA22U64.mandatory.append #[Zifencei, Ss1p11, Ss1p12, Sv39,
        Svpbmt, Svnapot, Svinval]
    optional := RVA22U64.optional.append #[Sv57, Sstc, Sscofpmf, Zkr, H,
        Smstateen]
    uoptional := RVA22U64.uoptional.erase Zkr
    incompatible := RVA22U64.incompatible
end Profiles

inductive Unary
| clz | ctz | cpop
deriving BEq, Repr, Hashable, Inhabited

inductive Binary
| add | sub
| mul | mulh
| div | rem
| slt
| and | or | xor
| andn | orn | xnor
| shiftl | shiftr
| rotl | rotr
| min | max
deriving BEq, Repr, Hashable, Inhabited

inductive Instruction
| unary : Unary -> Instruction
| binary : Binary -> Instruction

structure HardwareDesc where
    xlen : Nat
    extensions : Array Extensions
    (latency throughput : Instruction -> Nat := fun _ => 1)

inductive Opcode
| load   | load_fp  | custom_0   | misc_mem | op_imm | auipc      | op_imm_32 | res_48b
| store  | store_fp | custom_1   | amo      | op     | lui        | op_32     | res_64b
| madd   | msub     | nmsub      | nmadd    | op_fp  | reserved_1 | custom_2  | res_48b'
| branch | jalr     | reserved_2 | jal      | system | reserved_3 | custom_3  | res_80b

class Encode (a : Type) where
    /- Is this instruction supported by the target? -/
    supported (extensions : Array Extensions) : a -> Bool
    /- Regardless of support, encode the instruction -/
    opcode : a -> Opcode
    (funct3 funct5 funct7 : a -> UInt64 := fun _ => 0)

/-

An instruction takes a number of immediate values and/or registers and writes up to one register.

An instruction may read or modify specific CSR values. Or a sequence may require a precondition
on a CSR value, notably floating point and vector extensions.

-/

section Evaluator
variable {ty : Type}
    [Add ty] [Sub ty] [Mul ty] [AndOp ty] [OrOp ty] [ShiftLeft ty] [ShiftRight ty] [Complement ty] [Div ty] [Mod ty] [Xor ty]
    [OfNat ty 0] [OfNat ty 63] [OfNat ty 1] [OfNat ty 64]
    [LT ty] [DecidableEq ty] [DecidableRel (@LT.lt ty _)]

namespace Unary
    instance : Encode Unary where
        supported extensions _ := extensions.contains .Zba
        opcode _ := .op_imm -- alternatively .op_imm_32
        funct3 := fun | .clz | .ctz | .cpop => 1
        funct5 := fun | .clz => 0
                      | .ctz => 1
                      | .cpop => 2
        funct7 := fun | .clz | .ctz | .cpop => 48

    def eval (a : ty) : Unary -> ty
    -- FIXME: Lean should expose these operations...
    | clz => Id.run do
        let mut a := a
        let mut count : ty := 0
        for _ in [: 64] do
            if a &&& (1 <<< 63) = 0 then
                count := count + 1
                a := a <<< 1
            else
                break
        count
    | ctz => Id.run do
        let mut a := a
        let mut count : ty := 0
        for _ in [: 64] do
            if a &&& 1 = 0 then
                count := count + 1
                a := a >>> 1
            else
                break
        count
    | cpop => Id.run do
        let mut a := a
        let mut count : ty := 0
        for _ in [: 64] do
            if a &&& (1 <<< 63) != 0 then
                count := count + 1
            a := a <<< 1
        count
end Unary

namespace Binary
    instance : Encode Binary where
        supported extensions _ := extensions.contains .Zba
        opcode _ := .op -- alternatively .op_imm{,_32} or .fp
        funct3 := fun _ => 0
        funct5 := fun _ => 0
        funct7 := fun _ => 0

    /- FIXME: only implemented XLEN unsigned semantics. -/
    def eval (a b : ty) : Binary -> ty
    | add => a + b
    | sub => a - b
    | mul => a * b
    | mulh => 0 -- (a.toNat * b.toNat) >>> 64 |> UInt64.ofNat
    -- RISC-V divide by zero semantic diverges from Leans!
    | div => if b = 0 then ~~~0 else a / b
    | rem => a % b
    | and => a &&& b
    | or => a ||| b
    | xor => a ^^^ b
    | min => if a < b then a else b
    | max => if a < b then b else a
    | slt => if a < b then 1 else 0
    | shiftl => a <<< (b &&& 63)
    | shiftr => a >>> (b &&& 63)
    | andn => a &&& ~~~b
    | orn => a ||| ~~~b
    | xnor => a ^^^ ~~~b
    | rotl => (a <<< (b &&& 63)) ||| (a >>> (64 - (b &&& 63)))
    | rotr => (a >>> (b &&& 63)) ||| (a <<< (64 - (b &&& 63)))
end Binary
end Evaluator