{"action":"created","issue":{"url":"https://api.github.com/repos/Microsoft/dafny/issues/63","repository_url":"https://api.github.com/repos/Microsoft/dafny","labels_url":"https://api.github.com/repos/Microsoft/dafny/issues/63/labels{/name}","comments_url":"https://api.github.com/repos/Microsoft/dafny/issues/63/comments","events_url":"https://api.github.com/repos/Microsoft/dafny/issues/63/events","html_url":"https://github.com/Microsoft/dafny/issues/63","id":192194679,"number":63,"title":"reveal inside a function body \"leaks out\", requiring its callers to use the same reveal","user":{"login":"0xabu","id":13037682,"avatar_url":"https://avatars.githubusercontent.com/u/13037682?v=3","gravatar_id":"","url":"https://api.github.com/users/0xabu","html_url":"https://github.com/0xabu","followers_url":"https://api.github.com/users/0xabu/followers","following_url":"https://api.github.com/users/0xabu/following{/other_user}","gists_url":"https://api.github.com/users/0xabu/gists{/gist_id}","starred_url":"https://api.github.com/users/0xabu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/0xabu/subscriptions","organizations_url":"https://api.github.com/users/0xabu/orgs","repos_url":"https://api.github.com/users/0xabu/repos","events_url":"https://api.github.com/users/0xabu/events{/privacy}","received_events_url":"https://api.github.com/users/0xabu/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"qunyanm","id":15744202,"avatar_url":"https://avatars.githubusercontent.com/u/15744202?v=3","gravatar_id":"","url":"https://api.github.com/users/qunyanm","html_url":"https://github.com/qunyanm","followers_url":"https://api.github.com/users/qunyanm/followers","following_url":"https://api.github.com/users/qunyanm/following{/other_user}","gists_url":"https://api.github.com/users/qunyanm/gists{/gist_id}","starred_url":"https://api.github.com/users/qunyanm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/qunyanm/subscriptions","organizations_url":"https://api.github.com/users/qunyanm/orgs","repos_url":"https://api.github.com/users/qunyanm/repos","events_url":"https://api.github.com/users/qunyanm/events{/privacy}","received_events_url":"https://api.github.com/users/qunyanm/received_events","type":"User","site_admin":false},"assignees":[{"login":"qunyanm","id":15744202,"avatar_url":"https://avatars.githubusercontent.com/u/15744202?v=3","gravatar_id":"","url":"https://api.github.com/users/qunyanm","html_url":"https://github.com/qunyanm","followers_url":"https://api.github.com/users/qunyanm/followers","following_url":"https://api.github.com/users/qunyanm/following{/other_user}","gists_url":"https://api.github.com/users/qunyanm/gists{/gist_id}","starred_url":"https://api.github.com/users/qunyanm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/qunyanm/subscriptions","organizations_url":"https://api.github.com/users/qunyanm/orgs","repos_url":"https://api.github.com/users/qunyanm/repos","events_url":"https://api.github.com/users/qunyanm/events{/privacy}","received_events_url":"https://api.github.com/users/qunyanm/received_events","type":"User","site_admin":false}],"milestone":null,"comments":1,"created_at":"2016-11-29T05:57:11Z","updated_at":"2016-12-02T18:11:40Z","closed_at":null,"body":"The following Dafny fails to verify, unless the reveal line at the end of the lemma is uncommented:\r\n```\r\ntype globalsmap = map<string, seq<int>>\r\n\r\npredicate {:axiom} ValidGlobal(g:string)\r\n\r\npredicate {:opaque} ValidGlobalStateOpaque(globals: globalsmap)\r\n{\r\n    forall g :: ValidGlobal(g) <==> g in globals && |globals[g]| == 1\r\n}\r\n\r\nfunction GlobalWord(gm:globalsmap, g:string): int\r\n    requires ValidGlobalStateOpaque(gm) && ValidGlobal(g)\r\n{\r\n    reveal_ValidGlobalStateOpaque();\r\n    gm[g][0]\r\n}\r\n\r\nfunction GlobalUpdate(gm: globalsmap, g:string, v:int): globalsmap\r\n    requires ValidGlobalStateOpaque(gm) && ValidGlobal(g)\r\n    ensures ValidGlobalStateOpaque(GlobalUpdate(gm, g, v))\r\n{\r\n    reveal_ValidGlobalStateOpaque();\r\n    gm[g := gm[g][0 := v]]\r\n}\r\n\r\nlemma test()\r\n{\r\n    ghost var gm1:globalsmap;\r\n    ghost var g: string;\r\n    ghost var v: int;\r\n    assume ValidGlobal(g) && ValidGlobalStateOpaque(gm1);\r\n    ghost var gm2 := GlobalUpdate(gm1, g, v);\r\n    //reveal_ValidGlobalStateOpaque();\r\n    assert GlobalWord(gm2, g) == v;\r\n}\r\n```\r\n\r\nUnless @parno and I are mistaken, GlobalUpdate and GlobalWord need the reveal for wellformedness, but the caller lemma shouldn't care because it can see the body of each function, yet it fails to see the effect of the update without the reveal. This appears to be an interaction between the opaque, map and seq, since I found that replacing the seq with a single element makes it go away. It may also be related to #56, although there's only one opaque here."},"comment":{"url":"https://api.github.com/repos/Microsoft/dafny/issues/comments/264522008","html_url":"https://github.com/Microsoft/dafny/issues/63#issuecomment-264522008","issue_url":"https://api.github.com/repos/Microsoft/dafny/issues/63","id":264522008,"user":{"login":"qunyanm","id":15744202,"avatar_url":"https://avatars.githubusercontent.com/u/15744202?v=3","gravatar_id":"","url":"https://api.github.com/users/qunyanm","html_url":"https://github.com/qunyanm","followers_url":"https://api.github.com/users/qunyanm/followers","following_url":"https://api.github.com/users/qunyanm/following{/other_user}","gists_url":"https://api.github.com/users/qunyanm/gists{/gist_id}","starred_url":"https://api.github.com/users/qunyanm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/qunyanm/subscriptions","organizations_url":"https://api.github.com/users/qunyanm/orgs","repos_url":"https://api.github.com/users/qunyanm/repos","events_url":"https://api.github.com/users/qunyanm/events{/privacy}","received_events_url":"https://api.github.com/users/qunyanm/received_events","type":"User","site_admin":false},"created_at":"2016-12-02T18:11:40Z","updated_at":"2016-12-02T18:11:40Z","body":"I think the problem is that the assume statement in test() and the subsequent requires from the call to GlobalUpdate() and GlobalWord() don't have enough fuel to trigger the function definition axiom of ValidGlobalStateOpaque, Therefore, in the call to GlobalWord(gm2,g), it is not guaranteed that gm2[g][0] is valid. I am guessing we failed the index [0], if replacing the seq with a single element works(though the error message didn't say index out of bound). It does seem counter-intuitive to require reveal in test() when it can see the body of GlobalUpdate() and GlobalWord(), but I am not sure how to fix it."}}
{"actor":{"display_login":"qunyanm"}}