Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Spec.AEAD.fsti.hints
[
"�(�\u001de�����\u0017^7C\nq",
[
[
"Spec.AEAD.uu___2",
1,
0,
0,
[ "@query" ],
0,
"de4d3b4a8ef2d659ca98cb2eaf79ba75"
],
[
"Spec.AEAD.cipher_alg_of_supported_alg",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"typing_Spec.AEAD.is_supported_alg"
],
0,
"4a2e13bbf0dbd05cc0f1934ac739f480"
],
[
"Spec.AEAD.key_length",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Spec.AEAD.AES128_CCM",
"disc_equation_Spec.AEAD.AES128_CCM8",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_CCM",
"disc_equation_Spec.AEAD.AES256_CCM8",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Pervasives.inversion",
"equation_Lib.IntTypes.unsigned",
"equation_Spec.AEAD.is_supported_alg", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.AEAD.alg", "inversion-interp",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AEAD.is_supported_alg", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"14ff6885a18e153208535164643c6f4c"
],
[
"Spec.AEAD.tag_length",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Spec.AEAD.AES128_CCM",
"disc_equation_Spec.AEAD.AES128_CCM8",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_CCM",
"disc_equation_Spec.AEAD.AES256_CCM8",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equation_FStar.Pervasives.inversion",
"fuel_guarded_inversion_Spec.AEAD.alg", "inversion-interp"
],
0,
"ef061b81fbdb5c31b2dedae0aa6f1b2b"
],
[
"Spec.AEAD.iv_length",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.Winfinite",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_FStar.Integers.width_of_sw",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"typing_Spec.AEAD.is_supported_alg"
],
0,
"370141f6da8bb4d2ab8ee855735beeda"
],
[
"Spec.AEAD.max_length",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"typing_Prims.pow2", "typing_Spec.AEAD.is_supported_alg"
],
0,
"cd93909b3dfa5d3117d01a2bd4851e80"
],
[
"Spec.AEAD.lbytes",
1,
0,
0,
[ "@query" ],
0,
"20f6f6683d0c830a273e99acd00a99a3"
],
[
"Spec.AEAD.correctness",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.AEAD.cipher_length",
"equation_Spec.AEAD.encrypted", "equation_Spec.AEAD.max_length",
"equation_Spec.AEAD.plain", "equation_Spec.AEAD.tag_length",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_064506d56a6af7ceef8b06aef3cb54e5",
"refinement_interpretation_Tm_refine_ff4fb9e743a804b2a539fcf5d276f129",
"typing_Spec.AEAD.encrypt"
],
0,
"155c84d2d1c0d8b3d3eecb5b50e55eab"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...