• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • 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
      • Bigmems
        • Bigmem-asymmetric
        • Bigmem
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Projects

Bigmems

2^64-byte memory models that are logically a record.

The bigmems library implements multiple memory models with 2^64 bytes of space as abstract stobjs. These models use different techniques to lazily allocate the space as you use it. Logically they are equivalent, sharing the same logical definitions, but they may have different performance characteristics because they have different executable definitions.

If you're writing a book, you should use bigmem::bigmem. This stobj is "attachable," so users of your book can attach other bigmem implementations to it if they so chooose. See the topics for the individual bigmem implementations below for more information about particular memory models.

Subtopics

Bigmem-asymmetric
A 2^64-byte memory model that is logically a record but provides array-like performance for a fixed amount of emulated memory and slow(er) performance for the remaining (higher) memory locations.
Bigmem
A 2^64-byte memory model that is logically a record but provides array-like performance during execution