stobj-preservation

Included Books

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

include-book

(include-book "just-expand")

other

(defxdoc preservation-thms
  :parents (stobj)
  :short "Automation for proving that stobj-modifying functions preserve
certain properties"
  :long "
<p>A major pain when programming in logic mode with stobjs is maintaining
all the invariants necessary to prove guards.  We provide utilities to define a
set of theorem templates and to prove those theorems of a function.</p>

<p>Usage:
@({
 (def-stobj-preservation-thms fnname
    :stobjname my-stobj
    :templates my-stobj-pres-templates
    :omit (my-thm-template-x my-thm-template-y)
    :history my-stobj-pres-history) })
tries to prove a set of preservation theorems as stored in the table
<tt>my-st-pres-templates</tt>.</p>

<p>To add a new preservation theorem to the existing set, use, for example,
@({
  (add-stobj-preservation-thm
   nth-of-field-preserved
   :vars (id)
   :body `(implies (< id (my-index ,orig-stobj))
                   (equal (nth id (nth ',*fieldi* ,new-stobj))
                          (nth id (nth ',*fieldi* ,orig-stobj))))
   :hints `(,@expand/induct-hints
            (and stable-under-simplificationp
                 '(:in-theory (enable my-index))))
   :enable '(my-rule my-ruleset)
   :disable '(bad-rule other-rules)
   :rule-classes `(:rewrite (:linear :trigger-terms (,new-stobj)))
   :templates my-stobj-pres-templates
   :history my-stobj-pres-history)})
Certain placeholder variables can be used in the body, hints, enable, disable,
and rule-classes fields:
<ul>
<li><tt>orig-stobj</tt> is the variable denoting the original stobj before modification</li>
<li><tt>new-stobj</tt> is the term giving the modified stobj after the function
call: for example, @('(mv-nth 1 (modify-my-stobj my-stobj))')</li>
<li><tt>call</tt> is the call of the function without the possible
<tt>mv-nth</tt>, for example, @('(modify-my-stobj my-stobj)')</li>
<li><tt>expand/induct-hints</tt> are a generated set of hints specific to each
function for which the preservation theorem is to be proved, which expand and
 (if recursive) induct on that function</li>
<li><tt>fn</tt> is the function being worked on</li>
<li><tt>fn$</tt> is the @('deref-macro-name') of that function,
e.g. <tt>binary-logior</tt> if the <tt>fn</tt> were <tt>logior</tt></li>
<li><tt>formals</tt> is the formals of the function, possibly with some
modification to the names, but the same ones used in <tt>call</tt> and
<tt>new-stobj</tt>.</li></ul>
The <tt>:vars</tt> argument should be a list containing all of the variable
names used in the theorem body; if the formals of the function contain any of
these variables, we will use a modified list of formals that avoids them.</p>

<p>One additional keyword argument, <tt>:deps</tt>, is allowed; if provided,
this should be a list of stobj-preservation-thm template names such as
<tt>nth-node-preserved</tt> above.  This signifies that this theorem should
only be proved of functions for which the dependencies were also proved.</p>

<p>Two additional macros, @('retroactive-add-stobj-preservation-thm') and
@('retroactive-add-stobj-preservation-thm-local') are similar to
@('add-stobj-preservation-thm') but additionally prove the new theorem for all
existing functions for which other stobj-preservation-thms have already been
proved, modulo the dependencies of the new theorem. The <tt>-local</tt> version
makes the addition of the new theorem local to the current book or encapsulate,
so that nonlocal calls of <tt>def-stobj-preservation-thms</tt> won't include
it.</p>

<p>All of these macros take keyword arguments <tt>templates</tt> and
<tt>history</tt>, which should be symbols.  These symbols are the ACL2 table
names in which the templates and usage history are stored.  (The history is
used mainly for checking dependencies).  In order to simplify the usage of this
utility, we supply a macro-generating macro:
@({
 (def-stobj-preservation-macros :name hello
                                :default-stobjname my-stobj
                                :templates my-templates-table
                                :history my-history-table)})
which defines simple wrapper macros
@({
 (def-hello-preservation-thms ...)
 (add-hello-preservation-thm ...)
 (retroactive-add-hello-preservation-thm ...)
 (retroactive-add-hello-preservation-thm-local ...)})
that behave the same as the ones above, execpt that they don't take the
<tt>:templates</tt> or <tt>:history</tt> arguments and they use
<tt>my-stobj</tt> by default for <tt>:stobjname</tt>.</p>
")

fix-formals-for-varsfunction

(defun fix-formals-for-vars
  (vars formals)
  (declare (xargs :mode :program))
  (if (atom vars)
    formals
    (let* ((pos (position (car vars) formals)) (formals (if pos
            (update-nth pos
              (genvar (car vars) (symbol-name (car vars)) 0 formals)
              formals)
            formals)))
      (fix-formals-for-vars (cdr vars) formals))))

add-stobj-preservation-recordmacro

(defmacro add-stobj-preservation-record
  (fn stobjname tmpname histtable)
  (let ((pair (cons fn stobjname)))
    `(table ,HISTTABLE
      ',PAIR
      (cons ',TMPNAME
        (cdr (assoc-equal ',PAIR (table-alist ',HISTTABLE world)))))))

check-deps-satisfiedfunction

(defun check-deps-satisfied
  (deps fn stobjname histtable state)
  (declare (xargs :mode :program :stobjs state))
  (subsetp-eq deps
    (cdr (assoc-equal (cons fn stobjname)
        (table-alist histtable (w state))))))

mk-stobj-preservation-thmfunction

(defun mk-stobj-preservation-thm
  (fn stobjname template histtable state)
  (declare (xargs :mode :program :stobjs state))
  (b* (((nths name
        vars
        body
        hints
        ruleset
        deps
        enable
        disable
        rule-classes) template) (world (w state))
      (fn$ (deref-macro-name fn (macro-aliases world)))
      (formals (fix-formals-for-vars vars (formals fn$ world)))
      (stobjs-out (stobjs-out fn$ world))
      (thmname (intern-in-package-of-symbol (concatenate 'string
            (symbol-name name)
            "-OF-"
            (symbol-name fn))
          fn))
      (call (cons fn formals))
      (new-stobj (if (cdr stobjs-out)
          `(mv-nth ,(POSITION STOBJNAME STOBJS-OUT) ,CALL)
          call))
      (recp (recursivep fn$ t world))
      (expand/induct-hints (if (and recp (not (cdr recp)))
          `((just-induct-and-expand ,CALL))
          `(("Goal" . ,(APPEND '(:DO-NOT-INDUCT T) `(:IN-THEORY (DISABLE (:DEFINITION ,FN$)))
         (IF (AND RECP (NOT (CDR RECP)))
             NIL
             `(:EXPAND (,CALL)))))))))
    `(make-event (b* (((unless (check-deps-satisfied ',DEPS
              ',FN
              ',STOBJNAME
              ',HISTTABLE
              state)) '(value-triple :skipped)) (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?EXPAND/INDUCT-HINTS) HISTTABLE) ',EXPAND/INDUCT-HINTS)
          (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?NEW-STOBJ) HISTTABLE) ',NEW-STOBJ)
          (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?CALL) HISTTABLE) ',CALL)
          (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?FN) HISTTABLE) ',FN)
          (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?FN$) HISTTABLE) ',FN$)
          (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?ORIG-STOBJ) HISTTABLE) ',STOBJNAME)
          (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?FORMALS) HISTTABLE) ',FORMALS)
          (,(INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME '?STOBJS-OUT) HISTTABLE) ',STOBJS-OUT))
        `(encapsulate nil
          (local (in-theory (e/d* ,,ENABLE ,,DISABLE)))
          (defthm ,',THMNAME
            ,,BODY
            :hints ,,HINTS
            :rule-classes ,,RULE-CLASSES)
          ,@',(AND RULESET `((ADD-TO-RULESET ,RULESET ,THMNAME)))
          (add-stobj-preservation-record ,',FN
            ,',STOBJNAME
            ,',NAME
            ,',HISTTABLE))))))

mk-stobj-preservation-thmsfunction

(defun mk-stobj-preservation-thms
  (fn stobjname omit templates histtable state)
  (declare (xargs :mode :program :stobjs state))
  (if (atom templates)
    nil
    (if (and (cdar templates) (not (member (caar templates) omit)))
      (cons (mk-stobj-preservation-thm fn
          stobjname
          (car templates)
          histtable
          state)
        (mk-stobj-preservation-thms fn
          stobjname
          omit
          (cdr templates)
          histtable
          state))
      (mk-stobj-preservation-thms fn
        stobjname
        omit
        (cdr templates)
        histtable
        state))))

def-stobj-preservation-thms-fnfunction

(defun def-stobj-preservation-thms-fn
  (fn stobjname omit template-table histtable state)
  (declare (xargs :mode :program :stobjs state))
  (list* 'progn
    (mk-stobj-preservation-thms fn
      stobjname
      omit
      (reverse (table-alist template-table (w state)))
      histtable
      state)))

def-stobj-preservation-thmsmacro

(defmacro def-stobj-preservation-thms
  (fn &key (stobjname 'stobj) (omit 'nil) templates history)
  `(make-event (def-stobj-preservation-thms-fn ',FN
      ',STOBJNAME
      ',OMIT
      ',TEMPLATES
      ',HISTORY
      state)))

other

(defxdoc def-stobj-preservation-thms
  :parents (preservation-thms)
  :short "Prove the existing set of aigstobj preservation theorems for a given function"
  :long "See @(see acl2::preservation-thms) for complete documentation.")

mk-stobj-preservation-thms-each-fnfunction

(defun mk-stobj-preservation-thms-each-fn
  (records templates history state)
  (declare (xargs :mode :program :stobjs state))
  (if (atom records)
    nil
    (cons `(def-stobj-preservation-thms ,(CAAAR RECORDS)
        :stobjname ,(CDAAR RECORDS)
        :templates ,TEMPLATES
        :history ,HISTORY)
      (mk-stobj-preservation-thms-each-fn (cdr records)
        templates
        history
        state))))

do-stobj-preservation-thms-fnfunction

(defun do-stobj-preservation-thms-fn
  (unique-name templates history state)
  (declare (xargs :mode :program :stobjs state)
    (ignore unique-name))
  (cons 'progn
    (mk-stobj-preservation-thms-each-fn (reverse (table-alist history (w state)))
      templates
      history
      state)))

do-stobj-preservation-thmsmacro

(defmacro do-stobj-preservation-thms
  (unique-name &key templates history)
  `(make-event (do-stobj-preservation-thms-fn ',UNIQUE-NAME
      ',TEMPLATES
      ',HISTORY
      state)))

add-stobj-preservation-thm-fnfunction

(defun add-stobj-preservation-thm-fn
  (name vars
    body
    hints
    ruleset
    templates
    history
    deps
    enable
    disable
    rule-classes)
  (declare (ignorable history))
  `(progn (table ,TEMPLATES
      ',NAME
      ',(LIST VARS BODY HINTS RULESET DEPS ENABLE DISABLE RULE-CLASSES)) . ,(AND RULESET `((DEF-RULESET! ,RULESET NIL)))))

add-stobj-preservation-thmmacro

(defmacro add-stobj-preservation-thm
  (name &key
    vars
    body
    hints
    ruleset
    templates
    history
    deps
    enable
    disable
    (rule-classes ':rewrite))
  (add-stobj-preservation-thm-fn name
    vars
    body
    hints
    ruleset
    templates
    history
    deps
    enable
    disable
    rule-classes))

other

(defxdoc add-stobj-preservation-thm
  :parents (preservation-thms)
  :short "Add a theorem template to the def-stobj-preservation-thms database"
  :long "See @(see acl2::preservation-thms) for complete documentation.")

retroactive-add-stobj-preservation-thmmacro

(defmacro retroactive-add-stobj-preservation-thm
  (name &rest args &key templates history &allow-other-keys)
  `(encapsulate nil
    (local (table ,TEMPLATES nil nil :clear))
    (add-stobj-preservation-thm ,NAME . ,ARGS)
    (do-stobj-preservation-thms ,NAME
      :templates ,TEMPLATES
      :history ,HISTORY)))

other

(defxdoc retroactive-add-stobj-preservation-thm
  :parents (preservation-thms)
  :short "Add a theorem template to the def-stobj-preservation-thms database
and prove it about existing functions"
  :long "See @(see acl2::preservation-thms) for complete documentation.")

retroactive-add-stobj-preservation-thm-localmacro

(defmacro retroactive-add-stobj-preservation-thm-local
  (name &rest args &key templates history &allow-other-keys)
  `(progn (encapsulate nil
      (local (table ,TEMPLATES nil nil :clear))
      (local (add-stobj-preservation-thm ,NAME . ,ARGS))
      (do-stobj-preservation-thms ,NAME
        :templates ,TEMPLATES
        :history ,HISTORY))
    (local (add-stobj-preservation-thm ,NAME . ,ARGS))))

other

(defxdoc retroactive-add-stobj-preservation-thm-local
  :parents (preservation-thms)
  :short "Localy add a theorem template to the def-stobj-preservation-thms database
and (nonlocally) prove it about existing functions"
  :long "See @(see acl2::preservation-thms) for complete documentation.")

def-stobj-preservation-macros-fnfunction

(defun def-stobj-preservation-macros-fn
  (name default-stobjname templates history)
  (b* ((defthms-name (intern-in-package-of-symbol (concatenate 'string
           "DEF-"
           (symbol-name name)
           "-PRESERVATION-THMS")
         name)) (add-name (intern-in-package-of-symbol (concatenate 'string
            "ADD-"
            (symbol-name name)
            "-PRESERVATION-THM")
          name))
      (retro-name (intern-in-package-of-symbol (concatenate 'string
            "RETROACTIVE-ADD-"
            (symbol-name name)
            "-PRESERVATION-THM")
          name))
      (retro-local-name (intern-in-package-of-symbol (concatenate 'string
            "RETROACTIVE-ADD-"
            (symbol-name name)
            "-PRESERVATION-THM-LOCAL")
          name)))
    `(progn (defmacro ,DEFTHMS-NAME
        (fn &key (stobjname ',DEFAULT-STOBJNAME) omit)
        `(def-stobj-preservation-thms ,FN
          :stobjname ,STOBJNAME
          :omit ,OMIT
          :templates ,',TEMPLATES
          :history ,',HISTORY))
      (defxdoc ,DEFTHMS-NAME
        :parents (preservation-thms)
        :short "Generated by def-stobj-preservation-macros."
        :long "See @(see acl2::preservation-thms) for complete documentation.")
      (defmacro ,ADD-NAME
        (name &key
          vars
          body
          hints
          ruleset
          deps
          enable
          disable
          (rule-classes ':rewrite))
        `(add-stobj-preservation-thm ,NAME
          :vars ,VARS
          :body ,BODY
          :hints ,HINTS
          :deps ,DEPS
          :ruleset ,RULESET
          :templates ,',TEMPLATES
          :history ,',HISTORY
          :enable ,ENABLE
          :disable ,DISABLE
          :rule-classes ,RULE-CLASSES))
      (defxdoc ,ADD-NAME
        :parents (preservation-thms)
        :short "Generated by def-stobj-preservation-macros."
        :long "See @(see acl2::preservation-thms) for complete documentation.")
      (defmacro ,RETRO-NAME
        (name &rest args)
        `(retroactive-add-stobj-preservation-thm ,NAME
          ,@ARGS
          :templates ,',TEMPLATES
          :history ,',HISTORY))
      (defxdoc ,RETRO-NAME
        :parents (preservation-thms)
        :short "Generated by def-stobj-preservation-macros."
        :long "See @(see acl2::preservation-thms) for complete documentation.")
      (defmacro ,RETRO-LOCAL-NAME
        (name &rest args)
        `(retroactive-add-stobj-preservation-thm-local ,NAME
          ,@ARGS
          :templates ,',TEMPLATES
          :history ,',HISTORY))
      (defxdoc ,RETRO-LOCAL-NAME
        :parents (preservation-thms)
        :short "Generated by def-stobj-preservation-macros."
        :long "See @(see acl2::preservation-thms) for complete documentation."))))

def-stobj-preservation-macrosmacro

(defmacro def-stobj-preservation-macros
  (&key name default-stobjname templates history)
  (def-stobj-preservation-macros-fn name
    default-stobjname
    templates
    history))