• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • 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
          • Segmentation
          • Register-readers-and-writers
          • Other-non-deterministic-computations
            • Hw_rnd_gen-logic
            • Hw_rnd_gen
            • Other-non-deterministic-computations-exec
            • Environment
            • Paging
          • Implemented-opcodes
          • Proof-utilities
          • To-do
          • Concrete-simulation-examples
          • Model-validation
          • Utils
          • Debugging-code-proofs
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • Other-non-deterministic-computations

    Other-non-deterministic-computations-exec

    Definitions of non-deterministic computations to be used for execution

    We smash the definition of hw_rnd_gen to provide random numbers during execution by using Lisp's random function.