• 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
          • For-loop-init-rewriter
            • Statements/blocks/cases/fundefs-loopinit
              • Statement-loopinit
              • Swcase-list-loopinit
              • Statement-list-loopinit
              • Fundef-loopinit
              • Block-option-loopinit
              • Swcase-loopinit
              • Block-loopinit
        • Language
        • Yul-json
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• For-loop-init-rewriter

Statements/blocks/cases/fundefs-loopinit

Mutually recursive functions to move loop initializers before loops in statements, blocks, cases, and function definitions.

Definitions and Theorems

Function: statement-loopinit

(defun statement-loopinit (stmt)
 (declare (xargs :guard (statementp stmt)))
 (let ((__function__ 'statement-loopinit))
  (declare (ignorable __function__))
  (statement-case
   stmt
   :block (statement-block (block-loopinit stmt.get))
   :variable-single (statement-fix stmt)
   :variable-multi (statement-fix stmt)
   :assign-single (statement-fix stmt)
   :assign-multi (statement-fix stmt)
   :funcall (statement-fix stmt)
   :if (make-statement-if :test stmt.test
                          :body (block-loopinit stmt.body))
   :for
   (statement-block
    (block
     (append
      (statement-list-loopinit (block->statements stmt.init))
      (list
           (make-statement-for :init (block nil)
                               :test stmt.test
                               :update (block-loopinit stmt.update)
                               :body (block-loopinit stmt.body))))))
   :switch (make-statement-switch
                :target stmt.target
                :cases (swcase-list-loopinit stmt.cases)
                :default (block-option-loopinit stmt.default))
   :leave (statement-leave)
   :break (statement-break)
   :continue (statement-continue)
   :fundef (statement-fundef (fundef-loopinit stmt.get)))))

Function: statement-list-loopinit

(defun statement-list-loopinit (stmts)
  (declare (xargs :guard (statement-listp stmts)))
  (let ((__function__ 'statement-list-loopinit))
    (declare (ignorable __function__))
    (cond ((endp stmts) nil)
          (t (cons (statement-loopinit (car stmts))
                   (statement-list-loopinit (cdr stmts)))))))

Function: block-loopinit

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

Function: block-option-loopinit

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

Function: swcase-loopinit

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

Function: swcase-list-loopinit

(defun swcase-list-loopinit (cases)
  (declare (xargs :guard (swcase-listp cases)))
  (let ((__function__ 'swcase-list-loopinit))
    (declare (ignorable __function__))
    (cond ((endp cases) nil)
          (t (cons (swcase-loopinit (car cases))
                   (swcase-list-loopinit (cdr cases)))))))

Function: fundef-loopinit

(defun fundef-loopinit (fdef)
  (declare (xargs :guard (fundefp fdef)))
  (let ((__function__ 'fundef-loopinit))
    (declare (ignorable __function__))
    (make-fundef :name (fundef->name fdef)
                 :inputs (fundef->inputs fdef)
                 :outputs (fundef->outputs fdef)
                 :body (block-loopinit (fundef->body fdef)))))

Theorem: return-type-of-statement-loopinit.new-stmt

(defthm return-type-of-statement-loopinit.new-stmt
  (b* ((?new-stmt (statement-loopinit stmt)))
    (statementp new-stmt))
  :rule-classes :rewrite)

Theorem: return-type-of-statement-list-loopinit.new-stmt

(defthm return-type-of-statement-list-loopinit.new-stmt
  (b* ((?new-stmt (statement-list-loopinit stmts)))
    (statement-listp new-stmt))
  :rule-classes :rewrite)

Theorem: return-type-of-block-loopinit.new-block

(defthm return-type-of-block-loopinit.new-block
  (b* ((?new-block (block-loopinit block)))
    (blockp new-block))
  :rule-classes :rewrite)

Theorem: return-type-of-block-option-loopinit.new-block?

(defthm return-type-of-block-option-loopinit.new-block?
  (b* ((?new-block? (block-option-loopinit block?)))
    (block-optionp new-block?))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-loopinit.new-case

(defthm return-type-of-swcase-loopinit.new-case
  (b* ((?new-case (swcase-loopinit case)))
    (swcasep new-case))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-list-loopinit.new-cases

(defthm return-type-of-swcase-list-loopinit.new-cases
  (b* ((?new-cases (swcase-list-loopinit cases)))
    (swcase-listp new-cases))
  :rule-classes :rewrite)

Theorem: return-type-of-fundef-loopinit.new-fdef

(defthm return-type-of-fundef-loopinit.new-fdef
  (b* ((?new-fdef (fundef-loopinit fdef)))
    (fundefp new-fdef))
  :rule-classes :rewrite)

Theorem: statement-loopinit-of-statement-fix-stmt

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

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

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

Theorem: block-loopinit-of-block-fix-block

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

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

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

Theorem: swcase-loopinit-of-swcase-fix-case

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

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

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

Theorem: fundef-loopinit-of-fundef-fix-fdef

(defthm fundef-loopinit-of-fundef-fix-fdef
  (equal (fundef-loopinit (fundef-fix fdef))
         (fundef-loopinit fdef)))

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

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

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

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

Theorem: block-loopinit-block-equiv-congruence-on-block

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

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

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

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

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

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

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

Theorem: fundef-loopinit-fundef-equiv-congruence-on-fdef

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

Subtopics

Statement-loopinit

Move loop initializers before loops in statements.

Swcase-list-loopinit

Move loop initializers before loops in lists of switch cases.

Statement-list-loopinit

Move loop initializers before loops in lists of statements.

Fundef-loopinit

Move loop initializers before loops in function definitions.

Block-option-loopinit

Move loop initializers before loops in optional blocks.

Swcase-loopinit

Move loop initializers before loops in switch cases.

Block-loopinit

Move loop initializers before loops in blocks.