Revision c596c6bb21e6e478e0b46159ef182ccce6a695cb authored by Konrad Kohbrok on 16 April 2018, 13:51:58 UTC, committed by Konrad Kohbrok on 16 April 2018, 13:51:58 UTC
1 parent 68d3953
Spec.SHA2.fst.hints
[
"Ġ\u0001ĊÁ
\u000eẃÍcĠḞH\u001fỳQE",
[
[
"Spec.SHA2.pow2_values",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.pow2_values",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.pow2_values",
3,
0,
1,
[ "@query", "equation_Prims.l_True" ],
0
],
[
"Spec.SHA2.pow2_values",
4,
0,
1,
[
"@query", "equation_FStar.HyperHeap.test0", "equation_Prims._assert",
"equation_Prims.assert_norm",
"function_token_typing_FStar.HyperHeap.test0",
"projection_inverse_BoxInt_proj_0"
],
0
],
[ "Spec.SHA2.uu___is_SHA2_224", 1, 0, 1, [ "@query" ], 0 ],
[ "Spec.SHA2.uu___is_SHA2_256", 1, 0, 1, [ "@query" ], 0 ],
[ "Spec.SHA2.uu___is_SHA2_384", 1, 0, 1, [ "@query" ], 0 ],
[ "Spec.SHA2.uu___is_SHA2_512", 1, 0, 1, [ "@query" ], 0 ],
[
"Spec.SHA2.size_word",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.size_hash_final_w",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.size_k_w",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.size_len_8",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.size_len_ul_8",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_Spec.SHA2.size_len_8",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_FStar.UInt32.Mk_v"
],
0
],
[
"Spec.SHA2.size_len_ul_8",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
"haseqSpec.SHA2_Tm_refine_530be526726c3b66223dd819f9d65058",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.max_input8",
1,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512", "equation_Prims.pos",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0
],
[
"Spec.SHA2.word",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512", "equation_FStar.UInt32.t",
"equation_FStar.UInt64.t",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.word_n",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.v'",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.hash_w",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.k_w",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.ws_w",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.block_w",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.words_to_be",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok",
"equality_tok_Spec.SHA2.SHA2_512@tok",
"equation_Spec.SHA2.size_word", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.words_to_be",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.words_to_be",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Mul.op_Star",
"equation_Prims.nat", "equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.words_from_be",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok",
"equality_tok_Spec.SHA2.SHA2_512@tok",
"equation_Spec.SHA2.size_word", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.words_from_be",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.words_from_be",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Mul.op_Star",
"equation_Prims.nat", "equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.word_add_mod",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok",
"equality_tok_Spec.SHA2.SHA2_512@tok", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.word_logxor",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.word_logand",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok",
"equality_tok_Spec.SHA2.SHA2_512@tok", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.word_logor",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.word_lognot",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.word_shift_right",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"constructor_distinct_Tm_unit", "disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_Prims.nat",
"equation_Spec.SHA2.size_word", "equation_Spec.SHA2.v_",
"equation_Spec.SHA2.word", "fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"fuel_guarded_inversion_Spec.SHA2.hash_alg", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.SHA2.size_word"
],
0
],
[
"Spec.SHA2.word_shift_right",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.word_shift_right",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"data_elim_FStar.UInt32.Mk", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
"equation_FStar.UInt64.n", "equation_Spec.SHA2.v_",
"fuel_guarded_inversion_FStar.UInt32.t_", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Spec.SHA2_Tm_refine_fa09253699d304a74f7c0155ca92dc5e",
"typing_Spec.SHA2.v_"
],
0
],
[
"Spec.SHA2.rotate_right32",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Lib_Tm_refine_42cf8cb5aa2c0a99d2c5dc29ce6c326a"
],
0
],
[
"Spec.SHA2.rotate_right64",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_FStar.UInt64.n", "equation_Prims.nat",
"function_token_typing_FStar.UInt32.n",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.SHA2_Tm_refine_5119d4a133868cbb7eb3e04a27fbd259"
],
0
],
[
"Spec.SHA2.word_rotate_right",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok", "equation_Spec.SHA2.word",
"equation_Spec.SHA2.word_n",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.op224_256",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[ "Spec.SHA2.op224_256", 2, 0, 1, [ "@query" ], 0 ],
[
"Spec.SHA2.op384_512",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[ "Spec.SHA2.op384_512", 2, 0, 1, [ "@query" ], 0 ],
[
"Spec.SHA2.op0",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512", "equation_Spec.SHA2.op224_256",
"equation_Spec.SHA2.op384_512",
"fuel_guarded_inversion_Spec.SHA2.hash_alg"
],
0
],
[
"Spec.SHA2.op0",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2._Sigma0",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.Mk",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt8.n",
"equation_Prims.nat", "equation_Spec.Lib.op_String_Access",
"equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256",
"equation_Spec.SHA2.op384_512", "equation_Spec.SHA2.word",
"equation_Spec.SHA2.word_n",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Spec.SHA2.op224_256",
"function_token_typing_Spec.SHA2.op384_512", "int_inversion",
"int_typing", "kinding_FStar.UInt32.t_@tok",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Seq.Create_Tm_refine_036fb6020f4219ad59b2c9e02e579d2c",
"refinement_interpretation_Spec.SHA2_Tm_refine_a56d4a59fba339ca5210379815875fe9",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Seq.Create.create_12",
"typing_Spec.SHA2.op0", "typing_Spec.SHA2.word_n"
],
0
],
[
"Spec.SHA2._Sigma1",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"data_elim_FStar.UInt32.Mk", "data_typing_intro_FStar.UInt32.Mk@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_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_FStar.UInt8.n",
"equation_Prims.nat", "equation_Spec.Lib.op_String_Access",
"equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256",
"equation_Spec.SHA2.op384_512", "equation_Spec.SHA2.word_n",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n", "int_inversion", "int_typing",
"kinding_FStar.UInt32.t_@tok", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Seq.Create_Tm_refine_036fb6020f4219ad59b2c9e02e579d2c",
"refinement_interpretation_Spec.SHA2_Tm_refine_a56d4a59fba339ca5210379815875fe9",
"typing_FStar.UInt32.uint_to_t", "typing_Seq.Create.create_12",
"typing_Spec.SHA2.op0"
],
0
],
[
"Spec.SHA2._sigma0",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion",
"constructor_distinct_Spec.SHA2.SHA2_512",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_FStar.UInt8.n",
"equation_Prims.nat", "equation_Spec.Lib.op_String_Access",
"equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256",
"equation_Spec.SHA2.op384_512", "equation_Spec.SHA2.size_word",
"equation_Spec.SHA2.word_n",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Spec.SHA2.op384_512", "int_inversion",
"int_typing", "kinding_FStar.UInt32.t_@tok",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Seq.Create_Tm_refine_036fb6020f4219ad59b2c9e02e579d2c",
"refinement_interpretation_Spec.SHA2_Tm_refine_23e10c6f289fc2dbf6b7252679704f99",
"refinement_interpretation_Spec.SHA2_Tm_refine_a56d4a59fba339ca5210379815875fe9",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_Seq.Create.create_12", "typing_Spec.SHA2.op0",
"typing_Spec.SHA2.size_word"
],
0
],
[
"Spec.SHA2._sigma1",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"data_elim_FStar.UInt64.Mk", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
"equation_FStar.UInt8.n", "equation_Prims.nat",
"equation_Spec.Lib.op_String_Access", "equation_Spec.SHA2.op0",
"equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512",
"equation_Spec.SHA2.size_word", "equation_Spec.SHA2.word",
"equation_Spec.SHA2.word_n",
"fuel_guarded_inversion_FStar.UInt64.t_",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Spec.SHA2.op224_256",
"function_token_typing_Spec.SHA2.op384_512", "int_inversion",
"int_typing", "kinding_FStar.UInt32.t_@tok",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Seq.Create_Tm_refine_036fb6020f4219ad59b2c9e02e579d2c",
"refinement_interpretation_Spec.SHA2_Tm_refine_a56d4a59fba339ca5210379815875fe9",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_Seq.Create.create_12"
],
0
],
[
"Spec.SHA2.k224_256",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.k224_256",
2,
0,
1,
[
"@query", "constructor_distinct_Spec.SHA2.SHA2_256",
"equality_tok_Spec.SHA2.SHA2_256@tok", "equation_Spec.SHA2.size_k_w"
],
0
],
[
"Spec.SHA2.h224",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.h224",
2,
0,
1,
[ "@query", "equation_Spec.SHA2.size_hash_w" ],
0
],
[
"Spec.SHA2.h256",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.h256",
2,
0,
1,
[ "@query", "equation_Spec.SHA2.size_hash_w" ],
0
],
[
"Spec.SHA2.k384_512",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.k384_512",
2,
0,
1,
[
"@query", "constructor_distinct_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_512@tok", "equation_Spec.SHA2.size_k_w"
],
0
],
[
"Spec.SHA2.h384",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.h384",
2,
0,
1,
[ "@query", "equation_Spec.SHA2.size_hash_w" ],
0
],
[
"Spec.SHA2.h512",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.h512",
2,
0,
1,
[ "@query", "equation_Spec.SHA2.size_hash_w" ],
0
],
[
"Spec.SHA2.k0",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok",
"equality_tok_Spec.SHA2.SHA2_512@tok", "equation_FStar.UInt32.t",
"equation_FStar.UInt64.t", "equation_Spec.SHA2.k224_256",
"equation_Spec.SHA2.k384_512", "equation_Spec.SHA2.size_k_w",
"equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_Spec.SHA2.k224_256",
"function_token_typing_Spec.SHA2.k384_512",
"refinement_interpretation_Spec.SHA2_Tm_refine_5192aede6bb68caf43d07d51f049a736",
"refinement_interpretation_Spec.SHA2_Tm_refine_dee9a5878d78d163586b211d15f7586b"
],
0
],
[
"Spec.SHA2.k0",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.h0",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"disc_equation_Spec.SHA2.SHA2_224",
"disc_equation_Spec.SHA2.SHA2_256",
"disc_equation_Spec.SHA2.SHA2_384",
"disc_equation_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_224@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_384@tok",
"equality_tok_Spec.SHA2.SHA2_512@tok", "equation_FStar.UInt32.t",
"equation_FStar.UInt64.t", "equation_Spec.SHA2.h224",
"equation_Spec.SHA2.h256", "equation_Spec.SHA2.h384",
"equation_Spec.SHA2.h512", "equation_Spec.SHA2.size_hash_w",
"equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_Spec.SHA2.h224",
"function_token_typing_Spec.SHA2.h256",
"function_token_typing_Spec.SHA2.h384",
"function_token_typing_Spec.SHA2.h512",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0
],
[
"Spec.SHA2.h0",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.ws",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_62f7433d7b3860092ec12d60810d2dc7_1",
"binder_x_e7c84c8dabcf88f0cc3f76c78c70dea2_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
"equation_Spec.SHA2.size_block_w", "int_inversion", "int_typing",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.SHA2_Tm_refine_3af3bff18f700f32e87e124cbe1b32d7",
"refinement_interpretation_Spec.SHA2_Tm_refine_b3ff6f4df4e7a5b04e8bd7cae749a73e",
"well-founded-ordering-on-nat"
],
0
],
[
"Spec.SHA2.shuffle_core",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.Lib.op_String_Access", "equation_Spec.SHA2.counter",
"equation_Spec.SHA2.hash_w", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.size_hash_w", "equation_Spec.SHA2.word",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Spec.SHA2_Tm_refine_986f9c270132d5f890d11a02a2363e39",
"refinement_interpretation_Spec.SHA2_Tm_refine_b01a3abf8fe93d0e62b65df542fb8b5b",
"refinement_interpretation_Spec.SHA2_Tm_refine_b3ff6f4df4e7a5b04e8bd7cae749a73e",
"refinement_interpretation_Spec.SHA2_Tm_refine_ee814d4e8a4808c214edeec88bbd1a40",
"typing_Spec.SHA2.k0"
],
0
],
[
"Spec.SHA2.shuffle_core",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.shuffle",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.SHA2.size_ws_w",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.SHA2.size_ws_w"
],
0
],
[
"Spec.SHA2.update",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt8.t",
"equation_Prims.nat", "equation_Spec.SHA2.bytes",
"equation_Spec.SHA2.hash_w", "equation_Spec.SHA2.shuffle",
"equation_Spec.SHA2.size_block", "equation_Spec.SHA2.size_block_w",
"equation_Spec.SHA2.size_hash_w", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Spec.SHA2_Tm_refine_2a6f9d99da9f8dc6f84fa5c49ff83a04",
"refinement_interpretation_Spec.SHA2_Tm_refine_b3ff6f4df4e7a5b04e8bd7cae749a73e",
"refinement_interpretation_Spec.SHA2_Tm_refine_d9a92071b9ddac72450889d06ec974b8"
],
0
],
[
"Spec.SHA2.update",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.update_multi",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.update_multi",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Mul.op_Star",
"equation_Spec.SHA2.size_block", "equation_Spec.SHA2.size_block_w",
"equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.SHA2.update_multi",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "binder_x_a66974f5e9035a80f46c72088eeef9c0_0",
"binder_x_d65ca857490311eefa13a728b8c37dea_2", "bool_inversion",
"constructor_distinct_Spec.SHA2.SHA2_256",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Spec.SHA2.SHA2_256@tok", "equation_FStar.Mul.op_Star",
"equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.n",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"equation_Spec.SHA2.bytes", "equation_Spec.SHA2.k224_256",
"equation_Spec.SHA2.size_block", "equation_Spec.SHA2.size_block_w",
"equation_Spec.SHA2.size_k_w", "equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_Spec.SHA2.k224_256", "int_inversion",
"int_typing", "kinding_FStar.UInt32.t_@tok",
"kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "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",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.SHA2_Tm_refine_84a1c1a97d159523644923d8badd3403",
"refinement_interpretation_Spec.SHA2_Tm_refine_cefd9d26c359a9480611ffc2bda20ff8",
"refinement_interpretation_Spec.SHA2_Tm_refine_dee9a5878d78d163586b211d15f7586b",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_Spec.SHA2.size_block", "typing_Spec.SHA2.size_word",
"well-founded-ordering-on-nat"
],
0
],
[
"Spec.SHA2.update_multi",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.update_multi",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.pad0_length",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"equation_FStar.Mul.op_Star", "equation_Prims.nat",
"equation_Spec.SHA2.size_block", "equation_Spec.SHA2.size_block_w",
"equation_Spec.SHA2.size_len_8", "equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.SHA2.pad0_length",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.pad0_length",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.pad",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.Endianness.big_bytes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Spec.SHA2.SHA2_224",
"constructor_distinct_Spec.SHA2.SHA2_256",
"constructor_distinct_Spec.SHA2.SHA2_384",
"constructor_distinct_Spec.SHA2.SHA2_512",
"equality_tok_Spec.SHA2.SHA2_256@tok",
"equality_tok_Spec.SHA2.SHA2_512@tok",
"equation_FStar.Endianness.bytes",
"equation_FStar.Endianness.lbytes",
"equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_FStar.UInt8.n", "equation_FStar.UInt8.t",
"equation_FStar.UInt8.uint_to_t", "equation_Prims.nat",
"equation_Spec.SHA2.h224", "equation_Spec.SHA2.k224_256",
"equation_Spec.SHA2.max_input8", "equation_Spec.SHA2.pad0_length",
"equation_Spec.SHA2.size_block", "equation_Spec.SHA2.size_block_w",
"equation_Spec.SHA2.size_hash_w", "equation_Spec.SHA2.size_len_8",
"equation_Spec.SHA2.size_len_ul_8", "equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Spec.SHA2.h224",
"function_token_typing_Spec.SHA2.k224_256", "int_inversion",
"int_typing", "kinding_FStar.UInt32.t_@tok",
"kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "lemma_Spec.SHA2.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Seq.Create_Tm_refine_fe4495a9f5fcd2ee177e966b5faf7cd8",
"refinement_interpretation_Spec.SHA2_Tm_refine_2218afb41c74e2a0c4f749e6f230c3c5",
"refinement_interpretation_Spec.SHA2_Tm_refine_2d4354035d54798ff2acce250308fd9a",
"refinement_interpretation_Spec.SHA2_Tm_refine_9684aaaba1b62eaf29c01dc9b94c8f93",
"refinement_interpretation_Spec.SHA2_Tm_refine_affec237ff7b6f8c1172e0d265014cb1",
"refinement_interpretation_Spec.SHA2_Tm_refine_bfc750a24876ee4830d5d007a9e6dccc",
"refinement_interpretation_Spec.SHA2_Tm_refine_dee9a5878d78d163586b211d15f7586b",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Seq.Create.create_64",
"typing_Spec.SHA2.pad0_length", "typing_Spec.SHA2.size_block",
"typing_Spec.SHA2.size_len_8", "typing_Spec.SHA2.size_len_ul_8",
"typing_Spec.SHA2.size_word", "typing_tok_Spec.SHA2.SHA2_256@tok",
"typing_tok_Spec.SHA2.SHA2_512@tok"
],
0
],
[
"Spec.SHA2.pad",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.pad",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.pad",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.update_last",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Mul.op_Star",
"equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.UInt8.t",
"equation_Prims.nat", "equation_Spec.SHA2.bytes",
"equation_Spec.SHA2.pad", "equation_Spec.SHA2.size_block",
"equation_Spec.SHA2.size_block_w", "equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg", "int_inversion",
"kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.SHA2_Tm_refine_10bac3ce752214f1a9a982c7e1238a3e",
"refinement_interpretation_Spec.SHA2_Tm_refine_2218afb41c74e2a0c4f749e6f230c3c5",
"refinement_interpretation_Spec.SHA2_Tm_refine_e38d3ead4f62fac064d81779d7dc38a7"
],
0
],
[
"Spec.SHA2.update_last",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.finish",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt8.t",
"equation_Prims.nat", "equation_Spec.Lib.lbytes",
"equation_Spec.SHA2.hash_w", "equation_Spec.SHA2.size_hash",
"equation_Spec.SHA2.size_hash_final_w",
"equation_Spec.SHA2.size_hash_w", "equation_Spec.SHA2.word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.SHA2_Tm_refine_b3ff6f4df4e7a5b04e8bd7cae749a73e",
"typing_Spec.SHA2.size_hash_final_w", "typing_Spec.SHA2.word"
],
0
],
[
"Spec.SHA2.finish",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.finish",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.hash",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion",
"constructor_distinct_Spec.SHA2.SHA2_256",
"equality_tok_Spec.SHA2.SHA2_256@tok", "equation_FStar.Mul.op_Star",
"equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt32.n",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"equation_Spec.SHA2.bytes", "equation_Spec.SHA2.h0",
"equation_Spec.SHA2.size_block", "equation_Spec.SHA2.size_block_w",
"equation_Spec.SHA2.size_hash_w", "equation_Spec.SHA2.size_k_w",
"equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg",
"function_token_typing_FStar.UInt32.n", "int_inversion",
"int_typing", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"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",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.Seq.Properties_Tm_refine_3421154546287b0f0c012dd3d63b4945",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.SHA2_Tm_refine_b3ff6f4df4e7a5b04e8bd7cae749a73e",
"refinement_interpretation_Spec.SHA2_Tm_refine_ee54924869d0ad0a665ff08e754ef482",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_Spec.SHA2.h0", "typing_Spec.SHA2.size_block"
],
0
],
[
"Spec.SHA2.hash",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.hash",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.hash'",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.SHA2.SHA2_256",
"equation_FStar.Mul.op_Star", "equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"equation_Spec.SHA2.bytes", "equation_Spec.SHA2.h0",
"equation_Spec.SHA2.pad", "equation_Spec.SHA2.size_block",
"equation_Spec.SHA2.size_block_w", "equation_Spec.SHA2.size_hash_w",
"equation_Spec.SHA2.size_word",
"fuel_guarded_inversion_Spec.SHA2.hash_alg", "int_inversion",
"kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.SHA2_Tm_refine_10bac3ce752214f1a9a982c7e1238a3e",
"refinement_interpretation_Spec.SHA2_Tm_refine_b3ff6f4df4e7a5b04e8bd7cae749a73e",
"refinement_interpretation_Spec.SHA2_Tm_refine_ee54924869d0ad0a665ff08e754ef482",
"typing_Spec.SHA2.h0", "typing_Spec.SHA2.size_block",
"typing_Spec.SHA2.size_word"
],
0
],
[
"Spec.SHA2.hash'",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.SHA2.hash'",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
]
]
]
Computing file changes ...
