• 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
            • Xeq-fundef
            • Xeq-expr-cond
            • Xeq-expr-binary
            • Xeq-block-item-list-cons
            • Xeq-stmt-ifelse
            • Xeq-expr-const
            • Gen-param-thms
            • Gen-from-params
            • Xeq-decl-decl
            • Gout
            • Gen-block-item-list-thm
            • Xeq-stmt-while
            • Xeq-stmt-dowhile
            • Gin
            • Xeq-expr-ident
            • Gen-block-item-thm
            • Xeq-stmt-if
            • Xeq-expr-cast
            • Gen-initer-single-thm
            • Gen-init-scope-thm
            • Gen-expr-thm
            • Xeq-expr-unary
            • Gen-decl-thm
            • Gen-stmt-thm
            • Xeq-stmt-return
            • Xeq-stmt-expr
            • Xeq-block-item-decl
            • Xeq-block-item-stmt
            • Xeq-stmt-compound
            • Xeq-initer-single
            • Gen-thm-name
            • Gin-update
            • Gen-var-assertions
            • Tyspecseq-to-type
            • Xeq-block-item-list-empty
            • Gout-no-thm
            • Irr-gout
          • 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
          • 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

Xeq-stmt-if

Equality lifting transformation of an if statement (without else).

Signature

(xeq-stmt-if test test-new test-thm-name 
             then then-new then-thm-name gin) 
 
  → 
(mv stmt gout)

Arguments

test — Guard (exprp test).

test-new — Guard (exprp test-new).

test-thm-name — Guard (symbolp test-thm-name).

then — Guard (stmtp then).

then-new — Guard (stmtp then-new).

then-thm-name — Guard (symbolp then-thm-name).

gin — Guard (ginp gin).

Returns

stmt — Type (stmtp stmt).

gout — Type (goutp gout).

Definitions and Theorems

Function: xeq-stmt-if

(defun xeq-stmt-if (test test-new test-thm-name
                         then then-new then-thm-name gin)
 (declare (xargs :guard (and (exprp test)
                             (exprp test-new)
                             (symbolp test-thm-name)
                             (stmtp then)
                             (stmtp then-new)
                             (symbolp then-thm-name)
                             (ginp gin))))
 (declare (xargs :guard (and (expr-unambp test)
                             (expr-annop test)
                             (expr-unambp test-new)
                             (expr-annop test-new)
                             (stmt-unambp then)
                             (stmt-annop then)
                             (stmt-unambp then-new)
                             (stmt-annop then-new))))
 (let ((__function__ 'xeq-stmt-if))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (stmt (make-stmt-if :test test :then then))
    (stmt-new (make-stmt-if :test test-new
                            :then then-new))
    ((unless (and test-thm-name then-thm-name))
     (mv stmt-new (gout-no-thm gin)))
    (then-types (stmt-types then))
    ((mv & old-test) (ldm-expr test))
    ((mv & new-test) (ldm-expr test-new))
    ((mv & old-then) (ldm-stmt then))
    ((mv & new-then) (ldm-stmt then-new))
    ((mv & then-ctypes)
     (ldm-type-option-set then-types))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::stmt-kind)
            (:e c::stmt-if->test)
            (:e c::stmt-if->then)
            (:e c::stmt-if)
            (:e c::type-nonchar-integerp)
            (:e insert)
            (:e subset)
            set::subset-in
            c::compustate-frames-number-of-exec-expr
            c::compustate-frames-number-of-exec-stmt
            c::compustatep-when-compustate-resultp-and-not-errorp
            stmt-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons test-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               then-thm-name
               (cons
                (cons
                 'compst
                 (cons
                  (cons
                   'mv-nth
                   (cons
                    '1
                    (cons
                      (cons 'c::exec-expr
                            (cons (cons 'quote (cons old-test 'nil))
                                  '(compst old-fenv (1- limit))))
                      'nil)))
                  'nil))
                '((limit (1- limit))))))
             (cons
              (cons
               ':instance
               (cons
                'stmt-if-true-congruence
                (cons
                 (cons 'old-test
                       (cons (cons 'quote (cons old-test 'nil))
                             'nil))
                 (cons
                  (cons 'old-then
                        (cons (cons 'quote (cons old-then 'nil))
                              'nil))
                  (cons
                   (cons 'new-test
                         (cons (cons 'quote (cons new-test 'nil))
                               'nil))
                   (cons
                    (cons 'new-then
                          (cons (cons 'quote (cons new-then 'nil))
                                'nil))
                    (cons
                     (cons
                         'types
                         (cons (cons 'quote (cons then-ctypes 'nil))
                               'nil))
                     'nil)))))))
              (cons
               (cons
                ':instance
                (cons
                 'stmt-if-false-congruence
                 (cons
                  (cons 'old-test
                        (cons (cons 'quote (cons old-test 'nil))
                              'nil))
                  (cons
                   (cons 'old-then
                         (cons (cons 'quote (cons old-then 'nil))
                               'nil))
                   (cons
                    (cons 'new-test
                          (cons (cons 'quote (cons new-test 'nil))
                                'nil))
                    (cons
                      (cons 'new-then
                            (cons (cons 'quote (cons new-then 'nil))
                                  'nil))
                      'nil))))))
               (cons
                (cons
                 ':instance
                 (cons
                  'stmt-if-test-errors
                  (cons
                   (cons 'test
                         (cons (cons 'quote (cons old-test 'nil))
                               'nil))
                   (cons
                      (cons 'then
                            (cons (cons 'quote (cons old-then 'nil))
                                  'nil))
                      '((fenv old-fenv))))))
                (cons
                 (cons
                  ':instance
                  (cons
                   'stmt-if-then-errors
                   (cons
                    (cons 'test
                          (cons (cons 'quote (cons old-test 'nil))
                                'nil))
                    (cons
                      (cons 'then
                            (cons (cons 'quote (cons old-then 'nil))
                                  'nil))
                      '((fenv old-fenv))))))
                 'nil))))))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-stmt-thm stmt stmt-new gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv stmt-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: stmtp-of-xeq-stmt-if.stmt

(defthm stmtp-of-xeq-stmt-if.stmt
  (b* (((mv ?stmt ?gout)
        (xeq-stmt-if test test-new test-thm-name
                     then then-new then-thm-name gin)))
    (stmtp stmt))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-stmt-if.gout

(defthm goutp-of-xeq-stmt-if.gout
  (b* (((mv ?stmt ?gout)
        (xeq-stmt-if test test-new test-thm-name
                     then then-new then-thm-name gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: stmt-unambp-of-xeq-stmt-if

(defthm stmt-unambp-of-xeq-stmt-if
  (implies (and (expr-unambp test-new)
                (stmt-unambp then-new))
           (b* (((mv ?stmt ?gout)
                 (xeq-stmt-if test test-new test-thm-name
                              then then-new then-thm-name gin)))
             (stmt-unambp stmt))))

Theorem: stmt-annop-of-xeq-stmt-if

(defthm stmt-annop-of-xeq-stmt-if
  (implies (and (expr-annop test-new)
                (stmt-annop then-new))
           (b* (((mv ?stmt ?gout)
                 (xeq-stmt-if test test-new test-thm-name
                              then then-new then-thm-name gin)))
             (stmt-annop stmt))))

Theorem: stmt-aidentp-of-xeq-stmt-if

(defthm stmt-aidentp-of-xeq-stmt-if
  (implies (and (expr-aidentp test-new gcc)
                (stmt-aidentp then-new gcc))
           (b* (((mv ?stmt ?gout)
                 (xeq-stmt-if test test-new test-thm-name
                              then then-new then-thm-name gin)))
             (stmt-aidentp stmt gcc))))