Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.SHA.SHA_helpers.fst.hints
[
"\u001a�\u0000ll\u000f\rdyo\u0004�\u001f��",
[
[
"Vale.SHA.SHA_helpers.vv",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"cc304368fe27b6c0ea97a1e33ed2f5be"
],
[
"Vale.SHA.SHA_helpers.to_uint32",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"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", "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,
"9997da3b449a8c511e1faa7bcfa4c550"
],
[
"Vale.SHA.SHA_helpers.k",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.List.Tot.Properties.llist",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.size_k_w", "equation_Vale.SHA.SHA_helpers.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"typing_Spec.SHA2.Constants.k224_256",
"typing_Spec.SHA2.Constants.k224_256_l"
],
0,
"5186114ab7cb4529c4b82e0e51dbf086"
],
[
"Vale.SHA.SHA_helpers.reveal_word",
1,
0,
0,
[ "@query", "equation_Vale.SHA.SHA_helpers.word" ],
0,
"d349407746f55c9e62dd9dbb821d877c"
],
[
"Vale.SHA.SHA_helpers.bytes_blocks",
1,
0,
0,
[
"@query", "equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"projection_inverse_BoxInt_proj_0"
],
0,
"3ad46766f0d67f89f6ae62a8d1807192"
],
[
"Vale.SHA.SHA_helpers.add_mod_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.IntTypes.unsigned", "primitive_Prims.op_AmpAmp",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v"
],
0,
"9c38202ea361bbe2d1d3cd0537e96a1f"
],
[
"Vale.SHA.SHA_helpers.add_mod_lemma",
2,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.add_mod"
],
0,
"46490da92d07002de5690f02898a8b32"
],
[
"Vale.SHA.SHA_helpers.ws_opaque",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2.size_k_w",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413"
],
0,
"87e9e48db830cb63c371aa25b99d389d"
],
[
"Vale.SHA.SHA_helpers.shuffle_core_opaque",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2.size_k_w",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"6c6a85a4548729cba0935c3f1d68b2e1"
],
[
"Vale.SHA.SHA_helpers.update_multi_reveal",
1,
0,
0,
[ "@query" ],
0,
"dc84b3f67900eb0f45b2cb759f977ade"
],
[
"Vale.SHA.SHA_helpers.update_multi_opaque",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t",
"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_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.bytes_blocks",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3891824b4d5874bf21bffea346ced817",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"783e09b4d788de6ad489dd57ff724d3f"
],
[
"Vale.SHA.SHA_helpers.update_multi_transparent",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t",
"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_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.bytes_blocks",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3891824b4d5874bf21bffea346ced817",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"1ba36556584dd69a095820a8f5e0d253"
],
[
"Vale.SHA.SHA_helpers.byte_to_nat8",
1,
0,
0,
[
"@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_Prims.nat", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"33217e8248b2a8a158e358180dbf3772"
],
[
"Vale.SHA.SHA_helpers.nat8_to_byte",
1,
0,
0,
[
"@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_Prims.nat", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"9c3515e54b0d25525a7b7a0c8552be7c"
],
[
"Vale.SHA.SHA_helpers.repeat_range_vale",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c6633917f79a67f4eaac4ed70320fc6"
],
0,
"ebbd0cec02cf0715a83314f4119bf460"
],
[
"Vale.SHA.SHA_helpers.lemma_repeat_range_0_vale",
1,
0,
0,
[ "@query" ],
0,
"c0f732a0405c6192ca4ef3a45d7cab43"
],
[
"Vale.SHA.SHA_helpers.update_multi_opaque_vale",
1,
0,
0,
[
"@query", "equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"202c06aeb92282dd3c19a68d3819a6c8"
],
[
"Vale.SHA.SHA_helpers.make_hash_def",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_Spec.Hash.Definitions.word",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"e843699c09a6b054c71dba4e853c6585"
],
[
"Vale.SHA.SHA_helpers.make_hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.SHA.SHA_helpers.hash256",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"db4ca8fec18c732626251382741538ea"
],
[
"Vale.SHA.SHA_helpers.make_hash",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_8cf13b3d7099fa3705dae664b3780000",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"9368a20a4f1cc8be5d480a1010932eed"
],
[
"Vale.SHA.SHA_helpers.make_hash_reveal",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_8cf13b3d7099fa3705dae664b3780000",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"c3d5016ab2b10806219b6348b57e0289"
],
[
"Vale.SHA.SHA_helpers.make_ordered_hash_def",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_Spec.Hash.Definitions.word",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"eadfaf2515722fd7ca15f3e528418ec5"
],
[
"Vale.SHA.SHA_helpers.make_ordered_hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.SHA.SHA_helpers.hash256",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"afa29af808f2f116c88d6f29aa5d4eed"
],
[
"Vale.SHA.SHA_helpers.make_ordered_hash",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_981e3eec9d5a51798e689e2b247f6e8c",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"ce73d5d78b0046af8757b9a02fc4e7cc"
],
[
"Vale.SHA.SHA_helpers.make_ordered_hash_reveal",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.Hash.Definitions.words_state",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_981e3eec9d5a51798e689e2b247f6e8c",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"b4bc2d62ff6d7ec52cc8338b1bd88497"
],
[
"Vale.SHA.SHA_helpers.shuffle_core_properties",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.List.Tot.Properties.llist",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2.Lemmas.shuffle_core_", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.size_k_w",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.shuffle_core_opaque",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_Prims.int",
"function_token_typing_Spec.SHA2.Lemmas.shuffle_core",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"token_correspondence_Lib.IntTypes.add_mod",
"token_correspondence_Spec.SHA2.Lemmas.shuffle_core_",
"token_correspondence_Spec.SHA2.op_Plus_Dot",
"typing_Spec.SHA2.Constants.k224_256",
"typing_Spec.SHA2.Constants.k224_256_l",
"typing_Vale.SHA.SHA_helpers.shuffle_core_opaque"
],
0,
"a6035253eebeb02be0b822110fa8f70b"
],
[
"Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
1,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"52229fa9d8dfa5a7c3e3c1d661eff0f6"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_rnds2_spec_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
"equation_Lib.IntTypes.v", "equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
"equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
"equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.op_Amp_Dot",
"equation_Spec.SHA2.op_Hat_Dot", "equation_Spec.SHA2.op_Tilde_Dot",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_quad32",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_def",
"equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Lib.IntTypes.logand",
"function_token_typing_Lib.IntTypes.logxor",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec",
"lemma_Lib.IntTypes.v_injective",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"token_correspondence_Lib.IntTypes.logand",
"token_correspondence_Lib.IntTypes.lognot",
"token_correspondence_Lib.IntTypes.logxor",
"token_correspondence_Spec.SHA2.op_Amp_Dot",
"token_correspondence_Spec.SHA2.op_Hat_Dot",
"token_correspondence_Spec.SHA2.op_Tilde_Dot",
"token_correspondence_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_def",
"typing_FStar.UInt32.add_mod", "typing_Lib.IntTypes.logand",
"typing_Lib.IntTypes.lognot", "typing_Lib.IntTypes.logxor",
"typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2._Sigma0",
"typing_Spec.SHA2._Sigma1",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.make_hash",
"typing_Vale.SHA.SHA_helpers.nat32_to_word",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_Vale.SHA.SHA_helpers.vv", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"e87a919ea610018f80578bdb312cf1c4"
],
[
"Vale.SHA.SHA_helpers.lemma_add_mod_commutes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt.add_mod",
"lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"typing_FStar.UInt32.add_mod"
],
0,
"2263f571da8d096d8d58f6effd72dae7"
],
[
"Vale.SHA.SHA_helpers.lemma_add_mod_associates_U32",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.add_mod",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.IntTypes.add_mod", "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.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.add_mod", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"dcf9a9ae5d4d1326b5b421172cf18105"
],
[
"Vale.SHA.SHA_helpers.lemma_add_wrap_is_add_mod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.add_mod",
"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.mk_int",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv", "int_inversion", "int_typing",
"lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.add_mod",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"f3a8744d7230d9bdb704b10a323e76d7"
],
[
"Vale.SHA.SHA_helpers.add_wrap_commutes",
1,
0,
0,
[ "@query", "equation_Vale.Def.Types_s.add_wrap" ],
0,
"fe4cc1ba4cc530a45297c9c34dbc99ae"
],
[
"Vale.SHA.SHA_helpers.lemma_add_mod_a",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.is_sha2",
"projection_inverse_BoxBool_proj_0"
],
0,
"4c89f58953ec776103c48f14e57eed91"
],
[
"Vale.SHA.SHA_helpers.lemma_add_mod_e",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.UInt.add_mod", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
"equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.op_Hat_Dot",
"lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"token_correspondence_Spec.SHA2.op_Hat_Dot",
"typing_FStar.UInt32.add_mod"
],
0,
"33fdf65754defc0b054a133df98d16a0"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_rnds2_spec_update_is_shuffle_core",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868",
"Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb",
"Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7",
"b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
"equation_Lib.IntTypes.v", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2.Lemmas.shuffle_core_", "equation_Spec.SHA2._Ch",
"equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
"equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.block_w",
"equation_Spec.SHA2.counter", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.op_Amp_Dot", "equation_Spec.SHA2.op_Hat_Dot",
"equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.op_Tilde_Dot",
"equation_Spec.SHA2.size_k_w",
"equation_Vale.SHA.SHA_helpers.add_mod32",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.shuffle_core_opaque",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.SHA.SHA_helpers.ws_opaque",
"equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Prims.int",
"function_token_typing_Spec.SHA2.Lemmas.shuffle_core",
"function_token_typing_Spec.SHA2.op_Plus_Dot",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"l_and-interp", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.v_injective",
"lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca",
"refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"token_correspondence_Lib.IntTypes.add_mod",
"token_correspondence_Lib.IntTypes.logand",
"token_correspondence_Lib.IntTypes.lognot",
"token_correspondence_Lib.IntTypes.logxor",
"token_correspondence_Spec.SHA2.Lemmas.shuffle_core_",
"token_correspondence_Spec.SHA2.op_Amp_Dot",
"token_correspondence_Spec.SHA2.op_Hat_Dot",
"token_correspondence_Spec.SHA2.op_Plus_Dot",
"token_correspondence_Spec.SHA2.op_Tilde_Dot",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
"typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.lognot",
"typing_Lib.IntTypes.logxor", "typing_Spec.Hash.Definitions.word",
"typing_Spec.SHA2.Constants.k224_256", "typing_Spec.SHA2.Lemmas.ws",
"typing_Spec.SHA2._Ch", "typing_Spec.SHA2._Maj",
"typing_Spec.SHA2._Sigma0", "typing_Spec.SHA2._Sigma1",
"typing_Spec.SHA2.k0", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"6a561250f57a99aaced26817c94866cf"
],
[
"Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_core_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.hash256", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"typing_Vale.SHA.SHA_helpers.shuffle_core_opaque"
],
0,
"2f762b6cedd85d4cd474bb8872d52d6c"
],
[
"Vale.SHA.SHA_helpers.lemma_rnds_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.size_k_w",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_core_quad32",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413"
],
0,
"dcca73a5e07dcd2d696058cdd134ecb5"
],
[
"Vale.SHA.SHA_helpers.lemma_rnds2_spec_quad32_is_shuffle_core_x2",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44",
"Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
"equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
"equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.op_Amp_Dot", "equation_Spec.SHA2.op_Hat_Dot",
"equation_Spec.SHA2.op_Tilde_Dot", "equation_Spec.SHA2.size_k_w",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.SHA.SHA_helpers.add_mod32",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.make_hash",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_core_quad32",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Lib.IntTypes.logand",
"function_token_typing_Lib.IntTypes.logxor",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.pow2_2", "lemma_Lib.IntTypes.v_injective",
"lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
"refinement_interpretation_Tm_refine_d60a0e9fdf52cedb444de54cc40036f8",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"token_correspondence_Lib.IntTypes.logand",
"token_correspondence_Lib.IntTypes.lognot",
"token_correspondence_Lib.IntTypes.logxor",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Spec.SHA2.op_Amp_Dot",
"token_correspondence_Spec.SHA2.op_Hat_Dot",
"token_correspondence_Spec.SHA2.op_Tilde_Dot",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
"typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.lognot",
"typing_Lib.IntTypes.logxor", "typing_Lib.IntTypes.minint",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.SHA2.Constants.k224_256", "typing_Spec.SHA2._Sigma0",
"typing_Spec.SHA2._Sigma1", "typing_Spec.SHA2.k0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.make_hash",
"typing_Vale.SHA.SHA_helpers.nat32_to_word",
"typing_Vale.SHA.SHA_helpers.shuffle_core_opaque",
"typing_Vale.SHA.SHA_helpers.vv", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"d3983b0cef0723ee995a3492b0478a42"
],
[
"Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32_x2_shifts",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868",
"Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"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.range",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
"equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
"equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.op_Amp_Dot",
"equation_Spec.SHA2.op_Hat_Dot", "equation_Spec.SHA2.op_Tilde_Dot",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Lib.IntTypes.logand",
"function_token_typing_Lib.IntTypes.logxor",
"function_token_typing_Vale.Def.Words_s.nat32",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective",
"lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"token_correspondence_Lib.IntTypes.logand",
"token_correspondence_Lib.IntTypes.lognot",
"token_correspondence_Lib.IntTypes.logxor",
"token_correspondence_Spec.SHA2.op_Amp_Dot",
"token_correspondence_Spec.SHA2.op_Hat_Dot",
"token_correspondence_Spec.SHA2.op_Tilde_Dot",
"typing_FStar.UInt32.add_mod", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.lognot",
"typing_Lib.IntTypes.logxor", "typing_Spec.SHA2._Sigma0",
"typing_Spec.SHA2._Sigma1",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.make_hash",
"typing_Vale.SHA.SHA_helpers.nat32_to_word",
"typing_Vale.SHA.SHA_helpers.vv", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"786cead07882212c89c34c1e5462bc68"
],
[
"Vale.SHA.SHA_helpers.sha256_rnds2_spec_quad32_is_shuffle_core_x2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.add_mod32",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_quad32",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.SHA.SHA_helpers.ws_opaque",
"fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
"int_typing", "lemma_Lib.IntTypes.v_injective",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca",
"refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
"typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.k0",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_Vale.SHA.SHA_helpers.ws_opaque",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"5d3c5a78a86e7c01894a7d4014dc526c"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_rnds2_two_steps",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.squash", "equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2.k0",
"equation_Spec.SHA2.size_k_w",
"equation_Vale.SHA.SHA_helpers.add_mod32",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.ws_opaque", "int_inversion",
"l_and-interp", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c124008fc327788c7ae91c746355ecc5"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_rnds2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.k", "l_and-interp",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
"typing_Vale.SHA.SHA_helpers.k"
],
0,
"f76f72d46672926212c8616cae529bf3"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_rnds2",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2.size_k_w",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.k",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.SHA.SHA_helpers.word_to_nat32", "int_inversion",
"l_and-interp", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
"refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
"typing_Vale.SHA.SHA_helpers.k"
],
0,
"e3b592c5a91503d1dda464a74ef53078"
],
[
"Vale.SHA.SHA_helpers.ws_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"4a6a49cc25729b58c8eb0575f02e96a3"
],
[
"Vale.SHA.SHA_helpers._sigma0_quad32",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.is_sha2",
"projection_inverse_BoxBool_proj_0"
],
0,
"5a32304715e93d4cfc9f6d45e87d61f7"
],
[
"Vale.SHA.SHA_helpers._sigma1_quad32",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.is_sha2",
"projection_inverse_BoxBool_proj_0"
],
0,
"4e13e32f049910738448afa7edea60ab"
],
[
"Vale.SHA.SHA_helpers.ws_partial_def",
1,
0,
0,
[
"@query", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"dd8b0b89de664b9cca6acc1a03e1db5b"
],
[
"Vale.SHA.SHA_helpers.ws_partial_reveal",
1,
0,
0,
[ "@query" ],
0,
"e0ad801d79d8e963326ff2ffbe79339e"
],
[
"Vale.SHA.SHA_helpers.lemma_add_wrap_quad32_is_add_mod_quad32",
1,
0,
0,
[
"@query", "equation_Vale.Arch.Types.add_wrap_quad32",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.add_mod_quad32",
"function_token_typing_Vale.Def.Words_s.nat32",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1"
],
0,
"b55a2c7e1f5500ee47738f5978a2f191"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg1",
1,
0,
0,
[ "@query" ],
0,
"1782e453a0d76f6f2f383baf6f37d6f9"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2._sigma0", "equation_Spec.SHA2.size_k_w",
"equation_Vale.Arch.Types.add_wrap_quad32",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers._sigma0_quad32",
"equation_Vale.SHA.SHA_helpers.add_mod_quad32",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.ws_partial_def",
"equation_Vale.SHA.SHA_helpers.ws_quad32",
"equation_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.SHA.SHA_helpers.ws_partial",
"function_token_typing_Vale.X64.CryptoInstructions_s.sha256_msg1_spec",
"int_inversion", "int_typing", "lemma_FStar.UInt32.uv_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.SHA.SHA_helpers.ws_partial_def",
"token_correspondence_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
"typing_Spec.SHA2._sigma0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"795879827d7b468e22966553d9cb7d99"
],
[
"Vale.SHA.SHA_helpers.lemma_add_mod_ws_rearrangement",
1,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.add_mod",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"7d42d79508e8c84442d18604b34b59c0"
],
[
"Vale.SHA.SHA_helpers.ws_computed",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"primitive_Prims.op_LessThan", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"typing_Lib.IntTypes.unsigned",
"typing_Spec.Hash.Definitions.is_sha2",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"b3dad50df8c5023e6ba134c5efac3011"
],
[
"Vale.SHA.SHA_helpers.lemma_ws_computed_is_ws",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
"@fuel_irrelevance_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.add_mod", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.v",
"equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2._sigma1", "equation_Spec.SHA2.block_w",
"equation_Spec.SHA2.counter", "equation_Spec.SHA2.op_Plus_Dot",
"equation_Spec.SHA2.size_k_w",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.SHA.SHA_helpers.ws_computed",
"equation_Vale.SHA.SHA_helpers.ws_opaque",
"equation_with_fuel_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
"function_token_typing_Spec.SHA2.Lemmas.ws", "int_inversion",
"lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.v_injective",
"lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"token_correspondence_Lib.IntTypes.add_mod",
"token_correspondence_Spec.SHA2.Lemmas.ws_aux",
"token_correspondence_Spec.SHA2.op_Plus_Dot",
"typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2.Lemmas.ws",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"960ec44c44eb540c0ea57ecabf2da1d6"
],
[
"Vale.SHA.SHA_helpers.lemma_ws_computed_is_ws_opaque",
1,
0,
0,
[ "@query", "equation_Vale.SHA.SHA_helpers.ws_opaque" ],
0,
"ec22b01e9e9d61a05fd82ec115fe24eb"
],
[
"Vale.SHA.SHA_helpers.ws_computed_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3e5c61bca107489f496b1a6560516d19",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"fa7263d49578331e8cb0ce4ebd00017a"
],
[
"Vale.SHA.SHA_helpers.lemma_ws_computed_is_ws_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.ws_computed_quad32",
"equation_Vale.SHA.SHA_helpers.ws_quad32",
"primitive_Prims.op_LessThan", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3e5c61bca107489f496b1a6560516d19",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"9c09e86ea99fd4b94dbb20a745217bec"
],
[
"Vale.SHA.SHA_helpers.lemma_ws_computed_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"bool_inversion", "constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2._sigma0", "equation_Spec.SHA2._sigma1",
"equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
"equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers._sigma0_quad32",
"equation_Vale.SHA.SHA_helpers._sigma1_quad32",
"equation_Vale.SHA.SHA_helpers.add_mod_quad32",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.SHA.SHA_helpers.ws_computed",
"equation_Vale.SHA.SHA_helpers.ws_computed_quad32",
"equation_Vale.SHA.SHA_helpers.ws_opaque",
"equation_Vale.SHA.SHA_helpers.ws_quad32",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.v_injective",
"lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8606f8c053de9c08417ea96222333455",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
"refinement_interpretation_Tm_refine_d60a0e9fdf52cedb444de54cc40036f8",
"typing_FStar.UInt32.add_mod", "typing_Lib.IntTypes.add_mod",
"typing_Lib.IntTypes.unsigned",
"typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2._sigma0",
"typing_Spec.SHA2._sigma1", "typing_Spec.SHA2.ws",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers._sigma0_quad32",
"typing_Vale.SHA.SHA_helpers.add_mod_quad32",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_Vale.SHA.SHA_helpers.ws_quad32",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"f4e52d374d7408168abe9d779f29a8b3"
],
[
"Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb"
],
0,
"9a48cadb540bc2ed41b873a4a8510166"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg1_spec_t_partial",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.ws_partial_def",
"function_token_typing_Vale.SHA.SHA_helpers.ws_partial",
"int_inversion", "l_and-interp", "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_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.SHA.SHA_helpers.ws_partial_def"
],
0,
"caab7f06895d865e5df195bdb19829d2"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg1_spec_t",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2._sigma0", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers._sigma0_quad32",
"equation_Vale.SHA.SHA_helpers.add_mod_quad32",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.ws_opaque",
"equation_Vale.SHA.SHA_helpers.ws_quad32",
"equation_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.X64.CryptoInstructions_s.sha256_msg1_spec",
"int_inversion", "l_and-interp", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
"typing_Spec.SHA2._sigma0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"e2e09efb1b335e00e9ac5af66a12f614"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_step2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2._sigma0", "equation_Spec.SHA2._sigma1",
"equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
"equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers._sigma0_quad32",
"equation_Vale.SHA.SHA_helpers.add_mod_quad32",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.SHA.SHA_helpers.ws_computed",
"equation_Vale.SHA.SHA_helpers.ws_computed_quad32",
"equation_Vale.SHA.SHA_helpers.ws_opaque",
"equation_Vale.SHA.SHA_helpers.ws_quad32",
"equation_Vale.X64.CryptoInstructions_s.sha256_msg2_spec_def",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.X64.CryptoInstructions_s.sha256_msg2_spec",
"int_inversion", "int_typing", "l_and-interp",
"lemma_Lib.IntTypes.v_injective",
"lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb",
"token_correspondence_Vale.X64.CryptoInstructions_s.sha256_msg2_spec_def",
"typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.unsigned",
"typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2.Lemmas.ws",
"typing_Spec.SHA2._sigma0", "typing_Spec.SHA2._sigma1",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.to_uint32",
"typing_Vale.SHA.SHA_helpers.ws_opaque",
"typing_Vale.SHA.SHA_helpers.ws_quad32",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"da0316dc3526e946e8b8a2cf57412e0f"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg2",
1,
0,
0,
[ "@query" ],
0,
"c13df75087773a39acdcf67b567ad3b5"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg2",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.SHA2.size_k_w", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"96032b2da3067ffcdbefd9f428e69fc4"
],
[
"Vale.SHA.SHA_helpers.k_reqs",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.SHA.SHA_helpers.k",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_07420f653b2652e2852306d7d9338f6d",
"refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
"typing_Vale.SHA.SHA_helpers.k"
],
0,
"807fc9e20580250238d387b74422bdb6"
],
[
"Vale.SHA.SHA_helpers.quads_to_block",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint32",
"equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_Lib.IntTypes.uint32", "int_typing",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"fce6660c5e4aa55fd5795baf7a206a30"
],
[
"Vale.SHA.SHA_helpers.lemma_quads_to_block",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_2b5485809f7439c44769748bbc713872"
],
0,
"02c9337093a6a7580ea9f83c2ba1b24b"
],
[
"Vale.SHA.SHA_helpers.lemma_quads_to_block",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_1606e1a7da0583d7bad9677dcf38161d",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_c25dec9c72aa6b7bf5bd6f72fdcce3c3",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.UInt.max_int", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"equation_Spec.Hash.Definitions.sha2_alg",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_t",
"equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
"equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_select",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.counter",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.quads_to_block",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"equation_Vale.SHA.SHA_helpers.ws_opaque",
"equation_Vale.SHA.SHA_helpers.ws_quad32",
"equation_with_fuel_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Spec.SHA2.Lemmas.ws",
"function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing",
"interpretation_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
"interpretation_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"interpretation_Tm_abs_d324b025050975942eed8e4180033924",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2b5485809f7439c44769748bbc713872",
"refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
"refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_963efb8f77bcba49b31d59ffbced85c9",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
"refinement_interpretation_Tm_refine_f403a81b4216eb73ad8a1c1c2f0a1d83",
"token_correspondence_Spec.SHA2.Lemmas.ws_aux",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2.Lemmas.ws",
"typing_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
"typing_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"typing_Tm_abs_d324b025050975942eed8e4180033924",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.SHA.SHA_helpers.quads_to_block",
"typing_Vale.SHA.SHA_helpers.ws_opaque",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"a7e83d71834f4fd22ae6da85d2630aff"
],
[
"Vale.SHA.SHA_helpers.translate_hash_update",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.add_mod",
"equation_Lib.IntTypes.add_mod", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.Types.add_wrap_quad32",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.vv",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.v_injective",
"lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_229a5e8eb8bb5562044d0cd62fb30564",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d60a0e9fdf52cedb444de54cc40036f8",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
"typing_Lib.IntTypes.mk_int",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.nat32_to_word",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"90ae6d2b4886175a627670494e97893a"
],
[
"Vale.SHA.SHA_helpers.update_block",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"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_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"e8804529c8e92bd91ec001e78581a401"
],
[
"Vale.SHA.SHA_helpers.lemma_update_block_equiv",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.Agile.Hash.update",
"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.SHA2.op_Plus_Dot", "equation_Spec.SHA2.update_pre",
"equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.update_block",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Spec.SHA2.update", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_ad8571230fdeaf581ec3410ca58dbe3e",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"token_correspondence_Spec.Agile.Hash.update",
"token_correspondence_Spec.SHA2.update_pre",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"cbd97b6f67414093cc3132589119ae80"
],
[
"Vale.SHA.SHA_helpers.update_lemma",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.UInt.add_mod", "equation_Lib.IntTypes.add_mod",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.is_sha2",
"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.SHA2.Lemmas.shuffle_aux",
"equation_Spec.SHA2.size_k_w",
"equation_Vale.Arch.Types.add_wrap_quad32",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.shuffle_core_opaque",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.update_block",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0d26a30f050a4b0c55b0762dfcb7cab2",
"refinement_interpretation_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4303d0c89988fe82aadcf16754a5b20f",
"refinement_interpretation_Tm_refine_516841552c075993547f605f17f21002",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"token_correspondence_Lib.IntTypes.add_mod",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
"typing_Spec.Hash.Definitions.word_t", "typing_Spec.Loops.seq_map2",
"typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.SHA.SHA_helpers.make_hash",
"typing_Vale.SHA.SHA_helpers.update_block",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok",
"well-founded-ordering-on-nat"
],
0,
"63679978fdf0d94c8d39ec9d4052a7f7"
],
[
"Vale.SHA.SHA_helpers.update_multi_quads",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_0",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.split", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_e7547d4e3bc4c2d7d07f503e85b9b717",
"typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
],
0,
"9eed5ddf752209854ebf211a4ced946f"
],
[
"Vale.SHA.SHA_helpers.lemma_le_bytes_to_seq_quad32_empty",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"91eeed1e143dd1b7520d1ed00b9ae0c2"
],
[
"Vale.SHA.SHA_helpers.lemma_le_bytes_to_seq_quad32_length",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.squash",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"5255c7491f1833a54ad21576d65c6fad"
],
[
"Vale.SHA.SHA_helpers.lemma_slice_commutes_reverse_bytes_nat32_quad32_seq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq"
],
0,
"1b8eb79aba6cb270f14e20f5e4b02ecd"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_quads_unfold",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"@fuel_irrelevance_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"@query", "b2t_def", "equation_Prims.squash",
"equation_with_fuel_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"9b821f9f56f4ca6caa11d4f99a16af99"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_quads_short",
1,
1,
0,
[
"@MaxFuel_assumption",
"@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"@query",
"equation_with_fuel_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"primitive_Prims.op_LessThan", "projection_inverse_BoxInt_proj_0"
],
0,
"f98e4882674c767f0e3fa9456e1b7219"
],
[
"Vale.SHA.SHA_helpers.update_multi_one",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.Seq.Properties.split",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.size_t", "equation_Lib.Sequence.seq",
"equation_Prims.eqtype",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.bytes_block",
"equation_Spec.Hash.Definitions.bytes_blocks",
"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_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.bytes",
"equation_Vale.SHA.SHA_helpers.bytes_blocks",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_Spec.Hash.Lemmas.update_multi_update",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7540e34d933027d9a3465a151eb57527",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_b08c21a5805b9ea145285da72ddb1ea9",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt8.t", "typing_Spec.Agile.Hash.update_multi",
"typing_Spec.Hash.Definitions.block_length",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"4e65f1f2ee82d867bfa9b18f823d1e88"
],
[
"Vale.SHA.SHA_helpers.lemma_be_to_n_4",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Seq.Properties.last", "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.ByteSequence.nat_from_bytes_be",
"equation_Lib.ByteSequence.nat_from_intseq_be",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
"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.range",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Types_s.be_bytes_to_nat32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_with_fuel_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Vale.Def.Words.Four_s.four_to_nat",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_2bb29967df4c7f51a83f5fb98944d5d2",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv",
"lemma_Lib.IntTypes.pow2_3", "lemma_Lib.IntTypes.pow2_4",
"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",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_40635fb096fd2f76bb3d32d45a9d3d4a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d3f3b0326a40b22c084e873c3571a01",
"refinement_interpretation_Tm_refine_6017c6d7f5d6f16aa02c5de0bae953ad",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83452a5d8515fc994ff43c85b1b18e18",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt8.uint_to_t",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt.fits", "typing_FStar.UInt8.v",
"typing_Lib.ByteSequence.nat_from_intseq_be_",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words_s.int_to_natN",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"5ad7a6c45a60201fc5975da5f8d86656"
],
[
"Vale.SHA.SHA_helpers.lemma_endian_relation",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_4217d864395e427d3d50043a7013186f",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_c25dec9c72aa6b7bf5bd6f72fdcce3c3",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Tm_unit", "disc_equation_Lib.IntTypes.U1",
"eq2-interp", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.ByteSequence.nat_from_bytes_be",
"equation_Lib.ByteSequence.uint_from_bytes_be",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mk_int",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos",
"equation_Prims.squash",
"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_of_bytes",
"equation_Vale.Arch.Types.reverse_bytes_nat32_quad32",
"equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
"equation_Vale.Def.Types_s.be_bytes_to_nat32",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.Def.Types_s.nat32_to_be_bytes",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Types_s.reverse_bytes_nat32_def",
"equation_Vale.Def.Words.Four_s.four_select",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.reverse_seq",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.SHA.SHA_helpers.block_w",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.quads_to_block",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.to_uint32",
"equation_Vale.SHA.SHA_helpers.word",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32",
"function_token_typing_Vale.Def.Words.Four_s.nat_to_four",
"function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_4f03474956a6a2311e7d7bb19e902da5",
"interpretation_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
"interpretation_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"interpretation_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
"interpretation_Tm_abs_d324b025050975942eed8e4180033924",
"interpretation_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
"kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_a",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_164c3a661e54954c7dffc0eba5297a30",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_342c9cca61362b433980438d26ded5b2",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_36761decbc261e6443324da875d9d5c2",
"refinement_interpretation_Tm_refine_386cc03d241e5f4a0a84f0ca50489700",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_79d1f88e3feaf4f011c530ae4970c006",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_830fcadbd451dad13f5a1d292e9e4412",
"refinement_interpretation_Tm_refine_963efb8f77bcba49b31d59ffbced85c9",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
"refinement_interpretation_Tm_refine_be21a78039e791db0e843dbd3b1f77f6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f21dd5802eb4c999bcae09802023d5fd",
"refinement_interpretation_Tm_refine_fae547c0c57b476075b6de4468df2cfa",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Lib.ByteSequence.uints_from_bytes_be",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Spec.Hash.Definitions.words_of_bytes",
"token_correspondence_Vale.Arch.Types.reverse_bytes_nat32_quad32",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def",
"typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
"typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index",
"typing_Spec.Hash.Definitions.word_length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
"typing_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"typing_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
"typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Types_s.nat32_to_be_bytes",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words.Seq_s.seq_to_four_BE",
"typing_Vale.SHA.SHA_helpers.quads_to_block",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"ca0eb7ccb0ac0b013e07454ae78bb8c9"
],
[
"Vale.SHA.SHA_helpers.lemma_mod_transform",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Prims.eqtype",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_Vale.Def.Words_s.nat8",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
],
0,
"b8ab4e202220dc174ef9d00160af7ab0"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_equiv_vale",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_2",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_3",
"binder_x_6efd6f1848d6dc888dd6a85a4fabc17f_4",
"binder_x_b5ecdf6b68431b1ae5a51ce9723a824d_5",
"binder_x_e5783cd4c27820e67b27bc7b42ce4f40_0",
"binder_x_e5783cd4c27820e67b27bc7b42ce4f40_1",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_FStar.Seq.Properties.split",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.size_t", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.bytes_blocks",
"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_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.byte",
"equation_Vale.SHA.SHA_helpers.bytes",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.update_multi_opaque",
"equation_Vale.SHA.SHA_helpers.update_multi_opaque_vale",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Spec.Agile.Hash.update_multi",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32_seq",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_43b3b4e76ec6fcef7f5ade88a814aaa5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_7ccde69e15dd30180324c8ef1fa8b87b",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a9e181f2b4db9770dc5da297b02d21b8",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c70800497694fd7a03bdc0b39878a9c4",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.SHA.SHA_helpers.update_multi_opaque_aux",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_Spec.Agile.Hash.update_multi",
"typing_Spec.Hash.Definitions.block_length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.SHA.SHA_helpers.update_multi_opaque_vale",
"typing_Vale.SHA.SHA_helpers.update_multi_quads",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok",
"well-founded-ordering-on-nat"
],
0,
"2204868db279d1cbc885add21b0441c9"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_quads",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8117376fa751a9089be3b927d5831062",
"typing_FStar.Seq.Base.length"
],
0,
"74e0280c2004e4cc31e3cc04dc4966ed"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_quads",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8117376fa751a9089be3b927d5831062",
"refinement_interpretation_Tm_refine_ec52b9f9f8eb4bdfce9c337da9c88747",
"typing_FStar.Seq.Base.length"
],
0,
"2df869a7f08d5758e469c68b7e59d4d1"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_quads",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"@fuel_irrelevance_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_e5783cd4c27820e67b27bc7b42ce4f40_1",
"equation_FStar.Seq.Properties.split", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_with_fuel_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"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_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_46ff6445a55ccc12cce752faeb810bb5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8528cd6408f39eb28756c48c55356a8",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq"
],
0,
"d56e52818d2949a2a7180f1578a1064f"
],
[
"Vale.SHA.SHA_helpers.le_bytes_to_hash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_1ce1f604e3636d4aefb8e634e669999e",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
"equation_Prims.nat",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"primitive_Prims.op_disEquality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_25aa5013196fbd0a35c92458222d0340",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"07ab5c29563bb5d7b538c0a1d285c30b"
],
[
"Vale.SHA.SHA_helpers.lemma_le_bytes_to_hash_quads_part1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.SHA.SHA_helpers.le_bytes_to_hash",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def"
],
0,
"549bd9793a84bec3863287e457c084bf"
],
[
"Vale.SHA.SHA_helpers.lemma_le_bytes_to_hash_quads",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_1606e1a7da0583d7bad9677dcf38161d",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_c25dec9c72aa6b7bf5bd6f72fdcce3c3",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U32", "eq2-interp",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_select",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.le_bytes_to_hash",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"interpretation_Tm_abs_d324b025050975942eed8e4180033924",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_963efb8f77bcba49b31d59ffbced85c9",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f403a81b4216eb73ad8a1c1c2f0a1d83",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.SHA.SHA_helpers.nat32_to_word",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"typing_Tm_abs_d324b025050975942eed8e4180033924",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.SHA.SHA_helpers.le_bytes_to_hash"
],
0,
"921900daa3d5103ccd7c8a3bd943815e"
],
[
"Vale.SHA.SHA_helpers.lemma_hash_to_bytes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"f4fef3b2fd03ee3edc57721390b105b4"
],
[
"Vale.SHA.SHA_helpers.lemma_hash_to_bytes",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC", "eq2-interp",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint32",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.SHA.SHA_helpers.hash256",
"equation_Vale.SHA.SHA_helpers.le_bytes_to_hash",
"equation_Vale.SHA.SHA_helpers.nat32_to_word",
"equation_Vale.SHA.SHA_helpers.word",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.SHA.SHA_helpers.le_bytes_to_hash"
],
0,
"02cf9a6bad36fc6685d1ae0b49e1969d"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_opaque_vale_is_update_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"7945ffb86e006528c67cf3686d69139c"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_opaque_vale_is_update_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Prims.squash",
"equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.update_multi_opaque",
"equation_Vale.SHA.SHA_helpers.update_multi_opaque_vale",
"equation_Vale.SHA.SHA_helpers.update_multi_transparent",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.Agile.Hash.update_multi",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"token_correspondence_Vale.SHA.SHA_helpers.update_multi_opaque_aux"
],
0,
"25528dc6c64aee74952eb7bc54cde894"
]
]
]
Computing file changes ...
