• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Riscv
        • Specification
        • Executable
        • Specialized
          • Rv64im
          • Rv32im
            • Semantics32
              • Exec32-bgeu
              • Exec32-bltu
              • Exec32-blt
              • Exec32-bge
              • Exec32-bne
              • Exec32-beq
              • Exec32-jalr
              • Exec32-branch
              • Exec32-jal
              • Exec32-op
              • Exec32-store
              • Exec32-op-imm
              • Exec32-load
              • Exec32-sra
              • Exec32-sltiu
              • Exec32-op-imms
              • Exec32-srl
              • Exec32-slti
              • Exec32-remu
              • Exec32-rem
              • Exec32-auipc
              • Exec32-xori
              • Exec32-srli
              • Exec32-srai
              • Exec32-ori
              • Exec32-divu
              • Exec32-andi
              • Exec32-addi
              • Exec32-sltu
              • Exec32-slt
              • Exec32-sll
              • Exec32-mulhsu
              • Exec32-lhu
              • Exec32-div
              • Exec32-xor
              • Exec32-slli
              • Exec32-sh
              • Exec32-mulhu
              • Exec32-mulh
              • Exec32-lh
              • Exec32-lbu
              • Exec32-sw
              • Exec32-sub
              • Exec32-sb
              • Exec32-or
              • Exec32-lw
              • Exec32-lb
              • Exec32-and
              • Exec32-mul
              • Exec32-add
              • Exec32-instr
              • Eff32-addr
              • Exec32-lui
              • States32
              • Execution32
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Semantics32

    Exec32-lui

    Semantics of the LUI instruction [ISA:2.4.1].

    Signature
    (exec32-lui rd imm stat) → new-stat
    Arguments
    rd — Guard (ubyte5p rd).
    imm — Guard (ubyte20p imm).
    stat — Guard (state32p stat).
    Returns
    new-stat — Type (state32p 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 write the integer to rd. We increment the program counter.

    Definitions and Theorems

    Function: exec32-lui

    (defun exec32-lui (rd imm stat)
      (declare (xargs :guard (and (ubyte5p rd)
                                  (ubyte20p imm)
                                  (state32p stat))))
      (let ((__function__ 'exec32-lui))
        (declare (ignorable __function__))
        (b* ((result (ash (ubyte20-fix imm) 12))
             (stat (write32-xreg rd result stat))
             (stat (inc32-pc stat)))
          stat)))

    Theorem: state32p-of-exec32-lui

    (defthm state32p-of-exec32-lui
      (b* ((new-stat (exec32-lui rd imm stat)))
        (state32p new-stat))
      :rule-classes :rewrite)

    Theorem: exec32-lui-of-ubyte5-fix-rd

    (defthm exec32-lui-of-ubyte5-fix-rd
      (equal (exec32-lui (ubyte5-fix rd) imm stat)
             (exec32-lui rd imm stat)))

    Theorem: exec32-lui-ubyte5-equiv-congruence-on-rd

    (defthm exec32-lui-ubyte5-equiv-congruence-on-rd
      (implies (ubyte5-equiv rd rd-equiv)
               (equal (exec32-lui rd imm stat)
                      (exec32-lui rd-equiv imm stat)))
      :rule-classes :congruence)

    Theorem: exec32-lui-of-ubyte20-fix-imm

    (defthm exec32-lui-of-ubyte20-fix-imm
      (equal (exec32-lui rd (ubyte20-fix imm) stat)
             (exec32-lui rd imm stat)))

    Theorem: exec32-lui-ubyte20-equiv-congruence-on-imm

    (defthm exec32-lui-ubyte20-equiv-congruence-on-imm
      (implies (acl2::ubyte20-equiv imm imm-equiv)
               (equal (exec32-lui rd imm stat)
                      (exec32-lui rd imm-equiv stat)))
      :rule-classes :congruence)

    Theorem: exec32-lui-of-state32-fix-stat

    (defthm exec32-lui-of-state32-fix-stat
      (equal (exec32-lui rd imm (state32-fix stat))
             (exec32-lui rd imm stat)))

    Theorem: exec32-lui-state32-equiv-congruence-on-stat

    (defthm exec32-lui-state32-equiv-congruence-on-stat
      (implies (state32-equiv stat stat-equiv)
               (equal (exec32-lui rd imm stat)
                      (exec32-lui rd imm stat-equiv)))
      :rule-classes :congruence)