[ "m]%n\u0007\u0019\u0017", [ [ "Hacl.Spec.RSAPSS.blocks_bits_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "5764d5d21083dbb8e758d2acb625ab29" ], [ "Hacl.Spec.RSAPSS.blocks_bits_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2", "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_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "bdab8a5f6d99a5ada0f358e21fd1aa31" ], [ "Hacl.Spec.RSAPSS.blocks_numb_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e5ff8a34ba8c8d261dda53bb839425ed" ], [ "Hacl.Spec.RSAPSS.blocks_numb_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "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_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "995a75de9135326c6570603be9a6e254" ], [ "Hacl.Spec.RSAPSS.bn_lt_pow2", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6947eeb04cc87783f724969397daccee" ], [ "Hacl.Spec.RSAPSS.bn_lt_pow2", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f044a520f33cec5f1ffb97fad68d9cd7" ], [ "Hacl.Spec.RSAPSS.bn_lt_pow2", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_inversion", "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_ca3218c12763b17ce56d4338a3b25f5e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "91c5a466af94412367b0838dc59ad5b3" ], [ "Hacl.Spec.RSAPSS.bn_eval_lt_pow2_modBits", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ca3218c12763b17ce56d4338a3b25f5e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ad0099ac055691c88632876fa11dfc88" ], [ "Hacl.Spec.RSAPSS.bn_eval_lt_pow2_modBits", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "27c75512fdd5f2c3453d7d5dc825309a" ], [ "Hacl.Spec.RSAPSS.bn_eval_lt_pow2_modBits", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ca3218c12763b17ce56d4338a3b25f5e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "71c228f3adfc3e645ec5b59658735bf3" ], [ "Hacl.Spec.RSAPSS.bn_lt_pow2_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8", "refinement_interpretation_Tm_refine_ca3218c12763b17ce56d4338a3b25f5e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "0ca079ff9586088c2628e26f909d356e" ], [ "Hacl.Spec.RSAPSS.bn_lt_pow2_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "bf27c58ad029a1465906a7a2b51e1528" ], [ "Hacl.Spec.RSAPSS.bn_lt_pow2_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.bn_lt_pow2", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1bc4bcbe4cabfaecf9cab0615ab0bb13", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_82995ba10c27999ff68cb2f423d8322b", "refinement_interpretation_Tm_refine_8bfea23f1ac4519cc5286ee2c6bbe35a", "refinement_interpretation_Tm_refine_9aa95d60dcdba9bfa5654e7dfdada927", "refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba", "refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8", "refinement_interpretation_Tm_refine_ca3218c12763b17ce56d4338a3b25f5e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f6ee57baa8c09234d642cef2e7e9e68e", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb0", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Hacl.Spec.Bignum.bn_get_ith_bit", "typing_Hacl.Spec.RSAPSS.bn_lt_pow2", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e3625e03b9fa613b4a74ea39c543b41c" ], [ "Hacl.Spec.RSAPSS.bn_eval_sub", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_b73ae1553bb8122cf6e200a51166d113", "refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8", "refinement_interpretation_Tm_refine_ca3218c12763b17ce56d4338a3b25f5e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "a5a0251d2e6ddf32fe7bc1e3a147e669" ], [ "Hacl.Spec.RSAPSS.bn_eval_sub", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "49a993865f9d7c1c16cf360906ac944b" ], [ "Hacl.Spec.RSAPSS.bn_eval_sub", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.slice", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "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_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_4a1627b4ec52a6d55c2e1bf08596b1df", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b73ae1553bb8122cf6e200a51166d113", "refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8", "refinement_interpretation_Tm_refine_ca3218c12763b17ce56d4338a3b25f5e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e84e70206efd63edd4c3fc7a2498d039", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "70cd264edd3bad62eeeb5b5ef8f03bc1" ], [ "Hacl.Spec.RSAPSS.pkey_len_pre", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "80c5868ec220c7318efbbd771c9f56d3" ], [ "Hacl.Spec.RSAPSS.skey_len_pre", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "67a3687b743a4ed2e5ca8fbd450953c9" ], [ "Hacl.Spec.RSAPSS.rsapss_pkey_pre", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "0e7f7e66b61dbc87bb54447539c0d6d3" ], [ "Hacl.Spec.RSAPSS.rsapss_pkey_pre", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f8b6bf67a4503f4c0c97081413d51bdf" ], [ "Hacl.Spec.RSAPSS.rsapss_pkey_pre", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c997e9d6cdd257eb091d5df1365340f7" ], [ "Hacl.Spec.RSAPSS.rsapss_skey_pre", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f597974aed8deb933e4e1ed843522d7d" ], [ "Hacl.Spec.RSAPSS.rsapss_skey_pre", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d98ec620580da04a630ef085f61b7a69" ], [ "Hacl.Spec.RSAPSS.rsapss_skey_pre", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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_0fe85c19e8efe98332bc47c04dccab44", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "refinement_interpretation_Tm_refine_f9e282bae3bc8f14d70b37fc3c535e7b", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8a1a5785d773a3be8c83164d23c824b2" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_pre", 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", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3ba9c4c5acf6383c02df393c4339a9e0" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_post", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3aaf7261cf78aaea611c59fd188f8849" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_post", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "644c33ea5672c71d68e8ebf48cbf06ce" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_post", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_sign_pre", "equation_Hacl.Spec.RSAPSS.rsapss_skey_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus", "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_7665eae1a09701632806c6d237eb2b97", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a330069aff0944e76f5bfc569abfcbdd", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.sub", "typing_Prims.pow2", "typing_Spec.RSAPSS.hash_is_supported", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "24e515c4829b9b19849f206de1cb8ae4" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_post1", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f22433992966104b5a3699fcd956abac" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_post1", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4c0e28d764ff8dd8790ab31b7667c234" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_post1", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_skey_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus", "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_7665eae1a09701632806c6d237eb2b97", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a330069aff0944e76f5bfc569abfcbdd", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.sub", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8b1b8f0fab645a2871fc385319ec07c2" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_post", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "53183b2dd74b22572faaaf153b9727fc" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_post", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "b23c60895418c57b5f15013f805b1eb0" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_post", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_verify_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "189b5c25256b18da84e16197acc165a4" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_post1", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c1a90634a8d093f7d03a13b19acda8ee" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_post1", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "a6024cbd3f9f105c5980f1075eb79789" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_post1", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4dc1b842004fbd00d4b871c597d98429" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_bn", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a330069aff0944e76f5bfc569abfcbdd", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d95b81f01b6e7c82a96e33c858dd1ba5" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_bn", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ac74d4fbc78321e0c13e618120eef5a4" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_bn", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "eq2-interp", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.blocks0", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_post", "equation_Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_pre", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_skey_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.NatMod.nat_mod", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "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_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_2cdb81665238403d595420381e28218c", "refinement_interpretation_Tm_refine_4fe9a5df27ca5859eef8add9fc6819fb", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_7665eae1a09701632806c6d237eb2b97", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_a330069aff0944e76f5bfc569abfcbdd", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d7a864ad48d8d01e39af22e13020447f", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.bn_v", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.NatMod.pow_mod", "typing_Lib.Sequence.sub", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "b36a4357de01d721461ef9f43333b1ee" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_msg_to_bn", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "cca8db1149cb164f7265272bb3bceb18" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_msg_to_bn", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.rsapss_sign_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "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.Hash.Definitions.hash_length", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "equation_Spec.RSAPSS.os2ip", "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_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_448579d1e002c52419fab7e24a1ddfee", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_77422a8b31f5d7e40ddb9d5c04ae7584", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ae9cd860763f73e90bcaae088ca19a22", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.RSAPSS.hash_is_supported", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "95740bd20ff83821e8f4b4e15697a85c" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_compute_sgnt", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a330069aff0944e76f5bfc569abfcbdd", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4fd2a9a1bf9cd1828f2135a11a268cd5" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_compute_sgnt", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "61992170bc8053d7d2bbeccbbd224701" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_compute_sgnt", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6b6fe707c481f20ae8052e8c6c089b5e" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ac429458e201ff5f1ab231c37b157a3d" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3009d533d4250f08c00f4262aa86f59b" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_skey_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.sub", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c865c399283286f855feb123122d6f8d" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "int_inversion", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "73d5f246510330f9ad923f6a2ec15aa4" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "16c61a4b860672ecfa6228ceb0477fa2" ], [ "Hacl.Spec.RSAPSS.rsapss_sign_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.eq", "equation_FStar.UInt32.eq", "equation_FStar.UInt64.eq", "equation_Hacl.Spec.Bignum.Base.mask_values", "equation_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.blocks0", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_post", "equation_Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_pre", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_sign_", "equation_Hacl.Spec.RSAPSS.rsapss_sign_bn", "equation_Hacl.Spec.RSAPSS.rsapss_sign_compute_sgnt", "equation_Hacl.Spec.RSAPSS.rsapss_sign_msg_to_bn", "equation_Hacl.Spec.RSAPSS.rsapss_sign_post", "equation_Hacl.Spec.RSAPSS.rsapss_sign_pre", "equation_Hacl.Spec.RSAPSS.rsapss_skey_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.NatMod.nat_mod", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.i2osp", "equation_Spec.RSAPSS.os2ip", "equation_Spec.RSAPSS.rsapss_sign_", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_e", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_n", "proj_equation_Spec.RSAPSS.Mk_rsapss_skey_d", "proj_equation_Spec.RSAPSS.Mk_rsapss_skey_pkey", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.RSAPSS.Mk_rsapss_pkey_e", "projection_inverse_Spec.RSAPSS.Mk_rsapss_pkey_n", "projection_inverse_Spec.RSAPSS.Mk_rsapss_skey_d", "projection_inverse_Spec.RSAPSS.Mk_rsapss_skey_pkey", "refinement_interpretation_Tm_refine_02f400218d898abe3d4eb33e8155bc31", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_2cdb81665238403d595420381e28218c", "refinement_interpretation_Tm_refine_448579d1e002c52419fab7e24a1ddfee", "refinement_interpretation_Tm_refine_4fe9a5df27ca5859eef8add9fc6819fb", "refinement_interpretation_Tm_refine_52b260fbf764e6f52338d81ab41bf472", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_7665eae1a09701632806c6d237eb2b97", "refinement_interpretation_Tm_refine_77422a8b31f5d7e40ddb9d5c04ae7584", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_a330069aff0944e76f5bfc569abfcbdd", "refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d7a864ad48d8d01e39af22e13020447f", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb", "typing_Hacl.Spec.Bignum.Definitions.bn_v", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.zeros", "typing_Lib.NatMod.pow_mod", "typing_Lib.Sequence.sub", "typing_Lib.Sequence.to_seq", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "3638d7c2fee0176092f689522fa2f64f" ], [ "Hacl.Spec.RSAPSS.rsapss_sign", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "cf9f66cd55c07c4a981eaf42d5a9bc19" ], [ "Hacl.Spec.RSAPSS.rsapss_sign", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "b8b2bd70e5f3be1932c9d959fbe2e1f9" ], [ "Hacl.Spec.RSAPSS.rsapss_sign", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_sign_post", "equation_Hacl.Spec.RSAPSS.rsapss_sign_post1", "equation_Hacl.Spec.RSAPSS.rsapss_sign_pre", "equation_Hacl.Spec.RSAPSS.rsapss_skey_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "equation_Spec.RSAPSS.rsapss_sign", "equation_Spec.RSAPSS.rsapss_sign_", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_Spec.RSAPSS.hash_is_supported" ], 0, "150466330a36ea0e596c0df6fd946def" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_bn", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f5bb0982fe20c0a919b4d403f7f5bc11" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_bn", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "a2402576871a95f56a46888f4f3cbfe6" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_bn", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.blocks0", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_pre", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_02f400218d898abe3d4eb33e8155bc31", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cc5db9e9e8be18c77f30c7d7fc620faa", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.ones", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "eafa33261ab398b5142481d04a1a7c1b" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_bn_to_msg", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e95b23e4126ea11a990c45467eab5d1d" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_bn_to_msg", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fbf4dfba3ea08457ebfb73caea4dbd28" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_bn_to_msg", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.rsapss_verify_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_36e7340acb459c52f49b11bd8f98210b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e84e70206efd63edd4c3fc7a2498d039", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Spec.RSAPSS.hash_is_supported", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8559e4e5fb2e2c6cce8ce63d1574f5aa" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_compute_msg", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "96a54d22c0f16d02ea0cc1d632fbff53" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_compute_msg", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c2578d46aa084491c65fbad09f136001" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_compute_msg", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.hash_is_supported", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.RSAPSS.hash_is_supported", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "512626f23f54bbc5667e5b647799875c" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ac1e699ea3c678ff9060ff1c658aa2a8" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "1e830bc55b0d740856c4d0e05e957b59" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_verify_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "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.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "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_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_7196fd310e7260eb7451e4c79f524513", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e84e70206efd63edd4c3fc7a2498d039", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.RSAPSS.hash_is_supported", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "9bb4ed1e562f51a38137e3a938391b1e" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "int_inversion", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "07587f91c8d0bf7c17ecf275eec1bd85" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d661897abfa00a4108bb783f17f787d2" ], [ "Hacl.Spec.RSAPSS.rsapss_verify_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Base.mask_values", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.blocks0", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_post", "equation_Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_pre", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_verify_", "equation_Hacl.Spec.RSAPSS.rsapss_verify_bn", "equation_Hacl.Spec.RSAPSS.rsapss_verify_bn_to_msg", "equation_Hacl.Spec.RSAPSS.rsapss_verify_compute_msg", "equation_Hacl.Spec.RSAPSS.rsapss_verify_post", "equation_Hacl.Spec.RSAPSS.rsapss_verify_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.NatMod.nat_mod", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.i2osp", "equation_Spec.RSAPSS.os2ip", "equation_Spec.RSAPSS.rsapss_verify_", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_e", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_n", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.RSAPSS.Mk_rsapss_pkey_e", "projection_inverse_Spec.RSAPSS.Mk_rsapss_pkey_n", "refinement_interpretation_Tm_refine_02f400218d898abe3d4eb33e8155bc31", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_36e7340acb459c52f49b11bd8f98210b", "refinement_interpretation_Tm_refine_4fe9a5df27ca5859eef8add9fc6819fb", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_602f7fb975cb72fc9795ad692974c7f5", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba", "refinement_interpretation_Tm_refine_c13a70ca65378e882aee506828fc9da8", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cc5db9e9e8be18c77f30c7d7fc620faa", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d713009c6d7c693536a1749a1adc7cae", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e84e70206efd63edd4c3fc7a2498d039", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "refinement_interpretation_Tm_refine_f6ee57baa8c09234d642cef2e7e9e68e", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb", "typing_Hacl.Spec.Bignum.Definitions.bn_v", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.zeros", "typing_Lib.NatMod.pow_mod", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d2b6b21d392b3ecb2b407f95de4b74c7" ], [ "Hacl.Spec.RSAPSS.rsapss_verify", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "65bbb58937d285c00ab648d2b6225bbb" ], [ "Hacl.Spec.RSAPSS.rsapss_verify", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "0c487b15a9f43bd35c2aa6676dbff5f3" ], [ "Hacl.Spec.RSAPSS.rsapss_verify", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_verify_post", "equation_Hacl.Spec.RSAPSS.rsapss_verify_post1", "equation_Hacl.Spec.RSAPSS.rsapss_verify_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "equation_Spec.RSAPSS.rsapss_verify", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_FStar.UInt.fits", "typing_Spec.RSAPSS.hash_is_supported" ], 0, "dd4376b5fee860e1b5d626950db80953" ], [ "Hacl.Spec.RSAPSS.bn_check_num_bits", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "964616f2f18d4bf90f77957450f9fd2b" ], [ "Hacl.Spec.RSAPSS.bn_check_num_bits", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "909cf4020793e2fd77df05b5b7d06f2e" ], [ "Hacl.Spec.RSAPSS.bn_check_num_bits", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Base.mask_values", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Equality", "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_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.zeros", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "a87996510c000efe9b7c163bcd5ff8b4" ], [ "Hacl.Spec.RSAPSS.rsapss_check_modulus", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "b948b301960be0b1cc87f2a48e813e0c" ], [ "Hacl.Spec.RSAPSS.rsapss_check_modulus", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "9228fb70ee5d11386203a9668981103e" ], [ "Hacl.Spec.RSAPSS.rsapss_check_modulus", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Base.mask_values", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.sub_mod_lemma", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "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_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d159fe5e58af2d5c150976d4684f3dc1", "refinement_interpretation_Tm_refine_e9c455cd5242bb3ccaf5d51a0c71360b", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.v", "typing_Lib.IntTypes.zeros", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "c11dddceaa6ea7d375f3947a16958b91" ], [ "Hacl.Spec.RSAPSS.rsapss_check_exponent", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f77f6e7f81ca8cd80cdbb2e5530392ba" ], [ "Hacl.Spec.RSAPSS.rsapss_check_exponent", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "9ea55fd40f8ce6189fe2d82653d73bfa" ], [ "Hacl.Spec.RSAPSS.rsapss_check_exponent", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Base.mask_values", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_e9c455cd5242bb3ccaf5d51a0c71360b", "typing_Hacl.Spec.Bignum.Definitions.bn_v", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.zeros", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "69abd3b49e2c8ebec0522bdeb6a51a11" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey_post", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "67008754a381cdbc5ba22c708f5ccd95" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey_post", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e620bbdac1e69ff0a85e91700b46a62b" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey_post", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "5a90b704359380f6918e6de24ab045b2" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey_post", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "660271de75d1e082b315b919f7ff138a" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey_post", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "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_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "35aa52068c41fcacc2ff67636934afd3" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey_post", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e2e920a4c6022b26d4b9cd1777b2d84d" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "1cfd5ca0590aa2a20fd27750582a2566" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8a9a9bc43b5f5d66497f4a79a52cf70e" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3", "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_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "refinement_interpretation_Tm_refine_f6c57233c579527eec2284a37ebc29fc", "refinement_interpretation_Tm_refine_f6ee57baa8c09234d642cef2e7e9e68e", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3af7ea0e0de2fa4f7bfe202dbd583f81" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "26ae87242f8c75529cc776f1765470ff" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey_lemma", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "2d6f33d820207ec0f43210c5bdc6eaa7" ], [ "Hacl.Spec.RSAPSS.rsapss_load_pkey_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.eq", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.eq", "equation_FStar.UInt64.eq", "equation_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_load_pkey", "equation_Hacl.Spec.RSAPSS.rsapss_load_pkey_post", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.modBits_t", "equation_Spec.RSAPSS.os2ip", "equation_Spec.RSAPSS.rsapss_load_pkey", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "kinding_Spec.RSAPSS.rsapss_pkey@tok", "l_and-interp", "lemma_FStar.Pervasives.invertOption", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_e", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_n", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Spec.RSAPSS.Mk_rsapss_pkey_e", "projection_inverse_Spec.RSAPSS.Mk_rsapss_pkey_n", "refinement_interpretation_Tm_refine_02f400218d898abe3d4eb33e8155bc31", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_153e687ebdbb4db2f55ced5c1e1dde07", "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_76744baf3c4ce1d34545bfdce173bf70", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0", "refinement_interpretation_Tm_refine_90a5495b5b490292930fdfb1c373304a", "refinement_interpretation_Tm_refine_9709793eb4d89958a1ba9b1b486244ca", "refinement_interpretation_Tm_refine_a32ee161e357c9710477326b2ab509af", "refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba", "refinement_interpretation_Tm_refine_a6fce85b67bdd71ab9416e435ac3b18a", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_af5ed72d7485a2fb7572601a8fd3615c", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d258417644cd33aefe030a24d979e6ad", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d7d8909a06e424f0c2893c6e910e18", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e1cf50390411fb38aa21003d641ae74c", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "refinement_interpretation_Tm_refine_f6ee57baa8c09234d642cef2e7e9e68e", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.v", "typing_Lib.IntTypes.zeros", "typing_Lib.RawIntTypes.u32_to_UInt32", "typing_Lib.RawIntTypes.u64_to_UInt64", "typing_Lib.Sequence.index", "typing_Lib.Sequence.to_seq", "typing_Prims.pow2", "typing_Spec.RSAPSS.rsapss_load_pkey", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "501fba629587f33b6d61f4e89dcaa0fd" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "b6847acacbfb5f0f0c14edf2d2a08e89" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "dfee7000bc51c244ce95c3852ecc63a0" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_load_pkey", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0565159ca1a4309c5fab2a6822440faa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83678983ec55b67ecd96b529e7f356b3", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f6ee57baa8c09234d642cef2e7e9e68e", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.blocks", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "94fee72d021d3e362edbcd83939b7009" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e3b1dd373cbdbc94f68905df2c578ed1" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey_lemma", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "a4d6743fb0b517c89fbdce8b08e5c607" ], [ "Hacl.Spec.RSAPSS.rsapss_load_skey_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.eq", "equation_FStar.UInt32.eq", "equation_FStar.UInt64.eq", "equation_Hacl.Spec.Bignum.Base.unsafe_bool_of_limb", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.bn_check_num_bits", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_check_exponent", "equation_Hacl.Spec.RSAPSS.rsapss_load_pkey", "equation_Hacl.Spec.RSAPSS.rsapss_load_pkey_post", "equation_Hacl.Spec.RSAPSS.rsapss_load_skey", "equation_Hacl.Spec.RSAPSS.rsapss_load_skey_post", "equation_Hacl.Spec.RSAPSS.rsapss_pkey_pre", "equation_Hacl.Spec.RSAPSS.rsapss_skey_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.modBits_t", "equation_Spec.RSAPSS.os2ip", "equation_Spec.RSAPSS.rsapss_load_pkey", "equation_Spec.RSAPSS.rsapss_load_skey", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "kinding_Spec.RSAPSS.rsapss_skey@tok", "l_and-interp", "lemma_FStar.Pervasives.invertOption", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.RSAPSS.Mk_rsapss_skey_d", "proj_equation_Spec.RSAPSS.Mk_rsapss_skey_pkey", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Spec.RSAPSS.Mk_rsapss_skey_d", "projection_inverse_Spec.RSAPSS.Mk_rsapss_skey_pkey", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_153e687ebdbb4db2f55ced5c1e1dde07", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_4601c7943b9f49090403f1760fd6232f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_6f6a8ba7f271e7a687b123c03b9d39b8", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83678983ec55b67ecd96b529e7f356b3", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9709793eb4d89958a1ba9b1b486244ca", "refinement_interpretation_Tm_refine_a6332c30dd0f7eb5f4148d63b72c78ba", "refinement_interpretation_Tm_refine_a6fce85b67bdd71ab9416e435ac3b18a", "refinement_interpretation_Tm_refine_a75bc5d6c7bb84c5f44bcec68c6b8447", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e9c455cd5242bb3ccaf5d51a0c71360b", "refinement_interpretation_Tm_refine_eb8fe5007401a8b70dac38f24fc64b3b", "refinement_interpretation_Tm_refine_ee46a8145a021ba9fdc888415678d8f6", "refinement_interpretation_Tm_refine_f6ee57baa8c09234d642cef2e7e9e68e", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Hacl.Spec.RSAPSS.bn_check_num_bits", "typing_Hacl.Spec.RSAPSS.rsapss_check_exponent", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.v", "typing_Lib.IntTypes.zeros", "typing_Lib.RawIntTypes.u32_to_UInt32", "typing_Lib.RawIntTypes.u64_to_UInt64", "typing_Lib.Sequence.index", "typing_Lib.Sequence.sub", "typing_Spec.RSAPSS.rsapss_load_skey", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "ac12b046762a669bb546e18d7f7cd9e7" ], [ "Hacl.Spec.RSAPSS.rsapss_skey_sign", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f315f5750970cf3448ce60f8385cbd3d" ], [ "Hacl.Spec.RSAPSS.rsapss_skey_sign", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "15e1cae10eca9c94f09d3091d304d443" ], [ "Hacl.Spec.RSAPSS.rsapss_skey_sign", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_load_skey", "equation_Hacl.Spec.RSAPSS.rsapss_load_skey_post", "equation_Hacl.Spec.RSAPSS.rsapss_sign_post1", "equation_Hacl.Spec.RSAPSS.skey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "equation_Spec.RSAPSS.modBits_t", "equation_Spec.RSAPSS.rsapss_skey_sign", "fuel_guarded_inversion_Spec.RSAPSS.rsapss_pkey", "fuel_guarded_inversion_Spec.RSAPSS.rsapss_skey", "int_inversion", "kinding_Spec.RSAPSS.rsapss_skey@tok", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_e", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_n", "proj_equation_Spec.RSAPSS.Mk_rsapss_skey_d", "proj_equation_Spec.RSAPSS.Mk_rsapss_skey_pkey", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.None_a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_ce0651008b932fd5b67f9859b574454a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_Lib.IntTypes.bits", "typing_Spec.RSAPSS.__proj__Mk_rsapss_skey__item__pkey", "typing_Spec.RSAPSS.hash_is_supported", "typing_Spec.RSAPSS.rsapss_load_skey", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "7fcd20fd09fd6d88edfa0cc064a1b9ff" ], [ "Hacl.Spec.RSAPSS.rsapss_pkey_verify", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fa21cf5dc3d50e83e52722475fe98d39" ], [ "Hacl.Spec.RSAPSS.rsapss_pkey_verify", 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_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "df9f29fd16cde69260be3de80502292f" ], [ "Hacl.Spec.RSAPSS.rsapss_pkey_verify", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.blocks", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.RSAPSS.pkey_len_pre", "equation_Hacl.Spec.RSAPSS.rsapss_load_pkey_post", "equation_Hacl.Spec.RSAPSS.rsapss_verify_post1", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.RSAPSS.blocks", "equation_Spec.RSAPSS.hash_is_supported", "equation_Spec.RSAPSS.modBits_t", "equation_Spec.RSAPSS.rsapss_pkey_verify", "fuel_guarded_inversion_Spec.RSAPSS.rsapss_pkey", "int_inversion", "kinding_Spec.RSAPSS.rsapss_pkey@tok", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_e", "proj_equation_Spec.RSAPSS.Mk_rsapss_pkey_n", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_68b6caaa439389b926e1f13e0ddbda05", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_af61b6de27527a4c262716f67a596235", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f45224c64ec2d6453f0c426ff4ef8441", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_Lib.IntTypes.bits", "typing_Spec.RSAPSS.hash_is_supported", "typing_Spec.RSAPSS.rsapss_load_pkey", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "27fd76f618adc567ded9968d931b7691" ] ] ]