Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Program-execution
Introduction
X86isa-build-instructions
Publications
Contributors
Machine
Syscalls
Cpuid
X86isa-state
Linear-memory
Rflag-specifications
Characterizing-undefined-behavior
Top-level-memory
App-view
X86-decoder
Physical-memory
Decoding-and-spec-utils
Instructions
X86-modes
Register-readers-and-writers
Segmentation
Other-non-deterministic-computations
Environment
Components-of-the-environment-field
Reading-memory-as-strings-or-bytes
Converting-between-strings-and-bytes
Writing-strings-or-bytes-to-memory
Paging
Implemented-opcodes
Proof-utilities
To-do
Concrete-simulation-examples
Model-validation
Utils
Debugging-code-proofs
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Machine
Environment
Defining the environment field for reasoning about non-deterministic computations
Subtopics
Components-of-the-environment-field
Reading-memory-as-strings-or-bytes
Converting-between-strings-and-bytes
Writing-strings-or-bytes-to-memory