{"action":"created","issue":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/64","repository_url":"https://api.github.com/repos/mit-plv/fiat-crypto","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/64/labels{/name}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/64/comments","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/64/events","html_url":"https://github.com/mit-plv/fiat-crypto/issues/64","id":177659658,"number":64,"title":"How to push representation changes through `Let_In`?","user":{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars.githubusercontent.com/u/918403?v=3","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2016-09-18T15:55:33Z","updated_at":"2016-09-22T00:15:18Z","closed_at":null,"body":"@JasonGross @achlipala: I am failing to derive a version of `EdDSA.sign` where types of `Let`-bound variables are changed to an efficient representation.\r\n\r\nThere seem to be three issues\r\n\r\n- The definition of `sign` is not parametrized over `nat`, so I cannot do representation changes by plugging in both spec and optimized parameters and proving relatedness as we ended up doing for the field and elliptic curve levels.\r\n- unification fails on pattern fragment modulo beta (https://github.com/mit-plv/fiat-crypto/commit/cfdc4236c19db609a67d816b15cc1480a106974a#diff-5366caedd04016399124d528353b4a5cR258, of course I tried to do this using `rewrite` first). In particular I cannot `rewrite<-` with `Let_In (f e) C = Let_In e (fun v => C (f v))`.\r\n- the return type of `sign` is determined by `combine : forall a, word a -> forall b, word b -> word (a+b)`, which prevents most tactics from filling in the return type automatically; specifying it manually works but makes tactic code quite verbose.\r\n\r\nUnless something comes up from this thread that bypasses all three issues, I will give up on synthesizing the representation change part  of optimizing signing, and write and verify the fast version manually."},"comment":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments/248779511","html_url":"https://github.com/mit-plv/fiat-crypto/issues/64#issuecomment-248779511","issue_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/64","id":248779511,"user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"created_at":"2016-09-22T00:15:18Z","updated_at":"2016-09-22T00:15:18Z","body":"1. How do you plan to express the optimized version, if you need something other than `nat`, and `word` is dependent on `nat`?\r\n2. Let me try to clarify it a bit: the idea is that you need to make sure that Coq never has to solve a problem of the form `?P (f n) == expression`, and only problems of the form `?P n == expression` for `n` a variable.  We want to transform `Let_In v (fun n => P (f n))` into `Let_In (f v) P`.  We need to \"hide\" the `f` from Coq, so we build a package that contains both `v` and `f v`.  Then we can bind this package in the `Let_In`, as `Let_In package (fun pkg => P (f (project_v pkg)))`.  Now we can replace `f (project_v pkg)` with `project_fv pkg`.  Finally, we need to do clean-up; we actually want to bind `f v`, not the package, and we want to unfold the projection."}}
{"actor":{"display_login":"JasonGross"}}