Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Hacl.Hash.Core.SHA1.fst.hints
[
"\u001b�g�O�\u0015���mf6[�",
[
[
"Hacl.Hash.Core.SHA1._h0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"e3b2cd2ef5b8222f1ccc276e725fef7b"
],
[
"Hacl.Hash.Core.SHA1.legacy_alloca",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"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",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Preorder.preorder",
"equation_FStar.Preorder.preorder_rel",
"equation_FStar.Preorder.reflexive", "equation_Lib.IntTypes.uint32",
"equation_LowStar.ImmutableBuffer.immutable_preorder",
"equation_Spec.Agile.Hash.init",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA1.h0",
"equation_Spec.SHA1.init", "equation_Spec.SHA1.init_as_list",
"function_token_typing_Lib.IntTypes.uint32",
"interpretation_Tm_abs_b4ae3c8c313abed48b0c4141f8bc0016",
"refinement_interpretation_Tm_refine_4dd3fe13ba2ac81d13f00faa0949c051",
"refinement_interpretation_Tm_refine_9ca7807bfc284168a2426f4440262824",
"refinement_interpretation_Tm_refine_bd10f09297e0e7dc08314f7d9211801c",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_ee8b234aa6cf07c6ef04345829148435",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_LowStar.ImmutableBuffer.immutable_preorder",
"typing_Spec.SHA1.init_as_list"
],
0,
"ac67ef2e419a82eb105dd81c442f7ba1"
],
[
"Hacl.Hash.Core.SHA1.h0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.SHA1.h0", "equation_Spec.SHA1.init", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0207297b10867c240da10ed929d36896",
"refinement_interpretation_Tm_refine_728e2b11bbc45a9bb5659524bb5e8df3",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Core.SHA1._h0",
"typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.SHA1.init"
],
0,
"3d37ffce3bb916e4024ad6b9258e54ee"
],
[
"Hacl.Hash.Core.SHA1.legacy_init",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"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",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"equation_Spec.Agile.Hash.init",
"equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.SHA1.init",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"int_inversion", "int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_upd",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_135cafc4c407172bc17ed2a0ce14e9ee",
"refinement_interpretation_Tm_refine_24171a21ae8d6250de8142846e764866",
"refinement_interpretation_Tm_refine_4ab971658e114a862c610590eddf8955",
"refinement_interpretation_Tm_refine_4cfac83ca5dc4f4b2f69d62bde44624e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_9e5431dc8b1642920ee351bea45b8660",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Hash.Definitions.word", "typing_Spec.SHA1.init",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"27e02df96e293f341fd6ffc329662d53"
],
[
"Hacl.Hash.Core.SHA1.w_inv'",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@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.Hash.Core.SHA1.w_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Hash.Definitions.word",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"c595a7679e002235edd946098c11bd53"
],
[
"Hacl.Hash.Core.SHA1.w_loop_inv",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Core.SHA1.block_t",
"equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.word_t",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "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_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"997d4c9b69feef897b5be2ce61e67521"
],
[
"Hacl.Hash.Core.SHA1.w_inv_elim",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"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.Hash.Core.SHA1.w_inv_",
"equation_Hacl.Hash.Core.SHA1.w_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Prims.squash", "equation_Spec.Hash.Definitions.word",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"l_and-interp", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Hash.Definitions.word",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"978b021f7dcfb21e2fbb8d63f8b5e21a"
],
[
"Hacl.Hash.Core.SHA1.w_loop_inv_elim",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"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.Hash.Core.SHA1.block_t",
"equation_Hacl.Hash.Core.SHA1.w_inv_",
"equation_Hacl.Hash.Core.SHA1.w_loop_inv",
"equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.word_t",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"l_and-interp", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"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_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"b5f97b52eaa734aea1bac5fd6773198e"
],
[
"Hacl.Hash.Core.SHA1.index_32_be'",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"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.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_AmpAmp", "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_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_05eeb8a0f4055e228bd046054bddb62d",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a2ab50b26a5c765696073ecc7252b93b",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq",
"typing_Lib.ByteSequence.uint_at_index_be",
"typing_Lib.ByteSequence.uints_from_bytes_be",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.mul", "typing_Lib.Sequence.index",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"7af871552323aa6f6f907ba1e88824a8"
],
[
"Hacl.Hash.Core.SHA1.w_body_value",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.SHA1.w_.fuel_instrumented",
"@fuel_irrelevance_Spec.SHA1.w_.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.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt",
"equation_Hacl.Hash.Core.SHA1.block_t",
"equation_Hacl.Hash.Core.SHA1.w_inv_",
"equation_Hacl.Hash.Core.SHA1.w_loop_inv",
"equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.rotval",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA1.w",
"equation_Spec.SHA1.word_block",
"equation_with_fuel_Spec.SHA1.w_.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "l_and-interp", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"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_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_2a9d64ff26e8ce8dfca85e1c63876c34",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_af3524604a4dfd4f05f8932c14c56d0d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e94019ba296cc08a679d3ed9759b4476",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_05e15190c946858f68c69156f585f95a",
"typing_FStar.Ghost.reveal", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_Lib.ByteSequence.uints_from_bytes_be",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.block_word_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"e4c7e98564054fac8bc6011ccbd47019"
],
[
"Hacl.Hash.Core.SHA1.lt_S_r",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"384a0ed9ba7ae763f5e7bc8f2eec41e5"
],
[
"Hacl.Hash.Core.SHA1.w_body",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"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.Hash.Core.SHA1.block_t",
"equation_Hacl.Hash.Core.SHA1.w_inv_",
"equation_Hacl.Hash.Core.SHA1.w_loop_inv",
"equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.word_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"int_inversion",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"l_and-interp",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "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_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5fafc2da9e45e4cc64ee84722312dc27",
"refinement_interpretation_Tm_refine_703a7d2fe02b9ca7064a2cc5d0ed1a46",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_e94019ba296cc08a679d3ed9759b4476",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_05e15190c946858f68c69156f585f95a",
"true_interp", "typing_FStar.Ghost.reveal", "typing_FStar.UInt32.v",
"typing_Lib.ByteSequence.uints_from_bytes_be",
"typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.block_word_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"3570190bf456a2668c71eb7bf8794385"
],
[
"Hacl.Hash.Core.SHA1.w",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"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.Hash.Core.SHA1.block_t",
"equation_Hacl.Hash.Core.SHA1.w_inv",
"equation_Hacl.Hash.Core.SHA1.w_inv_",
"equation_Hacl.Hash.Core.SHA1.w_loop_inv",
"equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.word_t",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"l_and-interp", "lemma_FStar.Ghost.reveal_hide",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_AmpAmp", "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_4b12a172e671bfbe6a27d14190000803",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_d9a69009508517dad67f8347944dbb2f",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_05e15190c946858f68c69156f585f95a",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"8d79871098f2bb0960fb4ec6e46428ef"
],
[
"Hacl.Hash.Core.SHA1.upd5",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0575197a5bfbce094fbbc4752d6f0a83",
"refinement_interpretation_Tm_refine_47f7d72cb804a2caca3569d60da54e94",
"refinement_interpretation_Tm_refine_482b06e5a74271bbd8c3d69550d68f59",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_544f8a10e8878f55a9f2150d7d422a71",
"refinement_interpretation_Tm_refine_93cc928978a8436a38153dd4de924396",
"refinement_interpretation_Tm_refine_cadd301a6914616c995234a1c6ddfae6",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"true_interp", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"46749b6c155bd8c1adf0b15d1119bc34"
],
[
"Hacl.Hash.Core.SHA1.step3_body",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Ghost_interpretation_Tm_ghost_arrow_e2f4c1991753137c5a80c115428d0cef",
"Spec.SHA1_interpretation_Tm_arrow_5179a47a8889eaf0f9b968a3cecd04b1",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@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.Hash.Core.SHA1.w_inv",
"equation_Hacl.Hash.Core.SHA1.w_inv_",
"equation_Hacl.Hash.Core.SHA1.w_t",
"equation_Hacl.Hash.Definitions.state", "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_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA1.step3_body__aux",
"equation_Spec.SHA1.step3_body_w_t", "equation_Spec.SHA1.w",
"equation_Spec.SHA1.word_block",
"function_token_typing_FStar.Ghost.reveal",
"function_token_typing_Spec.SHA1.step3_body_",
"function_token_typing_Spec.SHA1.word_block", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"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_1a7342538ca80f9d26af1465da683bf7",
"refinement_interpretation_Tm_refine_457b459ca55b425569fac95945d04d19",
"refinement_interpretation_Tm_refine_4ab971658e114a862c610590eddf8955",
"refinement_interpretation_Tm_refine_50f3dcb312c61cacd85d8a19ef243108",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703a7d2fe02b9ca7064a2cc5d0ed1a46",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.Ghost.reveal",
"token_correspondence_Spec.SHA1.step3_body__aux",
"typing_FStar.Ghost.reveal",
"typing_FStar.Seq.Properties.seq_of_list", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.SHA1.step3_body_w_t",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"c3f8bb9b40fbc332e42042c549f7877e"
],
[
"Hacl.Hash.Core.SHA1.zero_out",
1,
0,
0,
[ "@query" ],
0,
"58a2425eb7c7cc46d7e9fe162356278f"
],
[
"Hacl.Hash.Core.SHA1.zero_out",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1dadea411cd6aea069a22f4ce6ad367e",
"refinement_interpretation_Tm_refine_22ea23156c96d1f95a36c1bf3ce83086",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_85b64abb9c2f68e7bad1761e265ecae9",
"refinement_interpretation_Tm_refine_879c0531660edf141e05adab3475474e",
"refinement_interpretation_Tm_refine_f00f8a5027d18e4477fe20cd6a8e47aa",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.Definitions.word",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"5cc6228d56918af96754f88de41b19a7"
],
[
"Hacl.Hash.Core.SHA1.spec_step3_body_spec",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Hacl.Hash.Core.SHA1_interpretation_Tm_ghost_arrow_6da11f406a8292b335e053b0d15044e2",
"Prims_interpretation_Tm_ghost_arrow_0283b8a2a36bbec52abac4e3d837674a",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Hacl.Hash.Core.SHA1.spec_step3_body", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.words_state", "int_inversion",
"interpretation_Tm_abs_f64027353d7621d991a0c7b6f4f5db11",
"refinement_interpretation_Tm_refine_457b459ca55b425569fac95945d04d19",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_785b445c1ccb59eaa8c666ff5bddec28",
"typing_FStar.Ghost.elift1",
"typing_Spec.Hash.Definitions.words_state",
"typing_Tm_abs_f64027353d7621d991a0c7b6f4f5db11",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"0e4b3d8772c17686c8e97158f4fcb0c3"
],
[
"Hacl.Hash.Core.SHA1.step3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Ghost_interpretation_Tm_ghost_arrow_e2f4c1991753137c5a80c115428d0cef",
"Prims_interpretation_Tm_ghost_arrow_0283b8a2a36bbec52abac4e3d837674a",
"Spec.Loops_interpretation_Tm_arrow_991012978bfe18b65525b7a05d6a8a37",
"Spec.SHA1_interpretation_Tm_arrow_5deff49f7f1856fb39cedfc46d8ece6e",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "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.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_C.Loops.repeat_range_body_spec",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"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.Hash.Core.SHA1.block_t",
"equation_Hacl.Hash.Core.SHA1.w_inv",
"equation_Hacl.Hash.Core.SHA1.w_inv_",
"equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.SHA1.compute_w_post",
"equation_Spec.SHA1.index_compute_w", "equation_Spec.SHA1.step3_aux",
"equation_Spec.SHA1.step3_body", "equation_Spec.SHA1.step3_body_w_t",
"equation_Spec.SHA1.word_block",
"function_token_typing_FStar.Ghost.reveal",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"function_token_typing_Spec.SHA1.step3",
"function_token_typing_Spec.SHA1.step3_body",
"function_token_typing_Spec.SHA1.word_block",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.v_injective",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_457b459ca55b425569fac95945d04d19",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6ba711c7854d10c818e9d6022d656341",
"refinement_interpretation_Tm_refine_785b445c1ccb59eaa8c666ff5bddec28",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_85b64abb9c2f68e7bad1761e265ecae9",
"refinement_interpretation_Tm_refine_942729fd9703f37ca311a66f05cb2165",
"refinement_interpretation_Tm_refine_998ed54a258fc4b011af23dea8b4c8b1",
"refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d357a34950e2c18698620c6db0dd1449",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_d9a69009508517dad67f8347944dbb2f",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_862db9fdbb465abbf62ca2339d2eb474",
"token_correspondence_FStar.Ghost.reveal",
"token_correspondence_Spec.SHA1.index_compute_w",
"token_correspondence_Spec.SHA1.step3_aux",
"token_correspondence_Spec.SHA1.step3_body",
"typing_C.Loops.repeat_range_body_spec", "typing_FStar.Ghost.elift1",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Map.restrict",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Seq.Base.empty", "typing_FStar.Set.complement",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.Set.union", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t",
"typing_Spec.Hash.Definitions.words_state",
"typing_Spec.SHA1.step3_body_w_t",
"typing_Tm_abs_ed4cda90676a02d35713650cfe70afa7",
"typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"49945600b649f9d3e0968cefa2cbe0bd"
],
[
"Hacl.Hash.Core.SHA1.step4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.block_t",
"equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"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_length",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.SHA1.step4_aux", "equation_Spec.SHA1.word_block",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.SHA1.step4", "int_inversion",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "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_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_4ab971658e114a862c610590eddf8955",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_d9a69009508517dad67f8347944dbb2f",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Spec.SHA1.step4_aux", "typing_FStar.UInt32.v",
"typing_Lib.ByteSequence.uints_from_bytes_be",
"typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.block_word_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA1.step4",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"2c3bfb08aa2b790941aefdbcb6d6884a"
],
[
"Hacl.Hash.Core.SHA1.legacy_update",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.Hash_interpretation_Tm_arrow_9511bb3e8dd03332bdc255a2a2621d89",
"Spec.Hash.Definitions_interpretation_Tm_arrow_3919213edab5530de5a42c49ef9baf98",
"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",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Hacl.Hash.Definitions.state",
"equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Spec.Agile.Hash.update",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.update_t",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_of_bytes",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.SHA1.update", "equation_Spec.SHA1.update_aux",
"equation_Spec.SHA1.words_of_bytes_block",
"function_token_typing_Lib.ByteSequence.uints_from_bytes_be",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.Agile.Hash.update",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"refinement_interpretation_Tm_refine_106b7d32cbd2cbaf6ef5c427df6f1bcd",
"refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe",
"refinement_interpretation_Tm_refine_d9a69009508517dad67f8347944dbb2f",
"token_correspondence_Spec.Agile.Hash.update",
"token_correspondence_Spec.Hash.Definitions.words_of_bytes",
"token_correspondence_Spec.SHA1.update_aux",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.Definitions.word",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"7b36e01a2c74b932a924f93a79ff5a47"
]
]
]
Computing file changes ...
