{"action":"created","issue":{"url":"https://api.github.com/repos/tamarin-prover/tamarin-prover/issues/297","repository_url":"https://api.github.com/repos/tamarin-prover/tamarin-prover","labels_url":"https://api.github.com/repos/tamarin-prover/tamarin-prover/issues/297/labels{/name}","comments_url":"https://api.github.com/repos/tamarin-prover/tamarin-prover/issues/297/comments","events_url":"https://api.github.com/repos/tamarin-prover/tamarin-prover/issues/297/events","html_url":"https://github.com/tamarin-prover/tamarin-prover/pull/297","id":371199933,"node_id":"MDExOlB1bGxSZXF1ZXN0MjIzNzAwNjIy","number":297,"title":"Compute variants directly in Maude","user":{"login":"kmilner","id":8351604,"node_id":"MDQ6VXNlcjgzNTE2MDQ=","avatar_url":"https://avatars2.githubusercontent.com/u/8351604?v=4","gravatar_id":"","url":"https://api.github.com/users/kmilner","html_url":"https://github.com/kmilner","followers_url":"https://api.github.com/users/kmilner/followers","following_url":"https://api.github.com/users/kmilner/following{/other_user}","gists_url":"https://api.github.com/users/kmilner/gists{/gist_id}","starred_url":"https://api.github.com/users/kmilner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kmilner/subscriptions","organizations_url":"https://api.github.com/users/kmilner/orgs","repos_url":"https://api.github.com/users/kmilner/repos","events_url":"https://api.github.com/users/kmilner/events{/privacy}","received_events_url":"https://api.github.com/users/kmilner/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2018-10-17T18:01:47Z","updated_at":"2018-10-17T18:45:45Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/tamarin-prover/tamarin-prover/pulls/297","html_url":"https://github.com/tamarin-prover/tamarin-prover/pull/297","diff_url":"https://github.com/tamarin-prover/tamarin-prover/pull/297.diff","patch_url":"https://github.com/tamarin-prover/tamarin-prover/pull/297.patch"},"body":"I know previously there was some issue with Maude's variant generation (or it didn't exist?) but from some testing it seems to work now, at least with all of the case studies.\r\n\r\nIf we can use it, it is much faster than the the iterated unification calls to maude that are used currently, which scale very poorly in the number of variants. An example from @galadran:\r\n\r\n```theory splitTest\r\nbegin\r\n\r\nbuiltins: diffie-hellman\r\n\r\nrule testDH:\r\n    [In(<<x,y>,<z,w>>)]\r\n  --[]->\r\n    [Out(<x^z,y^w>)]\r\n\r\nend\r\n```\r\nhas 2209 variants, which takes over 7 hours to partially evaluate on a large server using the develop branch. After this change, the same theory can be partially evaluated on my laptop in just over 7 minutes.\r\n\r\nOn a smaller theory with 47 variants, \r\n```theory normTest\r\nbegin\r\n\r\nbuiltins: diffie-hellman\r\n\r\nrule testDH:\r\n    [In(<x,y>)]\r\n  --[]->\r\n    [Out(x^y)]\r\n\r\nend\r\n```\r\nthe time to partially evaluate drops from ~8 seconds to ~2 seconds.\r\n\r\nIn general this has only small effects on the existing case studies, as most of the time is dominated by theorem proving, though a few examples improve pretty dramatically:  `ake/bilinear/Joux_analyzed.spthy` and `ake/bilinear/Joux_EphkRev_analyzed.spthy` get about 4x faster. From the `examples/sp14/` folder, in @galadran's testing:\r\n\r\n> group_joux is now 16 seconds (down from 102 seconds)\r\n> Joux1 has improved from 70 seconds to 5.4 seconds\r\n> Joux2 has improved from 71 seconds to 8 seconds\r\n> Moderate improvements on all the other case studies as well\r\n\r\nThe variants generated by maude end up having different names in them, which leads to a fairly large diff, but so far as we can tell the actual variants and proofs are the same. The renaming leads to a couple files files running slightly slower, I believe because the different order of variants returned by maude ends up reordering some of the cases.\r\n\r\n@galadran is just rerunning full regression tests which we'll post here when they're ready, for anyone who is interested in checking the timing/proof diffs."},"comment":{"url":"https://api.github.com/repos/tamarin-prover/tamarin-prover/issues/comments/430744039","html_url":"https://github.com/tamarin-prover/tamarin-prover/pull/297#issuecomment-430744039","issue_url":"https://api.github.com/repos/tamarin-prover/tamarin-prover/issues/297","id":430744039,"node_id":"MDEyOklzc3VlQ29tbWVudDQzMDc0NDAzOQ==","user":{"login":"rsasse","id":2189451,"node_id":"MDQ6VXNlcjIxODk0NTE=","avatar_url":"https://avatars3.githubusercontent.com/u/2189451?v=4","gravatar_id":"","url":"https://api.github.com/users/rsasse","html_url":"https://github.com/rsasse","followers_url":"https://api.github.com/users/rsasse/followers","following_url":"https://api.github.com/users/rsasse/following{/other_user}","gists_url":"https://api.github.com/users/rsasse/gists{/gist_id}","starred_url":"https://api.github.com/users/rsasse/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/rsasse/subscriptions","organizations_url":"https://api.github.com/users/rsasse/orgs","repos_url":"https://api.github.com/users/rsasse/repos","events_url":"https://api.github.com/users/rsasse/events{/privacy}","received_events_url":"https://api.github.com/users/rsasse/received_events","type":"User","site_admin":false},"created_at":"2018-10-17T18:45:45Z","updated_at":"2018-10-17T18:45:45Z","author_association":"MEMBER","body":"We would really prefer to use 2.7.1, not even 2.7 anymore."}}
{"actor":{"display_login":"rsasse"}}