• 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
          • Semantics
            • Exec-bltu
              • Exec-blt
              • Exec-bgeu
              • Exec-bge
              • Exec-jalr
              • Exec-bne
              • Exec-beq
              • Exec-sra
              • Exec-op
              • Exec-srl
              • Exec-op-imms-32
              • Exec-op-32
              • Exec-srlw
              • Exec-sraw
              • Exec-sll
              • Exec-remuw
              • Exec-op-imms64
              • Exec-op-imms32
              • Exec-op-imm-32
              • Exec-branch
              • Exec-addi
              • Exec-srliw
              • Exec-sraiw
              • Exec-sltiu
              • Exec-remw
              • Exec-op-imm
              • Exec-load
              • Exec-jal
              • Exec-divuw
              • Exec-sub
              • Exec-store
              • Exec-srli64
              • Exec-srli32
              • Exec-srai64
              • Exec-srai32
              • Exec-sllw
              • Exec-remu
              • Exec-divw
              • Exec-addiw
              • Exec-xori
              • Exec-slti
              • Exec-slliw
              • Exec-rem
              • Exec-ori
              • Exec-mulhsu
              • Exec-divu
              • Exec-andi
              • Exec-add
              • Exec-sw
              • Exec-sltu
              • Exec-slt
              • Exec-slli64
              • Exec-slli32
              • Exec-mulhu
              • Exec-div
              • Exec-auipc
              • Exec-addw
              • Exec-mulw
              • Exec-mulh
              • Exec-lwu
              • Exec-xor
              • Exec-subw
              • Exec-or
              • Exec-lhu
              • Exec-lbu
              • Exec-and
              • Exec-sd
              • Exec-mul
              • Exec-lh
              • Exec-ld
              • Exec-lb
              • Exec-sh
              • Exec-sb
              • Exec-lw
              • Exec-lui
              • Eff-addr
              • Exec-instr
            • Features
            • States
            • Instructions
            • Encoding
            • Reads-over-writes
            • Execution
            • Decoding
          • Executable
          • Specialized
        • 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
    • Semantics

    Exec-bltu

    Semantics of the BLTU instruction [ISA:2.5.2].

    Signature
    (exec-bltu rs1 rs2 imm pc stat feat) → new-stat
    Arguments
    rs1 — Guard (ubyte5p rs1).
    rs2 — Guard (ubyte5p rs2).
    imm — Guard (ubyte12p imm).
    stat — Guard (statp stat).
    feat — Guard (featp feat).
    Returns
    new-stat — Type (statp new-stat).

    We read two unsigned XLEN-bit integers from rs1 and rs2. We use the 12 bits of the immediate as the high bits of a 13-bit integer, whose low bit is 0 (i.e. the immediate measures multiples of 2); the unsigned 13-bit integer is sign-extended to XLEN bits, obtaining an offset. We add the offset to the address of the instruction, which is passed as the pc input to this function; this is the branch target. We compare the two unsigned integers from the registers: if the first one is less than the second one, we write the branch target to the program counter; otherwise, we increment the program counter.

    Definitions and Theorems

    Function: exec-bltu

    (defun exec-bltu (rs1 rs2 imm pc stat feat)
      (declare (xargs :guard (and (ubyte5p rs1)
                                  (ubyte5p rs2)
                                  (ubyte12p imm)
                                  (statp stat)
                                  (featp feat))))
      (declare (xargs :guard (and (stat-validp stat feat)
                                  (cond ((feat-32p feat) (ubyte32p pc))
                                        ((feat-64p feat) (ubyte64p pc))
                                        (t (impossible)))
                                  (< (lnfix rs1) (feat->xnum feat))
                                  (< (lnfix rs2) (feat->xnum feat)))))
      (let ((__function__ 'exec-bltu))
        (declare (ignorable __function__))
        (b* ((rs1-operand (read-xreg-unsigned (ubyte5-fix rs1)
                                              stat feat))
             (rs2-operand (read-xreg-unsigned (ubyte5-fix rs2)
                                              stat feat))
             (offset (loghead (feat->xlen feat)
                              (logext 13 (ash (ubyte12-fix imm) 1))))
             (target-pc (+ pc offset))
             (stat (if (< rs1-operand rs2-operand)
                       (write-pc target-pc stat feat)
                     (inc4-pc stat feat))))
          stat)))

    Theorem: statp-of-exec-bltu

    (defthm statp-of-exec-bltu
      (b* ((new-stat (exec-bltu rs1 rs2 imm pc stat feat)))
        (statp new-stat))
      :rule-classes :rewrite)

    Theorem: stat-validp-of-exec-bltu

    (defthm stat-validp-of-exec-bltu
      (implies (stat-validp stat feat)
               (b* ((?new-stat (exec-bltu rs1 rs2 imm pc stat feat)))
                 (stat-validp new-stat feat))))

    Theorem: exec-bltu-of-ubyte5-fix-rs1

    (defthm exec-bltu-of-ubyte5-fix-rs1
      (equal (exec-bltu (ubyte5-fix rs1)
                        rs2 imm pc stat feat)
             (exec-bltu rs1 rs2 imm pc stat feat)))

    Theorem: exec-bltu-ubyte5-equiv-congruence-on-rs1

    (defthm exec-bltu-ubyte5-equiv-congruence-on-rs1
      (implies (ubyte5-equiv rs1 rs1-equiv)
               (equal (exec-bltu rs1 rs2 imm pc stat feat)
                      (exec-bltu rs1-equiv rs2 imm pc stat feat)))
      :rule-classes :congruence)

    Theorem: exec-bltu-of-ubyte5-fix-rs2

    (defthm exec-bltu-of-ubyte5-fix-rs2
      (equal (exec-bltu rs1 (ubyte5-fix rs2)
                        imm pc stat feat)
             (exec-bltu rs1 rs2 imm pc stat feat)))

    Theorem: exec-bltu-ubyte5-equiv-congruence-on-rs2

    (defthm exec-bltu-ubyte5-equiv-congruence-on-rs2
      (implies (ubyte5-equiv rs2 rs2-equiv)
               (equal (exec-bltu rs1 rs2 imm pc stat feat)
                      (exec-bltu rs1 rs2-equiv imm pc stat feat)))
      :rule-classes :congruence)

    Theorem: exec-bltu-of-ubyte12-fix-imm

    (defthm exec-bltu-of-ubyte12-fix-imm
      (equal (exec-bltu rs1 rs2 (ubyte12-fix imm)
                        pc stat feat)
             (exec-bltu rs1 rs2 imm pc stat feat)))

    Theorem: exec-bltu-ubyte12-equiv-congruence-on-imm

    (defthm exec-bltu-ubyte12-equiv-congruence-on-imm
      (implies (acl2::ubyte12-equiv imm imm-equiv)
               (equal (exec-bltu rs1 rs2 imm pc stat feat)
                      (exec-bltu rs1 rs2 imm-equiv pc stat feat)))
      :rule-classes :congruence)

    Theorem: exec-bltu-of-stat-fix-stat

    (defthm exec-bltu-of-stat-fix-stat
      (equal (exec-bltu rs1 rs2 imm pc (stat-fix stat)
                        feat)
             (exec-bltu rs1 rs2 imm pc stat feat)))

    Theorem: exec-bltu-stat-equiv-congruence-on-stat

    (defthm exec-bltu-stat-equiv-congruence-on-stat
      (implies (stat-equiv stat stat-equiv)
               (equal (exec-bltu rs1 rs2 imm pc stat feat)
                      (exec-bltu rs1 rs2 imm pc stat-equiv feat)))
      :rule-classes :congruence)

    Theorem: exec-bltu-of-feat-fix-feat

    (defthm exec-bltu-of-feat-fix-feat
      (equal (exec-bltu rs1 rs2 imm pc stat (feat-fix feat))
             (exec-bltu rs1 rs2 imm pc stat feat)))

    Theorem: exec-bltu-feat-equiv-congruence-on-feat

    (defthm exec-bltu-feat-equiv-congruence-on-feat
      (implies (feat-equiv feat feat-equiv)
               (equal (exec-bltu rs1 rs2 imm pc stat feat)
                      (exec-bltu rs1 rs2 imm pc stat feat-equiv)))
      :rule-classes :congruence)