hash-stobjs - ACL2 Book

Included Books

hons-remove-assoc top-with-meta assert-bang

other

(in-package "ACL2")

include-book

(include-book "std/alists/hons-remove-assoc" :dir :system)

hons-remove-assoc-acl2-count-weaktheorem

(defthm hons-remove-assoc-acl2-count-weak
  (<= (acl2-count (hons-remove-assoc x al)) (acl2-count al))
  :rule-classes :linear)

not-assoc-hons-remove-assoctheorem

(defthm not-assoc-hons-remove-assoc
  (not (hons-assoc-equal k (hons-remove-assoc k al))))

assoc-hons-remove-assoc-difftheorem

(defthm assoc-hons-remove-assoc-diff
  (implies (not (equal j k))
    (equal (hons-assoc-equal k (hons-remove-assoc j al))
      (hons-assoc-equal k al))))

hons-remove-assoc-repeattheorem

(defthm hons-remove-assoc-repeat
  (equal (hons-remove-assoc k (hons-remove-assoc k al))
    (hons-remove-assoc k al)))

local

(local (include-book "arithmetic/top-with-meta" :dir :system))

count-keys-hons-remove-assoctheorem

(defthm count-keys-hons-remove-assoc
  (equal (count-keys (hons-remove-assoc k al))
    (if (consp (hons-assoc-equal k al))
      (1- (count-keys al))
      (count-keys al))))

count-keys-constheorem

(defthm count-keys-cons
  (equal (count-keys (cons (cons k v) al))
    (if (consp (hons-assoc-equal k al))
      (count-keys al)
      (+ 1 (count-keys al)))))

prove-ht-theoremsmacro

(defmacro prove-ht-theorems
  (field stobj &optional renaming)
  (let ((get (defstobj-fnname field :accessor :hash-table renaming)) (boundp (defstobj-fnname field :boundp :hash-table renaming))
      (put (defstobj-fnname field :updater :hash-table renaming))
      (rem (defstobj-fnname field :remove :hash-table renaming))
      (count (defstobj-fnname field :count :hash-table renaming))
      (clear (defstobj-fnname field :clear :hash-table renaming))
      (init (defstobj-fnname field :init :hash-table renaming))
      (make (defstobj-fnname stobj :creator :hash-table renaming)))
    `(progn (defthm ,(PACKN-POS (LIST FIELD "-INIT-IS-CLEAR") FIELD)
        (equal (,INIT size rehash-size rehash-threshold ,STOBJ)
          (,CLEAR ,STOBJ)))
      (defthm ,(PACKN-POS (LIST FIELD "-GET-BOUNDP") FIELD)
        (implies (,GET k ,STOBJ) (,BOUNDP k ,STOBJ)))
      (defthm ,(PACKN-POS (LIST FIELD "-BOUNDP-START") FIELD)
        (not (,BOUNDP k (,MAKE))))
      (defthm ,(PACKN-POS (LIST FIELD "-BOUNDP-CLEAR") FIELD)
        (not (,BOUNDP k (,CLEAR ,STOBJ))))
      (defthm ,(PACKN-POS (LIST FIELD "-BOUNDP-PUT-SAME") FIELD)
        (,BOUNDP k (,PUT k v ,STOBJ)))
      (defthm ,(PACKN-POS (LIST FIELD "-BOUNDP-PUT-DIFF") FIELD)
        (implies (not (equal j k))
          (equal (,BOUNDP k (,PUT j v ,STOBJ)) (,BOUNDP k ,STOBJ))))
      (defthm ,(PACKN-POS (LIST FIELD "-GET-PUT-SAME") FIELD)
        (equal (,GET k (,PUT k v ,STOBJ)) v))
      (defthm ,(PACKN-POS (LIST FIELD "-GET-PUT-DIFF") FIELD)
        (implies (not (equal j k))
          (equal (,GET k (,PUT j v ,STOBJ)) (,GET k ,STOBJ))))
      (defthm ,(PACKN-POS (LIST FIELD "-REM-BOUNDP-SAME") FIELD)
        (not (,BOUNDP k (,REM k ,STOBJ))))
      (defthm ,(PACKN-POS (LIST FIELD "-REM-BOUNDP-DIFF") FIELD)
        (implies (not (equal j k))
          (equal (,BOUNDP k (,REM j ,STOBJ)) (,BOUNDP k ,STOBJ))))
      (defthm ,(PACKN-POS (LIST FIELD "-REM-GET-DIFF") FIELD)
        (implies (not (equal j k))
          (equal (,GET k (,REM j ,STOBJ)) (,GET k ,STOBJ))))
      (defthm ,(PACKN-POS (LIST FIELD "-COUNT-START") FIELD)
        (equal (,COUNT (,MAKE)) 0))
      (defthm ,(PACKN-POS (LIST FIELD "-COUNT-PUT") FIELD)
        (equal (,COUNT (,PUT k v ,STOBJ))
          (if (,BOUNDP k ,STOBJ)
            (,COUNT ,STOBJ)
            (+ 1 (,COUNT ,STOBJ)))))
      (defthm ,(PACKN-POS (LIST FIELD "-COUNT-REM") FIELD)
        (equal (,COUNT (,REM k ,STOBJ))
          (if (,BOUNDP k ,STOBJ)
            (- (,COUNT ,STOBJ) 1)
            (,COUNT ,STOBJ))))
      (defthm ,(PACKN-POS (LIST FIELD "-COUNT-CLEAR") FIELD)
        (equal (,COUNT (,CLEAR ,STOBJ)) 0)))))

local

(local (progn (defstobj bigstobj
      (bigarray :type (array (unsigned-byte 16) (100))
        :initially 0)
      (bighash :type (hash-table eql))
      (slowhash :type (hash-table equal))
      (eqhash :type (hash-table eq 70))
      (honshash :type (hash-table hons-equal)))
    (make-event (let* ((bigstobj (bighash-put 0 0 bigstobj)) (bigstobj (slowhash-put (list 0) 0 bigstobj))
          (bigstobj (eqhash-put 'a 0 bigstobj))
          (bigstobj (honshash-put (list 0) 0 bigstobj)))
        (mv nil '(value-triple :invisible) state bigstobj)))
    (include-book "std/testing/assert-bang" :dir :system)
    (assert! (equal (bighash-get 0 bigstobj) 0))
    (assert! (equal (slowhash-get '(0) bigstobj) 0))
    (assert! (equal (eqhash-get 'a bigstobj) 0))
    (assert! (equal (honshash-get '(0) bigstobj) 0))
    (defun init-stuff
      (n bigstobj state)
      (declare (xargs :stobjs (bigstobj state)
          :verify-guards nil
          :guard (natp n)))
      (if (zp n)
        (mv bigstobj state)
        (mv-let (rnd state)
          (random$ 10000 state)
          (let* ((bigstobj (update-bigarrayi n rnd bigstobj)) (bigstobj (bighash-put n rnd bigstobj))
              (bigstobj (slowhash-put (list n) rnd bigstobj))
              (bigstobj (eqhash-put (packn (list 'a n)) rnd bigstobj))
              (bigstobj (honshash-put (list n) rnd bigstobj)))
            (init-stuff (- n 1) bigstobj state)))))
    (make-event (mv-let (bigstobj state)
        (init-stuff 99 bigstobj state)
        (mv nil '(value-triple :invisible) state bigstobj)))
    (assert! (equal (bighash-count bigstobj) 100))
    (assert! (equal (slowhash-count bigstobj) 100))
    (assert! (equal (eqhash-count bigstobj) 100))
    (assert! (equal (honshash-count bigstobj) 100))
    (make-event (let* ((bigstobj (slowhash-put (cons 1 2) 3 bigstobj)) (bigstobj (slowhash-put (cons 1 2) 4 bigstobj))
          (bigstobj (honshash-put (cons 1 2) 3 bigstobj))
          (bigstobj (honshash-put (cons 1 2) 4 bigstobj)))
        (mv nil '(value-triple :invisible) state bigstobj)))
    (assert! (equal (slowhash-get (cons 1 2) bigstobj) 4))
    (assert! (equal (slowhash-count bigstobj) 101))
    (assert! (equal (honshash-get (cons 1 2) bigstobj) 4))
    (assert! (equal (honshash-count bigstobj) 101))
    (defun check-same
      (n bigstobj)
      (declare (xargs :stobjs (bigstobj)
          :verify-guards nil
          :guard (natp n)))
      (if (zp n)
        t
        (let ((expect (bigarrayi n bigstobj)))
          (and (equal (bighash-get n bigstobj) expect)
            (equal (slowhash-get (list n) bigstobj) expect)
            (equal (bighash-boundp n bigstobj) t)
            (equal (slowhash-boundp (list n) bigstobj) t)
            (equal (eqhash-boundp (packn (list 'a n)) bigstobj) t)
            (equal (honshash-boundp (list n) bigstobj) t)
            (equal (mv-list 2 (bighash-get? n bigstobj))
              (list expect t))
            (equal (mv-list 2 (slowhash-get? (list n) bigstobj))
              (list expect t))
            (equal (mv-list 2 (eqhash-get? (packn (list 'a n)) bigstobj))
              (list expect t))
            (equal (mv-list 2 (honshash-get? (list n) bigstobj))
              (list expect t))
            (check-same (- n 1) bigstobj)))))
    (assert! (check-same 99 bigstobj))
    (assert! (not (bighash-boundp 101 bigstobj)))
    (assert! (equal (mv-list 2 (bighash-get? 101 bigstobj))
        (list nil nil)))
    (assert! (not (slowhash-boundp 101 bigstobj)))
    (assert! (equal (mv-list 2 (slowhash-get? 101 bigstobj))
        (list nil nil)))
    (assert! (not (slowhash-boundp (list 101) bigstobj)))
    (assert! (equal (mv-list 2 (slowhash-get? (list 101) bigstobj))
        (list nil nil)))
    (assert! (not (eqhash-boundp (packn (list 'a 101)) bigstobj)))
    (assert! (equal (mv-list 2 (honshash-get? (packn (list 'a 101)) bigstobj))
        (list nil nil)))
    (assert! (not (honshash-boundp 101 bigstobj)))
    (assert! (equal (mv-list 2 (honshash-get? 101 bigstobj))
        (list nil nil)))
    (assert! (not (honshash-boundp (list 101) bigstobj)))
    (assert! (equal (mv-list 2 (honshash-get? (list 101) bigstobj))
        (list nil nil)))
    (make-event (let* ((bigstobj (bighash-rem 3 bigstobj)) (bigstobj (slowhash-rem (list 3) bigstobj))
          (bigstobj (eqhash-rem (packn (list 'a 3)) bigstobj))
          (bigstobj (honshash-rem (list 3) bigstobj)))
        (mv nil '(value-triple :invisible) state bigstobj)))
    (assert! (not (bighash-boundp 3 bigstobj)))
    (assert! (not (slowhash-boundp (list 3) bigstobj)))
    (assert! (not (eqhash-boundp (packn (list 'a 3)) bigstobj)))
    (assert! (not (honshash-boundp (list 3) bigstobj)))
    (assert! (equal (slowhash-count bigstobj) 100))
    (assert! (equal (honshash-count bigstobj) 100))
    (assert! (equal (bighash-count bigstobj) 99))
    (assert! (equal (eqhash-count bigstobj) 99))
    (make-event (let* ((bigstobj (slowhash-clear bigstobj)) (bigstobj (honshash-clear bigstobj))
          (bigstobj (bighash-init 10000 nil nil bigstobj))
          (bigstobj (eqhash-init 1 30 1/2 bigstobj)))
        (mv nil '(value-triple :invisible) state bigstobj)))
    (assert! (equal (bighash-count bigstobj) 0))
    (assert! (equal (slowhash-count bigstobj) 0))
    (assert! (equal (eqhash-count bigstobj) 0))
    (assert! (equal (honshash-count bigstobj) 0))
    (assert! (equal (bighash-get 5 bigstobj) nil))
    (assert! (equal (slowhash-get (list 5) bigstobj) nil))
    (assert! (equal (eqhash-get (packn (list 'a 5)) bigstobj) nil))
    (assert! (equal (slowhash-get (list 5) bigstobj) nil))))