• 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
        • Syntax-for-tools
        • Atc
          • Atc-implementation
          • Atc-tutorial
          • Pure-expression-execution
            • Exec-expr-pure
            • Expr-pure-limit
            • Exec-expr-pure-list
            • Expr-list-pure-limit
            • Exec-expr-list-to-exec-expr-pure-list-when-expr-pure-list-limit
            • Induct-exec-expr-of-pure
            • Exec-expr-to-exec-expr-pure-when-expr-pure-limit
            • Exec-expr-list-to-exec-expr-pure-list-when-not-errorp
            • Exec-expr-to-exec-expr-pure-when-not-errorp
            • Induct-exec-expr-list-of-pure
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • 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

• Pure-expression-execution

Expr-list-pure-limit

Limit to pass to exec-expr-list for the execution of the given list of pure expressions to terminate.

Signature

(expr-list-pure-limit exprs) → limit

Arguments

exprs — Guard (expr-listp exprs).

Returns

limit — Type (posp limit).

If the list is empty, we still need 1 because exec-expr-list checks the limit against zp before examining the list. If the list is not empty, we additionally need enough to execute the first and the rest, so we take the maximum.

Definitions and Theorems

Function: expr-list-pure-limit

(defun expr-list-pure-limit (exprs)
  (declare (xargs :guard (expr-listp exprs)))
  (declare (xargs :guard (expr-list-purep exprs)))
  (cond ((endp exprs) 1)
        (t (1+ (max (expr-pure-limit (car exprs))
                    (expr-list-pure-limit (cdr exprs)))))))

Theorem: posp-of-expr-list-pure-limit

(defthm posp-of-expr-list-pure-limit
  (b* ((limit (expr-list-pure-limit exprs)))
    (posp limit))
  :rule-classes (:rewrite :type-prescription))

Theorem: expr-list-pure-limit-of-expr-list-fix-exprs

(defthm expr-list-pure-limit-of-expr-list-fix-exprs
  (equal (expr-list-pure-limit (expr-list-fix exprs))
         (expr-list-pure-limit exprs)))

Theorem: expr-list-pure-limit-expr-list-equiv-congruence-on-exprs

(defthm expr-list-pure-limit-expr-list-equiv-congruence-on-exprs
  (implies (expr-list-equiv exprs exprs-equiv)
           (equal (expr-list-pure-limit exprs)
                  (expr-list-pure-limit exprs-equiv)))
  :rule-classes :congruence)