Spec.SHA2.fst.hints
[
"T�D}g�1���C��n\u0011�",
[
[
"Spec.SHA2.size_k_w",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"11df99525ed0a44e8adf498709eea483"
],
[
"Spec.SHA2.word_n",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"783cf45d0f00fe8e8f479f6caf235f44"
],
[
"Spec.SHA2.v'",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"2fa93876a4cc2ad4f74f774cfff8d9c3"
],
[
"Spec.SHA2.k_w",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"59c772c96f51856a275fdd5a4d1d0c75"
],
[
"Spec.SHA2.word_add_mod",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"d3eb4c1cb3085207b5a600463395e71c"
],
[
"Spec.SHA2.word_logxor",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"782a4dcd7c0bd68b1e6a46840ac38cc6"
],
[
"Spec.SHA2.word_logand",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"37f21cc41ac4060dc3c7b3b5ced4554e"
],
[
"Spec.SHA2.word_logor",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"fd455d148bc5c696ec37a2d7898d7c9f"
],
[
"Spec.SHA2.word_lognot",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"c5d5991e83b96299020f69a226058f4d"
],
[
"Spec.SHA2.word_shift_right",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.SHA2.v_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.UInt.shift_right_value_lemma",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.UInt32.v", "typing_FStar.UInt64.v",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"7ca9c27684ed11bf4655403f0f7c65ca"
],
[
"Spec.SHA2.word_shift_right",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "function_token_typing_FStar.UInt32.n",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.UInt32.v"
],
0,
"faa77a1ea92284e836cb7010d1c664c8"
],
[
"Spec.SHA2.rotate_right32",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_42cf8cb5aa2c0a99d2c5dc29ce6c326a",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt32.v"
],
0,
"a8a68d3cb487e76ea57130e6e8be3f2e"
],
[
"Spec.SHA2.rotate_right64",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5119d4a133868cbb7eb3e04a27fbd259",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt32.v", "typing_FStar.UInt64.v"
],
0,
"3aa63b23aa74b3ea6801f33dd9e0c81d"
],
[
"Spec.SHA2.word_rotate_right",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.word_n",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"610311d00a3db83868cab24a186ffcba"
],
[
"Spec.SHA2.ops",
1,
2,
1,
[ "@query", "assumption_FStar.UInt32.t__uu___haseq" ],
0,
"dc53256497d920e08984024ddac227af"
],
[
"Spec.SHA2.op0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"typing_Spec.Hash.Definitions.is_sha2"
],
0,
"5bacd064e2f42cc16900aa00ced7e8aa"
],
[
"Spec.SHA2._Sigma0",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "constructor_distinct_Tm_unit",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.SHA2.op0",
"equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512",
"equation_Spec.SHA2.word_n",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.SHA2.ops",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_Spec.SHA2.Mkops_c0",
"proj_equation_Spec.SHA2.Mkops_c1",
"proj_equation_Spec.SHA2.Mkops_c2",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.SHA2.Mkops_c0",
"projection_inverse_Spec.SHA2.Mkops_c1",
"projection_inverse_Spec.SHA2.Mkops_c2",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Spec.Hash.Definitions.is_sha2",
"typing_Spec.SHA2.__proj__Mkops__item__c0",
"typing_Spec.SHA2.__proj__Mkops__item__c1",
"typing_Spec.SHA2.__proj__Mkops__item__c2", "typing_Spec.SHA2.op0",
"typing_Spec.SHA2.word_n"
],
0,
"2e7ffd4322f9435f55317b419446e5fc"
],
[
"Spec.SHA2._Sigma1",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "constructor_distinct_Tm_unit",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.SHA2.op0",
"equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512",
"equation_Spec.SHA2.word_n",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.SHA2.ops",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_Spec.SHA2.Mkops_c3",
"proj_equation_Spec.SHA2.Mkops_c4",
"proj_equation_Spec.SHA2.Mkops_c5",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.SHA2.Mkops_c3",
"projection_inverse_Spec.SHA2.Mkops_c4",
"projection_inverse_Spec.SHA2.Mkops_c5",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Spec.Hash.Definitions.is_sha2",
"typing_Spec.SHA2.__proj__Mkops__item__c3",
"typing_Spec.SHA2.__proj__Mkops__item__c4",
"typing_Spec.SHA2.__proj__Mkops__item__c5", "typing_Spec.SHA2.op0",
"typing_Spec.SHA2.word_n"
],
0,
"70db406108a4bfbd7a5a62590d71993f"
],
[
"Spec.SHA2._sigma0",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "constructor_distinct_Tm_unit",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256",
"equation_Spec.SHA2.op384_512", "equation_Spec.SHA2.word_n",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.SHA2.ops",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.SHA2.Mkops_e0",
"proj_equation_Spec.SHA2.Mkops_e1",
"proj_equation_Spec.SHA2.Mkops_e2",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.SHA2.Mkops_e0",
"projection_inverse_Spec.SHA2.Mkops_e1",
"projection_inverse_Spec.SHA2.Mkops_e2",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Spec.Hash.Definitions.is_sha2",
"typing_Spec.SHA2.__proj__Mkops__item__e0", "typing_Spec.SHA2.op0",
"typing_Spec.SHA2.word_n"
],
0,
"303d87baa18eb543ffea951d2c312b2d"
],
[
"Spec.SHA2._sigma1",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "constructor_distinct_Tm_unit",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256",
"equation_Spec.SHA2.op384_512", "equation_Spec.SHA2.word_n",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.SHA2.ops",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_Spec.SHA2.Mkops_e3",
"proj_equation_Spec.SHA2.Mkops_e4",
"proj_equation_Spec.SHA2.Mkops_e5",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.SHA2.Mkops_e3",
"projection_inverse_Spec.SHA2.Mkops_e4",
"projection_inverse_Spec.SHA2.Mkops_e5",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Spec.Hash.Definitions.is_sha2",
"typing_Spec.SHA2.__proj__Mkops__item__e3",
"typing_Spec.SHA2.__proj__Mkops__item__e4", "typing_Spec.SHA2.op0",
"typing_Spec.SHA2.word_n"
],
0,
"99783fc4f8ef637300706059d391c7c9"
],
[
"Spec.SHA2.h0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_FStar.List.Tot.Properties.llist",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"typing_Spec.Hash.Definitions.is_sha2",
"typing_Spec.SHA2.Constants.h224_l",
"typing_Spec.SHA2.Constants.h256_l",
"typing_Spec.SHA2.Constants.h384_l",
"typing_Spec.SHA2.Constants.h512_l"
],
0,
"ae4b0f18a5a1009c1c065642e03bd0e7"
],
[
"Spec.SHA2.k0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_FStar.List.Tot.Properties.llist", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.size_k_w",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"typing_Spec.Hash.Definitions.is_sha2",
"typing_Spec.SHA2.Constants.k224_256_l",
"typing_Spec.SHA2.Constants.k384_512_l"
],
0,
"97fd658e2cd8d850bea288c22e937002"
],
[
"Spec.SHA2.k0",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"e98e0f5c48bbcc88ff1a8e5a3ec600ad"
],
[
"Spec.SHA2.ws_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_e1b5e8043a83793e7f7b9d051beb8439_1",
"binder_x_e6cf0887f763ac48873f31576fccdc3e_0",
"binder_x_fa16d3e062096b51402d249c254edb9f_2", "bool_inversion",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_2db19a6cd136e83a967cec5c7456ece9",
"refinement_interpretation_Tm_refine_9c454287a229df633da990c83d3ffd57",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Hash.Definitions.is_sha2",
"well-founded-ordering-on-nat"
],
0,
"b5c45c58879ba3129fdb7dce73583af8"
],
[
"Spec.SHA2.shuffle_core_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.SHA2.counter", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.size_k_w",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca",
"refinement_interpretation_Tm_refine_b01a3abf8fe93d0e62b65df542fb8b5b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_Spec.SHA2.k0", "typing_Spec.SHA2.size_k_w"
],
0,
"4f4ee046dec43206665b6c5c157b8a6e"
],
[
"Spec.SHA2.shuffle_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.SHA2.size_k_w",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.SHA2.size_k_w"
],
0,
"db1c53ae76f11acafab7ee639fc12780"
],
[
"Spec.SHA2.update_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.words_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_79f632aa3673390dc46de32f66260b13"
],
0,
"01f12f3a89064f8372616c995edb4d02"
]
]
]