• 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
                • Xeq-declon-declon
                • Gen-param-thms
                • Gen-from-params
                • 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
                • Gen-declon-thm
                • Xeq-expr-unary
                • Gen-stmt-thm
                • Xeq-stmt-return
                • Xeq-stmt-expr
                • Xeq-block-item-declon
                • 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 
            specs specs-new declor declor-new 
            asm? attribs declons declons-new 
            body body-new body-thm-name info gin) 
 
  → 
(mv fundef gout)
    Arguments
    extension — Guard (booleanp extension).
    specs — Guard (decl-spec-listp specs).
    specs-new — Guard (decl-spec-listp specs-new).
    declor — Guard (declorp declor).
    declor-new — Guard (declorp declor-new).
    asm? — Guard (asm-name-spec-optionp asm?).
    attribs — Guard (attrib-spec-listp attribs).
    declons — Guard (declon-listp declons).
    declons-new — Guard (declon-listp declons-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 specs specs-new declor declor-new
                             asm? attribs declons declons-new
                             body body-new body-thm-name info gin)
 (declare (xargs :guard (and (booleanp extension)
                             (decl-spec-listp specs)
                             (decl-spec-listp specs-new)
                             (declorp declor)
                             (declorp declor-new)
                             (asm-name-spec-optionp asm?)
                             (attrib-spec-listp attribs)
                             (declon-listp declons)
                             (declon-listp declons-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 specs)
                             (decl-spec-list-annop specs)
                             (decl-spec-list-unambp specs-new)
                             (decl-spec-list-annop specs-new)
                             (declor-unambp declor)
                             (declor-annop declor)
                             (declor-unambp declor-new)
                             (declor-annop declor-new)
                             (declon-list-unambp declons)
                             (declon-list-annop declons)
                             (declon-list-unambp declons-new)
                             (declon-list-annop declons-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
                         :specs specs
                         :declor declor
                         :asm? asm?
                         :attribs attribs
                         :declons declons
                         :body body
                         :info info))
    (new-fundef (make-fundef :extension extension
                             :specs specs-new
                             :declor declor-new
                             :asm? asm?
                             :attribs attribs
                             :declons declons-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
                    specs specs-new declor declor-new
                    asm? attribs declons declons-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
                    specs specs-new declor declor-new
                    asm? attribs declons declons-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 specs-new)
                (declor-unambp declor-new)
                (declon-list-unambp declons-new)
                (comp-stmt-unambp body-new))
           (b* (((mv c$::?fundef ?gout)
                 (xeq-fundef extension
                             specs specs-new declor declor-new
                             asm? attribs declons declons-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 specs-new)
                (declor-annop declor-new)
                (declon-list-annop declons-new)
                (comp-stmt-annop body-new)
                (fundef-infop info))
           (b* (((mv c$::?fundef ?gout)
                 (xeq-fundef extension
                             specs specs-new declor declor-new
                             asm? attribs declons declons-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 specs-new)
                (decl-spec-list-aidentp specs-new gcc)
                (declor-unambp declor-new)
                (declor-aidentp declor-new gcc)
                (attrib-spec-list-aidentp attribs gcc)
                (declon-list-unambp declons-new)
                (declon-list-aidentp declons-new gcc)
                (comp-stmt-unambp body-new)
                (comp-stmt-aidentp body-new gcc))
           (b* (((mv c$::?fundef ?gout)
                 (xeq-fundef extension
                             specs specs-new declor declor-new
                             asm? attribs declons declons-new
                             body body-new body-thm-name info gin)))
             (fundef-aidentp fundef gcc))))