• 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

Gen-block-item-list-thm

Generate a theorem for the transformation of a list of block items.

Signature

(gen-block-item-list-thm old new vartys const-new thm-index hints) 
  → 
(mv thm-event thm-name updated-thm-index)

Arguments

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

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

vartys — Guard (c::ident-type-mapp vartys).

const-new — Guard (symbolp const-new).

thm-index — Guard (posp thm-index).

hints — Guard (true-listp hints).

Returns

thm-event — Type (pseudo-event-formp thm-event).

thm-name — Type (symbolp thm-name).

updated-thm-index — Type (posp updated-thm-index).

Unlike gen-block-item-thm, here we have a single vartys instead of a vartys-pre and a vartys-post. This is intentional, because we are only interested in variables that will survive the scope of the list of block items, which are the variables in scope at the start of the list.

Definitions and Theorems

Function: gen-block-item-list-thm

(defun gen-block-item-list-thm
       (old new vartys const-new thm-index hints)
 (declare (xargs :guard (and (block-item-listp old)
                             (block-item-listp new)
                             (c::ident-type-mapp vartys)
                             (symbolp const-new)
                             (posp thm-index)
                             (true-listp hints))))
 (declare (xargs :guard (and (block-item-list-unambp old)
                             (block-item-list-annop old)
                             (block-item-list-unambp new)
                             (block-item-list-annop new))))
 (let ((__function__ 'gen-block-item-list-thm))
  (declare (ignorable __function__))
  (b*
   ((old (block-item-list-fix old))
    (new (block-item-list-fix new))
    ((unless (block-item-list-formalp old))
     (raise "Internal error: ~x0 is not in the formalized subset."
            old)
     (mv '(_) nil 1))
    ((unless (block-item-list-formalp new))
     (raise "Internal error: ~x0 is not in the formalized subset."
            new)
     (mv '(_) nil 1))
    (types (block-item-list-types old))
    ((unless (equal (block-item-list-types new)
                    types))
     (raise
      "Internal error: ~
                the types ~x0 of the new block item list ~x1 differ from ~
                the types ~x2 of the old block item list ~x3."
      (block-item-list-types new)
      new types old)
     (mv '(_) nil 1))
    (vars-pre (gen-var-assertions vartys 'compst))
    ((mv & old-items)
     (ldm-block-item-list old))
    ((mv & new-items)
     (ldm-block-item-list new))
    ((mv & ctypes)
     (ldm-type-option-set types))
    (formula
     (cons
      'b*
      (cons
       (cons (cons 'old-items
                   (cons (cons 'quote (cons old-items 'nil))
                         'nil))
             (cons (cons 'new-items
                         (cons (cons 'quote (cons new-items 'nil))
                               'nil))
                   '(((mv old-result old-compst)
                      (c::exec-block-item-list
                           old-items compst old-fenv limit))
                     ((mv new-result new-compst)
                      (c::exec-block-item-list
                           new-items compst new-fenv limit)))))
       (cons
        (cons
         'implies
         (cons
          (cons 'and
                (cons '(> (c::compustate-frames-number compst)
                          0)
                      (append vars-pre
                              '((not (c::errorp old-result))))))
          (cons
           (cons
            'and
            (cons
             '(not (c::errorp new-result))
             (cons
              '(equal old-result new-result)
              (cons
               '(equal old-compst new-compst)
               (cons
                (cons
                    'in
                    (cons '(c::type-option-of-stmt-value old-result)
                          (cons (cons 'quote (cons ctypes 'nil))
                                'nil)))
                'nil)))))
           'nil)))
        'nil))))
    ((mv thm-name thm-index)
     (gen-thm-name const-new thm-index))
    (thm-event
     (cons
      'defrule
      (cons
           thm-name
           (cons formula
                 (cons ':rule-classes
                       (cons 'nil
                             (cons ':hints (cons hints 'nil)))))))))
   (mv thm-event thm-name thm-index))))

Theorem: pseudo-event-formp-of-gen-block-item-list-thm.thm-event

(defthm pseudo-event-formp-of-gen-block-item-list-thm.thm-event
 (b*
  (((mv ?thm-event ?thm-name ?updated-thm-index)
    (gen-block-item-list-thm old
                             new vartys const-new thm-index hints)))
  (pseudo-event-formp thm-event))
 :rule-classes :rewrite)

Theorem: symbolp-of-gen-block-item-list-thm.thm-name

(defthm symbolp-of-gen-block-item-list-thm.thm-name
 (b*
  (((mv ?thm-event ?thm-name ?updated-thm-index)
    (gen-block-item-list-thm old
                             new vartys const-new thm-index hints)))
  (symbolp thm-name))
 :rule-classes :rewrite)

Theorem: posp-of-gen-block-item-list-thm.updated-thm-index

(defthm posp-of-gen-block-item-list-thm.updated-thm-index
 (b*
  (((mv ?thm-event ?thm-name ?updated-thm-index)
    (gen-block-item-list-thm old
                             new vartys const-new thm-index hints)))
  (posp updated-thm-index))
 :rule-classes :rewrite)

Theorem: gen-block-item-list-thm-of-block-item-list-fix-old

(defthm gen-block-item-list-thm-of-block-item-list-fix-old
 (equal
    (gen-block-item-list-thm (block-item-list-fix old)
                             new vartys const-new thm-index hints)
    (gen-block-item-list-thm old
                             new vartys const-new thm-index hints)))

Theorem: gen-block-item-list-thm-block-item-list-equiv-congruence-on-old

(defthm
    gen-block-item-list-thm-block-item-list-equiv-congruence-on-old
 (implies
  (c$::block-item-list-equiv old old-equiv)
  (equal
    (gen-block-item-list-thm old
                             new vartys const-new thm-index hints)
    (gen-block-item-list-thm old-equiv
                             new vartys const-new thm-index hints)))
 :rule-classes :congruence)

Theorem: gen-block-item-list-thm-of-block-item-list-fix-new

(defthm gen-block-item-list-thm-of-block-item-list-fix-new
 (equal
    (gen-block-item-list-thm old (block-item-list-fix new)
                             vartys const-new thm-index hints)
    (gen-block-item-list-thm old
                             new vartys const-new thm-index hints)))

Theorem: gen-block-item-list-thm-block-item-list-equiv-congruence-on-new

(defthm
    gen-block-item-list-thm-block-item-list-equiv-congruence-on-new
 (implies
  (c$::block-item-list-equiv new new-equiv)
  (equal
      (gen-block-item-list-thm old
                               new vartys const-new thm-index hints)
      (gen-block-item-list-thm old new-equiv
                               vartys const-new thm-index hints)))
 :rule-classes :congruence)