• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
      • Std/lists
      • Omaps
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
        • Maybe-stringp
        • Maybe-natp
        • Two-nats-measure
        • Impossible
        • Bytep
          • Byte
          • Bytes-as-digits-in-base-256
            • Bebytes=>nat
            • Lebytes=>nat
            • Nat=>bebytes
            • Nat=>lebytes
            • Nat=>bebytes*
            • Nat=>lebytes*
            • Nat=>lebytes+
            • Nat=>bebytes+
            • Bits/bytes-digit-grouping
          • Bytep-additional-theorems
        • Nat-list-measure
        • Maybe-posp
        • Nibblep
        • Organize-symbols-by-pkg
        • Organize-symbols-by-name
        • Lnfix
        • Good-valuep
        • Streqv
        • Chareqv
        • Symbol-package-name-non-cl
        • Arith-equivs
        • Induction-schemes
        • Maybe-integerp
        • Char-fix
        • Pos-fix
        • Symbol-package-name-lst
        • Mbt$
        • Maybe-bitp
        • Good-pseudo-termp
        • Str-fix
        • Maybe-string-fix
        • Nonkeyword-listp
        • Lifix
        • Bfix
        • Std/basic/if*
        • Impliez
        • Tuplep
        • Std/basic/intern-in-package-of-symbol
        • Lbfix
        • Std/basic/symbol-name-lst
        • True
        • Std/basic/rfix
        • Std/basic/realfix
        • Std/basic/member-symbol-name
        • Std/basic/fix
        • False
        • Std/basic/nfix
        • Std/basic/ifix
      • Std/system
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Kestrel-utilities
  • Bytep

Bytes-as-digits-in-base-256

Specialized versions of the operations to convert between natural numbers and digits that use bytes as digits, in base 256.

Subtopics

Bebytes=>nat
Convert a big-endian list of bytes, seen as digits in base 256, to their value.
Lebytes=>nat
Convert a little-endian list of bytes, seen as digits in base 256, to their value.
Nat=>bebytes
Convert a natural number to its big-endian list of bytes, seen as digits in base 256, of specified length.
Nat=>lebytes
Convert a natural number to its little-endian list of bytes, seen as digits in base 256, of specified length.
Nat=>bebytes*
Convert a natural number to its minimum-length big-endian list of bytes, seen as sigits in base 256.
Nat=>lebytes*
Convert a natural number to its minimum-length little-endian list of bytes, seen as sigits in base 256.
Nat=>lebytes+
Convert a natural number to its non-empty minimum-length little-endian list of bytes, seen as sigits in base 256.
Nat=>bebytes+
Convert a natural number to its non-empty minimum-length big-endian list of bytes, seen as sigits in base 256.
Bits/bytes-digit-grouping
Specialized versions of the operations to group and ungroup digitsthat are bits (base 2) and bytes (base 256).