Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
Spec.MD5.fst.hints
[
"\"\u0002g\u0014�k�ݖ�Ŝ1\b�\u0000",
[
[
"Spec.MD5.init_as_list",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "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_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"325fa2652159bb6eed66a03c60443991"
],
[
"Spec.MD5.init",
1,
8,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"data_elim_Prims.Cons", "data_typing_intro_Prims.Nil@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_Lib.IntTypes.uint32", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.MD5.init_as_list",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint32", "int_inversion",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.List.Tot.Base.length", "typing_Spec.MD5.init_as_list"
],
0,
"bbd8259127e2e98fe863622685c6ca89"
],
[
"Spec.MD5.t_as_list",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "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_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d7defbc6e2f37807ed5cffc3c3777a02"
],
[
"Spec.MD5.t",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint32",
"equation_Spec.MD5.t_as_list",
"function_token_typing_Lib.IntTypes.uint32",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_Spec.MD5.t_as_list"
],
0,
"b38845b3a36f86228ea693acc39f09eb"
],
[
"Spec.MD5.round_op_gen_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.MD5.abcd_idx", "equation_Spec.MD5.abcd_t",
"equation_Spec.MD5.t", "equation_Spec.MD5.t_idx",
"equation_Spec.MD5.x_idx", "equation_Spec.MD5.x_t",
"function_token_typing_Lib.IntTypes.uint32", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_upd",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c2b2f0397c6f216bb58dc34f34f2bdfe",
"refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f",
"typing_Spec.MD5.t"
],
0,
"7457396fffc68d187ddf3bdfc4a1f1b9"
],
[
"Spec.MD5.round1_aux",
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_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"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_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.MD5.rotate_idx", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
"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_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"9cfa74ab4de1aa643650a5cf1830981a"
],
[
"Spec.MD5.round2_aux",
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_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"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_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.MD5.rotate_idx", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
"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_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8ca4b522b3e70dea04b5e8df93705b28"
],
[
"Spec.MD5.round3_aux",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.MD5.rotate_idx", "equation_Spec.MD5.x_t",
"function_token_typing_Lib.IntTypes.uint32", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
"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_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt32.uint_to_t"
],
0,
"79be46ef9b3cd134e458c954569c1b77"
],
[
"Spec.MD5.round4_aux",
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_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"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_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.MD5.rotate_idx", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
"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_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ef750efcd80b863a1663017dd12c73ab"
],
[
"Spec.MD5.overwrite_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.uint32",
"equation_Spec.MD5.abcd_idx", "equation_Spec.MD5.abcd_t",
"equation_Spec.MD5.ia", "equation_Spec.MD5.ib",
"equation_Spec.MD5.ic", "equation_Spec.MD5.id",
"function_token_typing_Lib.IntTypes.uint32",
"lemma_FStar.Seq.Base.lemma_len_upd",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"f3c7f2c461fa4c1b8b86de36d3e2ee0b"
],
[
"Spec.MD5.update_aux",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.word_length",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"f752dc67884e479a60b6d90ce454bbd1"
],
[
"Spec.MD5.update_aux",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.MD5.abcd_t",
"equation_Spec.MD5.ia", "equation_Spec.MD5.ib",
"equation_Spec.MD5.ic", "equation_Spec.MD5.id", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_acdad29ca25b25c98ec14726b3dbe3d6",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8cdedfc8b701357cbd8a161a4efda0d5"
],
[
"Spec.MD5.update",
1,
2,
1,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t"
],
0,
"594166ca0fa95c8ac9ddbf24dafb82e0"
],
[
"Spec.MD5.finish",
1,
2,
1,
[ "@query" ],
0,
"6de6ddcfb96a58293e04449968d3e729"
]
]
]
Computing file changes ...
