• 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-binary
            • Xeq-block-item-list-cons
            • Xeq-stmt-ifelse
            • Xeq-expr-cond
            • Xeq-expr-const
            • Gen-param-thms
            • Gen-expr-thm
            • Gen-from-params
            • Xeq-decl-decl
            • Xeq-expr-unary
            • Xeq-stmt-dowhile
            • Xeq-expr-cast
            • Lift-expr-pure-thm
            • Xeq-stmt-while
            • Gout
            • Gen-block-item-list-thm
            • Xeq-stmt-if
            • Gin
            • Xeq-expr-ident
            • Gen-expr-pure-thm
            • Gen-block-item-thm
            • Xeq-stmt-expr
            • Gen-initer-single-thm
            • Gen-init-scope-thm
            • Xeq-stmt-return
            • Gen-decl-thm
            • Gen-stmt-thm
            • Xeq-block-item-decl
            • Xeq-initer-single
            • Xeq-block-item-stmt
            • Xeq-stmt-compound
            • 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-block-item-list-cons

Equality lifting transformation of a non-empty list of block items.

Signature

(xeq-block-item-list-cons item item-new item-thm-name 
                          items items-new items-thm-name gin) 
 
  → 
(mv item+items gout)

Arguments

item — Guard (block-itemp item).

item-new — Guard (block-itemp item-new).

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

items — Guard (block-item-listp items).

items-new — Guard (block-item-listp items-new).

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

gin — Guard (ginp gin).

Returns

item+items — Type (block-item-listp item+items).

gout — Type (goutp gout).

The resulting list of block items is obtained by consing the possibly transformed first item and the possibly transformed rest of the items.

We generate a theorem iff theorems were generated for both the first item and (the list of) the rest of the items.

Definitions and Theorems

Function: xeq-block-item-list-cons

(defun xeq-block-item-list-cons
       (item item-new item-thm-name
             items items-new items-thm-name gin)
 (declare (xargs :guard (and (block-itemp item)
                             (block-itemp item-new)
                             (symbolp item-thm-name)
                             (block-item-listp items)
                             (block-item-listp items-new)
                             (symbolp items-thm-name)
                             (ginp gin))))
 (declare (xargs :guard (and (block-item-unambp item)
                             (block-item-annop item)
                             (block-item-unambp item-new)
                             (block-item-annop item-new)
                             (block-item-list-unambp items)
                             (block-item-list-annop items)
                             (block-item-list-unambp items-new)
                             (block-item-list-annop items-new))))
 (let ((__function__ 'xeq-block-item-list-cons))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (item (block-item-fix item))
    (items (block-item-list-fix items))
    (item-new (block-item-fix item-new))
    (items-new (block-item-list-fix items-new))
    (item+items (cons item items))
    (item+items-new (cons item-new items-new))
    (gout-no-thm (gout-no-thm gin))
    ((unless (and item-thm-name items-thm-name))
     (mv item+items-new gout-no-thm))
    (first-types (block-item-types item))
    (rest-types (block-item-list-types items))
    ((mv & old-item) (ldm-block-item item))
    ((mv & new-item)
     (ldm-block-item item-new))
    ((mv & old-items)
     (ldm-block-item-list items))
    ((mv & new-items)
     (ldm-block-item-list items-new))
    ((mv & first-ctypes)
     (ldm-type-option-set first-types))
    ((mv & rest-ctypes)
     (ldm-type-option-set rest-types))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''(c::stmt-value-kind-possibilities
               (:e delete)
               (:e union)
               c::compustate-frames-number-of-exec-block-item
               c::compustatep-when-compustate-resultp-and-not-errorp
               block-item-list-cons-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons item-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               items-thm-name
               (cons
                (cons
                 'compst
                 (cons
                  (cons
                   'mv-nth
                   (cons
                    '1
                    (cons
                      (cons 'c::exec-block-item
                            (cons (cons 'quote (cons old-item 'nil))
                                  '(compst old-fenv (1- limit))))
                      'nil)))
                  'nil))
                '((limit (1- limit))))))
             (cons
              (cons
               ':instance
               (cons
                'block-item-list-cons-first-congruence
                (cons
                 (cons 'old-item
                       (cons (cons 'quote (cons old-item 'nil))
                             'nil))
                 (cons
                  (cons 'old-items
                        (cons (cons 'quote (cons old-items 'nil))
                              'nil))
                  (cons
                   (cons 'new-item
                         (cons (cons 'quote (cons new-item 'nil))
                               'nil))
                   (cons
                    (cons 'new-items
                          (cons (cons 'quote (cons new-items 'nil))
                                'nil))
                    (cons
                     (cons
                        'first-types
                        (cons (cons 'quote (cons first-ctypes 'nil))
                              'nil))
                     (cons
                      (cons
                         'rest-types
                         (cons (cons 'quote (cons rest-ctypes 'nil))
                               'nil))
                      'nil))))))))
              (cons
               (cons
                ':instance
                (cons
                 'block-item-list-cons-rest-congruence
                 (cons
                  (cons 'old-item
                        (cons (cons 'quote (cons old-item 'nil))
                              'nil))
                  (cons
                   (cons 'old-items
                         (cons (cons 'quote (cons old-items 'nil))
                               'nil))
                   (cons
                    (cons 'new-item
                          (cons (cons 'quote (cons new-item 'nil))
                                'nil))
                    (cons
                     (cons 'new-items
                           (cons (cons 'quote (cons new-items 'nil))
                                 'nil))
                     (cons
                      (cons
                        'first-types
                        (cons (cons 'quote (cons first-ctypes 'nil))
                              'nil))
                      (cons
                       (cons
                         'rest-types
                         (cons (cons 'quote (cons rest-ctypes 'nil))
                               'nil))
                       'nil))))))))
               (cons
                (cons
                 ':instance
                 (cons
                  'block-item-list-cons-first-errors
                  (cons
                   (cons 'item
                         (cons (cons 'quote (cons old-item 'nil))
                               'nil))
                   (cons
                     (cons 'items
                           (cons (cons 'quote (cons old-items 'nil))
                                 'nil))
                     '((fenv old-fenv))))))
                (cons
                 (cons
                  ':instance
                  (cons
                   'block-item-list-cons-rest-errors
                   (cons
                    (cons 'item
                          (cons (cons 'quote (cons old-item 'nil))
                                'nil))
                    (cons
                     (cons 'items
                           (cons (cons 'quote (cons old-items 'nil))
                                 'nil))
                     '((fenv old-fenv))))))
                 'nil))))))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-block-item-list-thm item+items item+items-new gin.vartys
                              gin.const-new gin.thm-index hints)))
   (mv item+items-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: block-item-listp-of-xeq-block-item-list-cons.item+items

(defthm block-item-listp-of-xeq-block-item-list-cons.item+items
  (b*
   (((mv ?item+items ?gout)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))
   (block-item-listp item+items))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-block-item-list-cons.gout

(defthm goutp-of-xeq-block-item-list-cons.gout
  (b*
   (((mv ?item+items ?gout)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))
   (goutp gout))
  :rule-classes :rewrite)

Theorem: xeq-block-item-list-cons-of-block-item-fix-item

(defthm xeq-block-item-list-cons-of-block-item-fix-item
 (equal
     (xeq-block-item-list-cons (block-item-fix item)
                               item-new item-thm-name
                               items items-new items-thm-name gin)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))

Theorem: xeq-block-item-list-cons-block-item-equiv-congruence-on-item

(defthm xeq-block-item-list-cons-block-item-equiv-congruence-on-item
 (implies
  (c$::block-item-equiv item item-equiv)
  (equal
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)
     (xeq-block-item-list-cons item-equiv item-new item-thm-name
                               items items-new items-thm-name gin)))
 :rule-classes :congruence)

Theorem: xeq-block-item-list-cons-of-block-item-fix-item-new

(defthm xeq-block-item-list-cons-of-block-item-fix-item-new
 (equal
     (xeq-block-item-list-cons item (block-item-fix item-new)
                               item-thm-name
                               items items-new items-thm-name gin)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))

Theorem: xeq-block-item-list-cons-block-item-equiv-congruence-on-item-new

(defthm
   xeq-block-item-list-cons-block-item-equiv-congruence-on-item-new
 (implies
  (c$::block-item-equiv item-new item-new-equiv)
  (equal
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)
     (xeq-block-item-list-cons item item-new-equiv item-thm-name
                               items items-new items-thm-name gin)))
 :rule-classes :congruence)

Theorem: xeq-block-item-list-cons-of-block-item-list-fix-items

(defthm xeq-block-item-list-cons-of-block-item-list-fix-items
 (equal
     (xeq-block-item-list-cons item item-new item-thm-name
                               (block-item-list-fix items)
                               items-new items-thm-name gin)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))

Theorem: xeq-block-item-list-cons-block-item-list-equiv-congruence-on-items

(defthm
 xeq-block-item-list-cons-block-item-list-equiv-congruence-on-items
 (implies
  (c$::block-item-list-equiv items items-equiv)
  (equal
   (xeq-block-item-list-cons item item-new item-thm-name
                             items items-new items-thm-name gin)
   (xeq-block-item-list-cons item item-new item-thm-name items-equiv
                             items-new items-thm-name gin)))
 :rule-classes :congruence)

Theorem: xeq-block-item-list-cons-of-block-item-list-fix-items-new

(defthm xeq-block-item-list-cons-of-block-item-list-fix-items-new
 (equal
     (xeq-block-item-list-cons item item-new item-thm-name
                               items (block-item-list-fix items-new)
                               items-thm-name gin)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))

Theorem: xeq-block-item-list-cons-block-item-list-equiv-congruence-on-items-new

(defthm
 xeq-block-item-list-cons-block-item-list-equiv-congruence-on-items-new
 (implies
  (c$::block-item-list-equiv items-new items-new-equiv)
  (equal
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)
     (xeq-block-item-list-cons item item-new item-thm-name items
                               items-new-equiv items-thm-name gin)))
 :rule-classes :congruence)

Theorem: block-item-list-unambp-of-xeq-block-item-list-cons

(defthm block-item-list-unambp-of-xeq-block-item-list-cons
 (implies
  (and (block-item-unambp item-new)
       (block-item-list-unambp items-new))
  (b*
   (((mv ?item+items ?gout)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))
   (block-item-list-unambp item+items))))

Theorem: block-item-list-annop-of-xeq-block-item-list-cons

(defthm block-item-list-annop-of-xeq-block-item-list-cons
 (implies
  (and (block-item-annop item-new)
       (block-item-list-annop items-new))
  (b*
   (((mv ?item+items ?gout)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))
   (block-item-list-annop item+items))))

Theorem: block-item-list-aidentp-of-xeq-block-item-list-cons

(defthm block-item-list-aidentp-of-xeq-block-item-list-cons
 (implies
  (and (block-item-aidentp item-new gcc)
       (block-item-list-aidentp items-new gcc))
  (b*
   (((mv ?item+items ?gout)
     (xeq-block-item-list-cons item item-new item-thm-name
                               items items-new items-thm-name gin)))
   (block-item-list-aidentp item+items gcc))))