• 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
            • Xeq-declon-declon
            • Gen-param-thms
            • Gen-from-params
            • 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
            • Gen-declon-thm
            • Xeq-expr-unary
            • Gen-stmt-thm
            • Xeq-stmt-return
            • Xeq-stmt-expr
            • Xeq-block-item-declon
            • 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-binary

Equality lifting transformation of a binary expression.

Signature

(xeq-expr-binary op arg1 arg1-new arg1-thm-name 
                 arg2 arg2-new arg2-thm-name info gin) 
 
  → 
(mv expr gout)

Arguments

op — Guard (binopp op).

arg1 — Guard (exprp arg1).

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

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

arg2 — Guard (exprp arg2).

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

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

info — Guard (expr-binary-infop info).

gin — Guard (ginp gin).

Returns

expr — Type (exprp expr).

gout — Type (goutp gout).

We generate a theorem only if theorems were generated for both argument expressions.

For pure strict binary operators, we generate a theorem if additionally both argument expressions are pure, since the order of evaluation is unspecified in C.

For non-strict binary operators (which are pure), the argument expressions may be pure or not, because the order of evaluation is always determined.

For the non-pure strict simple assignment operator, for theorem generation we require the left expression to be a variable. The right expression does not have to be pure, because when the left expression is a variable, the order of evaluation does not matter, because the (previous) value of the assigned variable does not matter. Note that this supports multiple assignments x = y = z = ....

For the remaining (non-pure strict) operators, namely compound assignments, we do not generate any theorems for now.

Definitions and Theorems

Function: xeq-expr-binary

(defun xeq-expr-binary (op arg1 arg1-new arg1-thm-name
                           arg2 arg2-new arg2-thm-name info gin)
 (declare (xargs :guard (and (binopp op)
                             (exprp arg1)
                             (exprp arg1-new)
                             (symbolp arg1-thm-name)
                             (exprp arg2)
                             (exprp arg2-new)
                             (symbolp arg2-thm-name)
                             (expr-binary-infop info)
                             (ginp gin))))
 (declare (xargs :guard (and (expr-unambp arg1)
                             (expr-annop arg1)
                             (expr-unambp arg1-new)
                             (expr-annop arg1-new)
                             (expr-unambp arg2)
                             (expr-annop arg2)
                             (expr-unambp arg2-new)
                             (expr-annop arg2-new))))
 (let ((__function__ 'xeq-expr-binary))
  (declare (ignorable __function__))
  (b* (((gin gin) gin)
       (expr (make-expr-binary :op op
                               :arg1 arg1
                               :arg2 arg2
                               :info info))
       (expr-new (make-expr-binary :op op
                                   :arg1 arg1-new
                                   :arg2 arg2-new
                                   :info info))
       (gout-no-thm (gout-no-thm gin))
       ((unless (and arg1-thm-name arg2-thm-name))
        (mv expr-new gout-no-thm)))
   (cond
    ((and (c$::binop-purep op)
          (c$::binop-strictp op))
     (b*
      (((unless (and (expr-purep arg1)
                     (expr-purep arg2)))
        (mv expr-new gout-no-thm))
       (cop (ldm-binop op))
       ((mv & old-arg1) (ldm-expr arg1))
       ((mv & old-arg2) (ldm-expr arg2))
       ((mv & new-arg1) (ldm-expr arg1-new))
       ((mv & new-arg2) (ldm-expr arg2-new))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e c::binop-kind)
               (:e c::binop-purep)
               (:e c::binop-strictp)
               (:e c::expr-binary)
               (:e c::type-nonchar-integerp)
               (:e c::promote-type)
               (:e c::uaconvert-types)
               (:e c::type-sint)
               (:e member-equal)
               (:e c::expr-purep)
               expr-compustate-vars)
            (cons
             ':use
             (cons
              (cons
               (cons ':instance
                     (cons arg1-thm-name '((limit (1- limit)))))
               (cons
                (cons
                 ':instance
                 (cons
                  arg2-thm-name
                  (cons
                   (cons
                    'compst
                    (cons
                     (cons
                      'mv-nth
                      (cons
                       '1
                       (cons
                        (cons
                            'c::exec-expr
                            (cons (cons 'quote (cons old-arg1 'nil))
                                  '(compst old-fenv (1- limit))))
                        'nil)))
                     'nil))
                   '((limit (1- limit))))))
                (cons
                 (cons ':instance
                       (cons arg2-thm-name '((limit (1- limit)))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'expr-binary-pure-strict-congruence
                    (cons
                     (cons 'op
                           (cons (cons 'quote (cons cop 'nil))
                                 'nil))
                     (cons
                      (cons 'old-arg1
                            (cons (cons 'quote (cons old-arg1 'nil))
                                  'nil))
                      (cons
                       (cons
                            'old-arg2
                            (cons (cons 'quote (cons old-arg2 'nil))
                                  'nil))
                       (cons
                        (cons
                            'new-arg1
                            (cons (cons 'quote (cons new-arg1 'nil))
                                  'nil))
                        (cons
                         (cons
                            'new-arg2
                            (cons (cons 'quote (cons new-arg2 'nil))
                                  'nil))
                         'nil)))))))
                  (cons
                   (cons
                    ':instance
                    (cons
                     'expr-binary-pure-strict-errors
                     (cons
                      (cons 'op
                            (cons (cons 'quote (cons cop 'nil))
                                  'nil))
                      (cons
                       (cons
                            'arg1
                            (cons (cons 'quote (cons old-arg1 'nil))
                                  'nil))
                       (cons
                        (cons
                            'arg2
                            (cons (cons 'quote (cons old-arg2 '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))))
    ((member-eq (binop-kind op)
                '(:logand :logor))
     (b*
      (((mv & old-arg1) (ldm-expr arg1))
       ((mv & old-arg2) (ldm-expr arg2))
       ((mv & new-arg1) (ldm-expr arg1-new))
       ((mv & new-arg2) (ldm-expr arg2-new))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e c::expr-binary)
               (:e c::binop-logand)
               (:e c::binop-logor)
               (:e c::type-sint)
               (: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 arg1-thm-name '((limit (1- limit)))))
               (cons
                (cons
                 ':instance
                 (cons
                  arg2-thm-name
                  (cons
                   (cons
                    'compst
                    (cons
                     (cons
                      'mv-nth
                      (cons
                       '1
                       (cons
                        (cons
                            'c::exec-expr
                            (cons (cons 'quote (cons old-arg1 'nil))
                                  '(compst old-fenv (1- limit))))
                        'nil)))
                     'nil))
                   '((limit (1- limit))))))
                (cons
                 (cons
                  ':instance
                  (cons
                   (case (binop-kind op)
                     (:logand 'expr-binary-logand-first-congruence)
                     (:logor 'expr-binary-logor-first-congruence))
                   (cons
                    (cons 'old-arg1
                          (cons (cons 'quote (cons old-arg1 'nil))
                                'nil))
                    (cons
                     (cons 'old-arg2
                           (cons (cons 'quote (cons old-arg2 'nil))
                                 'nil))
                     (cons
                      (cons 'new-arg1
                            (cons (cons 'quote (cons new-arg1 'nil))
                                  'nil))
                      (cons
                       (cons
                            'new-arg2
                            (cons (cons 'quote (cons new-arg2 'nil))
                                  'nil))
                       'nil))))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    (case (binop-kind op)
                     (:logand 'expr-binary-logand-second-congruence)
                     (:logor 'expr-binary-logor-second-congruence))
                    (cons
                     (cons 'old-arg1
                           (cons (cons 'quote (cons old-arg1 'nil))
                                 'nil))
                     (cons
                      (cons 'old-arg2
                            (cons (cons 'quote (cons old-arg2 'nil))
                                  'nil))
                      (cons
                       (cons
                            'new-arg1
                            (cons (cons 'quote (cons new-arg1 'nil))
                                  'nil))
                       (cons
                        (cons
                            'new-arg2
                            (cons (cons 'quote (cons new-arg2 'nil))
                                  'nil))
                        'nil))))))
                  (cons
                   (cons
                    ':instance
                    (cons
                     (case (binop-kind op)
                       (:logand 'expr-binary-logand-first-errors)
                       (:logor 'expr-binary-logor-first-errors))
                     (cons
                      (cons 'arg1
                            (cons (cons 'quote (cons old-arg1 'nil))
                                  'nil))
                      (cons
                       (cons
                            'arg2
                            (cons (cons 'quote (cons old-arg2 'nil))
                                  'nil))
                       '((fenv old-fenv))))))
                   (cons
                    (cons
                     ':instance
                     (cons
                      (case (binop-kind op)
                        (:logand 'expr-binary-logand-second-errors)
                        (:logor 'expr-binary-logor-second-errors))
                      (cons
                       (cons
                            'arg1
                            (cons (cons 'quote (cons old-arg1 'nil))
                                  'nil))
                       (cons
                        (cons
                            'arg2
                            (cons (cons 'quote (cons old-arg2 '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))))
    ((eq (binop-kind op) :asg)
     (b*
      (((unless (and (expr-case arg1 :ident)
                     (equal (expr-type arg1)
                            (expr-type arg2))
                     (type-integerp (expr-type arg1))))
        (mv expr-new gout-no-thm))
       ((mv & cvar)
        (ldm-ident (expr-ident->ident arg1)))
       ((mv & old-arg2) (ldm-expr arg2))
       ((mv & new-arg2) (ldm-expr arg2-new))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e c::expr-kind)
               (:e c::expr-ident)
               (:e c::expr-ident->get)
               (:e c::expr-binary->op)
               (:e c::expr-binary->arg1)
               (:e c::expr-binary->arg2)
               (:e c::expr-binary)
               (:e c::binop-kind)
               (:e c::binop-asg)
               (:e c::ident)
               (:e c::type-nonchar-integerp)
               c::not-errorp-when-compustate-has-var-with-type-p
               expr-compustate-vars)
            (cons
             ':use
             (cons
              (cons
               arg1-thm-name
               (cons
                (cons ':instance
                      (cons arg2-thm-name '((limit (1- limit)))))
                (cons
                 (cons
                  ':instance
                  (cons
                   'expr-binary-asg-congruence
                   (cons
                    (cons 'var
                          (cons (cons 'quote (cons cvar 'nil))
                                'nil))
                    (cons
                     (cons 'old-arg
                           (cons (cons 'quote (cons old-arg2 'nil))
                                 'nil))
                     (cons
                      (cons 'new-arg
                            (cons (cons 'quote (cons new-arg2 'nil))
                                  'nil))
                      'nil)))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'expr-binary-asg-errors
                    (cons
                     (cons 'var
                           (cons (cons 'quote (cons cvar 'nil))
                                 'nil))
                     (cons
                      (cons 'expr
                            (cons (cons 'quote (cons old-arg2 '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))))
    (t (mv expr-new gout-no-thm))))))

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

(defthm exprp-of-xeq-expr-binary.expr
  (b* (((mv ?expr ?gout)
        (xeq-expr-binary op arg1 arg1-new arg1-thm-name
                         arg2 arg2-new arg2-thm-name info gin)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-expr-binary.gout

(defthm goutp-of-xeq-expr-binary.gout
  (b* (((mv ?expr ?gout)
        (xeq-expr-binary op arg1 arg1-new arg1-thm-name
                         arg2 arg2-new arg2-thm-name info gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-xeq-expr-binary

(defthm expr-unambp-of-xeq-expr-binary
 (implies
      (and (expr-unambp arg1-new)
           (expr-unambp arg2-new))
      (b* (((mv ?expr ?gout)
            (xeq-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
        (expr-unambp expr))))

Theorem: expr-annop-of-xeq-expr-binary

(defthm expr-annop-of-xeq-expr-binary
 (implies
      (and (expr-annop arg1-new)
           (expr-annop arg2-new)
           (expr-binary-infop info))
      (b* (((mv ?expr ?gout)
            (xeq-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
        (expr-annop expr))))

Theorem: expr-aidentp-of-xeq-expr-binary

(defthm expr-aidentp-of-xeq-expr-binary
 (implies
      (and (expr-aidentp arg1-new gcc)
           (expr-aidentp arg2-new gcc))
      (b* (((mv ?expr ?gout)
            (xeq-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
        (expr-aidentp expr gcc))))