• 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
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
        • Transformations
          • Renaming-variables
          • Dead-code-eliminator
          • Renamings
          • Disambiguator
          • Unique-variables
          • Dead-code-eliminator-static-safety
          • No-function-definitions
          • Unique-functions
          • Renaming-functions
          • Dead-code-eliminator-no-loop-initializers
          • Dead-code-eliminator-no-function-definitions
          • No-loop-initializers
            • Statements/blocks/cases/fundefs-noloopinitp
              • Swcase-noloopinitp
              • Swcase-list-noloopinitp
              • Statement-noloopinitp
              • Statement-list-noloopinitp
              • Fundef-noloopinitp
              • Block-option-noloopinitp
              • Block-noloopinitp
          • For-loop-init-rewriter
        • Language
        • Yul-json
      • 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

• No-loop-initializers

Statements/blocks/cases/fundefs-noloopinitp

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

Definitions and Theorems

Function: statement-noloopinitp

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

Function: statement-list-noloopinitp

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

Function: block-noloopinitp

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

Function: block-option-noloopinitp

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

Function: swcase-noloopinitp

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

Function: swcase-list-noloopinitp

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

Function: fundef-noloopinitp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: statement-noloopinitp-of-statement-fix-stmt

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

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

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

Theorem: block-noloopinitp-of-block-fix-block

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

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

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

Theorem: swcase-noloopinitp-of-swcase-fix-case

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

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

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

Theorem: fundef-noloopinitp-of-fundef-fix-fundef

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

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

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

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

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

Theorem: block-noloopinitp-block-equiv-congruence-on-block

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

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

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

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

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

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

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

Theorem: fundef-noloopinitp-fundef-equiv-congruence-on-fundef

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

Theorem: block-option-noloopinitp-when-blockp

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

Subtopics

Swcase-noloopinitp

Check that a switch case has empty loop initialization blocks.

Swcase-list-noloopinitp

Check that a list of switch cases has empty loop initialization blocks.

Statement-noloopinitp

Check that a statement has empty loop initialization blocks.

Statement-list-noloopinitp

Check that a list of statements has empty loop initialization blocks.

Fundef-noloopinitp

Check that a function definition has empty loop initialization blocks.

Block-option-noloopinitp

Check that an optional block has empty loop initialization blocks.

Block-noloopinitp

Check that a block has empty loop initialization blocks.