{"action":"created","issue":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/248","repository_url":"https://api.github.com/repos/mit-plv/fiat-crypto","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/248/labels{/name}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/248/comments","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/248/events","html_url":"https://github.com/mit-plv/fiat-crypto/pull/248","id":263344807,"number":248,"title":"Curves from JSON","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","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},"labels":[{"id":401987310,"url":"https://api.github.com/repos/mit-plv/fiat-crypto/labels/awaiting-reviewer-feedback","name":"awaiting-reviewer-feedback","color":"fbca04","default":false},{"id":603966218,"url":"https://api.github.com/repos/mit-plv/fiat-crypto/labels/Coq%208.7","name":"Coq 8.7","color":"5319e7","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2017-10-06T06:10:03Z","updated_at":"2017-10-11T18:37:42Z","closed_at":null,"author_association":"OWNER","pull_request":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/248","html_url":"https://github.com/mit-plv/fiat-crypto/pull/248","diff_url":"https://github.com/mit-plv/fiat-crypto/pull/248.diff","patch_url":"https://github.com/mit-plv/fiat-crypto/pull/248.patch"},"body":"The X25519 curves are now generated from `.json` files.  This code only works in >= 8.7, because it makes use of the recently-merged-from-fiat `transparent_abstract` tactic to allow defining things in tactics without massive slowdown.  The structure is as follows:\r\n0. The module types and tactic definitions that set up the infrastructure live in `src/Specific/Framework/`\r\n1. There are `.json` files in `src/Specific/CurveParameters/` that specify curve characteristics.  These configuration files don't yet handle Montgomery/P256, nor Karatsuba.  @andres-erbsen @jadephilipoom do you have thoughts on unifying the synthesis in all these different cases?\r\n\r\nA simple example is `x2555_130.json`, which is:\r\n```json\r\n{\r\n    \"modulus\"          : \"2^255-5\",\r\n    \"base\"             : \"130\",\r\n    \"a24\"              : \"121665 (* XXX TODO(andreser) FIXME?  Is this right for this curve? *)\",\r\n    \"sz\"               : \"3\",\r\n    \"bitwidth\"         : \"128\",\r\n    \"carry_chain1\"     : \"default\",\r\n    \"carry_chain2\"     : [\"0\", \"1\"],\r\n    \"coef_div_modulus\" : \"2\",\r\n    \"operations\"       : [\"ladderstep\"]\r\n}\r\n```\r\nA more complicated example is `x25519_c64.json`:\r\n```json\r\n{\r\n    \"modulus\"          : \"2^255-19\",\r\n    \"base\"             : \"51\",\r\n    \"a24\"              : \"121665\",\r\n    \"sz\"               : \"5\",\r\n    \"bitwidth\"         : \"64\",\r\n    \"carry_chain1\"     : \"default\",\r\n    \"carry_chain2\"     : [\"0\", \"1\"],\r\n    \"coef_div_modulus\" : \"2\",\r\n    \"operations\"       : [\"femul\", \"fesquare\", \"freeze\", \"ladderstep\"],\r\n    \"extra_files\"      : [\"X25519_C64/scalarmult.c\"],\r\n    \"compiler\"         : \"gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes\",\r\n    \"mul_header\"       : \"(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)\",\r\n    \"mul_code\"\r\n    :\r\n    \"\r\n  uint128_t t[5];\r\n  limb r0,r1,r2,r3,r4,s0,s1,s2,s3,s4,c;\r\n\r\n  r0 = in[0];\r\n  r1 = in[1];\r\n  r2 = in[2];\r\n  r3 = in[3];\r\n  r4 = in[4];\r\n\r\n  s0 = in2[0];\r\n  s1 = in2[1];\r\n  s2 = in2[2];\r\n  s3 = in2[3];\r\n  s4 = in2[4];\r\n\r\n  t[0]  =  ((uint128_t) r0) * s0;\r\n  t[1]  =  ((uint128_t) r0) * s1 + ((uint128_t) r1) * s0;\r\n  t[2]  =  ((uint128_t) r0) * s2 + ((uint128_t) r2) * s0 + ((uint128_t) r1) * s1;\r\n  t[3]  =  ((uint128_t) r0) * s3 + ((uint128_t) r3) * s0 + ((uint128_t) r1) * s2 + ((uint128_t) r2) * s1;\r\n  t[4]  =  ((uint128_t) r0) * s4 + ((uint128_t) r4) * s0 + ((uint128_t) r3) * s1 + ((uint128_t) r1) * s3 + ((uint128_t) r2) * s2;\r\n\r\n  r4 *= 19;\r\n  r1 *= 19;\r\n  r2 *= 19;\r\n  r3 *= 19;\r\n\r\n  t[0] += ((uint128_t) r4) * s1 + ((uint128_t) r1) * s4 + ((uint128_t) r2) * s3 + ((uint128_t) r3) * s2;\r\n  t[1] += ((uint128_t) r4) * s2 + ((uint128_t) r2) * s4 + ((uint128_t) r3) * s3;\r\n  t[2] += ((uint128_t) r4) * s3 + ((uint128_t) r3) * s4;\r\n  t[3] += ((uint128_t) r4) * s4;\r\n\",\r\n    \"square_header\"    : \"(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)\",\r\n    \"square_code\"\r\n    :\r\n    \"\r\n  uint128_t t[5];\r\n  limb r0,r1,r2,r3,r4,c;\r\n  limb d0,d1,d2,d4,d419;\r\n\r\n  r0 = in[0];\r\n  r1 = in[1];\r\n  r2 = in[2];\r\n  r3 = in[3];\r\n  r4 = in[4];\r\n\r\n  do {\r\n    d0 = r0 * 2;\r\n    d1 = r1 * 2;\r\n    d2 = r2 * 2 * 19;\r\n    d419 = r4 * 19;\r\n    d4 = d419 * 2;\r\n\r\n    t[0] = ((uint128_t) r0) * r0 + ((uint128_t) d4) * r1 + (((uint128_t) d2) * (r3     ));\r\n    t[1] = ((uint128_t) d0) * r1 + ((uint128_t) d4) * r2 + (((uint128_t) r3) * (r3 * 19));\r\n    t[2] = ((uint128_t) d0) * r2 + ((uint128_t) r1) * r1 + (((uint128_t) d4) * (r3     ));\r\n    t[3] = ((uint128_t) d0) * r3 + ((uint128_t) d1) * r2 + (((uint128_t) r4) * (d419   ));\r\n    t[4] = ((uint128_t) d0) * r4 + ((uint128_t) d1) * r3 + (((uint128_t) r2) * (r2     ));\r\n\"\r\n}\r\n```\r\n3. The `src/Specific/CurveParameters/remake_curves.sh` script holds a list of curves to be made, what directories they should end up living in, and it invokes `src/Specific/Framework/make_curve.py` to transform these files into outputs.  The Python script fills in a few defaults (such as computing `s` and `c` from the modulus, if you don't pass them explicitly), and does a lot of processing on the C code that is pasted verbatim from donna to get it to be in the right format for Coq.\r\n\r\nThis Python script creates the files:\r\n- `CurveParameters.v` (the Coq-ified version of the json file, which instantiates an appropriate module type);\r\n- `Synthesis.v`, which instantiates a `MakeSynthesisTactics` with the curve parameter modules, invokes a tactic from the applied module functor to synthesize all of the relevant non-reflective bits (basically, what used to live in @jadephilipoom 's `ArithmeticSynthesisTest.v`), and then instantiates another module functor `PackageSynthesis` which defines notations via tactics in terms to access the names of the various fields defined by the synthesis tactic; \r\n- any other files you ask it for, such as `compiler.sh`, `femul.v`, `femulDisplay.v`.  All of the `*Display.v` files are simple, and all the the operation synthesis files have a single `Definition` (with the appropriate type), and solve the definition by invoking a single tactic defined in `PackageSynthesis`, e.g., `synthesize_mul` or `synthesize_ladderstep`."},"comment":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments/335906969","html_url":"https://github.com/mit-plv/fiat-crypto/pull/248#issuecomment-335906969","issue_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/248","id":335906969,"user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","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":"2017-10-11T18:37:42Z","updated_at":"2017-10-11T18:37:42Z","author_association":"OWNER","body":"> I also don't understand what the glue does\r\n\r\nThe (pre)glue code does three things: (1) reassociate sigmas, arrows, products, etc; (2) `rewrite <- sig_from_previous_layer_of_synthesis by make_use_of_preconditions_tac ()`; (3) `change <some computed expression based on reflection primitives and with [dlet] in the right places`.\r\n\r\n> but just wrapping additional layers around it instead of detangling some sounds miserable.\r\n\r\nAgreed.  I'm going to try to do some detangling on top of #250."}}
{"actor":{"display_login":"JasonGross"}}