acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / add-ons / hash-stobjs.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "ACL2-HACKER" (APPEND (QUOTE (VALUE SET-W! ASSERT-EVENT MSG LD-EVISC-TUPLE CONNECTED-BOOK-DIRECTORY GUARD-CHECKING-ON INHIBIT-OUTPUT-LST PRINT-CLAUSE-IDS ACL2-RAW-MODE-P RAW-MODE-RESTORE-LST SAVED-OUTPUT-TOKEN-LST TAINTED-OKP IN-PACKAGE-FN DEFPKG-FN PE! TRANS! PSO PSO! VALUE-TRIPLE DEFAULT-EVISC-TUPLE TTAG HARD SOFT PROGN! UNTOUCHABLE-FNS UNTOUCHABLE-VARS LD-REDEFINITION-ACTION SET-LD-SKIP-PROOFSP SET-LD-REDEFINITION-ACTION SET-LD-PROMPT SET-LD-KEYWORD-ALIASES SET-LD-PRE-EVAL-FILTER SET-LD-ERROR-TRIPLES SET-LD-ERROR-ACTION SET-LD-QUERY-CONTROL-ALIST SET-CBD-FN SET-RAW-MODE SET-RAW-MODE-FN SET-TAINTED-OKP PUSH-UNTOUCHABLE-FN REMOVE-UNTOUCHABLE-FN SET-RAW-MODE-ON SET-RAW-MODE-OFF TEMP-TOUCHABLE-VARS TEMP-TOUCHABLE-FNS SET-TEMP-TOUCHABLE-VARS SET-TEMP-TOUCHABLE-FNS BUILT-IN-PROGRAM-MODE-FNS PROGRAM-FNS-WITH-RAW-CODE GLOBAL-VALUE CURRENT-ACL2-WORLD LD-LEVEL *WORMHOLEP* RAW-MODE-P MAX-ABSOLUTE-EVENT-NUMBER GETPROP ER-LET* *VALID-OUTPUT-NAMES* STATE-GLOBAL-LET* EXTENSION ABSOLUTE-TO-RELATIVE-COMMAND-NUMBER ACCESS-COMMAND-TUPLE-NUMBER GLOBAL-SET-LST COMMAND-NUMBER-BASELINE EVENT-NUMBER-BASELINE NEXT-ABSOLUTE-COMMAND-NUMBER ADD-COMMAND-LANDMARK NEXT-ABSOLUTE-EVENT-NUMBER ADD-EVENT-LANDMARK SCAN-TO-COMMAND CERTIFY-BOOK-FN F-GET-GLOBAL F-PUT-GLOBAL F-BOUNDP-GLOBAL CHECKPOINT-PROCESSORS GLOBAL-VAL ACL2-VERSION EARLIER-ACL2-VERSIONP)) (QUOTE (PROGN!-WITH-BINDINGS HACKER PROGN+TOUCHABLE PROGN=TOUCHABLE PROGN!+TOUCHABLE PROGN!=TOUCHABLE WITH-TOUCHABLE PROGN+REDEF WITH-REDEF-ALLOWED IN-RAW-MODE WITH-RAW-MODE ASSERT-PROGRAM-MODE ENSURE-PROGRAM-ONLY-FLAG ENSURE-PROGRAM-ONLY HAS-SPECIAL-RAW-DEFINITION ENSURE-SPECIAL-RAW-DEFINITION-FLAG ASSERT-NO-SPECIAL-RAW-DEFINITION RECONSTRUCT-DECLARE-LST MODIFY-RAW-DEFUN-PERMANENT PROGN+ALL-TTAGS-ALLOWED DEFLABELS TTAG-SKIP-PROOFS PROGN+TTAG-SKIP-PROOFS)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)))
(DEFPKG "XDOC" (SET-DIFFERENCE-EQ (UNION-EQ (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (B* QUIT EXIT VALUE DEFXDOC DEFXDOC-RAW MACRO-ARGS XDOC-EXTEND DEFSECTION DEFSECTION-PROGN CUTIL LNFIX SET-DEFAULT-PARENTS GETPROP FORMALS JUSTIFICATION DEF-BODIES CURRENT-ACL2-WORLD DEF-BODY ACCESS THEOREM UNTRANSLATED-THEOREM GUARD XDOC XDOC! UNQUOTE UNDOCUMENTED ASSERT! TOP EXPLODE IMPLODE))) (QUOTE NIL)) NIL ((:SYSTEM . "xdoc/portcullis.lisp") (:SYSTEM . "xdoc/top.lisp") (:SYSTEM . "arithmetic/nat-listp.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "arithmetic/top-with-meta.lisp")) T)
(DEFPKG "ACL2-CRG" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "arithmetic/top-with-meta.lisp")) T)
(DEFPKG "ACL2-AGP" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "arithmetic/top-with-meta.lisp")) T)
(DEFPKG "ACL2-ASG" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "arithmetic/top-with-meta.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((27 RECORD-EXPANSION (LOCAL (PROGN (DEFSTOBJ BIGSTOBJ (BIGARRAY :TYPE (ARRAY (UNSIGNED-BYTE 16) (100)) :INITIALLY 0) (BIGHASH :TYPE (HASH-TABLE EQL)) (SLOWHASH :TYPE (HASH-TABLE EQUAL))) (MAKE-EVENT (LET* ((BIGSTOBJ (BIGHASH-PUT 0 0 BIGSTOBJ)) (BIGSTOBJ (SLOWHASH-PUT (LIST 0) 0 BIGSTOBJ))) (MV NIL (QUOTE (VALUE-TRIPLE :INVISIBLE)) STATE BIGSTOBJ))) (INCLUDE-BOOK "misc/assert" :DIR :SYSTEM) (ASSERT! (EQUAL (BIGHASH-GET 0 BIGSTOBJ) 0)) (ASSERT! (EQUAL (SLOWHASH-GET (QUOTE (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))) (INIT-STUFF (- N 1) BIGSTOBJ STATE))))) (MAKE-EVENT (MV-LET (BIGSTOBJ STATE) (INIT-STUFF 99 BIGSTOBJ STATE) (MV NIL (QUOTE (VALUE-TRIPLE :INVISIBLE)) STATE BIGSTOBJ))) (ASSERT! (EQUAL (BIGHASH-COUNT BIGSTOBJ) 100)) (ASSERT! (EQUAL (SLOWHASH-COUNT BIGSTOBJ) 100)) (MAKE-EVENT (LET* ((BIGSTOBJ (SLOWHASH-PUT (CONS 1 2) 3 BIGSTOBJ)) (BIGSTOBJ (SLOWHASH-PUT (CONS 1 2) 4 BIGSTOBJ))) (MV NIL (QUOTE (VALUE-TRIPLE :INVISIBLE)) STATE BIGSTOBJ))) (ASSERT! (EQUAL (SLOWHASH-GET (CONS 1 2) BIGSTOBJ) 4)) (ASSERT! (EQUAL (SLOWHASH-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 (MV-LIST 2 (BIGHASH-GET? N BIGSTOBJ)) (LIST EXPECT T)) (EQUAL (MV-LIST 2 (SLOWHASH-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))) (MAKE-EVENT (LET* ((BIGSTOBJ (BIGHASH-REM 3 BIGSTOBJ)) (BIGSTOBJ (SLOWHASH-REM (LIST 3) BIGSTOBJ))) (MV NIL (QUOTE (VALUE-TRIPLE :INVISIBLE)) STATE BIGSTOBJ))) (ASSERT! (NOT (BIGHASH-BOUNDP 3 BIGSTOBJ))) (ASSERT! (NOT (SLOWHASH-BOUNDP (LIST 3) BIGSTOBJ))) (ASSERT! (EQUAL (SLOWHASH-COUNT BIGSTOBJ) 100)) (ASSERT! (EQUAL (BIGHASH-COUNT BIGSTOBJ) 99)) (MAKE-EVENT (LET* ((BIGSTOBJ (SLOWHASH-CLEAR BIGSTOBJ)) (BIGSTOBJ (BIGHASH-INIT 10000 NIL NIL BIGSTOBJ))) (MV NIL (QUOTE (VALUE-TRIPLE :INVISIBLE)) STATE BIGSTOBJ))) (ASSERT! (EQUAL (BIGHASH-COUNT BIGSTOBJ) 0)) (ASSERT! (EQUAL (SLOWHASH-COUNT BIGSTOBJ) 0)) (ASSERT! (EQUAL (BIGHASH-GET 5 BIGSTOBJ) NIL)) (ASSERT! (EQUAL (SLOWHASH-GET (LIST 5) BIGSTOBJ) NIL)))) (LOCAL (VALUE-TRIPLE :ELIDED))))
NIL
(("/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp" "hash-stobjs" "hash-stobjs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:HASH-STOBJS "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp") (:REDEF+ "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp"))) . 1257498041) (LOCAL ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729)) (LOCAL ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 304413851)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1403689963)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1629957550)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370)) (LOCAL ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095)) (LOCAL ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063)) (LOCAL ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148)) (LOCAL ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1939433116)))
74794251