{"action":"created","issue":{"url":"https://api.github.com/repos/wies/grasshopper/issues/31","repository_url":"https://api.github.com/repos/wies/grasshopper","labels_url":"https://api.github.com/repos/wies/grasshopper/issues/31/labels{/name}","comments_url":"https://api.github.com/repos/wies/grasshopper/issues/31/comments","events_url":"https://api.github.com/repos/wies/grasshopper/issues/31/events","html_url":"https://github.com/wies/grasshopper/issues/31","id":379458630,"node_id":"MDU6SXNzdWUzNzk0NTg2MzA=","number":31,"title":"Assume lemmas don't modify fields or global variables?","user":{"login":"siddharth-krishna","id":10712637,"node_id":"MDQ6VXNlcjEwNzEyNjM3","avatar_url":"https://avatars0.githubusercontent.com/u/10712637?v=4","gravatar_id":"","url":"https://api.github.com/users/siddharth-krishna","html_url":"https://github.com/siddharth-krishna","followers_url":"https://api.github.com/users/siddharth-krishna/followers","following_url":"https://api.github.com/users/siddharth-krishna/following{/other_user}","gists_url":"https://api.github.com/users/siddharth-krishna/gists{/gist_id}","starred_url":"https://api.github.com/users/siddharth-krishna/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/siddharth-krishna/subscriptions","organizations_url":"https://api.github.com/users/siddharth-krishna/orgs","repos_url":"https://api.github.com/users/siddharth-krishna/repos","events_url":"https://api.github.com/users/siddharth-krishna/events{/privacy}","received_events_url":"https://api.github.com/users/siddharth-krishna/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-11-10T20:27:24Z","updated_at":"2018-11-10T20:44:09Z","closed_at":null,"author_association":"COLLABORATOR","body":"Example:\r\n```\r\ntype K;\r\n\r\nstruct Node {\r\n  var next: Node;\r\n  var len: Int;\r\n  var keys: Array<K>;\r\n  var ptrs: Array<Node>;\r\n}\r\n\r\ndefine hrepSpatial(x) {\r\n  acc(x) &*& acc(x.keys) &*& acc(x.ptrs)\r\n}\r\n\r\ndatatype FlowDom = fd(ks: Map<K, Int>, ir: Map<K, Int>)\r\n\r\ndatatype Interface = int(fm: Map<Node, Map<Node, FlowDom>>)\r\n\r\nfunction fm_ind(x: Node) returns (fm: Map<Node, Map<Node, FlowDom>>)\r\n\r\npure predicate intValid(I: Interface)\r\n  \r\nlemma dummy(x: Node, I: Interface, k: K)\r\n  requires (forall y: Node :: I.fm[x][y].ks[k] == 0)\r\n  ensures intValid(I) == true\r\n  // Adding this means the assert goes through but the postcondition fails\r\n  //ensures B == old(B) && x.len == old(x.len)\r\n\r\nvar B: Int\r\n\r\nprocedure foo(x: Node, Ix: Interface, k: K)\r\n  requires hrepSpatial(x)\r\n  requires (forall y: Node :: Ix.fm[x][y].ks[k] == 0)\r\n  requires x.len == 2*B\r\n  ensures hrepSpatial(x)\r\n{\r\n  pure assert x.len == 2*B;\r\n  dummy(x, Ix, k);\r\n  pure assert x.len == 2*B;\r\n}\r\n```\r\n\r\nThe symbolic execution back-end can prove this, because `dummy` has no spatial footprint, so the value of `x.len` doesn't change. But the standard back-end can't prove the assertion after the call to `dummy`. Should we assume that procedures marked as lemmas don't change any state?\r\n\r\nBtw, a strange thing happens if I add the commented out postcondition of `dummy`: the assertion goes through but the postcondition of `foo` fails without any debug information.. is that because it's not clear what the footprint of `dummy` is?"},"comment":{"url":"https://api.github.com/repos/wies/grasshopper/issues/comments/437619917","html_url":"https://github.com/wies/grasshopper/issues/31#issuecomment-437619917","issue_url":"https://api.github.com/repos/wies/grasshopper/issues/31","id":437619917,"node_id":"MDEyOklzc3VlQ29tbWVudDQzNzYxOTkxNw==","user":{"login":"wies","id":3307936,"node_id":"MDQ6VXNlcjMzMDc5MzY=","avatar_url":"https://avatars1.githubusercontent.com/u/3307936?v=4","gravatar_id":"","url":"https://api.github.com/users/wies","html_url":"https://github.com/wies","followers_url":"https://api.github.com/users/wies/followers","following_url":"https://api.github.com/users/wies/following{/other_user}","gists_url":"https://api.github.com/users/wies/gists{/gist_id}","starred_url":"https://api.github.com/users/wies/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wies/subscriptions","organizations_url":"https://api.github.com/users/wies/orgs","repos_url":"https://api.github.com/users/wies/repos","events_url":"https://api.github.com/users/wies/events{/privacy}","received_events_url":"https://api.github.com/users/wies/received_events","type":"User","site_admin":false},"created_at":"2018-11-10T20:44:09Z","updated_at":"2018-11-10T20:44:09Z","author_association":"OWNER","body":"Yes, we should assume that lemmas don't change state (and enforce this using a simple type system in the front-end).\r\n\r\nI don't know what's going on in the post-condition. There seems to be no label in the counterexample either, which is strange."}}
{"actor":{"display_login":"wies"}}