Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Hacl.Impl.Matrix.fst.hints
[
"2\u001e�z�\u007f���\u0000_�S���",
[
[
"Hacl.Impl.Matrix.matrix_t",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"afbea2dd93ea8f8cb7d9c6328beec509"
],
[
"Hacl.Impl.Matrix.as_matrix",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Hacl.Impl.Matrix.elem", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_lemma",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"fdc4441470470406052f2f903e965f1f"
],
[
"Hacl.Impl.Matrix.matrix_create",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_Lib.IntTypes.uint16",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_a3553290b796580f552fc9b8c41cb4f4",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c5d9965835e1f1fcac9db74a201e2b47"
],
[
"Hacl.Impl.Matrix.matrix_create",
2,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Hacl.Impl.Matrix.elem", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Matrix.create", "int_typing",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55f253d1879ae6aeb32422d301232d0f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a3553290b796580f552fc9b8c41cb4f4",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.mul", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8bef4bde265d181efb9bbef17362e7be"
],
[
"Hacl.Impl.Matrix.mget",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"39697f9bbbc0faccc5aa4b40e67a3b29"
],
[
"Hacl.Impl.Matrix.mget",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_Hacl.Impl.Matrix.elem", "equation_Lib.Buffer.modifies",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.Matrix.mget",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.mul_mod_lemma",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_6b5c942e218e786e5085ddaac3ea3ac9",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.IntTypes.v",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"277cb3d9c10ca10949e692f2a6439607"
],
[
"Hacl.Impl.Matrix.mset",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8d534637b06b81f5034f68c9098e2386"
],
[
"Hacl.Impl.Matrix.mset",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"equation_Spec.Matrix.mset",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.mul_mod_lemma",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.IntTypes.op_At_Percent_Dot",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5d9bef34ac92b1d2db3c42532a16ad83"
],
[
"Hacl.Impl.Matrix.op_String_Access",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_cea1f722a74b74ac9e0cdad8a776cad7",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"32546a5cef8f61ff8c6455407db974b7"
],
[
"Hacl.Impl.Matrix.op_String_Access",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_cea1f722a74b74ac9e0cdad8a776cad7"
],
0,
"ec0b6bc3711078ba516bfabc41b7ec2b"
],
[
"Hacl.Impl.Matrix.op_String_Assignment",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_cea1f722a74b74ac9e0cdad8a776cad7",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"72270615ce556a88e89341a30f5750c3"
],
[
"Hacl.Impl.Matrix.op_String_Assignment",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_cea1f722a74b74ac9e0cdad8a776cad7"
],
0,
"d2e67fbda56f1248d5a91af59ea06c3b"
],
[
"Hacl.Impl.Matrix.get",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"34f960fcbf9301562f98c14f99c88571"
],
[
"Hacl.Impl.Matrix.map2_inner_inv",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "int_inversion",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_45d6f9bffbf261550136aadfcda78f48",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"49d30ab86c1429f449ef84564ed9ba82"
],
[
"Hacl.Impl.Matrix.map2_inner",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ba985bb53b81bda71184c45ee764c314"
],
[
"Hacl.Impl.Matrix.map2_inner",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.max_int",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Matrix.matrix",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_0bb4f73b8eb61a6bef0ae4329b9380ed",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_278fde365961b864c121c18951175e9f",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_818b08e49238083809d72cd1e3babbc1",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_939c7661dedde3862fe03d67ae27585f",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_ab3f63bfb9cb66bbfd147f6a46f59694",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_cea1f722a74b74ac9e0cdad8a776cad7",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Matrix.mset", "typing_tok_Lib.Buffer.MUT@tok",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"704efbcb47e0fef0d65808e22ade2914"
],
[
"Hacl.Impl.Matrix.map2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"62d269ab2d930ea3d83dc6c7905cb069"
],
[
"Hacl.Impl.Matrix.map2",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0581b08fc69f9bad1f5e0160becc0e60",
"refinement_interpretation_Tm_refine_0bb4f73b8eb61a6bef0ae4329b9380ed",
"refinement_interpretation_Tm_refine_15a5117ea4b29076ac44b474b9a72353",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_2a76de48fa0488ebf0b17074daf5abfc",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_45d6f9bffbf261550136aadfcda78f48",
"refinement_interpretation_Tm_refine_4b1aa00f0df1af9127792fc1c2e40e3a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_818b08e49238083809d72cd1e3babbc1",
"refinement_interpretation_Tm_refine_82be21fd0959ee321cf731cf9de81f1e",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_98c41d637545f36558345bfefe13fcfa",
"refinement_interpretation_Tm_refine_991637d5ec1c6b885b7019721f133689",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_ab3f63bfb9cb66bbfd147f6a46f59694",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_ebbe193f883042ea7f7473dc3fc44d99",
"refinement_interpretation_Tm_refine_f7bc93f824be57965cb8bedf19301fc2",
"refinement_interpretation_Tm_refine_f86a8a01cd81053a20e44315619d09d2",
"typing_Lib.Buffer.loc", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5b0bd87b56f66de522abb802c6d57d61"
],
[
"Hacl.Impl.Matrix.matrix_add",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"67f9258947f88bb3097e4caf85f09655"
],
[
"Hacl.Impl.Matrix.matrix_add",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.live", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_Spec.Matrix.add",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_17dc9b6cd9ab4fdccc47d80c28e4f79f",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c08f0c98d577777754704759e17cfd38",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.Buffer.loc",
"typing_LowStar.Buffer.trivial_preorder",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"fec11ca68c244850d391bb6d354b452d"
],
[
"Hacl.Impl.Matrix.matrix_sub",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"9869765288703819f02623deafcb3071"
],
[
"Hacl.Impl.Matrix.matrix_sub",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"equation_Spec.Matrix.matrix",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"interpretation_Tm_abs_d8a319dfe7981b188e6b274de421250a",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"primitive_Prims.op_Multiply",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_17dc9b6cd9ab4fdccc47d80c28e4f79f",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6670a1a291aa5d4bf3d6239925bbde6e",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_98c41d637545f36558345bfefe13fcfa",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_b0faad0d459bb289468c283eb08b0841",
"refinement_interpretation_Tm_refine_b211dfa1092a080eb7d14a14c06f61bc",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_d80e5c6aacfc563910dec0b68a0d7f34",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq", "typing_Spec.Matrix.map2",
"typing_Spec.Matrix.sub", "typing_tok_Lib.Buffer.MUT@tok",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"432e686cd7459748b3090ffbdf092823"
],
[
"Hacl.Impl.Matrix.mul_inner",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"6cf8a28dd5a04fd547392fe5e845f3d9"
],
[
"Hacl.Impl.Matrix.mul_inner",
2,
1,
0,
[ "@query" ],
0,
"744a916af16f9551bfb05679abeaf10f"
],
[
"Hacl.Impl.Matrix.mul_inner",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Spec.Matrix.sum_.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Spec.Matrix.sum_.fuel_instrumented", "@query",
"Hacl.Impl.Matrix_interpretation_Tm_ghost_arrow_7405c28e056138cef242c9499959fa67",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Matrix_interpretation_Tm_ghost_arrow_72bbfb83a25d926183af1873807265fe",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion",
"bool_typing", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Matrix.sum",
"equation_with_fuel_Spec.Matrix.sum_.fuel_instrumented",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_d6ffe54d8b82877ad874a42d387ce9c9",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_Lib.Buffer.bget_as_seq",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03ed9debde05391d4ee5ae09e9690145",
"refinement_interpretation_Tm_refine_0581b08fc69f9bad1f5e0160becc0e60",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a17ca0fec24af3ab020dad6cf70b4d1",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_873133828c907cbc2718aea6e8b831ae",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"refinement_interpretation_Tm_refine_98c41d637545f36558345bfefe13fcfa",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_a5c1b398f96e3506835dfbe23f668463",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_b139eaa50e9b12b31a2f0a63633415e0",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_dd541438174411489d6a947719e9d4aa",
"refinement_interpretation_Tm_refine_f2dd858e1cb44a644dcdba98eef03629",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.sel",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.includes",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_Lib.Buffer.as_seq",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.create", "typing_Lib.Sequence.upd",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"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_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"2ce7e712829d146d43efb903d8add27a"
],
[
"Hacl.Impl.Matrix.mul_inner_inv",
1,
0,
0,
[ "@query" ],
0,
"1cb9b722519061523e0b10cb4a50c9f4"
],
[
"Hacl.Impl.Matrix.mul_inner_inv",
2,
0,
0,
[ "@query" ],
0,
"254f146789288aef893664876b07f053"
],
[
"Hacl.Impl.Matrix.mul_inner_inv",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "int_inversion",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_45d6f9bffbf261550136aadfcda78f48",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"57efecdb88929921cd291bd28f1125bc"
],
[
"Hacl.Impl.Matrix.mul_inner1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c7dbbdcad18b15f4c3ddbcedcb261c25"
],
[
"Hacl.Impl.Matrix.mul_inner1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"3805d6876cfc29cb9d31ee80a269ac0a"
],
[
"Hacl.Impl.Matrix.mul_inner1",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Matrix.matrix",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0bb4f73b8eb61a6bef0ae4329b9380ed",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a17ca0fec24af3ab020dad6cf70b4d1",
"refinement_interpretation_Tm_refine_64ba117b106e987b0cd7d47599577776",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_73b859b35ca72959f42843b1165c2a3b",
"refinement_interpretation_Tm_refine_818b08e49238083809d72cd1e3babbc1",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_ab3f63bfb9cb66bbfd147f6a46f59694",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_dd541438174411489d6a947719e9d4aa",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"refinement_interpretation_Tm_refine_ffaac14d036149b5937f31432dea3c4b",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.IntTypes.mul",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Matrix.mset", "typing_tok_Lib.Buffer.MUT@tok",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"da8452e2e51b23ae8838e2f25f173d78"
],
[
"Hacl.Impl.Matrix.onemore",
1,
0,
0,
[ "@query" ],
0,
"5c31535fa9c7a5f5c782bf4556d9767f"
],
[
"Hacl.Impl.Matrix.onemore",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de2301407e875fa1a0195c33ec86df1f",
"refinement_interpretation_Tm_refine_e76bd1e3fcd1369d7232ec3854a8c984",
"refinement_interpretation_Tm_refine_ea61d79c0e2a0b954eaf9792648f1d17"
],
0,
"e4b7efdd5ef35b699d71a5f50856022b"
],
[
"Hacl.Impl.Matrix.onemore1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"09dc36217ee75150dfc781429a21a68c"
],
[
"Hacl.Impl.Matrix.onemore1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"e65d85424527f108320326d00dbdfc97"
],
[
"Hacl.Impl.Matrix.matrix_mul",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"9792c1ff7d70a6ba757a89594c90fdc5"
],
[
"Hacl.Impl.Matrix.matrix_mul",
2,
0,
0,
[ "@query" ],
0,
"a1c17f28bbd3ec1a2c630e07330c8e65"
],
[
"Hacl.Impl.Matrix.matrix_mul",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_054a6b66a100a59cad57dae5dfa08525",
"refinement_interpretation_Tm_refine_0581b08fc69f9bad1f5e0160becc0e60",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0bb4f73b8eb61a6bef0ae4329b9380ed",
"refinement_interpretation_Tm_refine_15a5117ea4b29076ac44b474b9a72353",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_2a76de48fa0488ebf0b17074daf5abfc",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_389557fb943f90daaa58d7d5c72205e0",
"refinement_interpretation_Tm_refine_45d6f9bffbf261550136aadfcda78f48",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_818b08e49238083809d72cd1e3babbc1",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8cb896bd120ccc55e1c13470bca7d8e0",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"refinement_interpretation_Tm_refine_98c41d637545f36558345bfefe13fcfa",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_ab3f63bfb9cb66bbfd147f6a46f59694",
"refinement_interpretation_Tm_refine_bba83bee4c916f3a031ef071d7d6ef01",
"refinement_interpretation_Tm_refine_be69fb695df20be267f4e7ab4e88af5b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f86a8a01cd81053a20e44315619d09d2",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"203c6a120df53ab17e424e5b22b8cf9d"
],
[
"Hacl.Impl.Matrix.mget_s",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c1c449506fba4f5a5e8c655e9656c98b"
],
[
"Hacl.Impl.Matrix.mget_s",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_Hacl.Impl.Matrix.elem", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies0", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.Matrix.mget_s",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.mul_mod_lemma",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_6b5c942e218e786e5085ddaac3ea3ac9",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.v",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ce7f3aae2243617fecb5735e25fe9741"
],
[
"Hacl.Impl.Matrix.get_s",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d4b21320734823ca01c41387f51e0fa4"
],
[
"Hacl.Impl.Matrix.mul_inner_s",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c6db071be4d2313432177e5016d8c049"
],
[
"Hacl.Impl.Matrix.mul_inner_s",
2,
1,
0,
[ "@query" ],
0,
"956a55557eb22f28fd549eb82aaea7ce"
],
[
"Hacl.Impl.Matrix.mul_inner_s",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Spec.Matrix.sum_.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Spec.Matrix.sum_.fuel_instrumented", "@query",
"Hacl.Impl.Matrix_interpretation_Tm_ghost_arrow_7405c28e056138cef242c9499959fa67",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Matrix_interpretation_Tm_ghost_arrow_72bbfb83a25d926183af1873807265fe",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion",
"bool_typing", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies0", "equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Matrix.sum",
"equation_with_fuel_Spec.Matrix.sum_.fuel_instrumented",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_e10103833e75f16a7337d053f95bddc0",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_Lib.Buffer.bget_as_seq",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0581b08fc69f9bad1f5e0160becc0e60",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a17ca0fec24af3ab020dad6cf70b4d1",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_71d2c54a27ef3b569e42fe6c08a889bf",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_873133828c907cbc2718aea6e8b831ae",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"refinement_interpretation_Tm_refine_98c41d637545f36558345bfefe13fcfa",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_a5c1b398f96e3506835dfbe23f668463",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_afbe08626a9da1d14c04fd477e28f889",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_eac5ad5e3303b5ba158d6d11c7e5a58b",
"refinement_interpretation_Tm_refine_f2dd858e1cb44a644dcdba98eef03629",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.sel",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.includes",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_Lib.Buffer.as_seq",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.create", "typing_Lib.Sequence.upd",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"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_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d6aee8bb769a7cc7e600ef2874556a80"
],
[
"Hacl.Impl.Matrix.mul_inner1_s",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"610173fc23fb074b587f1b5fea716140"
],
[
"Hacl.Impl.Matrix.mul_inner1_s",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"cb4b1cd3a5c578269385aae0a9ef94c6"
],
[
"Hacl.Impl.Matrix.mul_inner1_s",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies0",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Matrix.matrix",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0bb4f73b8eb61a6bef0ae4329b9380ed",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a17ca0fec24af3ab020dad6cf70b4d1",
"refinement_interpretation_Tm_refine_64ba117b106e987b0cd7d47599577776",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_73b859b35ca72959f42843b1165c2a3b",
"refinement_interpretation_Tm_refine_818b08e49238083809d72cd1e3babbc1",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_ab3f63bfb9cb66bbfd147f6a46f59694",
"refinement_interpretation_Tm_refine_afbe08626a9da1d14c04fd477e28f889",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"refinement_interpretation_Tm_refine_ffaac14d036149b5937f31432dea3c4b",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.IntTypes.mul",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Matrix.mset", "typing_tok_Lib.Buffer.MUT@tok",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"76466f5c8e90279376dccac66a2104d7"
],
[
"Hacl.Impl.Matrix.matrix_mul_s",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"415d2f80fb343d3002b3b79a9a005fa9"
],
[
"Hacl.Impl.Matrix.matrix_mul_s",
2,
0,
0,
[ "@query" ],
0,
"a14ec1543002338d2041faa932e548b3"
],
[
"Hacl.Impl.Matrix.matrix_mul_s",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16", "int_inversion",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0581b08fc69f9bad1f5e0160becc0e60",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0bb4f73b8eb61a6bef0ae4329b9380ed",
"refinement_interpretation_Tm_refine_15a5117ea4b29076ac44b474b9a72353",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_2a76de48fa0488ebf0b17074daf5abfc",
"refinement_interpretation_Tm_refine_34f93eba3f8ecef42036e4195ff2e556",
"refinement_interpretation_Tm_refine_389557fb943f90daaa58d7d5c72205e0",
"refinement_interpretation_Tm_refine_45d6f9bffbf261550136aadfcda78f48",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6b5d55d11ed1acb024feef2677a96851",
"refinement_interpretation_Tm_refine_8133d72096da1a54c6a90730a5304b71",
"refinement_interpretation_Tm_refine_818b08e49238083809d72cd1e3babbc1",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8cb896bd120ccc55e1c13470bca7d8e0",
"refinement_interpretation_Tm_refine_9231e7cec6d1e7c7590981bdd98c0893",
"refinement_interpretation_Tm_refine_98c41d637545f36558345bfefe13fcfa",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9e1d38115796ca45d4036c50bc0fb818",
"refinement_interpretation_Tm_refine_ab3f63bfb9cb66bbfd147f6a46f59694",
"refinement_interpretation_Tm_refine_adfc0890dd47f69636b183269dad9fba",
"refinement_interpretation_Tm_refine_bba83bee4c916f3a031ef071d7d6ef01",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f86a8a01cd81053a20e44315619d09d2",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d0fe3f694de96e86c3dd669b5ebe22fc"
],
[
"Hacl.Impl.Matrix.eq_u32_m",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"refinement_interpretation_Tm_refine_07aead5b1239d489c2a97b2236b5f3e4"
],
0,
"59a9cdee1e8c6597ee7df797a25c01c8"
],
[
"Hacl.Impl.Matrix.eq_u32_m",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.eq",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.eq",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Matrix.eq_m", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Equality",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_07aead5b1239d489c2a97b2236b5f3e4",
"refinement_interpretation_Tm_refine_0c1a7fcd8c5d6302f88f430256334c0e",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
"refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9f8f6290ae5c5057ec2ec3d3fc190a93",
"refinement_interpretation_Tm_refine_c612f4a2249856ccea8dcf33d3e828b0",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.uint_to_nat",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"cae66a0b67ba9f57e0b22dee9ae523fc"
],
[
"Hacl.Impl.Matrix.matrix_eq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_07aead5b1239d489c2a97b2236b5f3e4",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"dab8415c5a2b67a25879c6639daeff14"
],
[
"Hacl.Impl.Matrix.matrix_eq",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Spec.Matrix.fold_land_.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Spec.Matrix.fold_land_.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Spec.Matrix_interpretation_Tm_ghost_arrow_7f147d2788753c34e2959b31ed04dc51",
"Spec.Matrix_interpretation_Tm_ghost_arrow_e032ca87e35fff8d204160e6f15b42b9",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion",
"bool_typing", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_stack_region",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.eq_u32_m",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.bget", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies0",
"equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Matrix.matrix",
"equation_Spec.Matrix.matrix_eq",
"equation_Spec.Matrix.matrix_eq_fc",
"equation_with_fuel_Spec.Matrix.fold_land_.fuel_instrumented",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_f2738f059364540e4bcc5f3fff4dccc4",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.Buffer.bget_as_seq",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_07aead5b1239d489c2a97b2236b5f3e4",
"refinement_interpretation_Tm_refine_0b3b95729ce4407a30fc6bb91a1c8b61",
"refinement_interpretation_Tm_refine_0cc7d9611cbdaac83bcefb0ee6ef1ec1",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1c4c894037978a46f04bad691f583c43",
"refinement_interpretation_Tm_refine_1cc24a6bb7b92ee9a0e43bec06a41846",
"refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_40bf2b419500cd4bde698958b5e5cfa6",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a17ca0fec24af3ab020dad6cf70b4d1",
"refinement_interpretation_Tm_refine_5e9816ed25f94a959ae51315ca569319",
"refinement_interpretation_Tm_refine_7a58fbf297e388448152b41221903b6a",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a5c1b398f96e3506835dfbe23f668463",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_e09ac1e03ed499f31d54287f6f871030",
"refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_interpretation_Tm_refine_febe7e5dfb824f85118cae5eb51a98a5",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.includes",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.is_stack_region",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Hacl.Impl.Matrix.eq_u32_m", "typing_Lib.Buffer.as_seq",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.create",
"typing_Lib.Sequence.upd", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Spec.Matrix.fold_land_", "typing_Spec.Matrix.matrix_eq",
"typing_Tm_abs_f2738f059364540e4bcc5f3fff4dccc4",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c140bd7461daa7cf3253eaa2c9405cff"
],
[
"Hacl.Impl.Matrix.matrix_to_lbytes",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_lemma",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3aeafd20544c9c70f5dfdd2fa9ae7379",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.v",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ceead35e73a40fa512db9e9920b1cb4e"
],
[
"Hacl.Impl.Matrix.matrix_to_lbytes",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_Lib.IntTypes.uint16", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_lemma",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3aeafd20544c9c70f5dfdd2fa9ae7379",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"bedbbe7347c86f01f99c7be5ce327b35"
],
[
"Hacl.Impl.Matrix.matrix_to_lbytes",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"eq2-interp", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Matrix.matrix_to_lbytes_fc",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.Buffer.as_seq_gsub", "lemma_Lib.Buffer.modifies_sub",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1cc24a6bb7b92ee9a0e43bec06a41846",
"refinement_interpretation_Tm_refine_2330446138ca298f4519c894bc7c7361",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2ba455cded01fe132ebc2be46029f848",
"refinement_interpretation_Tm_refine_2be61a6a6aedcd196600c72c82df482a",
"refinement_interpretation_Tm_refine_2ddc5df8817091057d11dad9867e2611",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_3aeafd20544c9c70f5dfdd2fa9ae7379",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5b4b5258a4e6c216af70c2b4f014758a",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6cc5283c05af82d0831a60faf76593eb",
"refinement_interpretation_Tm_refine_755601d434c2ff65e9ec125d063243ce",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b4bf4b5b4548c72164aa59d91568d7c3",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e687bb4502d4c881edb4f236ffbdb1ab",
"refinement_interpretation_Tm_refine_e9c32a5fb00a4e8c339597118c871180",
"refinement_interpretation_Tm_refine_eab17cd9193c0faa80db7d81d9631553",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "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.UInt32.v",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.mul",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.mgsub",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"bccc37e1d34d9288a0ed3e6d91f4f7ef"
],
[
"Hacl.Impl.Matrix.matrix_from_lbytes",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.matrix_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint16",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.mul_lemma", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3aeafd20544c9c70f5dfdd2fa9ae7379",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.v",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"20a66da929927b75a6f5a23c5af49167"
],
[
"Hacl.Impl.Matrix.matrix_from_lbytes",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Impl.Matrix.lbytes", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_Lib.IntTypes.uint8", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_lemma",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3aeafd20544c9c70f5dfdd2fa9ae7379",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.mul",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"cf34090c660442d9600aa6847d1c46c0"
],
[
"Hacl.Impl.Matrix.matrix_from_lbytes",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"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_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.bget", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Matrix.matrix",
"equation_Spec.Matrix.matrix_from_lbytes_fc",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.Buffer.bget_as_seq", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.Sequence.eq_elim",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_198934f9ebf7e718b739cb483e272175",
"refinement_interpretation_Tm_refine_1cc24a6bb7b92ee9a0e43bec06a41846",
"refinement_interpretation_Tm_refine_1de8426f4795d59a42df9b22a452f23d",
"refinement_interpretation_Tm_refine_2330446138ca298f4519c894bc7c7361",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2ba455cded01fe132ebc2be46029f848",
"refinement_interpretation_Tm_refine_3aeafd20544c9c70f5dfdd2fa9ae7379",
"refinement_interpretation_Tm_refine_438c210de76097b1830aaecb71cf2a85",
"refinement_interpretation_Tm_refine_46522970f608b2fc0d1417e9d1a5c633",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5b4b5258a4e6c216af70c2b4f014758a",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_755601d434c2ff65e9ec125d063243ce",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_b36e5fc941aaa7366d8f31f0e02b4e03",
"refinement_interpretation_Tm_refine_b4bf4b5b4548c72164aa59d91568d7c3",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.mul",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.sub", "typing_Lib.Sequence.upd",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"29ea759efc33206b6a3ae3b876e530e7"
]
]
]
Computing file changes ...
