• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
          • Representation
          • Transformation-tools
            • Simpadd0
              • Simpadd0-implementation
                • Simpadd0-event-generation
                  • Simpadd0-exprs/decls/stmts
                  • Simpadd0-fundef
                    • Simpadd0-expr-cond
                    • Simpadd0-expr-binary
                    • Simpadd0-gen-expr-pure-thm
                    • Simpadd0-gen-block-item-list-thm
                    • Simpadd0-gen-block-item-thm
                    • Simpadd0-gen-stmt-thm
                    • Simpadd0-gen-from-params
                    • Simpadd0-expr-unary
                    • Simpadd0-gout
                    • Simpadd0-expr-const
                    • Simpadd0-block-item-list-one
                    • Simpadd0-block-item-stmt
                    • Simpadd0-gen-param-thms
                    • Simpadd0-expr-ident
                    • Simpadd0-stmt-return
                    • Simpadd0-gen-init-scope-thm
                    • Simpadd0-gin
                    • Simpadd0-expr-paren
                    • Simpadd0-expr-cast
                    • Simpadd0-filepath-transunit-map
                    • Simpadd0-extdecl-list
                    • Simpadd0-extdecl
                    • Simpadd0-transunit-ensemble
                    • Simpadd0-transunit
                    • Simpadd0-gen-var-hyps
                    • Simpadd0-tyspecseq-to-type
                    • Simpadd0-gin-update
                    • Simpadd0-gen-everything
                    • Irr-simpadd0-gout
                  • Simpadd0-process-inputs-and-gen-everything
                  • Simpadd0-fn
                  • Simpadd0-input-processing
                  • Simpadd0-macro-definition
                • Simpadd0-expr-option
                • Simpadd0-structdeclor-list
                • Simpadd0-structdecl-list
                • Simpadd0-spec/qual-list
                • Simpadd0-param-declon-list
                • Simpadd0-initdeclor-list
                • Simpadd0-dirabsdeclor-option
                • Simpadd0-dirabsdeclor
                • Simpadd0-desiniter-list
                • Simpadd0-absdeclor-option
                • Simpadd0-strunispec
                • Simpadd0-structdeclor
                • Simpadd0-structdecl
                • Simpadd0-statassert
                • Simpadd0-spec/qual
                • Simpadd0-param-declor
                • Simpadd0-param-declon
                • Simpadd0-member-designor
                • Simpadd0-initer-option
                • Simpadd0-initdeclor
                • Simpadd0-genassoc-list
                • Simpadd0-genassoc
                • Simpadd0-expr
                • Simpadd0-enumspec
                • Simpadd0-enumer-list
                • Simpadd0-dirdeclor
                • Simpadd0-desiniter
                • Simpadd0-designor-list
                • Simpadd0-designor
                • Simpadd0-declor-option
                • Simpadd0-decl-spec-list
                • Simpadd0-decl-spec
                • Simpadd0-decl-list
                • Simpadd0-const-expr-option
                • Simpadd0-const-expr
                • Simpadd0-block-item-list
                • Simpadd0-align-spec
                • Simpadd0-absdeclor
                • Simpadd0-type-spec
                • Simpadd0-tyname
                • Simpadd0-stmt
                • Simpadd0-label
                • Simpadd0-initer
                • Simpadd0-expr-list
                • Simpadd0-enumer
                • Simpadd0-declor
                • Simpadd0-decl
                • Simpadd0-block-item
              • Splitgso
              • Constant-propagation
              • Split-fn
              • Specialize
              • Split-all-gso
              • Copy-fn
              • Rename
              • Utilities
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Simpadd0-event-generation

    Simpadd0-fundef

    Transform a function definition.

    Signature
    (simpadd0-fundef fundef gin state) → (mv new-fundef gout)
    Arguments
    fundef — Guard (fundefp fundef).
    gin — Guard (simpadd0-ginp gin).
    Returns
    new-fundef — Type (fundefp new-fundef).
    gout — Type (simpadd0-goutp gout).

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

    The generated theorem contains local theorems that are used in the proof of the main theorem. The local theorems are about the initial scope of the function, and about the parameters in the computation state at the beginning of the execution of the function body.

    If the body of the function underwent no transformation, which we can see from the diffp component of simpadd0-gout, the theorem generated for the body just talks about its type, but the theorem for the function always involves an equality between c::exec-fun. If diffp is nil, we make use of a theorem from the language formalization that says that execution without function calls does not depend on the function environment: we instantiate that theorem for the body, using the old and new function environments.

    Definitions and Theorems

    Function: simpadd0-fundef-loop

    (defun simpadd0-fundef-loop (thms fun)
     (declare (xargs :guard (and (symbol-listp thms)
                                 (stringp fun))))
     (let ((__function__ 'simpadd0-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 (simpadd0-fundef-loop (cdr thms) fun)))
       (cons lemma-instance more-lemma-instances))))

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

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

    Function: simpadd0-fundef

    (defun simpadd0-fundef (fundef gin state)
     (declare (xargs :stobjs (state)))
     (declare (xargs :guard (and (fundefp fundef)
                                 (simpadd0-ginp gin))))
     (declare (xargs :guard (fundef-unambp fundef)))
     (let ((__function__ 'simpadd0-fundef))
      (declare (ignorable __function__))
      (b*
       (((fundef fundef) fundef)
        ((mv new-spec (simpadd0-gout gout-spec))
         (simpadd0-decl-spec-list fundef.spec gin state))
        (gin (simpadd0-gin-update gin gout-spec))
        ((mv new-declor (simpadd0-gout gout-declor))
         (simpadd0-declor fundef.declor gin state))
        (gin (simpadd0-gin-update gin gout-declor))
        ((mv new-decls (simpadd0-gout gout-decls))
         (simpadd0-decl-list fundef.decls gin state))
        (gin (simpadd0-gin-update gin gout-decls))
        ((unless (stmt-case fundef.body :compound))
         (raise
          "Internal error: the body of ~x0 is not a compound statement."
          (fundef-fix fundef))
         (mv (irr-fundef) (irr-simpadd0-gout)))
        (items (stmt-compound->items fundef.body))
        ((mv new-items (simpadd0-gout gout-body))
         (simpadd0-block-item-list items gin state))
        ((simpadd0-gin gin)
         (simpadd0-gin-update gin gout-body))
        (new-body (stmt-compound new-items))
        (new-fundef (make-fundef :extension fundef.extension
                                 :spec new-spec
                                 :declor new-declor
                                 :asm? fundef.asm?
                                 :attribs fundef.attribs
                                 :decls new-decls
                                 :body new-body))
        (gout-no-thm
         (make-simpadd0-gout
          :events (append gout-spec.events gout-declor.events
                          gout-decls.events gout-body.events)
          :thm-name nil
          :thm-index gin.thm-index
          :names-to-avoid gin.names-to-avoid
          :vartys
          (omap::update*
               gout-spec.vartys
               (omap::update*
                    gout-declor.vartys
                    (omap::update* gout-decls.vartys gout-body.vartys)))
          :diffp (or gout-spec.diffp gout-declor.diffp
                     gout-decls.diffp gout-body.diffp)))
        ((unless gout-body.thm-name)
         (mv new-fundef gout-no-thm))
        ((unless (fundef-formalp fundef))
         (mv new-fundef gout-no-thm))
        ((declor declor) fundef.declor)
        ((when (consp declor.pointers))
         (mv new-fundef gout-no-thm))
        ((unless (dirdeclor-case declor.direct :function-params))
         (mv new-fundef gout-no-thm))
        (params (dirdeclor-function-params->params declor.direct))
        (dirdeclor (dirdeclor-function-params->declor declor.direct))
        ((unless (dirdeclor-case dirdeclor :ident))
         (raise "Internal error: ~x0 is not just the function name."
                dirdeclor)
         (mv (irr-fundef) (irr-simpadd0-gout)))
        (fun (ident->unwrap (dirdeclor-ident->ident dirdeclor)))
        ((unless (stringp fun))
         (raise "Internal error: non-string identifier ~x0."
                fun)
         (mv (irr-fundef) (irr-simpadd0-gout)))
        ((mv erp ldm-params)
         (ldm-param-declon-list params))
        ((when erp) (mv new-fundef gout-no-thm))
        (type (block-item-list-type items))
        ((unless (type-formalp type))
         (raise "Internal error: function ~x0 returns ~x1."
                (fundef-fix fundef)
                type)
         (mv (irr-fundef) (irr-simpadd0-gout)))
        ((mv & ctype) (ldm-type type))
        ((mv okp
             args parargs arg-types arg-types-compst)
         (simpadd0-gen-from-params ldm-params gin))
        ((unless okp)
         (mv new-fundef gout-no-thm))
        ((mv init-scope-thm-event
             init-scope-thm-name)
         (simpadd0-gen-init-scope-thm
              ldm-params args parargs arg-types))
        ((mv param-thm-events param-thm-names)
         (simpadd0-gen-param-thms args arg-types-compst
                                  arg-types ldm-params args))
        (thm-name (packn-pos (list gin.const-new '-thm-
                                   gin.thm-index)
                             gin.const-new))
        (thm-index (1+ gin.thm-index))
        (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-result old-compst)
                     (cons (cons 'c::exec-fun
                                 (cons 'fun
                                       (cons (cons 'list args)
                                             '(compst old-fenv limit))))
                           'nil))
               (cons
                (cons
                     '(mv new-result 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 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-result)))))
              (cons
               (cons
                'and
                (cons
                 '(not (c::errorp new-result))
                 (cons
                  '(equal old-result new-result)
                  (cons
                   '(equal old-compst new-compst)
                   (cons
                    'old-result
                    (cons
                       (cons 'equal
                             (cons '(c::type-of-value old-result)
                                   (cons (cons 'quote (cons ctype '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
               (append
                (and
                 (not gout-body.diffp)
                 (cons
                  (cons
                   ':instance
                   (cons
                    'c::exec-block-item-list-without-calls
                    (cons
                     (cons
                      'items
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                             (cons 'ldm-block-item-list
                                   (cons (cons 'quote (cons items 'nil))
                                         'nil))
                             'nil)))
                       'nil))
                     (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))
                      '((fenv old-fenv)
                        (fenv1 new-fenv)
                        (limit (1- limit)))))))
                  'nil))
                (cons
                 init-scope-thm-name
                 (append
                  (simpadd0-fundef-loop param-thm-names fun)
                  (cons
                   (cons
                    ':instance
                    (cons
                     gout-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))
                      (append (and (not gout-body.diffp)
                                   '((fenv old-fenv)))
                              '((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-block-item-list)
                              (:e ldm-fundef)
                              (:e ldm-ident)
                              (:e ldm-type)
                              (:e ldm-block-item-list)
                              (:e c::tyname-to-type)
                              (:e c::type-sint)
                              (:e c::block-item-list-nocallsp)
                              c::errorp-of-error)))))))
          'nil))
        (thm-event
         (cons
          'defruled
          (cons
           thm-name
           (cons
            formula
            (cons
             ':hints
             (cons
                hints
                (cons ':prep-lemmas
                      (cons (cons init-scope-thm-event param-thm-events)
                            'nil)))))))))
       (mv
        new-fundef
        (make-simpadd0-gout
          :events (append gout-spec.events
                          gout-declor.events gout-decls.events
                          gout-body.events (list thm-event))
          :thm-name thm-name
          :thm-index thm-index
          :names-to-avoid (cons thm-name gout-body.names-to-avoid)
          :vartys
          (omap::update*
               gout-spec.vartys
               (omap::update*
                    gout-declor.vartys
                    (omap::update* gout-decls.vartys gout-body.vartys)))
          :diffp (or gout-spec.diffp gout-declor.diffp
                     gout-decls.diffp gout-body.diffp))))))

    Theorem: fundefp-of-simpadd0-fundef.new-fundef

    (defthm fundefp-of-simpadd0-fundef.new-fundef
      (b* (((mv ?new-fundef ?gout)
            (simpadd0-fundef fundef gin state)))
        (fundefp new-fundef))
      :rule-classes :rewrite)

    Theorem: simpadd0-goutp-of-simpadd0-fundef.gout

    (defthm simpadd0-goutp-of-simpadd0-fundef.gout
      (b* (((mv ?new-fundef ?gout)
            (simpadd0-fundef fundef gin state)))
        (simpadd0-goutp gout))
      :rule-classes :rewrite)

    Theorem: fundef-unambp-of-simpadd0-fundef

    (defthm fundef-unambp-of-simpadd0-fundef
      (b* (((mv ?new-fundef ?gout)
            (simpadd0-fundef fundef gin state)))
        (fundef-unambp new-fundef)))

    Theorem: simpadd0-fundef-of-fundef-fix-fundef

    (defthm simpadd0-fundef-of-fundef-fix-fundef
      (equal (simpadd0-fundef (fundef-fix fundef)
                              gin state)
             (simpadd0-fundef fundef gin state)))

    Theorem: simpadd0-fundef-fundef-equiv-congruence-on-fundef

    (defthm simpadd0-fundef-fundef-equiv-congruence-on-fundef
      (implies (c$::fundef-equiv fundef fundef-equiv)
               (equal (simpadd0-fundef fundef gin state)
                      (simpadd0-fundef fundef-equiv gin state)))
      :rule-classes :congruence)

    Theorem: simpadd0-fundef-of-simpadd0-gin-fix-gin

    (defthm simpadd0-fundef-of-simpadd0-gin-fix-gin
      (equal (simpadd0-fundef fundef (simpadd0-gin-fix gin)
                              state)
             (simpadd0-fundef fundef gin state)))

    Theorem: simpadd0-fundef-simpadd0-gin-equiv-congruence-on-gin

    (defthm simpadd0-fundef-simpadd0-gin-equiv-congruence-on-gin
      (implies (simpadd0-gin-equiv gin gin-equiv)
               (equal (simpadd0-fundef fundef gin state)
                      (simpadd0-fundef fundef gin-equiv state)))
      :rule-classes :congruence)