• 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
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
          • Concrete-syntax
          • Static-soundness
          • Static-semantics
            • Static-safety-checking
              • Check-safe-statements/blocks/cases/fundefs
                • Check-safe-statement
                • Check-safe-fundef
                • Check-safe-statement-list
                • Check-safe-block
                • Check-safe-swcase-list
                • Check-safe-block-option
                • Check-safe-swcase
              • Check-safe-expressions
              • Check-safe-fundef-list
              • Check-safe-variable-multi
              • Check-safe-variable-single
              • Check-safe-assign-multi
              • Check-safe-assign-single
              • Check-safe-path
              • Check-safe-extends-varset
              • Vars+modes
              • Add-vars
              • Add-var
              • Add-funtypes
              • Check-safe-literal
              • Funtype
              • Get-funtype
              • Check-var
              • Check-safe-top-block
              • Check-safe-path-list
              • Vars+modes-result
              • Funtype-result
              • Funtable-result
              • Funtable-for-fundefs
              • Funtype-for-fundef
              • Funtable
            • Static-shadowing-checking
            • Mode-set-result
            • Literal-evaluation
            • Static-identifier-checking
            • Static-safety-checking-evm
            • Mode-set
            • Modes
          • Errors
        • Yul-json
      • 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

• Static-safety-checking

Check-safe-statements/blocks/cases/fundefs

Check if statements, blocks, cases, and function definitions are safe.

These are checked in the context of a variable table for visible and accessible variables varset, and a function table funtab.

A successful check returns a set of possible modes in which execution may complete. The set of modes is used to check the conditions on the occurrence of leave, break, and continue statements described in [Yul: Specification of Yul: Restrictions on the Grammar]. The conditions there are phrased in terms of occurrences of constructs, but it is more convenient, in this formal static semantics, to check these conditions by putting restrictions on the possible modes statically calculated for statements and related constructs. This formulation is also more easily related to the dynamic semantics. At some point we may also formalize the conditions on the occurrence of leave, break, and continue statements described in [Yul: Specification of Yul: Restrictions on the Grammar], and show that they are equivalent to our formulation here.

Definitions and Theorems

Function: check-safe-statement

(defun check-safe-statement (stmt varset funtab)
 (declare (xargs :guard (and (statementp stmt)
                             (identifier-setp varset)
                             (funtablep funtab))))
 (let ((__function__ 'check-safe-statement))
  (declare (ignorable __function__))
  (statement-case
   stmt :block
   (b* (((okf modes)
         (check-safe-block stmt.get varset funtab)))
     (make-vars+modes :vars (identifier-set-fix varset)
                      :modes modes))
   :variable-single
   (b* (((okf varset)
         (check-safe-variable-single
              stmt.name stmt.init varset funtab)))
     (make-vars+modes :vars varset
                      :modes (insert (mode-regular) nil)))
   :variable-multi
   (b* (((okf varset)
         (check-safe-variable-multi
              stmt.names stmt.init varset funtab)))
     (make-vars+modes :vars varset
                      :modes (insert (mode-regular) nil)))
   :assign-single
   (b* (((okf &)
         (check-safe-assign-single
              stmt.target stmt.value varset funtab)))
     (make-vars+modes :vars (identifier-set-fix varset)
                      :modes (insert (mode-regular) nil)))
   :assign-multi
   (b* (((okf &)
         (check-safe-assign-multi
              stmt.targets stmt.value varset funtab)))
     (make-vars+modes :vars (identifier-set-fix varset)
                      :modes (insert (mode-regular) nil)))
   :funcall
   (b* (((okf results)
         (check-safe-funcall stmt.get varset funtab))
        ((unless (= results 0))
         (reserrf (list :discarded-values stmt.get))))
     (make-vars+modes :vars (identifier-set-fix varset)
                      :modes (insert (mode-regular) nil)))
   :if
   (b* (((okf results)
         (check-safe-expression stmt.test varset funtab))
        ((unless (= results 1))
         (reserrf (list :multi-valued-if-test stmt.test)))
        ((okf modes)
         (check-safe-block stmt.body varset funtab)))
     (make-vars+modes :vars (identifier-set-fix varset)
                      :modes (insert (mode-regular) modes)))
   :for
   (b* ((stmts (block->statements stmt.init))
        ((okf funtab)
         (add-funtypes (statements-to-fundefs stmts)
                       funtab))
        ((okf varsmodes)
         (check-safe-statement-list stmts varset funtab))
        (varset1 (vars+modes->vars varsmodes))
        (init-modes (vars+modes->modes varsmodes))
        ((when (in (mode-break) init-modes))
         (reserrf (list :break-in-loop-init stmt.init)))
        ((when (in (mode-continue) init-modes))
         (reserrf (list :continue-in-loop-init stmt.init)))
        ((okf results)
         (check-safe-expression stmt.test varset1 funtab))
        ((unless (= results 1))
         (reserrf (list :multi-valued-for-test stmt.test)))
        ((okf update-modes)
         (check-safe-block stmt.update varset1 funtab))
        ((when (in (mode-break) update-modes))
         (reserrf (list :break-in-loop-update stmt.update)))
        ((when (in (mode-continue) update-modes))
         (reserrf (list :continue-in-loop-update stmt.update)))
        ((okf body-modes)
         (check-safe-block stmt.body varset1 funtab))
        (modes (if (or (in (mode-leave) init-modes)
                       (in (mode-leave) update-modes)
                       (in (mode-leave) body-modes))
                   (insert (mode-leave)
                           (insert (mode-regular) nil))
                 (insert (mode-regular) nil))))
     (make-vars+modes :vars (identifier-set-fix varset)
                      :modes modes))
   :switch
   (b*
    (((okf results)
      (check-safe-expression stmt.target varset funtab))
     ((unless (= results 1))
      (reserrf (list :multi-valued-switch-target stmt.target)))
     ((unless (or (consp stmt.cases) stmt.default))
      (reserrf (list :no-cases-in-switch (statement-fix stmt))))
     ((unless
        (no-duplicatesp-equal (swcase-list->value-list stmt.cases)))
      (reserrf (list :duplicate-switch-cases (statement-fix stmt))))
     ((okf cases-modes)
      (check-safe-swcase-list stmt.cases varset funtab))
     ((okf default-modes)
      (check-safe-block-option stmt.default varset funtab)))
    (make-vars+modes :vars (identifier-set-fix varset)
                     :modes (union cases-modes default-modes)))
   :leave
   (make-vars+modes :vars (identifier-set-fix varset)
                    :modes (insert (mode-leave) nil))
   :break
   (make-vars+modes :vars (identifier-set-fix varset)
                    :modes (insert (mode-break) nil))
   :continue
   (make-vars+modes :vars (identifier-set-fix varset)
                    :modes (insert (mode-continue) nil))
   :fundef
   (b* (((okf &)
         (check-safe-fundef stmt.get funtab)))
     (make-vars+modes :vars (identifier-set-fix varset)
                      :modes (insert (mode-regular) nil))))))

Function: check-safe-statement-list

(defun check-safe-statement-list (stmts varset funtab)
  (declare (xargs :guard (and (statement-listp stmts)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-statement-list))
    (declare (ignorable __function__))
    (b* (((when (endp stmts))
          (make-vars+modes :vars (identifier-set-fix varset)
                           :modes (insert (mode-regular) nil)))
         ((okf varsmodes)
          (check-safe-statement (car stmts)
                                varset funtab))
         (varset (vars+modes->vars varsmodes))
         (first-modes (vars+modes->modes varsmodes))
         ((okf varsmodes)
          (check-safe-statement-list (cdr stmts)
                                     varset funtab))
         (varset (vars+modes->vars varsmodes))
         (rest-modes (vars+modes->modes varsmodes))
         (modes (if (in (mode-regular) first-modes)
                    (union first-modes rest-modes)
                  first-modes)))
      (make-vars+modes :vars varset
                       :modes modes))))

Function: check-safe-block

(defun check-safe-block (block varset funtab)
  (declare (xargs :guard (and (blockp block)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-block))
    (declare (ignorable __function__))
    (b* ((stmts (block->statements block))
         ((okf funtab)
          (add-funtypes (statements-to-fundefs stmts)
                        funtab))
         ((okf varsmodes)
          (check-safe-statement-list stmts varset funtab)))
      (vars+modes->modes varsmodes))))

Function: check-safe-block-option

(defun check-safe-block-option (block? varset funtab)
  (declare (xargs :guard (and (block-optionp block?)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-block-option))
    (declare (ignorable __function__))
    (block-option-case
         block?
         :none (insert (mode-regular) nil)
         :some (check-safe-block (block-option-some->val block?)
                                 varset funtab))))

Function: check-safe-swcase

(defun check-safe-swcase (case varset funtab)
  (declare (xargs :guard (and (swcasep case)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-swcase))
    (declare (ignorable __function__))
    (b* (((swcase case) case)
         ((okf &)
          (check-safe-literal case.value)))
      (check-safe-block case.body varset funtab))))

Function: check-safe-swcase-list

(defun check-safe-swcase-list (cases varset funtab)
  (declare (xargs :guard (and (swcase-listp cases)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-swcase-list))
    (declare (ignorable __function__))
    (b* (((when (endp cases)) nil)
         ((okf first-modes)
          (check-safe-swcase (car cases)
                             varset funtab))
         ((okf rest-modes)
          (check-safe-swcase-list (cdr cases)
                                  varset funtab)))
      (union first-modes rest-modes))))

Function: check-safe-fundef

(defun check-safe-fundef (fundef funtab)
 (declare (xargs :guard (and (fundefp fundef)
                             (funtablep funtab))))
 (let ((__function__ 'check-safe-fundef))
   (declare (ignorable __function__))
   (b*
    (((fundef fundef) fundef)
     ((okf varset)
      (add-vars fundef.inputs nil))
     ((okf varset)
      (add-vars fundef.outputs varset))
     ((okf modes)
      (check-safe-block fundef.body varset funtab))
     ((when (in (mode-break) modes))
      (reserrf (list :break-from-function (fundef-fix fundef))))
     ((when (in (mode-continue) modes))
      (reserrf (list :continue-from-function (fundef-fix fundef)))))
    nil)))

Theorem: return-type-of-check-safe-statement.varsmodes

(defthm return-type-of-check-safe-statement.varsmodes
  (b* ((?varsmodes (check-safe-statement stmt varset funtab)))
    (vars+modes-resultp varsmodes))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-statement-list.varsmodes

(defthm return-type-of-check-safe-statement-list.varsmodes
  (b* ((?varsmodes (check-safe-statement-list stmts varset funtab)))
    (vars+modes-resultp varsmodes))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-block.modes

(defthm return-type-of-check-safe-block.modes
  (b* ((?modes (check-safe-block block varset funtab)))
    (mode-set-resultp modes))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-block-option.modes

(defthm return-type-of-check-safe-block-option.modes
  (b* ((?modes (check-safe-block-option block? varset funtab)))
    (mode-set-resultp modes))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-swcase.modes

(defthm return-type-of-check-safe-swcase.modes
  (b* ((?modes (check-safe-swcase case varset funtab)))
    (mode-set-resultp modes))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-swcase-list.modes

(defthm return-type-of-check-safe-swcase-list.modes
  (b* ((?modes (check-safe-swcase-list cases varset funtab)))
    (mode-set-resultp modes))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-fundef._

(defthm return-type-of-check-safe-fundef._
  (b* ((?_ (check-safe-fundef fundef funtab)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-safe-statement-of-statement-fix-stmt

(defthm check-safe-statement-of-statement-fix-stmt
  (equal (check-safe-statement (statement-fix stmt)
                               varset funtab)
         (check-safe-statement stmt varset funtab)))

Theorem: check-safe-statement-of-identifier-set-fix-varset

(defthm check-safe-statement-of-identifier-set-fix-varset
  (equal (check-safe-statement stmt (identifier-set-fix varset)
                               funtab)
         (check-safe-statement stmt varset funtab)))

Theorem: check-safe-statement-of-funtable-fix-funtab

(defthm check-safe-statement-of-funtable-fix-funtab
  (equal (check-safe-statement stmt varset (funtable-fix funtab))
         (check-safe-statement stmt varset funtab)))

Theorem: check-safe-statement-list-of-statement-list-fix-stmts

(defthm check-safe-statement-list-of-statement-list-fix-stmts
  (equal (check-safe-statement-list (statement-list-fix stmts)
                                    varset funtab)
         (check-safe-statement-list stmts varset funtab)))

Theorem: check-safe-statement-list-of-identifier-set-fix-varset

(defthm check-safe-statement-list-of-identifier-set-fix-varset
 (equal (check-safe-statement-list stmts (identifier-set-fix varset)
                                   funtab)
        (check-safe-statement-list stmts varset funtab)))

Theorem: check-safe-statement-list-of-funtable-fix-funtab

(defthm check-safe-statement-list-of-funtable-fix-funtab
 (equal
      (check-safe-statement-list stmts varset (funtable-fix funtab))
      (check-safe-statement-list stmts varset funtab)))

Theorem: check-safe-block-of-block-fix-block

(defthm check-safe-block-of-block-fix-block
  (equal (check-safe-block (block-fix block)
                           varset funtab)
         (check-safe-block block varset funtab)))

Theorem: check-safe-block-of-identifier-set-fix-varset

(defthm check-safe-block-of-identifier-set-fix-varset
  (equal (check-safe-block block (identifier-set-fix varset)
                           funtab)
         (check-safe-block block varset funtab)))

Theorem: check-safe-block-of-funtable-fix-funtab

(defthm check-safe-block-of-funtable-fix-funtab
  (equal (check-safe-block block varset (funtable-fix funtab))
         (check-safe-block block varset funtab)))

Theorem: check-safe-block-option-of-block-option-fix-block?

(defthm check-safe-block-option-of-block-option-fix-block?
  (equal (check-safe-block-option (block-option-fix block?)
                                  varset funtab)
         (check-safe-block-option block? varset funtab)))

Theorem: check-safe-block-option-of-identifier-set-fix-varset

(defthm check-safe-block-option-of-identifier-set-fix-varset
  (equal (check-safe-block-option block? (identifier-set-fix varset)
                                  funtab)
         (check-safe-block-option block? varset funtab)))

Theorem: check-safe-block-option-of-funtable-fix-funtab

(defthm check-safe-block-option-of-funtable-fix-funtab
  (equal
       (check-safe-block-option block? varset (funtable-fix funtab))
       (check-safe-block-option block? varset funtab)))

Theorem: check-safe-swcase-of-swcase-fix-case

(defthm check-safe-swcase-of-swcase-fix-case
  (equal (check-safe-swcase (swcase-fix case)
                            varset funtab)
         (check-safe-swcase case varset funtab)))

Theorem: check-safe-swcase-of-identifier-set-fix-varset

(defthm check-safe-swcase-of-identifier-set-fix-varset
  (equal (check-safe-swcase case (identifier-set-fix varset)
                            funtab)
         (check-safe-swcase case varset funtab)))

Theorem: check-safe-swcase-of-funtable-fix-funtab

(defthm check-safe-swcase-of-funtable-fix-funtab
  (equal (check-safe-swcase case varset (funtable-fix funtab))
         (check-safe-swcase case varset funtab)))

Theorem: check-safe-swcase-list-of-swcase-list-fix-cases

(defthm check-safe-swcase-list-of-swcase-list-fix-cases
  (equal (check-safe-swcase-list (swcase-list-fix cases)
                                 varset funtab)
         (check-safe-swcase-list cases varset funtab)))

Theorem: check-safe-swcase-list-of-identifier-set-fix-varset

(defthm check-safe-swcase-list-of-identifier-set-fix-varset
  (equal (check-safe-swcase-list cases (identifier-set-fix varset)
                                 funtab)
         (check-safe-swcase-list cases varset funtab)))

Theorem: check-safe-swcase-list-of-funtable-fix-funtab

(defthm check-safe-swcase-list-of-funtable-fix-funtab
  (equal (check-safe-swcase-list cases varset (funtable-fix funtab))
         (check-safe-swcase-list cases varset funtab)))

Theorem: check-safe-fundef-of-fundef-fix-fundef

(defthm check-safe-fundef-of-fundef-fix-fundef
  (equal (check-safe-fundef (fundef-fix fundef)
                            funtab)
         (check-safe-fundef fundef funtab)))

Theorem: check-safe-fundef-of-funtable-fix-funtab

(defthm check-safe-fundef-of-funtable-fix-funtab
  (equal (check-safe-fundef fundef (funtable-fix funtab))
         (check-safe-fundef fundef funtab)))

Theorem: check-safe-statement-statement-equiv-congruence-on-stmt

(defthm check-safe-statement-statement-equiv-congruence-on-stmt
  (implies (statement-equiv stmt stmt-equiv)
           (equal (check-safe-statement stmt varset funtab)
                  (check-safe-statement stmt-equiv varset funtab)))
  :rule-classes :congruence)

Theorem: check-safe-statement-identifier-set-equiv-congruence-on-varset

(defthm
     check-safe-statement-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-safe-statement stmt varset funtab)
                  (check-safe-statement stmt varset-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-statement-funtable-equiv-congruence-on-funtab

(defthm check-safe-statement-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (check-safe-statement stmt varset funtab)
                  (check-safe-statement stmt varset funtab-equiv)))
  :rule-classes :congruence)

Theorem: check-safe-statement-list-statement-list-equiv-congruence-on-stmts

(defthm
 check-safe-statement-list-statement-list-equiv-congruence-on-stmts
 (implies
      (statement-list-equiv stmts stmts-equiv)
      (equal (check-safe-statement-list stmts varset funtab)
             (check-safe-statement-list stmts-equiv varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-statement-list-identifier-set-equiv-congruence-on-varset

(defthm
 check-safe-statement-list-identifier-set-equiv-congruence-on-varset
 (implies
      (identifier-set-equiv varset varset-equiv)
      (equal (check-safe-statement-list stmts varset funtab)
             (check-safe-statement-list stmts varset-equiv funtab)))
 :rule-classes :congruence)

Theorem: check-safe-statement-list-funtable-equiv-congruence-on-funtab

(defthm
      check-safe-statement-list-funtable-equiv-congruence-on-funtab
 (implies
      (funtable-equiv funtab funtab-equiv)
      (equal (check-safe-statement-list stmts varset funtab)
             (check-safe-statement-list stmts varset funtab-equiv)))
 :rule-classes :congruence)

Theorem: check-safe-block-block-equiv-congruence-on-block

(defthm check-safe-block-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (check-safe-block block varset funtab)
                  (check-safe-block block-equiv varset funtab)))
  :rule-classes :congruence)

Theorem: check-safe-block-identifier-set-equiv-congruence-on-varset

(defthm check-safe-block-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-safe-block block varset funtab)
                  (check-safe-block block varset-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-block-funtable-equiv-congruence-on-funtab

(defthm check-safe-block-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (check-safe-block block varset funtab)
                  (check-safe-block block varset funtab-equiv)))
  :rule-classes :congruence)

Theorem: check-safe-block-option-block-option-equiv-congruence-on-block?

(defthm
    check-safe-block-option-block-option-equiv-congruence-on-block?
  (implies
       (block-option-equiv block? block?-equiv)
       (equal (check-safe-block-option block? varset funtab)
              (check-safe-block-option block?-equiv varset funtab)))
  :rule-classes :congruence)

Theorem: check-safe-block-option-identifier-set-equiv-congruence-on-varset

(defthm
  check-safe-block-option-identifier-set-equiv-congruence-on-varset
  (implies
       (identifier-set-equiv varset varset-equiv)
       (equal (check-safe-block-option block? varset funtab)
              (check-safe-block-option block? varset-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-block-option-funtable-equiv-congruence-on-funtab

(defthm check-safe-block-option-funtable-equiv-congruence-on-funtab
  (implies
       (funtable-equiv funtab funtab-equiv)
       (equal (check-safe-block-option block? varset funtab)
              (check-safe-block-option block? varset funtab-equiv)))
  :rule-classes :congruence)

Theorem: check-safe-swcase-swcase-equiv-congruence-on-case

(defthm check-safe-swcase-swcase-equiv-congruence-on-case
  (implies (swcase-equiv case case-equiv)
           (equal (check-safe-swcase case varset funtab)
                  (check-safe-swcase case-equiv varset funtab)))
  :rule-classes :congruence)

Theorem: check-safe-swcase-identifier-set-equiv-congruence-on-varset

(defthm check-safe-swcase-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-safe-swcase case varset funtab)
                  (check-safe-swcase case varset-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-swcase-funtable-equiv-congruence-on-funtab

(defthm check-safe-swcase-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (check-safe-swcase case varset funtab)
                  (check-safe-swcase case varset funtab-equiv)))
  :rule-classes :congruence)

Theorem: check-safe-swcase-list-swcase-list-equiv-congruence-on-cases

(defthm check-safe-swcase-list-swcase-list-equiv-congruence-on-cases
  (implies
       (swcase-list-equiv cases cases-equiv)
       (equal (check-safe-swcase-list cases varset funtab)
              (check-safe-swcase-list cases-equiv varset funtab)))
  :rule-classes :congruence)

Theorem: check-safe-swcase-list-identifier-set-equiv-congruence-on-varset

(defthm
   check-safe-swcase-list-identifier-set-equiv-congruence-on-varset
  (implies
       (identifier-set-equiv varset varset-equiv)
       (equal (check-safe-swcase-list cases varset funtab)
              (check-safe-swcase-list cases varset-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-swcase-list-funtable-equiv-congruence-on-funtab

(defthm check-safe-swcase-list-funtable-equiv-congruence-on-funtab
  (implies
       (funtable-equiv funtab funtab-equiv)
       (equal (check-safe-swcase-list cases varset funtab)
              (check-safe-swcase-list cases varset funtab-equiv)))
  :rule-classes :congruence)

Theorem: check-safe-fundef-fundef-equiv-congruence-on-fundef

(defthm check-safe-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (check-safe-fundef fundef funtab)
                  (check-safe-fundef fundef-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-fundef-funtable-equiv-congruence-on-funtab

(defthm check-safe-fundef-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (check-safe-fundef fundef funtab)
                  (check-safe-fundef fundef funtab-equiv)))
  :rule-classes :congruence)

Theorem: check-safe-block-option-when-blockp

(defthm check-safe-block-option-when-blockp
  (implies (blockp block)
           (equal (check-safe-block-option block varset funtab)
                  (check-safe-block block varset funtab))))

Subtopics

Check-safe-statement

Check if a statement is safe.

Check-safe-fundef

Check if a function definition is safe.

Check-safe-statement-list

Check if a list of statements is safe.

Check-safe-block

Check if a block is safe.

Check-safe-swcase-list

Check if a list of cases is safe.

Check-safe-block-option

Check if an optional block is safe.

Check-safe-swcase

Check if a case is safe.