• 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
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • 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
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Static-semantics

Check-lt/le/gt/ge-expression

Check if an ordering expression is well-formed.

Signature

(check-lt/le/gt/ge-expression arg1 
                              arg2 arg1-type arg2-type arg1-obligs 
                              arg2-obligs err-keyword expr ctxt) 
 
  → 
result

Arguments

arg1 — Guard (expressionp arg1).

arg2 — Guard (expressionp arg2).

arg1-type — Guard (typep arg1-type).

arg2-type — Guard (typep arg2-type).

arg1-obligs — Guard (proof-obligation-listp arg1-obligs).

arg2-obligs — Guard (proof-obligation-listp arg2-obligs).

err-keyword — Guard (keywordp err-keyword).

expr — Guard (expressionp expr).

ctxt — Guard (contextp ctxt).

Returns

result — Type (type-resultp result).

The two types must be both (subtypes of) integers, both (subtypes of) characters, or both (subtypes of) strings. We calculate the supremum type, and check whether it is (a subtype of) any of these three types. The expression returns a boolean.

Definitions and Theorems

Function: check-lt/le/gt/ge-expression

(defun check-lt/le/gt/ge-expression
       (arg1 arg2 arg1-type arg2-type arg1-obligs
             arg2-obligs err-keyword expr ctxt)
  (declare (xargs :guard (and (expressionp arg1)
                              (expressionp arg2)
                              (typep arg1-type)
                              (typep arg2-type)
                              (proof-obligation-listp arg1-obligs)
                              (proof-obligation-listp arg2-obligs)
                              (keywordp err-keyword)
                              (expressionp expr)
                              (contextp ctxt))))
  (declare (ignorable expr))
  (let ((__function__ 'check-lt/le/gt/ge-expression))
    (declare (ignorable __function__))
    (b* ((supremum (supremum-type arg1-type
                                  arg2-type (context->tops ctxt))))
      (if (and supremum
               (subtypep supremum (type-integer)
                         (context->tops ctxt)))
          (make-type-result-ok
               :types (list (type-boolean))
               :obligations (append arg1-obligs arg2-obligs))
        (type-result-err (list err-keyword (expression-fix arg1)
                               (expression-fix arg2)
                               (type-fix arg1-type)
                               (type-fix arg2-type)))))))

Theorem: type-resultp-of-check-lt/le/gt/ge-expression

(defthm type-resultp-of-check-lt/le/gt/ge-expression
  (b* ((result (check-lt/le/gt/ge-expression
                    arg1
                    arg2 arg1-type arg2-type arg1-obligs
                    arg2-obligs err-keyword expr ctxt)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-lt/le/gt/ge-expression-of-expression-fix-arg1

(defthm check-lt/le/gt/ge-expression-of-expression-fix-arg1
 (equal
  (check-lt/le/gt/ge-expression (expression-fix arg1)
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-expression-equiv-congruence-on-arg1

(defthm
   check-lt/le/gt/ge-expression-expression-equiv-congruence-on-arg1
  (implies (expression-equiv arg1 arg1-equiv)
           (equal (check-lt/le/gt/ge-expression
                       arg1
                       arg2 arg1-type arg2-type arg1-obligs
                       arg2-obligs err-keyword expr ctxt)
                  (check-lt/le/gt/ge-expression
                       arg1-equiv
                       arg2 arg1-type arg2-type arg1-obligs
                       arg2-obligs err-keyword expr ctxt)))
  :rule-classes :congruence)

Theorem: check-lt/le/gt/ge-expression-of-expression-fix-arg2

(defthm check-lt/le/gt/ge-expression-of-expression-fix-arg2
 (equal
  (check-lt/le/gt/ge-expression arg1 (expression-fix arg2)
                                arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-expression-equiv-congruence-on-arg2

(defthm
   check-lt/le/gt/ge-expression-expression-equiv-congruence-on-arg2
  (implies (expression-equiv arg2 arg2-equiv)
           (equal (check-lt/le/gt/ge-expression
                       arg1
                       arg2 arg1-type arg2-type arg1-obligs
                       arg2-obligs err-keyword expr ctxt)
                  (check-lt/le/gt/ge-expression
                       arg1 arg2-equiv
                       arg1-type arg2-type arg1-obligs
                       arg2-obligs err-keyword expr ctxt)))
  :rule-classes :congruence)

Theorem: check-lt/le/gt/ge-expression-of-type-fix-arg1-type

(defthm check-lt/le/gt/ge-expression-of-type-fix-arg1-type
 (equal
  (check-lt/le/gt/ge-expression arg1 arg2 (type-fix arg1-type)
                                arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-type-equiv-congruence-on-arg1-type

(defthm
    check-lt/le/gt/ge-expression-type-equiv-congruence-on-arg1-type
  (implies (type-equiv arg1-type arg1-type-equiv)
           (equal (check-lt/le/gt/ge-expression
                       arg1
                       arg2 arg1-type arg2-type arg1-obligs
                       arg2-obligs err-keyword expr ctxt)
                  (check-lt/le/gt/ge-expression
                       arg1 arg2
                       arg1-type-equiv arg2-type arg1-obligs
                       arg2-obligs err-keyword expr ctxt)))
  :rule-classes :congruence)

Theorem: check-lt/le/gt/ge-expression-of-type-fix-arg2-type

(defthm check-lt/le/gt/ge-expression-of-type-fix-arg2-type
 (equal
  (check-lt/le/gt/ge-expression
       arg1 arg2 arg1-type (type-fix arg2-type)
       arg1-obligs
       arg2-obligs err-keyword expr ctxt)
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-type-equiv-congruence-on-arg2-type

(defthm
    check-lt/le/gt/ge-expression-type-equiv-congruence-on-arg2-type
  (implies (type-equiv arg2-type arg2-type-equiv)
           (equal (check-lt/le/gt/ge-expression
                       arg1
                       arg2 arg1-type arg2-type arg1-obligs
                       arg2-obligs err-keyword expr ctxt)
                  (check-lt/le/gt/ge-expression
                       arg1 arg2
                       arg1-type arg2-type-equiv arg1-obligs
                       arg2-obligs err-keyword expr ctxt)))
  :rule-classes :congruence)

Theorem: check-lt/le/gt/ge-expression-of-proof-obligation-list-fix-arg1-obligs

(defthm
 check-lt/le/gt/ge-expression-of-proof-obligation-list-fix-arg1-obligs
 (equal
  (check-lt/le/gt/ge-expression
       arg1 arg2 arg1-type arg2-type
       (proof-obligation-list-fix arg1-obligs)
       arg2-obligs err-keyword expr ctxt)
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-proof-obligation-list-equiv-congruence-on-arg1-obligs

(defthm
 check-lt/le/gt/ge-expression-proof-obligation-list-equiv-congruence-on-arg1-obligs
 (implies
      (proof-obligation-list-equiv arg1-obligs arg1-obligs-equiv)
      (equal (check-lt/le/gt/ge-expression
                  arg1
                  arg2 arg1-type arg2-type arg1-obligs
                  arg2-obligs err-keyword expr ctxt)
             (check-lt/le/gt/ge-expression
                  arg1 arg2
                  arg1-type arg2-type arg1-obligs-equiv
                  arg2-obligs err-keyword expr ctxt)))
 :rule-classes :congruence)

Theorem: check-lt/le/gt/ge-expression-of-proof-obligation-list-fix-arg2-obligs

(defthm
 check-lt/le/gt/ge-expression-of-proof-obligation-list-fix-arg2-obligs
 (equal
  (check-lt/le/gt/ge-expression
       arg1
       arg2 arg1-type arg2-type arg1-obligs
       (proof-obligation-list-fix arg2-obligs)
       err-keyword expr ctxt)
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-proof-obligation-list-equiv-congruence-on-arg2-obligs

(defthm
 check-lt/le/gt/ge-expression-proof-obligation-list-equiv-congruence-on-arg2-obligs
 (implies
      (proof-obligation-list-equiv arg2-obligs arg2-obligs-equiv)
      (equal (check-lt/le/gt/ge-expression
                  arg1
                  arg2 arg1-type arg2-type arg1-obligs
                  arg2-obligs err-keyword expr ctxt)
             (check-lt/le/gt/ge-expression
                  arg1 arg2 arg1-type
                  arg2-type arg1-obligs arg2-obligs-equiv
                  err-keyword expr ctxt)))
 :rule-classes :congruence)

Theorem: check-lt/le/gt/ge-expression-of-expression-fix-expr

(defthm check-lt/le/gt/ge-expression-of-expression-fix-expr
 (equal
  (check-lt/le/gt/ge-expression arg1 arg2 arg1-type
                                arg2-type arg1-obligs arg2-obligs
                                err-keyword (expression-fix expr)
                                ctxt)
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-expression-equiv-congruence-on-expr

(defthm
   check-lt/le/gt/ge-expression-expression-equiv-congruence-on-expr
 (implies
  (expression-equiv expr expr-equiv)
  (equal
     (check-lt/le/gt/ge-expression
          arg1
          arg2 arg1-type arg2-type arg1-obligs
          arg2-obligs err-keyword expr ctxt)
     (check-lt/le/gt/ge-expression arg1 arg2 arg1-type
                                   arg2-type arg1-obligs arg2-obligs
                                   err-keyword expr-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-lt/le/gt/ge-expression-of-context-fix-ctxt

(defthm check-lt/le/gt/ge-expression-of-context-fix-ctxt
 (equal
  (check-lt/le/gt/ge-expression arg1 arg2 arg1-type
                                arg2-type arg1-obligs arg2-obligs
                                err-keyword expr (context-fix ctxt))
  (check-lt/le/gt/ge-expression arg1
                                arg2 arg1-type arg2-type arg1-obligs
                                arg2-obligs err-keyword expr ctxt)))

Theorem: check-lt/le/gt/ge-expression-context-equiv-congruence-on-ctxt

(defthm
      check-lt/le/gt/ge-expression-context-equiv-congruence-on-ctxt
 (implies
  (context-equiv ctxt ctxt-equiv)
  (equal
     (check-lt/le/gt/ge-expression
          arg1
          arg2 arg1-type arg2-type arg1-obligs
          arg2-obligs err-keyword expr ctxt)
     (check-lt/le/gt/ge-expression arg1 arg2 arg1-type
                                   arg2-type arg1-obligs arg2-obligs
                                   err-keyword expr ctxt-equiv)))
 :rule-classes :congruence)