Theory Pratt_Certificate.Pratt_Certificate_Code

(*
  File:     Pratt_Certificate_Code.thy
  Author:   Manuel Eberl, TU München

  Efficient checking of Pratt certificates using the code generator.
  Evaluation on some big examples.
*)
theory Pratt_Certificate_Code
  imports
  Pratt_Certificate
  "HOL-Library.Code_Target_Numeral"
begin

subsection ‹Code generation for Pratt certificates›

text ‹
  The following one-time setup is required to set up code generation for the certificate
  checking. Other theories importing this theories do not have to do this again.
›

setup ‹
  Context.theory_map (Pratt.setup_valid_cert_code_conv
    (@{computation_check
        terms: Trueprop valid_pratt_tree "0::nat" "1::nat" "2::nat" "3::nat" "4::nat"
        datatypes: "pratt_tree list" "nat × nat × pratt_tree list" nat}))
›

text ‹
  We can now evaluate the efficiency of the procedure on some examples.
›

lemma "prime (131059 :: nat)"
  by (pratt (code))

lemma "prime (100000007 :: nat)"
  by (pratt (code))

lemma "prime (8504276003 :: nat)"
  by (pratt (code))

lemma "prime (52759926861157 :: nat)"
  by (pratt (code))

lemma "prime (39070009756439177203 :: nat)"
  by (pratt (code)
        ‹{39070009756439177203, 2, 
           {2, {3, 2, {2}}, {197, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}, 
            {11018051256751037, 2, {2, {19, 2, {2, {3, 2, {2}}}}, 
              {1249, 7, {2, {3, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}}}, 
              {116072344789, 2, {2, {3, 2, {2}}, 
                {3067, 2, {2, {3, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}, 
                  {73, 5, {2, {3, 2, {2}}}}}}, 
                {3153797, 2, {2, {788449, 11, 
                   {2, {3, 2, {2}}, {43, 3, 
                     {2, {3, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}}}, 
                    {191, 19, {2, {5, 2, {2}}, {19, 2, {2, {3, 2, {2}}}}}}}}}}}}}}}}›)

lemma "prime (933491553728809239092563013853810654040043466297416456476877 :: nat)"
  by (pratt (code)
        ‹{933491553728809239092563013853810654040043466297416456476877, 
             2, {2, {38463351105299604725411, 6, 
               {2, {5, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}, 
                {295871931579227728657, 5, 
                 {2, {3, 2, {2}}, {26041, 13, 
                   {2, {3, 2, {2}}, {5, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}, 
                    {31, 3, {2, {3, 2, {2}}, {5, 2, {2}}}}}}, 
                  {29009, 3, {2, {7, 3, {2, {3, 2, {2}}}}, 
                    {37, 2, {2, {3, 2, {2}}}}}}, 
                  {39133, 5, {2, {3, 2, {2}}, 
                    {1087, 3, {2, {3, 2, {2}}, 
                      {181, 2, {2, {3, 2, {2}}, {5, 2, {2}}}}}}}}, 
                  {208511, 7, {2, {5, 2, {2}}, {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}, 
                    {719, 11, {2, {359, 7, 
                       {2, {179, 2, {2, {89, 3, {2, {11, 2, {2, {5, 2, {2}}}}}}}}}}}}}}
                   }}}}, {6067409149902371339956289140415169329, 3, 
               {2, {11, 2, {2, {5, 2, {2}}}}, 
                {103, 5, {2, {3, 2, {2}}, {17, 3, {2}}}}, 
                {7955023343, 7, {2, {7, 3, {2, {3, 2, {2}}}}, 
                  {79, 3, {2, {3, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}}}, 
                  {1451, 2, {2, {5, 2, {2}}, {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}}}, 
                  {4957, 2, {2, {3, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}, 
                    {59, 2, {2, {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}}}}}}}, 
                {8108847767, 5, {2, {4054423883, 2, 
                   {2, {2027211941, 2, {2, {5, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}, 
                      {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}, 
                      {268861, 6, {2, {3, 2, {2}}, {5, 2, {2}}, 
                        {4481, 3, {2, {5, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}}}}}}}}}}}, 
                {5188630976471, 13, {2, {5, 2, {2}}, 
                  {518863097647, 5, {2, {3, 2, {2}}, 
                    {67, 2, {2, {3, 2, {2}}, {11, 2, {2, {5, 2, {2}}}}}}, 
                    {17881, 7, {2, {3, 2, {2}}, {5, 2, {2}}, 
                      {149, 2, {2, {37, 2, {2, {3, 2, {2}}}}}}}}, 
                    {24061, 10, {2, {3, 2, {2}}, {5, 2, {2}}, 
                      {401, 3, {2, {5, 2, {2}}}}}}}}}}}}}}
›)

text ‹
  The bulk command can now also use code generation.
  As an example, we prove some constants from FIPS 186-4 to be prime.
›

check_pratt_primes (code) fips_186_4_primes ‹
  {3, 2, {2}}
  {5, 2, {2}}
  {7, 3, {2, 3}}
  {11, 2, {2, 5}}
  {13, 2, {2, 3}}
  {17, 3, {2}}
  {19, 2, {2, 3}}
  {23, 5, {2, 11}}
  {29, 2, {2, 7}}
  {31, 3, {2, 3, 5}}
  {37, 2, {2, 3}}
  {41, 6, {2, 5}}
  {43, 3, {2, 3, 7}}
  {47, 5, {2, 23}}
  {53, 2, {2, 13}}
  {59, 2, {2, 29}}
  {61, 2, {2, 3, 5}}
  {67, 2, {2, 3, 11}}
  {71, 7, {2, 5, 7}}
  {73, 5, {2, 3}}
  {79, 3, {2, 3, 13}}
  {89, 3, {2, 11}}
  {97, 5, {2, 3}}
  {101, 2, {2, 5}}
  {103, 5, {2, 3, 17}}
  {107, 2, {2, 53}}
  {109, 6, {2, 3}}
  {113, 3, {2, 7}}
  {127, 3, {2, 3, 7}}
  {131, 2, {2, 5, 13}}
  {139, 2, {2, 3, 23}}
  {149, 2, {2, 37}}
  {151, 6, {2, 3, 5}}
  {157, 5, {2, 3, 13}}
  {163, 2, {2, 3}}
  {173, 2, {2, 43}}
  {179, 2, {2, 89}}
  {181, 2, {2, 3, 5}}
  {191, 19, {2, 5, 19}}
  {193, 5, {2, 3}}
  {197, 2, {2, 7}}
  {199, 3, {2, 3, 11}}
  {211, 2, {2, 3, 5, 7}}
  {223, 3, {2, 3, 37}}
  {227, 2, {2, 113}}
  {229, 6, {2, 3, 19}}
  {233, 3, {2, 29}}
  {239, 7, {2, 7, 17}}
  {241, 7, {2, 3, 5}}
  {251, 6, {2, 5}}
  {257, 3, {2}}
  {263, 5, {2, 131}}
  {269, 2, {2, 67}}
  {271, 6, {2, 3, 5}}
  {277, 5, {2, 3, 23}}
  {281, 3, {2, 5, 7}}
  {283, 3, {2, 3, 47}}
  {293, 2, {2, 73}}
  {311, 17, {2, 5, 31}}
  {313, 10, {2, 3, 13}}
  {317, 2, {2, 79}}
  {331, 3, {2, 3, 5, 11}}
  {337, 10, {2, 3, 7}}
  {347, 2, {2, 173}}
  {349, 2, {2, 3, 29}}
  {373, 2, {2, 3, 31}}
  {397, 5, {2, 3, 11}}
  {421, 2, {2, 3, 5, 7}}
  {439, 15, {2, 3, 73}}
  {491, 2, {2, 5, 7}}
  {509, 2, {2, 127}}
  {521, 3, {2, 5, 13}}
  {547, 2, {2, 3, 7, 13}}
  {569, 3, {2, 71}}
  {593, 3, {2, 37}}
  {599, 7, {2, 13, 23}}
  {607, 3, {2, 3, 101}}
  {619, 2, {2, 3, 103}}
  {631, 3, {2, 3, 5, 7}}
  {641, 3, {2, 5}}
  {653, 2, {2, 163}}
  {659, 2, {2, 7, 47}}
  {661, 2, {2, 3, 5, 11}}
  {683, 5, {2, 11, 31}}
  {727, 5, {2, 3, 11}}
  {757, 2, {2, 3, 7}}
  {811, 3, {2, 3, 5}}
  {877, 2, {2, 3, 73}}
  {881, 3, {2, 5, 11}}
  {907, 2, {2, 3, 151}}
  {919, 7, {2, 3, 17}}
  {937, 5, {2, 3, 13}}
  {1031, 14, {2, 5, 103}}
  {1033, 5, {2, 3, 43}}
  {1051, 7, {2, 3, 5, 7}}
  {1087, 3, {2, 3, 181}}
  {1117, 2, {2, 3, 31}}
  {1187, 2, {2, 593}}
  {1201, 11, {2, 3, 5}}
  {1237, 2, {2, 3, 103}}
  {1283, 2, {2, 641}}
  {1297, 10, {2, 3}}
  {1303, 6, {2, 3, 7, 31}}
  {1319, 13, {2, 659}}
  {1373, 2, {2, 7}}
  {1381, 2, {2, 3, 5, 23}}
  {1433, 3, {2, 179}}
  {1511, 11, {2, 5, 151}}
  {1531, 2, {2, 3, 5, 17}}
  {1543, 5, {2, 3, 257}}
  {1553, 3, {2, 97}}
  {1579, 3, {2, 3, 263}}
  {1613, 3, {2, 13, 31}}
  {1663, 3, {2, 3, 277}}
  {1693, 2, {2, 3, 47}}
  {1889, 3, {2, 59}}
  {2063, 5, {2, 1031}}
  {2089, 7, {2, 3, 29}}
  {2153, 3, {2, 269}}
  {2213, 2, {2, 7, 79}}
  {2389, 2, {2, 3, 199}}
  {2411, 6, {2, 5, 241}}
  {2437, 2, {2, 3, 7, 29}}
  {2477, 2, {2, 619}}
  {2707, 2, {2, 3, 11, 41}}
  {2731, 3, {2, 3, 5, 7, 13}}
  {3023, 5, {2, 1511}}
  {3191, 11, {2, 5, 11, 29}}
  {3253, 2, {2, 3, 271}}
  {3407, 5, {2, 13, 131}}
  {3433, 5, {2, 3, 11, 13}}
  {3517, 2, {2, 3, 293}}
  {3677, 2, {2, 919}}
  {3739, 7, {2, 3, 7, 89}}
  {3769, 7, {2, 3, 157}}
  {4127, 5, {2, 2063}}
  {4349, 2, {2, 1087}}
  {5449, 7, {2, 3, 227}}
  {6043, 5, {2, 3, 19, 53}}
  {6317, 2, {2, 1579}}
  {6829, 2, {2, 3, 569}}
  {8191, 17, {2, 3, 5, 7, 13}}
  {8389, 6, {2, 3, 233}}
  {8699, 2, {2, 4349}}
  {9227, 2, {2, 7, 659}}
  {9547, 2, {2, 3, 37, 43}}
  {10861, 2, {2, 3, 5, 181}}
  {10909, 2, {2, 3, 101}}
  {14461, 2, {2, 3, 5, 241}}
  {15601, 23, {2, 3, 5, 13}}
  {16657, 5, {2, 3, 347}}
  {16879, 3, {2, 3, 29, 97}}
  {16979, 2, {2, 13, 653}}
  {17293, 7, {2, 3, 11, 131}}
  {17449, 14, {2, 3, 727}}
  {17467, 3, {2, 3, 41, 71}}
  {18169, 11, {2, 3, 757}}
  {20341, 2, {2, 3, 5, 113}}
  {20599, 3, {2, 3, 3433}}
  {21407, 5, {2, 7, 11, 139}}
  {23609, 6, {2, 13, 227}}
  {28793, 3, {2, 59, 61}}
  {30859, 2, {2, 3, 37, 139}}
  {34429, 2, {2, 3, 19, 151}}
  {37447, 3, {2, 3, 79}}
  {38189, 2, {2, 9547}}
  {38557, 2, {2, 3, 7, 17}}
  {42641, 3, {2, 5, 13, 41}}
  {49481, 3, {2, 5, 1237}}
  {51419, 2, {2, 47, 547}}
  {51481, 17, {2, 3, 5, 11, 13}}
  {53197, 2, {2, 3, 11, 13, 31}}
  {54251, 2, {2, 5, 7, 31}}
  {54623, 5, {2, 31, 881}}
  {60449, 3, {2, 1889}}
  {61681, 29, {2, 3, 5, 257}}
  {64901, 2, {2, 5, 11, 59}}
  {65537, 3, {2}}
  {65677, 2, {2, 3, 13, 421}}
  {78283, 3, {2, 3, 4349}}
  {85999, 3, {2, 3, 11, 1303}}
  {87739, 7, {2, 3, 7, 2089}}
  {92581, 6, {2, 3, 5, 1543}}
  {104471, 11, {2, 5, 31, 337}}
  {126241, 7, {2, 3, 5, 263}}
  {133279, 3, {2, 3, 97, 229}}
  {145091, 2, {2, 5, 11, 1319}}
  {149309, 2, {2, 163, 229}}
  {155317, 5, {2, 3, 7, 43}}
  {161969, 3, {2, 53, 191}}
  {166571, 2, {2, 5, 16657}}
  {166823, 5, {2, 239, 349}}
  {248431, 3, {2, 3, 5, 7, 13}}
  {274177, 5, {2, 3, 7, 17}}
  {275729, 3, {2, 19, 907}}
  {312289, 14, {2, 3, 3253}}
  {330563, 2, {2, 19, 8699}}
  {336757, 2, {2, 3, 7, 19, 211}}
  {363557, 2, {2, 97, 937}}
  {370471, 3, {2, 3, 5, 53, 233}}
  {379787, 2, {2, 11, 61, 283}}
  {409891, 14, {2, 3, 5, 13, 1051}}
  {455737, 11, {2, 3, 17, 1117}}
  {490463, 14, {2, 7, 53, 661}}
  {495527, 5, {2, 41, 6043}}
  {568151, 17, {2, 5, 11, 1033}}
  {704251, 2, {2, 3, 5, 313}}
  {723127, 3, {2, 3, 191, 631}}
  {777241, 7, {2, 3, 5, 17, 127}}
  {858001, 17, {2, 3, 5, 11, 13}}
  {1276987, 2, {2, 3, 29, 41, 179}}
  {2995763, 2, {2, 7, 11, 397}}
  {2998279, 3, {2, 3, 166571}}
  {3969899, 2, {2, 19, 104471}}
  {5746001, 15, {2, 5, 13, 17}}
  {6051631, 6, {2, 3, 5, 13, 59, 263}}
  {6700417, 5, {2, 3, 17449}}
  {6937379, 2, {2, 7, 495527}}
  {7623851, 6, {2, 5, 13, 37, 317}}
  {8196883, 2, {2, 3, 79, 17293}}
  {8413201, 29, {2, 3, 5, 19, 41}}
  {8463023, 5, {2, 113, 37447}}
  {8620289, 3, {2, 151, 223}}
  {9211861, 2, {2, 3, 5, 7, 2437}}
  {9350987, 2, {2, 17, 229, 1201}}
  {9863677, 5, {2, 3, 311, 881}}
  {10577321, 17, {2, 5, 13, 20341}}
  {10924559, 7, {2, 59, 92581}}
  {11105363, 2, {2, 509, 10909}}
  {11393611, 10, {2, 3, 5, 379787}}
  {13928737, 15, {2, 3, 145091}}
  {15716741, 2, {2, 5, 13, 60449}}
  {19353437, 2, {2, 277, 17467}}
  {34110701, 15, {2, 5, 13, 19, 1381}}
  {46245989, 2, {2, 1693, 6829}}
  {51920273, 3, {2, 61, 53197}}
  {103840547, 2, {2, 51920273}}
  {105957871, 3, {2, 3, 5, 19, 211, 881}}
  {154950581, 2, {2, 5, 17, 455737}}
  {186406729, 7, {2, 3, 61, 157, 811}}
  {187019741, 2, {2, 5, 9350987}}
  {191039911, 3, {2, 3, 5, 41, 155317}}
  {204061199, 11, {2, 11, 23, 107, 3769}}
  {246608641, 19, {2, 3, 5, 21407}}
  {252396031, 3, {2, 3, 5, 8413201}}
  {272109983, 5, {2, 19, 73, 233, 421}}
  {290064143, 5, {2, 79, 491, 3739}}
  {308761441, 17, {2, 3, 5, 13, 49481}}
  {311245691, 2, {2, 5, 7, 17, 29, 311}}
  {513928823, 5, {2, 11, 59, 599, 661}}
  {532247449, 7, {2, 3, 61, 363557}}
  {622491383, 5, {2, 311245691}}
  {821796863, 5, {2, 37, 11105363}}
  {1458105463, 3, {2, 3, 11, 311, 877}}
  {2400573761, 3, {2, 5, 13, 347, 1663}}
  {2534364967, 3, {2, 3, 7, 8620289}}
  {2862218959, 3, {2, 3, 157, 1373, 2213}}
  {24098228377, 7, {2, 3, 109, 9211861}}
  {34282281433, 17, {2, 3, 7, 204061199}}
  {53448597593, 3, {2, 13, 513928823}}
  {65427463921, 17, {2, 3, 5, 7, 13, 2995763}}
  {66417393611, 6, {2, 5, 53, 173, 197, 3677}}
  {101785224689, 3, {2, 7, 131, 6937379}}
  {228572385721, 23, {2, 3, 5, 7, 272109983}}
  {455827231987, 2, {2, 3, 7, 43, 252396031}}
  {674750394557, 2, {2, 7, 24098228377}}
  {807145746439, 3, {2, 3, 47, 2862218959}}
  {1002328039319, 19, {2, 126241, 3969899}}
  {1436833069313, 3, {2, 16979, 330563}}
  {11290956913871, 13, {2, 5, 17, 66417393611}}
  {23314383343543, 3, {2, 3, 17, 228572385721}}
  {37344768852931, 3, {2, 3, 5, 7, 11, 149, 9863677}}
  {43800962361397, 6, {2, 3, 41, 10861, 8196883}}
  {44925942675193, 5, {2, 3, 3517, 532247449}}
  {67280421310721, 3, {2, 5, 47, 373, 2998279}}
  {108140989558681, 17, {2, 3, 5, 13, 683, 1433, 23609}}
  {145295143558111, 7, {2, 3, 5, 7, 13, 2534364967}}
  {432621809776543, 3, {2, 3, 87739, 821796863}}
  {7244839476697597, 2, {2, 3, 239, 54623, 46245989}}
  {7532705587894727, 5, {2, 29, 43, 331, 4127, 51419}}
  {46076956964474543, 5, {2, 23, 18169, 704251, 78283}}
  {55942463741690639, 7, {2, 7, 107, 37344768852931}}
  {60018716061994831, 7, {2, 3, 5, 7, 19, 777241, 19353437}}
  {108341181769254293, 2, {2, 17, 43, 2477, 54251, 275729}}
  {208150935158385979, 2, {2, 3, 11, 43, 127, 3023, 191039911}}
  {361725589517273017, 17, {2, 3, 7, 3191, 674750394557}}
  {1357291859799823621, 2, {2, 3, 5, 67, 6317, 53448597593}}
  {5933177618131140283, 2, {2, 3, 723127, 455827231987}}
  {88599952463812275001, 11, {2, 3, 5, 19, 281, 1187, 186406729}}
  {426632512014427833817, 11, {2, 3, 13, 89, 659, 23314383343543}}
  {529709925838459440593, 3, {2, 7, 181, 105957871, 246608641}}
  {3473195323567808068309, 2, {2, 3, 13, 19, 59, 9227, 65677, 10924559}}
  {4239602065187190872179, 2, {2, 3, 61, 193, 60018716061994831}}
  {35581458644053887931343, 5, {2, 17, 41, 568151, 44925942675193}}
  {120699720968197491947347, 3, {2, 3, 13, 34429, 290064143, 154950581}}
  {1647781915921980690468599, 13, {2, 17, 547, 88599952463812275001}}
  {9564682313913860059195669, 2, {2, 3, 7, 15716741, 7244839476697597}}
  {136401162692544977256234449, 3, {2, 31, 30859, 20599, 432621809776543}}
  {173308343918874810521923841, 3, {2, 5, 13, 28793, 361725589517273017}}
  {288626509448065367648032903, 6, {2, 3, 19, 37, 607, 5933177618131140283}}
  {1124679999981664229965379347, 2, {2, 3, 1553, 120699720968197491947347}}
  {1495199339761412565498084319, 6, {2, 3, 64901, 426632512014427833817}}
  {2624747550333869278416773953, 7, {2, 3, 1297, 16879, 208150935158385979}}
  {3433859179316188682119986911, 13, {2, 5, 439, 103840547, 7532705587894727}}
  {17942392077136950785977011829, 6, {2, 3, 1495199339761412565498084319}}
  {23964610537191310276190549303, 5, {2, 336757, 35581458644053887931343}}
  {862725979338887169942859774909, 2, {2, 3, 23964610537191310276190549303}}
  {20705423504133292078628634597817, 5, {2, 3, 862725979338887169942859774909}}
  {34646440928557194402992574983797, 2, {2, 3, 61, 347, 136401162692544977256234449}}
  {144471089338257942164514676806340723, 11,
    {2, 3, 11, 109, 14461, 133279, 3473195323567808068309}}
  {7427946019382605513260578233234962521, 3,
    {2, 5, 43800962361397, 4239602065187190872179}}
  {375503554633724504423937478103159147573209, 19,
    {2, 3, 2707, 166823, 34646440928557194402992574983797}}
  {413244619895455989650825325680172591660047, 5,
    {2, 17, 97, 6051631, 20705423504133292078628634597817}}
  {12397338596863679689524759770405177749801411, 2,
    {2, 3, 5, 413244619895455989650825325680172591660047}}
  {774023187263532362759620327192479577272145303, 3,
    {2, 3, 2411, 11290956913871, 34282281433, 46076956964474543}}
  {835945042244614951780389953367877943453916927241, 11,
    {2, 3, 5, 774023187263532362759620327192479577272145303}}
  {15994076126984618329123851002118749004583184815459808099, 2,
    {2, 10577321, 101785224689, 7427946019382605513260578233234962521}}
  {6277101735386680763835789423176059013767194773182842284081, 3,
    {2, 5, 2389, 9564682313913860059195669, 3433859179316188682119986911}}
  {6277101735386680763835789423207666416083908700390324961279, 11,
    {2, 59, 149309, 11393611, 108341181769254293, 288626509448065367648032903}}
  {50520606258875818707470860153287666700917696099933389351507, 2,
    {2, 89, 631, 85999, 13928737, 375503554633724504423937478103159147573209}}
  {1059392654943455286185473617842338478315215895509773412096307, 2,
    {2, 251, 248431, 8463023, 55942463741690639, 17942392077136950785977011829}}
  {26959946667150639794667015087019625940457807714424391721682722368061, 2,
    {2, 3, 5, 17, 2153, 50520606258875818707470860153287666700917696099933389351507}}
  {26959946667150639794667015087019630673557916260026308143510066298881, 22,
    {2, 3, 5, 17, 257, 641, 65537, 274177, 6700417, 67280421310721}}
  {115792089210356248762697446949407573529996955224135760342422259061068512044369, 7,
    {2, 3, 71, 131, 373, 3407, 17449, 38189, 1002328039319, 187019741, 622491383,
      2624747550333869278416773953}}
  {115792089210356248762697446949407573530086143415290314195533631308867097853951, 6,
    {2, 3, 5, 17, 257, 641, 1531, 65537, 490463, 6700417,
      835945042244614951780389953367877943453916927241}}
  {3055465788140352002733946906144561090641249606160407884365391979704929268480326390471,
    12,
    {2, 3, 5, 151, 347, 1276987, 1436833069313,
      1059392654943455286185473617842338478315215895509773412096307}}
  {19173790298027098165721053155794528970226934547887232785722672956982046098136719667167519737147526097,
    3, {2, 11, 8389, 38557, 312289, 1357291859799823621, 529709925838459440593,
         12397338596863679689524759770405177749801411}}
  {3636410625392624440351547907325502812950802686368714273274221490761556277859337865760708490235892541081304511,
    19,
    {2, 5, 19, 263, 5449, 15601, 370471, 144471089338257942164514676806340723,
      15994076126984618329123851002118749004583184815459808099}}
  {39402006196394479212279040100143613805079739270465446667946905279627659399113263569398956308152294913554433653942643,
    2, {2, 3, 7, 13, 1124679999981664229965379347,
         3055465788140352002733946906144561090641249606160407884365391979704929268480326390471}}
  {39402006196394479212279040100143613805079739270465446667948293404245721771496870329047266088258938001861606973112319,
    19,
    {2, 19, 67, 807145746439,
      19173790298027098165721053155794528970226934547887232785722672956982046098136719667167519737147526097}}
  {3615194794881930010216942559103847593050265703173292383701371712350878926821661243755933835426896058418509759880171943,
    3, {2, 3, 11, 31, 161969,
         3636410625392624440351547907325502812950802686368714273274221490761556277859337865760708490235892541081304511}}
  {6864797660130609714981900799081393217269435300143305409394463459185543183397655394245057746333217197532963996371363321113864768612440380340372808892707005449,
    3, {2, 7, 11, 1283, 1458105463, 1647781915921980690468599,
         3615194794881930010216942559103847593050265703173292383701371712350878926821661243755933835426896058418509759880171943}}
  {6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057151,
    3, {2, 3, 5, 11, 17, 31, 41, 53, 131, 157, 521, 1613, 2731, 8191, 61681, 51481, 42641,
         409891, 858001, 7623851, 5746001, 34110701, 308761441, 2400573761, 65427463921,
         108140989558681, 145295143558111, 173308343918874810521923841}}
›
thm fips_186_4_primes

text ‹
  Two more primes from PKCS #1 v2.2.
›
check_pratt_primes (code reduce) pkcs_1_primes ‹
  2
  {3, 2, {2}}
  {5, 2, {2}}
  {7, 3, {2, 3}}
  {11, 2, {2, 5}}
  {13, 2, {2, 3}}
  {17, 3, {2}}
  {19, 2, {2, 3}}
  {23, 5, {2, 11}}
  {29, 2, {2, 7}}
  {31, 3, {2, 3, 5}}
  {37, 2, {2, 3}}
  {43, 3, {2, 3, 7}}
  {47, 5, {2, 23}}
  {53, 2, {2, 13}}
  {61, 2, {2, 3, 5}}
  {67, 2, {2, 3, 11}}
  {71, 7, {2, 5, 7}}
  {73, 5, {2, 3}}
  {79, 3, {2, 3, 13}}
  {89, 3, {2, 11}}
  {97, 5, {2, 3}}
  {101, 2, {2, 5}}
  {107, 2, {2, 53}}
  {109, 6, {2, 3}}
  {127, 3, {2, 3, 7}}
  {131, 2, {2, 5, 13}}
  {137, 3, {2, 17}}
  {139, 2, {2, 3, 23}}
  {151, 6, {2, 3, 5}}
  {157, 5, {2, 3, 13}}
  {163, 2, {2, 3}}
  {179, 2, {2, 89}}
  {191, 19, {2, 5, 19}}
  {199, 3, {2, 3, 11}}
  {211, 2, {2, 3, 5, 7}}
  {239, 7, {2, 7, 17}}
  {241, 7, {2, 3, 5}}
  {251, 6, {2, 5}}
  {269, 2, {2, 67}}
  {281, 3, {2, 5, 7}}
  {283, 3, {2, 3, 47}}
  {293, 2, {2, 73}}
  {307, 5, {2, 3, 17}}
  {331, 3, {2, 3, 5, 11}}
  {359, 7, {2, 179}}
  {367, 6, {2, 3, 61}}
  {383, 5, {2, 191}}
  {419, 2, {2, 11, 19}}
  {443, 2, {2, 13, 17}}
  {449, 3, {2, 7}}
  {457, 13, {2, 3, 19}}
  {509, 2, {2, 127}}
  {557, 2, {2, 139}}
  {601, 7, {2, 3, 5}}
  {607, 3, {2, 3, 101}}
  {641, 3, {2, 5}}
  {659, 2, {2, 7, 47}}
  {839, 11, {2, 419}}
  {857, 3, {2, 107}}
  {881, 3, {2, 5, 11}}
  {887, 5, {2, 443}}
  {1019, 2, {2, 509}}
  {1171, 2, {2, 3, 5, 13}}
  {1229, 2, {2, 307}}
  {1291, 2, {2, 3, 5, 43}}
  {1381, 2, {2, 3, 5, 23}}
  {1459, 3, {2, 3}}
  {1699, 3, {2, 3, 283}}
  {1747, 2, {2, 3, 97}}
  {1973, 2, {2, 17, 29}}
  {2039, 7, {2, 1019}}
  {2129, 3, {2, 7, 19}}
  {2203, 5, {2, 3, 367}}
  {3251, 6, {2, 5, 13}}
  {3271, 3, {2, 3, 5, 109}}
  {3943, 3, {2, 3, 73}}
  {4259, 2, {2, 2129}}
  {4519, 3, {2, 3, 251}}
  {4801, 7, {2, 3, 5}}
  {4817, 3, {2, 7, 43}}
  {5059, 2, {2, 3, 281}}
  {5233, 10, {2, 3, 109}}
  {6011, 2, {2, 5, 601}}
  {6029, 2, {2, 11, 137}}
  {7937, 3, {2, 31}}
  {8461, 6, {2, 3, 5, 47}}
  {8741, 2, {2, 5, 19, 23}}
  {10069, 2, {2, 3, 839}}
  {10781, 10, {2, 5, 7, 11}}
  {11617, 10, {2, 3, 11}}
  {11777, 3, {2, 23}}
  {13219, 3, {2, 3, 2203}}
  {20411, 6, {2, 5, 13, 157}}
  {25763, 5, {2, 11, 1171}}
  {28807, 11, {2, 3, 4801}}
  {30133, 5, {2, 3, 31}}
  {35023, 5, {2, 3, 13, 449}}
  {40277, 2, {2, 10069}}
  {45191, 11, {2, 5, 4519}}
  {84407, 5, {2, 7, 6029}}
  {86249, 3, {2, 10781}}
  {176201, 6, {2, 5, 881}}
  {180799, 21, {2, 3, 30133}}
  {210139, 10, {2, 3, 35023}}
  {212923, 3, {2, 3, 3943}}
  {249341, 2, {2, 5, 7, 13, 137}}
  {350677, 2, {2, 3, 17, 191}}
  {352403, 2, {2, 176201}}
  {396623, 5, {2, 61, 3251}}
  {542293, 2, {2, 3, 45191}}
  {589921, 11, {2, 3, 5, 1229}}
  {704807, 5, {2, 352403}}
  {920021, 3, {2, 5, 157, 293}}
  {2837741, 3, {2, 5, 23, 31, 199}}
  {3112331, 2, {2, 5, 13, 89, 269}}
  {15400183, 3, {2, 3, 7, 61, 6011}}
  {22701929, 3, {2, 2837741}}
  {31276283, 2, {2, 607, 25763}}
  {40391489, 3, {2, 457, 1381}}
  {61600733, 2, {2, 15400183}}
  {68248303, 7, {2, 3, 17, 383, 1747}}
  {88441439, 7, {2, 5059, 8741}}
  {109949893, 2, {2, 3, 13, 704807}}
  {161083613, 2, {2, 1973, 20411}}
  {195931763, 2, {2, 13, 19, 396623}}
  {1056462481, 29, {2, 3, 5, 37, 13219}}
  {7458868649, 3, {2, 7, 11, 71, 199, 857}}
  {13200511703, 5, {2, 7, 641, 210139}}
  {14917737299, 2, {2, 7458868649}}
  {16835504321, 3, {2, 5, 211, 249341}}
  {19461802343, 5, {2, 1459, 2039, 3271}}
  {96535658711, 14, {2, 5, 239, 40391489}}
  {166735574953, 7, {2, 3, 23, 557, 542293}}
  {754709471627, 2, {2, 11, 367, 11777, 7937}}
  {856319303093, 3, {2, 11, 19461802343}}
  {33536916362861, 2, {2, 5, 101, 151, 109949893}}
  {41835914247601, 17, {2, 3, 5, 11, 1056462481}}
  {51184406731973, 2, {2, 19, 367, 5233, 350677}}
  {5132211217498247, 5, {2, 7, 79, 28807, 161083613}}
  {8131809253228537, 5, {2, 3, 359, 4817, 195931763}}
  {100573763533812059, 2, {2, 7, 23, 163, 84407, 22701929}}
  {579919627931177411, 6, {2, 5, 71, 8461, 96535658711}}
  {2491720775491575139, 3,
    {2, 3, 7, 19, 61, 307, 166735574953}}
  {10163916980269616149, 2, {2, 3, 13, 131, 659, 754709471627}}
  {52856068572087867403, 2, {2, 3, 887, 589921, 16835504321}}
  {61103715085640312453, 2, {2, 37, 31276283, 13200511703}}
  {1015333458682019563399, 3,
    {2, 3, 13, 19, 23, 131, 331, 11617, 3112331}}
  {1565243214961520886947, 2, {2, 7, 11, 10163916980269616149}}
  {615467116782935078317613149, 2,
    {2, 3, 88441439, 579919627931177411}}
  {12053184052872121075016965213807, 5,
    {2, 3, 17, 68248303, 212923, 8131809253228537}}
  {15761351183449477214527581079861, 6,
    {2, 3, 5, 51184406731973, 5132211217498247}}
  {749550393984295722148648633509624127063, 3,
    {2, 3, 920021, 856319303093, 52856068572087867403}}
  {913520378031647627719628067438521435803, 3,
    {2, 3, 2491720775491575139, 61103715085640312453}}
  {185430166316437744381147685635450956186364344774618775987236932440497693888277,
    5, {2, 3, 37, 67, 86249, 61600733, 1565243214961520886947,
         749550393984295722148648633509624127063}}
  {211370681965313945919700505464502129825342085259834493668100047798606905530671,
    3, {2, 3, 5, 241, 1291, 40277, 615467116782935078317613149,
         913520378031647627719628067438521435803}}
  {12838306333613466081342206156413564928317847531272891268867950693768039860692780471261470864893925814981313129184529468512637147111897684113005751175960887,
    5, {2, 3, 7, 19, 1699, 4259, 180799, 100573763533812059,
         41835914247601, 15761351183449477214527581079861,
         185430166316437744381147685635450956186364344774618775987236932440497693888277}}
  {12941401691266935282755640351590197563239229277655726246109613956195402922911737425132415889814716917409772155696641574604392302302177068799538311778540171,
    6, {2, 5, 14917737299, 33536916362861,
         1015333458682019563399,
         12053184052872121075016965213807,
         211370681965313945919700505464502129825342085259834493668100047798606905530671}}
›
thm pkcs_1_primes

end