openvm-fv/OpenvmFv/RV32D/auipc.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
import OpenvmFv.RV32D.Auxiliaries

namespace PureSpec

  structure AuipcInput where
    -- operands
    imm : BitVec 20
    rd: Fin 32
    -- registers
    PC : BitVec 32

  structure AuipcOutput where
    -- registers
    nextPC : BitVec 32
    rd : Option (Finset.Icc 1 31 × BitVec 32)

  def execute_AUIPC_pure (input : AuipcInput) : AuipcOutput :=
    {
      nextPC := (input.PC + 4)
      rd := if h: input.rd = 0
        then .none
        else (.some (⟨input.rd, by {
          apply Finset.mem_Icc.mpr
          omega
        }⟩, input.PC + (input.imm ++ 0#12)))
      : AuipcOutput
    }

  set_option maxHeartbeats 0 in
  lemma execute_AUIPC_pure_equiv
    (auipc_input : AuipcInput)
    (imm: BitVec 21)
    (rd: regidx)
    (h_input_imm: auipc_input.imm = imm)
    (h_input_rd: auipc_input.rd = regidx_to_fin rd)
    (h_input_pc: state.regs.get? Register.PC = .some auipc_input.PC)
  :
    (
      do
        Sail.writeReg Register.nextPC (Sail.BitVec.addInt (← Sail.readReg Register.PC) 4)
        LeanRV32D.Functions.execute (instruction.UTYPE (imm, rd, .AUIPC))
    ) state =
    let auipc_output := execute_AUIPC_pure auipc_input
    (do
      Sail.writeReg Register.nextPC auipc_output.nextPC
      match auipc_output.rd with
        | .some (reg, rd_val) => write_xreg reg rd_val
        | .none => pure ()
      (pure (ExecutionResult.Retire_Success ()))) state
  := by
    simp [
      readReg_succ h_input_pc,
      writeReg_state_success,
      LeanRV32D.Functions.execute,
      execute_AUIPC_pure,
      LeanRV32D.Functions.execute_UTYPE,
      LeanRV32D.Functions.get_arch_pc
    ]
    rewrite [readReg_succ (writeReg_read_diff h_input_pc (by trivial))]
    simp
    by_cases h_rd_0 : auipc_input.rd = 0 <;> simp [h_rd_0]
    . replace h_rd_0 : rd.1.toNat = 0
      := by
        simp [regidx_to_fin, h_rd_0] at h_input_rd
        rcases rd with ⟨ rd, h_rd ⟩
        simp_all
      simp [
        LeanRV32D.Functions.wX_bits,
        LeanRV32D.Functions.wX,
        h_rd_0
      ]
    . rcases rd with ⟨ rd, h_rd ⟩
      simp [regidx_to_fin] at h_input_rd
      simp [h_input_rd, Fin.ext_iff] at h_rd_0
      simp at h_rd
      simp [
        write_xreg,
        Sail.writeReg,
        PreSail.writeReg,
        LeanRV32D.Functions.wX_bits,
        LeanRV32D.Functions.wX,
        reg_of_fin
      ]
      interval_cases rd <;> simp
      . omega
      all_goals
        congr <;> simp_all

end PureSpec