• 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-expr-cond

Equality lifting transformation of a conditional expression.

Signature

(xeq-expr-cond test test-new test-thm-name 
               then then-new then-thm-name 
               else else-new else-thm-name gin) 
 
  → 
(mv expr gou)

Arguments

test — Guard (exprp test).

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

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

then — Guard (expr-optionp then).

then-new — Guard (expr-optionp then-new).

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

else — Guard (exprp else).

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

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

gin — Guard (ginp gin).

Returns

expr — Type (exprp expr).

gou — Type (goutp gou).

The resulting expression is obtained by combining the possibly transformed argument expression.

We generate a theorem iff a theorem was generated for the argument expressions, and the argument expressions are pure. The theorem is proved via a few general ones that we prove below. These are a bit more complicated than for strict expressions, because conditional expressions are non-strict: the branch not taken could return an error while the conditional expression does not.

Definitions and Theorems

Function: xeq-expr-cond

(defun xeq-expr-cond (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)
                             (expr-optionp then)
                             (expr-optionp then-new)
                             (symbolp then-thm-name)
                             (exprp else)
                             (exprp 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)
                             (expr-option-unambp then)
                             (expr-option-annop then)
                             (expr-option-unambp then-new)
                             (expr-option-annop then-new)
                             (expr-unambp else)
                             (expr-annop else)
                             (expr-unambp else-new)
                             (expr-annop else-new))))
 (let ((__function__ 'xeq-expr-cond))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (expr (make-expr-cond :test test
                          :then then
                          :else else))
    (expr-new (make-expr-cond :test test-new
                              :then then-new
                              :else else-new))
    ((unless (and test-thm-name
                  then-thm-name else-thm-name))
     (mv expr-new (gout-no-thm gin)))
    ((mv & old-test) (ldm-expr test))
    ((mv & old-then) (ldm-expr-option then))
    ((mv & old-else) (ldm-expr else))
    ((mv & new-test) (ldm-expr test-new))
    ((mv & new-then)
     (ldm-expr-option then-new))
    ((mv & new-else) (ldm-expr else-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':do-not
        (cons
         ''(preprocess)
         (cons
          ':in-theory
          (cons
           ''((:e c::expr-cond)
              (:e c::type-nonchar-integerp)
              (:e c::expr-value->value)
              (:e c::type-of-value)
              expr-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
                   'expr-cond-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))
                         'nil))))))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'expr-cond-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))
                          'nil))))))))
                  (cons
                   (cons
                    ':instance
                    (cons
                     'expr-cond-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
                      'expr-cond-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
                       'expr-cond-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-expr-thm expr expr-new gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv expr-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: exprp-of-xeq-expr-cond.expr

(defthm exprp-of-xeq-expr-cond.expr
  (b* (((mv ?expr ?gou)
        (xeq-expr-cond test test-new test-thm-name
                       then then-new then-thm-name
                       else else-new else-thm-name gin)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-expr-cond.gou

(defthm goutp-of-xeq-expr-cond.gou
  (b* (((mv ?expr ?gou)
        (xeq-expr-cond test test-new test-thm-name
                       then then-new then-thm-name
                       else else-new else-thm-name gin)))
    (goutp gou))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-xeq-expr-cond

(defthm expr-unambp-of-xeq-expr-cond
  (implies (and (expr-unambp test-new)
                (expr-option-unambp then-new)
                (expr-unambp else-new))
           (b* (((mv ?expr ?gou)
                 (xeq-expr-cond test test-new test-thm-name
                                then then-new then-thm-name
                                else else-new else-thm-name gin)))
             (expr-unambp expr))))

Theorem: expr-annop-of-xeq-expr-cond

(defthm expr-annop-of-xeq-expr-cond
  (implies (and (expr-annop test-new)
                (expr-option-annop then-new)
                (expr-annop else-new))
           (b* (((mv ?expr ?gou)
                 (xeq-expr-cond test test-new test-thm-name
                                then then-new then-thm-name
                                else else-new else-thm-name gin)))
             (expr-annop expr))))

Theorem: expr-aidentp-of-xeq-expr-cond

(defthm expr-aidentp-of-xeq-expr-cond
  (implies (and (expr-aidentp test-new gcc)
                (expr-option-aidentp then-new gcc)
                (expr-aidentp else-new gcc))
           (b* (((mv ?expr ?gou)
                 (xeq-expr-cond test test-new test-thm-name
                                then then-new then-thm-name
                                else else-new else-thm-name gin)))
             (expr-aidentp expr gcc))))