{"action":"created","issue":{"url":"https://api.github.com/repos/openssl/openssl/issues/2148","repository_url":"https://api.github.com/repos/openssl/openssl","labels_url":"https://api.github.com/repos/openssl/openssl/issues/2148/labels{/name}","comments_url":"https://api.github.com/repos/openssl/openssl/issues/2148/comments","events_url":"https://api.github.com/repos/openssl/openssl/issues/2148/events","html_url":"https://github.com/openssl/openssl/pull/2148","id":197578977,"number":2148,"title":"Add SAW AES proof.","user":{"login":"benlaurie","id":40044,"avatar_url":"https://avatars.githubusercontent.com/u/40044?v=3","gravatar_id":"","url":"https://api.github.com/users/benlaurie","html_url":"https://github.com/benlaurie","followers_url":"https://api.github.com/users/benlaurie/followers","following_url":"https://api.github.com/users/benlaurie/following{/other_user}","gists_url":"https://api.github.com/users/benlaurie/gists{/gist_id}","starred_url":"https://api.github.com/users/benlaurie/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/benlaurie/subscriptions","organizations_url":"https://api.github.com/users/benlaurie/orgs","repos_url":"https://api.github.com/users/benlaurie/repos","events_url":"https://api.github.com/users/benlaurie/events{/privacy}","received_events_url":"https://api.github.com/users/benlaurie/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2016-12-26T11:40:25Z","updated_at":"2016-12-27T14:56:29Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/openssl/openssl/pulls/2148","html_url":"https://github.com/openssl/openssl/pull/2148","diff_url":"https://github.com/openssl/openssl/pull/2148.diff","patch_url":"https://github.com/openssl/openssl/pull/2148.patch"},"body":"Use Galois' SAW tool to prove correctness of OpenSSL's AES implementation."},"comment":{"url":"https://api.github.com/repos/openssl/openssl/issues/comments/269336279","html_url":"https://github.com/openssl/openssl/pull/2148#issuecomment-269336279","issue_url":"https://api.github.com/repos/openssl/openssl/issues/2148","id":269336279,"user":{"login":"dot-asm","id":9038069,"avatar_url":"https://avatars.githubusercontent.com/u/9038069?v=3","gravatar_id":"","url":"https://api.github.com/users/dot-asm","html_url":"https://github.com/dot-asm","followers_url":"https://api.github.com/users/dot-asm/followers","following_url":"https://api.github.com/users/dot-asm/following{/other_user}","gists_url":"https://api.github.com/users/dot-asm/gists{/gist_id}","starred_url":"https://api.github.com/users/dot-asm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dot-asm/subscriptions","organizations_url":"https://api.github.com/users/dot-asm/orgs","repos_url":"https://api.github.com/users/dot-asm/repos","events_url":"https://api.github.com/users/dot-asm/events{/privacy}","received_events_url":"https://api.github.com/users/dot-asm/received_events","type":"User","site_admin":false},"created_at":"2016-12-27T14:56:29Z","updated_at":"2016-12-27T14:56:29Z","body":"> this could be made into a config target of its own\r\n\r\nI'd actually ask why dedicated target or option at all? The input that is used here is llvm byte-code for aes_core.c alone. Does one actually have to compile whole thing to take just single file? Isn't it sufficient to generate byte-code for that one source file? I mean it *is* sufficient, so why not do just that?\r\n\r\nIn case one argues that there is value in corresponding build passing 'make test'. I'd argue not really. What is exercised by 'saw' is llvm pseudo-code, while what is exercised by 'make test' (if it works, see previous comment) is actual machine code. One can only draw conclusion about correctness of input C code, but in such case what difference does it make how machine code was generated, with llvm pseudo-code in the middle or without?"}}
{"actor":{"display_login":"dot-asm"}}