Revision aa211c2d5a40dd6969fe8a469fcadfd27e8c8fe3 authored by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC, committed by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC
1 parent 6f91754
Vale.Poly1305.Equiv.fsti.hints
[
"r�G�a}\u001c��}\u0001s8\u0015�",
[
[
"Vale.Poly1305.Equiv.block_fun",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_Spec.Poly1305.size_key"
],
0,
"260ec3f6e2da1e95b92ccc61968e7b4a"
],
[
"Vale.Poly1305.Equiv.lemma_poly1305_equiv",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.Poly1305.key", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.ByteSequence.nat_from_bytes_le",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
"typing_tok_Lib.IntTypes.SEC@tok"
],
0,
"4a8da749551683e78f56cc0d1f64011f"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...