[ "P3fXD($$}", [ [ "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, "ae7567f82c176ea61bd8bc78ca4f2bae" ], [ "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, "3807117add7c00278a86cf1e1eae69b4" ], [ "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, "de1896df1631f6b70fd757aef56220f0" ], [ "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, "dd5e5a2219932abfeca9093e9b8cf79c" ], [ "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, "ee3afbaaaaae5bcf14359ee3e2a4a384" ], [ "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, "60eb087f1c64591aad08ad17c268c3dc" ], [ "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, "f686493a64fcb9a8a008e05515113564" ], [ "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, "8eadf408c1e561d3d37b0f428b72d10e" ], [ "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, "c2b17e92bd239a5dfdb5d1f815fc8da5" ], [ "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, "8ca565c72339fb9c9396fbb314ff6480" ], [ "EverCrypt.AutoConfig2.cpu_has_avx512", 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, "6e617ddd1665ddf52528bf11d488eb99" ], [ "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, "4f252b27986e8373f7daae100bf2966f" ], [ "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, "98c2ad72ec53ef438cafeb4f0c5d8670" ], [ "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, "381a7a65c09dd698ed60dc9cfc550174" ], [ "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, "801553559331bf17bc5a4855e5efe5c0" ], [ "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, "2081dcd7e69ade4a63a96a2b983eedfa" ], [ "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, "f409b23b2ec036621bde2c4a204833cc" ], [ "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, "500c51a50b314698df1205fcff3ac3a7" ], [ "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, "25bf2a81a1b0bb142e579f958fccfb45" ], [ "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, "b9d2f6bcbedaf1a844f1fceaffabf52b" ], [ "EverCrypt.AutoConfig2.recall", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "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_365abba901205a01d0ef28ebf2198c47", "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_avx512", "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.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "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.avx512_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, "47b6725e7a09b58ef831f57f3173b4a5" ], [ "EverCrypt.AutoConfig2.init_aesni_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_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", "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_avx512", "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.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_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.avx512_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, "5df87fd935fc3b72ca90a6fd6f06e3ac" ], [ "EverCrypt.AutoConfig2.init_shaext_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_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", "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_avx512", "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.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_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.avx512_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, "98e25c837f5763b93678ec04aeb25bbe" ], [ "EverCrypt.AutoConfig2.init_avx_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.UInt64_pretyping_0a6d0526dc068d94bc7967094b2dd513", "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_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_Vale.X64.CPU_Features_s.avx_enabled", "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.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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_AmpAmp", "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_2edd0a28a9cbd8f0909e1c087d9eaad3", "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_avx512", "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.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_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.avx512_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_inversion", "unit_typing" ], 0, "924d3429b98ef21df11cb3fa7b3ba29d" ], [ "EverCrypt.AutoConfig2.init_avx2_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.UInt64_pretyping_0a6d0526dc068d94bc7967094b2dd513", "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_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_Vale.X64.CPU_Features_s.avx2_enabled", "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.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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_AmpAmp", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_2edd0a28a9cbd8f0909e1c087d9eaad3", "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_avx512", "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.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_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.avx512_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_inversion", "unit_typing" ], 0, "870c972af10896da351fad49a1ab3301" ], [ "EverCrypt.AutoConfig2.init_adx_bmi2_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_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", "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_avx512", "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.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_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.avx512_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, "43b152d1dcdb1965e9ab94b66dc3b82b" ], [ "EverCrypt.AutoConfig2.init_sse_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_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_Vale.X64.CPU_Features_s.sse_enabled", "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_avx512", "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.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_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.avx512_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, "dcb8fd6ae4873c3ff0ee4b2830eb792b" ], [ "EverCrypt.AutoConfig2.init_movbe_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_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", "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_avx512", "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.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_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.avx512_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, "1676287e7f7ef264393fd344f4ca46c0" ], [ "EverCrypt.AutoConfig2.init_rdrand_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_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", "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_avx512", "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.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_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.avx512_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, "348aaff5f930fcb4915fb8ea98f5508c" ], [ "EverCrypt.AutoConfig2.init_avx512_flags", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.UInt64_pretyping_0a6d0526dc068d94bc7967094b2dd513", "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_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_Vale.X64.CPU_Features_s.avx512_enabled", "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.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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_AmpAmp", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_2912959f6e3d6a9f53a306876942cbd2", "refinement_interpretation_Tm_refine_2edd0a28a9cbd8f0909e1c087d9eaad3", "refinement_interpretation_Tm_refine_393f16037203a2d33a5ae6636b5c33ff", "refinement_interpretation_Tm_refine_6407aad17b99a5b8faed66d3c48f39db", "refinement_interpretation_Tm_refine_a27bd5e815ae88d8d53a3fa90623c819", "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_avx512", "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.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_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.avx512_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_inversion", "unit_typing" ], 0, "7f884a347fd00eefe31f6525b12c4b62" ], [ "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, "0aed675e7c3b5634b71b1cc964af4012" ], [ "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, "df9a546dd1a1e5282637ebb3a1b2d48e" ], [ "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, "dcd72ea8daeddd2532303ee04b7f758b" ], [ "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_avx512", "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.avx512_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, "5f4d3e37621a11ee46be43b0d85a15a0" ], [ "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_avx512", "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.avx512_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, "41e5f5dfbcd603578b61663432031fc7" ], [ "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_avx512", "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.avx512_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, "1cae3b216f2b273f8d80b97bca3e3e81" ], [ "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_avx512", "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.avx512_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, "74f8276d392da9190e0b1ed9046e2207" ], [ "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_avx512", "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.avx512_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, "f7851b7913b08fa65b6f0048e2cb46b3" ], [ "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_avx512", "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.avx512_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, "38f5a58a964b694278bfe1a21cd3e87b" ], [ "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_avx512", "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.avx512_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, "2c4bde9d60559e3fe432667f673182e8" ], [ "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_avx512", "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.avx512_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, "152eef66df88ec70403f6c67bb71f4a2" ], [ "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_avx512", "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.avx512_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, "527a0b54914b29af852ea82ed4551310" ], [ "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_avx512", "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.avx512_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, "78e9a570ed26a8d4903f4670945af45d" ], [ "EverCrypt.AutoConfig2.disable_avx512", 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_86edbfa443321374e43cf40521c958d1", "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_avx512", "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.avx512_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, "8fc54159ee90f68465c86e8555013c6f" ], [ "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, "57b09fb794bbd6712dda435504c01c5f" ], [ "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, "7c57995436be88c8d9ef9203bba07197" ], [ "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, "474a4b26e60b8bc3d597827ef08f9f2e" ], [ "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, "267f8c64e8c3ab73644d11d3c06b038f" ], [ "EverCrypt.AutoConfig2.has_vec128", 1, 0, 0, [ "@query", "bool_typing", "equation_EverCrypt.AutoConfig2.vec128_enabled", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, "77821297a8890c5ea9cdefc5e2ea17e6" ], [ "EverCrypt.AutoConfig2.has_vec256", 1, 0, 0, [ "@query", "bool_typing", "equation_EverCrypt.AutoConfig2.vec256_enabled", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, "f8ad6c574930f4e5256b0125f2d55e4e" ] ] ]