		Search-engine friendly clone of the ACL2 documentation.

Unsound-read

A faster alternative to serialize-read, which is unsound in general, but may be fine in many common cases.

The unsound-read is like serialize-read except that it does not take state. This means it works even in ordinary defconst events, which avoids the performance penalty of using make-event to read files, as described in serialize-in-books.

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 serialize routines, it is not build it into ACL2; instead, to use it you must first include its book, which requires a trust tag:

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

General form:

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

The arguments are as in serialize-read.

Explanation of Unsoundness

The logical problem with unsound-read is that, like any other function, it is expected to satisfy the functional equality axiom schema, namely,

(equal (unsound-read-fn filename hons-mode verbosep)
       (unsound-read-fn filename hons-mode verbosep))

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:

(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)))))))

Avoiding Unsoundness

If you want to safely use unsound-read to read some file, foo.sao, then you should not change foo.sao after reading it.

A common scenario is that you have some book, foo.lisp, that uses unsound-read to load foo.sao, using a defconst event. In this case, simply adding a depends-on line such as:

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

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.)