• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Error-checking
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
        • Schemalg
        • Expdata
        • Restrict
        • Casesplit
        • Simplify-term
        • Simplify-defun-sk
        • Parteval
        • Solve
        • Propagate-iso
        • Simplify
        • Wrap-output
        • Finite-difference
        • Drop-irrelevant-params
        • Copy-function
        • Rename-params
        • Utilities
        • Simplify-term-programmatic
        • Simplify-defun-sk-programmatic
        • Simplify-defun-programmatic
        • Simplify-defun+
        • Common-options
          • Untranslate-specifier
          • Print-specifier
          • Hints-specifier
            • Ensure-is-hints-specifier
              • Ensure-is-hints-specifier$
            • Canonical-hints-specifier-p
            • Canonicalize-hints-specifier
            • Hints-specifier-p
        • Common-concepts
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Prime-field-constraint-systems
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Java
      • C
      • Syntheto
      • Number-theory
      • Cryptography
      • Lists-light
      • File-io-light
      • Json
      • Built-ins
      • Solidity
      • Axe
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Hints-specifier
• Error-checking

Ensure-is-hints-specifier

Cause an error if a value is not a hints specifier.

Signature

(ensure-is-hints-specifier x legal-kwds description 
                           error-erp error-val ctx state) 
 
  → 
(mv erp val state)

Arguments

x — Value to check.

legal-kwds — Guard (and (keyword-listp legal-kwds) (no-duplicatesp-eq legal-kwds)).

description — Guard (msgp description).

error-erp — Flag to return in case of error.

error-val — Value to return in case of error.

ctx — Context for errors.

Returns

erp — Type (implies erp (equal erp error-erp)).

val — Type (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (canonical-hints-specifier-p val legal-kwds))) , given the guard.

Definitions and Theorems

Function: ensure-is-hints-specifier

(defun
 ensure-is-hints-specifier
 (x legal-kwds description
    error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (and (keyword-listp legal-kwds)
                                  (no-duplicatesp-eq legal-kwds))
                             (msgp description))))
 (b*
  (((unless (hints-specifier-p x legal-kwds))
    (er-soft+
     ctx error-erp error-val
     "~@0 must be an APT hints specifier.  See :DOC APT::HINTS-SPECIFIER."
     description)))
  (value (canonicalize-hints-specifier x legal-kwds))))

Theorem: return-type-of-ensure-is-hints-specifier.erp

(defthm
   return-type-of-ensure-is-hints-specifier.erp
   (b* (((mv ?erp ?val acl2::?state)
         (ensure-is-hints-specifier x legal-kwds description
                                    error-erp error-val ctx state)))
       (implies erp (equal erp error-erp)))
   :rule-classes :rewrite)

Theorem: return-type-of-ensure-is-hints-specifier.val

(defthm
 return-type-of-ensure-is-hints-specifier.val
 (implies
  (and
   (state-p state)
   (if
    (keyword-listp legal-kwds)
    ((lambda
        (acl2::x)
        (return-last
             'acl2::mbe1-raw
             (acl2::no-duplicatesp-eq-exec acl2::x)
             (return-last
                  'progn
                  (acl2::no-duplicatesp-eq-exec$guard-check acl2::x)
                  (no-duplicatesp-equal acl2::x))))
     legal-kwds)
    'nil)
   (msgp description))
  (b* (((mv ?erp ?val acl2::?state)
        (ensure-is-hints-specifier x legal-kwds description
                                   error-erp error-val ctx state)))
      (and (implies erp (equal val error-val))
           (implies (and (not erp) error-erp)
                    (canonical-hints-specifier-p val legal-kwds)))))
 :rule-classes :rewrite)

Subtopics

Ensure-is-hints-specifier$

Calls ensure-is-hints-specifier with ctx and state as the last two arguments.