• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
        • Transformations
          • Renaming-variables
          • Dead-code-eliminator
          • Renamings
          • Disambiguator
          • Unique-variables
          • Dead-code-eliminator-static-safety
          • No-function-definitions
            • Statements/blocks/cases/fundefs-nofunp
              • Fundef-nofunp
              • Statement-nofunp
              • Statement-list-nofunp
              • Block-option-nofunp
              • Block-nofunp
              • Swcase-list-nofunp
              • Swcase-nofunp
            • No-function-definitions-in-dynamic-semantics
            • Fundef-list-nofunp
            • Statements-to-fundefs-when-nofunp
          • Unique-functions
          • Renaming-functions
          • Dead-code-eliminator-no-loop-initializers
          • Dead-code-eliminator-no-function-definitions
          • No-loop-initializers
          • For-loop-init-rewriter
        • Language
        • Yul-json
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• No-function-definitions

Statements/blocks/cases/fundefs-nofunp

Mutually recursive functions that check the absence of function definitions in statements, blocks, cases, and function definitions.

Definitions and Theorems

Function: statement-nofunp

(defun statement-nofunp (stmt)
  (declare (xargs :guard (statementp stmt)))
  (let ((__function__ 'statement-nofunp))
    (declare (ignorable __function__))
    (statement-case stmt
                    :block (block-nofunp stmt.get)
                    :variable-single t
                    :variable-multi t
                    :assign-single t
                    :assign-multi t
                    :funcall t
                    :if (block-nofunp stmt.body)
                    :for (and (block-nofunp stmt.init)
                              (block-nofunp stmt.update)
                              (block-nofunp stmt.body))
                    :switch (and (swcase-list-nofunp stmt.cases)
                                 (block-option-nofunp stmt.default))
                    :leave t
                    :break t
                    :continue t
                    :fundef nil)))

Function: statement-list-nofunp

(defun statement-list-nofunp (stmts)
  (declare (xargs :guard (statement-listp stmts)))
  (let ((__function__ 'statement-list-nofunp))
    (declare (ignorable __function__))
    (or (endp stmts)
        (and (statement-nofunp (car stmts))
             (statement-list-nofunp (cdr stmts))))))

Function: block-nofunp

(defun block-nofunp (block)
  (declare (xargs :guard (blockp block)))
  (let ((__function__ 'block-nofunp))
    (declare (ignorable __function__))
    (statement-list-nofunp (block->statements block))))

Function: block-option-nofunp

(defun block-option-nofunp (block?)
  (declare (xargs :guard (block-optionp block?)))
  (let ((__function__ 'block-option-nofunp))
    (declare (ignorable __function__))
    (block-option-case block?
                       :some (block-nofunp block?.val)
                       :none t)))

Function: swcase-nofunp

(defun swcase-nofunp (case)
  (declare (xargs :guard (swcasep case)))
  (let ((__function__ 'swcase-nofunp))
    (declare (ignorable __function__))
    (block-nofunp (swcase->body case))))

Function: swcase-list-nofunp

(defun swcase-list-nofunp (cases)
  (declare (xargs :guard (swcase-listp cases)))
  (let ((__function__ 'swcase-list-nofunp))
    (declare (ignorable __function__))
    (or (endp cases)
        (and (swcase-nofunp (car cases))
             (swcase-list-nofunp (cdr cases))))))

Function: fundef-nofunp

(defun fundef-nofunp (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (let ((__function__ 'fundef-nofunp))
    (declare (ignorable __function__))
    (block-nofunp (fundef->body fundef))))

Theorem: return-type-of-statement-nofunp.yes/no

(defthm return-type-of-statement-nofunp.yes/no
  (b* ((?yes/no (statement-nofunp stmt)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-statement-list-nofunp.yes/no

(defthm return-type-of-statement-list-nofunp.yes/no
  (b* ((?yes/no (statement-list-nofunp stmts)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-block-nofunp.yes/no

(defthm return-type-of-block-nofunp.yes/no
  (b* ((?yes/no (block-nofunp block)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-block-option-nofunp.yes/no

(defthm return-type-of-block-option-nofunp.yes/no
  (b* ((?yes/no (block-option-nofunp block?)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-nofunp.yes/no

(defthm return-type-of-swcase-nofunp.yes/no
  (b* ((?yes/no (swcase-nofunp case)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-list-nofunp.yes/no

(defthm return-type-of-swcase-list-nofunp.yes/no
  (b* ((?yes/no (swcase-list-nofunp cases)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-fundef-nofunp.yes/no

(defthm return-type-of-fundef-nofunp.yes/no
  (b* ((?yes/no (fundef-nofunp fundef)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: statement-nofunp-of-statement-fix-stmt

(defthm statement-nofunp-of-statement-fix-stmt
  (equal (statement-nofunp (statement-fix stmt))
         (statement-nofunp stmt)))

Theorem: statement-list-nofunp-of-statement-list-fix-stmts

(defthm statement-list-nofunp-of-statement-list-fix-stmts
  (equal (statement-list-nofunp (statement-list-fix stmts))
         (statement-list-nofunp stmts)))

Theorem: block-nofunp-of-block-fix-block

(defthm block-nofunp-of-block-fix-block
  (equal (block-nofunp (block-fix block))
         (block-nofunp block)))

Theorem: block-option-nofunp-of-block-option-fix-block?

(defthm block-option-nofunp-of-block-option-fix-block?
  (equal (block-option-nofunp (block-option-fix block?))
         (block-option-nofunp block?)))

Theorem: swcase-nofunp-of-swcase-fix-case

(defthm swcase-nofunp-of-swcase-fix-case
  (equal (swcase-nofunp (swcase-fix case))
         (swcase-nofunp case)))

Theorem: swcase-list-nofunp-of-swcase-list-fix-cases

(defthm swcase-list-nofunp-of-swcase-list-fix-cases
  (equal (swcase-list-nofunp (swcase-list-fix cases))
         (swcase-list-nofunp cases)))

Theorem: fundef-nofunp-of-fundef-fix-fundef

(defthm fundef-nofunp-of-fundef-fix-fundef
  (equal (fundef-nofunp (fundef-fix fundef))
         (fundef-nofunp fundef)))

Theorem: statement-nofunp-statement-equiv-congruence-on-stmt

(defthm statement-nofunp-statement-equiv-congruence-on-stmt
  (implies (statement-equiv stmt stmt-equiv)
           (equal (statement-nofunp stmt)
                  (statement-nofunp stmt-equiv)))
  :rule-classes :congruence)

Theorem: statement-list-nofunp-statement-list-equiv-congruence-on-stmts

(defthm
     statement-list-nofunp-statement-list-equiv-congruence-on-stmts
  (implies (statement-list-equiv stmts stmts-equiv)
           (equal (statement-list-nofunp stmts)
                  (statement-list-nofunp stmts-equiv)))
  :rule-classes :congruence)

Theorem: block-nofunp-block-equiv-congruence-on-block

(defthm block-nofunp-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (block-nofunp block)
                  (block-nofunp block-equiv)))
  :rule-classes :congruence)

Theorem: block-option-nofunp-block-option-equiv-congruence-on-block?

(defthm block-option-nofunp-block-option-equiv-congruence-on-block?
  (implies (block-option-equiv block? block?-equiv)
           (equal (block-option-nofunp block?)
                  (block-option-nofunp block?-equiv)))
  :rule-classes :congruence)

Theorem: swcase-nofunp-swcase-equiv-congruence-on-case

(defthm swcase-nofunp-swcase-equiv-congruence-on-case
  (implies (swcase-equiv case case-equiv)
           (equal (swcase-nofunp case)
                  (swcase-nofunp case-equiv)))
  :rule-classes :congruence)

Theorem: swcase-list-nofunp-swcase-list-equiv-congruence-on-cases

(defthm swcase-list-nofunp-swcase-list-equiv-congruence-on-cases
  (implies (swcase-list-equiv cases cases-equiv)
           (equal (swcase-list-nofunp cases)
                  (swcase-list-nofunp cases-equiv)))
  :rule-classes :congruence)

Theorem: fundef-nofunp-fundef-equiv-congruence-on-fundef

(defthm fundef-nofunp-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (fundef-nofunp fundef)
                  (fundef-nofunp fundef-equiv)))
  :rule-classes :congruence)

Theorem: block-option-nofunp-when-blockp

(defthm block-option-nofunp-when-blockp
  (implies (blockp block)
           (equal (block-option-nofunp block)
                  (block-nofunp block))))

Subtopics

Fundef-nofunp

Check that a function definition has no nested function definitions.

Statement-nofunp

Check that a statement has no function definitions.

Statement-list-nofunp

Check that a list of statements has no function definitions.

Block-option-nofunp

Check that an optional block has no function definitions.

Block-nofunp

Check that a block has no function definitions.

Swcase-list-nofunp

Check that a list of switch cases has no function definitions.

Swcase-nofunp

Check that a switch case has no function definitions.