• 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
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
          • Atc-implementation
            • Atc-abstract-syntax
            • Atc-pretty-printer
            • Atc-event-and-code-generation
            • Fty-pseudo-term-utilities
            • Atc-term-recognizers
            • Atc-input-processing
              • Atc-process-target
              • Atc-process-const-name
              • Atc-process-function
              • Atc-process-target-list
              • Atc-process-inputs
              • Atc-process-file-name
              • Atc-process-const-name-aux
              • Atc-process-targets
              • Atc-process-print
              • Atc-process-pretty-printing
              • Atc-remove-called-fns
              • Atc-process-output-dir
              • Atc-process-proofs
              • Atc-process-header
              • *atc-allowed-pretty-printing-options*
              • *atc-allowed-options*
            • Atc-shallow-embedding
            • Atc-process-inputs-and-gen-everything
            • Atc-table
            • Atc-fn
            • Atc-pretty-printing-options
            • Atc-types
            • Atc-macro-definition
          • Atc-tutorial
        • Language
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Atc-input-processing

Atc-process-const-name

Process the :const-name input.

Signature

(atc-process-const-name options target-fns wrld) 
  → 
(mv erp prog-const wf-thm fn-thms fn-limits fn-body-limits)

Arguments

options — Guard (symbol-alistp options).

target-fns — Guard (symbol-listp target-fns).

wrld — Guard (plist-worldp wrld).

Returns

prog-const — Type (symbolp prog-const).

wf-thm — Type (symbolp wf-thm).

fn-thms — Type (symbol-symbol-alistp fn-thms), given (symbol-listp target-fns).

fn-limits — Type (symbol-symbol-alistp fn-limits), given (symbol-listp target-fns).

fn-body-limits — Type (symbol-symbol-alistp fn-body-limits), given (symbol-listp target-fns).

Since this input also determines, indirectly, the names of the theorems generated and exported by ATC, here we also calculate the names of those theorems, ensure they are fresh, and return them for use in event generation. More precisely, we return the name of the program well-formedness theorem and the names of the function correctness theorems; the latter are returned as an alist from the target functions to the respective theorem names.

The name of each theorem is obtained by appending something to the name of the constant. The thing appended differs across the theorems: thus, their names are all distinct by construction.

Besides the names of the generated theorems, we also return the names of the soon-to-be-generated limit functions. There will be one limit function for each target function, whose name is obtained by adding -limit after the constant name and the target function name: this will express a limit sufficient to execute the target function. There will be also an additional limit function for each recursive target function, whose name is obtained by adding -body-limit after the constant name and the target function name; this will express a limit sufficient to run any instance of the loop body.

Definitions and Theorems

Function: atc-process-const-name-aux

(defun atc-process-const-name-aux (target-fns prog-const wrld)
 (declare (xargs :guard (and (symbol-listp target-fns)
                             (symbolp prog-const)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-process-const-name-aux))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil)
    ((when (endp target-fns))
     (retok nil nil nil))
    (fn (car target-fns))
    (fn-thm (packn (list prog-const "-" (symbol-name fn)
                         "-CORRECT")))
    (msg? (acl2::fresh-namep-msg-weak fn-thm nil wrld))
    ((when msg?)
     (reterr
      (msg
       "The generated theorem name ~x0 ~
                         for the correctness theorem of the function ~x1 ~
                         is invalid: ~@2"
       fn-thm fn msg?)))
    ((erp fn-thms fn-limits fn-body-limits)
     (atc-process-const-name-aux (cdr target-fns)
                                 prog-const wrld))
    (fn-limit (packn (list prog-const "-" (symbol-name fn)
                           "-LIMIT")))
    (msg? (acl2::fresh-namep-msg-weak fn-limit 'function
                                      wrld))
    ((when msg?)
     (reterr
      (msg
       "The generated function name ~x0 ~
                         for the limit of the function ~x1 ~
                         is invalid: ~@2"
       fn-limit fn msg?)))
    ((when (not (irecursivep+ fn wrld)))
     (retok (acons fn fn-thm fn-thms)
            (acons fn fn-limit fn-limits)
            fn-body-limits))
    (fn-body-limit (packn (list prog-const "-" (symbol-name fn)
                                "-BODY-LIMIT")))
    (msg? (acl2::fresh-namep-msg-weak fn-body-limit 'function
                                      wrld))
    ((when msg?)
     (reterr
      (msg
       "The generated function name ~x0 ~
                         for the body limit of the function ~x1 ~
                         is invalid: ~@2"
       fn-body-limit fn msg?))))
   (retok (acons fn fn-thm fn-thms)
          (acons fn fn-limit fn-limits)
          (acons fn fn-body-limit fn-body-limits)))))

Theorem: symbol-symbol-alistp-of-atc-process-const-name-aux.fn-thms

(defthm symbol-symbol-alistp-of-atc-process-const-name-aux.fn-thms
 (implies
     (symbol-listp target-fns)
     (b* (((mv acl2::?erp
               ?fn-thms ?fn-limits ?fn-body-limits)
           (atc-process-const-name-aux target-fns prog-const wrld)))
       (symbol-symbol-alistp fn-thms)))
 :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-process-const-name-aux.fn-limits

(defthm symbol-symbol-alistp-of-atc-process-const-name-aux.fn-limits
 (implies
     (symbol-listp target-fns)
     (b* (((mv acl2::?erp
               ?fn-thms ?fn-limits ?fn-body-limits)
           (atc-process-const-name-aux target-fns prog-const wrld)))
       (symbol-symbol-alistp fn-limits)))
 :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-process-const-name-aux.fn-body-limits

(defthm
  symbol-symbol-alistp-of-atc-process-const-name-aux.fn-body-limits
 (implies
     (symbol-listp target-fns)
     (b* (((mv acl2::?erp
               ?fn-thms ?fn-limits ?fn-body-limits)
           (atc-process-const-name-aux target-fns prog-const wrld)))
       (symbol-symbol-alistp fn-body-limits)))
 :rule-classes :rewrite)

Function: atc-process-const-name

(defun atc-process-const-name (options target-fns wrld)
 (declare (xargs :guard (and (symbol-alistp options)
                             (symbol-listp target-fns)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-process-const-name))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil nil nil)
    (const-name-option (assoc-eq :const-name options))
    (const-name (if (consp const-name-option)
                    (cdr const-name-option)
                  :auto))
    ((unless (symbolp const-name))
     (reterr
      (msg
       "The :CONST-NAME input must be a symbol, ~
                      but ~x0 is not a symbol."
       const-name)))
    (prog-const (if (eq const-name :auto)
                    '*program*
                  const-name))
    (msg? (acl2::fresh-namep-msg-weak prog-const 'acl2::const
                                      wrld))
    ((when msg?)
     (reterr
      (msg
       "The constant name ~x0 ~
                      determined by the :CONST-NAME input ~x0 ~
                      is invalid: ~@2"
       prog-const const-name msg?)))
    (wf-thm (add-suffix prog-const "-WELL-FORMED"))
    (msg? (acl2::fresh-namep-msg-weak wf-thm nil wrld))
    ((when msg?)
     (reterr
      (msg
       "The generated theorem name ~x0 ~
                      for the well-formedness theorem is invalid: ~@1"
       wf-thm msg?)))
    ((erp fn-thms fn-limits fn-body-limits)
     (atc-process-const-name-aux target-fns prog-const wrld)))
   (retok prog-const wf-thm
          fn-thms fn-limits fn-body-limits))))

Theorem: symbolp-of-atc-process-const-name.prog-const

(defthm symbolp-of-atc-process-const-name.prog-const
  (b* (((mv acl2::?erp ?prog-const ?wf-thm
            ?fn-thms ?fn-limits ?fn-body-limits)
        (atc-process-const-name options target-fns wrld)))
    (symbolp prog-const))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-process-const-name.wf-thm

(defthm symbolp-of-atc-process-const-name.wf-thm
  (b* (((mv acl2::?erp ?prog-const ?wf-thm
            ?fn-thms ?fn-limits ?fn-body-limits)
        (atc-process-const-name options target-fns wrld)))
    (symbolp wf-thm))
  :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-process-const-name.fn-thms

(defthm symbol-symbol-alistp-of-atc-process-const-name.fn-thms
  (implies (symbol-listp target-fns)
           (b* (((mv acl2::?erp ?prog-const ?wf-thm
                     ?fn-thms ?fn-limits ?fn-body-limits)
                 (atc-process-const-name options target-fns wrld)))
             (symbol-symbol-alistp fn-thms)))
  :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-process-const-name.fn-limits

(defthm symbol-symbol-alistp-of-atc-process-const-name.fn-limits
  (implies (symbol-listp target-fns)
           (b* (((mv acl2::?erp ?prog-const ?wf-thm
                     ?fn-thms ?fn-limits ?fn-body-limits)
                 (atc-process-const-name options target-fns wrld)))
             (symbol-symbol-alistp fn-limits)))
  :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-process-const-name.fn-body-limits

(defthm
      symbol-symbol-alistp-of-atc-process-const-name.fn-body-limits
  (implies (symbol-listp target-fns)
           (b* (((mv acl2::?erp ?prog-const ?wf-thm
                     ?fn-thms ?fn-limits ?fn-body-limits)
                 (atc-process-const-name options target-fns wrld)))
             (symbol-symbol-alistp fn-body-limits)))
  :rule-classes :rewrite)