possible_limbs = 
Some
  [("2^127 - 1", [(64, [3]); (32, [5; 6; 7])]);
  ("2^129 - 25", [(64, [3; 4; 5]); (32, [5; 6; 7; 8; 9])]);
  ("2^130 - 5", [(64, [3; 4; 5]); (32, [5; 6; 7; 8; 9])]);
  ("2^137 - 13", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
  ("2^140 - 27", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
  ("2^141 - 9", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
  ("2^150 - 5", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
  ("2^150 - 3", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
  ("2^152 - 17", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
  ("2^158 - 15", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
  ("2^165 - 25", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
  ("2^166 - 5", [(64, [3; 4; 5]); (32, [6; 7; 8; 9; 10; 11])]);
  ("2^171 - 19", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
  ("2^174 - 17", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
  ("2^174 - 3", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
  ("2^189 - 25", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
  ("2^190 - 11", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
  ("2^191 - 19", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
  ("2^194 - 33", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
  ("2^196 - 15", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
  ("2^198 - 17", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
  ("2^206 - 5", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
  ("2^212 - 29", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
  ("2^213 - 3", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
  ("2^221 - 3", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
  ("2^222 - 117", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
  ("2^226 - 5", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
  ("2^230 - 27", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
  ("2^235 - 15", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
  ("2^243 - 9", [(64, [5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
  ("2^251 - 9", [(64, [5; 6; 7]); (32, [10; 11; 12; 13; 14; 15])]);
  ("2^255 - 765", [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
  ("2^255 - 19", [(64, [5; 6; 7]); (32, [10; 11; 12; 13; 14; 15])]);
  ("2^256 - 189", [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
  ("2^266 - 3",
  [(64, [5; 6; 7; 8; 9]); (32, [10; 11; 12; 13; 14; 15; 16; 17])]);
  ("2^285 - 9", [(64, [5; 6; 7; 8; 9]); (32, [11; 12; 13; 14; 15; 16; 17])]);
  ("2^291 - 19",
  [(64, [5; 6; 7; 8; 9]); (32, [12; 13; 14; 15; 16; 17; 18; 19])]);
  ("2^321 - 9",
  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
  ("2^336 - 17",
  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
  ("2^336 - 3",
  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
  ("2^338 - 15",
  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
  ("2^192 - 2^64 - 1", [(64, [4; 5]); (32, [9; 10; 11])]);
  ("2^216 - 2^108 - 1", [(64, [4; 5; 6; 7]); (32, [8; 10; 11; 12; 13])]);
  ("2^322 - 2^161 - 1",
  [(64, [6; 7; 8; 9; 10; 11]); (32, [12; 14; 15; 16; 17; 18; 19; 20; 21])]);
  ("2^205 - 45*2^198 - 1", [(64, []); (32, [])]);
  ("2^224 - 2^96 + 1", [(64, [5; 6; 7]); (32, [10; 11; 12; 13])]);
  ("2^256 - 2^224 + 2^192 + 2^96 - 1",
  [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
  ("2^256 - 2^32 - 977", [(64, [6; 7]); (32, [11; 12; 13; 14; 15])]);
  ("2^256 - 4294968273", [(64, [6; 7]); (32, [])]);
  ("2^256 - 88*2^240 - 1", [(64, []); (32, [])]);
  ("2^254 - 127*2^240 - 1", [(64, []); (32, [])])]
     : option (list (string * list (nat * list nat)))