Revision 84e3cebb5d2a7c2c7bef04ff990b5277b6b1e883 authored by Nikhil Swamy on 10 May 2017, 14:15:34 UTC, committed by Nikhil Swamy on 10 May 2017, 14:15:34 UTC
Spec.GaloisField.fst.hints
[
"9ćcKą_ˇ+ —™\u0002hu5f",
[
[
"Spec.GaloisField.polynomial",
1,
2,
1,
[
"@query", "equation_Prims.nat", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.GaloisField.field",
1,
2,
1,
[
"@query", "equation_Prims.pos", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0
],
[
"Spec.GaloisField.field",
2,
2,
1,
[
"@query", "equation_Prims.pos", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0
],
[
"Spec.GaloisField.field",
3,
2,
1,
[
"@query", "equation_Prims.pos", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0
],
[
"Spec.GaloisField.field",
4,
2,
1,
[
"@query", "assumption_FStar.Seq.Base.seq_haseq",
"assumption_Prims.HasEq_bool", "assumption_Prims.HasEq_int",
"bool_typing", "equation_FStar.BitVector.bv_t", "equation_Prims.pos",
"equation_Spec.GaloisField.polynomial",
"function_token_typing_Prims.bool",
"haseqTm_refine_d70501a9ebd0660fc59c3349dad118ea",
"haseqTm_refine_f048236b5f8051f83b495ea5eaa6127b",
"pretyping_f537159ed795b314b4e58c260361ae86",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction"
],
0
],
[ "Spec.GaloisField.__proj__GF__item__bits", 1, 2, 1, [ "@query" ], 0 ],
[
"Spec.GaloisField.__proj__GF__item__irred",
1,
2,
1,
[
"@query", "equation_Prims.pos", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.__proj__GF__item__irred",
2,
2,
1,
[
"@query", "proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_Spec.GaloisField.GF_bits"
],
0
],
[
"Spec.GaloisField.mk_field",
1,
2,
1,
[
"@query", "equation_Prims.pos", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0
],
[ "Spec.GaloisField.felem", 1, 2, 1, [ "@query" ], 0 ],
[
"Spec.GaloisField.to_felem",
1,
2,
1,
[
"@query", "equation_Prims.pos",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[ "Spec.GaloisField.from_felem", 1, 2, 1, [ "@query" ], 0 ],
[
"Spec.GaloisField.one",
1,
2,
1,
[
"@query", "equation_Prims.pos",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.add_comm",
1,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"equation_Prims.pos",
"fuel_guarded_inversion_Spec.GaloisField.field",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.add_comm",
2,
2,
1,
[
"@query", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_Prims.nat", "equation_Spec.GaloisField.fadd",
"equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.op_Plus_At",
"fuel_guarded_inversion_Spec.GaloisField.field",
"function_token_typing_Prims.bool", "int_inversion",
"lemma_FStar.BitVector.logxor_vec_definition",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"pretyping_f537159ed795b314b4e58c260361ae86",
"primitive_Prims.op_disEquality",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_9434c22c43537f4024e402e2621d048d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c44d6b2b02c0b515cd6e2f4d9892c368",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"typing_Spec.GaloisField.__proj__GF__item__bits",
"typing_Spec.GaloisField.op_Plus_At"
],
0
],
[
"Spec.GaloisField.add_asso",
1,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"equation_Prims.pos",
"fuel_guarded_inversion_Spec.GaloisField.field",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.add_asso",
2,
2,
1,
[
"@query", "bool_inversion", "bool_typing",
"equation_FStar.BitVector.bv_t", "equation_Prims.nat",
"equation_Spec.GaloisField.fadd", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.op_Plus_At",
"fuel_guarded_inversion_Spec.GaloisField.field",
"function_token_typing_Prims.bool",
"function_token_typing_Spec.GaloisField.op_Plus_At", "int_inversion",
"interpretation_Tm_arrow_a3662d68abfe43fc72a68aef5d4b0cc9",
"lemma_FStar.BitVector.logxor_vec_definition",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"pretyping_f537159ed795b314b4e58c260361ae86",
"primitive_Prims.op_disEquality",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c44d6b2b02c0b515cd6e2f4d9892c368",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"refinement_interpretation_Tm_refine_e8f9e19c92aa620b31a57e9462b0d317",
"refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
"token_correspondence_Spec.GaloisField.op_Plus_At",
"typing_FStar.Seq.Base.index",
"typing_Spec.GaloisField.__proj__GF__item__bits",
"typing_Spec.GaloisField.fadd", "typing_Spec.GaloisField.op_Plus_At"
],
0
],
[
"Spec.GaloisField.add_zero",
1,
2,
1,
[
"@query", "assumption_FStar.Seq.Base.seq_haseq",
"assumption_Prims.HasEq_bool", "assumption_Prims.HasEq_int",
"bool_typing", "equation_Prims.nat", "equation_Prims.pos",
"fuel_guarded_inversion_Spec.GaloisField.field",
"function_token_typing_Prims.bool",
"haseqTm_refine_b3222c15d4263a14769c5404a772e49b",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"pretyping_f537159ed795b314b4e58c260361ae86",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.add_zero",
2,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"equation_Prims.pos",
"fuel_guarded_inversion_Spec.GaloisField.field",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.add_zero",
3,
2,
1,
[
"@query", "bool_inversion", "bool_typing",
"equation_FStar.BitVector.bv_t", "equation_FStar.BitVector.zero_vec",
"equation_Prims.nat", "equation_Spec.GaloisField.fadd",
"equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.op_Plus_At",
"equation_Spec.GaloisField.zero",
"fuel_guarded_inversion_Spec.GaloisField.field",
"function_token_typing_Prims.bool", "int_inversion",
"lemma_FStar.BitVector.logxor_vec_definition",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_create",
"pretyping_f537159ed795b314b4e58c260361ae86",
"primitive_Prims.op_disEquality",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_3da648c6210d05df459edc3e0e276b34",
"refinement_interpretation_Tm_refine_9434c22c43537f4024e402e2621d048d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c44d6b2b02c0b515cd6e2f4d9892c368",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Spec.GaloisField.__proj__GF__item__bits",
"typing_Spec.GaloisField.op_Plus_At"
],
0
],
[
"Spec.GaloisField.shift_reduce",
1,
2,
1,
[
"@query", "equation_FStar.BitVector.bv_t", "equation_Prims.pos",
"equation_Spec.GaloisField.felem",
"fuel_guarded_inversion_Spec.GaloisField.field", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.shift_reduce",
2,
2,
1,
[ "@query", "assumption_Prims.HasEq_bool" ],
0
],
[
"Spec.GaloisField.cond_fadd",
1,
2,
1,
[
"@query", "equation_FStar.BitVector.bv_t", "equation_Prims.nat",
"equation_Spec.GaloisField.felem",
"fuel_guarded_inversion_Spec.GaloisField.field",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_bd0b5d3224ab1085f5b9e65129c924fd",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea"
],
0
],
[
"Spec.GaloisField.cond_fadd",
2,
2,
1,
[ "@query", "assumption_Prims.HasEq_bool" ],
0
],
[
"Spec.GaloisField.cond_fadd_lemma",
1,
2,
1,
[
"@query", "assumption_FStar.Seq.Base.seq_haseq",
"assumption_Prims.HasEq_bool", "assumption_Prims.HasEq_int",
"bool_typing", "equation_Prims.nat",
"fuel_guarded_inversion_Spec.GaloisField.field",
"function_token_typing_Prims.bool",
"haseqTm_refine_b3222c15d4263a14769c5404a772e49b",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"pretyping_f537159ed795b314b4e58c260361ae86",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bd0b5d3224ab1085f5b9e65129c924fd"
],
0
],
[
"Spec.GaloisField.cond_fadd_lemma",
2,
2,
1,
[
"@query", "fuel_guarded_inversion_Spec.GaloisField.field",
"refinement_interpretation_Tm_refine_b3222c15d4263a14769c5404a772e49b"
],
0
],
[
"Spec.GaloisField.cond_fadd_lemma",
3,
2,
1,
[
"@query", "equation_FStar.BitVector.bv_t",
"equation_FStar.List.Tot.Base.test_sort", "equation_Prims._assert",
"equation_Prims.nat", "equation_Spec.GaloisField.cond_fadd",
"equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.op_Plus_At",
"fuel_guarded_inversion_Spec.GaloisField.field",
"function_token_typing_FStar.List.Tot.Base.test_sort",
"int_inversion", "proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bd0b5d3224ab1085f5b9e65129c924fd",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"unit_inversion"
],
0
],
[
"Spec.GaloisField.cond_fadd_lemma",
4,
2,
1,
[ "@query", "assumption_Prims.HasEq_bool" ],
0
],
[
"Spec.GaloisField.fmul_loop",
1,
2,
1,
[
"@query", "binder_x_6a0b9084ba72fceece298e4ca3ddea66_3",
"binder_x_7f463b7e9970c4906c62a2d09b5645c0_0",
"binder_x_a4d91362c8910a3b2735ea125f316776_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Spec.GaloisField.shift_reduce",
"fuel_guarded_inversion_Spec.GaloisField.field", "int_inversion",
"int_typing", "pretyping_f537159ed795b314b4e58c260361ae86",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_07756818317f4fb4ea58d78214a9d1fb",
"refinement_interpretation_Tm_refine_326c0846fef922ec27d6e97e5c533bc0",
"refinement_interpretation_Tm_refine_b3222c15d4263a14769c5404a772e49b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c5982a6af31648b3f424c33b277bf009",
"typing_Spec.GaloisField.shift_reduce",
"well-founded-ordering-on-nat"
],
0
],
[
"Spec.GaloisField.fmul_loop",
2,
2,
1,
[
"@query", "assumption_Prims.HasEq_int",
"haseqTm_refine_07756818317f4fb4ea58d78214a9d1fb"
],
0
],
[
"Spec.GaloisField.fmul",
1,
2,
1,
[
"@query", "equation_Prims.pos",
"proj_equation_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.GaloisField.__proj__GF__item__bits"
],
0
],
[
"Spec.GaloisField.irr",
1,
2,
1,
[
"@query", "b2t_def", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt8.n",
"equation_Prims.nat", "function_token_typing_FStar.UInt8.n",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.GaloisField.gf8",
1,
2,
1,
[
"@query", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.GaloisField.a",
1,
2,
1,
[
"@query", "b2t_def", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Spec.GaloisField.gf8", "equation_Spec.GaloisField.irr",
"equation_Spec.GaloisField.mk_field",
"equation_Spec.GaloisField.polynomial",
"function_token_typing_Prims.bool",
"function_token_typing_Spec.GaloisField.irr",
"lemma_FStar.UInt.pow2_values",
"pretyping_f537159ed795b314b4e58c260361ae86",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.GaloisField.b",
1,
2,
1,
[
"@query", "b2t_def", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Spec.GaloisField.a", "equation_Spec.GaloisField.gf8",
"equation_Spec.GaloisField.irr",
"equation_Spec.GaloisField.mk_field",
"equation_Spec.GaloisField.to_felem",
"function_token_typing_Prims.bool",
"function_token_typing_Spec.GaloisField.a",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.GaloisField.a_plus_b",
1,
2,
1,
[
"@query", "b2t_def", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Spec.GaloisField.a", "equation_Spec.GaloisField.gf8",
"equation_Spec.GaloisField.irr",
"equation_Spec.GaloisField.mk_field",
"equation_Spec.GaloisField.to_felem",
"function_token_typing_Prims.bool",
"function_token_typing_Spec.GaloisField.a",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_bits",
"refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.GaloisField.test",
1,
2,
1,
[
"@query", "assumption_FStar.Seq.Base.seq_haseq",
"assumption_Prims.HasEq_bool", "assumption_Prims.HasEq_int",
"bool_typing", "equation_Prims.nat", "equation_Spec.GaloisField.gf8",
"equation_Spec.GaloisField.irr",
"equation_Spec.GaloisField.mk_field",
"function_token_typing_Prims.bool",
"haseqTm_refine_b3222c15d4263a14769c5404a772e49b",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"pretyping_f537159ed795b314b4e58c260361ae86",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_bits"
],
0
],
[
"Spec.GaloisField.test",
2,
2,
1,
[
"@query", "assumption_FStar.Seq.Base.seq_haseq",
"assumption_Prims.HasEq_bool", "assumption_Prims.HasEq_int",
"bool_typing", "equation_Prims.nat", "equation_Spec.GaloisField.gf8",
"equation_Spec.GaloisField.irr",
"equation_Spec.GaloisField.mk_field",
"function_token_typing_Prims.bool",
"haseqTm_refine_b3222c15d4263a14769c5404a772e49b",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"pretyping_f537159ed795b314b4e58c260361ae86",
"proj_equation_Spec.GaloisField.GF_bits",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_bits"
],
0
]
]
]
Computing file changes ...
