{"query-id":"1","query":"push","args":{"kind":"full","code":"module RSA\nopen FStar.Mul\n","line":1,"column":0}}
{"query-id":"2","query":"push","args":{"kind":"full","code":"\n(*! 1. write a function that computes [g^e] naively *)\n\nval pow: g:nat -> e:nat -> nat\n","line":3,"column":0}}
{"query-id":"3","query":"push","args":{"kind":"full","code":"\n// Solution:\nlet rec pow g e =\n  if e = 0\n  then 1\n  else g * pow g (e-1)\n","line":7,"column":0}}
{"query-id":"4","query":"push","args":{"kind":"full","code":"\n// Test: evaluate pow 2 16\n\n// A convenient notation [but it breaks proofs?]\n// unfold let (^) = pow\n\n\n(*! 2. prove [g^(e1 + e2) = g^e1 * g^e2] *)\n\nval lemma_pow_add (g: nat) (e1 e2: nat): Lemma (pow g (e1 + e2) = pow g e1 * pow g e2)\n","line":13,"column":0}}
{"query-id":"5","query":"push","args":{"kind":"full","code":"\n#set-options \"--initial_fuel 1 --initial_ifuel 1\"\nlet rec lemma_pow_add g e1 e2 =\n  if e2 = 0 then ()\n  else lemma_pow_add g e1 (e2 - 1)\n","line":23,"column":0}}
{"query-id":"6","query":"push","args":{"kind":"full","code":"\n#set-options \"--initial_fuel 1 --initial_ifuel 1\"\nlet rec lemma_pow_add g e1 e2 =\n  if e2 = 0 then ()\n  else lemma_pow_add g e1 (e2 - 1)\n","line":23,"column":0}}
{"query-id":"7","query":"push","args":{"kind":"full","code":"\n(*! 3. prove [(g^e1)^ e2 = g^(e1 * e2)] *)\n\nval lemma_pow_mul (g:nat) (e1 e2:nat): Lemma (pow (pow g e1) e2 = pow g (e1 * e2))\n","line":28,"column":0}}
{"query-id":"8","query":"push","args":{"kind":"full","code":"\nlet rec lemma_pow_mul g e1 e2 =\n  if e2 = 0 then ()\n  else\n    let e2': nat = e2 - 1 in\n    lemma_pow_mul g e1 e2';\n    lemma_pow_add g e1 (e1 * e2')\n","line":32,"column":0}}
{"query-id":"9","query":"push","args":{"kind":"full","code":"\n\n(*! 4. Implement exponentiation by squaring using\n       [ g^e = g^(e/2)^2]       when [g % 2 = 0]\n       [ g^e = g*(x^(e-1)/2)^2] when [g % 2 = 1 ] *)\n\nval fast_pow: nat -> nat -> nat\n","line":39,"column":0}}
{"query-id":"10","query":"push","args":{"kind":"full","code":"\nlet rec fast_pow g e =\n  match e with\n  | 0 -> 1\n  | _ ->\n    let g' = pow g (e/2) in\n    g' * g' * (if e % 2 = 0 then 1 else g)\n","line":46,"column":0}}
{"query-id":"11","query":"push","args":{"kind":"full","code":"\n(*! 5. Prove that exponentiation by squaring is correct *)\n\nval lemma_fast_pow (g:nat) (e:nat): Lemma (fast_pow g e = pow g e)\n","line":53,"column":0}}
{"query-id":"12","query":"push","args":{"kind":"full","code":"\n// You will need the lemmas from exercises 2 and 3\n// Hint: think how to relate e to e/2 and e%2\n\nlet lemma_fast_pow g e =\n  if e = 0 then () else\n    let e' = e/2 in\n    let b = e%2 in\n//  assert(e = 2 * e' + b);\n    lemma_pow_add g (2 * e') b;\n//  assert(pow g e = pow g (2 * e') * pow g b);\n    let r = if b = 0 then 1 else g in\n//  assert(r = pow g b);\n//    let g' = pow g e' in\n//  assert(fast_pow g e = g' * g' * r);\n    lemma_pow_mul g e' 2\n//  assert(pow g e = pow g' 2 * r);\n//  assert_norm(pow g' 2 = g' * g')\n","line":57,"column":0}}
{"query-id":"13","query":"pop","args":{"dummy":null}}
{"query-id":"14","query":"push","args":{"kind":"full","code":"\n// You will need the lemmas from exercises 2 and 3\n// Hint: think how to relate e to e/2 and e%2\n\nlet lemma_fast_pow g e =\n  if e = 0 then () else\n    let e' = e/2 in\n    let b = e%2 in\n//  assert(e = 2 * e' + b);\n    lemma_pow_add g (2 * e') b;\n//  assert(pow g e = pow g (2 * e') * pow g b);\n    let r = if b = 0 then 1 else g in\n//  assert(r = pow g b);\n//    let g' = pow g e' in\n//  assert(fast_pow g e = g' * g' * r);\n    lemma_pow_mul g e' 2\n//  assert(pow g e = pow g' 2 * r);\n//  assert_norm(pow g' 2 = g' * g')\n","line":57,"column":0}}
{"query-id":"15","query":"pop","args":{"dummy":null}}
{"query-id":"16","query":"push","args":{"kind":"full","code":"\n// You will need the lemmas from exercises 2 and 3\n// Hint: think how to relate e to e/2 and e%2\n\nlet lemma_fast_pow g e =\n  if e = 0 then () else\n    let e' = e/2 in\n    let b = e%2 in\n//  assert(e = 2 * e' + b);\n    lemma_pow_add g (2 * e') b;\n//  assert(pow g e = pow g (2 * e') * pow g b);\n    let r = if b = 0 then 1 else g in\n//  assert(r = pow g b);\n//    let g' = pow g e' in\n//  assert(fast_pow g e = g' * g' * r);\n    lemma_pow_mul g e' 2\n//  assert(pow g e = pow g' 2 * r);\n//  assert_norm(pow g' 2 = g' * g')\n","line":57,"column":0}}
{"query-id":"17","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":75,"column":0}}}
{"query-id":"18","query":"lookup","args":{"context":"code","symbol":"pow","requested-info":["type","documentation"],"location":{"filename":"<input>","line":73,"column":22}}}
{"query-id":"19","query":"lookup","args":{"context":"code","symbol":"pow","requested-info":["type","documentation"],"location":{"filename":"<input>","line":73,"column":22}}}