Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
EverCrypt.CTR.fst.hints
[
"��za��5օ̳�d�}`",
[
[
"EverCrypt.CTR.nonce_upper_bound",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Spec.Agile.Cipher.AES128",
"disc_equation_Spec.Agile.Cipher.AES256",
"disc_equation_Spec.Agile.Cipher.CHACHA20", "equation_Prims.squash",
"equation_Spec.Cipher.Expansion.uu___29",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"inversion-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"eada2cdd7b68f3c26a534448fdc5f824"
],
[
"EverCrypt.CTR.state_s",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"d3c64c25926143313bb862317330f4ad"
],
[
"EverCrypt.CTR.__proj__State__item__iv_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"8d310f2977a7fe2960938a723bbf3dc8"
],
[
"EverCrypt.CTR.__proj__State__item__iv_len",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_EverCrypt.CTR.state_s",
"proj_equation_EverCrypt.CTR.State_g_iv",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_EverCrypt.CTR.State_g_iv",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"0dc835cf786e0458553ad4995bb759b6"
],
[
"EverCrypt.CTR.__proj__State__item__xkey",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"9404997d562210dcfc9974d4a9f0f8e0"
],
[
"EverCrypt.CTR.__proj__State__item__xkey",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "fuel_guarded_inversion_EverCrypt.CTR.state_s",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"proj_equation_EverCrypt.CTR.State_i",
"projection_inverse_EverCrypt.CTR.State_i",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"0e90a22ba2cc25f1f84f695594d341a7"
],
[
"EverCrypt.CTR.cpu_features_invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20",
"disc_equation_Spec.Cipher.Expansion.Vale_AES128",
"disc_equation_Spec.Cipher.Expansion.Vale_AES256",
"equation_Prims.squash", "equation_Spec.Cipher.Expansion.uu___30",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Spec.Cipher.Expansion.uu___30",
"inversion-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"e87bb1ba36f202a555b28cd7c9b348c9"
],
[
"EverCrypt.CTR.invariant_s",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Spec.Agile.Cipher.cipher_alg__uu___haseq", "b2t_def",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U8", "eq2-interp",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.nonce_upper_bound",
"equation_FStar.UInt.min_int", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"equation_Prims.squash", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.Cipher.key", "equation_Spec.Agile.Cipher.nonce",
"equation_Spec.Agile.Cipher.nonce_bound",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.Cipher.Expansion.uu___29", "int_typing",
"inversion-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0a75f0cf88da5cc16f0b88ac8596762e",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_849d11bd4488c6a32fa952ced0f4d828",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length",
"typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"bbe01a77f23bad80cd724c444769723b"
],
[
"EverCrypt.CTR.invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_EverCrypt.CTR.state",
"equation_LowStar.Buffer.pointer",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e"
],
0,
"0a50c8b3a2823a035479927ee3512e20"
],
[
"EverCrypt.CTR.uu___85",
1,
0,
0,
[ "@query" ],
0,
"440842e613313ffc44b322eb7dee72ed"
],
[
"EverCrypt.CTR.uu___86",
1,
0,
0,
[ "@query" ],
0,
"24ecb71e5368b6a7559a91cc375b1aa0"
],
[
"EverCrypt.CTR.invariant_loc_in_footprint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_typing",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U8",
"data_elim_EverCrypt.CTR.State", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "equation_EverCrypt.CTR.state",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_t",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_EverCrypt.CTR.state_s",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"l_and-interp", "lemma_EverCrypt.CTR.invert_state_s",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"primitive_Prims.op_Equality", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0a75f0cf88da5cc16f0b88ac8596762e",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
"refinement_interpretation_Tm_refine_94e9a7f41130db86d255f278b02a4022",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_EverCrypt.CTR.footprint_s", "typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"4d64539c5acf6d403f53eb87dd14b64e"
],
[
"EverCrypt.CTR.frame_invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_typing",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U8",
"data_elim_EverCrypt.CTR.State", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.cpu_features_invariant",
"equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "equation_EverCrypt.CTR.state",
"equation_FStar.UInt.fits", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_EverCrypt.CTR.state_s",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"function_token_typing_Spec.AES.elem",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"l_and-interp", "lemma_EverCrypt.CTR.invert_state_s",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0a75f0cf88da5cc16f0b88ac8596762e",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
"refinement_interpretation_Tm_refine_94e9a7f41130db86d255f278b02a4022",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_EverCrypt.CTR.footprint_s", "typing_FStar.Set.singleton",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6612d2e2c14a2366bb93cd5ef7d83fae"
],
[
"EverCrypt.CTR.ctr",
1,
0,
0,
[
"@query", "b2t_def", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"199836aa4ab50b4ed06ba7b1bebbbb22"
],
[
"EverCrypt.CTR.alg_of_state",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "l_and-interp",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1a224e9182f63c8804d89d54542df7b3"
],
0,
"394ae7afcbe9ca4a1c1c0ce9db314c12"
],
[
"EverCrypt.CTR.create_in_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AES.AES128",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s",
"equation_EverCrypt.CTR.nonce_upper_bound",
"equation_EverCrypt.CTR.uint8",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.aes_key", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.AES.key_size",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.block_length",
"equation_Spec.Agile.Cipher.key",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Chacha20.key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"l_and-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_764dc2b54fa2320bf14bc0cb4a02d37d",
"refinement_interpretation_Tm_refine_7679fccd9d7a57bc9b6a8a96f0dcfb4b",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"767b83d1f7810ff44f404a4a2ce839f2"
],
[
"EverCrypt.CTR.vale_impl_of_alg",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"disc_equation_Spec.Agile.Cipher.AES128",
"disc_equation_Spec.Agile.Cipher.AES256",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equation_FStar.Pervasives.inversion",
"equation_Spec.Cipher.Expansion.vale_cipher_alg",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"inversion-interp",
"refinement_interpretation_Tm_refine_177c69f55dbc44094b230a6a570a50b1"
],
0,
"38669adb705e9c84d3c202d265910789"
],
[
"EverCrypt.CTR.create_in_vale",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing",
"constructor_distinct_EverCrypt.Error.InvalidIVLength",
"constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES128",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES256",
"data_elim_EverCrypt.CTR.State",
"equality_tok_EverCrypt.Error.InvalidIVLength@tok",
"equality_tok_EverCrypt.Error.Success@tok",
"equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.AES.AES256@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equation_EverCrypt.CTR.Keys.concrete_xkey_len",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.Keys.vale_impl",
"equation_EverCrypt.CTR.cpu_features_invariant",
"equation_EverCrypt.CTR.ctr", "equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.freeable",
"equation_EverCrypt.CTR.freeable_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "equation_EverCrypt.CTR.iv",
"equation_EverCrypt.CTR.kv",
"equation_EverCrypt.CTR.nonce_upper_bound",
"equation_EverCrypt.CTR.uint8",
"equation_EverCrypt.CTR.vale_impl_of_alg",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.lt", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.fresh_loc",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.aes_key", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.block_length",
"equation_Spec.Agile.Cipher.key",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Agile.Cipher.nonce_bound",
"equation_Spec.Chacha20.size_nonce",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.concrete_expand",
"equation_Spec.Cipher.Expansion.concrete_xkey",
"equation_Spec.Cipher.Expansion.concrete_xkey_length",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.Cipher.Expansion.vale_xkey_length",
"equation_Spec.GaloisField.gf",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"fuel_guarded_inversion_EverCrypt.CTR.state_s",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"l_and-interp", "lemma_EverCrypt.CTR.invert_state_s",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"proj_equation_EverCrypt.CTR.State_ctr",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.CTR.State_ctr",
"projection_inverse_EverCrypt.CTR.State_g_iv",
"projection_inverse_EverCrypt.CTR.State_g_key",
"projection_inverse_EverCrypt.CTR.State_i",
"projection_inverse_EverCrypt.CTR.State_iv",
"projection_inverse_EverCrypt.CTR.State_iv_len",
"projection_inverse_EverCrypt.CTR.State_xkey",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_08d038643b0553a506b9818e13398796",
"refinement_interpretation_Tm_refine_0a75f0cf88da5cc16f0b88ac8596762e",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95",
"refinement_interpretation_Tm_refine_1d6fbedf51ea327a7f584c6571771aee",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_3f1111aab9561e3f8eef978998729db0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_6becdf7fe181eded3d23a517bb814815",
"refinement_interpretation_Tm_refine_9100ab96093283c751c14419f2de4403",
"refinement_interpretation_Tm_refine_93ee49c914cab99d9057a4c4b81ac192",
"refinement_interpretation_Tm_refine_94e9a7f41130db86d255f278b02a4022",
"refinement_interpretation_Tm_refine_ac4623811749d1b02f6cf29babc48f6d",
"refinement_interpretation_Tm_refine_baddf01de5a99cc9ebb782610da52e20",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c3a3c22be65591eff091e47a99687f51",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_EverCrypt.CTR.Keys.concrete_xkey_len",
"typing_EverCrypt.CTR.footprint_s",
"typing_EverCrypt.TargetConfig.x64", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Set.singleton", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.pointer_or_null",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.loc_unused_in",
"typing_Spec.AES.gf8", "typing_Spec.Agile.Cipher.key",
"typing_Spec.Agile.Cipher.key_length",
"typing_Spec.Agile.Cipher.nonce", "typing_Spec.Chacha20.size_nonce",
"typing_Spec.Cipher.Expansion.cipher_alg_of_impl",
"typing_Spec.Cipher.Expansion.concrete_expand",
"typing_Spec.Cipher.Expansion.concrete_xkey_length",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_tok_EverCrypt.Error.InvalidIVLength@tok",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"8d74692d70254cc7c8699045aa84f2e4"
],
[
"EverCrypt.CTR.create_in",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"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.AES.AES128",
"disc_equation_EverCrypt.Error.InvalidIVLength",
"disc_equation_EverCrypt.Error.Success",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "equation_EverCrypt.CTR.uint8",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.aes_key",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.key",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Chacha20.key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"l_and-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
"refinement_interpretation_Tm_refine_764dc2b54fa2320bf14bc0cb4a02d37d",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"d12fac6b585bf243f324ec3d06c0ee38"
],
[
"EverCrypt.CTR.create_in",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES128",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES256",
"disc_equation_Spec.Agile.Cipher.AES128",
"disc_equation_Spec.Agile.Cipher.AES256",
"disc_equation_Spec.Agile.Cipher.CHACHA20", "eq2-interp",
"equality_tok_EverCrypt.Error.Success@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equality_tok_Spec.Cipher.Expansion.Hacl_CHACHA20@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equation_EverCrypt.CTR.Keys.concrete_xkey_len",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.cpu_features_invariant",
"equation_EverCrypt.CTR.ctr", "equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.freeable",
"equation_EverCrypt.CTR.freeable_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "equation_EverCrypt.CTR.iv",
"equation_EverCrypt.CTR.kv",
"equation_EverCrypt.CTR.nonce_upper_bound",
"equation_EverCrypt.CTR.state", "equation_EverCrypt.CTR.uint8",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"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.uint8", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.fresh_loc",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length",
"equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.Cipher.key",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Agile.Cipher.nonce_bound",
"equation_Spec.Chacha20.key", "equation_Spec.Chacha20.size_key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.concrete_expand",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Chacha20.key",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"l_and-interp", "lemma_EverCrypt.CTR.invariant_loc_in_footprint",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"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_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Negation",
"proj_equation_EverCrypt.CTR.State_ctr",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.CTR.State_ctr",
"projection_inverse_EverCrypt.CTR.State_g_iv",
"projection_inverse_EverCrypt.CTR.State_g_key",
"projection_inverse_EverCrypt.CTR.State_i",
"projection_inverse_EverCrypt.CTR.State_iv",
"projection_inverse_EverCrypt.CTR.State_xkey",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_05664c2d6fea24929b80d203feae6ae4",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_1cf12193ea5071a6eb67e17c2940e538",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_378d55d49125acd037737e17a58ef062",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_43d76111e0811f5312c363f74e37c850",
"refinement_interpretation_Tm_refine_497499815055cac9150608783be5cb0f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5963bab2912d4e29bad06a74cbfcb8be",
"refinement_interpretation_Tm_refine_5b03403a8d3fa4c655ec2b3c1e1359f8",
"refinement_interpretation_Tm_refine_764dc2b54fa2320bf14bc0cb4a02d37d",
"refinement_interpretation_Tm_refine_7679fccd9d7a57bc9b6a8a96f0dcfb4b",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8d84d0eb4d9a59e4351d53d4c37218fc",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d7d6381aa8ac92bd42b55934ccc9b4c4",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_EverCrypt.CTR.footprint_s",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.is_heap_color",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.Set.singleton",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.pointer_or_null",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.loc_unused_in",
"typing_Spec.AES.gf8", "typing_Spec.Agile.Cipher.nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_Spec.Agile.Cipher.CHACHA20@tok"
],
0,
"5a5d639570f16b9c475f56ba5540dc04"
],
[
"EverCrypt.CTR.copy_or_expand",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4eb056135451e14b9dcdc70a35bc3061"
],
[
"EverCrypt.CTR.copy_or_expand",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20",
"disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20",
"disc_equation_Spec.Cipher.Expansion.Vale_AES128",
"disc_equation_Spec.Cipher.Expansion.Vale_AES256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.AES.AES256@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equation_EverCrypt.CTR.Keys.concrete_xkey_len",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.cpu_features_invariant",
"equation_EverCrypt.CTR.uint8",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Prims.squash", "equation_Spec.AES.aes_key",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.key",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Chacha20.key", "equation_Spec.Chacha20.size_key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.concrete_expand",
"equation_Spec.Cipher.Expansion.concrete_xkey",
"equation_Spec.Cipher.Expansion.concrete_xkey_length",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.Cipher.Expansion.uu___30",
"equation_Spec.Cipher.Expansion.vale_xkey_length",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"function_token_typing_Spec.Cipher.Expansion.uu___30",
"int_inversion", "int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"inversion-interp", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_08d038643b0553a506b9818e13398796",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_705774411a48deb390cce9e31dd7c0d7",
"refinement_interpretation_Tm_refine_9100ab96093283c751c14419f2de4403",
"refinement_interpretation_Tm_refine_b924235af49cfbdeff10fa9c9f3258ea",
"refinement_interpretation_Tm_refine_d8c218ede7239d89a3a225bc3541ff51",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_ee6f6de6d08263a0bc873dcc8b983d39",
"refinement_interpretation_Tm_refine_f10315e12d7a82715dc69dbc7dc872a6",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_EverCrypt.CTR.Keys.concrete_xkey_len",
"typing_EverCrypt.TargetConfig.x64", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.minint",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8",
"typing_Spec.Cipher.Expansion.cipher_alg_of_impl",
"typing_Spec.Cipher.Expansion.concrete_expand",
"typing_Spec.Cipher.Expansion.concrete_xkey_length",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U8@tok",
"typing_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"typing_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "unit_inversion",
"unit_typing"
],
0,
"7be1b00716817578fa1ba39a9039ceca"
],
[
"EverCrypt.CTR.init",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def",
"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.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.CTR.uint8",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.aes_key", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.Cipher.key",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Chacha20.key",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"inversion-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_2e3ce49f5ae47c93e010a84fe1062b07",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_d127e0409e6398a978cf187152f34b79",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_EverCrypt.CTR.footprint",
"typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"c56853c3d750a6231e338c7dc2686dcb"
],
[
"EverCrypt.CTR.init",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"ed72eea06b658e3c48c66202dc36ba4d"
],
[
"EverCrypt.CTR.init",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20", "eq2-interp",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equation_EverCrypt.CTR.Keys.concrete_xkey_len",
"equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.ctr",
"equation_EverCrypt.CTR.e_alg", "equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.freeable",
"equation_EverCrypt.CTR.freeable_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "equation_EverCrypt.CTR.iv",
"equation_EverCrypt.CTR.kv",
"equation_EverCrypt.CTR.nonce_upper_bound",
"equation_EverCrypt.CTR.preserves_freeable",
"equation_EverCrypt.CTR.state", "equation_EverCrypt.CTR.uint8",
"equation_FStar.UInt.fits", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "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.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.aes_key", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.AES.key_size",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.block_length",
"equation_Spec.Agile.Cipher.key",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Agile.Cipher.nonce",
"equation_Spec.Agile.Cipher.nonce_bound",
"equation_Spec.Chacha20.key", "equation_Spec.Chacha20.size_key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.concrete_expand",
"equation_Spec.Cipher.Expansion.concrete_xkey",
"equation_Spec.Cipher.Expansion.concrete_xkey_length",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.Cipher.Expansion.uu___30",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"function_token_typing_Spec.Cipher.Expansion.uu___30",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"kinding_Spec.Agile.Cipher.cipher_alg@tok", "l_and-interp",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt32.uv_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_EverCrypt.CTR.State_ctr",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.CTR.State_ctr",
"projection_inverse_EverCrypt.CTR.State_g_iv",
"projection_inverse_EverCrypt.CTR.State_g_key",
"projection_inverse_EverCrypt.CTR.State_i",
"projection_inverse_EverCrypt.CTR.State_iv",
"projection_inverse_EverCrypt.CTR.State_xkey",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_2e3ce49f5ae47c93e010a84fe1062b07",
"refinement_interpretation_Tm_refine_3f6af2a10c13712b3aa160d04bbf782c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5afd134e68e42a30c35feaa60c623f3d",
"refinement_interpretation_Tm_refine_6a494d5de105c0e0c1721b52fdb89ff1",
"refinement_interpretation_Tm_refine_9100ab96093283c751c14419f2de4403",
"refinement_interpretation_Tm_refine_94e9a7f41130db86d255f278b02a4022",
"refinement_interpretation_Tm_refine_ba58c21e19049243e6257a6b4a615bc6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d127e0409e6398a978cf187152f34b79",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_EverCrypt.CTR.Keys.concrete_xkey_len",
"typing_EverCrypt.CTR.footprint", "typing_EverCrypt.CTR.footprint_s",
"typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.create",
"typing_FStar.Set.singleton", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.unsigned",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8",
"typing_Spec.Agile.Cipher.key", "typing_Spec.Agile.Cipher.nonce",
"typing_Spec.Cipher.Expansion.concrete_expand",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"cca4afb1ce49adefbe6b3aa347a665ba"
],
[
"EverCrypt.CTR.update_block_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.CTR.uint8", "equation_Lib.IntTypes.uint8",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_95c833bcb65bb030c0b462efadcd5888",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"e49c3b55322fa479f37d59d09876d388"
],
[
"EverCrypt.CTR.as_vale_key",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES128",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES256",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.AES.AES256@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl",
"equation_EverCrypt.CTR.Keys.vale_impl",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.aes_key", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.AES.key_size",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.key", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.Cipher.Expansion.uu___30",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"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",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"function_token_typing_Spec.Cipher.Expansion.uu___30",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "inversion-interp",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Modulus",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.Cipher.Expansion.cipher_alg_of_impl",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"b364e89c16e13e3522c7a0796c4de5bc"
],
[
"EverCrypt.CTR.vale_encrypt_is_hacl_encrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES128",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES256",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equation_EverCrypt.CTR.Keys.vale_impl",
"equation_EverCrypt.CTR.as_vale_key", "equation_EverCrypt.CTR.uint8",
"equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.block", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.Cipher.key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.uu___30",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Vale.AES.GCTR.make_gctr_plain_LE",
"equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
"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",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Cipher.Expansion.uu___30",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"inversion-interp", "lemma_FStar.Seq.Base.lemma_init_len",
"primitive_Prims.op_LessThan", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_1be7654c744eb647c46ba49213fc6462",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_EverCrypt.CTR.as_vale_key", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"f29e419a95d25984616164155ccefb70"
],
[
"EverCrypt.CTR.gctr_bytes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Prims.unit",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES128",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES256",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.AES.AES_s.algorithm",
"disc_equation_Spec.Cipher.Expansion.Vale_AES128",
"disc_equation_Spec.Cipher.Expansion.Vale_AES256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl",
"equation_EverCrypt.CTR.Keys.vale_impl",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_a00be2c1adcdd9b306da4262e1e66842",
"refinement_interpretation_Tm_refine_af0abb6a5fb528629a14e88d5f4701d0",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f2a716a9cba0850f388b77a430325223",
"typing_EverCrypt.CTR.Keys.vale_alg_of_vale_impl",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"unit_typing"
],
0,
"32e038b9778d7ec9eec1eada88e8275d"
],
[
"EverCrypt.CTR.uint128_of_uint32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Int.Cast.uint32_to_uint64",
"equation_FStar.UInt128.n", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
"typing_FStar.Int.Cast.uint32_to_uint64"
],
0,
"b2350f3fae2720b7e75c08be2f3cb795"
],
[
"EverCrypt.CTR.update_block_vale",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"EverCrypt.CTR_interpretation_Tm_arrow_4cce1bc00dadd7d3c18f14a422b8e5e8",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868",
"LowStar.Buffer_interpretation_Tm_arrow_9b1c273e798ef422e9aacaac3436c4f3",
"Prims_interpretation_Tm_ghost_arrow_0283b8a2a36bbec52abac4e3d837674a",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES128",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES256",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.CTR.Keys.key_offset",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl",
"equation_EverCrypt.CTR.Keys.vale_impl",
"equation_EverCrypt.CTR.as_vale_key",
"equation_EverCrypt.CTR.cpu_features_invariant",
"equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s",
"equation_EverCrypt.CTR.nonce_upper_bound",
"equation_EverCrypt.CTR.state", "equation_EverCrypt.CTR.uint8",
"equation_FStar.Endianness.bytes",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.poppable",
"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_FStar.UInt128.n", "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.uint8",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.Cipher.block_length",
"equation_Spec.Agile.Cipher.key", "equation_Spec.Agile.Cipher.nonce",
"equation_Spec.Agile.Cipher.nonce_bound",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.concrete_expand",
"equation_Spec.Cipher.Expansion.concrete_xkey",
"equation_Spec.Cipher.Expansion.concrete_xkey_length",
"equation_Spec.Cipher.Expansion.uu___29",
"equation_Spec.Cipher.Expansion.uu___30",
"equation_Spec.Cipher.Expansion.vale_aes_expansion",
"equation_Spec.Cipher.Expansion.vale_alg_of_cipher_alg",
"equation_Spec.Cipher.Expansion.vale_xkey_length",
"equation_Spec.GaloisField.gf", "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.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_EverCrypt.CTR.as_vale_key",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Cipher.Expansion.uu___29",
"function_token_typing_Spec.Cipher.Expansion.uu___30",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"l_and-interp", "lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.CTR.State_g_key",
"projection_inverse_EverCrypt.CTR.State_i",
"projection_inverse_EverCrypt.CTR.State_iv",
"projection_inverse_EverCrypt.CTR.State_xkey",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_1be7654c744eb647c46ba49213fc6462",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_2de624c162d100733662a5fed8d478ed",
"refinement_interpretation_Tm_refine_2f292d5f43402770c987311a02f5bb40",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_3f76b9bacc0c0c60cbff15d3cf051638",
"refinement_interpretation_Tm_refine_4093bc774a5fc0f519ad85d52272f044",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_785b445c1ccb59eaa8c666ff5bddec28",
"refinement_interpretation_Tm_refine_79f1f8b4d6774015af27e4432311c913",
"refinement_interpretation_Tm_refine_7c427542bcd2674efa54058831b0190e",
"refinement_interpretation_Tm_refine_849d11bd4488c6a32fa952ced0f4d828",
"refinement_interpretation_Tm_refine_94e9a7f41130db86d255f278b02a4022",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e10c95eacadfb5ac09085a6a4bed17f5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_EverCrypt.CTR.as_vale_key", "true_interp",
"typing_EverCrypt.CTR.Keys.key_offset",
"typing_EverCrypt.CTR.footprint_s",
"typing_FStar.Endianness.le_to_n", "typing_FStar.Ghost.elift1",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt128.v", "typing_FStar.UInt32.t",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8",
"typing_Spec.Agile.Cipher.key", "typing_Spec.Agile.Cipher.nonce",
"typing_Spec.Chacha20.size_key",
"typing_Spec.Cipher.Expansion.cipher_alg_of_impl",
"typing_Spec.Cipher.Expansion.concrete_expand",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.AES.AES_s.aes_encrypt_LE",
"typing_Vale.AES.AES_s.key_to_round_keys_LE",
"typing_Vale.AES.OptPublic.get_hkeys_reqs",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"c0c70f5a0645e03fe00b88cb058a690e"
],
[
"EverCrypt.CTR.update_block",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20",
"disc_equation_Spec.Cipher.Expansion.Vale_AES128",
"disc_equation_Spec.Cipher.Expansion.Vale_AES256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_EverCrypt.CTR.cpu_features_invariant",
"equation_EverCrypt.CTR.e_alg", "equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s",
"equation_EverCrypt.CTR.nonce_upper_bound",
"equation_EverCrypt.CTR.state", "equation_EverCrypt.CTR.uint8",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t",
"equation_Hacl.Impl.Chacha20.Core32.state",
"equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "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.size_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.Cipher.block_length",
"equation_Spec.Cipher.Expansion.cipher_alg_of_impl",
"equation_Spec.Cipher.Expansion.concrete_xkey_length",
"equation_Spec.Cipher.Expansion.uu___30",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Cipher.Expansion.uu___30",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"inversion-interp", "kinding_EverCrypt.CTR.state_s@tok",
"kinding_Spec.Agile.Cipher.cipher_alg@tok", "l_and-interp",
"lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.CTR.State_i",
"projection_inverse_EverCrypt.CTR.State_iv",
"projection_inverse_EverCrypt.CTR.State_xkey",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_16de093b5ba451a7237c9b46a641c643",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_3f6af2a10c13712b3aa160d04bbf782c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_52fa6887aa0e6889614b243798842a3c",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_6a494d5de105c0e0c1721b52fdb89ff1",
"refinement_interpretation_Tm_refine_94e9a7f41130db86d255f278b02a4022",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_af63369ba3e567e0d5939aa72ed434ab",
"refinement_interpretation_Tm_refine_bc761841f54eddf278259ea4158a0001",
"refinement_interpretation_Tm_refine_c85ac554457a2a3b150767cec1963310",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"refinement_interpretation_Tm_refine_f8baffb8cd8aa8f0ee18caedcdd0792e",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_EverCrypt.TargetConfig.x64",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.t", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.loc",
"typing_Lib.Sequence.create",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "unit_inversion", "unit_typing"
],
0,
"e90ceaa689e442ff02e7338b4fd6be3a"
],
[
"EverCrypt.CTR.free",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_typing",
"equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.e_alg",
"equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.footprint_s",
"equation_EverCrypt.CTR.freeable",
"equation_EverCrypt.CTR.freeable_s",
"equation_EverCrypt.CTR.invariant",
"equation_EverCrypt.CTR.invariant_s", "equation_EverCrypt.CTR.state",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"kinding_EverCrypt.CTR.state_s@tok",
"kinding_Spec.Agile.Cipher.cipher_alg@tok", "l_and-interp",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_LowStar.Monotonic.Buffer.freeable_disjoint_",
"lemma_LowStar.Monotonic.Buffer.freeable_length",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"projection_inverse_EverCrypt.CTR.State_iv",
"projection_inverse_EverCrypt.CTR.State_xkey",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_31ba8778ae2ab6e5eb721953a281e1b2",
"refinement_interpretation_Tm_refine_3f6af2a10c13712b3aa160d04bbf782c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_94e9a7f41130db86d255f278b02a4022",
"refinement_interpretation_Tm_refine_a196cb30b51cff857036aa82d52ec892",
"refinement_interpretation_Tm_refine_b443d6cebd48a51c9661a0986c617cf2",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_EverCrypt.CTR.footprint", "typing_EverCrypt.CTR.footprint_s",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"dbb75bf3913dbbff88d3ff1b6a32165c"
]
]
]
Computing file changes ...
