• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
          • Omaps
          • Directed-untranslate
          • Include-book-paths
          • Ubi
          • Numbered-names
          • Digits-any-base
            • Defdigits
              • Defdigits-implementation
            • Nat=>lendian*
            • Group-lendian
            • Defdigit-grouping
            • Ungroup-lendian
            • Lendian=>nat
            • Defthm-dab-return-types
            • Bendian=>nat
            • Nat=>bendian*
            • Trim-bendian*
            • Trim-lendian*
            • Nat=>lendian
            • Dab-digit-list-fix
            • Nat=>bendian
            • Ungroup-bendian
            • Group-bendian
            • Digits=>nat-injectivity-theorems
            • Dab-digit-listp
            • Nat=>lendian+
            • Dab-basep
            • Nat=>bendian+
            • Digits=>nat=>digits-inverses-theorems
            • Trim-lendian+
            • Trim-bendian+
            • Nat=>digits=>nat-inverses-theorems
            • Dab-digitp
            • Group/ungroup-inverses-theorems
            • Dab-digit-fix
            • Nat=>digits-injectivity-theorems
            • Dab-base
            • Digits-any-base-pow2
            • Dab-base-fix
          • Context-message-pair
          • With-auto-termination
          • Make-termination-theorem
          • Theorems-about-true-list-lists
          • Checkpoint-list
          • Sublis-expr+
          • Integers-from-to
          • Prove$
          • Defthm<w
          • System-utilities-non-built-in
          • Integer-range-fix
          • Minimize-ruler-extenders
          • Add-const-to-untranslate-preprocess
          • Unsigned-byte-fix
          • Signed-byte-fix
          • Defthmr
          • Paired-names
          • Unsigned-byte-list-fix
          • Signed-byte-list-fix
          • Show-books
          • Skip-in-book
          • Typed-tuplep
          • List-utilities
          • Checkpoint-list-pretty
          • Defunt
          • Keyword-value-list-to-alist
          • Magic-macroexpand
          • Top-command-number-fn
          • Bits-as-digits-in-base-2
          • Show-checkpoint-list
          • Ubyte11s-as-digits-in-base-2048
          • Named-formulas
          • Bytes-as-digits-in-base-256
          • String-utilities
          • Make-keyword-value-list-from-keys-and-value
          • Defmacroq
          • Integer-range-listp
          • Apply-fn-if-known
          • Trans-eval-error-triple
          • Checkpoint-info-list
          • Previous-subsumer-hints
          • Fms!-lst
          • Zp-listp
          • Trans-eval-state
          • Injections
          • Doublets-to-alist
          • Theorems-about-osets
          • Typed-list-utilities
          • Book-runes-alist
          • User-interface
          • Bits/ubyte11s-digit-grouping
          • Bits/bytes-digit-grouping
          • Message-utilities
          • Subsetp-eq-linear
          • Oset-utilities
          • Strict-merge-sort-<
          • Miscellaneous-enumerations
          • Maybe-unquote
          • Thm<w
          • Defthmd<w
          • Io-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • 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
  • Digits-any-base

Defdigits

Generate specialized versions of the operations to convert between natural numbers and digits, using specified existing recognizers and fixers for the digits.

Introduction

The operations in the library to convert between natural numbers and digits are parameterized over the base. The recognizers and fixers for (lists of) digits are also parameterized; they are binary functions.

Given a specific base, and specific unary recognizers and fixers for lists of digits in that base, it is possible to generate systematically versions of the operations in the library, and accompanying theorems, that are specialized to the base (and thus are not parameterized over it) and that depend on those unary recognizers and fixers. This macro carries out this specialization.

These specialized operations, in combination with the unary recognizers and fixers, are easier to use and reason about than the general operations, when the base is known.

General Form

(defdigits name
           :base ...
           :digit-pred ...
           :digit-fix ...
           :digits-pred ...
           :digits-fix ...
           :bendian-to-nat ...
           :lendian-to-nat ...
           :nat-to-bendian ...
           :nat-to-lendian ...
           :digit-pred-hints ...
           :digit-fix-hints ...
           :digit-pred-guard-hints ...
           :digit-fix-guard-hints ...
           :digits-pred-hints ...
           :digits-fix-hints ...
           :digits-pred-guard-hints ...
           :digits-fix-guard-hints ...
           :digits-description ...
           :parents ...
           :short ...
           :long ...
  )

Inputs

name

A symbol that names the ensemble of the generated specialized conversion functions. This is used as the XDOC topic under which the XDOC topics for the generated events are put.

:base

A positive integer greater than 1 that specifies the base.

:digit-pred
:digit-fix

Symbols that name existing functions, or macros for inline functions, to be used as specializations of dab-digitp and dab-digit-fix.

These must be part of an existing fixtype.

:digits-pred
:digits-fix

Symbols that name existing functions, or macros for inline functions, to be used as specializations of dab-digit-listp and dab-digit-list-fix.

These must be part of an existing fixtype.

:bendian-to-nat
:lendian-to-nat
:nat-to-bendian
:nat-to-lendian

Symbols that specify the names to use for the generated functions (see details below).

:digit-pred-hints
:digit-fix-hints
:digit-pred-guard-hints
:digit-fix-guard-hints
:digits-pred-hints
:digits-fix-hints
:digits-pred-guard-hints
:digits-fix-guard-hints

Hints to prove that the specialized recognizers and fixers are equivalent to the general ones, when their base argument is base. Besides the equalities of the functions, the guard of the recognizer must be equivalent to t, and the guard of the fixer must include the recognizer.

:digits-description

A string describing the values in digits-pred, used in the generated documentation. It must start with a lowercase character (because it is inserted in the middle of generated senteces) and it must be plural (so that the generated sentences are grammatically correct).

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the ensemble of the generated specialized conversion functions.

Generated Events

digit-pred-correct
digit-fix-correct

Two rewrite rules, disabled by default, that equate digit-pred and digit-fix with dab-digitp and dab-digit-fix applied to the specified base.

digit-pred-guard-correct

digit-fix-guard-correct

Two theorems, without rule classes, asserting that the guard of digit-pred is equivalent to t and that the guard of digit-fix includes digit-pred.

digits-pred-correct
digits-fix-correct

Two rewrite rules, disabled by default, that equate digits-pred and digits-fix with dab-digit-listp and dab-digit-list-fix applied to the specified base.

digits-pred-guard-correct

digits-fix-guard-correct

Two theorems, without rule classes, asserting that the guard of digits-pred is equivalent to t and that the guard of digits-fix includes digits-pred.

bendian-to-nat
lendian-to-nat
nat-to-bendian
nat-to-lendian
nat-to-bendian*
nat-to-lendian*
nat-to-bendian+
nat-to-lendian+

Specialized versions of bendian=>nat, lendian=>nat, nat=>bendian, nat=>lendian, nat=>bendian*, nat=>lendian*, nat=>bendian+, and nat=>lendian+, for the specified base. The names of the first four are as specified by the respective inputs; the names for the second four are obtained by adding * or + after the names of the third and fourth function. These new functions are accompanied by several theorems corresponding to ones that accompany the original functions, i.e. they are specialized versions of the general theorems; we also generate some theory invariants that prevent some of the generated rewrite rules from being simultaneously enabled. These theorems, and the guards, use digit-pred, digit-fix, digits-pred, and digits-fix instead of dab-digitp, dab-digit-fix, dab-digit-listp, and dab-digit-list-fix. The generated theorems can be seen in the implementation, which uses a readable backquote notation; they can also be seen in the generated XDOC.

The generated events include XDOC documentation. They are all under an XDOC for the ensemble, whose name is specified in the name input.

Subtopics

Defdigits-implementation
Implementation of defdigits.