• 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-ifelse

Equality lifting transformation of an if-else statement.

Signature

(xeq-stmt-ifelse test test-new test-thm-name 
                 then then-new then-thm-name 
                 else else-new else-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).

else — Guard (stmtp else).

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

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

gin — Guard (ginp gin).

Returns

stmt — Type (stmtp stmt).

gout — Type (goutp gout).

Definitions and Theorems

Function: xeq-stmt-ifelse

(defun xeq-stmt-ifelse (test test-new test-thm-name
                             then then-new then-thm-name
                             else else-new else-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)
                             (stmtp else)
                             (stmtp else-new)
                             (symbolp else-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)
                             (stmt-unambp else)
                             (stmt-annop else)
                             (stmt-unambp else-new)
                             (stmt-annop else-new))))
 (let ((__function__ 'xeq-stmt-ifelse))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (stmt (make-stmt-ifelse :test test
                            :then then
                            :else else))
    (stmt-new (make-stmt-ifelse :test test-new
                                :then then-new
                                :else else-new))
    ((unless (and test-thm-name
                  then-thm-name else-thm-name))
     (mv stmt-new (gout-no-thm gin)))
    (then-types (stmt-types then))
    (else-types (stmt-types else))
    ((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 & old-else) (ldm-stmt else))
    ((mv & new-else) (ldm-stmt else-new))
    ((mv & then-ctypes)
     (ldm-type-option-set then-types))
    ((mv & else-ctypes)
     (ldm-type-option-set else-types))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::stmt-kind)
            (:e c::stmt-ifelse->test)
            (:e c::stmt-ifelse->then)
            (:e c::stmt-ifelse->else)
            (:e c::stmt-ifelse)
            (: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
                else-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-ifelse-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 'old-else
                          (cons (cons 'quote (cons old-else '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
                            'new-else
                            (cons (cons 'quote (cons new-else 'nil))
                                  'nil))
                       (cons
                        (cons
                         'types
                         (cons (cons 'quote (cons then-ctypes 'nil))
                               'nil))
                        'nil)))))))))
               (cons
                (cons
                 ':instance
                 (cons
                  'stmt-ifelse-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 'old-else
                           (cons (cons 'quote (cons old-else '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
                            'new-else
                            (cons (cons 'quote (cons new-else 'nil))
                                  'nil))
                        (cons
                         (cons
                          'types
                          (cons
                               (cons 'quote (cons else-ctypes 'nil))
                               'nil))
                         'nil)))))))))
                (cons
                 (cons
                  ':instance
                  (cons
                   'stmt-ifelse-test-errors
                   (cons
                    (cons 'test
                          (cons (cons 'quote (cons old-test 'nil))
                                'nil))
                    (cons
                     (cons 'then
                           (cons (cons 'quote (cons old-then 'nil))
                                 'nil))
                     (cons
                      (cons 'else
                            (cons (cons 'quote (cons old-else 'nil))
                                  'nil))
                      '((fenv old-fenv)))))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'stmt-ifelse-then-errors
                    (cons
                     (cons 'test
                           (cons (cons 'quote (cons old-test 'nil))
                                 'nil))
                     (cons
                      (cons 'then
                            (cons (cons 'quote (cons old-then 'nil))
                                  'nil))
                      (cons
                       (cons
                            'else
                            (cons (cons 'quote (cons old-else 'nil))
                                  'nil))
                       '((fenv old-fenv)))))))
                  (cons
                   (cons
                    ':instance
                    (cons
                     'stmt-ifelse-else-errors
                     (cons
                      (cons 'test
                            (cons (cons 'quote (cons old-test 'nil))
                                  'nil))
                      (cons
                       (cons
                            'then
                            (cons (cons 'quote (cons old-then 'nil))
                                  'nil))
                       (cons
                        (cons
                            'else
                            (cons (cons 'quote (cons old-else '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-ifelse.stmt

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

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

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

Theorem: stmt-unambp-of-xeq-stmt-ifelse

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

Theorem: stmt-annop-of-xeq-stmt-ifelse

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

Theorem: stmt-aidentp-of-xeq-stmt-ifelse

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