• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
        • Vl-zip
          • Vl-zip-opts-p
          • Vl-zipfile
            • Vl-zipfile-fix
            • Vl-read-zip-header
              • Vl-read-zip-header-aux
              • Vl-read-zip-aux
            • Vl-maybe-zipfile
            • Vl-read-zip
            • Make-vl-zipfile
            • Vl-zipfile-equiv
            • Vl-zipfile-p
            • Change-vl-zipfile
            • Vl-zipfile->syntax
            • Vl-zipfile->filemap
            • Vl-zipfile->design
            • Vl-zipfile->defines
            • Vl-zipfile->name
            • Vl-zipfile->ltime
            • Vl-zipfile->date
            • Vl-write-zip
          • *vl-zip-help*
          • Vl-zip-top
          • Vl-zip-main
        • Vl-main
        • Split-plusargs
        • Vl-shell
        • Vl-json
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-read-zip-header

Vl-read-zip-header-aux

Signature

(vl-read-zip-header-aux channel &key (name 'name) 
                        (syntax 'syntax) 
                        (date 'date) 
                        (ltime 'ltime) 
                        (state 'state)) 
 
  → 
(mv name syntax date ltime new-state)

Arguments

channel — Guard (and (symbolp channel) (open-input-channel-p channel :object state)).

name — Guard (maybe-stringp name).

syntax — Guard (maybe-stringp syntax).

date — Guard (maybe-stringp date).

ltime — Guard (maybe-natp ltime).

Returns

name — Type (maybe-stringp name).

syntax — Type (maybe-stringp syntax).

date — Type (maybe-stringp date).

ltime — Type (maybe-natp ltime).

Definitions and Theorems

Function: vl-read-zip-header-aux-fn

(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: maybe-stringp-of-vl-read-zip-header-aux.name

(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: maybe-stringp-of-vl-read-zip-header-aux.syntax

(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: maybe-stringp-of-vl-read-zip-header-aux.date

(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: maybe-natp-of-vl-read-zip-header-aux.ltime

(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: state-p1-of-vl-read-zip-version-aux

(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: open-input-channel-p1-of-vl-read-zip-version-aux

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