[
"p\fÜ\u0012rSÑñŸ¿½ \u0017iÑ",
[
[
"Vale.Interop.Views.get8_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"521cd0ace1878616aed2fe3ce00e2c26"
],
[
"Vale.Interop.Views.get8_reveal",
1,
1,
0,
[ "@query" ],
0,
"da91c1192486f575c031438d7d5c1021"
],
[
"Vale.Interop.Views.put8_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
"Vale.Interop.Views_interpretation_Tm_arrow_2dd0c4bcae97dc98989285f8c291dc4b",
"equation_Prims.eqtype", "equation_Prims.nat", "int_typing",
"interpretation_Tm_abs_90d717ff23a3b502df97d7dd6779d73a",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.UInt8.t",
"typing_Tm_abs_90d717ff23a3b502df97d7dd6779d73a"
],
0,
"3241d28aa5ae337376d45e0807a71fcb"
],
[
"Vale.Interop.Views.put8_reveal",
1,
1,
0,
[ "@query" ],
0,
"2d4b6670e153ee596f0f7f137773546d"
],
[
"Vale.Interop.Views.inverses8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
"Prims_interpretation_Tm_ghost_arrow_0283b8a2a36bbec52abac4e3d837674a",
"Vale.Interop.Views_interpretation_Tm_arrow_2dd0c4bcae97dc98989285f8c291dc4b",
"Vale.Interop.Views_interpretation_Tm_ghost_arrow_423a1f6a8e54ac93da454104ac96decb",
"equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Down.inverses", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Interop.Views.get8_def",
"equation_Vale.Interop.Views.put8_def",
"function_token_typing_Vale.Interop.Views.get8",
"function_token_typing_Vale.Interop.Views.put8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_90d717ff23a3b502df97d7dd6779d73a",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.Interop.Views.get8",
"token_correspondence_Vale.Interop.Views.get8_def",
"token_correspondence_Vale.Interop.Views.put8",
"token_correspondence_Vale.Interop.Views.put8_def",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_Tm_abs_90d717ff23a3b502df97d7dd6779d73a",
"typing_Vale.Interop.Views.get8", "typing_Vale.Interop.Views.put8"
],
0,
"7985cc35f8df2dabf66ab64bb69342aa"
],
[
"Vale.Interop.Views.up_view8",
1,
1,
0,
[
"@query", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Up.inverses",
"function_token_typing_LowStar.BufferView.Down.inverses",
"token_correspondence_LowStar.BufferView.Up.inverses"
],
0,
"bd3ef7db5f6538cbf503e7ba142ee257"
],
[
"Vale.Interop.Views.down_view8",
1,
1,
0,
[ "@query", "equation_LowStar.BufferView.Down.inverses" ],
0,
"ce269ff9636cb9968d2f54165da5bfee"
],
[
"Vale.Interop.Views.get16_def",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.Seq.Properties.lseq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat", "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",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"587e11c051fde9c56eb2bf38e5683c5f"
],
[
"Vale.Interop.Views.get16_reveal",
1,
1,
0,
[ "@query" ],
0,
"5e4132c0e3cacf9023408e111183c02e"
],
[
"Vale.Interop.Views.put16_def",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_upd", "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_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_FStar.UInt8.t", "typing_Prims.pow2"
],
0,
"11ceafa2d35bd921fee8bf8c3dbccb09"
],
[
"Vale.Interop.Views.put16_reveal",
1,
1,
0,
[ "@query" ],
0,
"a7dcb816cd360016915bf2927f694143"
],
[
"Vale.Interop.Views.inverses16",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
"Prims_interpretation_Tm_ghost_arrow_0283b8a2a36bbec52abac4e3d837674a",
"Vale.Interop.Views_interpretation_Tm_arrow_e9743f4ae755ac8030f1e9865c22cb65",
"Vale.Interop.Views_interpretation_Tm_ghost_arrow_98161352d059303bdff8d2a259ea66a8",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_LowStar.BufferView.Down.inverses", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Interop.Views.get16_def",
"equation_Vale.Interop.Views.put16_def",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Vale.Interop.Views.get16",
"function_token_typing_Vale.Interop.Views.put16", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt16.uv_inv", "lemma_FStar.UInt16.vu_inv",
"lemma_FStar.UInt8.uv_inv", "lemma_FStar.UInt8.vu_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_25c72d704900d626b30894312c325451",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Interop.Views.get16",
"token_correspondence_Vale.Interop.Views.get16_def",
"token_correspondence_Vale.Interop.Views.put16",
"token_correspondence_Vale.Interop.Views.put16_def",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.upd",
"typing_FStar.UInt16.v", "typing_FStar.UInt8.t",
"typing_FStar.UInt8.uint_to_t", "typing_FStar.UInt8.v",
"typing_Vale.Interop.Views.get16", "typing_Vale.Interop.Views.put16"
],
0,
"f5f5abe6d370e8f90da6c71d262910e5"
],
[
"Vale.Interop.Views.up_view16",
1,
1,
0,
[
"@query", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Up.inverses",
"function_token_typing_LowStar.BufferView.Down.inverses",
"token_correspondence_LowStar.BufferView.Up.inverses"
],
0,
"26bcca0e786a7e3182f402af836d5644"
],
[
"Vale.Interop.Views.down_view16",
1,
1,
0,
[ "@query", "equation_LowStar.BufferView.Down.inverses" ],
0,
"ad62f888564bd609c5ad3ea7750fda94"
],
[
"Vale.Interop.Views.get32_def",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "equation_FStar.Seq.Properties.lseq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.eqtype",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"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",
"function_token_typing_Vale.Def.Words_s.nat8",
"lemma_FStar.Seq.Base.lemma_init_len", "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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"b61e82a1d49db82a4c378c7c8a5f011b"
],
[
"Vale.Interop.Views.get32_reveal",
1,
1,
0,
[ "@query" ],
0,
"2e4236140d7f39f9df12e798e592723d"
],
[
"Vale.Interop.Views.put32_def",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seqn",
"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", "int_typing",
"lemma_FStar.Seq.Base.lemma_init_len",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"b41bf40bd028b8a01a88da546a417510"
],
[
"Vale.Interop.Views.put32_reveal",
1,
1,
0,
[ "@query" ],
0,
"f445ceb7e1a65891204769750ae42931"
],
[
"Vale.Interop.Views.inverses32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"Vale.Interop.Views_interpretation_Tm_arrow_cffd032005b463ca536a992a3d0af441",
"b2t_def", "equation_FStar.Seq.Properties.lseq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t",
"equation_LowStar.BufferView.Down.inverses", "equation_Prims.nat",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Views.get32",
"equation_Vale.Interop.Views.get32_def",
"equation_Vale.Interop.Views.put32",
"equation_Vale.Interop.Views.put32_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Interop.Views.get32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
"lemma_Vale.Def.Words.Seq.seq_uint8_to_seq_nat8_to_seq_uint8",
"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_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Interop.Views.get32",
"token_correspondence_Vale.Interop.Views.get32_def",
"token_correspondence_Vale.Interop.Views.put32",
"token_correspondence_Vale.Interop.Views.put32_def",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt32.v",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Four_s.four_to_nat",
"typing_Vale.Def.Words.Four_s.nat_to_four",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.Def.Words.Seq_s.seq_to_four_LE",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
],
0,
"89566d9574835994cd928dd41323d561"
],
[
"Vale.Interop.Views.up_view32",
1,
1,
0,
[
"@query", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Up.inverses",
"function_token_typing_LowStar.BufferView.Down.inverses",
"token_correspondence_LowStar.BufferView.Up.inverses"
],
0,
"ea20bfc92fe891815f65e1fa6099d76b"
],
[
"Vale.Interop.Views.down_view32",
1,
1,
0,
[ "@query", "equation_LowStar.BufferView.Down.inverses" ],
0,
"72f36607eefd7ab96158085ab50ff668"
],
[
"Vale.Interop.Views.get64_def",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "equation_FStar.Seq.Properties.lseq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"lemma_FStar.Seq.Base.lemma_init_len",
"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",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"8ec9d3ba286f36011afa560bee588ca3"
],
[
"Vale.Interop.Views.get64_reveal",
1,
1,
0,
[ "@query" ],
0,
"8a080de1a016ed312f96814c65662a10"
],
[
"Vale.Interop.Views.put64_def",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"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",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"8da7239b07952106360c3d531ed24ace"
],
[
"Vale.Interop.Views.put64_reveal",
1,
1,
0,
[ "@query" ],
0,
"da8ce59d9e32a7efcd16eb4f6b466597"
],
[
"Vale.Interop.Views.inverses64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"Vale.Interop.Views_interpretation_Tm_arrow_44253793d4f3c6b5988256e0c330391f",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_LowStar.BufferView.Down.inverses", "equation_Prims.nat",
"equation_Vale.Def.Types_s.le_bytes_to_nat64",
"equation_Vale.Def.Types_s.le_nat64_to_bytes",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Views.get64",
"equation_Vale.Interop.Views.get64_def",
"equation_Vale.Interop.Views.put64",
"equation_Vale.Interop.Views.put64_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Interop.Views.get64", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt64.uv_inv",
"lemma_FStar.UInt64.vu_inv",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
"lemma_Vale.Def.Words.Seq.seq_uint8_to_seq_nat8_to_seq_uint8",
"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",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a97bb01c04ffe0871485a0f7264ef673",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Vale.Interop.Views.get64",
"token_correspondence_Vale.Interop.Views.get64_def",
"token_correspondence_Vale.Interop.Views.put64",
"token_correspondence_Vale.Interop.Views.put64_def",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt64.v",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Types_s.le_bytes_to_nat64",
"typing_Vale.Def.Types_s.le_nat64_to_bytes",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
],
0,
"c5539306ebe77460e17f7184d484cabd"
],
[
"Vale.Interop.Views.up_view64",
1,
1,
0,
[
"@query", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Up.inverses",
"function_token_typing_LowStar.BufferView.Down.inverses",
"token_correspondence_LowStar.BufferView.Up.inverses"
],
0,
"bbb501533119bfa2c0148da664c4768b"
],
[
"Vale.Interop.Views.down_view64",
1,
1,
0,
[ "@query", "equation_LowStar.BufferView.Down.inverses" ],
0,
"b28b38df22a5cc4e9fbd78b4e0b1d41d"
],
[
"Vale.Interop.Views.get128_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"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",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"6bdf704cf6d673ef168b6259357c2387"
],
[
"Vale.Interop.Views.get128_reveal",
1,
1,
0,
[ "@query" ],
0,
"d6ad1b4ce8a1ca2c76c9b7c5eb3c8e27"
],
[
"Vale.Interop.Views.put128_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"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",
"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"
],
0,
"688569f0eda1aa5826779b268a929e38"
],
[
"Vale.Interop.Views.put128_reveal",
1,
1,
0,
[ "@query" ],
0,
"1e1f30fbc17920954c25c5d63fbcafdf"
],
[
"Vale.Interop.Views.inverses128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Down.inverses", "equation_Prims.eqtype",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Views.get128_def",
"equation_Vale.Interop.Views.put128_def",
"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.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
"lemma_Vale.Def.Words.Seq.seq_uint8_to_seq_nat8_to_seq_uint8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.Interop.Views.get128_def",
"token_correspondence_Vale.Interop.Views.put128_def",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Types_s.le_quad32_to_bytes",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
],
0,
"e035c334de42680de3bb79a7556b4978"
],
[
"Vale.Interop.Views.up_view128",
1,
1,
0,
[
"@query", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Up.inverses",
"equation_Vale.Def.Types_s.quad32",
"function_token_typing_LowStar.BufferView.Down.inverses",
"token_correspondence_LowStar.BufferView.Up.inverses"
],
0,
"570eb10653f4388511e3a715115bb0e5"
],
[
"Vale.Interop.Views.down_view128",
1,
1,
0,
[ "@query", "equation_LowStar.BufferView.Down.inverses" ],
0,
"fe3f5daf0f7249002e0df9da837ff1da"
],
[
"Vale.Interop.Views.nat32s_to_nat128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"f96af0882a5a6078186e695d34023314"
],
[
"Vale.Interop.Views.get32_128_def",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "equation_FStar.Seq.Properties.lseq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"ba5dd8325e8cc72def15a7e1160dbdd5"
],
[
"Vale.Interop.Views.get32_128_reveal",
1,
1,
0,
[ "@query" ],
0,
"eb8543534a4c5c4b051a7b11c3b6afb5"
],
[
"Vale.Interop.Views.put32_128_def",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt32.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE"
],
0,
"e99cefd2736333ac3b1e5a2dc1788cd8"
],
[
"Vale.Interop.Views.put32_128_reveal",
1,
1,
0,
[ "@query" ],
0,
"d68f63ab33f8fc1f608df97ccc406c56"
],
[
"Vale.Interop.Views.get32_128_aux1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Interop.Views.get32_128_def",
"equation_Vale.Interop.Views.put32_128_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt32.uint_to_t",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Interop.Views.get32_128",
"function_token_typing_Vale.Interop.Views.put32_128",
"int_inversion", "int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.UInt32.uv_inv",
"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",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_FStar.UInt32.v",
"token_correspondence_Vale.Interop.Views.get32_128_def",
"token_correspondence_Vale.Interop.Views.put32_128_def",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt32.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.Interop.Views.get32_128"
],
0,
"e2946cafa870206da027f13a9b964b90"
],
[
"Vale.Interop.Views.put32_128_aux1",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt32_interpretation_Tm_arrow_33a06d9a3ec1c77524ab958d37ae1453",
"FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Views.get32_128_def",
"equation_Vale.Interop.Views.put32_128_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt32.v",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Interop.Views.get32_128",
"function_token_typing_Vale.Interop.Views.put32_128", "int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"lemma_FStar.Seq.Base.init_index_", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
"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",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_FStar.UInt32.uint_to_t",
"token_correspondence_FStar.UInt32.v",
"token_correspondence_Vale.Interop.Views.get32_128_def",
"token_correspondence_Vale.Interop.Views.put32_128_def",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt32.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"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.Interop.Views.put32_128"
],
0,
"62b3924b3691916ba88a5b64b848f34e"
],
[
"Vale.Interop.Views.inverses32_128",
1,
1,
0,
[
"@query", "equation_LowStar.BufferView.Down.inverses",
"equation_Vale.Def.Types_s.quad32",
"token_correspondence_Vale.Interop.Views.get32_128",
"token_correspondence_Vale.Interop.Views.put32_128"
],
0,
"9147e5b8e3d3f959c4da749e470c88db"
],
[
"Vale.Interop.Views.view32_128",
1,
1,
0,
[
"@query", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Up.inverses",
"equation_Vale.Def.Types_s.quad32",
"function_token_typing_LowStar.BufferView.Down.inverses",
"token_correspondence_LowStar.BufferView.Up.inverses"
],
0,
"8b1bf64f10329c695e1d5c0ee5241d5e"
]
]
]