		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-fun-correct-thm

Generate the correctness theorem for a C function.

Signature
(atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state) → (mv events print-event name lemma-name names-to-avoid)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; fn-def* — Guard (symbolp fn-def*).; init-formals — Guard (symbol-listp init-formals).; affect — Guard (symbol-listp affect).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; context-preamble — Guard (true-listp context-preamble).; compst-var — Guard (symbolp compst-var).; fenv-var — Guard (symbolp fenv-var).; limit-var — Guard (symbolp limit-var).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; fn-fun-env-thm — Guard (symbolp fn-fun-env-thm).; init-scope-expand-thm — Guard (symbolp init-scope-expand-thm).; init-scope-scopep-thm — Guard (symbolp init-scope-scopep-thm).; push-init-thm — Guard (symbolp push-init-thm).; pop-frame-thm — Guard (symbolp pop-frame-thm).; body-thm — Guard (symbolp body-thm).; body-type — Guard (typep body-type).; body-limit — Guard (pseudo-termp body-limit).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: events — Type (pseudo-event-form-listp events).; print-event — Type (pseudo-event-formp print-event).; name — Type (symbolp name), given (symbol-symbol-alistp fn-thms).; lemma-name — Type (symbolp lemma-name).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp names-to-avoid).

This will eventually replace atc-gen-cfun-correct-thm, once the modular proof generation approach is completed.

We make use of other modular theorems, whose names are passed to this ACL2 function. We use 1 more than the limit for the body as limit bound, because we need 1 to go from exec-fun to exec-block-item-list, which is what the body's theorem refers to.

We enable declar and assign in the generated hints because the correctness theorem generated about the body of the function (i.e. body-thm) does not that have that wrapper. We will need to add other wrappers like assign here, when we extend modular proofs to handle those. An alternative could be to include the wrappers in the theorems about the statements that form the body, and then we will not need to include them here.

Definitions and Theorems

Function: atc-gen-fun-correct-thm

(defun atc-gen-fun-correct-thm
       (fn fn-guard fn-def* init-formals
           affect typed-formals context-preamble
           compst-var fenv-var limit-var fn-thms
           fn-fun-env-thm init-scope-expand-thm
           init-scope-scopep-thm
           push-init-thm pop-frame-thm
           body-thm body-type body-limit prec-tags
           prec-objs names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (symbolp fn)
                         (symbolp fn-guard)
                         (symbolp fn-def*)
                         (symbol-listp init-formals)
                         (symbol-listp affect)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (true-listp context-preamble)
                         (symbolp compst-var)
                         (symbolp fenv-var)
                         (symbolp limit-var)
                         (symbol-symbol-alistp fn-thms)
                         (symbolp fn-fun-env-thm)
                         (symbolp init-scope-expand-thm)
                         (symbolp init-scope-scopep-thm)
                         (symbolp push-init-thm)
                         (symbolp pop-frame-thm)
                         (symbolp body-thm)
                         (typep body-type)
                         (pseudo-termp body-limit)
                         (atc-string-taginfo-alistp prec-tags)
                         (atc-string-objinfo-alistp prec-objs)
                         (symbol-listp names-to-avoid))))
 (let ((__function__ 'atc-gen-fun-correct-thm))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (lemma-name (pack fn '-correct))
    ((mv lemma-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          lemma-name nil names-to-avoid wrld))
    (formals (formals+ fn wrld))
    (result-var (if (type-case body-type :void)
                    nil
                  (genvar$ 'atc
                           "RESULT" nil formals state)))
    (limit (cons '+
                 (cons ''1 (cons body-limit 'nil))))
    (affect-new (acl2::add-suffix-to-fn-lst affect "-NEW"))
    (fn-results (append (and result-var (list result-var))
                        affect-new))
    (fn-binder (if (endp (cdr fn-results))
                   (car fn-results)
                 (cons 'mv fn-results)))
    (new-compst
         (atc-gen-fun-endstate affect
                               typed-formals compst-var prec-objs))
    (exec-hyps
     (cons
      'and
      (cons
       (cons 'compustatep
             (cons compst-var 'nil))
       (append
         context-preamble
         (cons (cons fn-guard formals)
               (cons (cons 'integerp (cons limit-var 'nil))
                     (cons (cons '>=
                                 (cons limit-var (cons limit 'nil)))
                           'nil)))))))
    (exec-concl
     (cons
      'equal
      (cons
       (cons
         'exec-fun
         (cons (cons 'ident
                     (cons (symbol-name fn) 'nil))
               (cons (cons 'list init-formals)
                     (cons compst-var
                           (cons fenv-var (cons limit-var 'nil))))))
       (cons (cons 'mv
                   (cons result-var (cons new-compst 'nil)))
             'nil))))
    (type-hyps (cons fn-guard formals))
    ((mv type-concl &)
     (atc-gen-term-type-formula
          (cons fn formals)
          body-type affect (list typed-formals)
          prec-tags))
    (exec-formula
     (cons
      'implies
      (cons
       exec-hyps
       (cons
        (cons
          'b*
          (cons (cons (cons fn-binder (cons (cons fn formals) 'nil))
                      'nil)
                (cons exec-concl 'nil)))
        'nil))))
    (type-formula (cons 'implies
                        (cons type-hyps (cons type-concl 'nil))))
    (lemma-formula
         (cons 'and
               (cons exec-formula (cons type-formula 'nil))))
    (valuep-when-type-pred
         (and result-var
              (atc-type-to-valuep-thm body-type prec-tags)))
    (type-of-value-when-type-pred
         (and result-var
              (atc-type-to-type-of-value-thm body-type prec-tags)))
    (type-to-quoted-thm?
        (and result-var
             (atc-type-to-type-to-quoted-thms body-type prec-tags)))
    (lemma-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-fun-open-return
            (cons
             'exec-fun-open-noreturn
             (cons
              '(:e type-void)
              (cons
               'not-zp-of-limit-variable
               (cons
                fn-fun-env-thm
                (cons
                 init-scope-expand-thm
                 (cons
                  init-scope-scopep-thm
                  (cons
                   push-init-thm
                   (cons
                    body-thm
                    (cons
                     '(:e fun-info->body)
                     (cons
                      'mv-nth-of-cons
                      (cons
                       '(:e zp)
                       (cons
                        'return-type-of-stmt-value-return
                        (cons
                         'return-type-of-stmt-value-none
                         (cons
                          'stmt-value-return->value?-of-stmt-value-return
                          (cons
                           'value-option-fix-when-value-optionp
                           (cons
                            'value-optionp-when-valuep
                            (cons
                             '(:e value-optionp)
                             (cons
                              '(:e type-of-value-option)
                              (append
                               (and
                                 result-var
                                 (list* valuep-when-type-pred
                                        type-of-value-when-type-pred
                                        type-to-quoted-thm?))
                               (cons
                                'type-of-value-option-when-valuep
                                (cons
                                 '(:e fun-info->result)
                                 (cons
                                  '(:e tyname-to-type)
                                  (append
                                   (and
                                    result-var
                                    (type-integerp body-type)
                                    (cons
                                     (cons
                                      ':e
                                      (cons
                                        (pack 'type-
                                              (type-kind body-type))
                                        'nil))
                                     'nil))
                                   (cons
                                    pop-frame-thm
                                    (cons
                                     fn-def*
                                     '(declar
                                       assign)))))))))))))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv lemma-event &)
     (evmac-generate-defthm lemma-name
                            :formula lemma-formula
                            :hints lemma-hints
                            :enable nil))
    (name (cdr (assoc-eq fn fn-thms)))
    (formula
     (cons
      'implies
      (cons
       (cons
        'and
        (cons
         (cons 'compustatep
               (cons compst-var 'nil))
         (append
          context-preamble
          (cons
               (untranslate$ (uguard+ fn wrld)
                             nil state)
               (cons (cons 'integerp (cons limit-var 'nil))
                     (cons (cons '>=
                                 (cons limit-var (cons limit 'nil)))
                           'nil))))))
       (cons
        (cons
          'b*
          (cons (cons (cons fn-binder (cons (cons fn formals) 'nil))
                      'nil)
                (cons exec-concl 'nil)))
        'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
           ':use
           (cons lemma-name
                 (cons ':in-theory
                       (cons (cons 'quote
                                   (cons (cons fn-guard 'nil) 'nil))
                             'nil)))))
      'nil))
    ((mv local-event exported-event)
     (evmac-generate-defthm name
                            :formula formula
                            :hints hints
                            :enable nil))
    (print-event
         (cons 'cw-event
               (cons '"~%~x0~|"
                     (cons (cons 'quote (cons exported-event 'nil))
                           'nil)))))
   (mv (list lemma-event local-event exported-event)
       print-event
       name lemma-name names-to-avoid))))

Theorem: pseudo-event-form-listp-of-atc-gen-fun-correct-thm.events

(defthm pseudo-event-form-listp-of-atc-gen-fun-correct-thm.events
 (b*
  (((mv ?events ?print-event
        ?name ?lemma-name ?names-to-avoid)
    (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals
                             affect typed-formals context-preamble
                             compst-var fenv-var limit-var fn-thms
                             fn-fun-env-thm init-scope-expand-thm
                             init-scope-scopep-thm
                             push-init-thm pop-frame-thm
                             body-thm body-type body-limit prec-tags
                             prec-objs names-to-avoid state)))
  (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-atc-gen-fun-correct-thm.print-event

(defthm pseudo-event-formp-of-atc-gen-fun-correct-thm.print-event
 (b*
  (((mv ?events ?print-event
        ?name ?lemma-name ?names-to-avoid)
    (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals
                             affect typed-formals context-preamble
                             compst-var fenv-var limit-var fn-thms
                             fn-fun-env-thm init-scope-expand-thm
                             init-scope-scopep-thm
                             push-init-thm pop-frame-thm
                             body-thm body-type body-limit prec-tags
                             prec-objs names-to-avoid state)))
  (pseudo-event-formp print-event))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-fun-correct-thm.name

(defthm symbolp-of-atc-gen-fun-correct-thm.name
  (implies (symbol-symbol-alistp fn-thms)
           (b* (((mv ?events ?print-event
                     ?name ?lemma-name ?names-to-avoid)
                 (atc-gen-fun-correct-thm
                      fn fn-guard fn-def* init-formals
                      affect typed-formals context-preamble
                      compst-var fenv-var limit-var fn-thms
                      fn-fun-env-thm init-scope-expand-thm
                      init-scope-scopep-thm
                      push-init-thm pop-frame-thm
                      body-thm body-type body-limit prec-tags
                      prec-objs names-to-avoid state)))
             (symbolp name)))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-fun-correct-thm.lemma-name

(defthm symbolp-of-atc-gen-fun-correct-thm.lemma-name
 (b*
  (((mv ?events ?print-event
        ?name ?lemma-name ?names-to-avoid)
    (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals
                             affect typed-formals context-preamble
                             compst-var fenv-var limit-var fn-thms
                             fn-fun-env-thm init-scope-expand-thm
                             init-scope-scopep-thm
                             push-init-thm pop-frame-thm
                             body-thm body-type body-limit prec-tags
                             prec-objs names-to-avoid state)))
  (symbolp lemma-name))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-fun-correct-thm.names-to-avoid

(defthm symbol-listp-of-atc-gen-fun-correct-thm.names-to-avoid
  (implies (symbol-listp names-to-avoid)
           (b* (((mv ?events ?print-event
                     ?name ?lemma-name ?names-to-avoid)
                 (atc-gen-fun-correct-thm
                      fn fn-guard fn-def* init-formals
                      affect typed-formals context-preamble
                      compst-var fenv-var limit-var fn-thms
                      fn-fun-env-thm init-scope-expand-thm
                      init-scope-scopep-thm
                      push-init-thm pop-frame-thm
                      body-thm body-type body-limit prec-tags
                      prec-objs names-to-avoid state)))
             (symbol-listp names-to-avoid)))
  :rule-classes :rewrite)