{"action":"created","issue":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/189","labels_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/189/labels{/name}","comments_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/189/comments","events_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/189/events","html_url":"https://github.com/GaloisInc/cryptol/issues/189","id":62197485,"number":189,"title":"Symbolic execution much much much slower than concrete execution","user":{"login":"weaversa","id":7407930,"avatar_url":"https://avatars.githubusercontent.com/u/7407930?v=3","gravatar_id":"","url":"https://api.github.com/users/weaversa","html_url":"https://github.com/weaversa","followers_url":"https://api.github.com/users/weaversa/followers","following_url":"https://api.github.com/users/weaversa/following{/other_user}","gists_url":"https://api.github.com/users/weaversa/gists{/gist_id}","starred_url":"https://api.github.com/users/weaversa/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/weaversa/subscriptions","organizations_url":"https://api.github.com/users/weaversa/orgs","repos_url":"https://api.github.com/users/weaversa/repos","events_url":"https://api.github.com/users/weaversa/events{/privacy}","received_events_url":"https://api.github.com/users/weaversa/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-03-16T20:16:06Z","updated_at":"2015-03-16T21:05:17Z","closed_at":null,"body":"This might be an SBV problem, or a Cryptol problem. I'm not sure.\r\n\r\nThe test in `examples/SHA1.cry` is slow to execute concretely:\r\n```\r\n$ cryptol2\r\n                        _        _\r\n   ___ _ __ _   _ _ __ | |_ ___ | |\r\n  / __| '__| | | | '_ \\| __/ _ \\| |\r\n | (__| |  | |_| | |_) | || (_) | |\r\n  \\___|_|   \\__, | .__/ \\__\\___/|_|\r\n            |___/|_| version 2.1.0 (489a926)\r\n\r\nLoading module Cryptol\r\nCryptol> :s warnDefaulting=off\r\nCryptol> :l examples/SHA1.cry \r\nLoading module Cryptol\r\nLoading module Main\r\nMain> :! date\r\nMon Mar 16 16:08:50 EDT 2015\r\nMain> :check\r\nproperty testsPass Using exhaustive testing.\r\n  0%\r\npassed 1 tests.\r\nQ.E.D.\r\nMain> :!date\r\nMon Mar 16 16:11:39 EDT 2015\r\n```\r\nBut, when `:prove` is used, instead of `:check`, after 8 minutes `cryptol` has used 4.8 gigs of RAM and has not yet even called the solver.\r\n\r\nDoes someone see where it is getting stuck? Perhaps this is the next good example for optimization."},"comment":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/comments/81938511","html_url":"https://github.com/GaloisInc/cryptol/issues/189#issuecomment-81938511","issue_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/189","id":81938511,"user":{"login":"acfoltzer","id":205266,"avatar_url":"https://avatars.githubusercontent.com/u/205266?v=3","gravatar_id":"","url":"https://api.github.com/users/acfoltzer","html_url":"https://github.com/acfoltzer","followers_url":"https://api.github.com/users/acfoltzer/followers","following_url":"https://api.github.com/users/acfoltzer/following{/other_user}","gists_url":"https://api.github.com/users/acfoltzer/gists{/gist_id}","starred_url":"https://api.github.com/users/acfoltzer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/acfoltzer/subscriptions","organizations_url":"https://api.github.com/users/acfoltzer/orgs","repos_url":"https://api.github.com/users/acfoltzer/repos","events_url":"https://api.github.com/users/acfoltzer/events{/privacy}","received_events_url":"https://api.github.com/users/acfoltzer/received_events","type":"User","site_admin":false},"created_at":"2015-03-16T21:05:17Z","updated_at":"2015-03-16T21:05:17Z","body":"So, that file includes the following test:\r\n\r\n```\r\nt3 = sha1 [ 'a' | i <- [1..1000000] ] ==\r\n     0x34AA973CD4C4DAA4F61EEB2BDBAD27316534016F\r\n```\r\n\r\nSince there aren't any variables here, this is of limited value for optimizing the symbolic simulator because the real answer probably is to just fall back to the concrete evaluator when there's nothing symbolic.\r\n\r\n@LeventErkok, do you think SBV might benefit from this example as a stress test for concrete evaluation?"}}