openvm-fv/OpenvmFv/RV32D/bgeu.lean at main · openvm-org/openvm-fv · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
import OpenvmFv.RV32D.Auxiliaries

namespace PureSpec

  structure BgeuInput where
    -- operands
    imm : BitVec 13
    r1_val: BitVec 32
    r2_val: BitVec 32
    -- registers
    PC : BitVec 32

  structure BgeuOutput where
    -- registers
    nextPC : BitVec 32
    -- result
    success : Bool
    throws : Bool

  def execute_BGEU_pure (input : BgeuInput) : BgeuOutput :=
    let skip := !(input.r1_val.toNat ≥b input.r2_val.toNat)
    let throws := !skip && BitVec.ofBool (input.PC + BitVec.signExtend 32 input.imm)[0] == 1#1
    let fails := throws || (!skip && BitVec.ofBool (input.PC + BitVec.signExtend 32 input.imm)[1] == 1#1)
    {
      nextPC := if skip || fails
        then (input.PC + 4)
        else (input.PC + BitVec.signExtend 32 input.imm)
      success := !fails
      throws := throws
      : BgeuOutput
    }

  lemma execute_BGEU_pure_succ_throws
    (input : BgeuInput)
  :
    let output := execute_BGEU_pure input
    output.success = true → output.throws = false
  := by
    simp [execute_BGEU_pure]
    grind

  @[simp]
  lemma sign_extend_equiv :
    @LeanRV32D.Functions.sign_extend width1 width2 =
    @BitVec.signExtend width1 width2
  := rfl

  set_option maxHeartbeats 0 in
  lemma execute_BGEU_pure_equiv
    (bgeu_input : BgeuInput)
    (imm: BitVec 13)
    (h_input_imm: bgeu_input.imm = imm)
    (h_input_r1: read_xreg (regidx_to_fin r1) state = EStateM.Result.ok (bgeu_input.r1_val) state)
    (h_input_r2: read_xreg (regidx_to_fin r2) state = EStateM.Result.ok (bgeu_input.r2_val) state)
    (h_input_pc: state.regs.get? Register.PC = .some bgeu_input.PC)
    (h_input_misa: state.regs.get? Register.misa = .some misa)
  :
    (
      do
        Sail.writeReg Register.nextPC (Sail.BitVec.addInt (← Sail.readReg Register.PC) 4)
        LeanRV32D.Functions.execute (instruction.BTYPE (imm, r2, r1, bop.BGEU ))
    ) state =
    let bgeu_output := execute_BGEU_pure bgeu_input
    (do
      Sail.writeReg Register.nextPC bgeu_output.nextPC
      if bgeu_output.throws then
        throw (Sail.Error.Assertion "extensions/I/base_insts.sail:59.29-59.30")
      else if !bgeu_output.success then
        pure (
          ExecutionResult.Memory_Exception (
            (virtaddr.Virtaddr (bgeu_input.PC + BitVec.signExtend 32 bgeu_input.imm)),
            (ExceptionType.E_Fetch_Addr_Align ())
          )
        )
      else
        (pure (ExecutionResult.Retire_Success ()))) state
  := by
    simp [
      readReg_succ h_input_pc,
      LeanRV32D.Functions.execute,
      writeReg_state_success,
      LeanRV32D.Functions.execute_BTYPE
    ]
    rewrite [rX_read_xreg_equiv _ r1 (regidx_to_fin r1) (by { simp [regidx_to_fin] })]
    rewrite [read_xreg_write_other_reg_state _ h_input_r1 reg_of_fin_neq_nextPC]
    simp
    rewrite [rX_read_xreg_equiv _ r2 (regidx_to_fin r2) (by { simp [regidx_to_fin] })]
    rewrite [read_xreg_write_other_reg_state _ h_input_r2 reg_of_fin_neq_nextPC]
    simp

    by_cases h_eq: bgeu_input.r2_val.toNat ≤ bgeu_input.r1_val.toNat <;>
    simp [h_eq, execute_BGEU_pure]
    rewrite [(readReg_succ (writeReg_read_diff h_input_pc (by trivial)))]
    simp
    rewrite [writeReg_read_diff h_input_misa (by trivial)]
    simp

    by_cases h_throws : (execute_BGEU_pure bgeu_input).throws <;>
    simp_all [execute_BGEU_pure]
    . by_cases h_success : (execute_BGEU_pure bgeu_input).success
      . simp [execute_BGEU_pure, h_eq, h_throws, h_input_imm] at h_success
        repeat rw [if_neg (by omega)]
        simp
      . simp [execute_BGEU_pure, h_eq, h_throws, h_input_imm] at h_success
        repeat rw [if_pos (by omega)]
        simp

end PureSpec