• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
        • Process-syntheto-toplevel-fn
        • Translation
        • Language
          • Static-semantics
            • Check-expression-fns
            • Subtypep
            • Match-type
            • Check-product-update-expression
            • Get-builtin-function-in/out/pre-post
            • Check-sum-update-expression
            • Check-sum-field-expression
            • Check-strict-binary-expression
            • Check-lt/le/gt/ge-expression
            • Check-eq/ne-expression
            • Check-div/rem-expression
            • Check-add/sub/mul-expression
            • Align-let-vars-values
            • Check-iff-expression
            • Check-function-definition-top/nontop
            • Check-sum-construct-expression
            • Check-rem-expression
            • Check-mul-expression
            • Check-sub-expression
            • Check-div-expression
            • Check-add-expression
            • Check-ne-expression
            • Check-lt-expression
            • Check-le-expression
            • Check-gt-expression
            • Check-ge-expression
            • Check-eq-expression
            • Check-function-specifier
            • Type-result
            • Check-product-construct-expression
            • Supremum-type
            • Check-call-expression
            • Check-product-field-expression
            • Check-function-definer
            • Make-subproof-obligations
            • Get-function-in/out/pre/post
            • Check-sum-test-expression
            • Match-field
            • Decompose-expression
            • Match-to-target
            • Check-unary-expression
            • Max-supertype
            • Match-type-list
            • Check-minus-expression
            • Check-type-definition
            • Check-not-expression
            • Check-type-product
            • Match-field-list
            • Check-type-subset
            • Check-type-definition-in-recursion
            • Align-let-vars-values-aux
            • Non-trivial-proof-obligation
            • Check-type-recursion
            • Check-function-specification
            • Check-toplevel
            • Supremum-type-list
            • Check-component-expression
            • Check-branch-list
            • Check-function-recursion
            • Check-function-definition
            • Binding
            • Check-function-header
            • Check-function-definition-list
            • Check-type-definition-list-in-recursion
            • Check-theorem
            • Check-nonstrict-binary-expression
            • Context-add-variables
            • Decompose-expression-aux
            • Check-alternative
            • Check-multi-expression
            • Check-type-sum
            • Check-type
            • Check-alternative-list
            • Context-add-condition
            • Check-type-definer
            • Check-transform
            • Check-variable
            • Check-transform-args
            • Check-toplevel-list
            • Context-add-condition-list
            • Check-if/when/unless-expression
            • Initializers-to-variable-substitution
            • Context-add-binding
            • Check-function-header-list
            • Context-add-toplevel
            • Ensure-single-type
            • Max-supertypes
            • Check-bind-expression
            • Check-type-list
            • Check-literal
            • Literal-type
            • Check-expression-list
            • Variable-context
            • Check-cond-expression
            • Check-branch
            • Args-without-defaults
            • Check-expression
            • *builtin-function-names*
            • Function-called-in
          • Abstract-syntax
          • Outcome
          • Abstract-syntax-operations
          • Outcome-list
          • Outcomes
        • Process-syntheto-toplevel
        • Shallow-embedding
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Static-semantics

Check-strict-binary-expression

Check if a strict binary expression is well-formed.

Signature

(check-strict-binary-expression 
     op arg1 
     arg2 arg1-result arg2-result expr ctxt) 
 
  → 
result

Arguments

op — Guard (binary-opp op).

arg1 — Guard (expressionp arg1).

arg2 — Guard (expressionp arg2).

arg1-result — Guard (type-resultp arg1-result).

arg2-result — Guard (type-resultp arg2-result).

expr — Guard (expressionp expr).

ctxt — Guard (contextp ctxt).

Returns

result — Type (type-resultp result).

The arg1-result and arg2-result parameters of this function are the results of checking the operand expressions. If any is an error, we propagate it, left first. Otherwise, we dispatch based on the binary operator: each operator's function returns a result, which may add proof obligations to the ones from the operand.

Definitions and Theorems

Function: check-strict-binary-expression

(defun check-strict-binary-expression
       (op arg1
           arg2 arg1-result arg2-result expr ctxt)
 (declare (xargs :guard (and (binary-opp op)
                             (expressionp arg1)
                             (expressionp arg2)
                             (type-resultp arg1-result)
                             (type-resultp arg2-result)
                             (expressionp expr)
                             (contextp ctxt))))
 (declare (xargs :guard (binary-op-strictp op)))
 (let ((__function__ 'check-strict-binary-expression))
  (declare (ignorable __function__))
  (type-result-case
   arg1-result
   :err (type-result-err arg1-result.info)
   :ok
   (b* ((arg1-type (ensure-single-type arg1-result.types)))
    (if (not arg1-type)
        (type-result-err (list :type-mismatch-multi
                               (expression-fix arg1)
                               arg1-result.types))
     (type-result-case
      arg2-result
      :err (type-result-err arg2-result.info)
      :ok
      (b* ((arg2-type (ensure-single-type arg2-result.types)))
       (if (not arg2-type)
           (type-result-err (list :type-mismatch-multi
                                  (expression-fix arg2)
                                  arg2-result.types))
        (case (binary-op-kind op)
         (:eq
            (check-eq-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:ne
            (check-ne-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:lt
            (check-lt-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:le
            (check-le-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:gt
            (check-gt-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:ge
            (check-ge-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:iff
           (check-iff-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:add
           (check-add-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:sub
           (check-sub-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:mul
           (check-mul-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:div
           (check-div-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (:rem
           (check-rem-expression arg1 arg2 arg1-type
                                 arg2-type arg1-result.obligations
                                 arg2-result.obligations expr ctxt))
         (t (prog2$ (impossible)
                    (type-result-err :impossible))))))))))))

Theorem: type-resultp-of-check-strict-binary-expression

(defthm type-resultp-of-check-strict-binary-expression
  (b* ((result (check-strict-binary-expression
                    op arg1 arg2
                    arg1-result arg2-result expr ctxt)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-strict-binary-expression-of-binary-op-fix-op

(defthm check-strict-binary-expression-of-binary-op-fix-op
  (equal (check-strict-binary-expression
              (binary-op-fix op)
              arg1
              arg2 arg1-result arg2-result expr ctxt)
         (check-strict-binary-expression
              op arg1 arg2
              arg1-result arg2-result expr ctxt)))

Theorem: check-strict-binary-expression-binary-op-equiv-congruence-on-op

(defthm
    check-strict-binary-expression-binary-op-equiv-congruence-on-op
  (implies (binary-op-equiv op op-equiv)
           (equal (check-strict-binary-expression
                       op arg1
                       arg2 arg1-result arg2-result expr ctxt)
                  (check-strict-binary-expression
                       op-equiv arg1 arg2
                       arg1-result arg2-result expr ctxt)))
  :rule-classes :congruence)

Theorem: check-strict-binary-expression-of-expression-fix-arg1

(defthm check-strict-binary-expression-of-expression-fix-arg1
  (equal (check-strict-binary-expression
              op (expression-fix arg1)
              arg2 arg1-result arg2-result expr ctxt)
         (check-strict-binary-expression
              op arg1 arg2
              arg1-result arg2-result expr ctxt)))

Theorem: check-strict-binary-expression-expression-equiv-congruence-on-arg1

(defthm
 check-strict-binary-expression-expression-equiv-congruence-on-arg1
 (implies (expression-equiv arg1 arg1-equiv)
          (equal (check-strict-binary-expression
                      op arg1
                      arg2 arg1-result arg2-result expr ctxt)
                 (check-strict-binary-expression
                      op arg1-equiv arg2
                      arg1-result arg2-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-strict-binary-expression-of-expression-fix-arg2

(defthm check-strict-binary-expression-of-expression-fix-arg2
 (equal
  (check-strict-binary-expression op arg1 (expression-fix arg2)
                                  arg1-result arg2-result expr ctxt)
  (check-strict-binary-expression
       op arg1 arg2
       arg1-result arg2-result expr ctxt)))

Theorem: check-strict-binary-expression-expression-equiv-congruence-on-arg2

(defthm
 check-strict-binary-expression-expression-equiv-congruence-on-arg2
 (implies (expression-equiv arg2 arg2-equiv)
          (equal (check-strict-binary-expression
                      op arg1
                      arg2 arg1-result arg2-result expr ctxt)
                 (check-strict-binary-expression
                      op arg1 arg2-equiv
                      arg1-result arg2-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-strict-binary-expression-of-type-result-fix-arg1-result

(defthm
      check-strict-binary-expression-of-type-result-fix-arg1-result
  (equal (check-strict-binary-expression
              op
              arg1 arg2 (type-result-fix arg1-result)
              arg2-result expr ctxt)
         (check-strict-binary-expression
              op arg1 arg2
              arg1-result arg2-result expr ctxt)))

Theorem: check-strict-binary-expression-type-result-equiv-congruence-on-arg1-result

(defthm
 check-strict-binary-expression-type-result-equiv-congruence-on-arg1-result
 (implies
  (type-result-equiv arg1-result arg1-result-equiv)
  (equal
      (check-strict-binary-expression
           op arg1
           arg2 arg1-result arg2-result expr ctxt)
      (check-strict-binary-expression op arg1 arg2 arg1-result-equiv
                                      arg2-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-strict-binary-expression-of-type-result-fix-arg2-result

(defthm
      check-strict-binary-expression-of-type-result-fix-arg2-result
  (equal
       (check-strict-binary-expression op arg1 arg2 arg1-result
                                       (type-result-fix arg2-result)
                                       expr ctxt)
       (check-strict-binary-expression
            op arg1 arg2
            arg1-result arg2-result expr ctxt)))

Theorem: check-strict-binary-expression-type-result-equiv-congruence-on-arg2-result

(defthm
 check-strict-binary-expression-type-result-equiv-congruence-on-arg2-result
 (implies
  (type-result-equiv arg2-result arg2-result-equiv)
  (equal
      (check-strict-binary-expression
           op arg1
           arg2 arg1-result arg2-result expr ctxt)
      (check-strict-binary-expression op arg1 arg2 arg1-result
                                      arg2-result-equiv expr ctxt)))
 :rule-classes :congruence)

Theorem: check-strict-binary-expression-of-expression-fix-expr

(defthm check-strict-binary-expression-of-expression-fix-expr
 (equal
   (check-strict-binary-expression op arg1 arg2 arg1-result
                                   arg2-result (expression-fix expr)
                                   ctxt)
   (check-strict-binary-expression
        op arg1 arg2
        arg1-result arg2-result expr ctxt)))

Theorem: check-strict-binary-expression-expression-equiv-congruence-on-expr

(defthm
 check-strict-binary-expression-expression-equiv-congruence-on-expr
 (implies
  (expression-equiv expr expr-equiv)
  (equal
      (check-strict-binary-expression
           op arg1
           arg2 arg1-result arg2-result expr ctxt)
      (check-strict-binary-expression op arg1 arg2 arg1-result
                                      arg2-result expr-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-strict-binary-expression-of-context-fix-ctxt

(defthm check-strict-binary-expression-of-context-fix-ctxt
  (equal (check-strict-binary-expression
              op arg1 arg2 arg1-result
              arg2-result expr (context-fix ctxt))
         (check-strict-binary-expression
              op arg1 arg2
              arg1-result arg2-result expr ctxt)))

Theorem: check-strict-binary-expression-context-equiv-congruence-on-ctxt

(defthm
    check-strict-binary-expression-context-equiv-congruence-on-ctxt
 (implies
  (context-equiv ctxt ctxt-equiv)
  (equal
      (check-strict-binary-expression
           op arg1
           arg2 arg1-result arg2-result expr ctxt)
      (check-strict-binary-expression op arg1 arg2 arg1-result
                                      arg2-result expr ctxt-equiv)))
 :rule-classes :congruence)