{"action":"created","comment":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments/176899879","pull_request_review_id":106689459,"id":176899879,"diff_hunk":"@@ -0,0 +1,873 @@\n+Require Import Coq.Bool.Bool.\n+Require Import Coq.micromega.Lia.\n+Require Import Coq.ZArith.ZArith.\n+Require Import Coq.ZArith.Znumtheory.\n+Require Import Crypto.Experiments.Loops.\n+Require Import Crypto.Util.Tactics.DestructHead.\n+Require Import Crypto.Util.ZUtil.\n+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.\n+\n+Local Open Scope Z_scope.\n+\n+Module BinaryExtendedGCD.\n+  Section BinaryExtendedGCD.\n+    (** This section implements a constant-time version of the binary extended\n+        GCD algorithm, for computing modular inverses. It is the fully general\n+        version, supporting even moduli. In most cases, more specific algorithms\n+        should be used. For instance, inverting by a prime is simpler to do with\n+        Fermat's Little Theorem. However, RSA key generation requires the most\n+        general version.\n+\n+        This algorithm is adapted from the Handbook of Applied Cryptography,\n+        section 14.4.3, algorithm 14.61. It was modified slightly to better\n+        bound coefficients, then recast into constant-time selects:\n+\n+        1. Negate [B] and [C] so they are positive. The invariant now involves a\n+           subtraction.\n+\n+        2. If step 2 (both [x] and [y] are even) runs, abort immediately. This\n+           algorithm only cares about [x] and [y] relatively prime.\n+\n+        3. Subtract copies of [x] and [y] as needed in step 6 (both [u] and [v]\n+           are odd) so coefficients stay in bounds.\n+\n+        4. Replace the [u >= v] check with [u > v]. This changes the end\n+           condition to [v = 0] rather than [u = 0]. This saves an extra\n+           subtraction due to which coefficients were negated.\n+\n+        5. Rename x and y to a and n, to capture that one is a modulus.\n+\n+        6. Rearrange steps 4 through 6 slightly. Merge the loops in steps 4 and\n+           5 into the main loop (step 7's goto), and move step 6 to the start of\n+           the loop iteration, ensuring each loop iteration halves at least one\n+           value.\n+\n+        Note this algorithm does not handle either input being zero. *)\n+\n+    (** This is a constant-time algorithm, so first define fixed-width words to\n+        compute over. In particular, we want to capture the non-trivial bounds on\n+        the intermediate values. A [word] is an integer with specified bit\n+        width. The actual implementation will represent this with an array of\n+        smaller machine words. *)\n+    Inductive word (bits : Z) :=\n+    | Word : Z -> word bits.\n+\n+    Definition wrap (bits val : Z) : Z := val mod 2^bits.\n+\n+    Definition to_Z {bits : Z} (a : word bits) : Z :=\n+      match a with Word v => v end.\n+    Definition to_word {bits : Z} (val : Z) :=\n+      Word bits (wrap bits val).\n+\n+    (** Our algorithm is implemented over the following constant-time\n+        primitives. [add] and [sub] return a carry and borrow bit,\n+        respectively. *)\n+    Definition add {bits : Z} (a b : word bits) : bool * word bits :=\n+      let a' := to_Z a in\n+      let b' := to_Z b in\n+      (2^bits <=? a' + b', to_word (a' + b')).\n+    Definition sub {bits : Z} (a b : word bits) : bool * word bits :=\n+      let a' := to_Z a in\n+      let b' := to_Z b in\n+      (a' <? b', to_word (a' - b')).\n+    Definition rshift1 {bits : Z} (a : word bits) : word bits :=\n+      to_word ((to_Z a) / 2).\n+    Definition select {bits : Z} (t : bool) (a b : word bits) : word bits :=\n+      if t then a else b.\n+    Definition odd {bits : Z} (a : word bits) : bool := Z.odd (to_Z a).\n+    Definition is_one {bits: Z} (a : word bits) : bool := to_Z a =? 1.\n+\n+\n+    (** These helpers are implemented with temporaries. They return the final\n+        values of the temporaries, to model clobbering them in imperative\n+        code. *)\n+    Definition maybe_rshift1_carry {bits : Z}\n+               (t carry : bool) (a : word bits) : word bits * word bits :=\n+      let tmp := rshift1 a in\n+      let a := select t tmp a in\n+      let a := if t && carry then to_word ((to_Z a)  + 2^(bits - 1))\n+               else a in\n+      (a, tmp).\n+\n+    Definition maybe_rshift1 {bits : Z} (t : bool) :=\n+      @maybe_rshift1_carry bits t false.\n+\n+    Definition maybe_add {bits : Z}\n+               (t : bool) (a b : word bits) : bool * word bits * word bits :=\n+      let (carry, tmp) := add a b in\n+      let a := select t tmp a in\n+      (carry && t, a, tmp).\n+\n+    (** We ultimately wish to compute [a] inverse mod [n]. Parameterize over\n+        both values' public widths. ([a]'s width may be smaller than [n]'s if it\n+        publicly-bounded. For instance, RSA key generation involves a public\n+        small [a], typically 65537, and a large secret modulus, the totient. *)\n+    Context {abits nbits : Z}.\n+    Context {abits_positive : 0 < abits}.\n+    Context {nbits_positive : 0 < nbits}.\n+\n+    (** This is our loop state. *)\n+    Definition state : Set :=\n+      word abits * word nbits * (* a, n *)\n+      word nbits * word abits * word nbits * word abits * (* A, B, C, D *)\n+      word nbits * word nbits (* u, v *).\n+\n+    Definition step (s : state) : state :=\n+      let '(a, n, A, B, C, D, u, v) := s in\n+      (* If both |u| and |v| are odd, subtract the smaller from the larger. *)\n+      let both_odd := odd u && odd v in\n+      let (v_less_than_u, tmp) := sub v u in\n+      let v := select (both_odd && negb v_less_than_u) tmp v in\n+      let (_, tmp) := sub u v in\n+      let u := select (both_odd && v_less_than_u) tmp u in\n+\n+      (* If we updated one of the values, update the corresponding\n+         coefficient. *)\n+      let (carry, tmp) := add A C in\n+      let (borrow, tmp2) := sub tmp n in\n+      let borrow := borrow && negb carry in\n+      let tmp := select borrow tmp tmp2 in\n+      let A := select (both_odd && v_less_than_u) tmp A in\n+      let C := select (both_odd && negb v_less_than_u) tmp C in\n+\n+      let (_, tmp) := add B D in\n+      let (_, tmp2) := sub tmp a in\n+      let tmp := select borrow tmp tmp2 in\n+      let B := select (both_odd && v_less_than_u) tmp B in\n+      let D := select (both_odd && negb v_less_than_u) tmp D in\n+\n+      (* Our loop invariants hold at this point. Additionally, exactly one of\n+         [u] and [v] is now even. *)\n+      let u_even := negb (odd u) in\n+      let v_even := negb (odd v) in\n+\n+      (* Halve the even one and adjust the corresponding coefficient. *)\n+      let (u, tmp) := maybe_rshift1 u_even u in\n+      let A_or_B_odd := odd A || odd B in\n+      let '(A_carry, A, tmp) := maybe_add (A_or_B_odd && u_even) A n in\n+      let '(B_carry, B, tmp) := maybe_add (A_or_B_odd && u_even) B a in\n+      let (A, tmp) := maybe_rshift1_carry u_even A_carry A in\n+      let (B, tmp) := maybe_rshift1_carry u_even B_carry B in\n+\n+      let (v, tmp) := maybe_rshift1 v_even v in\n+      let C_or_D_odd := odd C || odd D in\n+      let '(C_carry, C, tmp) := maybe_add (C_or_D_odd && v_even) C n in\n+      let '(D_carry, D, tmp) := maybe_add (C_or_D_odd && v_even) D a in\n+      let (C, tmp) := maybe_rshift1_carry v_even C_carry C in\n+      let (D, tmp) := maybe_rshift1_carry v_even D_carry D in\n+      (a, n, A, B, C, D, u, v).\n+\n+    Definition mod_inverse_consttime\n+               (a : word abits) (n : word nbits) : option (word nbits) :=\n+      if negb (odd a) && negb (odd n)\n+      then None\n+      else\n+        let u := to_word (to_Z a) in\n+        let v := n in\n+        let A := to_word 1 in\n+        let B := to_word 0 in\n+        let C := to_word 0 in\n+        let D := to_word 1 in\n+        let i := 0 in\n+        let '(a, n, A, B, C, D, u, v, _) :=\n+            (while (fun '(_, i) => i <? abits + nbits)\n+                   (fun '(s, i) => (step s, i + 1))\n+                   (Z.to_nat (abits + nbits))\n+                   (a, n, A, B, C, D, u, v, i)) in\n+        if is_one u\n+        then Some A\n+        else None.\n+\n+\n+    (** Proofs *)\n+\n+    (** To simplify analysis, we split each loop in the middle, where the loop\n+        invariant also holds. *)\n+\n+    Definition odd_step (s : state) : state :=\n+      let '(a, n, A, B, C, D, u, v) := s in\n+\n+      (* If both |u| and |v| are odd, subtract the smaller from the larger. *)\n+      let both_odd := odd u && odd v in\n+      let (v_less_than_u, tmp) := sub v u in\n+      let v := select (both_odd && negb v_less_than_u) tmp v in\n+      let (_, tmp) := sub u v in\n+      let u := select (both_odd && v_less_than_u) tmp u in\n+\n+      (* If we updated one of the values, update the corresponding\n+         coefficient. *)\n+      let (carry, tmp) := add A C in\n+      let (borrow, tmp2) := sub tmp n in\n+      let borrow := borrow && negb carry in\n+      let tmp := select borrow tmp tmp2 in\n+      let A := select (both_odd && v_less_than_u) tmp A in\n+      let C := select (both_odd && negb v_less_than_u) tmp C in\n+\n+      let (_, tmp) := add B D in\n+      let (_, tmp2) := sub tmp a in\n+      let tmp := select borrow tmp tmp2 in\n+      let B := select (both_odd && v_less_than_u) tmp B in\n+      let D := select (both_odd && negb v_less_than_u) tmp D in\n+      (a, n, A, B, C, D, u, v).\n+\n+    Definition even_step (s : state) : state :=\n+      let '(a, n, A, B, C, D, u, v) := s in\n+\n+      (* This step should be called after [odd_step], which ensures at least one\n+         of [u] and [v] are even. *)\n+      let u_even := negb (odd u) in\n+      let v_even := negb (odd v) in\n+\n+      (* Halve the even one and adjust the corresponding coefficient. *)\n+      let (u, tmp) := maybe_rshift1 u_even u in\n+      let A_or_B_odd := odd A || odd B in\n+      let '(A_carry, A, tmp) := maybe_add (A_or_B_odd && u_even) A n in\n+      let '(B_carry, B, tmp) := maybe_add (A_or_B_odd && u_even) B a in\n+      let (A, tmp) := maybe_rshift1_carry u_even A_carry A in\n+      let (B, tmp) := maybe_rshift1_carry u_even B_carry B in\n+\n+      let (v, tmp) := maybe_rshift1 v_even v in\n+      let C_or_D_odd := odd C || odd D in\n+      let '(C_carry, C, tmp) := maybe_add (C_or_D_odd && v_even) C n in\n+      let '(D_carry, D, tmp) := maybe_add (C_or_D_odd && v_even) D a in\n+      let (C, tmp) := maybe_rshift1_carry v_even C_carry C in\n+      let (D, tmp) := maybe_rshift1_carry v_even D_carry D in\n+      (a, n, A, B, C, D, u, v).\n+\n+    Ltac destruct_state s :=\n+      destruct s as [[[[[[[[a] [n]] [A]] [B]] [C]] [D]] [u]] [v]].\n+\n+    Lemma step_even_odd (s : state) :\n+      even_step (odd_step s) = step s.\n+    Proof.\n+      destruct_state s. reflexivity. Qed.\n+\n+    (** Next, we establish a core GCD invariant that the loop will maintain. *)\n+\n+    Definition invariant (s : state) :=\n+      match s with\n+      | (Word a, Word n, Word A, Word B, Word C, Word D, Word u, Word v) =>\n+        (* Bounds on all values. Note [B] and [D] have slightly looser bounds\n+           than [A] and [C]. *)\n+        0 < n < 2^nbits /\\\n+        0 < a < 2^abits /\\\n+        a < n /\\\n+        0 < u <= a /\\\n+        0 <= v <= n /\\\n+        0 <= A < n /\\\n+        0 <= B <= a /\\\n+        0 <= C < n /\\\n+        0 <= D <= a /\\\n+        (* The both even case is discarded early; [a] cannot have an inverse mod\n+           [n] if both are even. *)\n+        (Z.odd u = true \\/ Z.odd v = true) /\\\n+        (Z.odd a = true \\/ Z.odd n = true) /\\\n+        (* The extended GCD invariant. *)\n+        u = A*a - B*n /\\\n+        v = D*n - C*a /\\\n+        Z.gcd u v = Z.gcd a n\n+      end.\n+\n+    Lemma if_func_distr (X Y : Type) (f : X -> Y) (t : bool) (a b : X) :\n+      (if t then f a else f b) = f (if t then a else b).\n+    Proof. destruct t; reflexivity. Qed.\n+\n+    Lemma if_mod_distr (t : bool) (a b n : Z) :\n+      (if t then a mod n else b mod n) = (if t then a else b) mod n.\n+    Proof. destruct t; reflexivity. Qed.\n+\n+    Ltac simplify_words :=\n+      cbv [select odd add sub rshift1 maybe_add maybe_rshift1\n+                  maybe_rshift1_carry to_Z to_word wrap is_one];\n+      try rewrite !if_func_distr.\n+\n+    Ltac bool_to_prop_once :=\n+      first [rewrite andb_true_iff in * |\n+             rewrite andb_false_iff in * |\n+             rewrite orb_true_iff in * |\n+             rewrite orb_false_iff in * |\n+             rewrite negb_true_iff in * |\n+             rewrite negb_false_iff in * |\n+             rewrite Z.eqb_eq in * |\n+             rewrite Z.eqb_neq in * |\n+             rewrite Z.ltb_lt in * |\n+             rewrite Z.ltb_ge in * |\n+             rewrite Z.leb_le in * |\n+             rewrite Z.leb_gt in *].\n+\n+    (** Consider all possible parities for [u] and [v], but discard the one where\n+        [u] and [v] are both even. *)\n+    Ltac destruct_odd_u_v u v :=\n+      destruct (Z.odd u) eqn:Hu;\n+      destruct (Z.odd v) eqn:Hv;\n+      [ | | |\n+        (* [u] and [v] cannot both be even by [invariant]. *)\n+        destruct_head'_and;\n+        destruct_head'_or;\n+        match goal with\n+        | H : false = true |- _ => inversion H\n+        end ].\n+\n+    (** This is a roundabout way of saying [n < A + C] that comes out of [add]\n+        and [sub] in [odd_step]. *)\n+    Lemma add_then_sub_gt (bits n A C : Z)\n+          (Hn : 0 <= n < 2^bits)\n+          (HA : 0 <= A < 2^bits)\n+          (HC : 0 <= C < 2^bits) :\n+      ((A + C) mod 2^bits <? n) && negb (2^bits <=? A + C) = (A + C <? n).\n+    Proof.\n+      destruct (A + C <? n) eqn:HACn;\n+        destruct (A + C <? 2^bits) eqn:HAC2bits;\n+        repeat first [bool_to_prop_once | split];\n+        repeat match goal with\n+               | H : ?a < ?m |- context[?a mod ?m] =>\n+                 rewrite (Z.mod_small a m) by lia\n+               | _ => lia\n+               end.\n+    Qed.\n+\n+    (** Prove the left version of [Z.gcd_sub_diag_r]. *)\n+    Lemma Zgcd_sub_diag_l (n m : Z) : Z.gcd (n - m) m = Z.gcd n m.\n+    Proof.\n+      rewrite (Z.gcd_comm (n - m) m).\n+      rewrite (Z.gcd_comm n m).\n+      apply Z.gcd_sub_diag_r.\n+    Qed.\n+\n+    (** The following bounds on [B + D] come out of [nia], but [nia] takes a\n+        long time to discover this in the context of the full proof. *)\n+    Lemma AC_lt_BD_le (a n A B C D : Z) :\n+      0 <= a < n ->\n+      0 < A*a - B*n <= a ->\n+      0 <= D*n - C*a <= n ->\n+      A + C < n ->\n+      B + D <= a.\n+    Proof. nia. Qed.\n+\n+    Lemma AC_ge_BD_ge (a n A B C D : Z) :\n+      0 <= a < n ->\n+      0 < A*a - B*n <= a ->\n+      0 <= D*n - C*a <= n ->\n+      n <= A + C ->\n+      a <= B + D.\n+    Proof. nia. Qed.\n+\n+    Lemma odd_step_invariant\n+          (s : state)\n+          (H : invariant s) :\n+      invariant (odd_step s).\n+    Proof.\n+      destruct_state s.\n+      unfold odd_step, invariant in *.\n+      simplify_words.\n+\n+      rewrite add_then_sub_gt by lia.\n+\n+      (* Expand all cases and simplify. While doing so, help [lia] with bounds\n+         on [B + D] to go with the [A + C] bounds. *)\n+      destruct (A + C <? n) eqn:HACn;\n+        [ assert (B + D <= a) by (apply (AC_lt_BD_le a n A B C D);\n+                                  repeat bool_to_prop_once; lia) |\n+          assert (a <= B + D) by (apply (AC_ge_BD_ge a n A B C D);\n+                                  repeat bool_to_prop_once; lia) ];\n+        destruct_odd_u_v u v;\n+        destruct (v <? u) eqn:Huv;\n+        cbn;\n+\n+        (* Discard the cases where [odd_step] is a no-op. [Hu] and [Hv] must be\n+           re-applied due to some simplification. *)\n+        try rewrite Hu;\n+        try rewrite Hv;\n+        try apply H;\n+\n+        destruct_head'_and;\n+        repeat match goal with\n+               | _ => bool_to_prop_once\n+               | _ => rewrite Zminus_mod_idemp_l\n+               (* Note this relies both on [destruct] and [cbn] above clearing\n+                  all dead branches, as well as [Zminus_mod_idemp_l] above\n+                  simplifying some expressions. Some operations intentionally\n+                  overflow or underflow, but are either discarded by [select] or\n+                  cancelled out by a later operation. *)\n+               | _ => rewrite Z.mod_small\n+               | _ => split\n+               | _ => apply Z.mod_pos_bound\n+               | _ => rewrite Zgcd_sub_diag_l\n+               | _ => rewrite Z.gcd_sub_diag_r\n+               | _ => progress auto\n+               | _ => lia\n+               end.\n+    Qed.\n+\n+    (** [even_step] writes [(x + y) / 2] slightly funny. *)\n+    Lemma add_carry_div2 (bits x y : Z)\n+          (Hbits : 0 < bits)\n+          (Hx : 0 <= x < 2^bits)\n+          (Hy : 0 <= y < 2^bits) :\n+      (if 2^bits <=? x + y\n+       then ((x + y) mod 2^bits / 2 + 2^(bits-1))\n+       else (x + y) mod 2^bits / 2) = (x + y) / 2.\n+    Proof.\n+      destruct (2^bits <=? x + y) eqn:Hxy; repeat bool_to_prop_once.\n+      { (* 2^bits <= x + y *)\n+        rewrite Z.mod_small_1 by lia.\n+        replace (2^bits) with (2*2^(bits-1)) by (rewrite <- Z.pow_succ_r; f_equal; lia).\n+        rewrite Z.div_sub' by lia.\n+        lia. }\n+      { (* x + y < 2^bits *)\n+        rewrite Z.mod_small by lia.\n+        lia. }\n+    Qed.\n+\n+    Lemma pos_even_le (z : Z) (Heven : Z.odd z = false) (Hpos : 0 < z) :\n+      2 <= z.\n+    Proof.\n+      destruct (z =? 1) eqn:H1; repeat bool_to_prop_once.\n+      { rewrite H1 in Heven.\n+        cbn in Heven.\n+        inversion Heven. }\n+      { lia. }\n+    Qed.\n+\n+    Lemma gcd_div_rel_prime_l (a b c : Z)\n+          (Hc : 0 < c)\n+          (Hdiv : (c | a))\n+          (Hrel : rel_prime b c) :\n+      Z.gcd (a / c) b = Z.gcd a b.\n+    Proof.\n+      symmetry.\n+      apply Z.gcd_unique.\n+      - apply Z.gcd_nonneg.\n+      - apply (Z.divide_transitive (Z.gcd (a / c) b) (a / c) a).\n+        + apply Z.gcd_divide_l.\n+        + exists c; apply Zdivide_Zdiv_eq; trivial.\n+      - apply Z.gcd_divide_r.\n+      - intros q Hqa Hqb.\n+        destruct Hdiv as [x Hx].\n+        rewrite Hx in *.\n+        rewrite Z_div_mult by lia.\n+        apply Z.gcd_greatest;\n+          try apply (Gauss q c x);\n+          try apply (rel_prime_div b c q);\n+          try rewrite Z.mul_comm;\n+          trivial.\n+    Qed.\n+\n+    Lemma gcd_div_rel_prime_r (a b c : Z)\n+          (Hc : 0 < c)\n+          (Hrel : rel_prime a c)\n+          (Hdiv : (c | b)) :\n+      Z.gcd a (b / c) = Z.gcd a b.\n+    Proof.\n+      rewrite (Z.gcd_comm a (b/c)).\n+      rewrite (Z.gcd_comm a b).\n+      apply gcd_div_rel_prime_l; trivial.\n+    Qed.\n+\n+    (** Some easy lemmas bridging [Z.odd] with [Z.modulo], which\n+        [Z.div_mod_to_quot_rem] can handle. *)\n+    Lemma odd_mod_2 : forall z : Z,\n+        Z.odd z = true <-> z mod 2 = 1.\n+    Proof.\n+      intros z; split; intros H.\n+      - rewrite Zmod_odd; rewrite H; reflexivity.\n+      - rewrite Zmod_odd in H;\n+          destruct (Z.odd z); try trivial; lia.\n+    Qed.\n+    Lemma even_mod_2 : forall z : Z,\n+        Z.odd z = false <-> z mod 2 = 0.\n+    Proof.\n+      intros z; split; intros H.\n+      - rewrite Zmod_odd; rewrite H; reflexivity.\n+      - rewrite Zmod_odd in H;\n+          destruct (Z.odd z); try trivial; lia.\n+    Qed.\n+\n+    Ltac fail_if_mod t m := match t with\n+                            | _ mod m => fail 1\n+                            | _ => idtac\n+                            end.\n+\n+    Ltac push_mod_down_in t m :=","path":"src/Arithmetic/BinaryExtendedGCD.v","position":491,"original_position":491,"commit_id":"b661ce63ca921855ae1f4a9dfbad7bffb24ea8ae","original_commit_id":"b661ce63ca921855ae1f4a9dfbad7bffb24ea8ae","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},"body":"Have you seen the `push_Zmod` tactic in one of the ZUtil files?  It's probably better to make a copy of that tactic, in that file, and adapt it to work in hypotheses.  Unless you want to not consider things modulo things other than `m`?","created_at":"2018-03-24T04:37:01Z","updated_at":"2018-03-24T04:46:53Z","html_url":"https://github.com/mit-plv/fiat-crypto/pull/333#discussion_r176899879","pull_request_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333","author_association":"OWNER","_links":{"self":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments/176899879"},"html":{"href":"https://github.com/mit-plv/fiat-crypto/pull/333#discussion_r176899879"},"pull_request":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333"}}},"pull_request":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333","id":177189178,"html_url":"https://github.com/mit-plv/fiat-crypto/pull/333","diff_url":"https://github.com/mit-plv/fiat-crypto/pull/333.diff","patch_url":"https://github.com/mit-plv/fiat-crypto/pull/333.patch","issue_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/333","number":333,"state":"open","locked":false,"title":"Add a constant-time binary extended GCD algorithm.","user":{"login":"davidben","id":109690,"avatar_url":"https://avatars0.githubusercontent.com/u/109690?v=4","gravatar_id":"","url":"https://api.github.com/users/davidben","html_url":"https://github.com/davidben","followers_url":"https://api.github.com/users/davidben/followers","following_url":"https://api.github.com/users/davidben/following{/other_user}","gists_url":"https://api.github.com/users/davidben/gists{/gist_id}","starred_url":"https://api.github.com/users/davidben/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/davidben/subscriptions","organizations_url":"https://api.github.com/users/davidben/orgs","repos_url":"https://api.github.com/users/davidben/repos","events_url":"https://api.github.com/users/davidben/events{/privacy}","received_events_url":"https://api.github.com/users/davidben/received_events","type":"User","site_admin":false},"body":"Here's my latest foray into this amusement. I suspect some of this could be factored out better, but I wasn't sure what the right structure was.\r\n\r\n---\r\n\r\nThankfully, most modular inverses involve a prime or at least odd modulus, but RSA key generation requires inverting with an even modulus (the totient). Implementing that in constant-time is tricky.\r\n\r\nThis file adapts the binary extended GCD algorithm in the Handbook of Applied Cryptography. This is to verify the C implementation in https://boringssl-review.googlesource.com/c/boringssl/+/26370.","created_at":"2018-03-23T21:33:21Z","updated_at":"2018-03-24T04:46:53Z","closed_at":null,"merged_at":null,"merge_commit_sha":"4a38f96379ef7ec9222ad0b54d8f903631e6fe22","assignee":null,"assignees":[],"requested_reviewers":[{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","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}],"requested_teams":[],"labels":[],"milestone":null,"commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333/commits","review_comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333/comments","review_comment_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments{/number}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/333/comments","statuses_url":"https://api.github.com/repos/mit-plv/fiat-crypto/statuses/b661ce63ca921855ae1f4a9dfbad7bffb24ea8ae","head":{"label":"davidben:binary-ext-gcd","ref":"binary-ext-gcd","sha":"b661ce63ca921855ae1f4a9dfbad7bffb24ea8ae","user":{"login":"davidben","id":109690,"avatar_url":"https://avatars0.githubusercontent.com/u/109690?v=4","gravatar_id":"","url":"https://api.github.com/users/davidben","html_url":"https://github.com/davidben","followers_url":"https://api.github.com/users/davidben/followers","following_url":"https://api.github.com/users/davidben/following{/other_user}","gists_url":"https://api.github.com/users/davidben/gists{/gist_id}","starred_url":"https://api.github.com/users/davidben/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/davidben/subscriptions","organizations_url":"https://api.github.com/users/davidben/orgs","repos_url":"https://api.github.com/users/davidben/repos","events_url":"https://api.github.com/users/davidben/events{/privacy}","received_events_url":"https://api.github.com/users/davidben/received_events","type":"User","site_admin":false},"repo":{"id":116173280,"name":"fiat-crypto","full_name":"davidben/fiat-crypto","owner":{"login":"davidben","id":109690,"avatar_url":"https://avatars0.githubusercontent.com/u/109690?v=4","gravatar_id":"","url":"https://api.github.com/users/davidben","html_url":"https://github.com/davidben","followers_url":"https://api.github.com/users/davidben/followers","following_url":"https://api.github.com/users/davidben/following{/other_user}","gists_url":"https://api.github.com/users/davidben/gists{/gist_id}","starred_url":"https://api.github.com/users/davidben/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/davidben/subscriptions","organizations_url":"https://api.github.com/users/davidben/orgs","repos_url":"https://api.github.com/users/davidben/repos","events_url":"https://api.github.com/users/davidben/events{/privacy}","received_events_url":"https://api.github.com/users/davidben/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/davidben/fiat-crypto","description":"Cryptographic Primitive Code Generation by Fiat","fork":true,"url":"https://api.github.com/repos/davidben/fiat-crypto","forks_url":"https://api.github.com/repos/davidben/fiat-crypto/forks","keys_url":"https://api.github.com/repos/davidben/fiat-crypto/keys{/key_id}","collaborators_url":"https://api.github.com/repos/davidben/fiat-crypto/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/davidben/fiat-crypto/teams","hooks_url":"https://api.github.com/repos/davidben/fiat-crypto/hooks","issue_events_url":"https://api.github.com/repos/davidben/fiat-crypto/issues/events{/number}","events_url":"https://api.github.com/repos/davidben/fiat-crypto/events","assignees_url":"https://api.github.com/repos/davidben/fiat-crypto/assignees{/user}","branches_url":"https://api.github.com/repos/davidben/fiat-crypto/branches{/branch}","tags_url":"https://api.github.com/repos/davidben/fiat-crypto/tags","blobs_url":"https://api.github.com/repos/davidben/fiat-crypto/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/davidben/fiat-crypto/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/davidben/fiat-crypto/git/refs{/sha}","trees_url":"https://api.github.com/repos/davidben/fiat-crypto/git/trees{/sha}","statuses_url":"https://api.github.com/repos/davidben/fiat-crypto/statuses/{sha}","languages_url":"https://api.github.com/repos/davidben/fiat-crypto/languages","stargazers_url":"https://api.github.com/repos/davidben/fiat-crypto/stargazers","contributors_url":"https://api.github.com/repos/davidben/fiat-crypto/contributors","subscribers_url":"https://api.github.com/repos/davidben/fiat-crypto/subscribers","subscription_url":"https://api.github.com/repos/davidben/fiat-crypto/subscription","commits_url":"https://api.github.com/repos/davidben/fiat-crypto/commits{/sha}","git_commits_url":"https://api.github.com/repos/davidben/fiat-crypto/git/commits{/sha}","comments_url":"https://api.github.com/repos/davidben/fiat-crypto/comments{/number}","issue_comment_url":"https://api.github.com/repos/davidben/fiat-crypto/issues/comments{/number}","contents_url":"https://api.github.com/repos/davidben/fiat-crypto/contents/{+path}","compare_url":"https://api.github.com/repos/davidben/fiat-crypto/compare/{base}...{head}","merges_url":"https://api.github.com/repos/davidben/fiat-crypto/merges","archive_url":"https://api.github.com/repos/davidben/fiat-crypto/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/davidben/fiat-crypto/downloads","issues_url":"https://api.github.com/repos/davidben/fiat-crypto/issues{/number}","pulls_url":"https://api.github.com/repos/davidben/fiat-crypto/pulls{/number}","milestones_url":"https://api.github.com/repos/davidben/fiat-crypto/milestones{/number}","notifications_url":"https://api.github.com/repos/davidben/fiat-crypto/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/davidben/fiat-crypto/labels{/name}","releases_url":"https://api.github.com/repos/davidben/fiat-crypto/releases{/id}","deployments_url":"https://api.github.com/repos/davidben/fiat-crypto/deployments","created_at":"2018-01-03T19:22:02Z","updated_at":"2018-01-03T19:22:17Z","pushed_at":"2018-03-23T21:25:00Z","git_url":"git://github.com/davidben/fiat-crypto.git","ssh_url":"git@github.com:davidben/fiat-crypto.git","clone_url":"https://github.com/davidben/fiat-crypto.git","svn_url":"https://github.com/davidben/fiat-crypto","homepage":"","size":24470,"stargazers_count":0,"watchers_count":0,"language":"Coq","has_issues":false,"has_projects":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"open_issues_count":0,"license":null,"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"mit-plv:master","ref":"master","sha":"02a847a95ffc6c64b6bf8ce0ba38ca3b3d797f38","user":{"login":"mit-plv","id":11860253,"avatar_url":"https://avatars3.githubusercontent.com/u/11860253?v=4","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"repo":{"id":42269036,"name":"fiat-crypto","full_name":"mit-plv/fiat-crypto","owner":{"login":"mit-plv","id":11860253,"avatar_url":"https://avatars3.githubusercontent.com/u/11860253?v=4","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/mit-plv/fiat-crypto","description":"Cryptographic Primitive Code Generation by Fiat","fork":false,"url":"https://api.github.com/repos/mit-plv/fiat-crypto","forks_url":"https://api.github.com/repos/mit-plv/fiat-crypto/forks","keys_url":"https://api.github.com/repos/mit-plv/fiat-crypto/keys{/key_id}","collaborators_url":"https://api.github.com/repos/mit-plv/fiat-crypto/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/mit-plv/fiat-crypto/teams","hooks_url":"https://api.github.com/repos/mit-plv/fiat-crypto/hooks","issue_events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/events{/number}","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/events","assignees_url":"https://api.github.com/repos/mit-plv/fiat-crypto/assignees{/user}","branches_url":"https://api.github.com/repos/mit-plv/fiat-crypto/branches{/branch}","tags_url":"https://api.github.com/repos/mit-plv/fiat-crypto/tags","blobs_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/refs{/sha}","trees_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/trees{/sha}","statuses_url":"https://api.github.com/repos/mit-plv/fiat-crypto/statuses/{sha}","languages_url":"https://api.github.com/repos/mit-plv/fiat-crypto/languages","stargazers_url":"https://api.github.com/repos/mit-plv/fiat-crypto/stargazers","contributors_url":"https://api.github.com/repos/mit-plv/fiat-crypto/contributors","subscribers_url":"https://api.github.com/repos/mit-plv/fiat-crypto/subscribers","subscription_url":"https://api.github.com/repos/mit-plv/fiat-crypto/subscription","commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/commits{/sha}","git_commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/commits{/sha}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/comments{/number}","issue_comment_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments{/number}","contents_url":"https://api.github.com/repos/mit-plv/fiat-crypto/contents/{+path}","compare_url":"https://api.github.com/repos/mit-plv/fiat-crypto/compare/{base}...{head}","merges_url":"https://api.github.com/repos/mit-plv/fiat-crypto/merges","archive_url":"https://api.github.com/repos/mit-plv/fiat-crypto/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/mit-plv/fiat-crypto/downloads","issues_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues{/number}","pulls_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls{/number}","milestones_url":"https://api.github.com/repos/mit-plv/fiat-crypto/milestones{/number}","notifications_url":"https://api.github.com/repos/mit-plv/fiat-crypto/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/labels{/name}","releases_url":"https://api.github.com/repos/mit-plv/fiat-crypto/releases{/id}","deployments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/deployments","created_at":"2015-09-10T20:29:16Z","updated_at":"2018-03-23T18:02:36Z","pushed_at":"2018-03-23T21:33:21Z","git_url":"git://github.com/mit-plv/fiat-crypto.git","ssh_url":"git@github.com:mit-plv/fiat-crypto.git","clone_url":"https://github.com/mit-plv/fiat-crypto.git","svn_url":"https://github.com/mit-plv/fiat-crypto","homepage":"","size":24555,"stargazers_count":71,"watchers_count":71,"language":"Coq","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":14,"mirror_url":null,"archived":false,"open_issues_count":30,"license":{"key":"mit","name":"MIT License","spdx_id":"MIT","url":"https://api.github.com/licenses/mit"},"forks":14,"open_issues":30,"watchers":71,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333"},"html":{"href":"https://github.com/mit-plv/fiat-crypto/pull/333"},"issue":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/333"},"comments":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/333/comments"},"review_comments":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333/comments"},"review_comment":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/333/commits"},"statuses":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/statuses/b661ce63ca921855ae1f4a9dfbad7bffb24ea8ae"}},"author_association":"COLLABORATOR"}}
{"actor":{"display_login":"JasonGross"}}