From 24179cc34cb98db1a73715b32753c8232facfb42 Mon Sep 17 00:00:00 2001 From: Tony Arcieri Date: Wed, 12 Feb 2025 11:53:23 -0700 Subject: [PATCH] Add proptests for `Signature` encoding Ensures encoded signatures can be round tripped successfully, i.e. encoded and then decoded again without errors or panics. --- Cargo.lock | 1 + ml-dsa/Cargo.toml | 1 + ml-dsa/src/hint.rs | 2 +- ml-dsa/src/lib.rs | 7 ++- .../tests/sig-encoding.proptest-regressions | 8 ++++ ml-dsa/tests/sig-encoding.rs | 46 +++++++++++++++++++ 6 files changed, 60 insertions(+), 5 deletions(-) create mode 100644 ml-dsa/tests/sig-encoding.proptest-regressions create mode 100644 ml-dsa/tests/sig-encoding.rs diff --git a/Cargo.lock b/Cargo.lock index c4f2d006..6667fa03 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -690,6 +690,7 @@ dependencies = [ "hybrid-array", "num-traits", "pkcs8", + "proptest", "rand", "rand_core", "serde", diff --git a/ml-dsa/Cargo.toml b/ml-dsa/Cargo.toml index ebecf487..4ab3515f 100644 --- a/ml-dsa/Cargo.toml +++ b/ml-dsa/Cargo.toml @@ -37,6 +37,7 @@ criterion = "0.5.1" hex = { version = "0.4.3", features = ["serde"] } hex-literal = "0.4.1" pkcs8 = { version = "=0.11.0-rc.1", features = ["pem"] } +proptest = "1" rand = "0.8.5" serde = { version = "1.0.215", features = ["derive"] } serde_json = "1.0.132" diff --git a/ml-dsa/src/hint.rs b/ml-dsa/src/hint.rs index df9f321e..c9bf06c5 100644 --- a/ml-dsa/src/hint.rs +++ b/ml-dsa/src/hint.rs @@ -33,7 +33,7 @@ fn use_hint(h: bool, r: Elem) -> Elem { } } -#[derive(Clone, PartialEq)] +#[derive(Clone, PartialEq, Debug)] pub struct Hint

(pub Array, P::K>) where P: SignatureParams; diff --git a/ml-dsa/src/lib.rs b/ml-dsa/src/lib.rs index 3efe91cf..077f4528 100644 --- a/ml-dsa/src/lib.rs +++ b/ml-dsa/src/lib.rs @@ -17,8 +17,7 @@ //! # Quickstart //! //! ``` -//! use ml_dsa::{MlDsa65, KeyGen}; -//! use signature::{Keypair, Signer, Verifier}; +//! use ml_dsa::{MlDsa65, KeyGen, signature::{Keypair, Signer, Verifier}}; //! //! let mut rng = rand::thread_rng(); //! let kp = MlDsa65::key_gen(&mut rng); @@ -86,10 +85,10 @@ use crate::util::B64; pub use crate::param::{EncodedSignature, EncodedSigningKey, EncodedVerifyingKey, MlDsaParams}; pub use crate::util::B32; -pub use signature::Error; +pub use signature::{self, Error}; /// An ML-DSA signature -#[derive(Clone, PartialEq)] +#[derive(Clone, PartialEq, Debug)] pub struct Signature { c_tilde: Array, z: Vector, diff --git a/ml-dsa/tests/sig-encoding.proptest-regressions b/ml-dsa/tests/sig-encoding.proptest-regressions new file mode 100644 index 00000000..ac22ac50 --- /dev/null +++ b/ml-dsa/tests/sig-encoding.proptest-regressions @@ -0,0 +1,8 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc ac6ac164887b286d32343863bf9bf242a73cf2f49b1cade341e42431c8fe1c0a # shrinks to sig = Signature { c_tilde: Array([74, 138, 221, 44, 116, 0, 0, 100, 202, 216, 99, 212, 48, 128, 207, 91, 75, 221, 59, 103, 130, 193, 167, 250, 248, 152, 240, 174, 64, 25, 199, 54, 229, 68, 228, 220, 191, 38, 175, 33, 6, 75, 231, 127, 162, 200, 32, 66]), z: Vector(Array([Polynomial(Array([Elem(7976457), Elem(340810), Elem(8350609), Elem(368022), Elem(160149), Elem(8246946), Elem(265593), Elem(484829), Elem(180754), Elem(308625), Elem(8063854), Elem(8339120), Elem(202009), Elem(8241758), Elem(8335989), Elem(7878017), Elem(8072), Elem(206442), Elem(35206), Elem(429846), Elem(291869), Elem(8205024), Elem(271604), Elem(7960658), Elem(90), Elem(308067), Elem(1273), Elem(421696), Elem(8082260), Elem(313900), Elem(8000793), Elem(7949789), Elem(156247), Elem(8222610), Elem(8291733), Elem(98332), Elem(8248268), Elem(27178), Elem(361673), Elem(8328957), Elem(387894), Elem(8167517), Elem(58975), Elem(8336669), Elem(8187293), Elem(7988216), Elem(8155288), Elem(8122752), Elem(8098797), Elem(8053190), Elem(8241438), Elem(461866), Elem(381179), Elem(440359), Elem(8037999), Elem(8246943), Elem(8100889), Elem(7856679), Elem(8317333), Elem(7945386), Elem(8366736), Elem(313517), Elem(436962), Elem(8340220), Elem(133005), Elem(8351392), Elem(198397), Elem(359237), Elem(283600), Elem(7934254), Elem(82715), Elem(342524), Elem(141236), Elem(7959839), Elem(208840), Elem(8160689), Elem(8003726), Elem(8178519), Elem(220091), Elem(8332681), Elem(290878), Elem(359890), Elem(517998), Elem(296410), Elem(8377848), Elem(294372), Elem(411452), Elem(8075767), Elem(8251681), Elem(183214), Elem(440836), Elem(7932002), Elem(489312), Elem(7949140), Elem(8224967), Elem(35877), Elem(7900798), Elem(8146766), Elem(419000), Elem(8003495), Elem(8168735), Elem(7892784), Elem(7946834), Elem(391753), Elem(227488), Elem(8186937), Elem(8062374), Elem(7919195), Elem(7949906), Elem(8170764), Elem(174705), Elem(197202), Elem(8095187), Elem(8184562), Elem(321932), Elem(440336), Elem(7865131), Elem(8351100), Elem(387037), Elem(298350), Elem(7888303), Elem(405636), Elem(8198961), Elem(125417), Elem(7900247), Elem(436190), Elem(8127621), Elem(516820), Elem(8313567), Elem(8118838), Elem(8024834), Elem(262376), Elem(8240179), Elem(8038374), Elem(165693), Elem(66387), Elem(8322812), Elem(8196689), Elem(7949528), Elem(8069154), Elem(8301452), Elem(8143974), Elem(29986), Elem(8155048), Elem(92905), Elem(324797), Elem(424817), Elem(8102323), Elem(7975625), Elem(225870), Elem(8131889), Elem(7877064), Elem(7943530), Elem(449888), Elem(8200233), Elem(365308), Elem(44507), Elem(8053110), Elem(459278), Elem(198499), Elem(7907246), Elem(92557), Elem(359618), Elem(8078017), Elem(8323398), Elem(342583), Elem(480438), Elem(8086650), Elem(8321722), Elem(430985), Elem(476012), Elem(8233536), Elem(7932211), Elem(245171), Elem(89697), Elem(8278181), Elem(7882285), Elem(126356), Elem(298673), Elem(8220110), Elem(8019427), Elem(258699), Elem(8227988), Elem(8062132), Elem(8158130), Elem(8043045), Elem(7958475), Elem(8314830), Elem(8334608), Elem(8145779), Elem(8260702), Elem(8214651), Elem(8231331), Elem(310425), Elem(348629), Elem(8292200), Elem(57276), Elem(246357), Elem(8040270), Elem(100290), Elem(8025135), Elem(8270328), Elem(515938), Elem(8287026), Elem(482842), Elem(8141158), Elem(202679), Elem(249444), Elem(8188008), Elem(136958), Elem(8361267), Elem(8215802), Elem(317041), Elem(512966), Elem(7932849), Elem(8131793), Elem(8180968), Elem(221672), Elem(318691), Elem(497624), Elem(336047), Elem(235296), Elem(198345), Elem(8141740), Elem(309460), Elem(8323567), Elem(8316977), Elem(8059091), Elem(520550), Elem(12650), Elem(475706), Elem(8343400), Elem(125114), Elem(115392), Elem(122440), Elem(7907867), Elem(270353), Elem(7874116), Elem(7886031), Elem(357917), Elem(8378703), Elem(8251028), Elem(364976), Elem(8256183), Elem(176193), Elem(8284784), Elem(478081), Elem(8029233), Elem(418900), Elem(362487), Elem(8167304), Elem(494141), Elem(7921672), Elem(8292637), Elem(8268576), Elem(8116500)])), Polynomial(Array([Elem(80799), Elem(7941448), Elem(37868), Elem(7909299), Elem(8087634), Elem(8306920), Elem(8175465), Elem(8331079), Elem(349289), Elem(8349724), Elem(8229849), Elem(8190627), Elem(309957), Elem(7918542), Elem(331311), Elem(8064711), Elem(7937865), Elem(363448), Elem(98935), Elem(357208), Elem(8859), Elem(48904), Elem(373139), Elem(100628), Elem(8312930), Elem(7961586), Elem(414834), Elem(209209), Elem(8006142), Elem(7880533), Elem(8327921), Elem(1548), Elem(7977362), Elem(8296508), Elem(328650), Elem(384266), Elem(333911), Elem(8159730), Elem(8124998), Elem(432237), Elem(8292214), Elem(8135473), Elem(182213), Elem(7884242), Elem(435014), Elem(7920092), Elem(320327), Elem(393197), Elem(8214807), Elem(8068404), Elem(159336), Elem(8299240), Elem(7968770), Elem(57370), Elem(8315506), Elem(8019469), Elem(8254047), Elem(28663), Elem(7953216), Elem(8085115), Elem(7940199), Elem(7983692), Elem(495913), Elem(67254), Elem(8018436), Elem(8044162), Elem(7498), Elem(13107), Elem(8011805), Elem(318678), Elem(8265035), Elem(8376301), Elem(291063), Elem(8273661), Elem(80985), Elem(7948272), Elem(7885776), Elem(8344490), Elem(434270), Elem(11489), Elem(213453), Elem(395759), Elem(350921), Elem(7937276), Elem(7944269), Elem(300161), Elem(358219), Elem(8154223), Elem(522150), Elem(7947289), Elem(114056), Elem(8019221), Elem(7956681), Elem(301562), Elem(273491), Elem(188720), Elem(7942516), Elem(56159), Elem(339273), Elem(8088007), Elem(8120531), Elem(8253285), Elem(8247736), Elem(8016326), Elem(8078092), Elem(476802), Elem(8285938), Elem(7970028), Elem(91236), Elem(7965965), Elem(308679), Elem(506195), Elem(8030740), Elem(8336405), Elem(205967), Elem(260212), Elem(7979743), Elem(114638), Elem(254253), Elem(8371885), Elem(503734), Elem(8172347), Elem(278880), Elem(8144672), Elem(272715), Elem(150083), Elem(49386), Elem(478644), Elem(361015), Elem(8375013), Elem(180776), Elem(94637), Elem(142465), Elem(8025916), Elem(162562), Elem(164018), Elem(8077031), Elem(8065329), Elem(8303684), Elem(7966065), Elem(47544), Elem(8193774), Elem(8150352), Elem(8192725), Elem(7893740), Elem(8373374), Elem(8062832), Elem(8136512), Elem(49261), Elem(441330), Elem(7960604), Elem(205110), Elem(262563), Elem(21418), Elem(468197), Elem(421809), Elem(399919), Elem(59867), Elem(484654), Elem(8262517), Elem(8087148), Elem(93171), Elem(14950), Elem(410164), Elem(371445), Elem(8175378), Elem(8103478), Elem(8128092), Elem(489571), Elem(7969208), Elem(8275089), Elem(7997675), Elem(8311102), Elem(8081871), Elem(8364897), Elem(455569), Elem(258372), Elem(84457), Elem(8060177), Elem(8241521), Elem(7925110), Elem(514829), Elem(334095), Elem(7897422), Elem(8039703), Elem(222226), Elem(304267), Elem(7927735), Elem(8188101), Elem(144926), Elem(376724), Elem(368218), Elem(92245), Elem(8086381), Elem(8269121), Elem(8213744), Elem(8199728), Elem(34298), Elem(8057495), Elem(292126), Elem(8088996), Elem(7998775), Elem(7890125), Elem(4789), Elem(8124248), Elem(54152), Elem(8360583), Elem(21854), Elem(8053490), Elem(8294653), Elem(8154360), Elem(7963070), Elem(309628), Elem(435764), Elem(415201), Elem(8092310), Elem(8301520), Elem(523153), Elem(8193361), Elem(247506), Elem(407104), Elem(7947759), Elem(8073193), Elem(8128346), Elem(8307721), Elem(7878360), Elem(8024720), Elem(8337626), Elem(171708), Elem(7980152), Elem(455622), Elem(122098), Elem(258413), Elem(21450), Elem(8151102), Elem(7997406), Elem(8274093), Elem(7919584), Elem(122923), Elem(373955), Elem(8024409), Elem(5790), Elem(27582), Elem(8099445), Elem(8210823), Elem(8196487), Elem(8269130), Elem(270643), Elem(7907081), Elem(8093935), Elem(404567), Elem(69099), Elem(435278), Elem(48893), Elem(8109962), Elem(512469)])), Polynomial(Array([Elem(8049350), Elem(510887), Elem(235181), Elem(293449), Elem(8196769), Elem(307198), Elem(133735), Elem(8058934), Elem(8039996), Elem(8202378), Elem(8270599), Elem(198534), Elem(7902360), Elem(8137537), Elem(419319), Elem(8355069), Elem(163271), Elem(8157519), Elem(8272611), Elem(8013310), Elem(8243032), Elem(63567), Elem(426128), Elem(375214), Elem(7950530), Elem(8100212), Elem(8017127), Elem(8064550), Elem(101722), Elem(8341595), Elem(121998), Elem(8027629), Elem(168627), Elem(483362), Elem(8244540), Elem(138815), Elem(186925), Elem(8065350), Elem(188333), Elem(7882383), Elem(304979), Elem(7933562), Elem(8057963), Elem(8114676), Elem(207914), Elem(8081292), Elem(361452), Elem(79320), Elem(8363737), Elem(182821), Elem(513863), Elem(8122557), Elem(7967939), Elem(343302), Elem(301770), Elem(7987822), Elem(192701), Elem(8205875), Elem(430956), Elem(8316281), Elem(1326), Elem(85056), Elem(210241), Elem(339593), Elem(8258745), Elem(517746), Elem(251264), Elem(7942474), Elem(8233162), Elem(165545), Elem(8090521), Elem(7976448), Elem(8346315), Elem(160341), Elem(491285), Elem(7977894), Elem(7964657), Elem(8165752), Elem(8068530), Elem(8043833), Elem(8363584), Elem(244701), Elem(7883093), Elem(38119), Elem(155213), Elem(385990), Elem(250840), Elem(7941259), Elem(8229269), Elem(91245), Elem(151727), Elem(195791), Elem(7898416), Elem(7914256), Elem(8001699), Elem(8061221), Elem(7865370), Elem(238072), Elem(8150993), Elem(517160), Elem(8128354), Elem(246201), Elem(8262668), Elem(7870260), Elem(8243377), Elem(8107046), Elem(8371549), Elem(7877849), Elem(238028), Elem(128663), Elem(7857971), Elem(8186363), Elem(223467), Elem(7870497), Elem(256300), Elem(8117285), Elem(8294054), Elem(8069755), Elem(7999018), Elem(311689), Elem(254295), Elem(8016749), Elem(27669), Elem(7990659), Elem(7983889), Elem(19044), Elem(1394), Elem(74765), Elem(8207863), Elem(8222302), Elem(8177126), Elem(260525), Elem(7870477), Elem(8115806), Elem(7942539), Elem(217095), Elem(442744), Elem(95814), Elem(121156), Elem(8166592), Elem(8295571), Elem(255705), Elem(7931750), Elem(152222), Elem(487498), Elem(248035), Elem(288507), Elem(16753), Elem(19623), Elem(93532), Elem(149726), Elem(57303), Elem(8916), Elem(448037), Elem(488486), Elem(8130599), Elem(429112), Elem(7958178), Elem(8306309), Elem(466739), Elem(8199717), Elem(88823), Elem(500048), Elem(8263063), Elem(69530), Elem(8356531), Elem(397073), Elem(8174662), Elem(508839), Elem(391074), Elem(8141340), Elem(8371793), Elem(50354), Elem(8054657), Elem(447261), Elem(242202), Elem(8277827), Elem(318910), Elem(8117523), Elem(7890821), Elem(29445), Elem(340688), Elem(92952), Elem(8129746), Elem(298920), Elem(8131770), Elem(37824), Elem(8182303), Elem(419622), Elem(8148567), Elem(367749), Elem(8201220), Elem(111755), Elem(127474), Elem(8027834), Elem(103534), Elem(8156989), Elem(7861264), Elem(7945335), Elem(200147), Elem(7947679), Elem(251753), Elem(452916), Elem(369251), Elem(8314450), Elem(256454), Elem(8330263), Elem(7891850), Elem(265582), Elem(7963550), Elem(45490), Elem(458314), Elem(104360), Elem(8217764), Elem(8116598), Elem(65163), Elem(8168748), Elem(310716), Elem(8375737), Elem(325940), Elem(183132), Elem(8164853), Elem(155123), Elem(236368), Elem(70559), Elem(43129), Elem(8074914), Elem(8354154), Elem(109622), Elem(8251837), Elem(7860955), Elem(504423), Elem(50025), Elem(8180195), Elem(7970345), Elem(8026500), Elem(8124472), Elem(245269), Elem(8343588), Elem(7913067), Elem(8206759), Elem(8228048), Elem(7944584), Elem(7952941), Elem(8306040), Elem(8116368), Elem(8244878), Elem(7891744), Elem(8316763), Elem(231206), Elem(362254), Elem(8374896), Elem(7903817), Elem(8122084), Elem(8108663), Elem(449060)])), Polynomial(Array([Elem(8047676), Elem(8148146), Elem(8197643), Elem(88396), Elem(72599), Elem(7959274), Elem(8204396), Elem(8228338), Elem(8152804), Elem(8061687), Elem(343607), Elem(516079), Elem(8195409), Elem(8214005), Elem(316794), Elem(8266551), Elem(235998), Elem(62226), Elem(303696), Elem(8296491), Elem(8133444), Elem(8175931), Elem(208216), Elem(335806), Elem(8124714), Elem(7949135), Elem(8345810), Elem(460537), Elem(82888), Elem(189488), Elem(7950497), Elem(8081010), Elem(217785), Elem(461585), Elem(8299759), Elem(8218965), Elem(519575), Elem(369440), Elem(7883878), Elem(8188258), Elem(175758), Elem(8320726), Elem(8344180), Elem(220573), Elem(432928), Elem(323402), Elem(269341), Elem(8103247), Elem(8203652), Elem(32297), Elem(8319793), Elem(8134172), Elem(8213435), Elem(8196230), Elem(156788), Elem(7890836), Elem(246683), Elem(469078), Elem(8203939), Elem(8206363), Elem(206517), Elem(317435), Elem(8318843), Elem(7976586), Elem(450236), Elem(8071967), Elem(8126531), Elem(8139620), Elem(8378521), Elem(7988027), Elem(8155146), Elem(7977509), Elem(8054877), Elem(264414), Elem(113750), Elem(8009600), Elem(7969803), Elem(7862256), Elem(59108), Elem(78875), Elem(8122167), Elem(241666), Elem(432831), Elem(8248143), Elem(423949), Elem(43982), Elem(7911313), Elem(100453), Elem(48008), Elem(7937732), Elem(8243338), Elem(8214236), Elem(8098693), Elem(130008), Elem(8328209), Elem(274673), Elem(199123), Elem(239069), Elem(243023), Elem(8076609), Elem(8325585), Elem(309018), Elem(54516), Elem(369480), Elem(48957), Elem(249768), Elem(7887339), Elem(129104), Elem(391802), Elem(8305640), Elem(7913248), Elem(8272730), Elem(5854), Elem(8085113), Elem(8332891), Elem(8376731), Elem(8243352), Elem(214955), Elem(8251751), Elem(144761), Elem(8273535), Elem(8226311), Elem(8365665), Elem(8169109), Elem(8182688), Elem(402019), Elem(138575), Elem(8177570), Elem(413748), Elem(7892582), Elem(208376), Elem(7977826), Elem(8296532), Elem(102523), Elem(7993985), Elem(8069393), Elem(8274798), Elem(305479), Elem(459635), Elem(109188), Elem(8059828), Elem(405843), Elem(295101), Elem(264047), Elem(8288294), Elem(354618), Elem(465265), Elem(431229), Elem(7963368), Elem(30015), Elem(361465), Elem(8024771), Elem(155661), Elem(269789), Elem(179244), Elem(7891520), Elem(469703), Elem(79369), Elem(8006203), Elem(8109603), Elem(40581), Elem(8313506), Elem(482761), Elem(504101), Elem(462594), Elem(114899), Elem(150351), Elem(28087), Elem(11852), Elem(65374), Elem(8353061), Elem(8030666), Elem(248747), Elem(7988540), Elem(199161), Elem(118353), Elem(218145), Elem(102706), Elem(10907), Elem(8289466), Elem(181935), Elem(8239288), Elem(240907), Elem(34543), Elem(351912), Elem(222272), Elem(90729), Elem(488603), Elem(324303), Elem(268270), Elem(7946994), Elem(42628), Elem(8151326), Elem(168834), Elem(7938672), Elem(157425), Elem(332788), Elem(177989), Elem(8350549), Elem(7937508), Elem(8217586), Elem(7950942), Elem(233004), Elem(30849), Elem(439419), Elem(260617), Elem(8064696), Elem(39697), Elem(296122), Elem(190755), Elem(7900775), Elem(94765), Elem(7949244), Elem(8122147), Elem(8025717), Elem(279370), Elem(329992), Elem(508950), Elem(95723), Elem(233498), Elem(8227770), Elem(158856), Elem(303529), Elem(8282133), Elem(214246), Elem(264832), Elem(15113), Elem(483955), Elem(182240), Elem(8217015), Elem(297791), Elem(188057), Elem(7899147), Elem(69366), Elem(8065374), Elem(8354871), Elem(8278622), Elem(7878542), Elem(254067), Elem(8117219), Elem(7980696), Elem(300399), Elem(8225046), Elem(255114), Elem(8318124), Elem(510689), Elem(7944854), Elem(8022485), Elem(8216991), Elem(8009048), Elem(8077155), Elem(7984079), Elem(8156831), Elem(323339), Elem(7983212), Elem(8286848)])), Polynomial(Array([Elem(8169019), Elem(270126), Elem(8379225), Elem(8180733), Elem(8174240), Elem(196600), Elem(408932), Elem(110615), Elem(8219798), Elem(85437), Elem(132343), Elem(8123816), Elem(9319), Elem(111523), Elem(148090), Elem(8051534), Elem(8095988), Elem(8015786), Elem(8142757), Elem(7869285), Elem(392682), Elem(7927933), Elem(396861), Elem(402631), Elem(8288920), Elem(173545), Elem(24386), Elem(8205), Elem(162166), Elem(8101459), Elem(376650), Elem(295931), Elem(19622), Elem(8269288), Elem(516367), Elem(8323142), Elem(7984601), Elem(292445), Elem(221256), Elem(490471), Elem(8179016), Elem(6514), Elem(7973154), Elem(380289), Elem(314221), Elem(8198437), Elem(187351), Elem(8217170), Elem(8298952), Elem(8324216), Elem(434), Elem(7883260), Elem(126297), Elem(50079), Elem(386405), Elem(366896), Elem(8236408), Elem(472543), Elem(8356665), Elem(7921794), Elem(85736), Elem(318422), Elem(160024), Elem(8158274), Elem(403131), Elem(8203536), Elem(8276904), Elem(151384), Elem(7866232), Elem(8089943), Elem(127711), Elem(8326236), Elem(292655), Elem(307465), Elem(7873109), Elem(495287), Elem(8274361), Elem(8056195), Elem(7883008), Elem(389847), Elem(370774), Elem(96876), Elem(8341860), Elem(346678), Elem(8059144), Elem(8037812), Elem(8366116), Elem(7941464), Elem(103457), Elem(7919918), Elem(177963), Elem(7881275), Elem(66946), Elem(391169), Elem(8240908), Elem(8315472), Elem(47376), Elem(238788), Elem(8256367), Elem(131471), Elem(288644), Elem(433590), Elem(497736), Elem(303187), Elem(51919), Elem(152895), Elem(459023), Elem(385236), Elem(7920405), Elem(8321410), Elem(357040), Elem(241247), Elem(8025087), Elem(450418), Elem(65651), Elem(368829), Elem(8320627), Elem(186578), Elem(8361021), Elem(8223550), Elem(7864871), Elem(7938388), Elem(8131964), Elem(175825), Elem(109045), Elem(393833), Elem(8337340), Elem(419070), Elem(121421), Elem(140417), Elem(8304496), Elem(189404), Elem(196745), Elem(473770), Elem(368344), Elem(7989977), Elem(8317451), Elem(297578), Elem(8201409), Elem(8094103), Elem(294530), Elem(8220222), Elem(7922189), Elem(7929415), Elem(8184411), Elem(433576), Elem(247636), Elem(116442), Elem(5207), Elem(7948757), Elem(205916), Elem(320892), Elem(359606), Elem(8233057), Elem(8134620), Elem(289851), Elem(444061), Elem(137078), Elem(478661), Elem(8357177), Elem(146836), Elem(8311676), Elem(68527), Elem(516223), Elem(184444), Elem(8195290), Elem(7966529), Elem(8321734), Elem(434386), Elem(8177876), Elem(7860418), Elem(7918701), Elem(8299359), Elem(8083742), Elem(8331679), Elem(8356958), Elem(171089), Elem(8231839), Elem(317008), Elem(8017936), Elem(7933092), Elem(384991), Elem(31162), Elem(292075), Elem(246367), Elem(411816), Elem(8056361), Elem(8361169), Elem(8038654), Elem(8209131), Elem(170579), Elem(8201475), Elem(248838), Elem(30721), Elem(172205), Elem(374160), Elem(7920166), Elem(8200250), Elem(388897), Elem(8141202), Elem(200), Elem(8243366), Elem(152457), Elem(484889), Elem(7896649), Elem(32525), Elem(8264285), Elem(8105230), Elem(148909), Elem(101135), Elem(286991), Elem(8361697), Elem(7880096), Elem(55208), Elem(337488), Elem(8264392), Elem(441999), Elem(8128984), Elem(62570), Elem(188573), Elem(8251356), Elem(377191), Elem(8270386), Elem(318804), Elem(7879379), Elem(190766), Elem(242229), Elem(7877194), Elem(8363043), Elem(8247683), Elem(114320), Elem(332365), Elem(7894836), Elem(7935748), Elem(405406), Elem(258354), Elem(237931), Elem(236449), Elem(175555), Elem(8300437), Elem(8252742), Elem(8040144), Elem(298009), Elem(85755), Elem(7978618), Elem(7931818), Elem(124865), Elem(112660), Elem(8210164), Elem(233292), Elem(252389), Elem(8115), Elem(8118002), Elem(8366389), Elem(8338230), Elem(245222)]))])), h: Hint(Array([Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, true, false, false, false, false, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, true, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, true]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false])])) } +cc 379a3f932cf961b16a2935a79b7bc422ed98e796655805bbb19be1f686e826dd # shrinks to sig = Signature { c_tilde: Array([88, 60, 221, 48, 27, 83, 254, 234, 40, 99, 217, 25, 44, 212, 55, 182, 196, 149, 189, 56, 210, 248, 85, 239, 11, 216, 45, 31, 14, 181, 64, 73, 71, 202, 64, 163, 98, 246, 154, 142, 133, 129, 46, 65, 30, 64, 165, 54, 159, 233, 43, 109, 158, 21, 105, 52, 35, 252, 133, 15, 207, 182, 200, 67]), z: Vector(Array([Polynomial(Array([Elem(8270926), Elem(8313647), Elem(89286), Elem(265706), Elem(474135), Elem(51069), Elem(289599), Elem(68435), Elem(8063206), Elem(363537), Elem(209895), Elem(7875315), Elem(517305), Elem(8064757), Elem(356057), Elem(429211), Elem(221469), Elem(8097365), Elem(122600), Elem(207423), Elem(512875), Elem(57073), Elem(7963384), Elem(509565), Elem(340330), Elem(477534), Elem(438585), Elem(297650), Elem(466024), Elem(8199066), Elem(93220), Elem(8058921), Elem(86914), Elem(7926588), Elem(7886692), Elem(147968), Elem(8085488), Elem(433367), Elem(390569), Elem(446426), Elem(8257438), Elem(403612), Elem(8355551), Elem(7933854), Elem(8326004), Elem(228169), Elem(56329), Elem(147070), Elem(213720), Elem(8065029), Elem(8250096), Elem(148742), Elem(8171787), Elem(7930155), Elem(8229327), Elem(125910), Elem(412303), Elem(340714), Elem(7914416), Elem(384353), Elem(219490), Elem(35657), Elem(8176033), Elem(280602), Elem(178178), Elem(8307030), Elem(8002881), Elem(8304079), Elem(11549), Elem(172235), Elem(343464), Elem(450535), Elem(40164), Elem(8277160), Elem(8360720), Elem(272771), Elem(8181026), Elem(286472), Elem(8313716), Elem(8180868), Elem(321855), Elem(481020), Elem(465915), Elem(198284), Elem(8263137), Elem(430291), Elem(8219802), Elem(7950858), Elem(237342), Elem(8369738), Elem(445102), Elem(258468), Elem(8214250), Elem(8078316), Elem(8368282), Elem(506651), Elem(7909261), Elem(8331757), Elem(8031664), Elem(152207), Elem(8127146), Elem(8032394), Elem(7877972), Elem(8309841), Elem(8014236), Elem(511092), Elem(111666), Elem(356403), Elem(8262122), Elem(164138), Elem(7934918), Elem(8210290), Elem(8212339), Elem(8305369), Elem(8266761), Elem(135966), Elem(8269142), Elem(523713), Elem(276725), Elem(8204974), Elem(411013), Elem(194534), Elem(8023581), Elem(8026246), Elem(162596), Elem(8197525), Elem(8214842), Elem(68153), Elem(8250230), Elem(8062898), Elem(416763), Elem(8356946), Elem(91951), Elem(411614), Elem(8009777), Elem(7887123), Elem(439671), Elem(7954805), Elem(8196775), Elem(80066), Elem(8126269), Elem(8352689), Elem(240015), Elem(8232403), Elem(7913526), Elem(8178831), Elem(412527), Elem(246805), Elem(487582), Elem(146958), Elem(112715), Elem(8004288), Elem(8349767), Elem(8278708), Elem(8160357), Elem(386894), Elem(8268038), Elem(174265), Elem(7953505), Elem(138430), Elem(8343059), Elem(479955), Elem(8064140), Elem(8097433), Elem(8336478), Elem(192074), Elem(321222), Elem(238292), Elem(8144516), Elem(480505), Elem(41743), Elem(8274760), Elem(469333), Elem(7881224), Elem(480507), Elem(242357), Elem(8237806), Elem(78135), Elem(8082717), Elem(8211849), Elem(478117), Elem(7932154), Elem(8231974), Elem(8212441), Elem(8048637), Elem(459978), Elem(463380), Elem(8378029), Elem(8313261), Elem(128137), Elem(319055), Elem(445813), Elem(8368229), Elem(315734), Elem(7891390), Elem(7915880), Elem(8164122), Elem(506704), Elem(8264136), Elem(339675), Elem(7865472), Elem(238179), Elem(8219287), Elem(63930), Elem(7888633), Elem(65448), Elem(8324345), Elem(8357805), Elem(122028), Elem(195217), Elem(304803), Elem(185101), Elem(876), Elem(8172889), Elem(8164221), Elem(407218), Elem(8288810), Elem(8185363), Elem(508349), Elem(8355107), Elem(7998427), Elem(8250045), Elem(8376149), Elem(157239), Elem(418597), Elem(7990511), Elem(7891572), Elem(8299227), Elem(8198028), Elem(515956), Elem(7997522), Elem(8301817), Elem(15474), Elem(273065), Elem(7878470), Elem(7881313), Elem(8217292), Elem(7966658), Elem(8132281), Elem(8183366), Elem(44412), Elem(8001916), Elem(524001), Elem(8094638), Elem(8103061), Elem(497228), Elem(350243), Elem(7922761), Elem(7932871), Elem(489266), Elem(196359), Elem(204071), Elem(8111379), Elem(118738), Elem(8066268), Elem(8235910)])), Polynomial(Array([Elem(9687), Elem(119161), Elem(59196), Elem(497459), Elem(8303601), Elem(7928713), Elem(365553), Elem(65219), Elem(358129), Elem(7976691), Elem(8227529), Elem(7957083), Elem(7906886), Elem(371921), Elem(7920095), Elem(222139), Elem(8197884), Elem(8070395), Elem(296836), Elem(147949), Elem(8186532), Elem(271548), Elem(8163186), Elem(364083), Elem(8029974), Elem(178663), Elem(179356), Elem(8021678), Elem(7876389), Elem(8226956), Elem(8341395), Elem(7992500), Elem(330318), Elem(7876924), Elem(60355), Elem(8110870), Elem(4810), Elem(91689), Elem(7939248), Elem(8055511), Elem(513701), Elem(8176807), Elem(481585), Elem(273333), Elem(215689), Elem(8158012), Elem(8051887), Elem(388826), Elem(8141245), Elem(8233358), Elem(71822), Elem(8091062), Elem(83572), Elem(8211938), Elem(8316202), Elem(487233), Elem(7969059), Elem(165483), Elem(7886516), Elem(8346849), Elem(7873743), Elem(341984), Elem(8076002), Elem(49047), Elem(8212731), Elem(7884180), Elem(246197), Elem(8078568), Elem(202240), Elem(321372), Elem(208753), Elem(8351071), Elem(407241), Elem(228304), Elem(229626), Elem(8266466), Elem(7896462), Elem(8028593), Elem(284801), Elem(6874), Elem(8357548), Elem(8163113), Elem(8022173), Elem(8149258), Elem(77114), Elem(155653), Elem(8137285), Elem(8218562), Elem(442652), Elem(6309), Elem(169296), Elem(8079243), Elem(273051), Elem(391634), Elem(225719), Elem(8253414), Elem(8167886), Elem(7977416), Elem(66736), Elem(60595), Elem(484597), Elem(7891028), Elem(31597), Elem(190278), Elem(509299), Elem(8006975), Elem(8151883), Elem(7929158), Elem(7944983), Elem(347469), Elem(356148), Elem(362451), Elem(393851), Elem(246176), Elem(10473), Elem(7991911), Elem(156144), Elem(196298), Elem(8051233), Elem(468252), Elem(295975), Elem(388076), Elem(439099), Elem(7864129), Elem(8161518), Elem(7865402), Elem(416600), Elem(12941), Elem(185732), Elem(202203), Elem(370436), Elem(7891331), Elem(7986249), Elem(8190653), Elem(7881949), Elem(27673), Elem(214098), Elem(8032565), Elem(8192131), Elem(8271894), Elem(421360), Elem(8112883), Elem(513790), Elem(291464), Elem(8062102), Elem(332185), Elem(8249674), Elem(8006649), Elem(8114642), Elem(8175442), Elem(483166), Elem(7979808), Elem(281668), Elem(329744), Elem(111467), Elem(8182383), Elem(7909133), Elem(8003633), Elem(7869995), Elem(8057511), Elem(230917), Elem(8184295), Elem(7898756), Elem(7721), Elem(8073422), Elem(8160756), Elem(81785), Elem(291071), Elem(137188), Elem(7952015), Elem(7903377), Elem(452747), Elem(7857300), Elem(8000869), Elem(294563), Elem(417242), Elem(315290), Elem(256350), Elem(241407), Elem(3227), Elem(509575), Elem(274543), Elem(148205), Elem(8152542), Elem(282643), Elem(96379), Elem(8337843), Elem(8271028), Elem(160508), Elem(7928504), Elem(8202034), Elem(8000439), Elem(7985975), Elem(8327662), Elem(7895800), Elem(8185544), Elem(232828), Elem(140143), Elem(8152164), Elem(8066007), Elem(8220014), Elem(26035), Elem(7897455), Elem(8123204), Elem(471563), Elem(250235), Elem(8341982), Elem(8056067), Elem(8223163), Elem(494602), Elem(479469), Elem(147806), Elem(8259443), Elem(7862485), Elem(8173957), Elem(8010), Elem(8322290), Elem(462796), Elem(409138), Elem(458805), Elem(8180024), Elem(8295238), Elem(512888), Elem(8204525), Elem(7900183), Elem(8193773), Elem(8060263), Elem(8195992), Elem(81883), Elem(7887706), Elem(7938156), Elem(8183672), Elem(8372659), Elem(7972394), Elem(8193229), Elem(7944481), Elem(301928), Elem(8146144), Elem(76585), Elem(121301), Elem(405221), Elem(7884838), Elem(7974485), Elem(266805), Elem(179638), Elem(77422), Elem(156652), Elem(313781), Elem(7995665), Elem(7898625), Elem(66442), Elem(8191574), Elem(8014721), Elem(7981555), Elem(7980754), Elem(7963392)])), Polynomial(Array([Elem(114542), Elem(8215096), Elem(422523), Elem(8283557), Elem(8037892), Elem(50376), Elem(359570), Elem(131437), Elem(399343), Elem(8321764), Elem(473312), Elem(188289), Elem(8093561), Elem(486063), Elem(8306479), Elem(51822), Elem(8189289), Elem(123201), Elem(8012264), Elem(379378), Elem(190967), Elem(444538), Elem(493848), Elem(443872), Elem(8243315), Elem(8318968), Elem(322797), Elem(231354), Elem(339879), Elem(316770), Elem(8036132), Elem(242502), Elem(444698), Elem(417530), Elem(434816), Elem(8077817), Elem(7959368), Elem(8064502), Elem(7886590), Elem(8097865), Elem(8325040), Elem(8194610), Elem(8318045), Elem(239839), Elem(8287283), Elem(226822), Elem(471942), Elem(8116773), Elem(414889), Elem(169947), Elem(7969109), Elem(440992), Elem(56294), Elem(7858627), Elem(43358), Elem(7922305), Elem(346648), Elem(21120), Elem(8165445), Elem(7924807), Elem(8250245), Elem(7872610), Elem(8319123), Elem(7930273), Elem(8059285), Elem(256337), Elem(8209220), Elem(121160), Elem(235373), Elem(8140665), Elem(102516), Elem(506881), Elem(329987), Elem(126392), Elem(113890), Elem(8178013), Elem(8353605), Elem(492279), Elem(7978038), Elem(123012), Elem(7957353), Elem(214118), Elem(8228407), Elem(7942620), Elem(8131933), Elem(8309866), Elem(212031), Elem(7905883), Elem(376639), Elem(8305417), Elem(8310204), Elem(140911), Elem(8231075), Elem(21622), Elem(7966296), Elem(8059267), Elem(191103), Elem(8122809), Elem(517065), Elem(495307), Elem(457890), Elem(8239212), Elem(522060), Elem(489571), Elem(8155316), Elem(8025377), Elem(7895782), Elem(457017), Elem(403598), Elem(211037), Elem(47613), Elem(457298), Elem(8220629), Elem(7923885), Elem(372947), Elem(505070), Elem(335986), Elem(94489), Elem(7934661), Elem(8202721), Elem(7998893), Elem(8233390), Elem(196503), Elem(103410), Elem(8312230), Elem(8148395), Elem(32914), Elem(8281665), Elem(7912813), Elem(114673), Elem(7983514), Elem(8021593), Elem(8161720), Elem(109633), Elem(8365504), Elem(8194563), Elem(235832), Elem(8285877), Elem(7957043), Elem(8130976), Elem(199183), Elem(438733), Elem(441060), Elem(298467), Elem(422208), Elem(8185067), Elem(484116), Elem(8279937), Elem(8152161), Elem(7864765), Elem(406192), Elem(16221), Elem(380053), Elem(46880), Elem(8266723), Elem(8138859), Elem(8239390), Elem(496680), Elem(8265782), Elem(8023613), Elem(72806), Elem(300027), Elem(8062556), Elem(397658), Elem(41014), Elem(380995), Elem(9356), Elem(7892893), Elem(7994670), Elem(301744), Elem(261078), Elem(8221760), Elem(74223), Elem(370022), Elem(8257218), Elem(8152396), Elem(278103), Elem(344854), Elem(8369317), Elem(8369823), Elem(179606), Elem(456828), Elem(126472), Elem(8077821), Elem(8117504), Elem(7858494), Elem(8327060), Elem(361784), Elem(453419), Elem(8047112), Elem(8322368), Elem(339664), Elem(8322704), Elem(131921), Elem(277780), Elem(8023194), Elem(516125), Elem(264576), Elem(344799), Elem(7857389), Elem(8154177), Elem(100772), Elem(7962498), Elem(195312), Elem(8204096), Elem(443753), Elem(8103466), Elem(8079423), Elem(8168907), Elem(8243183), Elem(8033797), Elem(454346), Elem(8001186), Elem(301070), Elem(8054308), Elem(102001), Elem(80534), Elem(100146), Elem(7991916), Elem(192829), Elem(237113), Elem(8177677), Elem(186790), Elem(429958), Elem(8155543), Elem(408613), Elem(83372), Elem(8274100), Elem(402671), Elem(488687), Elem(8037210), Elem(291861), Elem(452098), Elem(8347548), Elem(79840), Elem(7928528), Elem(7891694), Elem(53086), Elem(450387), Elem(343000), Elem(29052), Elem(8090952), Elem(482272), Elem(64415), Elem(167026), Elem(8121557), Elem(7924918), Elem(306763), Elem(8326413), Elem(8162679), Elem(7858303), Elem(8182328), Elem(8141076), Elem(44186), Elem(7992041), Elem(8168012)])), Polynomial(Array([Elem(8133282), Elem(8374481), Elem(8192796), Elem(71363), Elem(373552), Elem(8363152), Elem(57644), Elem(405563), Elem(8307573), Elem(7912214), Elem(8155369), Elem(373841), Elem(456167), Elem(11657), Elem(8196902), Elem(8204457), Elem(8305083), Elem(34796), Elem(8327599), Elem(7904565), Elem(275755), Elem(8270645), Elem(517538), Elem(433999), Elem(8119882), Elem(175797), Elem(23861), Elem(8173891), Elem(200999), Elem(57177), Elem(8215368), Elem(7905921), Elem(8168005), Elem(8182322), Elem(8117750), Elem(8186101), Elem(516056), Elem(8349959), Elem(466842), Elem(8082124), Elem(8212766), Elem(317929), Elem(95677), Elem(7999735), Elem(247707), Elem(312848), Elem(242093), Elem(7899), Elem(7965565), Elem(430171), Elem(338330), Elem(8099520), Elem(89073), Elem(271027), Elem(7988300), Elem(8144093), Elem(8228134), Elem(294356), Elem(113452), Elem(7986450), Elem(8092349), Elem(181154), Elem(8019147), Elem(8323966), Elem(8140698), Elem(8327097), Elem(304287), Elem(7949053), Elem(7938092), Elem(8205818), Elem(267503), Elem(6951), Elem(351245), Elem(8303688), Elem(7921375), Elem(7910754), Elem(102915), Elem(385170), Elem(8201581), Elem(214087), Elem(7890742), Elem(7992696), Elem(98457), Elem(7883241), Elem(286565), Elem(149617), Elem(521070), Elem(7953718), Elem(140422), Elem(395191), Elem(9942), Elem(347347), Elem(8134348), Elem(388318), Elem(7910516), Elem(407277), Elem(516370), Elem(436127), Elem(23859), Elem(499296), Elem(326669), Elem(8296148), Elem(471826), Elem(442265), Elem(83198), Elem(8088260), Elem(77568), Elem(24620), Elem(299465), Elem(7912132), Elem(397877), Elem(8056610), Elem(498877), Elem(243534), Elem(172018), Elem(385043), Elem(8006475), Elem(8051491), Elem(8139313), Elem(227748), Elem(52284), Elem(8322235), Elem(117067), Elem(8193260), Elem(441282), Elem(468000), Elem(7913728), Elem(332336), Elem(483374), Elem(7901000), Elem(8105123), Elem(7872084), Elem(3412), Elem(318673), Elem(487222), Elem(8025448), Elem(207465), Elem(165146), Elem(514494), Elem(5581), Elem(8346043), Elem(8300185), Elem(7990926), Elem(475817), Elem(7894850), Elem(8362530), Elem(8054871), Elem(334132), Elem(232982), Elem(8171300), Elem(8020907), Elem(415441), Elem(7902834), Elem(475085), Elem(8015080), Elem(7996211), Elem(8309220), Elem(400393), Elem(472500), Elem(361535), Elem(8368477), Elem(308771), Elem(8206373), Elem(98111), Elem(161528), Elem(7927796), Elem(247459), Elem(373793), Elem(8171907), Elem(8216362), Elem(275734), Elem(7974395), Elem(8167707), Elem(8280770), Elem(194420), Elem(383106), Elem(7991601), Elem(366916), Elem(506148), Elem(120081), Elem(8023650), Elem(8244933), Elem(178020), Elem(8319882), Elem(56788), Elem(416760), Elem(8272714), Elem(239428), Elem(90271), Elem(234298), Elem(404193), Elem(8279408), Elem(486849), Elem(48845), Elem(8057375), Elem(8006911), Elem(520412), Elem(8082892), Elem(121625), Elem(84330), Elem(109607), Elem(455261), Elem(7892375), Elem(8167489), Elem(8213059), Elem(228786), Elem(37491), Elem(237395), Elem(237520), Elem(62330), Elem(217145), Elem(8341384), Elem(8214843), Elem(42204), Elem(7944554), Elem(8265517), Elem(8358725), Elem(8044311), Elem(8205698), Elem(8217144), Elem(8082162), Elem(227940), Elem(8282168), Elem(74390), Elem(8379504), Elem(74496), Elem(327979), Elem(99144), Elem(494739), Elem(471359), Elem(280797), Elem(42918), Elem(405854), Elem(511871), Elem(8126472), Elem(17663), Elem(117056), Elem(8343455), Elem(8217557), Elem(8049973), Elem(8026018), Elem(7890540), Elem(189082), Elem(191806), Elem(320918), Elem(7910919), Elem(505801), Elem(7992482), Elem(8014220), Elem(510762), Elem(7946611), Elem(280418), Elem(8296656), Elem(8070581), Elem(59122), Elem(8196814)])), Polynomial(Array([Elem(250829), Elem(8193654), Elem(8195537), Elem(226495), Elem(8220791), Elem(8107283), Elem(8052326), Elem(266123), Elem(7884889), Elem(93802), Elem(208927), Elem(7897671), Elem(227282), Elem(7979734), Elem(190285), Elem(98276), Elem(8327974), Elem(434270), Elem(83118), Elem(20971), Elem(370003), Elem(170599), Elem(220097), Elem(85976), Elem(8152698), Elem(8359341), Elem(471154), Elem(8289575), Elem(191861), Elem(8047340), Elem(7870135), Elem(72823), Elem(319443), Elem(8323509), Elem(206878), Elem(190417), Elem(8223266), Elem(384055), Elem(8182252), Elem(8246487), Elem(7867902), Elem(208696), Elem(7870423), Elem(141575), Elem(152983), Elem(316613), Elem(8175506), Elem(307278), Elem(193406), Elem(171193), Elem(166062), Elem(123828), Elem(453908), Elem(430160), Elem(60063), Elem(8015560), Elem(7859172), Elem(8364328), Elem(7960164), Elem(8342060), Elem(7998056), Elem(472712), Elem(187662), Elem(157553), Elem(17570), Elem(25081), Elem(7949934), Elem(7936802), Elem(7906507), Elem(334502), Elem(396364), Elem(492760), Elem(344362), Elem(72324), Elem(8303304), Elem(8359270), Elem(7902985), Elem(267517), Elem(8134540), Elem(8219706), Elem(8372838), Elem(7873306), Elem(303470), Elem(8369085), Elem(8303252), Elem(40901), Elem(498484), Elem(8202923), Elem(197925), Elem(475894), Elem(55812), Elem(521899), Elem(7990606), Elem(289032), Elem(8222432), Elem(8095695), Elem(475513), Elem(219971), Elem(240453), Elem(8070127), Elem(3863), Elem(8371861), Elem(514729), Elem(8346154), Elem(494491), Elem(265533), Elem(8343923), Elem(157587), Elem(8171144), Elem(8130823), Elem(221387), Elem(8270617), Elem(170654), Elem(8086180), Elem(188448), Elem(13279), Elem(8060597), Elem(8367220), Elem(185004), Elem(117861), Elem(119580), Elem(8104238), Elem(8087774), Elem(8124332), Elem(7901719), Elem(7245), Elem(250042), Elem(8301712), Elem(8128557), Elem(235811), Elem(382567), Elem(522982), Elem(363246), Elem(400176), Elem(8256273), Elem(8093679), Elem(308408), Elem(8312400), Elem(271968), Elem(8365462), Elem(7865369), Elem(267258), Elem(377150), Elem(7972937), Elem(215418), Elem(185566), Elem(8081247), Elem(7978151), Elem(7864357), Elem(496562), Elem(163932), Elem(81186), Elem(7959433), Elem(95273), Elem(8032245), Elem(411340), Elem(8257181), Elem(317823), Elem(8026712), Elem(97161), Elem(8305769), Elem(389434), Elem(8007726), Elem(8294530), Elem(8241386), Elem(334855), Elem(8301468), Elem(7962904), Elem(8282087), Elem(482103), Elem(411950), Elem(500068), Elem(31376), Elem(7874659), Elem(294900), Elem(123958), Elem(279997), Elem(24943), Elem(463548), Elem(223733), Elem(389251), Elem(330944), Elem(131220), Elem(230485), Elem(8341646), Elem(8342873), Elem(8170397), Elem(7899431), Elem(8281060), Elem(7985492), Elem(7912205), Elem(298728), Elem(226146), Elem(418394), Elem(447268), Elem(292408), Elem(8069627), Elem(458666), Elem(8178784), Elem(7964965), Elem(8368034), Elem(7982657), Elem(454256), Elem(37287), Elem(422487), Elem(523210), Elem(389154), Elem(8340342), Elem(104109), Elem(8070100), Elem(519515), Elem(74496), Elem(7916859), Elem(8022262), Elem(7882689), Elem(8041892), Elem(8136536), Elem(8097589), Elem(8025608), Elem(8149792), Elem(8012215), Elem(8240482), Elem(8202091), Elem(8361464), Elem(252606), Elem(387961), Elem(7875304), Elem(61567), Elem(8298950), Elem(70926), Elem(371915), Elem(234604), Elem(8238122), Elem(105536), Elem(79888), Elem(8367250), Elem(7883050), Elem(7898889), Elem(8010563), Elem(186233), Elem(7990774), Elem(248651), Elem(8312265), Elem(8233221), Elem(499803), Elem(8108972), Elem(8037189), Elem(483821), Elem(7885178), Elem(8370729), Elem(8262294), Elem(8342678), Elem(8876), Elem(317460), Elem(8072995), Elem(7878117)])), Polynomial(Array([Elem(463545), Elem(256506), Elem(309611), Elem(315093), Elem(196124), Elem(459708), Elem(316753), Elem(8144653), Elem(8068686), Elem(8173756), Elem(8291408), Elem(8278746), Elem(8034870), Elem(7911328), Elem(8320491), Elem(20019), Elem(8371830), Elem(471690), Elem(523146), Elem(8125942), Elem(8344561), Elem(495762), Elem(8088963), Elem(7861275), Elem(53404), Elem(8240941), Elem(7977135), Elem(320420), Elem(7909428), Elem(8212669), Elem(8283536), Elem(7970398), Elem(7891768), Elem(354562), Elem(8203885), Elem(7857142), Elem(142398), Elem(330997), Elem(167223), Elem(384463), Elem(7949577), Elem(258745), Elem(8046097), Elem(236133), Elem(293631), Elem(7898878), Elem(8182813), Elem(7910101), Elem(8020348), Elem(8226688), Elem(8252286), Elem(7872175), Elem(7867649), Elem(288406), Elem(478282), Elem(20069), Elem(8364866), Elem(8178062), Elem(8342158), Elem(8216137), Elem(118324), Elem(8199413), Elem(8176973), Elem(78171), Elem(7914642), Elem(8035281), Elem(7891035), Elem(7889392), Elem(8251482), Elem(8164620), Elem(7972563), Elem(69762), Elem(33409), Elem(8081739), Elem(229258), Elem(8072010), Elem(482527), Elem(367644), Elem(199955), Elem(8115479), Elem(8362983), Elem(8211122), Elem(30022), Elem(7941344), Elem(343067), Elem(146798), Elem(7967895), Elem(415655), Elem(284350), Elem(7877856), Elem(8165573), Elem(288709), Elem(8022069), Elem(8351538), Elem(8437), Elem(497233), Elem(8373038), Elem(8006666), Elem(286429), Elem(516612), Elem(8160261), Elem(96979), Elem(514237), Elem(7892785), Elem(151160), Elem(492982), Elem(500833), Elem(468096), Elem(7916091), Elem(8135228), Elem(237939), Elem(8341549), Elem(7925570), Elem(8287402), Elem(7885050), Elem(8086479), Elem(136489), Elem(8239513), Elem(8222496), Elem(8354250), Elem(8281980), Elem(253529), Elem(7861939), Elem(8117510), Elem(274646), Elem(483531), Elem(8106227), Elem(8223155), Elem(8050739), Elem(292818), Elem(5977), Elem(223238), Elem(190827), Elem(8219008), Elem(8023534), Elem(421978), Elem(7872642), Elem(511856), Elem(8212764), Elem(8190983), Elem(239461), Elem(7908615), Elem(428644), Elem(8353784), Elem(8293810), Elem(81372), Elem(8006385), Elem(8249048), Elem(359070), Elem(134430), Elem(343898), Elem(346971), Elem(8303411), Elem(8290470), Elem(7899693), Elem(342575), Elem(94843), Elem(478718), Elem(8101364), Elem(451628), Elem(7879661), Elem(8129767), Elem(311655), Elem(96023), Elem(8177121), Elem(8342335), Elem(8249789), Elem(181372), Elem(496149), Elem(8358694), Elem(8072085), Elem(8020028), Elem(448755), Elem(8172040), Elem(7880302), Elem(7919779), Elem(326559), Elem(8379018), Elem(32132), Elem(7999050), Elem(8357406), Elem(414133), Elem(8044828), Elem(7888515), Elem(8131511), Elem(7989194), Elem(7892517), Elem(8314004), Elem(8103144), Elem(8037273), Elem(8034796), Elem(8153898), Elem(182893), Elem(340648), Elem(8257890), Elem(78219), Elem(7866877), Elem(8075275), Elem(8067553), Elem(7889707), Elem(96409), Elem(97416), Elem(8104572), Elem(8379441), Elem(269021), Elem(8375999), Elem(8376433), Elem(95237), Elem(7956344), Elem(8309726), Elem(258499), Elem(130766), Elem(147802), Elem(363116), Elem(228650), Elem(8220403), Elem(7923553), Elem(8292026), Elem(187199), Elem(113124), Elem(514050), Elem(515968), Elem(8152729), Elem(8151429), Elem(145339), Elem(8027719), Elem(459764), Elem(8316549), Elem(82384), Elem(434883), Elem(414719), Elem(7983963), Elem(300488), Elem(195773), Elem(23387), Elem(7325), Elem(8096416), Elem(288138), Elem(8172942), Elem(7918798), Elem(162887), Elem(428713), Elem(462442), Elem(96104), Elem(111042), Elem(79171), Elem(275069), Elem(7995499), Elem(29347), Elem(113281), Elem(482116), Elem(7962249), Elem(8238649), Elem(127652), Elem(8047331), Elem(8105513)])), Polynomial(Array([Elem(8347379), Elem(8091850), Elem(8008526), Elem(8045659), Elem(8224543), Elem(8320054), Elem(8295750), Elem(483904), Elem(8232742), Elem(8116951), Elem(7911278), Elem(200862), Elem(321376), Elem(8068476), Elem(394311), Elem(8009820), Elem(178463), Elem(8131818), Elem(175628), Elem(289557), Elem(470755), Elem(458899), Elem(7871631), Elem(495838), Elem(478254), Elem(7949647), Elem(8021744), Elem(312222), Elem(7900133), Elem(213449), Elem(8205142), Elem(415931), Elem(351856), Elem(8283980), Elem(8258599), Elem(236030), Elem(238760), Elem(8210779), Elem(7223), Elem(274106), Elem(497946), Elem(7897181), Elem(8038951), Elem(8362717), Elem(7943483), Elem(275352), Elem(312102), Elem(7879475), Elem(8108350), Elem(8043750), Elem(135738), Elem(65351), Elem(519681), Elem(324237), Elem(7929797), Elem(8282269), Elem(63758), Elem(8321022), Elem(121976), Elem(7938638), Elem(86474), Elem(273792), Elem(8122394), Elem(500539), Elem(8075590), Elem(143201), Elem(7942038), Elem(195269), Elem(8245279), Elem(16319), Elem(7980793), Elem(7981546), Elem(8367553), Elem(7946182), Elem(261748), Elem(124768), Elem(8052371), Elem(8250333), Elem(140858), Elem(8018857), Elem(8018629), Elem(211678), Elem(309545), Elem(23473), Elem(475531), Elem(434441), Elem(402430), Elem(8214061), Elem(7885768), Elem(8149362), Elem(229564), Elem(283469), Elem(2024), Elem(7946339), Elem(356374), Elem(8208739), Elem(196725), Elem(171552), Elem(8327414), Elem(7955332), Elem(8318896), Elem(7966043), Elem(7886828), Elem(8356240), Elem(99555), Elem(302531), Elem(444988), Elem(8044131), Elem(8192732), Elem(202969), Elem(8340203), Elem(252990), Elem(94222), Elem(8200070), Elem(8312074), Elem(8236784), Elem(8022041), Elem(8041207), Elem(311912), Elem(101781), Elem(8081535), Elem(429048), Elem(7870344), Elem(286257), Elem(15758), Elem(345499), Elem(7907996), Elem(360466), Elem(483437), Elem(313888), Elem(8079049), Elem(229702), Elem(7866622), Elem(75509), Elem(56954), Elem(7899801), Elem(7950219), Elem(8143857), Elem(92325), Elem(7984836), Elem(246342), Elem(8152304), Elem(8161408), Elem(81941), Elem(72879), Elem(225834), Elem(232095), Elem(7881141), Elem(107556), Elem(460250), Elem(8290962), Elem(7883545), Elem(8042688), Elem(465090), Elem(8365970), Elem(145742), Elem(441327), Elem(181494), Elem(8105864), Elem(7875117), Elem(335363), Elem(79571), Elem(7922907), Elem(7917291), Elem(7998280), Elem(8043354), Elem(8366820), Elem(510877), Elem(229447), Elem(8317750), Elem(87468), Elem(8356312), Elem(8324786), Elem(8079064), Elem(239403), Elem(8258110), Elem(66530), Elem(110411), Elem(8252448), Elem(8315087), Elem(210462), Elem(137521), Elem(8202480), Elem(8235018), Elem(8256915), Elem(268539), Elem(412119), Elem(108432), Elem(228544), Elem(8359557), Elem(477193), Elem(7862616), Elem(8335599), Elem(93251), Elem(8341796), Elem(263474), Elem(117643), Elem(8214288), Elem(8247488), Elem(7922511), Elem(515553), Elem(8351419), Elem(8298055), Elem(8101902), Elem(7977444), Elem(8188505), Elem(31829), Elem(8092261), Elem(7947546), Elem(8199350), Elem(8046229), Elem(8004709), Elem(409164), Elem(8339281), Elem(415437), Elem(242455), Elem(7952942), Elem(8366070), Elem(405074), Elem(7932418), Elem(8082062), Elem(8198975), Elem(221801), Elem(7931720), Elem(8254792), Elem(8208491), Elem(8378716), Elem(7951683), Elem(7937336), Elem(8099784), Elem(7862949), Elem(8079950), Elem(8010623), Elem(7950471), Elem(8353752), Elem(7960872), Elem(205421), Elem(8333382), Elem(7923140), Elem(7938744), Elem(8236471), Elem(47726), Elem(430657), Elem(7910650), Elem(8031407), Elem(8228923), Elem(155173), Elem(8218253), Elem(8041544), Elem(236416), Elem(382935), Elem(7987408), Elem(180619), Elem(8307316), Elem(226722), Elem(7900043)]))])), h: Hint(Array([Array([false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]), Array([true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, true, false, false, true, false, false, false, false, false, false, true, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]), Array([false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, true, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]), Array([false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false])])) } diff --git a/ml-dsa/tests/sig-encoding.rs b/ml-dsa/tests/sig-encoding.rs new file mode 100644 index 00000000..08847ed1 --- /dev/null +++ b/ml-dsa/tests/sig-encoding.rs @@ -0,0 +1,46 @@ +use ml_dsa::{signature::Signer, KeyGen, MlDsa44, MlDsa65, MlDsa87, MlDsaParams, Signature, B32}; +use proptest::prelude::*; + +fn example_signature(seed_bytes: &B32) -> Signature

{ + let keypair = P::key_gen_internal(seed_bytes); + let msg = b""; + keypair.signing_key().sign(msg) +} + +prop_compose! { + fn mldsa44_signature()(seed_bytes in any::<[u8; 32]>()) -> Signature { + example_signature::(seed_bytes.as_ref()) + } +} + +prop_compose! { + fn mldsa65_signature()(seed_bytes in any::<[u8; 32]>()) -> Signature { + example_signature::(seed_bytes.as_ref()) + } +} + +prop_compose! { + fn mldsa87_signature()(seed_bytes in any::<[u8; 32]>()) -> Signature { + example_signature::(seed_bytes.as_ref()) + } +} + +proptest! { + #[test] + fn mldsa44_round_trip(sig in mldsa44_signature()) { + let sig_decoded = Signature::::decode(&sig.encode()); + prop_assert_eq!(Some(sig), sig_decoded); + } + + #[test] + fn mldsa65_round_trip(sig in mldsa65_signature()) { + let sig_decoded = Signature::::decode(&sig.encode()); + prop_assert_eq!(Some(sig), sig_decoded); + } + + #[test] + fn mldsa87_round_trip(sig in mldsa87_signature()) { + let sig_decoded = Signature::::decode(&sig.encode()); + prop_assert_eq!(Some(sig), sig_decoded); + } +}