unsound-read

(in-package "ACL2")

(defxdoc unsound-read
  :parents (std/io serialize)
  :short "A faster alternative to @(see serialize-read), which is unsound in
general, but may be fine in many common cases."
  :long "<p>The @('unsound-read') is like @(see serialize-read) except that it
does not take @(see state).  This means it works even in ordinary @(see
defconst) events, which avoids the performance penalty of using @(see
make-event) to read files, as described in @(see serialize-in-books).</p>

<p>As its name suggests, @('unsound-read') is unsound and it can easily be used
to prove @('nil'); see below.  Because of this, unlike the other @(see
serialize) routines, it is not build it into ACL2; instead, to use it you must
first include its book, which requires a <see topic='@(url defttag)'>trust
tag</see>:</p>

@({
 (include-book "std/io/unsound-read" :dir :system :ttags (:unsound-read))
})

<p>General form:</p>

@({
  (unsound-read filename
                [:hons-mode {:always, :never, :smart}]
                [:verbose   {t, nil}])
    -->
  obj
})

<p>The arguments are as in @(see serialize-read).</p>


<h3>Explanation of Unsoundness</h3>

<p>The logical problem with @('unsound-read') is that, like any other function,
it is expected to satisfy the functional equality axiom schema, namely,</p>

@({
  (equal (unsound-read-fn filename hons-mode verbosep)
         (unsound-read-fn filename hons-mode verbosep))
})

<p>But we can easily violate this property by modifying the file system between
calls of @('unsound-read').  For instance, here is a proof of @('nil') that is
carried out in @('std/io/serialize-tests.lisp'):</p>

@({
  (local
   (encapsulate
    ()
    ;; Write NIL to test.sao
    (make-event
     (let ((state (serialize-write "test.sao" nil)))
       (value '(value-triple :invisible))))

    ;; Prove that test.sao contains NIL.
    (defthm lemma-1
      (equal (unsound-read "test.sao") nil)
      :rule-classes nil)

    ;; Write T to test.sao
    (make-event
     (let ((state (serialize-write "test.sao" t)))
       (value '(value-triple :invisible))))

    ;; Prove that test.sao contains T.
    (defthm lemma-2
      (equal (unsound-read "test.sao") t)
      :rule-classes nil)

    ;; Arrive at our contradiction.
    (defthm qed
      nil
      :rule-classes nil
      :hints(("Goal"
              :use ((:instance lemma-1)
                    (:instance lemma-2))
              :in-theory (disable (unsound-read-fn)))))))
})

<h3>Avoiding Unsoundness</h3>

<p>If you want to safely use @('unsound-read') to read some file, @('foo.sao'),
then you should not change @('foo.sao') after reading it.</p>

<p>A common scenario is that you have some book, @('foo.lisp'), that uses
@('unsound-read') to load @('foo.sao'), using a @(see defconst) event.  In this
case, simply adding a @('depends-on') line such as:</p>

@({
    ; (depends-on "foo.sao")
    (defconst *contents* (unsound-read "foo.sao"))
})

<p>May, at least for users of @('cert.pl'), offer some minimal
protection. (This @('depends-on') line tells cert.pl to rebuild @('foo.cert')
any time that @('foo.sao') changes.)</p>")

(defttag :unsound-read)

(defstub unsound-read-fn-logical-def
  (filename honsp verbosep)
  t)

(include-raw "unsound-read-raw.lsp")