• 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-lb

    Semantics of the LB instruction [ISA:2.6].

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

    We calculate the effective address. We read an unsigned 8-bit integer from the effective address, and sign-extend it to XLEN bits. We write the result to rd. We increment the program counter.

    Definitions and Theorems

    Function: exec-lb

    (defun exec-lb (rd rs1 imm stat feat)
     (declare (xargs :guard (and (ubyte5p rd)
                                 (ubyte5p rs1)
                                 (ubyte12p imm)
                                 (statp stat)
                                 (featp feat))))
     (declare (xargs :guard (and (stat-validp stat feat)
                                 (< (lnfix rd) (feat->xnum feat))
                                 (< (lnfix rs1) (feat->xnum feat)))))
     (let ((__function__ 'exec-lb))
       (declare (ignorable __function__))
       (b*
        ((addr (eff-addr rs1 imm stat feat))
         (result
              (loghead (feat->xlen feat)
                       (logext 8
                               (read-memory-unsigned8 addr stat feat))))
         (stat (write-xreg (ubyte5-fix rd)
                           result stat feat))
         (stat (inc4-pc stat feat)))
        stat)))

    Theorem: statp-of-exec-lb

    (defthm statp-of-exec-lb
      (b* ((new-stat (exec-lb rd rs1 imm stat feat)))
        (statp new-stat))
      :rule-classes :rewrite)

    Theorem: stat-validp-of-exec-lb

    (defthm stat-validp-of-exec-lb
      (implies (and (stat-validp stat feat)
                    (< (lnfix rd) (feat->xnum feat)))
               (b* ((?new-stat (exec-lb rd rs1 imm stat feat)))
                 (stat-validp new-stat feat))))

    Theorem: exec-lb-of-ubyte5-fix-rd

    (defthm exec-lb-of-ubyte5-fix-rd
      (equal (exec-lb (ubyte5-fix rd)
                      rs1 imm stat feat)
             (exec-lb rd rs1 imm stat feat)))

    Theorem: exec-lb-ubyte5-equiv-congruence-on-rd

    (defthm exec-lb-ubyte5-equiv-congruence-on-rd
      (implies (ubyte5-equiv rd rd-equiv)
               (equal (exec-lb rd rs1 imm stat feat)
                      (exec-lb rd-equiv rs1 imm stat feat)))
      :rule-classes :congruence)

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

    (defthm exec-lb-of-ubyte5-fix-rs1
      (equal (exec-lb rd (ubyte5-fix rs1)
                      imm stat feat)
             (exec-lb rd rs1 imm stat feat)))

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

    (defthm exec-lb-ubyte5-equiv-congruence-on-rs1
      (implies (ubyte5-equiv rs1 rs1-equiv)
               (equal (exec-lb rd rs1 imm stat feat)
                      (exec-lb rd rs1-equiv imm stat feat)))
      :rule-classes :congruence)

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

    (defthm exec-lb-of-ubyte12-fix-imm
      (equal (exec-lb rd rs1 (ubyte12-fix imm)
                      stat feat)
             (exec-lb rd rs1 imm stat feat)))

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

    (defthm exec-lb-ubyte12-equiv-congruence-on-imm
      (implies (acl2::ubyte12-equiv imm imm-equiv)
               (equal (exec-lb rd rs1 imm stat feat)
                      (exec-lb rd rs1 imm-equiv stat feat)))
      :rule-classes :congruence)

    Theorem: exec-lb-of-stat-fix-stat

    (defthm exec-lb-of-stat-fix-stat
      (equal (exec-lb rd rs1 imm (stat-fix stat)
                      feat)
             (exec-lb rd rs1 imm stat feat)))

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

    (defthm exec-lb-stat-equiv-congruence-on-stat
      (implies (stat-equiv stat stat-equiv)
               (equal (exec-lb rd rs1 imm stat feat)
                      (exec-lb rd rs1 imm stat-equiv feat)))
      :rule-classes :congruence)

    Theorem: exec-lb-of-feat-fix-feat

    (defthm exec-lb-of-feat-fix-feat
      (equal (exec-lb rd rs1 imm stat (feat-fix feat))
             (exec-lb rd rs1 imm stat feat)))

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

    (defthm exec-lb-feat-equiv-congruence-on-feat
      (implies (feat-equiv feat feat-equiv)
               (equal (exec-lb rd rs1 imm stat feat)
                      (exec-lb rd rs1 imm stat feat-equiv)))
      :rule-classes :congruence)