{"action":"created","issue":{"url":"https://api.github.com/repos/GaloisInc/saw-script/issues/87","repository_url":"https://api.github.com/repos/GaloisInc/saw-script","labels_url":"https://api.github.com/repos/GaloisInc/saw-script/issues/87/labels{/name}","comments_url":"https://api.github.com/repos/GaloisInc/saw-script/issues/87/comments","events_url":"https://api.github.com/repos/GaloisInc/saw-script/issues/87/events","html_url":"https://github.com/GaloisInc/saw-script/issues/87","id":126306375,"number":87,"title":"Signed bitvector primitives in specifications","user":{"login":"brianhuffman","id":619882,"avatar_url":"https://avatars2.githubusercontent.com/u/619882?v=4","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":[{"id":200578657,"url":"https://api.github.com/repos/GaloisInc/saw-script/labels/enhancement","name":"enhancement","color":"84b6eb","default":true}],"state":"open","locked":false,"assignee":{"login":"brianhuffman","id":619882,"avatar_url":"https://avatars2.githubusercontent.com/u/619882?v=4","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},"assignees":[{"login":"brianhuffman","id":619882,"avatar_url":"https://avatars2.githubusercontent.com/u/619882?v=4","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}],"milestone":null,"comments":6,"created_at":"2016-01-12T23:53:15Z","updated_at":"2018-02-21T22:18:42Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"The following SAWCore primitives (mostly to do with signed bitvectors) appear in terms extracted from Java or LLVM, but are not expressible in Cryptol:\n\n```\nPrelude.bvUpd\nPrelude.bvSDiv\nPrelude.bvSRem\nPrelude.bvSShr\nPrelude.bvsgt\nPrelude.bvsge\nPrelude.bvslt\nPrelude.bvsle\nPrelude.bvTrunc\nPrelude.bvUExt\nPrelude.bvSExt\n```\n\nIt would be very useful to be able to state theorems (especially rewrite rules) involving these operations, so we should provide some way for users to be able to express them. A possibility would be to provide a saw-script primitive of type `Term` for each; these could then be used within the `{{` `}}` cryptol brackets.\n"},"comment":{"url":"https://api.github.com/repos/GaloisInc/saw-script/issues/comments/367495152","html_url":"https://github.com/GaloisInc/saw-script/issues/87#issuecomment-367495152","issue_url":"https://api.github.com/repos/GaloisInc/saw-script/issues/87","id":367495152,"user":{"login":"brianhuffman","id":619882,"avatar_url":"https://avatars2.githubusercontent.com/u/619882?v=4","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":"2018-02-21T22:18:42Z","updated_at":"2018-02-21T22:18:42Z","author_association":"CONTRIBUTOR","body":"I should probably remove everything from `cryptol_prims` that is a cryptol primitive now. And I need to make sure that `cryptol_prims` includes all the operators I listed above that still *aren't* cryptol primitives."}}
{"actor":{"display_login":"brianhuffman"}}