Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC
1 parent 2a5defc
Vale.Curve25519.X64.FastSqr.fst.hints
[
"\u001d��\u0013�&��80�%�p�[",
[
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_part1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.Interop.Types.TUInt64",
"equality_tok_Vale.Interop.Types.TUInt64@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"f36a8d4d0d2717c6fcc64fd7619aee8e"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_part1",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.Interop.Types.TUInt64",
"equality_tok_Vale.Interop.Types.TUInt64@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"699f2aa70d3413f1e0f85707590e5758"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_part1",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.Interop.Types.TUInt64",
"equality_tok_Vale.Interop.Types.TUInt64@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"05bf7694696bc83da0c8cc336057ffcf"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_part1",
4,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.Interop.Types.TUInt64",
"equality_tok_Vale.Interop.Types.TUInt64@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"ce984385b7adda8c78e805f90e14b712"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_part1",
5,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.Interop.Types.TUInt64",
"equality_tok_Vale.Interop.Types.TUInt64@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"ea852048f72aec8cd0c4b12f06bea401"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_part1",
6,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.Interop.Types.TUInt64",
"equality_tok_Vale.Interop.Types.TUInt64@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"d4fd03d16252816de10667474adef61a"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr_part1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"bool_typing", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Curve25519.Fast_defs.mul_nats",
"equation_Vale.Curve25519.Fast_defs.pow2_five",
"equation_Vale.Curve25519.Fast_defs.pow2_four",
"equation_Vale.Curve25519.Fast_defs.pow2_six",
"equation_Vale.Curve25519.Fast_defs.pow2_three",
"equation_Vale.Curve25519.Fast_defs.pow2_two",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.validSrcAddrs64",
"equation_Vale.X64.Decls.valid_maddr",
"equation_Vale.X64.Decls.valid_mem_operand",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"interpretation_Tm_abs_04b3853ff0623c15df32998ca19b9893",
"interpretation_Tm_abs_7aa638e85f956c56af9e7ebf7d5b8c65",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Xmms.lemma_equal_intro",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cf45485a3681cbe0d30939f25c2614df",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Prims.eq2",
"typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.Decls.cf", "typing_Vale.X64.Decls.update_cf",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms",
"unit_inversion", "unit_typing"
],
0,
"7b6a98397561b6614433d2169f9e5800"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpMonotone_fast_sqr_part1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part1",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"e98216ffb72669f852b909058c7ddb1e"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part1",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.X64.State.state"
],
0,
"92dc21124df717b7f0f868fffed0a915"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_part1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"b6946518c9990e01b37b0780fbce8e32"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_part1",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part1",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part1",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Xmms.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.State.Mkstate_flags",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"projection_inverse_Vale.X64.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part1",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkstate__item__flags",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms", "unit_typing"
],
0,
"464f2ae9ee00a3a70f9da6ef06a1b2a3"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr_part2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"proj_equation_Vale.X64.State.Mkstate_regs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__regs"
],
0,
"0a57cff471593f00f06f2957a2361cc4"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr_part2",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"bool_typing", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Curve25519.Fast_defs.pow2_five",
"equation_Vale.Curve25519.Fast_defs.pow2_four",
"equation_Vale.Curve25519.Fast_defs.pow2_seven",
"equation_Vale.Curve25519.Fast_defs.pow2_six",
"equation_Vale.Curve25519.Fast_defs.pow2_three",
"equation_Vale.Curve25519.Fast_defs.pow2_two",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.QuickCodes.range1",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_04b3853ff0623c15df32998ca19b9893",
"interpretation_Tm_abs_0d45dfc04bc6ea8e9a36599a56717bf2",
"interpretation_Tm_abs_7aa638e85f956c56af9e7ebf7d5b8c65",
"interpretation_Tm_abs_a7ecc8edd9a298a79dd9e61710866b7a",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Xmms.lemma_equal_intro",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
"refinement_interpretation_Tm_refine_a44999678a1ef301461788009870b35b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cf45485a3681cbe0d30939f25c2614df",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Vale.Curve25519.Fast_defs.pow2_six",
"typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.Decls.cf", "typing_Vale.X64.Decls.overflow",
"typing_Vale.X64.Decls.update_cf", "typing_Vale.X64.Decls.update_of",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms",
"unit_inversion", "unit_typing"
],
0,
"22efe2e2d0be5fe67f5a3a4a710ca4fc"
],
[
"Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"proj_equation_Vale.X64.State.Mkstate_regs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__regs"
],
0,
"9cc9e1af94084ecf2d8b47c600792df6"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpMonotone_fast_sqr_part2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part2",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"24f5980d01fa18fd358e2e14c741f82d"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part2",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.X64.State.state"
],
0,
"a7359499dd1353ccaa0af9f93a4b228d"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_part2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"709c726854812c2f7bfb1ea13ffb1905"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_part2",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp",
"equation_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part2",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part2",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Xmms.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.State.Mkstate_flags",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"projection_inverse_Vale.X64.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part2",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__flags",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms", "unit_typing"
],
0,
"38a49f508bc1dd3e941be16924cc3989"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_part3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Tactics.CanonCommMonoid.var",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Curve25519.Fast_defs.add_carry",
"equation_Vale.Curve25519.Fast_defs.mul_nats",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_FStar.Tactics.CanonCommMonoid.var",
"typing_Vale.Curve25519.Fast_defs.mul_nats",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__regs"
],
0,
"69d6ec27e4bf3e10aec518eae309cc12"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr_part3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Curve25519.Fast_defs.mul_nats",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"proj_equation_Vale.X64.State.Mkstate_regs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.Curve25519.Fast_defs.mul_nats",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__regs"
],
0,
"0657b61681d15fdf7b9bb32650d8e99d"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr_part3",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"bool_typing", "constructor_distinct_Vale.Interop.Types.TUInt64",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"data_typing_intro_Vale.X64.Machine_s.OReg@tok", "eq2-interp",
"equality_tok_Vale.Interop.Types.TUInt64@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.l_and", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Curve25519.Fast_defs.add_carry",
"equation_Vale.Curve25519.Fast_defs.bool_bit",
"equation_Vale.Curve25519.Fast_defs.mul_nats",
"equation_Vale.Curve25519.Fast_defs.pow2_eight",
"equation_Vale.Curve25519.Fast_defs.pow2_nine",
"equation_Vale.Def.Prop_s.prop0",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.modifies_buffer_specific",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.QuickCodes.range1",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.state_eta",
"equation_Vale.X64.State.update_reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_04b3853ff0623c15df32998ca19b9893",
"interpretation_Tm_abs_7aa638e85f956c56af9e7ebf7d5b8c65",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.modifies_buffer_addr",
"lemma_Vale.X64.Memory.modifies_buffer_elim",
"lemma_Vale.X64.Memory.modifies_buffer_readable",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
"lemma_Vale.X64.Memory.modifies_valid_taint64",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_eta", "lemma_Vale.X64.Regs.lemma_upd_eq",
"lemma_Vale.X64.Regs.lemma_upd_ne",
"lemma_Vale.X64.Xmms.lemma_equal_intro",
"lemma_Vale.X64.Xmms.lemma_eta", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.X64.Machine_s.OReg_r",
"projection_inverse_Vale.X64.State.Mkstate_flags",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
"refinement_interpretation_Tm_refine_809440a2e49ae18d732467ba1f4c9c0b",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
"refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cf45485a3681cbe0d30939f25c2614df",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_FStar.Seq.Base.upd",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_Prims.l_and", "typing_Vale.Curve25519.Fast_defs.mul_nats",
"typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.Decls.modifies_buffer_specific",
"typing_Vale.X64.Decls.update_cf",
"typing_Vale.X64.Decls.va_upd_operand_dst_opr64",
"typing_Vale.X64.Decls.validSrcAddrs64",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.buffer_readable",
"typing_Vale.X64.Memory.buffer_write",
"typing_Vale.X64.Memory.buffer_writeable",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms",
"typing_Vale.X64.State.state_eta",
"typing_Vale.X64.State.update_reg",
"typing_tok_Vale.Interop.Types.TUInt64@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"974339daf056f27a3fa40290bce6ffda"
],
[
"Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Curve25519.Fast_defs.mul_nats",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"proj_equation_Vale.X64.State.Mkstate_regs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.Curve25519.Fast_defs.mul_nats",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__regs"
],
0,
"f1d27c456bbb9a9d7ca242e123fd643d"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpMonotone_fast_sqr_part3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part3",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"68e49fac1aa18eb8930c6a73fd86ffef"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part3",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.X64.State.state"
],
0,
"3a987b32a6fac2177a79913217ec4976"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_part3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"c95d126f0cdc27b7c09b24b7e4a3c78f"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_part3",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part3",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_part3",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Xmms.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.State.Mkstate_flags",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"projection_inverse_Vale.X64.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_part3",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__flags",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms", "unit_typing"
],
0,
"6d2b9012385c238a3f90326cfd6ae78a"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr",
1,
1,
0,
[ "@query" ],
0,
"4e2a8baac984507525cfa82fbc4cf6f4"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Curve25519.Fast_defs.mul_nats",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Vale.Curve25519.Fast_defs.mul_nats"
],
0,
"9482259eb338ce5b3bf1f5e14c2a4c2c"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"bb786f9cc748583f8ebc5a345fa9a101"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Vale.Interop.Types.TUInt64", "eq2-interp",
"equality_tok_Vale.Interop.Types.TUInt64@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Curve25519.Fast_defs.mul_nats",
"equation_Vale.Curve25519.Fast_defs.pow2_eight",
"equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.QuickCodes.range1",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"l_and-interp", "lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Xmms.lemma_equal_intro",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "true_interp", "typing_Prims.eq2",
"typing_Vale.Curve25519.Fast_defs.mul_nats",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.Decls.modifies_buffer_specific",
"typing_Vale.X64.Decls.validSrcAddrs64",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms",
"typing_tok_Vale.Interop.Types.TUInt64@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"27aeaf40dbc56f15fdabdce3a61b0d47"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.State.state_eta",
"proj_equation_Vale.X64.State.Mkstate_mem",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"refinement_interpretation_Tm_refine_3a2f2b102c61aa0af3921b204a62e0ad",
"refinement_interpretation_Tm_refine_603bafd9f506525f10121a222be203b4",
"refinement_interpretation_Tm_refine_99b916266dfcd61a595db27cbc92ad5c",
"refinement_interpretation_Tm_refine_adcb2d85ae3a769829541b8d0a3dd4eb",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_ebfe2fb1af24a56887e1cb18cf9dbb6f"
],
0,
"5c7e62b09b0aa12cd82e7b99bd768eaa"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr",
4,
1,
0,
[ "@query" ],
0,
"346e512df7acfac0c543850f52a08829"
],
[
"Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"cdfb722e56880ac75ef2b8214e29330a"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpMonotone_fast_sqr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"a5dcda7dfb2c771fb705db190da6be75"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.X64.State.state"
],
0,
"c307c7344bc84f7acb1d01f8ca9bcbeb"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"f772f55435be0d03e7da2935475185d7"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Xmms.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.State.Mkstate_flags",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"projection_inverse_Vale.X64.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkstate__item__flags",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms", "unit_typing"
],
0,
"3f91bddd552771f01475e00ee43ef26d"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_fast_sqr_stdcall",
1,
1,
0,
[ "@query" ],
0,
"02abb0ad630837b8e2f1b6b2a2b6755f"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.X64.Decls.validDstAddrs64",
"fuel_guarded_inversion_Vale.X64.State.state",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"refinement_interpretation_Tm_refine_8cf601f1a6aec07ee65cf8e31b044179"
],
0,
"74eb379b2d103b95243a52b7ba752a15"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_fast_sqr_stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.Interop.Types.TUInt64@tok",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Curve25519.Fast_defs.pow2_eight",
"equation_Vale.Curve25519.Fast_defs.pow2_five",
"equation_Vale.Curve25519.Fast_defs.pow2_four",
"equation_Vale.Curve25519.Fast_defs.pow2_seven",
"equation_Vale.Curve25519.Fast_defs.pow2_six",
"equation_Vale.Curve25519.Fast_defs.pow2_three",
"equation_Vale.Curve25519.Fast_defs.pow2_two",
"equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.modifies_buffer_specific",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.QuickCodes.range1",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_06895279704f00fdc02dbeaa6d281b82",
"interpretation_Tm_abs_2b7fd08e20cc3c4be5c6c50b1827e1b8",
"interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
"interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
"l_and-interp", "lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Stack_i.lemma_compose_free_stack64",
"lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64",
"lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
"lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64",
"lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
"lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64",
"lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64",
"lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
"lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
"lemma_Vale.X64.Stack_i.lemma_store_new_valid64",
"lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64",
"lemma_Vale.X64.Xmms.lemma_equal_intro",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Prims.eq2",
"typing_Vale.X64.Decls.validSrcAddrs64",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.modifies",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp",
"typing_Vale.X64.Stack_i.valid_src_stack64",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__stack",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms",
"typing_tok_Vale.Interop.Types.TUInt64@tok",
"typing_tok_Vale.X64.Machine_s.Public@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"5f6f3c14dce24dbbe2f4863969506248"
],
[
"Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_stdcall",
1,
1,
0,
[ "@query" ],
0,
"6b20e51c6c477fccb921a9b81c64dfdb"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpMonotone_fast_sqr_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_stdcall",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.Decls.va_upd_stack",
"typing_Vale.X64.Decls.va_upd_stackTaint", "unit_typing"
],
0,
"7ba869ee3dc255091ee08af57a4aa949"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_stdcall",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"fuel_guarded_inversion_Vale.X64.State.state",
"interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
"interpretation_Tm_abs_ae6250f4283913a9dc13608eff7f3dd7",
"interpretation_Tm_abs_b6ab4bccb25ffc708f834aa8d487e389",
"interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
"proj_equation_Vale.X64.State.Mkstate_mem", "unit_typing"
],
0,
"035e232d6edb0067a93e534cdbf26fa9"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"18bade62709eb3f9de493808459f0390"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_fast_sqr_stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_stdcall",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_fast_sqr_stdcall",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_upd_stackTaint",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
"interpretation_Tm_abs_ae6250f4283913a9dc13608eff7f3dd7",
"interpretation_Tm_abs_b6ab4bccb25ffc708f834aa8d487e389",
"interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Xmms.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.State.Mkstate_flags",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"projection_inverse_Vale.X64.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Vale.Curve25519.X64.FastSqr.va_wpCompute_fast_sqr_stdcall",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.init_rsp",
"typing_Vale.X64.State.__proj__Mkstate__item__flags",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__stack",
"typing_Vale.X64.State.__proj__Mkstate__item__stackTaint",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms", "unit_typing"
],
0,
"5ff1426f53587317b02e60f0eed1f9df"
],
[
"Vale.Curve25519.X64.FastSqr.va_qcode_sqr2_stdcall",
1,
1,
0,
[ "@query" ],
0,
"4a79032b97fa4a4e2f42d661ec40d617"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_sqr2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.X64.Decls.validDstAddrs64",
"fuel_guarded_inversion_Vale.X64.State.state",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"refinement_interpretation_Tm_refine_99bfb9aee864b37f40df75b1f5890a4e"
],
0,
"f1047a56234d3da02d9486c1771d6518"
],
[
"Vale.Curve25519.X64.FastSqr.va_lemma_sqr2_stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.Interop.Types.TUInt64@tok",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Curve25519.Fast_defs.pow2_eight",
"equation_Vale.Curve25519.Fast_defs.pow2_five",
"equation_Vale.Curve25519.Fast_defs.pow2_four",
"equation_Vale.Curve25519.Fast_defs.pow2_seven",
"equation_Vale.Curve25519.Fast_defs.pow2_six",
"equation_Vale.Curve25519.Fast_defs.pow2_three",
"equation_Vale.Curve25519.Fast_defs.pow2_two",
"equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.modifies_buffer_specific",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.QuickCodes.range1",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_06895279704f00fdc02dbeaa6d281b82",
"interpretation_Tm_abs_2b7fd08e20cc3c4be5c6c50b1827e1b8",
"interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
"interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
"l_and-interp", "lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.modifies_buffer_addr",
"lemma_Vale.X64.Memory.modifies_buffer_readable",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
"lemma_Vale.X64.Memory.modifies_valid_taint64",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Stack_i.lemma_compose_free_stack64",
"lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64",
"lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
"lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64",
"lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
"lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64",
"lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64",
"lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
"lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
"lemma_Vale.X64.Stack_i.lemma_store_new_valid64",
"lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64",
"lemma_Vale.X64.Xmms.lemma_equal_intro",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Prims.eq2",
"typing_Vale.X64.Decls.validSrcAddrs64",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.modifies",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp",
"typing_Vale.X64.Stack_i.valid_src_stack64",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__stack",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms",
"typing_tok_Vale.Interop.Types.TUInt64@tok",
"typing_tok_Vale.X64.Machine_s.Public@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"5c5a9cf668c6998ddee620e9e79f71ce"
],
[
"Vale.Curve25519.X64.FastSqr.va_wp_sqr2_stdcall",
1,
1,
0,
[ "@query" ],
0,
"99c83c5c10944d4edd4ce9223b26cd06"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpMonotone_sqr2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_sqr2_stdcall",
"equation_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.Decls.va_upd_stack",
"typing_Vale.X64.Decls.va_upd_stackTaint", "unit_typing"
],
0,
"31b6d4a7f0d52c4c714b5defb95a4638"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpCompute_sqr2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_sqr2_stdcall",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"fuel_guarded_inversion_Vale.X64.State.state",
"interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
"interpretation_Tm_abs_ae6250f4283913a9dc13608eff7f3dd7",
"interpretation_Tm_abs_b6ab4bccb25ffc708f834aa8d487e389",
"interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
"proj_equation_Vale.X64.State.Mkstate_mem", "unit_typing"
],
0,
"8537462728cb3835565c8b8bb4e45362"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_sqr2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"08add5b2dd3e22f4d597ce32acdfc559"
],
[
"Vale.Curve25519.X64.FastSqr.va_wpProof_sqr2_stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.Curve25519.X64.FastSqr.va_wpCompute_sqr2_stdcall",
"equation_Vale.Curve25519.X64.FastSqr.va_wp_sqr2_stdcall",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_upd_stackTaint",
"equation_Vale.X64.Decls.validDstAddrs64",
"equation_Vale.X64.Decls.validSrcAddrs64",
"equation_Vale.X64.Machine_s.reg",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
"interpretation_Tm_abs_ae6250f4283913a9dc13608eff7f3dd7",
"interpretation_Tm_abs_b6ab4bccb25ffc708f834aa8d487e389",
"interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Xmms.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkstate_flags",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_regs",
"proj_equation_Vale.X64.State.Mkstate_stack",
"proj_equation_Vale.X64.State.Mkstate_stackTaint",
"proj_equation_Vale.X64.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.State.Mkstate_flags",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"projection_inverse_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_Vale.X64.State.Mkstate_ok",
"projection_inverse_Vale.X64.State.Mkstate_regs",
"projection_inverse_Vale.X64.State.Mkstate_stack",
"projection_inverse_Vale.X64.State.Mkstate_stackTaint",
"projection_inverse_Vale.X64.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Vale.Curve25519.X64.FastSqr.va_wpCompute_sqr2_stdcall",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.init_rsp",
"typing_Vale.X64.State.__proj__Mkstate__item__flags",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_Vale.X64.State.__proj__Mkstate__item__ok",
"typing_Vale.X64.State.__proj__Mkstate__item__regs",
"typing_Vale.X64.State.__proj__Mkstate__item__stack",
"typing_Vale.X64.State.__proj__Mkstate__item__stackTaint",
"typing_Vale.X64.State.__proj__Mkstate__item__xmms", "unit_typing"
],
0,
"fc76eaa8d2c23a87c43b2edee6ef586d"
]
]
]
Computing file changes ...
