• 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-pure-limit

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

Signature

(expr-pure-limit expr) → limit

Arguments

expr — Guard (exprp expr).

Returns

limit — Type (posp limit).

The function exec-expr handles possible non-termination via the artificial limit input to the execution functions. However, pure expressions always terminate, and we can calculate, for each pure expression, a limit value that we can pass to exec-expr for execution to terminate. Here we define such calculation.

The execution of the expression may terminate with an error, depending on the computation state and possibly function environment. However, here we are solely concerned with exec-expr not failing the (zp limit) test.

For variables and constants, we just need 1, because we just need to pass the initial test, and then there is no recursive call of exec-expr. For expressions with a single sub-expression, we add 1 to the limit for the sub-expression. For expressions with two or three sub-expressions, we add 1 to the maximum of the limits of the sub-expressions.

Note that currently type names do not undergo execution in our formal dynamic semantics, so for cast expressions we are only concerned with the sub-expression.

For strict expressions, the limit returned by this function is the minimum one for which execution does not fail (due to the limit): a smaller value would fail, because all sub-expressions are executed. For non-strict expressions, this is not necessarily the minimum: for instance, a && expression could have a first sub-expression that needs a much smaller limit than the second, and that first sub-expression may suffice to evaluate the expression.

Definitions and Theorems

Function: expr-pure-limit

(defun expr-pure-limit (expr)
  (declare (xargs :guard (exprp expr)))
  (declare (xargs :guard (expr-purep expr)))
  (expr-case expr
             :ident 1
             :const 1
             :arrsub (1+ (max (expr-pure-limit expr.arr)
                              (expr-pure-limit expr.sub)))
             :member (1+ (expr-pure-limit expr.target))
             :memberp (1+ (expr-pure-limit expr.target))
             :unary (1+ (expr-pure-limit expr.arg))
             :cast (1+ (expr-pure-limit expr.arg))
             :binary (1+ (max (expr-pure-limit expr.arg1)
                              (expr-pure-limit expr.arg2)))
             :cond (1+ (max (expr-pure-limit expr.test)
                            (max (expr-pure-limit expr.then)
                                 (expr-pure-limit expr.else))))
             :otherwise (prog2$ (impossible) 1)))

Theorem: posp-of-expr-pure-limit

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

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

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

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

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