Revision 8a7e1b7f7f7dda7d9ac75c7adbb915b5c7db208f authored by Dzomo the everest Yak on 09 January 2020, 09:25:31 UTC, committed by Dzomo the everest Yak on 09 January 2020, 09:25:31 UTC
1 parent 9cd0bde
Spec.RSAPSS.fst.hints
[
"rz���}���C��\u0019%�\u0010",
[
[
"Spec.RSAPSS.blocks",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"317df4b6f9b2ba655e0532be5b461ae6"
],
[
"Spec.RSAPSS.xor_bytes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"90fffff755169f4e13f2f810a50563c2"
],
[
"Spec.RSAPSS.xor_bytes",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8adb7aef1ad97d6bbae68365b87a6aa5"
],
[
"Spec.RSAPSS.xor_bytes",
3,
0,
0,
[ "@query" ],
0,
"8fe8f0fac78372aae38a05c69cea1f12"
],
[
"Spec.RSAPSS.sha2_256",
1,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"9acce153a39deffa8f07e6c8d2b7a96d"
],
[
"Spec.RSAPSS.sha2_256",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Spec.RSAPSS.hLen",
"equation_Spec.RSAPSS.max_input", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7a9bdf49ef7a8346011a869ad0933465",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"86f2848ec9901a97753c5a5dfe9fa059"
],
[
"Spec.RSAPSS.mgf_sha256_f",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_e0fe7f087bac97b52dc35fba7b9a152e",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"fe146e3bf24c3cc06f47d305ceeda245"
],
[
"Spec.RSAPSS.mgf_sha256_f",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_e0fe7f087bac97b52dc35fba7b9a152e"
],
0,
"b72c6be904a0a374ae912fb31da21e4c"
],
[
"Spec.RSAPSS.mgf_sha256_f",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.RSAPSS.hLen", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_4756c4a467e3f4df77adccc73c7cc7cb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_88ef94fe035cf45009c506efbe8f9660",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e0fe7f087bac97b52dc35fba7b9a152e",
"refinement_interpretation_Tm_refine_ffc9bf02f783b699fbdddf2a2663389d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"f4a56d169f8091e0a7db4f7f9604f878"
],
[
"Spec.RSAPSS.mgf_sha256_a",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3a9708a0918387aad4626280399c98c2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"8a822361353873c6f1d2062592dcddb3"
],
[
"Spec.RSAPSS.mgf_sha256",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8da970a25fb1850a6a176b9e7202fc0a"
],
[
"Spec.RSAPSS.mgf_sha256",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"142cf7d89929571e76e0e4264af4c347"
],
[
"Spec.RSAPSS.mgf_sha256",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.RSAPSS.blocks",
"equation_Spec.RSAPSS.hLen", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43ccb712f5c3d8144981b6f2bc88bf12",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b62b031a3466f64c12f83618ab9b2409",
"refinement_interpretation_Tm_refine_bc3e976e992e53bce2affc941a622b1c",
"refinement_interpretation_Tm_refine_d0b24b287180afeca72b9936d6519997",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e0fe7f087bac97b52dc35fba7b9a152e",
"refinement_interpretation_Tm_refine_e1bede3f327e8da08d5b1f69bef560c3",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"fd38b6a382fb49f5f07ccfdc2cf5bca9"
],
[
"Spec.RSAPSS.os2ip",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"00109dfe29ee4eac4dcd09bf0ad034ef"
],
[
"Spec.RSAPSS.os2ip",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"16fe33347803c60b270c477883b91154"
],
[
"Spec.RSAPSS.i2osp",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"a7a09c19421def5476d131085f580b69"
],
[
"Spec.RSAPSS.i2osp",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f55b7affb88720bf5567c7e9bbf631d7"
],
[
"Spec.RSAPSS.i2osp",
3,
0,
0,
[ "@query", "equation_Lib.Sequence.length" ],
0,
"270e377c8b54e3c643d131f06d5ad14b"
],
[
"Spec.RSAPSS.fmul",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"2863e2b0458c1550e0cf21d9aae8566c"
],
[
"Spec.RSAPSS.fpow",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"well-founded-ordering-on-nat"
],
0,
"76401170cc3fee519a72f2e277d3ac9b"
],
[
"Spec.RSAPSS.rsa_pubkey",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.RSAPSS.modBits_t",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235"
],
0,
"5fc74323afaf4595f953e27448e3a9d7"
],
[
"Spec.RSAPSS.__proj__Mk_rsa_pubkey__item__n",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.RSAPSS.modBits_t",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235"
],
0,
"bbfbf72c7cc7598d93a9c00edfef3776"
],
[
"Spec.RSAPSS.__proj__Mk_rsa_pubkey__item__n",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.RSAPSS.modBits_t",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235"
],
0,
"b961a803981f9b94a3fd81b4073a8552"
],
[
"Spec.RSAPSS.db_zero",
1,
0,
0,
[ "@query" ],
0,
"e399576aa94380ce050869f67363f485"
],
[
"Spec.RSAPSS.db_zero",
2,
0,
0,
[ "@query" ],
0,
"49a55a765ab1d700f474cc9e8f6f81ae"
],
[
"Spec.RSAPSS.db_zero",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"a9f1778528e9d1438ed98ab4eda3e5a9"
],
[
"Spec.RSAPSS.pss_encode",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3fe71f2f0f286c16c4713512c079ec1c",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"fff73b91e50e5e2b28f529fc8105f947"
],
[
"Spec.RSAPSS.pss_encode",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"3594677776df175295a5d75917fdaeb9"
],
[
"Spec.RSAPSS.pss_encode",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hLen",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_27dc038cce58e6a175dcb6195f80808a",
"refinement_interpretation_Tm_refine_2e60ac16dfc2d5c6accde2e03ee10a17",
"refinement_interpretation_Tm_refine_3fe71f2f0f286c16c4713512c079ec1c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42cb89b0c76274d5ad8011eab6dd2490",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_4c2959865f0c741bfd5450414ffcd1da",
"refinement_interpretation_Tm_refine_4cc54547e4a3f0677e4788a5316e6c4c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_72d5d433aa61bc02624adba0c1929d2d",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_82423e9b4b7e75f521d6e4d5075e4376",
"refinement_interpretation_Tm_refine_8432b0fa56a3826bd2ff84b1fa5a24cb",
"refinement_interpretation_Tm_refine_87e93cd9b9f50eb41fe191b341b464ee",
"refinement_interpretation_Tm_refine_c0a0f3f161b2242154b605a2a9d55fc3",
"refinement_interpretation_Tm_refine_d06b5b03433ead4bd61859f2ea3ebb83",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_dcf9ce8a8362a9829024d9f7de0823a8",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"e29ee3e16ff5f391ab7ba1ad531bf2c4"
],
[
"Spec.RSAPSS.pss_verify_",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"1c30516d7638731c176d5e11584f11e4"
],
[
"Spec.RSAPSS.pss_verify_",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"0c2a22e0ac07036fa65c10187373b4c4"
],
[
"Spec.RSAPSS.pss_verify_",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hLen",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2e60ac16dfc2d5c6accde2e03ee10a17",
"refinement_interpretation_Tm_refine_303069af31d2c0b822bdd15249b1140b",
"refinement_interpretation_Tm_refine_3e16bfc7be0ba2aa850ce050bfdbb996",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42cb89b0c76274d5ad8011eab6dd2490",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_601f9f284a2c45a059965f20345c0099",
"refinement_interpretation_Tm_refine_614a19167a990d25fd513e0a849b3dd3",
"refinement_interpretation_Tm_refine_65d99d36b3e0eeb927c7d852858fa0cd",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8432b0fa56a3826bd2ff84b1fa5a24cb",
"refinement_interpretation_Tm_refine_87e93cd9b9f50eb41fe191b341b464ee",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c9a6ef084c92ca5a8f86f4a7af0e93ba",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2"
],
0,
"2b50926d6cdb6fcb6c2964ac199d59e5"
],
[
"Spec.RSAPSS.pss_verify",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"cb2455fca37587277cdffc1582d81a2b"
],
[
"Spec.RSAPSS.pss_verify",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"eb13ce77111e64b47c061a05e2b4f8b8"
],
[
"Spec.RSAPSS.pss_verify",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hLen",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"3fcfd0203573ead2c24d51ed71de5054"
],
[
"Spec.RSAPSS.rsapss_sign",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "equation_Spec.RSAPSS.modBits_t",
"fuel_guarded_inversion_Spec.RSAPSS.rsa_privkey", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2c21692968114ae1e75257eccc072248",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235"
],
0,
"b8e6306529135cda0fc99190f07c64aa"
],
[
"Spec.RSAPSS.rsapss_sign",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "equation_Spec.RSAPSS.modBits_t",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235"
],
0,
"32561d2d2d253ceb1db77e679ffd1b73"
],
[
"Spec.RSAPSS.rsapss_sign",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hLen",
"equation_Spec.RSAPSS.modBits_t",
"fuel_guarded_inversion_Spec.RSAPSS.rsa_privkey",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2c21692968114ae1e75257eccc072248",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7969cc2c60952a7d46bbb0e17f7f26e2",
"refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235",
"refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8"
],
0,
"8d2f3a3e1853dd8f8f4ef7d0e5c33060"
],
[
"Spec.RSAPSS.rsapss_verify",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "equation_Spec.RSAPSS.modBits_t",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235"
],
0,
"f42fda5c47cd74d364fb5bfdf158c398"
],
[
"Spec.RSAPSS.rsapss_verify",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.RSAPSS.hLen", "equation_Spec.RSAPSS.modBits_t",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235"
],
0,
"ba67f3b0e58f9849ef61a2293c35d60f"
],
[
"Spec.RSAPSS.rsapss_verify",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.RSAPSS.blocks",
"equation_Spec.RSAPSS.hLen", "equation_Spec.RSAPSS.modBits_t",
"fuel_guarded_inversion_Spec.RSAPSS.rsa_pubkey",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_43e2345aa34610efddbddd3534552135",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba",
"refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235",
"refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8"
],
0,
"450d03632f01530d2ea7e55d692bbe89"
]
]
]
Computing file changes ...
