(vl-read-zip-header-aux channel &key (name 'name) (syntax 'syntax) (date 'date) (ltime 'ltime) (state 'state)) → (mv name syntax date ltime new-state)
Function:
(defun vl-read-zip-header-aux-fn (channel name syntax date ltime state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (maybe-stringp name) (maybe-stringp syntax) (maybe-stringp date) (maybe-natp ltime) (and (symbolp channel) (open-input-channel-p channel :object state))))) (let ((__function__ 'vl-read-zip-header-aux)) (declare (ignorable __function__)) (b* ((name (maybe-string-fix name)) (syntax (maybe-string-fix syntax)) (date (maybe-string-fix date)) (ltime (mbe :logic (if (maybe-natp ltime) ltime nil) :exec ltime)) ((unless (mbt (state-p state))) (mv name syntax date ltime state)) ((mv eofp obj state) (read-object channel state)) ((when eofp) (mv name syntax date ltime state)) ((unless (and (tuplep 2 obj) (symbolp (first obj)))) (vl-read-zip-header-aux channel)) ((list key value) obj) (name (if (and (eq key :name) (stringp value)) value name)) (syntax (if (and (eq key :syntax) (stringp value)) value syntax)) (date (if (and (eq key :date) (stringp value)) value date)) (ltime (if (and (eq key :ltime) (natp value)) value ltime)) ((when (and name syntax date ltime)) (mv name syntax date ltime state))) (vl-read-zip-header-aux channel))))
Theorem:
(defthm maybe-stringp-of-vl-read-zip-header-aux.name (b* (((mv ?name ?syntax ?date ?ltime ?new-state) (vl-read-zip-header-aux-fn channel name syntax date ltime state))) (maybe-stringp name)) :rule-classes :type-prescription)
Theorem:
(defthm maybe-stringp-of-vl-read-zip-header-aux.syntax (b* (((mv ?name ?syntax ?date ?ltime ?new-state) (vl-read-zip-header-aux-fn channel name syntax date ltime state))) (maybe-stringp syntax)) :rule-classes :type-prescription)
Theorem:
(defthm maybe-stringp-of-vl-read-zip-header-aux.date (b* (((mv ?name ?syntax ?date ?ltime ?new-state) (vl-read-zip-header-aux-fn channel name syntax date ltime state))) (maybe-stringp date)) :rule-classes :type-prescription)
Theorem:
(defthm maybe-natp-of-vl-read-zip-header-aux.ltime (b* (((mv ?name ?syntax ?date ?ltime ?new-state) (vl-read-zip-header-aux-fn channel name syntax date ltime state))) (maybe-natp ltime)) :rule-classes :type-prescription)
Theorem:
(defthm state-p1-of-vl-read-zip-version-aux (b* (((mv ?name ?syntax ?date ?ltime ?new-state) (vl-read-zip-header-aux-fn channel name syntax date ltime state))) (implies (and (state-p1 state) (symbolp channel) (open-input-channel-p1 channel :object state)) (state-p1 new-state))))
Theorem:
(defthm open-input-channel-p1-of-vl-read-zip-version-aux (b* (((mv ?name ?syntax ?date ?ltime ?new-state) (vl-read-zip-header-aux-fn channel name syntax date ltime state))) (implies (and (state-p1 state) (symbolp channel) (open-input-channel-p1 channel :object state)) (open-input-channel-p1 channel :object new-state))))