Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Community
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Fty-extensions
Isar
Kestrel-utilities
Set
Soft
C
Bv
Imp-language
Event-macros
Java
Riscv
Specification
Semantics
Features
Instructions
Instr
Instrp
Instr-fix
Instr-case
Instr-store
Instr-op-imms64
Instr-op-imms32
Instr-op-imms-32
Instr-op-imm-32
Instr-op-imm
Instr-op-32
Instr-op
Instr-load
Instr-branch
Make-instr-branch
Instr-branch->funct
Instr-branch->rs2
Instr-branch->rs1
Instr-branch->imm
Change-instr-branch
Instr-equiv
Instr-jalr
Instr-lui
Instr-jal
Instr-auipc
Instr-kind
Op-funct
Op-32-funct
Op-imm-funct
Load-funct
Instr-validp
Branch-funct
Op-imms-funct
Store-funct
Op-imms-32-funct
Instr-option
Op-imm-32-funct
Encoding
States
Reads-over-writes
Semantics-equivalences
Decoding
Execution
Executable
Specialized
Optimized
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Cryptography
Number-theory
Lists-light
Axe
Builtins
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Instr
Instr-branch
This is a product type, introduced by
fty::deftagsum
in support of
instr
.
Fields
funct —
branch-funct
rs1 —
ubyte5
rs2 —
ubyte5
imm —
ubyte12
Subtopics
Make-instr-branch
Basic constructor macro for
instr-branch
structures.
Instr-branch->funct
Get the
funct
field from a
instr-branch
.
Instr-branch->rs2
Get the
rs2
field from a
instr-branch
.
Instr-branch->rs1
Get the
rs1
field from a
instr-branch
.
Instr-branch->imm
Get the
imm
field from a
instr-branch
.
Change-instr-branch
Modifying constructor for
instr-branch
structures.