• 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
        • Transformation-tools
          • Simpadd0
          • Proof-generation
          • Split-gso
          • Wrap-fn
          • Constant-propagation
          • Specialize
          • Split-fn
          • Split-fn-when
          • Split-all-gso
          • Copy-fn
          • Variables-in-computation-states
          • Rename
          • Utilities
          • Proof-generation-theorems
            • Exec-error-theorems
            • Exec-congruence-theorems
            • Exec-loop-theorems
          • Input-processing
        • 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

• Proof-generation-theorems

Exec-error-theorems

Error theorems about execution.

These theorems say that if the execution of a sub-construct yields an error, so does the execution of the super-construct.

Transformations use these theorems in proof generation to actually show that if the super-construct does not yield an error, neither do its sub-constructs.

The theorem expr-pure-errors is a little different, because it relates pure expression execution and general expression execution applied to the same expressions. But it has a similar flavor and structure as the other theorems.

Definitions and Theorems

Theorem: expr-unary-errors

(defthm expr-unary-errors
 (implies
      (c::errorp (mv-nth 0
                         (c::exec-expr arg compst fenv (1- limit))))
      (c::errorp (mv-nth 0
                         (c::exec-expr (c::expr-unary op arg)
                                       compst fenv limit)))))

Theorem: expr-cast-errors

(defthm expr-cast-errors
 (implies
      (c::errorp (mv-nth 0
                         (c::exec-expr arg compst fenv (1- limit))))
      (c::errorp (mv-nth 0
                         (c::exec-expr (c::expr-cast tyname arg)
                                       compst fenv limit)))))

Theorem: expr-binary-pure-strict-errors

(defthm expr-binary-pure-strict-errors
 (b* (((mv eval1 compst1)
       (c::exec-expr arg1 compst fenv (1- limit)))
      ((mv eval2 &)
       (c::exec-expr arg2 compst1 fenv (1- limit))))
  (implies
      (and (c::binop-strictp op)
           (c::binop-purep op)
           (or (c::errorp eval1)
               (c::errorp eval2)))
      (c::errorp (mv-nth 0
                         (c::exec-expr (c::expr-binary op arg1 arg2)
                                       compst fenv limit))))))

Theorem: expr-binary-logand-first-errors

(defthm expr-binary-logand-first-errors
 (implies
  (c::errorp (mv-nth 0
                     (c::exec-expr arg1 compst fenv (1- limit))))
  (c::errorp (mv-nth 0
                     (c::exec-expr (c::expr-binary (c::binop-logand)
                                                   arg1 arg2)
                                   compst fenv limit)))))

Theorem: expr-binary-logand-second-errors

(defthm expr-binary-logand-second-errors
 (b* (((mv eval compst1)
       (c::exec-expr arg1 compst fenv (1- limit))))
  (implies
    (and (not (c::errorp eval))
         (c::type-nonchar-integerp
              (c::type-of-value (c::expr-value->value eval)))
         (c::test-value (c::expr-value->value eval))
         (c::errorp
              (mv-nth 0
                      (c::exec-expr arg2 compst1 fenv (1- limit)))))
    (c::errorp
         (mv-nth 0
                 (c::exec-expr (c::expr-binary (c::binop-logand)
                                               arg1 arg2)
                               compst fenv limit))))))

Theorem: expr-binary-logor-first-errors

(defthm expr-binary-logor-first-errors
 (implies
   (c::errorp (mv-nth 0
                      (c::exec-expr arg1 compst fenv (1- limit))))
   (c::errorp (mv-nth 0
                      (c::exec-expr (c::expr-binary (c::binop-logor)
                                                    arg1 arg2)
                                    compst fenv limit)))))

Theorem: expr-binary-logor-second-errors

(defthm expr-binary-logor-second-errors
 (b* (((mv eval compst1)
       (c::exec-expr arg1 compst fenv (1- limit))))
  (implies
   (and (not (c::errorp eval))
        (c::type-nonchar-integerp
             (c::type-of-value (c::expr-value->value eval)))
        (not (c::test-value (c::expr-value->value eval)))
        (c::errorp
             (mv-nth 0
                     (c::exec-expr arg2 compst1 fenv (1- limit)))))
   (c::errorp (mv-nth 0
                      (c::exec-expr (c::expr-binary (c::binop-logor)
                                                    arg1 arg2)
                                    compst fenv limit))))))

Theorem: expr-binary-asg-errors

(defthm expr-binary-asg-errors
 (implies
  (or
    (c::errorp (mv-nth 0
                       (c::exec-expr (c::expr-ident var)
                                     compst fenv (1- limit))))
    (c::errorp (mv-nth 0
                       (c::exec-expr expr compst fenv (1- limit)))))
  (c::errorp
       (mv-nth 0
               (c::exec-expr (c::expr-binary (c::binop-asg)
                                             (c::expr-ident var)
                                             expr)
                             compst fenv limit)))))

Theorem: expr-cond-test-errors

(defthm expr-cond-test-errors
 (implies
     (c::errorp (mv-nth 0
                        (c::exec-expr test compst fenv (1- limit))))
     (c::errorp (mv-nth 0
                        (c::exec-expr (c::expr-cond test then else)
                                      compst fenv limit)))))

Theorem: expr-cond-then-errors

(defthm expr-cond-then-errors
 (b* (((mv eval compst1)
       (c::exec-expr test compst fenv (1- limit))))
  (implies
    (and (not (c::errorp eval))
         (c::type-nonchar-integerp
              (c::type-of-value (c::expr-value->value eval)))
         (c::test-value (c::expr-value->value eval))
         (c::errorp
              (mv-nth 0
                      (c::exec-expr then compst1 fenv (1- limit)))))
    (c::errorp (mv-nth 0
                       (c::exec-expr (c::expr-cond test then else)
                                     compst fenv limit))))))

Theorem: expr-cond-else-errors

(defthm expr-cond-else-errors
 (b* (((mv eval compst1)
       (c::exec-expr test compst fenv (1- limit))))
  (implies
    (and (not (c::errorp eval))
         (c::type-nonchar-integerp
              (c::type-of-value (c::expr-value->value eval)))
         (not (c::test-value (c::expr-value->value eval)))
         (c::errorp
              (mv-nth 0
                      (c::exec-expr else compst1 fenv (1- limit)))))
    (c::errorp (mv-nth 0
                       (c::exec-expr (c::expr-cond test then else)
                                     compst fenv limit))))))

Theorem: initer-single-errors

(defthm initer-single-errors
 (implies
     (c::errorp (mv-nth 0
                        (c::exec-expr expr compst fenv (1- limit))))
     (c::errorp (mv-nth 0
                        (c::exec-initer (c::initer-single expr)
                                        compst fenv limit)))))

Theorem: stmt-expr-errors

(defthm stmt-expr-errors
 (implies
    (c::errorp (mv-nth 0
                       (c::exec-expr expr compst fenv (- limit 1))))
    (c::errorp (mv-nth 0
                       (c::exec-stmt (c::stmt-expr expr)
                                     compst fenv limit)))))

Theorem: stmt-return-errors

(defthm stmt-return-errors
 (implies
  (and
    expr
    (c::errorp (mv-nth 0
                       (c::exec-expr expr compst fenv (1- limit)))))
  (c::errorp (mv-nth 0
                     (c::exec-stmt (c::stmt-return expr)
                                   compst fenv limit)))))

Theorem: stmt-if-test-errors

(defthm stmt-if-test-errors
 (implies
     (c::errorp (mv-nth 0
                        (c::exec-expr test compst fenv (1- limit))))
     (c::errorp (mv-nth 0
                        (c::exec-stmt (c::stmt-if test then)
                                      compst fenv limit)))))

Theorem: stmt-if-then-errors

(defthm stmt-if-then-errors
 (b* (((mv test-eval compst1)
       (c::exec-expr test compst fenv (1- limit))))
  (implies
    (and (not (c::errorp test-eval))
         (c::type-nonchar-integerp
              (c::type-of-value (c::expr-value->value test-eval)))
         (c::test-value (c::expr-value->value test-eval))
         (c::errorp
              (mv-nth 0
                      (c::exec-stmt then compst1 fenv (1- limit)))))
    (c::errorp (mv-nth 0
                       (c::exec-stmt (c::stmt-if test then)
                                     compst fenv limit))))))

Theorem: stmt-ifelse-test-errors

(defthm stmt-ifelse-test-errors
 (implies
    (c::errorp (mv-nth 0
                       (c::exec-expr test compst fenv (1- limit))))
    (c::errorp (mv-nth 0
                       (c::exec-stmt (c::stmt-ifelse test then else)
                                     compst fenv limit)))))

Theorem: stmt-ifelse-then-errors

(defthm stmt-ifelse-then-errors
 (b* (((mv test-eval compst1)
       (c::exec-expr test compst fenv (1- limit))))
  (implies
    (and (not (c::errorp test-eval))
         (c::type-nonchar-integerp
              (c::type-of-value (c::expr-value->value test-eval)))
         (c::test-value (c::expr-value->value test-eval))
         (c::errorp
              (mv-nth 0
                      (c::exec-stmt then compst1 fenv (1- limit)))))
    (c::errorp (mv-nth 0
                       (c::exec-stmt (c::stmt-ifelse test then else)
                                     compst fenv limit))))))

Theorem: stmt-ifelse-else-errors

(defthm stmt-ifelse-else-errors
 (b* (((mv test-eval compst1)
       (c::exec-expr test compst fenv (1- limit))))
  (implies
    (and (not (c::errorp test-eval))
         (c::type-nonchar-integerp
              (c::type-of-value (c::expr-value->value test-eval)))
         (not (c::test-value (c::expr-value->value test-eval)))
         (c::errorp
              (mv-nth 0
                      (c::exec-stmt else compst1 fenv (1- limit)))))
    (c::errorp (mv-nth 0
                       (c::exec-stmt (c::stmt-ifelse test then else)
                                     compst fenv limit))))))

Theorem: stmt-compound-errors

(defthm stmt-compound-errors
 (implies
  (c::errorp
      (mv-nth 0
              (c::exec-block-item-list items (c::enter-scope compst)
                                       fenv (1- limit))))
  (c::errorp (mv-nth 0
                     (c::exec-stmt (c::stmt-compound items)
                                   compst fenv limit)))))

Theorem: decl-decl-errors

(defthm decl-decl-errors
 (b* ((declor (c::obj-declor-ident var))
      (declon (c::obj-declon (c::scspecseq-none)
                             tyspecs declor initer)))
  (implies
   (and
      initer
      (c::errorp
           (mv-nth 0
                   (c::exec-initer initer compst fenv (1- limit)))))
   (c::errorp (c::exec-obj-declon declon compst fenv limit)))))

Theorem: block-item-stmt-errors

(defthm block-item-stmt-errors
 (implies
    (c::errorp (mv-nth 0
                       (c::exec-stmt stmt compst fenv (1- limit))))
    (c::errorp (mv-nth 0
                       (c::exec-block-item (c::block-item-stmt stmt)
                                           compst fenv limit)))))

Theorem: block-item-decl-errors

(defthm block-item-decl-errors
 (implies
      (c::errorp (c::exec-obj-declon declon compst fenv (1- limit)))
      (c::errorp
           (mv-nth 0
                   (c::exec-block-item (c::block-item-declon declon)
                                       compst fenv limit)))))

Theorem: block-item-list-cons-first-errors

(defthm block-item-list-cons-first-errors
 (implies
  (c::errorp
       (mv-nth 0
               (c::exec-block-item item compst fenv (1- limit))))
  (c::errorp (mv-nth 0
                     (c::exec-block-item-list (cons item items)
                                              compst fenv limit)))))

Theorem: block-item-list-cons-rest-errors

(defthm block-item-list-cons-rest-errors
 (b* (((mv sval compst1)
       (c::exec-block-item item compst fenv (1- limit))))
  (implies
   (and
    (not (c::errorp sval))
    (equal (c::stmt-value-kind sval) :none)
    (c::errorp
     (mv-nth
          0
          (c::exec-block-item-list items compst1 fenv (1- limit)))))
   (c::errorp
        (mv-nth 0
                (c::exec-block-item-list (cons item items)
                                         compst fenv limit))))))