{"action":"created","issue":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/158","labels_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/158/labels{/name}","comments_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/158/comments","events_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/158/events","html_url":"https://github.com/GaloisInc/cryptol/issues/158","id":54384498,"number":158,"title":":sat and :prove fail on symbolic shifts with small-width index","user":{"login":"brianhuffman","id":619882,"avatar_url":"https://avatars.githubusercontent.com/u/619882?v=3","gravatar_id":"","url":"https://api.github.com/users/brianhuffman","html_url":"https://github.com/brianhuffman","followers_url":"https://api.github.com/users/brianhuffman/followers","following_url":"https://api.github.com/users/brianhuffman/following{/other_user}","gists_url":"https://api.github.com/users/brianhuffman/gists{/gist_id}","starred_url":"https://api.github.com/users/brianhuffman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/brianhuffman/subscriptions","organizations_url":"https://api.github.com/users/brianhuffman/orgs","repos_url":"https://api.github.com/users/brianhuffman/repos","events_url":"https://api.github.com/users/brianhuffman/events{/privacy}","received_events_url":"https://api.github.com/users/brianhuffman/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-01-14T22:12:54Z","updated_at":"2015-01-15T18:48:57Z","closed_at":"2015-01-15T18:48:57Z","body":"Cryptol fails to find a satisfying assignment for any formula containing a shift by a symbolic amount, if an index of width n is used to shift a bitvector of width greater than  2^n. (For example, shifting an 8-bit word by a 2-bit index, or a 32-bit word by a 4-bit index.) Even a reflexive equality is unprovable:\r\n\r\n    Cryptol> :sat \\(i:[2]) -> (1:[8]) << i == (1:[8]) << i\r\n    Unsatisfiable.\r\n\r\nUsing the `offline` prover shows what is going on. The symbolic shift of an 8-bit word is turned into an 8-entry lookup table. The contents of the lookup table are defined by a sequence of `assert` statements, which in this case are inconsistent.\r\n\r\n    Cryptol> :set prover=offline\r\n    Cryptol> :sat \\(i:[2]) -> (1:[8]) << i == (1:[8]) << i\r\n    Writing to SMT-Lib file standard output...\r\n    To determine the satisfiability of the expression, use an external SMT solver.\r\n    ; Automatically generated by SBV. Do not edit.\r\n    ; Created on Wed Jan 14 13:56:19 PST 2015\r\n    (set-option :produce-models true)\r\n    (set-logic QF_UFBV)\r\n    ; --- uninterpreted sorts ---\r\n    ; --- literal constants ---\r\n    (define-fun s_2 () Bool false)\r\n    (define-fun s_1 () Bool true)\r\n    (define-fun s1 () (_ BitVec 8) #x01)\r\n    (define-fun s2 () (_ BitVec 8) #x02)\r\n    (define-fun s3 () (_ BitVec 8) #x04)\r\n    (define-fun s4 () (_ BitVec 8) #x08)\r\n    (define-fun s5 () (_ BitVec 8) #x10)\r\n    (define-fun s6 () (_ BitVec 8) #x20)\r\n    (define-fun s7 () (_ BitVec 8) #x40)\r\n    (define-fun s8 () (_ BitVec 8) #x80)\r\n    (define-fun s9 () (_ BitVec 8) #x00)\r\n    ; --- skolem constants ---\r\n    (declare-fun s0 () (_ BitVec 2))\r\n    ; --- constant tables ---\r\n    (declare-fun table0 ((_ BitVec 2)) (_ BitVec 8))\r\n    (assert (= (table0 #b00) s1))\r\n    (assert (= (table0 #b01) s2))\r\n    (assert (= (table0 #b10) s3))\r\n    (assert (= (table0 #b11) s4))\r\n    (assert (= (table0 #b00) s5))\r\n    (assert (= (table0 #b01) s6))\r\n    (assert (= (table0 #b10) s7))\r\n    (assert (= (table0 #b11) s8))\r\n    ; --- skolemized tables ---\r\n    ; --- arrays ---\r\n    ; --- uninterpreted constants ---\r\n    ; --- user given axioms ---\r\n    ; --- formula ---\r\n    (assert ; no quantifiers\r\n       (let ((s10 (table0 s0)))\r\n       s_1))\r\n    (check-sat)\r\n\r\nCryptol's symbolic simulator uses `sbvShiftLeft` and `sbvShiftRight` from the SBV library to implement left and right shifts. It looks like those functions are buggy when used with a too-small index."},"comment":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/comments/70138858","html_url":"https://github.com/GaloisInc/cryptol/issues/158#issuecomment-70138858","issue_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/158","id":70138858,"user":{"login":"brianhuffman","id":619882,"avatar_url":"https://avatars.githubusercontent.com/u/619882?v=3","gravatar_id":"","url":"https://api.github.com/users/brianhuffman","html_url":"https://github.com/brianhuffman","followers_url":"https://api.github.com/users/brianhuffman/followers","following_url":"https://api.github.com/users/brianhuffman/following{/other_user}","gists_url":"https://api.github.com/users/brianhuffman/gists{/gist_id}","starred_url":"https://api.github.com/users/brianhuffman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/brianhuffman/subscriptions","organizations_url":"https://api.github.com/users/brianhuffman/orgs","repos_url":"https://api.github.com/users/brianhuffman/repos","events_url":"https://api.github.com/users/brianhuffman/events{/privacy}","received_events_url":"https://api.github.com/users/brianhuffman/received_events","type":"User","site_admin":false},"created_at":"2015-01-15T18:48:57Z","updated_at":"2015-01-15T18:48:57Z","body":"Thanks to @LeventErkok for fixing the problem in the upstream sbv library (LeventErkok/sbv#103). I have now merged the patch into our fork in revision 5f8b8947d4e1a0f2a2e4c283db3fdc762dab2a20."}}