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
EverCrypt.AutoConfig2.fst.hints
[
"Ó���\u0014)/�cǹ;��x",
[
[
"EverCrypt.AutoConfig2.cpu_has_shaext",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"51639b10203281cd6d65e36540dbaeeb"
],
[
"EverCrypt.AutoConfig2.cpu_has_aesni",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"91eba0621bf7cd6d2d2d49b9fa8cb939"
],
[
"EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"be413652b12cd14df36ce83e8ee4152f"
],
[
"EverCrypt.AutoConfig2.cpu_has_avx2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"8bd9aa7c9f1642a967c162d90d749213"
],
[
"EverCrypt.AutoConfig2.cpu_has_avx",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"aa5832fb2fe2ff236513c2f48374d6f7"
],
[
"EverCrypt.AutoConfig2.cpu_has_bmi2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"f480a10a7ba9a428f541fa4ab88ecb83"
],
[
"EverCrypt.AutoConfig2.cpu_has_adx",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"dc3a8c45a5b4b621f894fe1084c0fd69"
],
[
"EverCrypt.AutoConfig2.cpu_has_sse",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"835861837d7acc34657309d763bb336b"
],
[
"EverCrypt.AutoConfig2.cpu_has_movbe",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"19be7bf5876a3247aebb24f818bcb0bc"
],
[
"EverCrypt.AutoConfig2.cpu_has_rdrand",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"0dc9d2d4847e999983b95880e17bdd6d"
],
[
"EverCrypt.AutoConfig2.user_wants_hacl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"706482fc1f42cc49d37e2902380dd819"
],
[
"EverCrypt.AutoConfig2.user_wants_vale",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"d7267ddc8ce10dfb23db8575f66b0da8"
],
[
"EverCrypt.AutoConfig2.user_wants_openssl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"166aa045e0daf55f6e848cd4c7c5a565"
],
[
"EverCrypt.AutoConfig2.user_wants_bcrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"036116e66990067740b64a878b5b3696"
],
[
"EverCrypt.AutoConfig2.mk_getter",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_e9473220cd6ad720675cd06c0342affa",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"f7ef64cabe755461a1fe790e947ca83f"
],
[
"EverCrypt.AutoConfig2.wants_vale",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"13145a0f2bf68d66fdbb51d3674d0cf8"
],
[
"EverCrypt.AutoConfig2.wants_hacl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"f1479d6ab29da42dc88ffd9660bcd950"
],
[
"EverCrypt.AutoConfig2.wants_openssl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"dd9715d1f731e3ecf11ff9b3b3856e7f"
],
[
"EverCrypt.AutoConfig2.wants_bcrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"0b603b2f017fef6e5e6feeab278ae24e"
],
[
"EverCrypt.AutoConfig2.recall",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.bool",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"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_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"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",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"d018f0128ec525f3362647d31508c926"
],
[
"EverCrypt.AutoConfig2.init_aesni_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_213f39268db64150129a6df434827301",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"refinement_interpretation_Tm_refine_bfa2850a9e960bfa4a9b85ee1d4e07b0",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"ae07a4e5ec90f53f326ba0cc71d18e1a"
],
[
"EverCrypt.AutoConfig2.init_shaext_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"refinement_interpretation_Tm_refine_bfb9ab9112b4d74b258eff85502487aa",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"37299f2a2dda01d5c53f07b3295e68b4"
],
[
"EverCrypt.AutoConfig2.init_avx_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05beeeeb87931157677c80f85d54426d",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"fd3562c514134811facc8ae80fa8c295"
],
[
"EverCrypt.AutoConfig2.init_avx2_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"refinement_interpretation_Tm_refine_c83fd8958dff73b478a7102c1efc35db",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"ef6b4b1493d7b2e442fcea8fd60b9280"
],
[
"EverCrypt.AutoConfig2.init_adx_bmi2_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_219f8259731e5732c1e67f082c26eb8a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"refinement_interpretation_Tm_refine_9ab7fa522e38ab99a9c38c8f56955bee",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"2331f90669550c93c886f7b2b3c43200"
],
[
"EverCrypt.AutoConfig2.init_sse_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"refinement_interpretation_Tm_refine_ac551b6080b261220ee2b3ee90b64fca",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"e43238c53288d2d0350ab52d64c20745"
],
[
"EverCrypt.AutoConfig2.init_movbe_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"refinement_interpretation_Tm_refine_781e13bcd28356829ee721bda8605e6c",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"198b94feb9654764477609a7cb5ce1fa"
],
[
"EverCrypt.AutoConfig2.init_rdrand_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.UInt64.t__uu___haseq", "bool_inversion",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt64.uv_inv",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_3826c403dc7f5b06288893abc51a4648",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"f7adbe6efe9d78f41da0957cc1f0406c"
],
[
"EverCrypt.AutoConfig2.init_cpu_flags",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "unit_inversion",
"unit_typing"
],
0,
"949f6367e4ea46c6d7025f126d309458"
],
[
"EverCrypt.AutoConfig2.init",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0974bbc864bc148f144900ca94ac650b",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_547abb34f36bdc40a05a795dcff91e87",
"refinement_interpretation_Tm_refine_abe354c7478b02a2ad93777397b2eae9",
"true_interp", "typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled", "unit_typing"
],
0,
"e25e09a22b9ab1b862fabd058f5d9d7a"
],
[
"EverCrypt.AutoConfig2.mk_disabler",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.fp",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_9a5ec6bfbd2c8534ddcf95ec1b2fdf64",
"refinement_interpretation_Tm_refine_e0b7f4a9559ea987083b008250208d30",
"true_interp", "typing_EverCrypt.AutoConfig2.fp",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Vale.X64.CPU_Features_s.adx_enabled", "unit_typing"
],
0,
"d540eaee89cd99b6e672967c6dabffb6"
],
[
"EverCrypt.AutoConfig2.disable_avx2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ad69217d90e09dc5987a5bf2acb094cf",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"026fea7b64532b2f8270691b158654b6"
],
[
"EverCrypt.AutoConfig2.disable_avx",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_6d9f0f03a6b4d954bccf2185b86c7bdf",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"52d22428e00afac86c884d7a3c60fba7"
],
[
"EverCrypt.AutoConfig2.disable_bmi2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_8e4a37b6a33c8b697be90244c6fd3a68",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"ecca54eb17b3ee2e5ee1994972b0bff0"
],
[
"EverCrypt.AutoConfig2.disable_adx",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_37360d7643fb6a4ce55230101325c487",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"d80e2006d01f4d2ee6d230f4976cdb87"
],
[
"EverCrypt.AutoConfig2.disable_shaext",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_26c8cb8f5d31030d348bf64cae0c44ef",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"d61daed511d3fcb7d0d1910777486087"
],
[
"EverCrypt.AutoConfig2.disable_aesni",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_9d57a8037055a7764eff231b50e68463",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"4a40708dcf7daddfd54b7b7cbeb272ff"
],
[
"EverCrypt.AutoConfig2.disable_pclmulqdq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_d70748f3e5abaca906d2a1a1b7bbc435",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"71df7154e5b19a0bf0f7772d7cfcdd46"
],
[
"EverCrypt.AutoConfig2.disable_sse",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_caf7d9f2c237816f7bdac49f91fb83f3",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"9c9c1b51cae38d88de4d309a5b7aae9d"
],
[
"EverCrypt.AutoConfig2.disable_movbe",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1871cc368c50378a70a2e942b7aba3f6",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"3edd419327d3605c22653dfc7bbe1bcb"
],
[
"EverCrypt.AutoConfig2.disable_rdrand",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.flag",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.bool",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_3a2b2d5fe47cbf4ba2bf06d6d5b1e7a2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"true_interp", "typing_EverCrypt.AutoConfig2.cpu_has_adx",
"typing_EverCrypt.AutoConfig2.cpu_has_aesni",
"typing_EverCrypt.AutoConfig2.cpu_has_avx",
"typing_EverCrypt.AutoConfig2.cpu_has_avx2",
"typing_EverCrypt.AutoConfig2.cpu_has_bmi2",
"typing_EverCrypt.AutoConfig2.cpu_has_movbe",
"typing_EverCrypt.AutoConfig2.cpu_has_pclmulqdq",
"typing_EverCrypt.AutoConfig2.cpu_has_rdrand",
"typing_EverCrypt.AutoConfig2.cpu_has_shaext",
"typing_EverCrypt.AutoConfig2.cpu_has_sse",
"typing_EverCrypt.AutoConfig2.flag",
"typing_EverCrypt.AutoConfig2.fp",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx2_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.bmi2_enabled",
"typing_Vale.X64.CPU_Features_s.movbe_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_Vale.X64.CPU_Features_s.rdrand_enabled",
"typing_Vale.X64.CPU_Features_s.sha_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled", "unit_typing"
],
0,
"72a09e4206a869716e0ab0ace4f698c5"
],
[
"EverCrypt.AutoConfig2.disable_vale",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.fp",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_Prims.bool",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union", "unit_typing"
],
0,
"2cccfe5f6934b8230dc0cefd7d8e975e"
],
[
"EverCrypt.AutoConfig2.disable_hacl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.fp",
"equation_EverCrypt.AutoConfig2.fp_cpu_flags",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_Prims.bool",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union", "unit_typing"
],
0,
"4bba11e40af0f6a6845234c4e4b4b205"
],
[
"EverCrypt.AutoConfig2.disable_openssl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.fp",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_Prims.bool",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union", "unit_typing"
],
0,
"a04dc1bd01cf97932338d53004b60b97"
],
[
"EverCrypt.AutoConfig2.disable_bcrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_EverCrypt.AutoConfig2.eternal_pointer",
"equation_EverCrypt.AutoConfig2.fp",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"function_token_typing_Prims.bool",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_EverCrypt.AutoConfig2.fp_cpu_flags",
"typing_EverCrypt.AutoConfig2.user_wants_bcrypt",
"typing_EverCrypt.AutoConfig2.user_wants_hacl",
"typing_EverCrypt.AutoConfig2.user_wants_openssl",
"typing_EverCrypt.AutoConfig2.user_wants_vale",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union", "unit_typing"
],
0,
"1d8ed15d26790191d535f5b596acfa4a"
]
]
]
Computing file changes ...
