{"action":"closed","issue":{"url":"https://api.github.com/repos/acl2/acl2/issues/380","labels_url":"https://api.github.com/repos/acl2/acl2/issues/380/labels{/name}","comments_url":"https://api.github.com/repos/acl2/acl2/issues/380/comments","events_url":"https://api.github.com/repos/acl2/acl2/issues/380/events","html_url":"https://github.com/acl2/acl2/issues/380","id":76457506,"number":380,"title":"bitops/fast-logext","user":{"login":"jaredcdavis","id":6493363,"avatar_url":"https://avatars.githubusercontent.com/u/6493363?v=3","gravatar_id":"","url":"https://api.github.com/users/jaredcdavis","html_url":"https://github.com/jaredcdavis","followers_url":"https://api.github.com/users/jaredcdavis/followers","following_url":"https://api.github.com/users/jaredcdavis/following{/other_user}","gists_url":"https://api.github.com/users/jaredcdavis/gists{/gist_id}","starred_url":"https://api.github.com/users/jaredcdavis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaredcdavis/subscriptions","organizations_url":"https://api.github.com/users/jaredcdavis/orgs","repos_url":"https://api.github.com/users/jaredcdavis/repos","events_url":"https://api.github.com/users/jaredcdavis/events{/privacy}","received_events_url":"https://api.github.com/users/jaredcdavis/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/acl2/acl2/labels/Difficulty:%20Easy","name":"Difficulty: Easy","color":"FFFFFF"},{"url":"https://api.github.com/repos/acl2/acl2/labels/enhancement","name":"enhancement","color":"84b6eb"},{"url":"https://api.github.com/repos/acl2/acl2/labels/Performance","name":"Performance","color":"FFFFFF"}],"state":"closed","locked":false,"assignee":null,"milestone":{"url":"https://api.github.com/repos/acl2/acl2/milestones/5","html_url":"https://github.com/acl2/acl2/milestones/7.2","labels_url":"https://api.github.com/repos/acl2/acl2/milestones/5/labels","id":1092563,"number":5,"title":"7.2","description":"","creator":{"login":"ragerdl","id":2245886,"avatar_url":"https://avatars.githubusercontent.com/u/2245886?v=3","gravatar_id":"","url":"https://api.github.com/users/ragerdl","html_url":"https://github.com/ragerdl","followers_url":"https://api.github.com/users/ragerdl/followers","following_url":"https://api.github.com/users/ragerdl/following{/other_user}","gists_url":"https://api.github.com/users/ragerdl/gists{/gist_id}","starred_url":"https://api.github.com/users/ragerdl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ragerdl/subscriptions","organizations_url":"https://api.github.com/users/ragerdl/orgs","repos_url":"https://api.github.com/users/ragerdl/repos","events_url":"https://api.github.com/users/ragerdl/events{/privacy}","received_events_url":"https://api.github.com/users/ragerdl/received_events","type":"User","site_admin":false},"open_issues":3,"closed_issues":4,"state":"open","created_at":"2015-05-01T14:30:13Z","updated_at":"2015-06-30T23:07:49Z","due_on":null,"closed_at":null},"comments":0,"created_at":"2015-05-14T19:03:57Z","updated_at":"2015-06-30T23:07:49Z","closed_at":"2015-06-30T23:07:49Z","body":"Shilpi discovered that fast-logext 64 is not actually fast and developed a better alternative.  Making an issue to remind us to integrate this properly...\r\n\r\n```\r\nI've included some stand-alone ACL2 events below, including my\r\ndefinition of 64-bit sign extension, n64-to-i64. (n64-to-i64 x)\r\nhas been proved equal to (logext 64 x).\r\n\r\n;; ======================================================================\r\n\r\n(in-package \"ACL2\")\r\n(local (include-book \"centaur/bitops/ihs-extensions\" :dir :system))\r\n(local (include-book \"centaur/bitops/logbitp-bounds\" :dir :system))\r\n\r\n(local\r\n (encapsulate\r\n  ()\r\n\r\n  (local (include-book \"arithmetic/top-with-meta\" :dir :system))\r\n\r\n  (defthm logext-is-the-same-as-ntoi-helper-1\r\n    (implies (and (unsigned-byte-p (1+ n) x)\r\n                  (<= 0 n)\r\n                  (< x (expt 2 n)))\r\n             (equal (loghead n x) x)))))\r\n\r\n(local\r\n (encapsulate\r\n  ()\r\n  (local (include-book \"arithmetic-5/top\" :dir :system))\r\n\r\n  (defthm logext-is-the-same-as-ntoi-helper-2\r\n    (implies (and (unsigned-byte-p (1+ n) x)\r\n                  (not (zp (1+ n)))\r\n                  (<= (expt 2 n) x))\r\n             (equal (logapp n x -1)\r\n                    (+ x (- (expt 2 (1+ n))))))\r\n    :hints ((\"Goal\" :in-theory (e/d (logapp loghead) ()))))\r\n\r\n  (defthm logext-is-the-same-as-ntoi-helper-3\r\n    (implies (and (unsigned-byte-p (1+ n) x)\r\n                  (logbitp n x)\r\n                  (natp n)\r\n                  (< x (expt 2 n)))\r\n             (equal (logapp n x -1)\r\n                    x))\r\n    :hints ((\"Goal\" :in-theory (e/d (logapp logbitp) ()))))))\r\n\r\n(defun-inline n64-to-i64 (x)\r\n  (declare (type (unsigned-byte 64) x)\r\n           (xargs\r\n            :guard-hints ((\"Goal\" :in-theory\r\n                           (e/d (logext) ())))))\r\n  (mbe :logic (logext 64 x)\r\n       :exec\r\n       (if (< x 9223372036854775808) ;; 2^63\r\n           x\r\n         (- x 18446744073709551616 ;; 2^64\r\n            ))))\r\n\r\n;; ----------------------------------------------------------------------\r\n\r\n;; Some misleading timing tests (similar to those at the end of\r\n;; centaur/bitops/fast-logext):\r\n\r\n(local (include-book \"centaur/bitops/fast-logext\" :dir :system))\r\n\r\n(value :q)\r\n\r\n(time (loop for i  from 1 to 100000000 do (logext 64 i)))       ;;\r\n17.224293 sec, 6.4G\r\n(time (loop for i  from 1 to 100000000 do (fast-logext 64 i)))  ;;\r\n0.058751  sec\r\n(time (loop for i  from 1 to 100000000 do (n64-to-i64 i)))      ;;\r\n1.769468  sec\r\n\r\n;; ----------------------------------------------------------------------\r\n\r\n;; Some timing tests that aren't misleading:\r\n\r\n(defun fast-logext-test ()\r\n  (loop for i fixnum from 1 to 100000000 when (zerop (fast-logext 64 i))\r\n        do (return 17)))\r\n\r\n(time$ (fast-logext-test)) ;; 21.48 sec, 6.4G\r\n\r\n(defun ntoi-test ()\r\n  (loop for i fixnum from 1 to 100000000 when (zerop (n64-to-i64 i))\r\n        do (return 17)))\r\n\r\n(time$ (ntoi-test)) ;; 0.93 sec, 0 bytes\r\n\r\n;; ======================================================================\r\n```"}}