Enhanced variant of known-packages.
(known-packages+ state) → pkg-names
This returns the same result as known-packages,
but it includes a run-time check (which should always succeed) on the result
that allows us to prove the return type theorem
without strengthening the guard on
(defun known-packages+ (state) (declare (xargs :stobjs (state))) (declare (xargs :guard t)) (let ((__function__ 'known-packages+)) (declare (ignorable __function__)) (b* ((result (known-packages state))) (if (string-listp result) result (raise "Internal error: ~ the list of keys ~x0 of the alist of known packages ~ is not a true list of strings." result)))))
(defthm string-listp-of-known-packages+ (b* ((pkg-names (known-packages+ state))) (string-listp pkg-names)) :rule-classes :rewrite)