[
  "'Éø»–VŸµ‹®\u0014¯ÒÕ\u0007'",
  [
    [
      "Spec.Matrix.index_lt",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "845e4fcd1983cc1f08a4794d73076c63"
    ],
    [
      "Spec.Matrix.index_neq",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "46a0403ca2450b81988f6b5b1b9dc1f4"
    ],
    [
      "Spec.Matrix.index_neq",
      2,
      0,
      4,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok",
        "unit_inversion", "unit_typing"
      ],
      0,
      "2feb36401d705abe0d5e235f6b5433ac"
    ],
    [
      "Spec.Matrix.matrix",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99"
      ],
      0,
      "552098fe867df62f043b06132816b9c5"
    ],
    [
      "Spec.Matrix.create",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "equality_tok_Lib.IntTypes.U16@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U16@tok"
      ],
      0,
      "58b3717b32c75eb5455a4b1d220269f9"
    ],
    [
      "Spec.Matrix.mget",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint16",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Spec.Matrix.matrix",
        "function_token_typing_Lib.IntTypes.uint16",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "9c62bd49bfb86c2f3c8d2a4014c5e4da"
    ],
    [
      "Spec.Matrix.mset",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_f37327594b97f54132ce6bcb98ee4847", "int_inversion",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_kinding_Tm_refine_f37327594b97f54132ce6bcb98ee4847"
      ],
      0,
      "7c0467971122ace7a69a50ab16aecafc"
    ],
    [
      "Spec.Matrix.mset",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
        "equation_Lib.IntTypes.uint16", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.Matrix.matrix",
        "equation_Spec.Matrix.mget",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7c173c477b61fc4972425b59a911ff66",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "081e8ce51732dbb1e0dfe2f32cc0a15c"
    ],
    [
      "Spec.Matrix.extensionality",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "5f6de3ccb616f985374ff84e75022b23"
    ],
    [
      "Spec.Matrix.extensionality",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Spec.Matrix.mget",
        "function_token_typing_Lib.IntTypes.uint16", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_882c2b73cedb5ab008c3e9869165e7b2",
        "refinement_interpretation_Tm_refine_9476506d315d3fd36075ba27c438d57c",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.Sequence.index", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c32c2bdcf8de743a903dfdb0aff93435"
    ],
    [
      "Spec.Matrix.map",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b0e6906cffa68699a53afe6c17007c68"
    ],
    [
      "Spec.Matrix.map",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
        "refinement_interpretation_Tm_refine_483d65c37027744c7724b9a9b5acef84",
        "refinement_interpretation_Tm_refine_4cee3d64fe11745be301c4e1f6e0cc59",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b8a8524b6258366679de83172865ab2",
        "refinement_interpretation_Tm_refine_7404a9516dc78fa92282e4e24ca2e81c",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_Spec.Matrix.mset"
      ],
      0,
      "871ac221ac4b6508223fb704e2714592"
    ],
    [
      "Spec.Matrix.mod_pow2_felem",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f8e0a0c79ba1f336cf1dc7e419f92c98"
      ],
      0,
      "55b9883780bad27e16c5892c51066bd3"
    ],
    [
      "Spec.Matrix.mod_pow2_felem",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "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_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.mod_mask",
        "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", "int_inversion", "int_typing",
        "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.shift_left_lemma",
        "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.sub_mod_lemma",
        "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int",
        "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_0d47d71dc69930ad5481218da3e1d668",
        "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605",
        "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_a636b6491af501737c1eb06142217342",
        "refinement_interpretation_Tm_refine_caa10a11cf25c9029f6782cc574ef309",
        "refinement_interpretation_Tm_refine_f8e0a0c79ba1f336cf1dc7e419f92c98",
        "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53",
        "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.v",
        "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,
      "c9f50ff1f8e1a0310f570e136304ad70"
    ],
    [
      "Spec.Matrix.mod_pow2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_65e71441a9c851e4a25ea14f8e0e8f2e",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "1a171777c253ef9efa4a86fcd92bc0cc"
    ],
    [
      "Spec.Matrix.mod_pow2",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Spec.Matrix_interpretation_Tm_arrow_5330dab7bf94017f8b99d527dce2572f",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U16@tok", "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",
        "equation_Prims.pos", "equation_Spec.Matrix.mget",
        "function_token_typing_Spec.Matrix.mod_pow2_felem", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_65e71441a9c851e4a25ea14f8e0e8f2e",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_bbba8ab4d609330287c6a2fda1069130",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_Lib.IntTypes.v", "typing_Prims.pow2",
        "typing_Spec.Matrix.mget", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U16@tok"
      ],
      0,
      "dc666eb09648f5dad21c02cb9872bc1f"
    ],
    [
      "Spec.Matrix.map2",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "bf5382964b711d658b8ebba8d8e82a33"
    ],
    [
      "Spec.Matrix.map2",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
        "refinement_interpretation_Tm_refine_4cee3d64fe11745be301c4e1f6e0cc59",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b8a8524b6258366679de83172865ab2",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_9760814588e7eb2f8a7b2bd420efb54b",
        "refinement_interpretation_Tm_refine_b0faad0d459bb289468c283eb08b0841",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_f153ee7330c79f829c6592441bbe5c1e",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_Spec.Matrix.mset"
      ],
      0,
      "450d7bd2501bab887373a2c995617d5b"
    ],
    [
      "Spec.Matrix.add",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d57183bda6a1f1bf135799e8b1944df6"
    ],
    [
      "Spec.Matrix.add",
      2,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "1c93ae63b2194615c573b4e8e9976e3b"
    ],
    [
      "Spec.Matrix.sub",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "fa9835a92e24ad239e2cdc6149d0a393"
    ],
    [
      "Spec.Matrix.sub",
      2,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "cb207e42f59ef791a17415d7e79cca01"
    ],
    [
      "Spec.Matrix.sum_",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_093e9645ca082d559ab78544838239ca_2",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U16@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_50f098917d7c53f3ac6b56cab8191c7a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U16@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "183bba9c39190734ba4cfff2aa113799"
    ],
    [
      "Spec.Matrix.sum",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "2cfeb055bee6e8d521999dfaafdc2f40"
    ],
    [
      "Spec.Matrix.sum_extensionality",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "ced312a2f47a75191e2381e03addb7b0"
    ],
    [
      "Spec.Matrix.sum_extensionality",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Matrix.sum_.fuel_instrumented",
        "@fuel_irrelevance_Spec.Matrix.sum_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.Matrix_interpretation_Tm_ghost_arrow_4f21e107f4a12dcb14db84bfaf03c162",
        "Spec.Matrix_interpretation_Tm_ghost_arrow_72bbfb83a25d926183af1873807265fe",
        "binder_x_093e9645ca082d559ab78544838239ca_3",
        "binder_x_12157b724a07e6e39a1f6d49f9567881_0",
        "binder_x_d7f008a7aa7b14357ae92f40c0bc9035_1",
        "binder_x_d7f008a7aa7b14357ae92f40c0bc9035_2",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_with_fuel_Spec.Matrix.sum_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_32de15bbdf930f3a15b7cf5febb67c74",
        "refinement_interpretation_Tm_refine_3a6887d05f91540faea098745de7c6a8",
        "refinement_interpretation_Tm_refine_50f098917d7c53f3ac6b56cab8191c7a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a5c1b398f96e3506835dfbe23f668463",
        "well-founded-ordering-on-nat"
      ],
      0,
      "97e7730723d8ceae370e10b701e69dbd"
    ],
    [
      "Spec.Matrix.mul_inner",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "bf4fdf0a7af4f96e92eaf9ca7c341787"
    ],
    [
      "Spec.Matrix.mul_inner",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "d431294e2a2e8f95414e13f3d476c7ae"
    ],
    [
      "Spec.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_Spec.Matrix.sum_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.Matrix_interpretation_Tm_arrow_ec57fde4b7a9a13e58c910f2ef201144",
        "Spec.Matrix_interpretation_Tm_ghost_arrow_72bbfb83a25d926183af1873807265fe",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Matrix.sum",
        "equation_with_fuel_Spec.Matrix.sum_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_453267344f82e1b6d37de1fc30a4036b",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a0ae1dfde4252f372c00bdba2fc0d4ac",
        "refinement_interpretation_Tm_refine_a5c1b398f96e3506835dfbe23f668463",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d7f99d590f0c25ba2bfcada65fc92a05",
        "refinement_interpretation_Tm_refine_db646dcf75351678d2dc34a8c1094861",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U16@tok"
      ],
      0,
      "ef80de637cd30a8d9b0d884a55abfc69"
    ],
    [
      "Spec.Matrix.mul",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "3bb24fe8ba49467b16998146b8a36043"
    ],
    [
      "Spec.Matrix.mul",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "2dc449babc089d040afcf38b6e94ab61"
    ],
    [
      "Spec.Matrix.mul",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_Addition", "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_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
        "refinement_interpretation_Tm_refine_4cee3d64fe11745be301c4e1f6e0cc59",
        "refinement_interpretation_Tm_refine_53fc45d5894b161164501923be44c579",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b8a8524b6258366679de83172865ab2",
        "refinement_interpretation_Tm_refine_7d8a076287ad1f8e9211c49d92a0bac5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_a794ba8c5a9d27d39131ac273522ce03",
        "refinement_interpretation_Tm_refine_b53e627c3e02c51c40ebdfdeccb5e05a",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d7f99d590f0c25ba2bfcada65fc92a05",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_Spec.Matrix.mset"
      ],
      0,
      "274e1ee9b2b7e039e4e5c4723b1c6c42"
    ],
    [
      "Spec.Matrix.mget_s",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Spec.Matrix.matrix",
        "function_token_typing_Lib.IntTypes.uint16", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "112dd72ede2144524d39325f8dd3f88b"
    ],
    [
      "Spec.Matrix.mul_inner_s",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "1228c6040c467598973ddc50422c668b"
    ],
    [
      "Spec.Matrix.mul_inner_s",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "dbb24570a5be323041356f88e53eb00e"
    ],
    [
      "Spec.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_Spec.Matrix.sum_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.Matrix_interpretation_Tm_arrow_ec57fde4b7a9a13e58c910f2ef201144",
        "Spec.Matrix_interpretation_Tm_ghost_arrow_72bbfb83a25d926183af1873807265fe",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Matrix.sum",
        "equation_with_fuel_Spec.Matrix.sum_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_58142bfbfb21cff22f9bcfb515bbb252",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_2c67327e0ffeba8c213e18d247270c72",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a5c1b398f96e3506835dfbe23f668463",
        "refinement_interpretation_Tm_refine_ac12ac63cda1392d0b8d27d6d0def6ef",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d7f99d590f0c25ba2bfcada65fc92a05",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U16@tok"
      ],
      0,
      "161539faa16df366899c0c225c172b32"
    ],
    [
      "Spec.Matrix.mul_s",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "7bc493ff364d1e5011c3c77438c7cdef"
    ],
    [
      "Spec.Matrix.mul_s",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "59a1435cb30e2a4fb8f2b9019ef2bf5c"
    ],
    [
      "Spec.Matrix.mul_s",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_Addition", "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_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
        "refinement_interpretation_Tm_refine_4aff57a09b3abce700befe397fb52d66",
        "refinement_interpretation_Tm_refine_4cee3d64fe11745be301c4e1f6e0cc59",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b8a8524b6258366679de83172865ab2",
        "refinement_interpretation_Tm_refine_67e763cef56491483f5501153ae57759",
        "refinement_interpretation_Tm_refine_7d8a076287ad1f8e9211c49d92a0bac5",
        "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d7f99d590f0c25ba2bfcada65fc92a05",
        "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
        "refinement_interpretation_Tm_refine_fc0570ce2ee7f1839913e29e94b6636c",
        "typing_Spec.Matrix.mset"
      ],
      0,
      "bdf42c745743e1f54b903f805ca202c0"
    ],
    [
      "Spec.Matrix.matrix_eq",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.S128",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U16@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint16", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "primitive_Prims.op_Addition", "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_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
        "refinement_interpretation_Tm_refine_d33ac66dd71b06e106d5322f93f4449f",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.minint",
        "typing_Lib.IntTypes.zeros", "typing_Lib.Sequence.sub",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U16@tok"
      ],
      0,
      "498fdb063bc73e9638d74a8c2d680f11"
    ],
    [
      "Spec.Matrix.matrix_to_lbytes_f",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "29968ce90273577423fe52c3bdc86bb4"
    ],
    [
      "Spec.Matrix.matrix_to_lbytes_f",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "fdd7644fbd442f489fa44b5830663107"
    ],
    [
      "Spec.Matrix.matrix_to_lbytes_f",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "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_57d7c64afe8356b54a2af469d7a5eec1",
        "refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "b175ef63d365707af4579eb497339edd"
    ],
    [
      "Spec.Matrix.matrix_to_lbytes",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Spec.Matrix.matrix",
        "function_token_typing_Lib.IntTypes.uint16",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "67c7efef9c5782c87232ec738d07c082"
    ],
    [
      "Spec.Matrix.matrix_to_lbytes",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5a1d930845a0ce0146ad530cad7c78be"
    ],
    [
      "Spec.Matrix.matrix_to_lbytes",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint16", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "01253b46ccc1edb4eee0f1d037566ecb"
    ],
    [
      "Spec.Matrix.matrix_from_lbytes_f",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1"
      ],
      0,
      "cf05984754db6a565933c18b7c270d58"
    ],
    [
      "Spec.Matrix.matrix_from_lbytes_f",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "3d1db75cccee119cc17e7fe6d2e025e2"
    ],
    [
      "Spec.Matrix.matrix_from_lbytes_f",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "7130d6ea1b0e80d1fca82cd0a94ef493"
    ],
    [
      "Spec.Matrix.matrix_from_lbytes",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1",
        "refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "df906fbc1f5091c61b8f4d63d80602d4"
    ],
    [
      "Spec.Matrix.matrix_from_lbytes",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "1c6c2b9a82ddcc77e736b1e31c13beda"
    ],
    [
      "Spec.Matrix.matrix_from_lbytes",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Spec.Matrix.matrix",
        "equation_Spec.Matrix.matrix_from_lbytes_fc",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_57d7c64afe8356b54a2af469d7a5eec1",
        "refinement_interpretation_Tm_refine_5b8a8524b6258366679de83172865ab2",
        "refinement_interpretation_Tm_refine_6f77474ede8199333d3f4de9c694b4b9",
        "refinement_interpretation_Tm_refine_7db9169b18269449a9ef4bfa9739eb9c",
        "refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.Sequence.upd", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c6047d6d8d2070e314dda5b756187082"
    ]
  ]
]