• 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
          • Split-gso
          • Wrap-fn
          • Constant-propagation
          • Specialize
          • Split-fn
          • Split-fn-when
          • Split-all-gso
          • Copy-fn
          • Variables-in-computation-states
            • C::compustate-has-var-with-type-p
            • Exec-compustate-vars-theorems
            • C::compustate-has-vars-with-types-p
            • C::compustate-has-var-with-type-p-of-exit-exec-enter
            • C::compustate-has-vars-with-types-p-of-exit-exec-enter
            • C::compustate-has-vars-with-types-p-of-enter-scope
            • C::compustate-has-var-with-type-p-of-enter-scope
          • 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

• Variables-in-computation-states

Exec-compustate-vars-theorems

Theorems about variables in computation states w.r.t. execution.

These theorems are about c::compustate-has-var-with-type-p, and how the execution of constructs preserve and/or modify it.

Definitions and Theorems

Theorem: expr-ident-compustate-vars

(defthm expr-ident-compustate-vars
  (b* ((expr (c::expr-ident var))
       (result (c::exec-expr-pure expr compst))
       (value (c::expr-value->value result)))
    (implies (c::compustate-has-var-with-type-p var type compst)
             (equal (c::type-of-value value)
                    (c::type-fix type)))))

Theorem: expr-compustate-vars

(defthm expr-compustate-vars
 (b* (((mv result compst1)
       (c::exec-expr expr compst fenv limit)))
  (implies (and (not (c::errorp result))
                (c::compustate-has-var-with-type-p var type compst))
           (c::compustate-has-var-with-type-p var type compst1))))

Theorem: expr-compustate-vars-multi

(defthm expr-compustate-vars-multi
 (b* (((mv eval compst1)
       (c::exec-expr expr compst fenv limit)))
  (implies (and (> (c::compustate-frames-number compst)
                   0)
                (not (c::errorp eval))
                (c::compustate-has-vars-with-types-p vartys compst))
           (c::compustate-has-vars-with-types-p vartys compst1))))

Theorem: stmt-compustate-vars

(defthm stmt-compustate-vars
 (b* (((mv sval compst1)
       (c::exec-stmt stmt compst fenv limit)))
  (implies (and (> (c::compustate-frames-number compst)
                   0)
                (not (c::errorp sval))
                (c::compustate-has-var-with-type-p var type compst))
           (c::compustate-has-var-with-type-p var type compst1))))

Theorem: stmt-compustate-vars-multi

(defthm stmt-compustate-vars-multi
 (b* (((mv sval compst1)
       (c::exec-stmt stmt compst fenv limit)))
  (implies (and (> (c::compustate-frames-number compst)
                   0)
                (not (c::errorp sval))
                (c::compustate-has-vars-with-types-p vartys compst))
           (c::compustate-has-vars-with-types-p vartys compst1))))

Theorem: initer-compustate-vars

(defthm initer-compustate-vars
 (b* (((mv result compst1)
       (c::exec-initer initer compst fenv limit)))
  (implies (and (> (c::compustate-frames-number compst)
                   0)
                (not (c::errorp result))
                (c::compustate-has-var-with-type-p var type compst))
           (c::compustate-has-var-with-type-p var type compst1))))

Theorem: decl-decl-compustate-vars-old

(defthm decl-decl-compustate-vars-old
  (b* ((declor (c::obj-declon->declor declon))
       (var (c::obj-declor-ident->get declor))
       (initer (c::obj-declon->init? declon))
       ((mv & compst0)
        (c::exec-initer initer compst fenv (1- limit)))
       (compst1 (c::exec-obj-declon declon compst fenv limit)))
    (implies
         (and (equal (c::obj-declon->scspec declon)
                     (c::scspecseq-none))
              (equal (c::obj-declor-kind declor)
                     :ident)
              (not (c::errorp compst1))
              (c::identp var1)
              (not (equal var var1))
              (c::compustate-has-var-with-type-p var1 type compst0))
         (c::compustate-has-var-with-type-p var1 type compst1))))

Theorem: decl-decl-compustate-vars-new

(defthm decl-decl-compustate-vars-new
  (b* ((declor (c::obj-declon->declor declon))
       (tyspecs (c::obj-declon->tyspec declon))
       (compst1 (c::exec-obj-declon declon compst fenv limit)))
    (implies (and (equal (c::obj-declon->scspec declon)
                         (c::scspecseq-none))
                  (equal (c::obj-declor-kind declor)
                         :ident)
                  (equal type (c::tyspecseq-to-type tyspecs))
                  (equal var (c::obj-declor-ident->get declor))
                  (not (c::errorp compst1)))
             (c::compustate-has-var-with-type-p var type compst1))))

Theorem: block-item-stmt-compustate-vars

(defthm block-item-stmt-compustate-vars
  (b* ((stmt (c::block-item-stmt->get item))
       ((mv & compst0)
        (c::exec-stmt stmt compst fenv (1- limit)))
       ((mv result compst1)
        (c::exec-block-item item compst fenv limit)))
    (implies
         (and (equal (c::block-item-kind item) :stmt)
              (not (c::errorp result))
              (c::compustate-has-var-with-type-p var type compst0))
         (c::compustate-has-var-with-type-p var type compst1))))

Theorem: block-item-decl-compustate-vars

(defthm block-item-decl-compustate-vars
  (b* ((declon (c::block-item-declon->get item))
       (compst0 (c::exec-obj-declon declon compst fenv (1- limit)))
       ((mv result compst1)
        (c::exec-block-item item compst fenv limit)))
    (implies
         (and (equal (c::block-item-kind item)
                     :declon)
              (not (c::errorp result))
              (c::compustate-has-var-with-type-p var type compst0))
         (c::compustate-has-var-with-type-p var type compst1))))

Theorem: block-item-list-empty-compustate-vars

(defthm block-item-list-empty-compustate-vars
 (b* (((mv result compst1)
       (c::exec-block-item-list items compst fenv limit)))
  (implies (and (equal items nil)
                (not (c::errorp result))
                (c::compustate-has-var-with-type-p var type compst))
           (c::compustate-has-var-with-type-p var type compst1))))

Theorem: block-item-list-cons-compustate-vars

(defthm block-item-list-cons-compustate-vars
 (b* ((item (car item+items))
      (items (cdr item+items))
      ((mv result0 compst0)
       (c::exec-block-item item compst fenv (1- limit)))
      ((mv & compst1)
       (c::exec-block-item-list items compst0 fenv (1- limit)))
      ((mv result2 compst2)
       (c::exec-block-item-list item+items compst fenv limit)))
  (implies
   (and
    (consp item+items)
    (not (c::errorp result2))
    (or (and (equal (c::stmt-value-kind result0)
                    :return)
             (c::compustate-has-var-with-type-p var type compst0))
        (and (equal (c::stmt-value-kind result0)
                    :none)
             (c::compustate-has-var-with-type-p var type compst1))))
   (c::compustate-has-var-with-type-p var type compst2))))