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

Equality lifting transformation of a function definition.

Signature

(xeq-fundef extension spec spec-new declor 
            declor-new asm? attribs decls decls-new 
            body body-new body-thm-name info gin) 
 
  → 
(mv fundef gout)

Arguments

extension — Guard (booleanp extension).

spec — Guard (decl-spec-listp spec).

spec-new — Guard (decl-spec-listp spec-new).

declor — Guard (declorp declor).

declor-new — Guard (declorp declor-new).

asm? — Guard (asm-name-spec-optionp asm?).

attribs — Guard (attrib-spec-listp attribs).

decls — Guard (decl-listp decls).

decls-new — Guard (decl-listp decls-new).

body — Guard (comp-stmtp body).

body-new — Guard (comp-stmtp body-new).

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

info — Guard (fundef-infop info).

gin — Guard (ginp gin).

Returns

fundef — Type (fundefp fundef).

gout — Type (goutp gout).

We generate a theorem for the function only under certain conditions, including the fact that a theorem for the body gets generated.

We generate the following theorems:

• A theorem about the initial scope of the function body. See gen-init-scope-thm.
• For each function parameter, a theorem saying that, after pushing a frame with the initial scope above, the computation state has a variable for the parameter with the associated type.
• The main theorem for the function definition, saying that, if the execution of the old function does not yield an error, neither does the execition of the new function, and they return the same results and computation states.

We use gen-from-params to obtain certain information from the parameters, which is used to generate the theorems. This information includes the variable-type map corresponding to the function parameters: we ensure that it is the same as the variable-type map from the validation table that annotates the start of the function body. In general the former is a sub-map of the latter, because the validation table could include global variables; but for now proof generation does not handle global variables, so we generate proofs for the body only if the theorems about the initial scope and the parameters suffice to establish the variable-type hypotheses of the body.

The function may use global variables not hidden by parameters. No assertions about global variables are returned by gen-from-params. We generate them directly from gin.vartys, after removing from that map any keys that are also function parameters, which hide the corresponding global variables.

Definitions and Theorems

Function: xeq-fundef-loop

(defun xeq-fundef-loop (thms fun)
 (declare (xargs :guard (and (symbol-listp thms)
                             (stringp fun))))
 (let ((__function__ 'xeq-fundef-loop))
  (declare (ignorable __function__))
  (b*
   (((when (endp thms)) nil)
    (thm (car thms))
    (lemma-instance
     (cons
      ':instance
      (cons
       thm
       (cons
        (cons
         'fun
         (cons
          (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-ident
                                 (cons (cons 'ident (cons fun 'nil))
                                       'nil))
                           'nil)))
          'nil))
        '((compst0 compst))))))
    (more-lemma-instances (xeq-fundef-loop (cdr thms) fun)))
   (cons lemma-instance more-lemma-instances))))

Theorem: true-listp-of-xeq-fundef-loop

(defthm true-listp-of-xeq-fundef-loop
  (b* ((lemma-instances (xeq-fundef-loop thms fun)))
    (true-listp lemma-instances))
  :rule-classes :rewrite)

Function: xeq-fundef

(defun xeq-fundef (extension spec spec-new declor
                             declor-new asm? attribs decls decls-new
                             body body-new body-thm-name info gin)
 (declare (xargs :guard (and (booleanp extension)
                             (decl-spec-listp spec)
                             (decl-spec-listp spec-new)
                             (declorp declor)
                             (declorp declor-new)
                             (asm-name-spec-optionp asm?)
                             (attrib-spec-listp attribs)
                             (decl-listp decls)
                             (decl-listp decls-new)
                             (comp-stmtp body)
                             (comp-stmtp body-new)
                             (symbolp body-thm-name)
                             (fundef-infop info)
                             (ginp gin))))
 (declare (xargs :guard (and (decl-spec-list-unambp spec)
                             (decl-spec-list-annop spec)
                             (decl-spec-list-unambp spec-new)
                             (decl-spec-list-annop spec-new)
                             (declor-unambp declor)
                             (declor-annop declor)
                             (declor-unambp declor-new)
                             (declor-annop declor-new)
                             (decl-list-unambp decls)
                             (decl-list-annop decls)
                             (decl-list-unambp decls-new)
                             (decl-list-annop decls-new)
                             (comp-stmt-unambp body)
                             (comp-stmt-annop body)
                             (comp-stmt-unambp body-new)
                             (comp-stmt-annop body-new))))
 (let ((__function__ 'xeq-fundef))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (fundef (make-fundef :extension extension
                         :spec spec
                         :declor declor
                         :asm? asm?
                         :attribs attribs
                         :decls decls
                         :body body
                         :info info))
    (new-fundef (make-fundef :extension extension
                             :spec spec-new
                             :declor declor-new
                             :asm? asm?
                             :attribs attribs
                             :decls decls-new
                             :body body-new
                             :info info))
    (type (fundef-info->type info))
    (ident (declor->ident declor))
    (vartys-after-fundef (if (and (ident-formalp ident)
                                  (type-formalp type)
                                  (not (type-case type :void))
                                  (not (type-case type :char)))
                             (b* (((mv & cvar) (ldm-ident ident))
                                  ((mv & ctype) (ldm-type type)))
                               (omap::update cvar ctype gin.vartys))
                           gin.vartys))
    (gout-no-thm (change-gout (gout-no-thm gin)
                              :vartys vartys-after-fundef))
    ((unless body-thm-name)
     (mv new-fundef gout-no-thm))
    ((unless (fundef-formalp fundef))
     (mv new-fundef gout-no-thm))
    ((declor declor) declor)
    ((when (consp declor.pointers))
     (mv new-fundef gout-no-thm))
    ((mv okp params dirdeclor)
     (dirdeclor-case declor.direct
                     :function-params (mv t declor.direct.params
                                          declor.direct.declor)
                     :function-names (mv (endp declor.direct.names)
                                         nil declor.direct.declor)
                     :otherwise (mv nil nil (irr-dirdeclor))))
    ((unless okp)
     (mv new-fundef gout-no-thm))
    ((unless (dirdeclor-case dirdeclor :ident))
     (raise "Internal error: ~x0 is not just the function name."
            dirdeclor)
     (mv new-fundef (irr-gout)))
    (fun (ident->unwrap (dirdeclor-ident->ident dirdeclor)))
    ((unless (stringp fun))
     (raise "Internal error: non-string identifier ~x0."
            fun)
     (mv new-fundef (irr-gout)))
    ((mv erp ldm-params)
     (ldm-param-declon-list params))
    ((when erp) (mv new-fundef gout-no-thm))
    (types (fundef-types fundef))
    ((mv okp args parargs
         arg-types arg-types-compst param-vartys)
     (gen-from-params ldm-params gin))
    ((unless okp)
     (mv new-fundef gout-no-thm))
    ((mv init-scope-thm-event
         init-scope-thm-name thm-index)
     (gen-init-scope-thm ldm-params args parargs
                         arg-types gin.const-new gin.thm-index))
    (events (cons init-scope-thm-event gin.events))
    ((mv param-thm-events
         param-thm-names thm-index)
     (gen-param-thms arg-types-compst arg-types
                     ldm-params args init-scope-thm-name
                     gin.const-new thm-index))
    (events (append (rev param-thm-events) events))
    ((mv thm-name thm-index)
     (gen-thm-name gin.const-new thm-index))
    (global-vartys (omap::delete* (omap::keys param-vartys)
                                  gin.vartys))
    (global-vars-pre
     (gen-var-assertions
      global-vartys
      (cons
       'c::push-frame
       (cons
        (cons
         'c::frame
         (cons
          (cons 'quote (cons (c::ident fun) 'nil))
          (cons
           (cons
              'list
              (cons (cons 'c::init-scope
                          (cons (cons 'quote (cons ldm-params 'nil))
                                (cons (cons 'list args) 'nil)))
                    'nil))
           'nil)))
        '(compst)))))
    (formula
     (cons
      'b*
      (cons
       (cons
        (cons 'old
              (cons (cons 'quote
                          (cons (fundef-fix fundef) 'nil))
                    'nil))
        (cons
         (cons 'new
               (cons (cons 'quote (cons new-fundef 'nil))
                     'nil))
         (cons
          (cons
           'fun
           (cons
            (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-ident
                                 (cons (cons 'ident (cons fun 'nil))
                                       'nil))
                           'nil)))
            'nil))
          (cons
           (cons '(mv old-val old-compst)
                 (cons (cons 'c::exec-fun
                             (cons 'fun
                                   (cons (cons 'list args)
                                         '(compst old-fenv limit))))
                       'nil))
           (cons
            (cons
                 '(mv new-val new-compst)
                 (cons (cons 'c::exec-fun
                             (cons 'fun
                                   (cons (cons 'list args)
                                         '(compst new-fenv limit))))
                       'nil))
            'nil)))))
       (cons
        (cons
         'implies
         (cons
          (cons
            'and
            (append
                 global-vars-pre
                 (append arg-types
                         '((equal (c::fun-env-lookup fun old-fenv)
                                  (c::fun-info-from-fundef
                                       (mv-nth 1 (ldm-fundef old))))
                           (equal (c::fun-env-lookup fun new-fenv)
                                  (c::fun-info-from-fundef
                                       (mv-nth 1 (ldm-fundef new))))
                           (not (c::errorp old-val))))))
          (cons
           (cons
            'and
            (cons
             '(not (c::errorp new-val))
             (cons
              '(equal old-val new-val)
              (cons
               '(equal old-compst new-compst)
               (cons
                (cons
                 'in
                 (cons
                  '(c::type-of-value-option old-val)
                  (cons
                   (cons
                    'mv-nth
                    (cons
                     '1
                     (cons
                         (cons 'ldm-type-set
                               (cons (cons 'quote (cons types 'nil))
                                     'nil))
                         'nil)))
                   'nil)))
                'nil)))))
           'nil)))
        'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':expand
        (cons
         (cons
          (cons 'c::exec-fun
                (cons (cons 'quote (cons (c::ident fun) 'nil))
                      (cons (cons 'list args)
                            '(compst old-fenv limit))))
          (cons (cons 'c::exec-fun
                      (cons (cons 'quote (cons (c::ident fun) 'nil))
                            (cons (cons 'list args)
                                  '(compst new-fenv limit))))
                'nil))
         (cons
          ':use
          (cons
           (cons
            init-scope-thm-name
            (append
             (xeq-fundef-loop param-thm-names fun)
             (cons
              (cons
               ':instance
               (cons
                body-thm-name
                (cons
                 (cons
                  'compst
                  (cons
                   (cons
                    'c::push-frame
                    (cons
                     (cons
                      'c::frame
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                           (cons 'ldm-ident
                                 (cons (cons 'ident (cons fun 'nil))
                                       'nil))
                           'nil)))
                       (cons
                        (cons
                         'list
                         (cons
                          (cons
                           'c::init-scope
                           (cons
                                (cons 'quote (cons ldm-params 'nil))
                                (cons (cons 'list args) 'nil)))
                          'nil))
                        'nil)))
                     '(compst)))
                   'nil))
                 '((limit (1- limit))))))
              'nil)))
           '(:in-theory '((:e c::fun-info->body$inline)
                          (:e c::fun-info->params$inline)
                          (:e c::fun-info->result$inline)
                          (:e c::fun-info-from-fundef)
                          (:e ident)
                          (:e ldm-fundef)
                          (:e ldm-ident)
                          (:e ldm-type)
                          (:e ldm-type-set)
                          (:e ldm-comp-stmt)
                          (:e c::tyname-to-type)
                          (:e c::block-item-list-nocallsp)
                          (:e in)
                          c::errorp-of-error
                          c::compustate-frames-number-of-push-frame
                          (:t c::compustate-frames-number))))))))
      'nil))
    (thm-event
     (cons
      'defrule
      (cons
           thm-name
           (cons formula
                 (cons ':rule-classes
                       (cons 'nil
                             (cons ':hints (cons hints 'nil)))))))))
   (mv new-fundef
       (make-gout :events (cons thm-event events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys vartys-after-fundef)))))

Theorem: fundefp-of-xeq-fundef.fundef

(defthm fundefp-of-xeq-fundef.fundef
  (b* (((mv c$::?fundef ?gout)
        (xeq-fundef extension spec spec-new declor
                    declor-new asm? attribs decls decls-new
                    body body-new body-thm-name info gin)))
    (fundefp fundef))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-fundef.gout

(defthm goutp-of-xeq-fundef.gout
  (b* (((mv c$::?fundef ?gout)
        (xeq-fundef extension spec spec-new declor
                    declor-new asm? attribs decls decls-new
                    body body-new body-thm-name info gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: fundef-unambp-of-xeq-fundef

(defthm fundef-unambp-of-xeq-fundef
  (implies (and (decl-spec-list-unambp spec-new)
                (declor-unambp declor-new)
                (decl-list-unambp decls-new)
                (comp-stmt-unambp body-new))
           (b* (((mv c$::?fundef ?gout)
                 (xeq-fundef extension spec spec-new declor
                             declor-new asm? attribs decls decls-new
                             body body-new body-thm-name info gin)))
             (fundef-unambp fundef))))

Theorem: fundef-annop-of-xeq-fundef

(defthm fundef-annop-of-xeq-fundef
  (implies (and (decl-spec-list-annop spec-new)
                (declor-annop declor-new)
                (decl-list-annop decls-new)
                (comp-stmt-annop body-new)
                (fundef-infop info))
           (b* (((mv c$::?fundef ?gout)
                 (xeq-fundef extension spec spec-new declor
                             declor-new asm? attribs decls decls-new
                             body body-new body-thm-name info gin)))
             (fundef-annop fundef))))

Theorem: fundef-aidentp-of-xeq-fundef

(defthm fundef-aidentp-of-xeq-fundef
  (implies (and (decl-spec-list-unambp spec-new)
                (decl-spec-list-aidentp spec-new gcc)
                (declor-unambp declor-new)
                (declor-aidentp declor-new gcc)
                (attrib-spec-list-aidentp attribs gcc)
                (decl-list-unambp decls-new)
                (decl-list-aidentp decls-new gcc)
                (comp-stmt-unambp body-new)
                (comp-stmt-aidentp body-new gcc))
           (b* (((mv c$::?fundef ?gout)
                 (xeq-fundef extension spec spec-new declor
                             declor-new asm? attribs decls decls-new
                             body body-new body-thm-name info gin)))
             (fundef-aidentp fundef gcc))))