Skip to main content

Browse the archive

Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC 
Attempt to set environment correctly for Windows
 
Co-authored-by: @protz
1 parent ca37fbf
Raw File
Spec.P256.Normalisation.fst.hints 
[
  "��ˢX\u001f�X\tVsJ���",
  [
    [
      "Spec.P256.Normalisation.lemma_norm_as_specification",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.P256.Definitions.prime256",
        "equation_Spec.P256.Normalisation.prime",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Prims.pow2"
      ],
      0,
      "fe1cb862c1f8088357d78713530d3b59"
    ],
    [
      "Spec.P256.Normalisation.lemma_norm_as_specification",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.P256.Definitions.prime256",
        "equation_Spec.P256.Normalisation.prime",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "0df57e452ef53e6c2b1560be0c9f1207"
    ],
    [
      "Spec.P256.Normalisation.lemma_norm_as_specification",
      3,
      2,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.P256.Definitions.prime256",
        "equation_Spec.P256.Lemmas.modp_inv2_pow",
        "equation_Spec.P256.Normalisation.prime", "equation_Spec.P256._norm",
        "equation_Spec.P256.isPointAtInfinity",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "equation_with_fuel_Spec.P256.Lemmas.pow.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_15ee4b6ca6124261eed673db98456b79",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_63a4f630760342b5b6b2edf3ff6a1313",
        "refinement_interpretation_Tm_refine_756d6d7488d671a60fd5fd35e51c7a75",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "token_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
        "typing_Prims.pow2"
      ],
      0,
      "93258afbf839d33796db718a11b3893e"
    ]
  ]
]
back to top