		Search-engine friendly clone of the ACL2 documentation.

Semantics64

Exec64-auipc

Semantics of the AUIPC instruction [ISA:4.2.1].

Signature
(exec64-auipc rd imm pc stat) → new-stat
Arguments: rd — Guard (ubyte5p rd).; imm — Guard (ubyte20p imm).; pc — Guard (ubyte64p pc).; stat — Guard (state64p stat).
Returns: new-stat — Type (state64p new-stat).

We use the 20 bits of the immediate as the high bits of an unsigned 32-bit integer, whose low bits are 0. We extend the unsigned 32-bit integer to 64 bits, obtaining an unsigned 64-bit address. We add the latter to the address of the instruction, which is passed as the pc input to this function. We write the result to rd. We increment the program counter.

Definitions and Theorems

Function: exec64-auipc

(defun exec64-auipc (rd imm pc stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte20p imm)
                              (ubyte64p pc)
                              (state64p stat))))
  (let ((__function__ 'exec64-auipc))
    (declare (ignorable __function__))
    (b* ((offset (loghead 64
                          (logext 32 (ash (ubyte20-fix imm) 12))))
         (result (+ (ubyte64-fix pc) offset))
         (stat (write64-xreg rd result stat))
         (stat (inc64-pc stat)))
      stat)))

Theorem: state64p-of-exec64-auipc

(defthm state64p-of-exec64-auipc
  (b* ((new-stat (exec64-auipc rd imm pc stat)))
    (state64p new-stat))
  :rule-classes :rewrite)

Theorem: exec64-auipc-of-ubyte5-fix-rd

(defthm exec64-auipc-of-ubyte5-fix-rd
  (equal (exec64-auipc (ubyte5-fix rd)
                       imm pc stat)
         (exec64-auipc rd imm pc stat)))

Theorem: exec64-auipc-ubyte5-equiv-congruence-on-rd

(defthm exec64-auipc-ubyte5-equiv-congruence-on-rd
  (implies (ubyte5-equiv rd rd-equiv)
           (equal (exec64-auipc rd imm pc stat)
                  (exec64-auipc rd-equiv imm pc stat)))
  :rule-classes :congruence)

Theorem: exec64-auipc-of-ubyte20-fix-imm

(defthm exec64-auipc-of-ubyte20-fix-imm
  (equal (exec64-auipc rd (ubyte20-fix imm)
                       pc stat)
         (exec64-auipc rd imm pc stat)))

Theorem: exec64-auipc-ubyte20-equiv-congruence-on-imm

(defthm exec64-auipc-ubyte20-equiv-congruence-on-imm
  (implies (acl2::ubyte20-equiv imm imm-equiv)
           (equal (exec64-auipc rd imm pc stat)
                  (exec64-auipc rd imm-equiv pc stat)))
  :rule-classes :congruence)

Theorem: exec64-auipc-of-ubyte64-fix-pc

(defthm exec64-auipc-of-ubyte64-fix-pc
  (equal (exec64-auipc rd imm (ubyte64-fix pc)
                       stat)
         (exec64-auipc rd imm pc stat)))

Theorem: exec64-auipc-ubyte64-equiv-congruence-on-pc

(defthm exec64-auipc-ubyte64-equiv-congruence-on-pc
  (implies (acl2::ubyte64-equiv pc pc-equiv)
           (equal (exec64-auipc rd imm pc stat)
                  (exec64-auipc rd imm pc-equiv stat)))
  :rule-classes :congruence)

Theorem: exec64-auipc-of-state64-fix-stat

(defthm exec64-auipc-of-state64-fix-stat
  (equal (exec64-auipc rd imm pc (state64-fix stat))
         (exec64-auipc rd imm pc stat)))

Theorem: exec64-auipc-state64-equiv-congruence-on-stat

(defthm exec64-auipc-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (exec64-auipc rd imm pc stat)
                  (exec64-auipc rd imm pc stat-equiv)))
  :rule-classes :congruence)